diff -r 4ac9d55573da -r 19849d258890 edits.txt --- a/edits.txt Fri Apr 04 17:01:12 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1372 +0,0 @@ -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