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<n)
and the nat_case rules and congruence rules
HOL/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 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<k assumption
18 June
MAKE-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 the
types, when exception TYPE is raised.
HOL/llist: some tidying
23 June
HOL/llist/Lconst_type: generalized from Lconst(M): LList({M})
24 June
MAKE-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 an
identifier 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 compatibility
25 June
MAKE-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" extension
HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation
HOL/llist/iterates_equality,lmap_lappend_distrib: tidied
28 June
HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable
name preservation
HOL/llist: co-induction rules applied with res_inst_tac to state the
bisimulation directly
2 July
MAKE-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 June
CHANGES 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" 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 <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 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