many renamings and changes. Simproc for cancelling common terms in relations
EDITS TO THE ISABELLE SYSTEM FOR 199311 January */README: Eliminated references to Makefile.NJ, which no longer exists.**** New tar file placed on /homes/lcp (464K) **** 14 JanuaryProvers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracingprints conditions correctly.{CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed fromadd_mult_dist, to agree with the other _distrib rules20 JanuaryPure/Syntax/type_ext.ML: "I have fixed a few anomalies in the prettyprinting annotations for types. Only the layout has changed." -- Toby21 January{CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse22 JanuaryZF/ex/equiv: new theory of equivalence classesZF/ex/integ: new theory of integersHOL/set.thy: added indentation of 3 to all binding operatorsZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I25 JanuaryMAKE-ALL (NJ 0.75) ran perfectly. It took 3:19 hours!?ZF/bool/not,and,or,xor: new27 JanuaryZF/ex/bin: new theory of binary integer arithmetic27 JanuaryMAKE-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: newHOL/subset/mem_rews,set_congs,set_ss: newHOL/simpdata/o_apply: new; added to HOL_ss29 JanuaryPure/Thy/syntax/mk_structure: the dummy theory created by type infixes isnow called name^"(type infix)" instead of "", avoid triggering a spuriouserror "Attempt to merge different versions of theory: " inPure/sign/merge_stamps2 FebruaryMAKE-ALL (Poly/ML) ran perfectly. It took 2:48 hours. Runs in 1992 tookunder 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutesaccording to make10836.log.Pure/Thy/scan/comment: renamed from komtPure/Thy/scan/numeric: renamed from zahlPure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified byTobias 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: nowwith ID, ... in lower case and other tidying3 FebruaryMAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours.4 FebruaryHOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m<n)and the nat_case rules and congruence rulesHOL/sum/sumE: now has the "strong" form with equality assumptions. WAS val prems = goalw Sum.thy [Inl_def,Inr_def] "[| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) \ \ |] ==> 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 FebruaryChanges from Tobias:Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does notPure/Thy/syntax: uses new list_of, list_of19 FebruaryHOL/ex/arith: moved to main HOL directoryHOL/prod: now define the type "unit" and constant "(): unit"11 FebruaryHOL/arith: eliminated redefinitions of nat_ss and arith_ss12 FebruaryMAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours.Pure/Thy/scan/string: now correctly recognizes ML-style strings.15 FebruaryMAKE-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 FebruaryPure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, asit was unused.Pure/Syntax/earley0A: modified accordingly.19 FebruaryMAKE-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 FebruaryMAKE-ALL (NJ 0.93) ran perfectly. It took 3:30 hours 10 MarchHOL/fun/image_eqI: fixed bad pattern11 MarchMAKE-ALL (Poly/ML) failed in HOL!HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset lawsof Int and Un.12 MarchZF/ex/misc: new example from Bledsoe15 MarchZF/perm: two new theorems inspired by Pastre16 MarchWeakened congruence rules for HOL: speeds simplification considerably byNOT simplifying the body of a conditional or eliminator.HOL/simpdata/mk_weak_congs: new, to make weakened congruence rulesHOL/simpdata/congs: renamed HOL_congs and weakened the "if" ruleHOL/simpdata/HOL_congs: now contains polymorphic rules for the overloadedoperators < and <=HOL/prod: weakened the congruence rule for splitHOL/sum: weakened the congruence rule for caseHOL/nat: weakened the congruence rule for nat_case and nat_recHOL/list: weakened the congruence rule for List_rec and list_recHOL & test rebuilt perfectlyPure/goals/prepare_proof/mkresult: fixed bug in signature check. Nowcompares the FINAL signature with that from the original theory.Pure/goals/prepare_proof: ensures that [prove_]goalw checks that thedefinitions do not update the proof state.17 MarchMAKE-ALL (Poly/ML) ran perfectly.18 MarchMAKE-ALL (Poly/ML) failed in HOL/ex/SubstitutionsHOL/ex/Subst/setplus: changed Set.thy to Setplus.thy wherenecessaryZF/perm: proved some rules about inj and surjZF/ex/misc: did some of Pastre's examplesPure/library/gen_ins,gen_union: newHOL/ex/Subst/subst: renamed rangeE to srangeE18 MarchMAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss inex/Subst/alistHOL/list/list_congs: new; re-organized simpsets a bitPure/goals/sign_error: newPure/goals/prepare_proof,by_com: now print the list of new theories whenthe signature of the proof state changes HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writingthe library functions fst, sndHOL/fun/image_compose: new21 MarchMAKE-ALL (NJ 0.93) ran perfectly. It took 3:50 hours MAKE-ALL (Poly/ML) ran perfectly. It took 3:21 hoursMuch 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-writingthe library functions fst, sndHOL/prod/prod_fun_imageI,E: newHOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unifyof Pure24 MarchHOL/trancl/comp_subset_Sigma: newHOL/wf/wfI: newHOL/Subst: moved from HOL/ex/Subst to shorten pathnamesHOL/Makefile: target 'test' now loads Subst/ROOT separately*** Installation of gfp, coinduction, ... to HOL ***HOL/gfp,llist: newHOL/univ,sexp,list: replaced with new versionSexp 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 explicittype checking than before. Defining a type 'sexp' would eliminate this,but would also require a whole new set of primitives, similar to thosedefined in univ.thy but restricted to well-founded trees.25 MarchPure/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 ina premise was getting renamed when its occurrence in the flexflex pairs wasnot. 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 withLogic.auto_rename:=false. Elements of the fix:1. rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (theexisting flex-flex pairs) as an extra argument. rename_bvs preserves allVars in tpairs.2. bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairsto newAs.HOL/lfp,gfp,ex/set: renamed Tarski to lfp_TarskiHOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renameddef_Tarski to def_lfp_Tarski 26 MarchMAKE-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 inPure/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 leavingshow_types set at false. Pure/goals/read: no longer creates a null TVarPure/Syntax/lexicon/string_of_vname: now handles null namesPure/Syntax/printer/string_of_typ: tidied/usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bugMAKE-ALL on this directory ran perfectly/usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version29 MarchMAKE-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 MarchZF/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 AprilMAKE-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 unificationPure/Makefile and ROOT.ML: included pattern.MLPure/library.ML: added predicate downto0Pure/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 AprilMAKE-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.MLProvers/simp.MLHOL/ex/meson.ML*Affected files (those mentioning compat_resolve_tac)Pure/tactic.MLProvers/typedsimp.MLCTT/ctt.MLPure/stringtree: saved on Isabelle/oldPure/net: newPure/Makefile/FILES: now mentions net.ML, not stringtree.MLPure/ROOT: now mentions net.ML, not stringtree.MLPure/goals/compat_goal: DELETEDPure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm,delete_thm,head_string: DELETEDPure/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: NEWPure/tactic/filt_resolve_tac: new implementation using nets!Provers/simp: replaced by new versionProvers/typedsimp: changed compat_resolve_tac to filt_resolve_tac andupdated commentsCTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tacCTT testedHOL/ex/meson/ins_term,has_reps: replaced Stringtree by NetFOL testedProvers/simp/cong_const: new, replaces head_string call in cong_constsProvers/simp: renamed variables: atomic to at and cong_consts to ccsZF/ex/bin/integ_of_bin_type: proof required reordering of rules --typechk_tac now respects this ordering!ZF testedDOCUMENTATIONLogics/CTT: Removed mention of compat_resolve_tac Ref/goals: deleted compat_goal's entryProvers/hypsubst/lasthyp_subst_tac: deletedFOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works!12 AprilMAKE-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_tacFOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tacFOLP/{int-prover,classical}/step_tac: calls inst_step_tac {FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac isused explicitly!!FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost uselessFOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and calluniq_assume_tacProvers/classical: REPLACED BY 'NET' VERSION!13 AprilMAKE-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 boundvariables not common to both sides. Arguments containing "banned" boundvariables are deleted -- but this should ONLY be done if the occurrence isrigid!unify/CHANGE_FAIL: new, for flexible occurrence of bound variableunify/change_bnos: now takes "flex" as argument, indicating path status14 AprilMAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LKLK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflexchangesPure/goals/gethyps: now calls METAHYPS directlyrm-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.MLMAKE-ALL (Poly/ML) ran perfectly. It took 2:39 hours! (albatross)New version of simp on Isabelle/new -- instantiates unknowns provided onlyone rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR]works with FOLP/ex/nat, but in general could fail in the event ofoverlapping rewrite rules, since FOLP always instantiates unknowns duringrewriting.ZF: tested with new versionHOL: 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' requireby (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 makesMETAHYPS version workZF/arith/add_not_less_self: adds anti_refl_rewZF/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 VarsHOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in (CCONTR_rule RS allI)*** REJECTED15 AprilThese overnight runs involve Provers/simp.ML with old treatment of rules(match_tac) and no METAHYPS; they test the new flexflex pairs anddiscrimination 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 downdiscrimination 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_equalityZF/ex/bin/integ_of_bin_succ... it is 1.5 to 3 times faster than ASM_SIMP_TAC. But cannot replaceASM_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 callingmake_database, so that users can call make_database for their object-logics.Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there isonly one subgoal.19 AprilMAKE-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 argto the auto_tac.FOL,HOL/simpdata: auto_tac now handles the hyps argumentZF/simpdata/standard_auto_tac: deletedZF/simpdata/auto_tac: added hyps argumentZF/epsilon/eclose_least_lemma: no special auto_tac */ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..."20 AprilMAKE-ALL failed in HOL/SubstHOL/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 syntaxesPure/Syntax/lexicon.ML: added name_of_tokenPure/Syntax/earley0A.ML: updated print_gram21 AprilMAKE-ALL (NJ 0.93) ran perfectly. It took 3:44 hoursMAKE-ALL (Poly/ML) failed in HOL due to lack of disc spaceHOL/list,llist: now share NIL, CONS, List_Fun and List_casemake-all: now compresses the log files, which were taking up 4M; thisreduces their space by more than 1/3rm-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 theeffect of an initial (cut_facts_tac prems 1). The final theorem is thesame as it would be without the quantifier.ZF: used the point above to simplify many proofsZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac22 AprilMAKE-ALL (NJ 0.93) ran perfectly. It took 3:52 hours??MAKE-ALL (Poly/ML) ran perfectly. It took 3:16 hours30 AprilHOL: 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 MayMAKE-ALL (NJ 0.93) ran out of space in LK.MAKE-ALL (Poly/ML) ran perfectly. It took 3:14 hoursPure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) iswrite-protected5 MayHOL/list/not_Cons_self: renamed from l_not_Cons_lHOL/list/not_CONS_self: newHOL/llist.thy/Lconst: changed type and def to remove LeafHOL/llist.ML: changed Lconst theorems6 MayMAKE-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 versionsHOL/hol.thy: type classes plus, minus, times; overloaded operators + - *HOL/set: set enumeration via "insert" additions to set_cs and set_ssHOL/set,subset,equalities: various lemmas to do with {}, insert and -HOL/llist: One of the proofs needs one fewer commandsHOL/arith: many proofs require type constraints due to overloading** end Installation **ZF/ex/misc: added new lemmas from Abrial's paper7 May HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previoussimplification 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 thesimpset. SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed. The ordinarysimplification tactics perform case splits if present in the simpset.The simplifier finds out for itself what constant is affected. Instead ofsupplying 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 hoursCube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 andDEPTH_SOLVEHOL: installation of NORM tag for simplication. How was it forgotten??HOL/hol.thy: declaration of NORMHOL/simpdata: NORM_def supplied to SimpFun10 MayMAKE-ALL (Poly/ML) ran perfectly. It took 3:33 hours??11 MayHOL/prod/Prod_eq: renamed Pair_eqHOL/ex/lex-prod: wf_lex_prod: simplified proofHOL/fun/inj_eq: newHOL/llist/sumPairE: deleted, thanks to new simplifier's case splits!12 MayMAKE-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 rules13 MayPure/logic/flexpair: moved to term, with "equals" etc. Now pervasivePure/logic/mk_flexpair: now exportedPure/logic/dest_flexpair: newPure/goals/print_exn: now prints the error message for TERM and TYPEPure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop becauseflexflex 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 pairsPure/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 datatypePure/type/type_sig: changed from a type abbrev to a datatypeThese changes needed for abstract type printing in NJPure/tctical/print_sg,print_theory: newPure/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 nowdepend on Drule and have sharing constraints.14 MayInstalling 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 versionPure/ROOT: calls install_pp_nj to install printing for NJ*/ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) forPoly/ML [ZF,LCF,Modal do not need them since they inherit them from anotherlogic -- make_database is not used]17 MayMAKE-ALL (NJ 0.93) ran perfectly. It took 3:57 hours??Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias)18 MayMAKE-ALL (Poly/ML) ran perfectly. It took 3:36 hours19 MayZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead ofcomplex assumptions20 MayHOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl,null and list_case.1 JuneMAKE-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 newmake_elim_preserve to preserve Var indexes when creating the eliminationrule.ZF/ex/ramsey: modified calls to dres_inst_tac2 JunePure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to thecurrent directory, since the pathname may lead to a non-writeable area.HOL/arith: renamed / and // to div and modZF/arith: renamed #/ and #// to div and modMAKE-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 functionFOLP/ex/ROOT: inserted commit call to avoid Poly/ML problemsmake-all: now builds FOLP also!3 JuneZF/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.MLAll object-logic Makefiles: EXAMPLES ARE NO LONGER SAVED. This saves discand avoids problems (in New Jersey ML) of writing to the currentlyexecuting image.4 JunePure/logic/rewritec: now uses nets for greater speed. Functor LogicFun nowtakes 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 JunePure/tactic/is_letdig: moved to libraryPure/Syntax/lexicon/is_qld: deleted, was same as is_letdigMAKE-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 JuneMAKE-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 JuneHOL/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.Addedval freeze_vars: term -> termval thaw_vars: term -> termval strip_all_imp: term * int -> term list * term * intMoved 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_simpsetval add_mss: meta_simpset * thm list -> meta_simpsetval empty_mss: meta_simpsetval mk_mss: thm list -> meta_simpsetval mark_prop_def: thmval truepropI: thmval 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 -> thmval trace_simp: bool refSimplified concl_of: call to Logic.skip_flexpairs redundant.drule.ML:Added(* rewriting *)val asm_rewrite_rule: (thm -> thm list) -> thm list -> thm -> thmval rewrite_goal_rule: (thm -> thm list) -> thm list -> int -> thm -> thmval rewrite_goals_rule: (thm -> thm list) -> thm list -> thm -> thm(* derived concepts *)val forall_trueprop_eq: thmval implies_trueprop_eq: thmval mk_trueprop_eq: thm -> thmval reflexive_eq: thmval reflexive_thm: thmval trueprop_implies_eq: thmval thm_implies: thm -> thm -> thmval thm_equals: thm -> thm -> thm(*Moved here from tactic.ML:*)val asm_rl: thmval cut_rl: thmval revcut_rl: thmtactic.ML:Addedval asm_rewrite_goal_tac: (thm -> thm list) -> thm list -> int -> tacticval asm_rewrite_goals_tac: (thm -> thm list) -> thm list -> tacticval asm_rewrite_tac: (thm -> thm list) -> thm list -> tacticval fold_goal_tac: thm list -> int -> tacticval rewrite_goal_tac: thm list -> int -> tacticMoved to drule.ML:val asm_rl: thmval cut_rl: thmval revcut_rl: thmgoals.ML:Changed prepare_proof to make sure that rewriting with empty list ofmeta-thms is identity.** End of Toby's changes **16 JunePure/sign/typ_of,read_ctyp: newPure/logic/dest_flexpair: now exportedPure/drule/flexpair_intr,flexpair_elim: new; fixes a bug inflexpair_abs_elim_listHOL/equalities/image_empty,image_insert: newHOL/ex/finite/Fin_imageI: newInstalled Martin Coen's CCL as new object-logic17 June** More changes from Munich (Markus Wenzel) **Pure/library: added the, is_some, is_none, separate and improved space_implodePure/sign: Sign.extend now calls Syntax.extend with list of constantsPure/symtab: added is_nullPure/Syntax/sextension: added empty_sextPure/Syntax/syntax: changed Syntax.extend for compatibility with future versionHOL now exceeds poly's default heap size. Hence HOL/Makefile needs tospecify -h 8000.HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption18 JuneMAKE-ALL (Poly/ML) ran perfectly. It took 4:59 hours on dunlin (with CCL).Pure/sign/read_def_cterm: now prints the offending terms, as well as thetypes, when exception TYPE is raised.HOL/llist: some tidying23 JuneHOL/llist/Lconst_type: generalized from Lconst(M): LList({M})24 JuneMAKE-ALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross (with CCL)MAKE-ALL (NJ 0.93) failed in CCL due to use of "abstraction" as anidentifier in CCL.ML**** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL)CCL/ROOT: added ".ML" extension to use commands for NJ compatibility25 JuneMAKE-ALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross.MAKE-ALL (NJ 0.93) failed in HOL due to lack of ".ML" extensionHOL/fun/rangeE,imageE: eta-expanded f to get variable name preservationHOL/llist/iterates_equality,lmap_lappend_distrib: tidied28 JuneHOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variablename preservation HOL/llist: co-induction rules applied with res_inst_tac to state thebisimulation directly2 JulyMAKE-ALL (NJ 0.93) ran perfectly. It took 2:10 hours on albatross.MAKE-ALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross.92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database=**** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL)** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER **I have merged in the changes shown above since 24 JuneCHANGES LOG OF Markus Wenzel (MMW)=======29-Jun-1993 MMW *** Beta release of new syntax module *** (should be 99% backwards compatible) Pure/Thy/ROOT.ML added keywords for "translations" section Pure/Thy/syntax.ML minor cleanup added syntax for "translations" section .*.thy.ML files now human readable .*.thy.ML used to be generated incorrectly if no mixfix but "ML" section "ML" section no longer demands any definitions (parse_translation, ...) Pure/Thy/read.ML read_thy: added close_in added file_exists (not perfect) use_thy: now uses file_exists Pure/thm.ML added syn_of: theory -> 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" section30-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 -> unitEND MMW CHANGESPure/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_linesNB This could cause duplicate error messages from Pure/sign and Pure/typePure/goals/prove_goalw: now prints some of the information from print_exn9 JulyMAKE-ALL (Poly/ML) ran perfectly. It took 2:26 hours on albatross.**** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 12 JulyMAKE-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 JulyZF/zf.thy: new version from Marcus WenzelZF: ** installation of inductive definitions **changing the argument order of "split"; affects fst/snd toosum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thypair.ML ex/integ.MLchanging the argument order of "case" and adding "Part": sum.thy sum.MLZF/zf.ML/rev_subsetD,rev_bspec: newZF/mono: new rules for implicationZF/mono/Collect_mono: now for use with implication rulesZF/zf.ML/ballE': renamed rev_ballEZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.MLZF/list.ML: new version simply holds the datatype definitionNB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair.ZF/extend_ind.ML, datatype.ML: new filesZF/fin.ML: moved from ex/finite.ML23 JulyZF/ex/sexp: deleted this example -- it seems hardly worth the trouble ofporting.ZF/ex/bt.thy,bt.ML: files renamed bt-fn.thy, bt-fn.MLZF/ex/bt.ML: new version simply holds the datatype definitionZF/ex/term.thy,term.ML: files renamed term-fn.thy, term-fn.MLZF/ex/term.ML: new version simply holds the datatype definitionZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI26 JulyZF/univ/rank_ss: new, for proving recursion equationsZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff,field_of_prod:newZF/domrange/field_subset: modifiedZF/list/list_cases: no longer proved by induction!ZF/wf/wf_trancl: simplified proofZF/equalities: new laws for field29 JulyZF/trancl/trancl_induct: newZF/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 andpolishing; 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 <aprop>" 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 MLtranslations 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 idtYet 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, quoteMinor 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 Clasohm30 JulyMAKE-ALL (Poly/ML) ran perfectly.Pure/goals/print_sign_exn: new, takes most code from print_exnPure/goals/prove_goalw: displays exceptions using print_sign_exnPure/drule/print_sg: now calls pretty_sg to agree with pprint_sgPure/library,...: replaced front/nth_tail by take/drop.Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: newthm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the abovePure/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_freesPure/term/subst_free: newPure/tactic/is_fact: newly exportedProvers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rulesPure/tactic/rename_last_tac: now uses Syntax.is_identifier instead offorall is_letdig**** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 2 AugustMAKE-ALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStrMAKE-ALL (Poly/ML) failed in ZF/enum. It took 2:33 hours on albatross.Pure/drule/triv_forall_equality: newPure/tactic/prune_params_tac: newProvers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac3 AugustPure/tactic/rule_by_tactic: newZF/perm/compEpair: now proved via rule_by_tacticZF/extend_ind/cases,mk_cases: newZF/datatype/mk_free: newZF/list: now calls List.mk_cases4 AugustProvers/slow_tac,slow_best_tac: new5 AugustMAKE-ALL (Poly/ML) failed in ZFZF/sum/sumE2: deleted since unusedZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: newZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset6 AugustPure/goals/prepare_proof: after "Additional hypotheses", now actuallyprints them!ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed fromTransset_Union, Transset_InterZF/ordinal/Transset_Union: new ZF/univ/pair_in_univ: renamed Pair_in_univZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changeduses in extend_ind.ML, nat.ML, trancl.ML.ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.MLZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added9 AugustZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now onSyntax/sextension. 11 AugustPure/library.ML: added functionsassocs: (''a * 'b list) list -> ''a -> 'b listtransitive_closure: (''a * ''a list) list -> (''a * ''a list) listPure/type.ML: deleted (inefficient) transitive_closure