/[mojave]/metaprl/theories/tactic/top_tacticals.ml
ViewVC logotype

Log of /metaprl/theories/tactic/top_tacticals.ml

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 2 months ago) by nogin
File length: 18235 byte(s)
Diff to previous 3328
- 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 3328 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 11 23:58:51 2001 UTC (19 years, 11 months ago) by nogin
File length: 18259 byte(s)
Diff to previous 3307
FOL theory is now complete.


Revision 3307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 2 22:34:20 2001 UTC (19 years, 11 months ago) by kopylov
File length: 17791 byte(s)
Diff to previous 3282
- added rules applyEquality to intro resource

- many rules (e.g. letT and elimination rules for the intersection and union types)
  produces equality hypotheses in the subgoals that rarely used in practice.
  Now such rules thin these hypotheses by default.
  To avoid this one can use doNotThinT = thinningT false.


Revision 3282 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 18:41:55 2001 UTC (20 years ago) by kopylov
File length: 17652 byte(s)
Diff to previous 3277
New tactics ans cnversionals are documented.


Revision 3277 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 00:12:25 2001 UTC (20 years ago) by kopylov
File length: 17386 byte(s)
Diff to previous 3274
- New tacticals
    onAllAssumT : (int -> tactic) -> tactic
    onAllMAssumT : (int -> tactic) -> tactic
  apply a tactic to all assumtions

 rwAll applies a convertion to all clauses
 rwcAll applies a convertion to all clauses for the given assumption
 rwAllAll applies a convertion to all assumption and to the goal sequent

 rwhAll,rwchAll,rwhAllAll, rwaAll,rwcaAll,rwaAllAll work by analogy

 Now these tactics does not work properly (see BUGS 3.12-3.14)

- Most of the theorems on records are proved


Revision 3274 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 17 21:41:29 2001 UTC (20 years ago) by kopylov
File length: 17279 byte(s)
Diff to previous 3235
- Added tacticals whileProgressMT and untilFailMT

- Implemented dependend records

- Change a rule for depended intersection


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: 17092 byte(s)
Diff to previous 3124
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 3124 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 31 22:44:31 2001 UTC (20 years, 4 months ago) by nogin
File length: 17080 byte(s)
Diff to previous 3123
Spelling changes.
For best results, upgrade to http://www.cs.cornell.edu/nogin/RPM/MetaPRL/noarch/words-2.1-1.noarch.html


Revision 3123 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 31 20:23:20 2001 UTC (20 years, 4 months ago) by kopylov
File length: 17018 byte(s)
Diff to previous 3058
There was inconsistent with the documentation and the implementation
of the ifLabT and RepeatT tactics.

The documentation about ifLabT is corrected.

The old repeatT tactic is now called whileProgressT.

The (repeatT tac)  is now defined as whileProgressT (tryT tac)

Still to do: implement the untilFailT tactic (Nuprl's REPEAT).


* whileProgressT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals while there is a progress.

* untilFailT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals until it fails.

* repeatT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals until it fails or no more
progress is made.

See also all-theories.pdf.


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: 16115 byte(s)
Diff to previous 2743
Last commit failed partway through...


Revision 2743 - (view) (download) (annotate) - [select for diffs]
Added Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 4664 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.

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


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