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