ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log

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

Revision 3591 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 19748 byte(s)
Diff to previous 3347
- Added an option to be have "THEORIES=all" in mk/config
(instead of THEORIES="long list of theories").
I will change all my nightly scripts to use THEORIES=all.

- Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
that would automatically contain \inputs corresponding to TEXTHEORIES.
(Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
was changed).

- Minor fixes in some display forms.

- Removed theories/caml that never had anything useful.

- Removed a few files from theories/ocaml_doc that seemed to be there by accident
(Jason, can you confirm?).

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

Revision 3344 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jul 21 23:23:43 2001 UTC (19 years, 11 months ago) by nogin
File length: 33016 byte(s)
Diff to previous 3329
- created a tcaT tactic that is equivalent to tryT (completeT autoT)
- created a filter macro "ttca" that is equivalent to
"thenT tcaT"
- moved memberTypeT from itt_collection to itt_struct
- updated itt_quickref a little.
- some cleanup in itt_fset and itt_collection

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: 35578 byte(s)
Diff to previous 3326
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theories.

Revision 3326 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 11 15:23:32 2001 UTC (19 years, 11 months ago) by nogin
File length: 35573 byte(s)
Diff to previous 3315
- trivialT can now do equalRefT and equalSymT when necessary to match
the conclusion with a hypothesis.
- turned couple of Itt_equal rules from primitives into interactives
- fixed a few FOL proofs
- removed some obsolete files

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: 35577 byte(s)
Diff to previous 3304
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
- 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 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: 35559 byte(s)
Diff to previous 3281
Added num_assums and nth_assums to Refine and Sequent.

Revision 3281 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 13:56:53 2001 UTC (20 years ago) by nogin
File length: 35615 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: 35948 byte(s)
Diff to previous 3232
Added support for the following syntax of resource improvement:
let resource name += expr
let resource name += [ expr1; expr2; ...; exprn ]

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: 36283 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: 36259 byte(s)
Diff to previous 3139
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 3139 - (view) (download) (annotate) - [select for diffs]
Modified Sun Feb 4 19:38:29 2001 UTC (20 years, 4 months ago) by nogin
File length: 36217 byte(s)
Diff to previous 3050
I moved the bind operator from ITT to the Perv module. This makes sense because
what we really mean by "bind" is a generic binding construction, not something
I've also replaced Perv!lambda with Perv!bind since it was now redundant
and it was indeed used as "bind", not as "lambda" (there were no beta-reduction
for Perv!lambda).

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: 36211 byte(s)
Diff to previous 3042
- 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
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 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: 35986 byte(s)
Diff to previous 2803
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 2803 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 23 18:40:31 1999 UTC (21 years, 11 months ago) by nogin
File length: 36904 byte(s)
Diff to previous 2753
Fixed intro/elim annotations in itt_collection

Revision 2753 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 25 00:19:15 1999 UTC (22 years ago) by jyh
File length: 36571 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]
Added Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 36641 byte(s)
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.

   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

   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).


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