/[mojave]/metaprl/theories/itt/itt_logic.ml
ViewVC logotype

Log of /metaprl/theories/itt/itt_logic.ml

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 7950)

Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 1 month ago) by nogin
File length: 50885 byte(s)
Diff to previous 3444
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.


Revision 3444 - (view) (download) (annotate) - [select for diffs]
Modified Thu Nov 15 23:03:47 2001 UTC (19 years, 7 months ago) by nogin
File length: 50886 byte(s)
Diff to previous 3347
Code cleanup:

I looked (using the code I've put into macro.ml) for places where the same code
appeared in several branches of a match or function expression. I changed those
places to use a complex pattern and a single copy of the code.


Revision 3347 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 25 20:21:35 2001 UTC (19 years, 10 months ago) by nogin
File length: 50944 byte(s)
Diff to previous 3334
I rewrote itt_collection using my "better_tt" ideas and proved all the
theorems in that theory.


Revision 3334 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 15 07:01:49 2001 UTC (19 years, 11 months ago) by nogin
File length: 50412 byte(s)
Diff to previous 3329
When a bound variable already exists in the goal, it should not be
supplied in the rule argument to prevent it from being renamed.


Revision 3329 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 13 21:34:19 2001 UTC (19 years, 11 months ago) by nogin
File length: 50424 byte(s)
Diff to previous 3315
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theories.


Revision 3315 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 5 21:15:43 2001 UTC (19 years, 11 months ago) by nogin
File length: 50428 byte(s)
Diff to previous 3313
I have changed the way autoT works.

Now autoT and trivialT share the same auto_resource. When a new tactic is
added to auto_resource, the auto_flag provides information on how to use the
tactic:
- AutoTrivial - use in trivialT; use in autoT before other tactics
- AutoNormal - use in autoT after AutoTrivial tactics
- AutoComplete - use in autoT after AutoTrivial and AutoNormal; use only
if autoT can prove all the genarated subgoals.

I added a few tactics to autoT with AutoComplete flag:
- dT elimination rules (but only when dT will do the thinning)
- JProver with multiplicity 1 (with some assumptions magic); use jAutoT i
to get an autoT version that will run JProver with multiplicity i intead of 1.

I added a flag AutoMustComplete to intro resource flags. This flag takes the
rule to AutoComplete level instead of the usual AutoNormal.

The new autoT no longer does backThruHypT and backThruAssumT (other than through
JProver). I added a new tactic logicAutoT that will do backThruHypT
and backThruAssumT in addition to normal autoT functionality.


Revision 3313 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 4 15:52:29 2001 UTC (19 years, 11 months ago) by nogin
File length: 48707 byte(s)
Diff to previous 3311
Made var_subst a little more general.
This fixes another bug that was affecting JProver.


Revision 3311 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 3 23:12:24 2001 UTC (19 years, 11 months ago) by nogin
File length: 48815 byte(s)
Diff to previous 3305
JProver shouldn't do "make_opname" all the time.


Revision 3305 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 1 20:27:30 2001 UTC (19 years, 11 months ago) by nogin
File length: 48701 byte(s)
Diff to previous 3304
Moved nthAssumT from Itt_struct to Itt_squash and made it do
sequent squashing/unsquashing as needed to match the assumption.


Revision 3304 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 30 03:22:54 2001 UTC (19 years, 11 months ago) by nogin
File length: 49013 byte(s)
Diff to previous 3302
Added num_assums and nth_assums to Refine and Sequent.


Revision 3302 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 29 23:06:26 2001 UTC (19 years, 11 months ago) by nogin
File length: 49172 byte(s)
Diff to previous 3293
Added a functionality to be able to limit JProver's maximal multiplicity level.


Revision 3293 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 11:13:06 2001 UTC (19 years, 11 months ago) by nogin
File length: 49002 byte(s)
Diff to previous 3281
Fixed a few proofs.


Revision 3281 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 13:56:53 2001 UTC (20 years ago) by nogin
File length: 49236 byte(s)
Diff to previous 3276
The redundant "_resource" suffix should not be used in resource names.


Revision 3276 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 19 15:17:10 2001 UTC (20 years ago) by nogin
File length: 49776 byte(s)
Diff to previous 3257
Added support for the following syntax of resource improvement:
let resource name += expr
and
let resource name += [ expr1; expr2; ...; exprn ]


Revision 3257 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 13 19:32:30 2001 UTC (20 years ago) by kopylov
File length: 50364 byte(s)
Diff to previous 3255
1. I added new primitive rules:
     Itt_struct.exchange
     Itt_pointwise.hypSubstPointwise
     Itt_pointwise.contextSubstPointwise

   The last two rules show the differences between pointwise and pairwise functionality.
   They are valid in pointwise functionality (as well as quoationtElimination2).

2. Itt_struct3 contains some rules that derived from these new ones.
   But thesd rules are valid in both functionalities.

3. I moved definition of natural numbers to a new theory Itt_nat.
   To prove induction for natural numbers one needs Itt_struct3.
   I almost proved it (leaving some simple arithmetic subgoals, that should
   be killed by arith)

4. I defined record type.
   Itt_record is a main theory of records.
   Itt_record_exm contains some examples.

5. I add a new conversion
        * applyAllC : conv list -> conv
   that applies all conversions to all subterms and a tactic
        * rwa : conv list -> int -> tactic
        = rw (applyAllC convs)


Revision 3255 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 8 19:24:25 2001 UTC (20 years ago) by kopylov
File length: 50130 byte(s)
Diff to previous 3252
moveToConlT is fixed


Revision 3252 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 5 22:41:19 2001 UTC (20 years ago) by nogin
File length: 50135 byte(s)
Diff to previous 3246
Fixed squash_resource annotations for empty types.


Revision 3246 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 1 20:57:31 2001 UTC (20 years ago) by kopylov
File length: 50151 byte(s)
Diff to previous 3238
- The theory ctt_markov (Constructive type theory with Markov
  Principle) is added.

- Some definitions and simple facts are added to itt_int_ext


Revision 3238 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 27 18:08:16 2001 UTC (20 years ago) by nogin
File length: 50147 byte(s)
Diff to previous 3235
I rewrote the Itt_squash tactics and the squash_resource implementation
and made sure most of the theories expand.

- I implemented squash_resource annotations - see documentation for
more information
- autoT will now always attempt to squash the sequent and unsquash all
the hypotheses

Left to do:
- Update the documentation, especially the itt_quickref.txt
- Itt_collections would not expand, but I was planning to rewrite it anyway,
so it does not make sense to try fixing the current version.
- Itt_fset would not expand, it needs lots of work, including (preferably)
some improvements to autoT (not squash-related).


Revision 3235 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 20 23:04:08 2001 UTC (20 years, 1 month ago) by nogin
File length: 50337 byte(s)
Diff to previous 3232
Display form fixes.

- TeX: all object-level terms (theorem statements, etc) are now typeset
in math mode.

- Tex: variable names are now parsed to detect indeces. In particular,
  'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}.

- Tex: `|' symbol in display forms is now always handled correctly.

- Numerous small fixes.


Revision 3232 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 17 22:06:20 2001 UTC (20 years, 1 month ago) by nogin
File length: 50321 byte(s)
Diff to previous 3223
I joined Itt_hide and Itt_squash into a single theory - Itt_squash that deals
with both the meta-level squash operator (Base_trivial!squash{}) and the type
theory squash operator (Itt_squash!squash{'A}). This makes sense because
these two operators are almost exectly the same in nature except for oe
being a meta-level operator and another - an object-level one.

This commit also renames Itt_hide!hide into Itt_squash!squash. This means
that we now have two operators named "squash", however this should not cause
any confusion since all part of the system (including the parser and display
form mechanism) take into account the number of arguments.

Warning: This commit probably broke lots of proofs. I plan to fix that
after I have a chance to rewrite the squash theory a little better (for
now I just copied the one from Itt_hide). Hopefully, I should have it
done within a week.


Revision 3223 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 23:59:11 2001 UTC (20 years, 1 month ago) by nogin
File length: 50319 byte(s)
Diff to previous 3074
Finally, I am able to commit what I was getting to
in all these commits over the last several days.

I changed the parser to index declared opnames by its "shape" -
last string of opname + parameter types + subterm arities
instead of just the last string (as it used to be). This means that
the parser now checks whether the usage of an opname corresponds
to its declaration. This allowed me to detect numerous typos in
display forms and even some rules and rewrites and, hopefully,
will prevent people from making such typos in the future.

This is only the first pass of the implementation. I still need to:
- make sure none of my fixes broke any display forms that used to work
  because of typos cancelling each other
- update the documentation
- implement checking of shapes on the opnames specified using the
  Module!name notation (currently no checking is done on such opnames)


Revision 3074 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 24 00:46:18 2000 UTC (20 years, 8 months ago) by jyh
File length: 50311 byte(s)
Diff to previous 3058
Update Itt_logic/implies_df to a nested dform (so it displays recursive
implications correctly).  Also, fixed a bug in rformat.ml that was causing
the formatter to calculate the left margin correctly.

I also forgot to mention two new things earlier.  I added the
cbreak [s1:s; s2:s] display form, which adds a break if the next text
element would overlow the right margin.  This is useful in text formatting.
The s1 and s2 are optional; cbreak <--> cbreak[""; " "].  Also, there
is now a display form pushm[str:s], which adds the text in every
indentatio, rather than whitespace.  This is useful for comment formatting,
where the comment lines are indented with the " * " string.


Revision 3058 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 20:41:19 2000 UTC (20 years, 9 months ago) by jyh
File length: 50045 byte(s)
Diff to previous 3056
Last commit failed partway through...


Revision 3056 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 4 17:09:49 2000 UTC (20 years, 9 months ago) by cwitty
File length: 38789 byte(s)
Diff to previous 3050
Started changing declare/prim_rw to define (as in TODO 2.01.2).
Also fixed an unsoundness in itt_dprod.ml where fst{} had two definitions:

 prim_rw unfoldFst : fst{'e} <--> spread{'e; u, v. 'u}
 prim_rw unfoldSnd : fst{'e} <--> spread{'e; u, v. 'v}


Revision 3050 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 20 01:40:18 2000 UTC (20 years, 10 months ago) by nogin
File length: 39058 byte(s)
Diff to previous 3048
- I added my personal TODO file that contains a list of things
that I am considering doing with/in/about/around MetaPRL

- I fixed the display form modes in ITT!!!
1) I added the except_mode[...] display form option. It is opposite
to the mode[...] option. The main idea was to be able to say
except_mode[src]
2) I made sure all the display forms in ITT (and below it, except for
Ocaml) are annotated with proper mode and except_mode options.
3) I added (in one of the previous commits) the  set_dfmode
command to MetaPRL toploop. Now  set_dfmode "src"  can be used
to produce terms in a form suitable for cutting and pasting into
.ml files and command line tactic arguments.
4) I updated the documentation accordingly.


Revision 3048 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 16 07:29:04 2000 UTC (20 years, 10 months ago) by nogin
File length: 39460 byte(s)
Diff to previous 3042
Fixed some mess with dispaly forms. But we still need to implement mode generality,
sets of modes (or at least something like mode[all except src] flag)
and make sure that the modes are correct on all the dforms.


Revision 3042 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 9 23:54:39 2000 UTC (20 years, 10 months ago) by nogin
File length: 39600 byte(s)
Diff to previous 3020
Got rid of Itt_equal!member.
----------------------------

Now the only way to represent membership in ITT is to use << equals{T;x;x} >>
To avoid extra typing, this can be typed as << x IN T >> (note that "IN" has
to be capitalized here, while in << x=x in T >> it has to be lowercase).

I updated the rules and tactics approprially. I also updated itt_quickref.txt
(Although I have not checked whether the original text was correct and if it was
not, my modifications could also be incorrect).

I reexpanded all the proofs. Most worked correctly, except for the following:
- Some proofs were nonexistant or incomplete even before my changes.
- Itt_fset is very outdated and would not expand without some major effort.
- Many proofs in Itt_collection are broken because of heavy reliance on tatcics
that need term arguments that were broken by the variable naming bug (BUGS 3.11).
I am not sure whether it's the only problem with Itt_collection (probably not).


Revision 3020 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 29 21:13:29 2000 UTC (20 years, 11 months ago) by nogin
File length: 41825 byte(s)
Diff to previous 3015
assumT shouldn't run assertT when the conclusion is already what we want.


Revision 3015 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 14 23:15:39 2000 UTC (21 years ago) by nogin
File length: 41831 byte(s)
Diff to previous 3014
I reformatted the TODO file from Emacs "outline" mode to a numbered text file.
We want to have numbers so that we can refer to items.

When items are added to or removed from BUGS and TODO files, we should not do
any renumbering to make sure the numbers stay the same.

Fixed a small problem with ITT <-> Jprover interface.


Revision 3014 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 13 06:16:19 2000 UTC (21 years ago) by nogin
File length: 41828 byte(s)
Diff to previous 3009
I wrote a proof tree normalization that tries to eliminate unnecessary nodes
in the proof tree and makes "deep" proof browsing much more
plesent.

Currently this is probably a little inefficient since it' too eager and
the results are not always saved. To fix this, we'll need to make Tactic_boot extracts
mutable so that we could do normalization (and other operations) properly lazily.

Other small changes.


Revision 3009 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 9 22:15:36 2000 UTC (21 years ago) by nogin
File length: 41695 byte(s)
Diff to previous 3008
Small Jprover<->MetaPRL interface fix - do not thin out universal
quantifier on instantiation.


Revision 3008 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 9 19:31:49 2000 UTC (21 years ago) by nogin
File length: 41602 byte(s)
Diff to previous 3007
Added iff handling for Jprover and Barber example


Revision 3007 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 8 11:55:06 2000 UTC (21 years ago) by nogin
File length: 41452 byte(s)
Diff to previous 3001
Smarter type inference algorithm capable of doing things like

# ti <<lambda{x.spread{'x;u,v.it}}>>;;
- : Refiner.Refiner.Refine.term = x:(Top X Top) --> Unit


Revision 3001 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 31 02:53:36 2000 UTC (21 years ago) by nogin
File length: 41969 byte(s)
Diff to previous 2997
Fixed a nasty bug in Jprover (after chaising it with Stephan for couple of hours)

Fixed a bug in the MetaPRL-Jprover interface.

Imported some Jprover tests and examples.


Revision 2997 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 30 13:58:39 2000 UTC (21 years ago) by nogin
File length: 41712 byte(s)
Diff to previous 2995
The Jprover interface is almost finished. It's partially working, I just
need to write some hack for v0_jprover non-empty types hack.


Revision 2995 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 30 05:28:42 2000 UTC (21 years ago) by nogin
File length: 39001 byte(s)
Diff to previous 2992
Moved Jprover output parsing into the JLogic interface. Still need to write the
output parsing for ITT_JLogic.

Eliminated some excessive whitespace from jall.ml

Eliminated some unnecessary exception handling code from jall.ml


Revision 2992 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 26 13:16:40 2000 UTC (21 years ago) by nogin
File length: 38553 byte(s)
Diff to previous 2985
Replaced the free_vars function from TermSubst interface with free_vars_list
and free_vars_set that return string list and StringSet.t respectively.


Revision 2985 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 25 05:14:42 2000 UTC (21 years ago) by nogin
File length: 38555 byte(s)
Diff to previous 2926
Merged the unify_mm branch.


Revision 2926 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 5 22:28:23 2000 UTC (21 years, 2 months ago) by steph
File length: 38548 byte(s)
Diff to previous 2923

Full first order prover for J plus (incomplete) proof reconstruction
in LJ, LJmc and LK.
Moreover, jprover starts from sequent


Revision 2923 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 16 23:30:08 2000 UTC (21 years, 3 months ago) by lolorigo
File length: 38453 byte(s)
Diff to previous 2922
moved nuprl_jlogic module to sensible place


Revision 2922 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 16 19:52:02 2000 UTC (21 years, 3 months ago) by lolorigo
File length: 39029 byte(s)
Diff to previous 2921
added/improved functionality for metaprl/jprover/nuprl5 io


Revision 2921 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 13 23:03:12 2000 UTC (21 years, 3 months ago) by steph
File length: 38454 byte(s)
Diff to previous 2905
 ----------------------------------------------------------------------
 Enter Log.  Lines beginning with `CVS:' are removed automatically

 Committing in .

 Modified Files:
 	itt_logic.ml itt_logic.mli
 ----------------------------------------------------------------------


Revision 2905 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 22 05:39:46 2000 UTC (21 years, 4 months ago) by nogin
File length: 38405 byte(s)
Diff to previous 2885
Added a new function for free variable testing.
Renamed all the free variable testing functions for uniformity:
   val is_var_free : string -> term -> bool
   val is_some_var_free : string list -> term -> bool
   val is_some_var_free_list : string list -> term list -> bool

Made Strict rewriter checking use is_some_var_free (speedup!).


Revision 2885 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 17 22:13:44 2000 UTC (21 years, 4 months ago) by nogin
File length: 38405 byte(s)
Diff to previous 2880
Fixed the jtest function


Revision 2880 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 2 18:19:32 2000 UTC (21 years, 4 months ago) by steph
File length: 38396 byte(s)
Diff to previous 2822
*** empty log message ***


Revision 2822 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 22 01:07:59 1999 UTC (21 years, 8 months ago) by nogin
File length: 37734 byte(s)
Diff to previous 2808
Added new function to mp_debug
let show_loading s = if !debug_load then Printf.eprintf s eflush

and replaced all usages of debug_load with show_loading


Revision 2808 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 25 19:09:25 1999 UTC (21 years, 9 months ago) by jyh
File length: 37762 byte(s)
Diff to previous 2790
I added a TeX mode for display.  This was a quick hack, and it
it _not_ the way it should be done long term.  We should be able
to do the formatting and indentation with boxes, etc.

I added SIL.  This theory is an incomplete semantics of a
"simple imperative language."


Revision 2790 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 6 15:35:50 1999 UTC (21 years, 11 months ago) by nogin
File length: 37840 byte(s)
Diff to previous 2786
Changed genAssumT:

generalize all the assumtions that have the "member" goal, not only the first one,
do the usual assumT thing for non-member goals

After the generalization, prove the "main" subgoal automatically


Revision 2786 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 5 13:38:57 1999 UTC (21 years, 11 months ago) by jyh
File length: 38081 byte(s)
Diff to previous 2775
Added: Itt_logic.genAssumT : int list -> tactic
This tactical "generalizes" over a set of assumptions.  The first
assumption should be for a membership judgment.  For example:
   ...
i. H >- t in T list
   ...
j. H >- Q[t]
   ...
   H >- P[t]
   BY genAssumT [i; j]
1. H >- all l: T list. (Q[l] => P[l])
2. H; x: (all l: T list. (Q[l] => P[l])) >- P[t]


Revision 2775 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 13:13:44 1999 UTC (21 years, 11 months ago) by jyh
File length: 36560 byte(s)
Diff to previous 2773
Things seem to be working pretty smoothly now.  This is mostly minor
fixes.  Still need to fix the problems with the mp toploop.

    1. Proofs now use Alexey's ASCII format.  By default, proofs
       should be saved to CVS in .prla format.  You can generate ASCII
       files by using "make export", or you can use the "export ()"
       instead of the "save ()" command in the editor.  For speed,
       .prlb files are now saved in a raw, marshaled format.  When you
       edit a theory, the newest of .cmoz, .prlb, or .prla files is
       loaded.  There is a new command "convert" to convert between
       all the different proof file formats.
          convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
          raw: save the file in fast, raw format
	  term: save the file as <magic#>/<marshaled term_io>
	  lib: send the file to the Nuprl5 library
	  ascii: create a .prla file

       Developers: _please_ mention any changes to the basic data
          structures in your CVS logs.  The things that matter are:
          Refiner.Refiner.TermType.term
	  Filter_summary.summary_info
	  Tactic_boot_sig.TacticType.{tactic_arg,extract}
	  Proof_boot.io_proof

       Users: to be safe, save all your proofs using "make export"
          before doing a cvs update.

    2. "expand ()" and "expand_all ()" now work.  I also added
       "clean ()" and "clean_all ()" commands to remove those peasky
       dangling proof nodes when you are satisfied with a proof.  By
       default, proofs are saved only down to the innermost rule-box
       level, and primitive refinements are omitted.  I haven't added
       a "deep_save ()" command; it seems unecessary.

    3. Sorry, but I had to move theories/boot into the filter.  There
       are no major changes here, but the directory structure in
       filter has changed significantly.

    4. I added a THEORIES variable to the mk/config file that
       specifies what theories you want to compile.  This means that
       you don't have to edit all the Makefiles when you add a theory,
       and it also means that you can keep your own theories without
       having to commit them to cvs.


Revision 2773 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 03:02:58 1999 UTC (21 years, 11 months ago) by nogin
File length: 33929 byte(s)
Diff to previous 2753
I wrote a decideT tactic, similar to Nuprl4 Decide tactic.

We need to prove some decidability rules and add them to the decide_resource
in order to make this tactic useful.


Revision 2753 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 25 00:19:15 1999 UTC (22 years ago) by jyh
File length: 33982 byte(s)
Diff to previous 2743
These are some minor changes to make things work better.  Changed
meaning of ThinOption in elim_resource: it now means to thin the hyp
by default, unless overridden by thinningT false.

Fixed some proof operations.  Added "move_to_assum" command to take
the current subgoal and make it an extra assumption of the entire
proof (it may not work at the moment).

ls now takes a _string_ argument.  Use ls "u";; to display only the
unproved rules in the current module.

Proved many membership variants of the standard type constructors,
but there are a few more to go.  When you are defining theories, I
believe you should use membership, not equality.  After all, equality
is derivable from membership, and membership is a lot easier.

Still to go: ASCII format proof files; save proofs _without_ extracts
by default.  The expand () function does not reexpand proofs correctly.
A few problems with proof navigation.


Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 34004 byte(s)
Diff to previous 2677
This is a major release; I bumped the release number to 0.6.
WARNING: There are major changes here, and there may be problems
   with this version that prevent you from using your old proof.
   Save your work before using this version.
NOTE: If you decide to try this out, and you find problems,
   please(!) send me email so I can fix it.

Changes:
   1. The proof structure is totally changed, so that the proof
      editor edits the raw proof extracts.  This means that you
      can view the actions of the refiner down to the primitive
      rule applications.  In the proof editor, you can use
      "down 0" (or "cd "0") to descend into the proof of a rule box.
      Primitive proofs are called "extracts", and are labeled with
      brackets (like [extract]).  To expand the extract, use the command
      "unfold ()".  You should be able to get all the way down to
      the primitive rule/rewrite applications.

      This also means that the format of the proof files (the .prlb
      files) has changed.  The old proof files are still valid,
      but this is a hack and will be deprecated in the next
      few months.  I haven't yet added Alexey's ASCII proof
      files, but that will come with the next release.

      As usual, the "undo ()" command undoes the last proof step,
      including "unfold ()".  The "nop ()" command, reset the undo
      stack.  I also added a "redo ()" command that undoes the
      last undo.

      There is a simple rule-box proof cache for collecting proofs
      as you edit them.  If cached proofs are available, you will
      see them in brackets (like [* # * *]) on the status line.
      I haven't yet:( added the commands to use cached proofs.

   2. Refiner changes.  I added two new features: the "cutT <term>"
      tactic cuts in a new assumption.  Also, you can apply
      rewrites directly on assumptions, with the "rwc" and
      "rwch" operations, that take a clause argument.  Basically,
      this means that instead of folding the goal, you can unfold
      the assumption.  I believe this is sound; let me know if
      you think otherwise!

   3. Resource changes.  I added resource automation, built on
      the basic resource parsing Alexey added.  Ratherthan writing
      resource code for every rule, you can annotate most rules
      to generate the resource code directly.  You can see lots of
      examples in the Itt theory.  Basically, there are three useful
      resources annotations:
         intro_resource []: adds the rule as an introduction in dT
         intro_resource [SelectOption i]: adds to selT i dT
         elim_resource []: adds as an elimination rule to dT.
            This normally tries to thin the hyp that was eliminated.
         elim_resource [ThinOption]: don't thin the hyp

      Rules should be annotated with labels on their clauses,
      like [wf], [main], [assertion], etc.  This means that in
      most tactic aplcations, you no longer need to have the
      thenLT [addHiddenLabel "main"; ...] part.

      N.B.  This is the most likey parts of this release to
      cause problems, because I deleted most old resource code.

      Also, you can still write standard resource code, but there
      is no longer a d_resource--it has been broken into two parts:
      the intro_resource for application to goals, and elim_resource
      for application to hyps.

   4. The proof editor is multi-threaded, so you can work on multiple
      proofs simultaneously.  In the normal Emacs editor, this is
      no help for you.  But there is a new Java editor with the
      standard point-and-click interface, and it views the proof
      in HTML, with multiple windows etc.  The beautiful thing is
      that you can use display forms to add commands to edit windows.
      The sad thing is that I built it on NT, Java 1.2 is required,
      and I haven't tried the blackdown.org Java release on Linux.
      This editor is pending some bug fixes from Sun to get the
      fonts right (they call this a standard release?).

      In any case, here are the direct implications.  The display
      forms have an "html" mode.  The display form formatting in
      the module Rformat has been completely redone, but display
      _should_ be the same as it was before.

      It is likely that I will add an HTML dump, so we can send
      uneditable proofs around by email or on the web.  Check out
      the file theories/base/summary.ml to see some example HTML
      display forms.

      The other issue: your MetaPRL process starts a web server on
      YOUR local machine using YOUR process id on the "next" available
      TCP port, and it serves files only from the search path that you pass
      MetaPRL.  I realize that this has security implications.  This
      is necessary to get browser access to the working MetaPRL proof.
      Is this crazy?  Let me know your beliefs, religious or
      otherwise.

   5. There are numerous minor changes.  I redid parts of the WeakMemo,
      Term_header_constr, and TermHash.  The theories/tactic directory
      has been split into tactic/boot (which is not compiled by MetaPRL),
      and theories/tactic (which is).

Jason


Revision 2677 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 27 12:31:06 1999 UTC (22 years ago) by eli
File length: 43397 byte(s)
Diff to previous 2674
Fix some slot[lt]{...} and slot[le]{...} to use quotes.


Revision 2674 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 26 00:41:08 1999 UTC (22 years ago) by nogin
File length: 43365 byte(s)
Diff to previous 2669
I removed @ from the parameter syntax for meta-parameters. Now
[xxx:s] is parsed as a meta-string parameter (MString "xxx") and
["xxx":s] is parsed as a string parameter (Sting "xxx")

I also copied .cmoz files to .prlb files until I've reached a fixpoint.


Revision 2669 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 23 21:55:17 1999 UTC (22 years, 1 month ago) by jyh
File length: 43406 byte(s)
Diff to previous 2652
This is a major modification to how parameters are handled.
1. All level parmeters are now meta.  That is, univ[@i:l] is
   exactly the same as univ[i:l].  The rewriter handles
   lavel expressions, so matching with levels like
   univ[3 | i':l | j:l] should work correctly.

   The syntax still requires the @ for meta-parameter of
   other types.  For instance, token["hello world":t] is
   a normal token, and token[@"hello world":t] is a
   token with a meta-parameter.

2. There are no more parameter expressions.  For instance,
   the term natural_number[@i + @j] is not valid anymore.
   To replace them, the module theories/base/base_meta.ml
   defines ML rewrites that implement the same functionality.
   For example,
      meta_sum{number[12]; number[5]} --> number[17]

3. There is no term natural_number[@i:n] any more.  This was
   always a bad name, since it has always been possible for the
   parameter to be negative.

4. The Itt_equal.cumulativity rule is no longer defined as a
   side-condition.  It now uses Base_meta.meta_lt to define
   inclusion on level expression.  Cumulativity expansion
   should be performed automatically by the dT tactic.
   So:
      sequent ['ext] { ... >- univ[@i:l] = univ[@i:l] in univ[@j:l] }
      BY dT 0
   should always either succeed or fail, without producing
   subgoals.

I haven't fully tested the side-conditions.  As usual, let me know
if you see anything strange.  Next, I'm looking at the
rewriter free variable soundness problem.


Revision 2652 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 13 23:18:29 1999 UTC (22 years, 1 month ago) by kopylov
File length: 43481 byte(s)
Diff to previous 2629
1) Added a bug list into BUGS

2) Changed the keywords:
axiom -> rule  (.mli files)
primrw -> prim_rw  (.ml files)
rwthm -> thm_rw  (.ml files)

3) Fixed the rule Itt_struct.hypSubstitution


Revision 2629 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 4 22:07:38 1999 UTC (22 years, 2 months ago) by jyh
File length: 43467 byte(s)
Diff to previous 2578
This is the first phase for modifying resources.
The Mp_resource interface has been substantially simplified, but
I believe that it retains as much functionality as it did before
the change.

The next step for me to add the Mp_resource support for
adding resources as rule annotations.


Revision 2578 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 28 22:53:13 1999 UTC (22 years, 4 months ago) by nogin
File length: 43990 byte(s)
Diff to previous 2531
Fixed some of "this expression should have type unit" warnings


Revision 2531 - (view) (download) (annotate) - [select for diffs]
Modified Wed Dec 30 03:58:59 1998 UTC (22 years, 5 months ago) by jyh
File length: 43976 byte(s)
Diff to previous 2529
The general intuitionistic propDecideT now works.
There was a bug in Itt_logic preventing << false >> from
being recognized.


Revision 2529 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 29 23:30:21 1998 UTC (22 years, 5 months ago) by jyh
File length: 43856 byte(s)
Diff to previous 2525
Added pigeonhole problem in editor/ml/test.ml.

To try it:

% ./mptop
# #use "y.ml";;
# refine timingT proveT;;


Revision 2525 - (view) (download) (annotate) - [select for diffs]
Modified Mon Dec 28 21:07:52 1998 UTC (22 years, 5 months ago) by jyh
File length: 43809 byte(s)
Diff to previous 2494
Numerous minor changes.

Added itt_fset: a theory of finite sets based on a list
implementation quotiented by equivalence under arbitrary
occurrences and ordering.

Added initial reflection theory.  Terms are quotiented by
alpha-equality, so normal well-formedness proofs are difficult,
and more work needs to be done to define free variables and
substitution.


Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 43521 byte(s)
Diff to previous 2456
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.


Revision 2456 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 5 22:31:37 1998 UTC (22 years, 9 months ago) by jyh
File length: 43525 byte(s)
Diff to previous 2443
Added license headers to each of the files in preparation for
the first major release.  The license is GNU public license; if
any of you have problems with that, let me know right away.  When
you add new code, you should credit yourself as the author.  When
you modify code, you should add a "Modified by:" to the header,
and possibly a short summary of your changes.

I tried to get the Author lists as correct as I remember, but there
are more than 550 files(!) and I may have made some mistakes. Please
add yourself if I didn't do it right.


Revision 2443 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 24 13:43:48 1998 UTC (22 years, 10 months ago) by jyh
File length: 42366 byte(s)
Diff to previous 2420
Slightly better Ensemble scheduling.
Native-code compiler has trouble marshaling functions--
its probably a problem with the marshaler.

Added Nl_num, a ML-only implementation of bignums.
This is slower than the C version used by OCaml, but
we can marshal the Nl_nums.  Most of the files changed
are just replacements of Num.* with Nl_num.*.


Revision 2420 - (view) (download) (annotate) - [select for diffs]
Modified Fri Aug 7 01:48:31 1998 UTC (22 years, 10 months ago) by jyh
File length: 42363 byte(s)
Diff to previous 2380
Added unify_subst type to retain unification info between separate
calls to TermSubst.unify.  This requires that type inference be modified,
and there are still some small modifications to be made in Itt_rfun.
We need to do some optimization in Cycle_dag and unification.


Revision 2380 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 2 17:12:26 1998 UTC (22 years, 10 months ago) by jyh
File length: 42351 byte(s)
Diff to previous 2376
Modified rewriter to handle Alexey's new sequents.  The rewriter is
now moved to a new directory refiner/rewrite.  Clause numbers in
TermMan now start with 1.  The tactics seem to work, but there may
be some lurking problems with hypothesis numbering.


Revision 2376 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 31 14:35:45 1998 UTC (22 years, 10 months ago) by jyh
File length: 38446 byte(s)
Diff to previous 2356
Added TPTP theory, and Ensemble library.  Fixed sequent displays.
BUG: rewrites fail on sequents.


Revision 2356 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 24 21:11:12 1998 UTC (22 years, 11 months ago) by nogin
File length: 23354 byte(s)
Diff to previous 2347
Functorized the Simple_print module over the Refiner module


Revision 2347 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 23 18:40:34 1998 UTC (22 years, 11 months ago) by nogin
File length: 23340 byte(s)
Diff to previous 2337
Moved eseqent type to the TermType module.
Made the types of esequent components hidden to make them read-only.


Revision 2337 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 22 00:34:42 1998 UTC (22 years, 11 months ago) by jyh
File length: 23287 byte(s)
Diff to previous 2336
Removed dest_sequent, and changed Term_man_sig.esequent to use arrays.


Revision 2336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 21 22:47:13 1998 UTC (22 years, 11 months ago) by jyh
File length: 23189 byte(s)
Diff to previous 2333
Added NL toploop so that we can compile NL native code.


Revision 2333 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 17 15:39:32 1998 UTC (22 years, 11 months ago) by jyh
File length: 23175 byte(s)
Diff to previous 2326
CZF is complete, although we may wish to add pairing and inf.


Revision 2326 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 14 21:04:31 1998 UTC (22 years, 11 months ago) by jyh
File length: 20901 byte(s)
Diff to previous 2325
Added to itt_derived.


Revision 2325 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 14 15:44:03 1998 UTC (22 years, 11 months ago) by jyh
File length: 20870 byte(s)
Diff to previous 2320
Intermediate version with auto tactic.


Revision 2320 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 9 21:08:59 1998 UTC (22 years, 11 months ago) by jyh
File length: 8797 byte(s)
Diff to previous 2314
Upgraded czf.


Revision 2314 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 8 15:42:11 1998 UTC (22 years, 11 months ago) by jyh
File length: 8796 byte(s)
Diff to previous 2309
Pushed higherC into the refiner for efficiency.


Revision 2309 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 21:39:34 1998 UTC (22 years, 11 months ago) by jyh
File length: 8050 byte(s)
Diff to previous 2307
Working czf_itt_set.


Revision 2307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 17:55:31 1998 UTC (22 years, 11 months ago) by nogin
File length: 7413 byte(s)
Diff to previous 2283
Removed $Log messages from all NL files.


Revision 2283 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 2 18:38:08 1998 UTC (22 years, 11 months ago) by jyh
File length: 9487 byte(s)
Diff to previous 2280
Refiner modules now raise RefineError exceptions directly.
Modules in this revision have two versions: one that raises
verbose exceptions, and another that uses a generic exception.


Revision 2280 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 1 04:38:04 1998 UTC (22 years, 11 months ago) by nogin
File length: 9487 byte(s)
Diff to previous 2272
Moved Refiner exceptions into a separate module RefineErrors


Revision 2272 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 23 22:12:44 1998 UTC (23 years ago) by jyh
File length: 9369 byte(s)
Diff to previous 2268
Improved rewriter speed with conversion tree and flist.


Revision 2268 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 22 19:46:48 1998 UTC (23 years ago) by jyh
File length: 9296 byte(s)
Diff to previous 2244
Rewriting in contexts.  This required a change in addressing,
and the body of the context is the _last_ subterm, not the first.


Revision 2244 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 15 22:33:52 1998 UTC (23 years ago) by jyh
File length: 9003 byte(s)
Diff to previous 2224
Added CZF.


Revision 2224 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 12 13:47:49 1998 UTC (23 years ago) by jyh
File length: 8760 byte(s)
Diff to previous 2209
D tactic works, added itt_bool.


Revision 2209 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 1 13:57:13 1998 UTC (23 years ago) by jyh
File length: 8676 byte(s)
Diff to previous 2190
Proving twice one is two.


Revision 2190 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 28 13:48:44 1998 UTC (23 years ago) by jyh
File length: 8408 byte(s)
Diff to previous 2152
Updated the editor to use new Refiner structure.
ITT needs dform names.


Revision 2152 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 24 02:44:07 1998 UTC (23 years, 2 months ago) by jyh
File length: 8269 byte(s)
Diff to previous 2150
Added more extensive debugging capabilities.


Revision 2150 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 22 22:45:29 1998 UTC (23 years, 2 months ago) by jyh
File length: 8048 byte(s)
Diff to previous 2061
*** empty log message ***


Revision 2061 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 8 15:02:40 1997 UTC (23 years, 9 months ago) by jyh
File length: 7944 byte(s)
Diff to previous 2047
This version compiles Ensemble.


Revision 2047 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 6 16:18:55 1997 UTC (23 years, 10 months ago) by jyh
File length: 7868 byte(s)
Diff to previous 2032
This is an ocaml version with subtyping, type inference,
d and eqcd tactics.  It is a basic system, but not debugged.


Revision 2032 - (view) (download) (annotate) - [select for diffs]
Added Mon Apr 28 15:52:46 1997 UTC (24 years, 1 month ago) by jyh
File length: 4140 byte(s)
This is the initial checkin of Nuprl-Light.
I am porting the editor, so it is not included
in this checkin.

Directories:
    refiner: logic engine
    filter: front end to the Ocaml compiler
    editor: Emacs proof editor
    util: utilities
    mk: Makefile templates


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26