isabelle: Changelog

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.

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.

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.

Brought in line with new organization of IOA.

New examples directories Resid and AC

Definition of 'let' declarations, from HOL

In binders, the default body priority is now p instead of 0.

Now builds Resid as a test

Renamed diff_sing_lepoll to Diff_sing_lepoll.

Renamed domain_diff_subset, range_diff_subset, field_diff_subset, converse_diff to domain_Diff_subset, range_Diff_subset, field_Diff_subset, converse_Diff for consistency. (Thanks to KG)

Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll to Diff_sing_lepoll, lepoll_Diff_sing and Diff_sing_eqpoll for consistency. Strengthened lepoll_Diff_sing. (Thanks to KG)

Updated CADE reference

Removes (obsolete) target if already present.

Directory example is now called NTP

ABP: Alternating bit protocol example

New example by Ole Rasmussen

Simplified some proofs and made them work for new hyp_subst_tac.

Deleted some useless things and made proofs of refl_comp_subset and comp_equivI more like the versions in ZF/EquivClass.ML

Simplified using pattern replacements.

adjusted HOLCF for new hyp_subst_tac

Defined vv1 using let. Introduced gg1, gg2.

Deleted subset_imp_Un_Diff_eq, as it is identical to Diff_partition. Used split_tac (sometimes via simplifier) to apply expand_if. Replaced lt_oadd_disj1 by lt_oadd_odiff_disj, using ordinal difference instead of a description. Removed the outer quantifier from all_sum_lepoll_m, all_sum_lepoll_m_2. Changed all "lesspoll succ(m)" to "lepoll m" and simplified proofs. Changed definitions of vv1 and ww1 to use lepoll instead of lesspoll; therefore vv1(f,b,succ(m)) becomes vv1(f,b,m). Moved proof of vv1_not_0 into the body of the proof using this result. Renamed variable aa to s. Simplified lemma_iv using addss. Renamed some theorems; combined some proofs.

Redefined OUnion in a definitional manner

Redefined OUnion in a definitional manner, and proved the rules again. Deleted the rules OUnionI/E as they were not needed. Proved OUN_cong. Extended OrdQuant_ss with oex_cong and defined Ord_atomize to extract rewrite rules from ALL x<i... assumptions.

Deleted lt_oadd_disj1

Recoded function atomize so that new ways of creating simplification rules can be added easily.

Defined ordinal difference, --

Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2, odiff_lt_mono2. Deleted duplicate copy of oadd_le_mono.

Proved lesspoll_succ_iff.

Completely rewrote split_tac. The old one failed in strange circumstances.

term.ML: add_loose_bnos now returns a list w/o duplicates. pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)

Added comment to function "loops".

(binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).

ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. MT.thy: Deleted extra space in clos_mk.

Removed the "exit 1" calls, since now the Makefile does them.

ROOT.ML: installed new hyp_subst_tac Nat.ML: Changed proof of lessE for new hyp_subst_tac

Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that the maxidx-filed of thms is computed correctly.

Local version of (original) hypsubst: needs no simplifier

Modified proofs for new hyp_subst_tac.