EDITS TO THE ISABELLE SYSTEM FOR 1993 11 January */README: Eliminated references to Makefile.NJ, which no longer exists. **** New tar file placed on /homes/lcp (464K) **** 14 January Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing prints conditions correctly. {CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from add_mult_dist, to agree with the other _distrib rules 20 January Pure/Syntax/type_ext.ML: "I have fixed a few anomalies in the pretty printing annotations for types. Only the layout has changed." -- Toby 21 January {CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse 22 January ZF/ex/equiv: new theory of equivalence classes ZF/ex/integ: new theory of integers HOL/set.thy: added indentation of 3 to all binding operators ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I 25 January MAKE-ALL (NJ 0.75) ran perfectly. It took 3:19 hours!? ZF/bool/not,and,or,xor: new 27 January ZF/ex/bin: new theory of binary integer arithmetic 27 January MAKE-ALL (Poly/ML) ran perfectly. It took 6:33 hours??? (ZF took almost 5 hours!) **** New tar file placed on /homes/lcp (472K) **** HOL/set/UN_cong,INT_cong: new HOL/subset/mem_rews,set_congs,set_ss: new HOL/simpdata/o_apply: new; added to HOL_ss 29 January Pure/Thy/syntax/mk_structure: the dummy theory created by type infixes is now called name^"(type infix)" instead of "", avoid triggering a spurious error "Attempt to merge different versions of theory: " in Pure/sign/merge_stamps 2 February MAKE-ALL (Poly/ML) ran perfectly. It took 2:48 hours. Runs in 1992 took under 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutes according to make10836.log. Pure/Thy/scan/comment: renamed from komt Pure/Thy/scan/numeric: renamed from zahl Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by Tobias to change ID, TVAR, ... to lower case. Cube/cube.thy,HOL/hol.thy,HOL/set.thy,CTT/ctt.thy,LK/lk.thy,ZF/zf.thy: now with ID, ... in lower case and other tidying 3 February MAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours. 4 February HOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m P(s)"; by (res_inst_tac [("t","s")] (Rep_Sum_inverse RS subst) 1); by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1); by (REPEAT (eresolve_tac [disjE,exE,ssubst] 1 ORELSE resolve_tac prems 1)); val sumE = result(); 8 February Changes from Tobias: Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does not Pure/Thy/syntax: uses new list_of, list_of1 9 February HOL/ex/arith: moved to main HOL directory HOL/prod: now define the type "unit" and constant "(): unit" 11 February HOL/arith: eliminated redefinitions of nat_ss and arith_ss 12 February MAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours. Pure/Thy/scan/string: now correctly recognizes ML-style strings. 15 February MAKE-ALL (NJ 0.75) ran perfectly. It took 1:37 hours (on albatross) MAKE-ALL (NJ 0.75) ran perfectly. It took 2:42 hours (on dunlin) MAKE-ALL (Poly/ML) ran perfectly. It took 2:53 hours (on dunlin) **** New tar file placed on /homes/lcp (480K) **** 18 February Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as it was unused. Pure/Syntax/earley0A: modified accordingly. 19 February MAKE-ALL (NJ 0.75) ran perfectly. It took 3:37 hours MAKE-ALL (Poly/ML) ran perfectly. It took 2:52 hours **** New tar file placed on /homes/lcp (480K) **** 20 February MAKE-ALL (NJ 0.93) ran perfectly. It took 3:30 hours 10 March HOL/fun/image_eqI: fixed bad pattern 11 March MAKE-ALL (Poly/ML) failed in HOL! HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws of Int and Un. 12 March ZF/ex/misc: new example from Bledsoe 15 March ZF/perm: two new theorems inspired by Pastre 16 March Weakened congruence rules for HOL: speeds simplification considerably by NOT simplifying the body of a conditional or eliminator. HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded operators < and <= HOL/prod: weakened the congruence rule for split HOL/sum: weakened the congruence rule for case HOL/nat: weakened the congruence rule for nat_case and nat_rec HOL/list: weakened the congruence rule for List_rec and list_rec HOL & test rebuilt perfectly Pure/goals/prepare_proof/mkresult: fixed bug in signature check. Now compares the FINAL signature with that from the original theory. Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the definitions do not update the proof state. 17 March MAKE-ALL (Poly/ML) ran perfectly. 18 March MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where necessary ZF/perm: proved some rules about inj and surj ZF/ex/misc: did some of Pastre's examples Pure/library/gen_ins,gen_union: new HOL/ex/Subst/subst: renamed rangeE to srangeE 18 March MAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in ex/Subst/alist HOL/list/list_congs: new; re-organized simpsets a bit Pure/goals/sign_error: new Pure/goals/prepare_proof,by_com: now print the list of new theories when the signature of the proof state changes HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing the library functions fst, snd HOL/fun/image_compose: new 21 March MAKE-ALL (NJ 0.93) ran perfectly. It took 3:50 hours MAKE-ALL (Poly/ML) ran perfectly. It took 3:21 hours Much slower now (about 30 minutes!) because of HOL/ex/Subst **** New tar file placed on /homes/lcp (504K) **** ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing the library functions fst, snd HOL/prod/prod_fun_imageI,E: new HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify of Pure 24 March HOL/trancl/comp_subset_Sigma: new HOL/wf/wfI: new HOL/Subst: moved from HOL/ex/Subst to shorten pathnames HOL/Makefile: target 'test' now loads Subst/ROOT separately *** Installation of gfp, coinduction, ... to HOL *** HOL/gfp,llist: new HOL/univ,sexp,list: replaced with new version Sexp is now the set of all well-founded trees, each of type 'a node set. There is no longer a type 'sexp'. Initial algebras require more explicit type checking than before. Defining a type 'sexp' would eliminate this, but would also require a whole new set of primitives, similar to those defined in univ.thy but restricted to well-founded trees. 25 March Pure/thm: renamed 'bires' to 'eres' in many places (not exported) -- biresolution now refers to resolution with (flag,rule) pairs. Pure/thm/bicompose_aux: SOUNDNESS BUG concerning variable renaming. A Var in a premise was getting renamed when its occurrence in the flexflex pairs was not. Martin Coen supplied the following proof of True=False in HOL: val [prem] = goal Set.thy "EX a:{c}.p=a ==> p=c"; br (prem RS bexE) 1; be ssubst 1; be singletonD 1; val l1 = result(); val rls = [refl] RL [bexI] RL [l1]; goal Set.thy "True = False"; brs rls 1; br singletonI 1; result(); Marcus Moore noted that the error only occurred with Logic.auto_rename:=false. Elements of the fix: 1. rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (the existing flex-flex pairs) as an extra argument. rename_bvs preserves all Vars in tpairs. 2. bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs to newAs. HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed def_Tarski to def_lfp_Tarski 26 March MAKE-ALL (NJ 0.93) ran perfectly. It took 4:25 hours! MAKE-ALL (Poly/ML) ran perfectly. It took 3:54 hours! (jobs overlapped) Pure/Thy/scan/is_digit,is_letter: deleted. They are already in Pure/library, and these versions used non-Standard string comparisons! Repairing a fault reported by David Aspinall: show_types := true; read "a"; (* followed by 'prin it' for NJ *) Raises exception LIST "hd". Also has the side effect of leaving show_types set at false. Pure/goals/read: no longer creates a null TVar Pure/Syntax/lexicon/string_of_vname: now handles null names Pure/Syntax/printer/string_of_typ: tidied /usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bug MAKE-ALL on this directory ran perfectly /usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version 29 March MAKE-ALL (NJ 0.93) ran perfectly. It took 4:14 hours! MAKE-ALL (Poly/ML) ran perfectly. It took 3:43 hours! **** New tar file placed on /homes/lcp (518K) **** 30 March ZF/univ/cons_in_Vfrom: deleted "[| a: Vfrom(A,i); b<=Vfrom(A,i) |] ==> cons(a,b) : Vfrom(A,succ(i))" since it was useless. 8 April MAKE-ALL (Poly/ML) ran perfectly. It took 3:49 hours! **** New tar file placed on /homes/lcp (520K) **** **** Updates for pattern unification (Tobias Nipkow) **** Pure/pattern.ML: new, pattern unification Pure/Makefile and ROOT.ML: included pattern.ML Pure/library.ML: added predicate downto0 Pure/unify.ML: call pattern unification first. Removed call to could_unify. FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead) **** Installation of Martin Coen's FOLP (FOL + proof objects) **** renamed PFOL, PIFOL to FOLP, IFOLP, etc. 9 April MAKE-ALL (NJ 0.93) ran perfectly. It took 4:05 hours! MAKE-ALL (Poly/ML) ran perfectly. It took 3:31 hours! **** New tar file placed on /homes/lcp (576K) **** **** Installation of Discrimination Nets **** *Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac) Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML Provers/simp.ML HOL/ex/meson.ML *Affected files (those mentioning compat_resolve_tac) Pure/tactic.ML Provers/typedsimp.ML CTT/ctt.ML Pure/stringtree: saved on Isabelle/old Pure/net: new Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML Pure/ROOT: now mentions net.ML, not stringtree.ML Pure/goals/compat_goal: DELETED Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm, delete_thm,head_string: DELETED Pure/tactic/biresolve_from_nets_tac, bimatch_from_nets_tac, net_biresolve_tac, net_bimatch_tac, resolve_from_net_tac, match_from_net_tac, net_resolve_tac, net_match_tac: NEW Pure/tactic/filt_resolve_tac: new implementation using nets! Provers/simp: replaced by new version Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and updated comments CTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tac CTT tested HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net FOL tested Provers/simp/cong_const: new, replaces head_string call in cong_consts Provers/simp: renamed variables: atomic to at and cong_consts to ccs ZF/ex/bin/integ_of_bin_type: proof required reordering of rules -- typechk_tac now respects this ordering! ZF tested DOCUMENTATION Logics/CTT: Removed mention of compat_resolve_tac Ref/goals: deleted compat_goal's entry Provers/hypsubst/lasthyp_subst_tac: deleted FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works! 12 April MAKE-ALL (NJ 0.93) ran perfectly. It took 4:03 hours! MAKE-ALL (Poly/ML) ran perfectly. It took 3:28 hours! FOLP/{int-prover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac FOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tac FOLP/{int-prover,classical}/step_tac: calls inst_step_tac {FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac is used explicitly!! FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call uniq_assume_tac Provers/classical: REPLACED BY 'NET' VERSION! 13 April MAKE-ALL (Poly/ML) failed in ZF and ran out of quota for Cube. Unification bug (nothing to do with pattern unification) Cleaning of flex-flex pairs attempts to remove all occurrences of bound variables not common to both sides. Arguments containing "banned" bound variables are deleted -- but this should ONLY be done if the occurrence is rigid! unify/CHANGE_FAIL: new, for flexible occurrence of bound variable unify/change_bnos: now takes "flex" as argument, indicating path status 14 April MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex changes Pure/goals/gethyps: now calls METAHYPS directly rm-logfiles: no longer mentions directories. WAS rm log {Pure,FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/make*.log rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/test rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/.*.thy.ML rm {FOL,ZF,HOL}/ex/.*.thy.ML MAKE-ALL (Poly/ML) ran perfectly. It took 2:39 hours! (albatross) New version of simp on Isabelle/new -- instantiates unknowns provided only one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR] works with FOLP/ex/nat, but in general could fail in the event of overlapping rewrite rules, since FOLP always instantiates unknowns during rewriting. ZF: tested with new version HOL: tested with new version, appeared to loop in llist/Lmap_ident **** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS **** ZF: failed in perm/comp_mem_injD1: the rule anti_refl_rew is too ambiguous! ZF/wfrec: all uses of wf_ss' require by (METAHYPS (fn hyps => cut_facts_tac hyps 1 THEN SIMP_TAC (wf_ss' addrews (hyps)) 1) 1); ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes METAHYPS version work ZF/arith/add_not_less_self: adds anti_refl_rew ZF/ex/prop-log/hyps_finite: the use of UN_I is very bad -- too undirected. Swapping the premises of UN_I would probably allow instantiation. ZF otherwise seems to work! HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in (CCONTR_rule RS allI) *** REJECTED 15 April These overnight runs involve Provers/simp.ML with old treatment of rules (match_tac) and no METAHYPS; they test the new flexflex pairs and discrimination nets, to see whether it runs faster. MAKE-ALL (NJ 0.93) ran perfectly. It took 3:39 hours (4 mins faster) MAKE-ALL (Poly/ML) ran perfectly. It took 3:23 hours (5 mins faster) ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down discrimination nets (and this rewrite used only ONCE) ZF/mem_not_refl: new; replaces obsolete anti_refl_rew **Timing experiments** fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1); On large examples such as ... HOL/arith/mod_quo_equality HOL/llist/LListD_implies_ntrunc_equality ZF/ex/bin/integ_of_bin_succ ... it is 1.5 to 3 times faster than ASM_SIMP_TAC. But cannot replace ASM_SIMP_TAC since the auto_tac sometimes fails due to lack of assumptions. If there are few assumptions then HYP_SIMP_TAC is no better. Pure/Makefile: now copies $(ML_DBASE) to $(BIN)/Pure instead of calling make_database, so that users can call make_database for their object-logics. Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is only one subgoal. 19 April MAKE-ALL (NJ 0.93) failed in HOL due to lack of disc space. MAKE-ALL (Poly/ML) ran perfectly. It took 3:23 hours **** Installation of new simplifier **** Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg to the auto_tac. FOL,HOL/simpdata: auto_tac now handles the hyps argument ZF/simpdata/standard_auto_tac: deleted ZF/simpdata/auto_tac: added hyps argument ZF/epsilon/eclose_least_lemma: no special auto_tac */ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..." 20 April MAKE-ALL failed in HOL/Subst HOL/Subst/setplus/cla_case: renamed imp_excluded_middle and simplified. Old version caused ambiguity in rewriting: "[| P ==> P-->Q; ~P ==> ~P-->Q |] ==> Q"; **** New tar file placed on /homes/lcp (????) **** Pure/Syntax: improvements to the printing of syntaxes Pure/Syntax/lexicon.ML: added name_of_token Pure/Syntax/earley0A.ML: updated print_gram 21 April MAKE-ALL (NJ 0.93) ran perfectly. It took 3:44 hours MAKE-ALL (Poly/ML) failed in HOL due to lack of disc space HOL/list,llist: now share NIL, CONS, List_Fun and List_case make-all: now compresses the log files, which were taking up 4M; this reduces their space by more than 1/3 rm-logfiles: now deletes compressed log files. ** Patrick Meche has noted that if the goal is stated with a leading !! quantifier, then the list of premises is always empty -- this gives the effect of an initial (cut_facts_tac prems 1). The final theorem is the same as it would be without the quantifier. ZF: used the point above to simplify many proofs ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac 22 April MAKE-ALL (NJ 0.93) ran perfectly. It took 3:52 hours?? MAKE-ALL (Poly/ML) ran perfectly. It took 3:16 hours 30 April HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow) HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert", new derivations for "singleton" HOL/llist.thy,llist.ML: changed {x.False} to {} **** New tar file placed on /homes/lcp (584K) **** 4 May MAKE-ALL (NJ 0.93) ran out of space in LK. MAKE-ALL (Poly/ML) ran perfectly. It took 3:14 hours Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is write-protected 5 May HOL/list/not_Cons_self: renamed from l_not_Cons_l HOL/list/not_CONS_self: new HOL/llist.thy/Lconst: changed type and def to remove Leaf HOL/llist.ML: changed Lconst theorems 6 May MAKE-ALL (Poly/ML) ran perfectly. It took 3:18 hours ** Installation of new HOL from Tobias ** HOL/ex/{finite,prop-log} made like the ZF versions HOL/hol.thy: type classes plus, minus, times; overloaded operators + - * HOL/set: set enumeration via "insert" additions to set_cs and set_ss HOL/set,subset,equalities: various lemmas to do with {}, insert and - HOL/llist: One of the proofs needs one fewer commands HOL/arith: many proofs require type constraints due to overloading ** end Installation ** ZF/ex/misc: added new lemmas from Abrial's paper 7 May HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous simplification now proves the subgoal. **** New tar file placed on /homes/lcp (584K) **** ** Installation of new simplifier from Tobias ** The "case_splits" parameter of SimpFun is moved from the signature to the simpset. SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed. The ordinary simplification tactics perform case splits if present in the simpset. The simplifier finds out for itself what constant is affected. Instead of supplying the pair (expand_if,"if"), supply just the rule expand_if. This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun. MAKE-ALL (Poly/ML) ran perfectly. It took 3:18 hours Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and DEPTH_SOLVE HOL: installation of NORM tag for simplication. How was it forgotten?? HOL/hol.thy: declaration of NORM HOL/simpdata: NORM_def supplied to SimpFun 10 May MAKE-ALL (Poly/ML) ran perfectly. It took 3:33 hours?? 11 May HOL/prod/Prod_eq: renamed Pair_eq HOL/ex/lex-prod: wf_lex_prod: simplified proof HOL/fun/inj_eq: new HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits! 12 May MAKE-ALL (NJ 0.93) ran out of space in HOL. MAKE-ALL (Poly/ML) failed in HOL. HOL/Subst/utermlemmas/utlemmas_ss: deleted Prod_eq from the congruence rules 13 May Pure/logic/flexpair: moved to term, with "equals" etc. Now pervasive Pure/logic/mk_flexpair: now exported Pure/logic/dest_flexpair: new Pure/goals/print_exn: now prints the error message for TERM and TYPE Pure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop because flexflex pairs can have any type at all. Thus == must have the same type. Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}. Pure/tctical/equal_abs_elim,equal_abs_elim_list: new (for METAHYPS fix) Pure/tctical/METAHYPS: now works if new proof state has flexflex pairs Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now, not by integers. (Changed by Tobias) *** Installation of more printing functions *** Pure/sign/sg: changed from a type abbrev to a datatype Pure/type/type_sig: changed from a type abbrev to a datatype These changes needed for abstract type printing in NJ Pure/tctical/print_sg,print_theory: new Pure/drule: new file containing derived rules and printing functions. Mostly from tctical.ML, but includes rewriting rules from tactic.ML. Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now depend on Drule and have sharing constraints. 14 May Installing new print functions for New Jersey: incompatible with Poly/ML! Pure/NJ/install_pp_nj: new (requires datatypes as above) Pure/POLY/install_pp_nj: a dummy version Pure/ROOT: calls install_pp_nj to install printing for NJ */ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) for Poly/ML [ZF,LCF,Modal do not need them since they inherit them from another logic -- make_database is not used] 17 May MAKE-ALL (NJ 0.93) ran perfectly. It took 3:57 hours?? Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias) 18 May MAKE-ALL (Poly/ML) ran perfectly. It took 3:36 hours 19 May ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of complex assumptions 20 May HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl, null and list_case. 1 June MAKE-ALL (Poly/ML) ran perfectly. It took 3:39 hours **** New tar file 92.tar.z placed on /homes/lcp (376K) **** MAKE-ALL (NJ 0.93) ran perfectly. It took 1:49 hours on albatross. Pure/tactic/dres_inst_tac,forw_inst_tac: now call the new make_elim_preserve to preserve Var indexes when creating the elimination rule. ZF/ex/ramsey: modified calls to dres_inst_tac 2 June Pure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to the current directory, since the pathname may lead to a non-writeable area. HOL/arith: renamed / and // to div and mod ZF/arith: renamed #/ and #// to div and mod MAKE-ALL (Poly/ML) ran perfectly. It took 1:48 hours on albatross. **** New tar file 92.tar.z placed on /homes/lcp (376K) **** Pure/NJ/commit: new dummy function FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems make-all: now builds FOLP also! 3 June ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_], <_,_> are formatted as {(_)}, [(_)], MAKE-ALL (Poly/ML) ran perfectly. It took 4:37 hours on muscovy (with FOLP). ZF/Makefile: removed obsolete target for .rules.ML All object-logic Makefiles: EXAMPLES ARE NO LONGER SAVED. This saves disc and avoids problems (in New Jersey ML) of writing to the currently executing image. 4 June Pure/logic/rewritec: now uses nets for greater speed. Functor LogicFun now takes Net as argument. Pure/ROOT: now loads net before logic. MAKE-ALL (Poly/ML) failed in ZF and HOL. LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL) 7 June Pure/tactic/is_letdig: moved to library Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig MAKE-ALL (Poly/ML) ran perfectly. It took 2:07 hours on albatross. MAKE-ALL (NJ 0.93) ran perfectly. It took 4:41 hours on dunlin. HOL/set/UN1,INT1: new union/intersection operators. Binders UN x.B(x), INT x.B(x). HOL/univ,llist: now use UN x.B(x) instead of Union(range(B)) HOL/subset: added lattice properties for INT, UN (both forms) 8 June MAKE-ALL (NJ 0.93) ran perfectly. It took 4:45 hours on dunlin. **** New tar file 92.tar.z placed on /homes/lcp (384K) **** 14 June HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp. Using def_wfrec hides such errors!! **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** ** NEW VERSION FROM MUNICH WITH ==-REWRITING ** ** The following changes are Toby's ** type.ML: Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars. Added both functions to the signature. sign.ML: Added val subsig: sg * sg -> bool to signature. Added trueprop :: prop and mark_prop : prop => prop to pure_sg. Added val freeze_vars: term -> term val thaw_vars: term -> term val strip_all_imp: term * int -> term list * term * int Moved rewritec_bottom and rewritec_top to thm.ML. Only bottom-up rewriting supported any longer. thm.ML: Added (* internal form of conditional ==-rewrite rules *) type meta_simpset val add_mss: meta_simpset * thm list -> meta_simpset val empty_mss: meta_simpset val mk_mss: thm list -> meta_simpset val mark_prop_def: thm val truepropI: thm val trueprop_def: thm (* bottom-up conditional ==-rewriting with local ==>-assumptions *) val rewrite_cterm: meta_simpset -> (thm -> thm list) -> (meta_simpset -> thm list -> Sign.cterm -> thm) -> Sign.cterm -> thm val trace_simp: bool ref Simplified concl_of: call to Logic.skip_flexpairs redundant. drule.ML: Added (* rewriting *) val asm_rewrite_rule: (thm -> thm list) -> thm list -> thm -> thm val rewrite_goal_rule: (thm -> thm list) -> thm list -> int -> thm -> thm val rewrite_goals_rule: (thm -> thm list) -> thm list -> thm -> thm (* derived concepts *) val forall_trueprop_eq: thm val implies_trueprop_eq: thm val mk_trueprop_eq: thm -> thm val reflexive_eq: thm val reflexive_thm: thm val trueprop_implies_eq: thm val thm_implies: thm -> thm -> thm val thm_equals: thm -> thm -> thm (*Moved here from tactic.ML:*) val asm_rl: thm val cut_rl: thm val revcut_rl: thm tactic.ML: Added val asm_rewrite_goal_tac: (thm -> thm list) -> thm list -> int -> tactic val asm_rewrite_goals_tac: (thm -> thm list) -> thm list -> tactic val asm_rewrite_tac: (thm -> thm list) -> thm list -> tactic val fold_goal_tac: thm list -> int -> tactic val rewrite_goal_tac: thm list -> int -> tactic Moved to drule.ML: val asm_rl: thm val cut_rl: thm val revcut_rl: thm goals.ML: Changed prepare_proof to make sure that rewriting with empty list of meta-thms is identity. ** End of Toby's changes ** 16 June Pure/sign/typ_of,read_ctyp: new Pure/logic/dest_flexpair: now exported Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in flexpair_abs_elim_list HOL/equalities/image_empty,image_insert: new HOL/ex/finite/Fin_imageI: new Installed Martin Coen's CCL as new object-logic 17 June ** More changes from Munich (Markus Wenzel) ** Pure/library: added the, is_some, is_none, separate and improved space_implode Pure/sign: Sign.extend now calls Syntax.extend with list of constants Pure/symtab: added is_null Pure/Syntax/sextension: added empty_sext Pure/Syntax/syntax: changed Syntax.extend for compatibility with future version HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to specify -h 8000. HOL/univ/ntrunc_subsetD, etc: deleted the useless j syntax Pure/Makefile SYNTAX_FILES: added Syntax/ast.ML Pure/Syntax/pretty.ML added str_of: T -> string Pure/Syntax/ast.ML added this file Pure/Syntax/extension.ML Pure/Syntax/parse_tree.ML Pure/Syntax/printer.ML Pure/Syntax/ROOT.ML Pure/Syntax/sextension.ML Pure/Syntax/syntax.ML Pure/Syntax/type_ext.ML Pure/Syntax/xgram.ML These files have been completely rewritten, though the global structure is similar to the old one. 30-Jun-1993 MMW New versions of HOL and Cube: use translation rules wherever possible; HOL/hol.thy cleaned up removed alt_tr', mk_bindopt_tr' alternative binders now implemented via translation rules and mk_alt_ast_tr' HOL/set.thy cleaned up removed type "finset" now uses category "args" for finite sets junked "ML" section added "translations" section HOL/list.thy cleaned up removed type "listenum" now uses category "args" for lists junked "ML" section added "translations" section Cube/cube.thy cleaned up changed indentation of Lam and Pi from 2 to 3 removed qnt_tr, qnt_tr', no_asms_tr, no_asms_tr' fixed fun_tr': all but one newly introduced frees will have type dummyT added "translations" section 30-Jun-1993, 05-Jul-1993 MMW Improved toplevel pretty printers: - unified interface for POLY and NJ; - print functions now insert atomic string into the toplevel's pp stream, rather than writing it to std_out (advantage: output appears at the correct position, disadvantage: output cannot be broken); (Is there anybody in this universe who exactly knows how Poly's install_pp is supposed to work?); Pure/NJ.ML removed dummy install_pp added make_pp, install_pp Pure/POLY.ML removed dummy install_pp_nj added make_pp Pure/ROOT.ML removed install_pp_nj stuff Pure/drule.ML added str_of_sg, str_of_theory, str_of_thm Pure/install_pp.ML added this file Pure/sign.ML added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp Pure/goals.ML added str_of_term, str_of_typ CTT/ROOT.ML Cube/ROOT.ML FOL/ROOT.ML FOLP/ROOT.ML HOL/ROOT.ML LK/ROOT.ML replaced install_pp stuff by 'use "../Pure/install_pp.ML"' 01-Jul-1993 MMW Misc small fixes CCL/ROOT.ML HOL/ROOT.ML added ".ML" suffix to some filenames HOL/ex/unsolved.ML replaced HOL_Rule.thy by HOL.thy Pure/NJ.ML quit was incorrectly int -> unit END MMW CHANGES Pure/Syntax/sextension/eta_contract: now initially false Pure/library/cat_lines: no longer calls "distinct" Pure/sign: replaced to calls of implode (map (apr(op^,"\n") o ... by cat_lines NB This could cause duplicate error messages from Pure/sign and Pure/type Pure/goals/prove_goalw: now prints some of the information from print_exn 9 July MAKE-ALL (Poly/ML) ran perfectly. It took 2:26 hours on albatross. **** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 12 July MAKE-ALL (NJ 0.93) ran perfectly. It took 2:13 hours on albatross. MAKE-ALL (Poly/ML) ran perfectly. It took 2:25 hours on albatross. 22 July ZF/zf.thy: new version from Marcus Wenzel ZF: ** installation of inductive definitions ** changing the argument order of "split"; affects fst/snd too sum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thy pair.ML ex/integ.ML changing the argument order of "case" and adding "Part": sum.thy sum.ML ZF/zf.ML/rev_subsetD,rev_bspec: new ZF/mono: new rules for implication ZF/mono/Collect_mono: now for use with implication rules ZF/zf.ML/ballE': renamed rev_ballE ZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.ML ZF/list.ML: new version simply holds the datatype definition NB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair. ZF/extend_ind.ML, datatype.ML: new files ZF/fin.ML: moved from ex/finite.ML 23 July ZF/ex/sexp: deleted this example -- it seems hardly worth the trouble of porting. ZF/ex/bt.thy,bt.ML: files renamed bt-fn.thy, bt-fn.ML ZF/ex/bt.ML: new version simply holds the datatype definition ZF/ex/term.thy,term.ML: files renamed term-fn.thy, term-fn.ML ZF/ex/term.ML: new version simply holds the datatype definition ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI 26 July ZF/univ/rank_ss: new, for proving recursion equations ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff, field_of_prod:new ZF/domrange/field_subset: modified ZF/list/list_cases: no longer proved by induction! ZF/wf/wf_trancl: simplified proof ZF/equalities: new laws for field 29 July ZF/trancl/trancl_induct: new ZF/trancl/rtrancl_induct,trancl_induct: now with more type information ** More changes from Munich (Markus Wenzel) ** Update of new syntax module (aka macro system): mostly internal cleanup and polishing; Pure/Syntax/* added Ast.stat_norm added Syntax.print_gram, Syntax.print_trans, Syntax.print_syntax cleaned type and Pure syntax: "_CLASSES" -> "classes", "_SORTS" -> "sorts", "_==>" -> "==>", "_fun" -> "fun", added some space for printing Printer: partial fix of the "PROP " problem: print "PROP " before any Var or Free of type propT Syntax: added ndependent_tr, dependent_tr' Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext) Changes to object logics: minor cleanups and replacement of most remaining ML translations by rewrite rules (see also file "Translations"); ZF/zf.thy added "translations" section removed all parse/print translations except ndependent_tr, dependent_tr' fixed dependent_tr': all but one newly introduced frees have type dummyT replaced id by idt in order to make terms rereadable if !show_types Cube/cube.thy removed necontext replaced fun_tr/tr' by ndependent_tr/dependent_tr' CTT/ctt.thy added translations rules for PROD and SUM removed dependent_tr removed definitions of ndependent_tr, dependent_tr' HOL/set.thy: replaced id by idt CCL/ROOT.ML: Logtic -> Logic CCL/set.thy added "translations" section removed "ML" section replaced id by idt CCL/types.thy added "translations" section removed definitions of ndependent_tr, dependent_tr' replaced id by idt Yet another improvement of toplevel pretty printers: output now breakable; Pure/NJ.ML Pure/POLY.ML improved make_pp Pure/install_pp.ML: replaced str_of_* by pprint_* Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_* Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_* Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_* Pure/Syntax/pretty.ML: added pprint, quote Minor changes and additions; Pure/sign.ML: renamed stamp "PURE" to "Pure" Pure/library.ML added quote: string -> string added to_lower: string -> bool Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm 30 July MAKE-ALL (Poly/ML) ran perfectly. Pure/goals/print_sign_exn: new, takes most code from print_exn Pure/goals/prove_goalw: displays exceptions using print_sign_exn Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg Pure/library,...: replaced front/nth_tail by take/drop. Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: new thm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the above Pure/logic/add_term_vars,add_term_frees,insert_aterm,atless: moved to term, joining similar functions for type variables; Logic.vars and Logic.frees are now term_vars and term_frees Pure/term/subst_free: new Pure/tactic/is_fact: newly exported Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of forall is_letdig **** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 2 August MAKE-ALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr MAKE-ALL (Poly/ML) failed in ZF/enum. It took 2:33 hours on albatross. Pure/drule/triv_forall_equality: new Pure/tactic/prune_params_tac: new Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac 3 August Pure/tactic/rule_by_tactic: new ZF/perm/compEpair: now proved via rule_by_tactic ZF/extend_ind/cases,mk_cases: new ZF/datatype/mk_free: new ZF/list: now calls List.mk_cases 4 August Provers/slow_tac,slow_best_tac: new 5 August MAKE-ALL (Poly/ML) failed in ZF ZF/sum/sumE2: deleted since unused ZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: new ZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset 6 August Pure/goals/prepare_proof: after "Additional hypotheses", now actually prints them! ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from Transset_Union, Transset_Inter ZF/ordinal/Transset_Union: new ZF/univ/pair_in_univ: renamed Pair_in_univ ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed uses in extend_ind.ML, nat.ML, trancl.ML. ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added 9 August ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on Syntax/sextension. 11 August Pure/library.ML: added functions assocs: (''a * 'b list) list -> ''a -> 'b list transitive_closure: (''a * ''a list) list -> (''a * ''a list) list Pure/type.ML: deleted (inefficient) transitive_closure