Krzysztof Grabczewski's (nearly) complete AC proofs

renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.

Added some lemmas about r^*.

Lambda calculus in de Bruijn notation. Proof of confluence.

Indexing of COMP

Indexing of FILTER and COND

show_sorts

Modified translation for pattern abstraction.

Moved induct2 from Hoare to Lfp.

Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.

converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex

added \CHOL

Calls 'rail' program for syntax diagrams

Changed some definitions and proofs to use pattern-matching.

Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.

case is defined using pattern-matching

Modified proofs for new form of 'split'.

Added pattern-matching code from CHOL/Prod.thy. Changed definitions so that split is now defined in terms of fst, snd. Now split is polymorphic. Deleted fsplit, as split(...)::o gives a similar effect -- NOT identical though, as fsplit(P,z) implied that z was a pair, while split(P,z) means only P(fst(z),snd(z)).

Modified proofs for (q)split, fst, snd for new definitions. The rule f(q)splitE is now called (q)splitE and is weaker than before. The rule '(q)split' is now a meta-equality; this required modifying all proofs involving e.g. split RS trans.

Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.

prove_case_equation now calls uses meta_eq_to_obj_eq to cope with new form of 'split'. Tried calling simp_tac instead of using resolution with trans, but it was significantly slower: 98.3 secs instead of 91.2 secs for ex/Enum.

show_sorts:=true forces display of types

trivial rewording

trivial change

Covers wrapper tacticals: setwrapper, ..., addss

fixed bug in thy_unchanged that occurred when the .thy file was changed but the .ML file hadn't been read before; tmpfile is now deleted immediatly after reading the .thy file in use_thy

Changed definitions so that qsplit is now defined in terms of qfst, qsnd. AT PRESENT THERE IS NO PATTERN-MATCHING FOR QSPLIT.

Modified proofs for (q)split, fst, snd for new definitions. The rule f(q)splitE is now called (q)splitE and is weaker than before. The rule '(q)split' is now a meta-equality; this required modifying all proofs involving e.g. split RS trans.

Changed some definitions and proofs to use pattern-matching.

Patterns can now be let-bound

Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.

Changed some definitions and proofs to use pattern-matching.

Changed some definitions and proofs to use pattern-matching.

Changed some definitions and proofs to use pattern-matching.

Now show_sorts:=true causes printing of types

Imported meta_eq_to_obj_eq from HOL for use with 'split'.

replaced store_thm by bind_thm

trivial change

new version

Covers defs and re-ordering of theory sections

Updates involving defs, addss, etc.

Simplified layout a little.

Corrected display of split f t: no more let. Also replaced "_abs" by "_lambda" --- the former was a mistake which happended to work.

Sections can now be given in any order.

Simplified proof of Hausdorff_next_exists.

Added functor f() = struct end to hide functors to save space.

Renamed insert_kbrl to insert_tagged_brl and exported it. Now subgoals_of_brl calls nprems_of, which is faster than length o prems_of.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Recoded addSIs, etc., so that nets are built incrementally instead of from scratch each time. The old approach used excessive time (>1 sec for adding a rule to ZF_cs) and probably excessive space. Now rep_claset includes all record fields. joinrules no longer sorts the rules on number of subgoals, since it does not see the full set of them; instead the number of subgoals modifies the priority.

updated version

Simple updates for compatibility with KG

Simplified, removing needless theorems about lambda.

Now loads the theory "Let". Could add it to FOL, but this appears to be incompatible with CCL.

HOL.thy: "@" is no longer introduced as a "binder" but has its own explicit translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further translation rules for abstractions with patterns take care of the rest. This is very modular and avoids problems with "binders" such as "!" mentioned below. let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u) Set.thy: UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@" above, except that "@" was a "binder" originally. Prod.thy: Added new syntax for pttrn which allows arbitrarily nested tuples. Two translation rules take care of %pttrn. Unfortunately they cannot be reversed. Hence a little ML-code is used as well. Note that now "! (x,y). ..." is syntactically valid but leads to a translation error. This is because "!" is introduced as a "binder" which means that its translation into lambda-terms is not done by a rewrite rule (aka macro) but by some fixed ML-code which comes after the rewriting stage and does not know how to handle patterns. This looks like a minor blemish since patterns in unbounded quantifiers are not that useful (well, except maybe in unique existence ...). Ideally, there should be two syntactic categories: idts, as we know and love it, which does not admit patterns. patterns, which is what idts has become now. There is one more point where patterns are now allowed but don't make sense: {e | idts . P} where idts is the list of local variables. Univ.thy: converted the defs for <++> and <**> into pattern form. It worked perfectly.

I have modified the grammar for idts (sequences of identifiers with optional type annotations). idts are generally used as in abstractions, be it lambda-abstraction or quantifiers. It now has roughly the form idts = pttrn* pttrn = idt where pttrn is a new nonterminal (type) not used anywhere else. This means that the Pure syntax for idts is in fact unchanged. The point is that the new nontermianl pttrn allows later extensions of this syntax. (See, for example, HOL/Prod.thy). The name idts is not quite accurate any longer and may become downright confusing once pttrn has been extended. Something should be done about this, in particular wrt to the manual.

Simplified proofs thanks to addss.

Fixed old bug in the simplifier. Term to be simplified now carries around its maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1 in most cases (ie no Vars), hence reasonable overhead.

Fixed bug.