--- a/src/ZF/ex/Acc.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/Acc.ML Tue Jun 21 16:26:34 1994 +0200
@@ -18,37 +18,34 @@
val type_intrs = []
val type_elims = []);
+(*The introduction rule must require a:field(r)
+ Otherwise acc(r) would be a proper class! *)
+
goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)";
by (etac Acc.elim 1);
by (fast_tac ZF_cs 1);
val acc_downward = result();
-val [major] = goal Acc.thy "field(r) <= acc(r) ==> wf(r)";
-by (rtac (major RS wfI2) 1);
-by (rtac subsetI 1);
-by (etac Acc.induct 1);
-by (etac (bspec RS mp) 1);
+val [major,indhyp] = goal Acc.thy
+ "[| a : acc(r); \
+\ !!x. [| x: acc(r); ALL y. <y,x>:r --> P(y) |] ==> P(x) \
+\ |] ==> P(a)";
+br (major RS Acc.induct) 1;
+br indhyp 1;
+by (fast_tac ZF_cs 2);
by (resolve_tac Acc.intrs 1);
-by (assume_tac 2);
-by (ALLGOALS (fast_tac ZF_cs));
-val acc_wfI = result();
-
-goal ZF.thy "!!r A. field(r Int A*A) <= field(r) Int A";
+ba 2;
by (fast_tac ZF_cs 1);
-val field_Int_prodself = result();
+val acc_induct = result();
-goal Acc.thy "wf(r Int (acc(r)*acc(r)))";
-by (rtac (field_Int_prodself RS wfI2) 1);
-by (rtac subsetI 1);
-by (etac IntE 1);
-by (etac Acc.induct 1);
-by (etac (bspec RS mp) 1);
-by (rtac IntI 1);
-by (assume_tac 1);
-by (resolve_tac Acc.intrs 1);
-by (assume_tac 2);
-by (ALLGOALS (fast_tac ZF_cs));
-val wf_acc_Int = result();
+goal Acc.thy "wf[acc(r)](r)";
+br wf_onI2 1;
+be acc_induct 1;
+by (fast_tac ZF_cs 1);
+val wf_on_acc = result();
+
+(* field(r) <= acc(r) ==> wf(r) *)
+val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf;
val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)";
by (rtac subsetI 1);
--- a/src/ZF/ex/Bin.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/Bin.ML Tue Jun 21 16:26:34 1994 +0200
@@ -14,7 +14,8 @@
[(["Plus", "Minus"], "i"),
(["op $$"], "[i,i]=>i")])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext [OldMixfix.Infixl("$$", "[i,i] => i", 60)]);
+ val ext = Some (Syntax.simple_sext
+ [OldMixfix.Infixl("$$", "[i,i] => i", 60)]);
val sintrs =
["Plus : bin",
"Minus : bin",
--- a/src/ZF/ex/Comb.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/Comb.ML Tue Jun 21 16:26:34 1994 +0200
@@ -19,7 +19,8 @@
[(["K","S"], "i"),
(["op #"], "[i,i]=>i")])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext [OldMixfix.Infixl("#", "[i,i] => i", 90)]);
+ val ext = Some (Syntax.simple_sext
+ [OldMixfix.Infixl("#", "[i,i] => i", 90)]);
val sintrs =
["K : comb",
"S : comb",
--- a/src/ZF/ex/Equiv.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/Equiv.ML Tue Jun 21 16:26:34 1994 +0200
@@ -1,9 +1,9 @@
-(* Title: ZF/ex/equiv.ML
+(* Title: ZF/ex/Equiv.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
-For equiv.thy. Equivalence relations in Zermelo-Fraenkel Set Theory
+For Equiv.thy. Equivalence relations in Zermelo-Fraenkel Set Theory
*)
val RSLIST = curry (op MRS);
@@ -20,7 +20,7 @@
val sym_trans_comp_subset = result();
goalw Equiv.thy [refl_def]
- "!!A r. refl(A,r) ==> r <= converse(r) O r";
+ "!!A r. [| refl(A,r); r <= A*A |] ==> r <= converse(r) O r";
by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 1);
val refl_comp_subset = result();
@@ -80,9 +80,8 @@
by (fast_tac ZF_cs 1);
val equiv_class_nondisjoint = result();
-val [major] = goalw Equiv.thy [equiv_def,refl_def]
- "equiv(A,r) ==> r <= A*A";
-by (rtac (major RS conjunct1 RS conjunct1) 1);
+goalw Equiv.thy [equiv_def] "!!A r. equiv(A,r) ==> r <= A*A";
+by (safe_tac ZF_cs);
val equiv_type = result();
goal Equiv.thy
@@ -137,9 +136,9 @@
val prems as [equivA,bcong,_] = goal Equiv.thy
"[| equiv(A,r); congruent(r,b); a: A |] ==> (UN x:r``{a}. b(x)) = b(a)";
by (cut_facts_tac prems 1);
-by (rtac UN_singleton 1);
-by (etac equiv_class_self 1);
-by (assume_tac 1);
+by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1);
+by (etac equiv_class_self 2);
+by (assume_tac 2);
by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]);
by (fast_tac ZF_cs 1);
val UN_equiv_class = result();
--- a/src/ZF/ex/Equiv.thy Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/Equiv.thy Tue Jun 21 16:26:34 1994 +0200
@@ -1,23 +1,18 @@
-(* Title: ZF/ex/equiv.thy
+(* Title: ZF/ex/Equiv.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Equivalence relations in Zermelo-Fraenkel Set Theory
*)
-Equiv = Trancl +
+Equiv = Rel + Perm +
consts
- refl,equiv :: "[i,i]=>o"
- sym :: "i=>o"
"'/" :: "[i,i]=>i" (infixl 90) (*set of equiv classes*)
congruent :: "[i,i=>i]=>o"
congruent2 :: "[i,[i,i]=>i]=>o"
rules
- refl_def "refl(A,r) == r <= (A*A) & (ALL x: A. <x,x> : r)"
- sym_def "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
- equiv_def "equiv(A,r) == refl(A,r) & sym(r) & trans(r)"
quotient_def "A/r == {r``{x} . x:A}"
congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
--- a/src/ZF/ex/LList.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/LList.ML Tue Jun 21 16:26:34 1994 +0200
@@ -28,6 +28,15 @@
val LCons_iff = LList.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
val LNil_LCons_iff = LList.mk_free "~ LNil=LCons(a,l)";
+goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
+by (rtac (LList.unfold RS trans) 1);
+bws LList.con_defs;
+by (fast_tac (qsum_cs addIs ([equalityI] @ codatatype_intrs)
+ addDs [LList.dom_subset RS subsetD]
+ addEs [A_into_quniv]
+ addSEs [QSigmaE]) 1);
+val llist_unfold = result();
+
(*** Lemmas to justify using "llist" in other recursive type definitions ***)
goalw LList.thy LList.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
--- a/src/ZF/ex/ParContract.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/ParContract.ML Tue Jun 21 16:26:34 1994 +0200
@@ -22,7 +22,8 @@
val type_intrs = Comb.intrs@[SigmaI];
val type_elims = [SigmaE2]);
-val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] = ParContract.intrs;
+val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] =
+ ParContract.intrs;
val parcontract_induct = standard
(ParContract.mutual_induct RS spec RS spec RSN (2,rev_mp));
--- a/src/ZF/ex/Primrec0.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/Primrec0.ML Tue Jun 21 16:26:34 1994 +0200
@@ -92,7 +92,7 @@
val ack_typechecks =
[ACK_in_primrec, primrec_into_fun RS apply_type,
- add_type, list_add_type, naturals_are_ordinals] @
+ add_type, list_add_type, nat_into_Ord] @
nat_typechecks @ List.intrs @ Primrec.intrs;
(*strict typechecking for the Ackermann proof; instantiates no vars*)
@@ -127,7 +127,7 @@
val ack_ss =
pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ,
- ack_type, naturals_are_ordinals];
+ ack_type, nat_into_Ord];
(*PROPERTY A 4*)
goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j < ack(i,j)";
@@ -161,7 +161,7 @@
goal Primrec.thy
"!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)";
by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
-by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS naturals_are_ordinals] 1));
+by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
val ack_le_mono2 = result();
(*PROPERTY A 6*)
@@ -194,7 +194,7 @@
goal Primrec.thy
"!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
-by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS naturals_are_ordinals] 1));
+by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
val ack_le_mono1 = result();
(*PROPERTY A 8*)
@@ -247,8 +247,7 @@
(*** MAIN RESULT ***)
val ack2_ss =
- ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type,
- naturals_are_ordinals];
+ ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, nat_into_Ord];
goalw Primrec.thy [SC_def]
"!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))";
--- a/src/ZF/ex/TF.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/TF.ML Tue Jun 21 16:26:34 1994 +0200
@@ -47,19 +47,27 @@
addDs [TF.dom_subset RS subsetD]
addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
-goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
-by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
+goalw TF.thy (tl TF.defs)
+ "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
+by (rtac (TF.unfold RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
by (rtac equalityI 1);
by (fast_tac unfold_cs 1);
by (fast_tac unfold_cs 1);
+val tree_forest_unfold = result();
+
+val tree_forest_unfold' = rewrite_rule (tl TF.defs) tree_forest_unfold;
+
+
+goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
+br (Part_Inl RS subst) 1;
+br (tree_forest_unfold' RS subst_context) 1;
val tree_unfold = result();
goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
-by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
-by (rewrite_goals_tac TF.con_defs);
-by (rtac equalityI 1);
-by (fast_tac unfold_cs 1);
-by (fast_tac unfold_cs 1);
+br (Part_Inr RS subst) 1;
+br (tree_forest_unfold' RS subst_context) 1;
val forest_unfold = result();
+
+
--- a/src/ZF/ex/Term.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/Term.ML Tue Jun 21 16:26:34 1994 +0200
@@ -21,6 +21,15 @@
val [ApplyI] = Term.intrs;
+(*Note that Apply is the identity function*)
+goal Term.thy "term(A) = A * list(term(A))";
+by (rtac (Term.unfold RS trans) 1);
+bws Term.con_defs;
+by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
+ addDs [Term.dom_subset RS subsetD]
+ addEs [A_into_univ, list_into_univ]) 1);
+val term_unfold = result();
+
(*Induction on term(A) followed by induction on List *)
val major::prems = goal Term.thy
"[| t: term(A); \
@@ -61,6 +70,9 @@
by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1));
val term_univ = result();
-val term_subset_univ = standard
- (term_mono RS (term_univ RSN (2,subset_trans)));
+val term_subset_univ =
+ term_mono RS (term_univ RSN (2,subset_trans)) |> standard;
+goal Term.thy "!!t A B. [| t: term(A); A <= univ(B) |] ==> t: univ(B)";
+by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1));
+val term_into_univ = result();
--- a/src/ZF/ex/misc.ML Tue Jun 21 11:55:36 1994 +0200
+++ b/src/ZF/ex/misc.ML Tue Jun 21 16:26:34 1994 +0200
@@ -45,50 +45,6 @@
result();
-(**** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ****)
-
-val SB_thy = merge_theories (Fixedpt.thy, Perm.thy);
-
-(** Lemma: Banach's Decomposition Theorem **)
-
-goal SB_thy "bnd_mono(X, %W. X - g``(Y - f``W))";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
-val decomp_bnd_mono = result();
-
-val [gfun] = goal SB_thy
- "g: Y->X ==> \
-\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \
-\ X - lfp(X, %W. X - g``(Y - f``W)) ";
-by (res_inst_tac [("P", "%u. ?v = X-u")]
- (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
-by (simp_tac (ZF_ss addsimps [subset_refl, double_complement,
- gfun RS fun_is_rel RS image_subset]) 1);
-val Banach_last_equation = result();
-
-val prems = goal SB_thy
- "[| f: X->Y; g: Y->X |] ==> \
-\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
-\ (YA Int YB = 0) & (YA Un YB = Y) & \
-\ f``XA=YA & g``YB=XB";
-by (REPEAT
- (FIRSTGOAL
- (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
-by (rtac Banach_last_equation 3);
-by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
-val decomposition = result();
-
-val prems = goal SB_thy
- "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
-by (cut_facts_tac prems 1);
-by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
-by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un]
- addIs [bij_converse_bij]) 1);
-(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
- is forced by the context!! *)
-val schroeder_bernstein = result();
-
-
(*** Composition of homomorphisms is a homomorphism ***)
(*Given as a challenge problem in
@@ -98,9 +54,9 @@
*)
(*collecting the relevant lemmas*)
-val hom_ss = ZF_ss addsimps [comp_func,comp_func_apply,SigmaI,apply_funtype];
+val hom_ss = ZF_ss addsimps [comp_fun,comp_fun_apply,SigmaI,apply_funtype];
-(*The problem below is proving conditions of rewrites such as comp_func_apply;
+(*The problem below is proving conditions of rewrites such as comp_fun_apply;
rewriting does not instantiate Vars; we must prove the conditions
explicitly.*)
fun hom_tac hyps =
@@ -166,7 +122,7 @@
[comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2];
fun pastre_facts (fact1::fact2::fact3::prems) =
- forw_iterate (prems @ [comp_surj, comp_inj, comp_func])
+ forw_iterate (prems @ [comp_surj, comp_inj, comp_fun])
pastre_rls [fact1,fact2,fact3] 4;
val prems = goalw Perm.thy [bij_def]