ViewVC logotype

Log of /metaprl/theories/itt/itt_bool.prla

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: 382352 byte(s)
Diff to previous 3343
- 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 3343 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 20 23:06:48 2001 UTC (19 years, 11 months ago) by nogin
File length: 382349 byte(s)
Diff to previous 3329
Itt_fset is finally complete!

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: 380300 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: 400353 byte(s)
Diff to previous 3296
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 3296 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 20:26:12 2001 UTC (20 years ago) by nogin
File length: 400118 byte(s)
Diff to previous 3280
Fixed a problem with cond rewrites labels that I accidentally introduced earlier.

Revision 3280 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 13:40:29 2001 UTC (20 years ago) by nogin
File length: 400117 byte(s)
Diff to previous 3279
Use byDefT in a few places.

Revision 3279 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 11:48:09 2001 UTC (20 years ago) by nogin
File length: 400192 byte(s)
Diff to previous 3272
- Renamed andthenC -> thenC
- Added byDefT : conv -> tactic
- Proved rewrites in Itt_dprod
- Removed some unused stuff from one of the filter_prog interfaces.

Revision 3272 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 17 14:10:39 2001 UTC (20 years ago) by nogin
File length: 400195 byte(s)
Diff to previous 3238
Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but
can also do thinning. I added it to trivialT, so now trivialT and autoT can
do thinning when matching the goal against assumptions.

Revision 3238 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 27 18:08:16 2001 UTC (20 years ago) by nogin
File length: 400282 byte(s)
Diff to previous 3139
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 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: 409907 byte(s)
Diff to previous 3058
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 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: 409957 byte(s)
Diff to previous 3047
Last commit failed partway through...

Revision 3047 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 14 04:28:07 2000 UTC (20 years, 10 months ago) by nogin
File length: 290708 byte(s)
Diff to previous 3042
I changed the unhide rules according to hide{A} = squash{A} semantics.

Alexei, can you take a look at my changes and see if you agree with them?
Also, do we need more elimination rules for union and more introduction rules
for intersection?

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: 299164 byte(s)
Diff to previous 3036
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 3036 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 27 19:55:54 2000 UTC (20 years, 10 months ago) by nogin
File length: 309313 byte(s)
Diff to previous 2912
- Fixed the problem with leaking attributes.

- Fixed the problem with top-level functions (such as clean_all)
removing the "Primivive" flag and replacing it with "Interactive".

- Fixed some display forms.

- Removed "empty" .prla files in ITT and "refreshed" the rest of them.

- More in BUGS and TODO.

- Other small changes.

Revision 2912 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 24 06:55:47 2000 UTC (21 years, 4 months ago) by jyh
File length: 397289 byte(s)
Diff to previous 2906
Most of the theories in Itt now expand without errors.
One exception is Itt_fset, which will require some work.

Revision 2906 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 22 17:42:16 2000 UTC (21 years, 4 months ago) by jyh
File length: 400838 byte(s)
Diff to previous 2805
Itt_bool now expands.

Revision 2805 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 23 20:51:24 1999 UTC (21 years, 11 months ago) by nogin
File length: 302345 byte(s)
Diff to previous 2804
Some theories still had Itt_squash!squash instead of Base_trivial!squash - fixed.
Now more old proofs expand correctly.

Revision 2804 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 23 19:50:37 1999 UTC (21 years, 11 months ago) by nogin
File length: 302497 byte(s)
Diff to previous 2788
reduceIfthenelse{True,False} were renamed to reduce_ifthenelse_{true,false}

Revision 2788 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 5 14:49:32 1999 UTC (21 years, 11 months ago) by jyh
File length: 302463 byte(s)
Diff to previous 2775
ifthenelse_member was defined twice.

Revision 2775 - (view) (download) (annotate) - [select for diffs]
Added Sun Jul 4 13:13:44 1999 UTC (21 years, 11 months ago) by jyh
File length: 364184 byte(s)
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:

       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.

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