Addition of cardinals and order types, various tidying
authorlcp
Tue Jun 21 17:20:34 1994 +0200 (1994-06-21 ago)
changeset 435ca5356bd315a
parent 434 89d45187f04d
child 436 0cdc840297bb
Addition of cardinals and order types, various tidying
src/ZF/Arith.ML
src/ZF/Cardinal.ML
src/ZF/Cardinal.thy
src/ZF/Fin.ML
src/ZF/Fin.thy
src/ZF/List.ML
src/ZF/List.thy
src/ZF/Makefile
src/ZF/Nat.ML
src/ZF/Nat.thy
src/ZF/Order.ML
src/ZF/Order.thy
src/ZF/OrderType.ML
src/ZF/OrderType.thy
src/ZF/Ordinal.ML
src/ZF/Ordinal.thy
src/ZF/Perm.ML
src/ZF/QPair.thy
src/ZF/ROOT.ML
src/ZF/Rel.ML
src/ZF/Rel.thy
src/ZF/Sum.ML
src/ZF/Trancl.ML
src/ZF/Trancl.thy
src/ZF/Univ.ML
src/ZF/Univ.thy
src/ZF/WF.ML
src/ZF/WF.thy
src/ZF/ZF.ML
src/ZF/equalities.ML
src/ZF/func.ML
src/ZF/ind_syntax.ML
src/ZF/intr_elim.ML
src/ZF/pair.ML
src/ZF/simpdata.ML
src/ZF/upair.ML
     1.1 --- a/src/ZF/Arith.ML	Tue Jun 21 16:26:34 1994 +0200
     1.2 +++ b/src/ZF/Arith.ML	Tue Jun 21 17:20:34 1994 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4      (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
     1.5  val rec_type = result();
     1.6  
     1.7 -val nat_le_refl = naturals_are_ordinals RS le_refl;
     1.8 +val nat_le_refl = nat_into_Ord RS le_refl;
     1.9  
    1.10  val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
    1.11  
    1.12 @@ -113,7 +113,7 @@
    1.13  by (ALLGOALS
    1.14      (asm_simp_tac
    1.15       (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
    1.16 -				diff_succ_succ, naturals_are_ordinals]))));
    1.17 +				diff_succ_succ, nat_into_Ord]))));
    1.18  val diff_le_self = result();
    1.19  
    1.20  (*** Simplification over add, mult, diff ***)
    1.21 @@ -150,12 +150,21 @@
    1.22  
    1.23  (*Commutative law for addition*)  
    1.24  val add_commute = prove_goal Arith.thy 
    1.25 -    "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
    1.26 - (fn prems=>
    1.27 -  [ (nat_ind_tac "n" prems 1),
    1.28 +    "!!m n. [| m:nat;  n:nat |] ==> m #+ n = n #+ m"
    1.29 + (fn _ =>
    1.30 +  [ (nat_ind_tac "n" [] 1),
    1.31      (ALLGOALS
    1.32 -     (asm_simp_tac
    1.33 -      (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
    1.34 +     (asm_simp_tac (arith_ss addsimps [add_0_right, add_succ_right]))) ]);
    1.35 +
    1.36 +val add_left_commute = prove_goal Arith.thy
    1.37 +    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> m#+(n#+k)=n#+(m#+k)"
    1.38 + (fn _ => [rtac (add_commute RS trans) 1, 
    1.39 +           rtac (add_assoc RS trans) 3, 
    1.40 +	   rtac (add_commute RS subst_context) 4,
    1.41 +	   REPEAT (ares_tac [add_type] 1)]);
    1.42 +
    1.43 +(*Addition is an AC-operator*)
    1.44 +val add_ac = [add_assoc, add_commute, add_left_commute];
    1.45  
    1.46  (*Cancellation law on the left*)
    1.47  val [knat,eqn] = goal Arith.thy 
    1.48 @@ -170,20 +179,17 @@
    1.49  
    1.50  (*right annihilation in product*)
    1.51  val mult_0_right = prove_goal Arith.thy 
    1.52 -    "m:nat ==> m #* 0 = 0"
    1.53 - (fn prems=>
    1.54 -  [ (nat_ind_tac "m" prems 1),
    1.55 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
    1.56 +    "!!m. m:nat ==> m #* 0 = 0"
    1.57 + (fn _=>
    1.58 +  [ (nat_ind_tac "m" [] 1),
    1.59 +    (ALLGOALS (asm_simp_tac arith_ss))  ]);
    1.60  
    1.61  (*right successor law for multiplication*)
    1.62  val mult_succ_right = prove_goal Arith.thy 
    1.63      "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
    1.64 - (fn _=>
    1.65 + (fn _ =>
    1.66    [ (nat_ind_tac "m" [] 1),
    1.67 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
    1.68 -       (*The final goal requires the commutative law for addition*)
    1.69 -    (rtac (add_commute RS subst_context) 1),
    1.70 -    (REPEAT (assume_tac 1))  ]);
    1.71 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps add_ac))) ]);
    1.72  
    1.73  (*Commutative law for multiplication*)
    1.74  val mult_commute = prove_goal Arith.thy 
    1.75 @@ -202,12 +208,11 @@
    1.76  
    1.77  (*Distributive law on the left; requires an extra typing premise*)
    1.78  val add_mult_distrib_left = prove_goal Arith.thy 
    1.79 -    "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
    1.80 +    "!!m. [| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
    1.81   (fn prems=>
    1.82 -      let val mult_commute' = read_instantiate [("m","k")] mult_commute
    1.83 -          val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
    1.84 -      in [ (simp_tac ss 1) ]
    1.85 -      end);
    1.86 +  [ (nat_ind_tac "m" [] 1),
    1.87 +    (asm_simp_tac (arith_ss addsimps [mult_0_right]) 1),
    1.88 +    (asm_simp_tac (arith_ss addsimps ([mult_succ_right] @ add_ac)) 1) ]);
    1.89  
    1.90  (*Associative law for multiplication*)
    1.91  val mult_assoc = prove_goal Arith.thy 
    1.92 @@ -261,9 +266,9 @@
    1.93  val div_rls =	(*for mod and div*)
    1.94      nat_typechecks @
    1.95      [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
    1.96 -     naturals_are_ordinals, not_lt_iff_le RS iffD1];
    1.97 +     nat_into_Ord, not_lt_iff_le RS iffD1];
    1.98  
    1.99 -val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
   1.100 +val div_ss = ZF_ss addsimps [nat_into_Ord, div_termination RS ltD,
   1.101  			     not_lt_iff_le RS iffD2];
   1.102  
   1.103  (*Type checking depends upon termination!*)
   1.104 @@ -311,7 +316,7 @@
   1.105  by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
   1.106  (*case n le x*)
   1.107  by (asm_full_simp_tac
   1.108 -     (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
   1.109 +     (arith_ss addsimps [not_lt_iff_le, nat_into_Ord,
   1.110  			 mod_geq, div_geq, add_assoc,
   1.111  			 div_termination RS ltD, add_diff_inverse]) 1);
   1.112  val mod_div_equality = result();
   1.113 @@ -350,7 +355,7 @@
   1.114  val add_lt_mono = result();
   1.115  
   1.116  (*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   1.117 -val lt_mono::ford::prems = goal Ord.thy
   1.118 +val lt_mono::ford::prems = goal Ordinal.thy
   1.119       "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
   1.120  \        !!i. i:k ==> Ord(f(i));		\
   1.121  \        i le j;  j:k				\
   1.122 @@ -363,7 +368,7 @@
   1.123  goal Arith.thy
   1.124      "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
   1.125  by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
   1.126 -by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
   1.127 +by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
   1.128  val add_le_mono1 = result();
   1.129  
   1.130  (* le monotonicity, BOTH arguments*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/Cardinal.ML	Tue Jun 21 17:20:34 1994 +0200
     2.3 @@ -0,0 +1,352 @@
     2.4 +(*  Title: 	ZF/Cardinal.ML
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1994  University of Cambridge
     2.8 +
     2.9 +Cardinals in Zermelo-Fraenkel Set Theory 
    2.10 +
    2.11 +This theory does NOT assume the Axiom of Choice
    2.12 +*)
    2.13 +
    2.14 +open Cardinal;
    2.15 +
    2.16 +(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
    2.17 +
    2.18 +(** Lemma: Banach's Decomposition Theorem **)
    2.19 +
    2.20 +goal Cardinal.thy "bnd_mono(X, %W. X - g``(Y - f``W))";
    2.21 +by (rtac bnd_monoI 1);
    2.22 +by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
    2.23 +val decomp_bnd_mono = result();
    2.24 +
    2.25 +val [gfun] = goal Cardinal.thy
    2.26 +    "g: Y->X ==>   					\
    2.27 +\    g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = 	\
    2.28 +\    X - lfp(X, %W. X - g``(Y - f``W)) ";
    2.29 +by (res_inst_tac [("P", "%u. ?v = X-u")] 
    2.30 +     (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
    2.31 +by (simp_tac (ZF_ss addsimps [subset_refl, double_complement,
    2.32 +			     gfun RS fun_is_rel RS image_subset]) 1);
    2.33 +val Banach_last_equation = result();
    2.34 +
    2.35 +val prems = goal Cardinal.thy
    2.36 +    "[| f: X->Y;  g: Y->X |] ==>   \
    2.37 +\    EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &    \
    2.38 +\                    (YA Int YB = 0) & (YA Un YB = Y) &    \
    2.39 +\                    f``XA=YA & g``YB=XB";
    2.40 +by (REPEAT 
    2.41 +    (FIRSTGOAL
    2.42 +     (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
    2.43 +by (rtac Banach_last_equation 3);
    2.44 +by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
    2.45 +val decomposition = result();
    2.46 +
    2.47 +val prems = goal Cardinal.thy
    2.48 +    "[| f: inj(X,Y);  g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
    2.49 +by (cut_facts_tac prems 1);
    2.50 +by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
    2.51 +by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un]
    2.52 +                    addIs [bij_converse_bij]) 1);
    2.53 +(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
    2.54 +   is forced by the context!! *)
    2.55 +val schroeder_bernstein = result();
    2.56 +
    2.57 +
    2.58 +(** Equipollence is an equivalence relation **)
    2.59 +
    2.60 +goalw Cardinal.thy [eqpoll_def] "X eqpoll X";
    2.61 +br exI 1;
    2.62 +br id_bij 1;
    2.63 +val eqpoll_refl = result();
    2.64 +
    2.65 +goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X";
    2.66 +by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1);
    2.67 +val eqpoll_sym = result();
    2.68 +
    2.69 +goalw Cardinal.thy [eqpoll_def]
    2.70 +    "!!X Y. [| X eqpoll Y;  Y eqpoll Z |] ==> X eqpoll Z";
    2.71 +by (fast_tac (ZF_cs addIs [comp_bij]) 1);
    2.72 +val eqpoll_trans = result();
    2.73 +
    2.74 +(** Le-pollence is a partial ordering **)
    2.75 +
    2.76 +goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y";
    2.77 +br exI 1;
    2.78 +be id_subset_inj 1;
    2.79 +val subset_imp_lepoll = result();
    2.80 +
    2.81 +val lepoll_refl = subset_refl RS subset_imp_lepoll;
    2.82 +
    2.83 +goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def]
    2.84 +    "!!X Y. X eqpoll Y ==> X lepoll Y";
    2.85 +by (fast_tac ZF_cs 1);
    2.86 +val eqpoll_imp_lepoll = result();
    2.87 +
    2.88 +goalw Cardinal.thy [lepoll_def]
    2.89 +    "!!X Y. [| X lepoll Y;  Y lepoll Z |] ==> X lepoll Z";
    2.90 +by (fast_tac (ZF_cs addIs [comp_inj]) 1);
    2.91 +val lepoll_trans = result();
    2.92 +
    2.93 +(*Asymmetry law*)
    2.94 +goalw Cardinal.thy [lepoll_def,eqpoll_def]
    2.95 +    "!!X Y. [| X lepoll Y;  Y lepoll X |] ==> X eqpoll Y";
    2.96 +by (REPEAT (etac exE 1));
    2.97 +by (rtac schroeder_bernstein 1);
    2.98 +by (REPEAT (assume_tac 1));
    2.99 +val eqpollI = result();
   2.100 +
   2.101 +val [major,minor] = goal Cardinal.thy
   2.102 +    "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P";
   2.103 +br minor 1;
   2.104 +by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));
   2.105 +val eqpollE = result();
   2.106 +
   2.107 +goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X";
   2.108 +by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1);
   2.109 +val eqpoll_iff = result();
   2.110 +
   2.111 +
   2.112 +(** LEAST -- the least number operator [from HOL/Univ.ML] **)
   2.113 +
   2.114 +val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
   2.115 +    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x.P(x)) = i";
   2.116 +by (rtac the_equality 1);
   2.117 +by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1);
   2.118 +by (REPEAT (etac conjE 1));
   2.119 +be (premOrd RS Ord_linear_lt) 1;
   2.120 +by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot])));
   2.121 +val Least_equality = result();
   2.122 +
   2.123 +goal Cardinal.thy "!!i. [| P(i);  Ord(i) |] ==> P(LEAST x.P(x))";
   2.124 +by (etac rev_mp 1);
   2.125 +by (trans_ind_tac "i" [] 1);
   2.126 +by (rtac impI 1);
   2.127 +by (rtac classical 1);
   2.128 +by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
   2.129 +by (assume_tac 2);
   2.130 +by (fast_tac (ZF_cs addSEs [ltE]) 1);
   2.131 +val LeastI = result();
   2.132 +
   2.133 +(*Proof is almost identical to the one above!*)
   2.134 +goal Cardinal.thy "!!i. [| P(i);  Ord(i) |] ==> (LEAST x.P(x)) le i";
   2.135 +by (etac rev_mp 1);
   2.136 +by (trans_ind_tac "i" [] 1);
   2.137 +by (rtac impI 1);
   2.138 +by (rtac classical 1);
   2.139 +by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
   2.140 +by (etac le_refl 2);
   2.141 +by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);
   2.142 +val Least_le = result();
   2.143 +
   2.144 +(*LEAST really is the smallest*)
   2.145 +goal Cardinal.thy "!!i. [| P(i);  i < (LEAST x.P(x)) |] ==> Q";
   2.146 +br (Least_le RSN (2,lt_trans2) RS lt_anti_refl) 1;
   2.147 +by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
   2.148 +val less_LeastE = result();
   2.149 +
   2.150 +goal Cardinal.thy "Ord(LEAST x.P(x))";
   2.151 +by (res_inst_tac [("Q","EX i. Ord(i) & P(i)")] (excluded_middle RS disjE) 1);
   2.152 +by (safe_tac ZF_cs);
   2.153 +br (Least_le RS ltE) 2;
   2.154 +by (REPEAT_SOME assume_tac);
   2.155 +bw Least_def;
   2.156 +by (rtac (the_0 RS ssubst) 1 THEN rtac Ord_0 2);
   2.157 +by (fast_tac FOL_cs 1);
   2.158 +val Ord_Least = result();
   2.159 +
   2.160 +
   2.161 +(** Basic properties of cardinals **)
   2.162 +
   2.163 +(*Not needed for simplification, but helpful below*)
   2.164 +val prems = goal Cardinal.thy
   2.165 +    "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))";
   2.166 +by (simp_tac (FOL_ss addsimps prems) 1);
   2.167 +val Least_cong = result();
   2.168 +
   2.169 +(*Need AC to prove   X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le  *)
   2.170 +goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
   2.171 +br Least_cong 1;
   2.172 +by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1);
   2.173 +val cardinal_cong = result();
   2.174 +
   2.175 +(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
   2.176 +goalw Cardinal.thy [eqpoll_def, cardinal_def]
   2.177 +    "!!A. well_ord(A,r) ==> |A| eqpoll A";
   2.178 +br LeastI 1;
   2.179 +be Ord_ordertype 2;
   2.180 +br exI 1;
   2.181 +be (ordertype_bij RS bij_converse_bij) 1;
   2.182 +val well_ord_cardinal_eqpoll = result();
   2.183 +
   2.184 +val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll 
   2.185 +                          |> standard;
   2.186 +
   2.187 +goal Cardinal.thy
   2.188 +    "!!X Y. [| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X eqpoll Y";
   2.189 +br (eqpoll_sym RS eqpoll_trans) 1;
   2.190 +be well_ord_cardinal_eqpoll 1;
   2.191 +by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1);
   2.192 +val well_ord_cardinal_eqE = result();
   2.193 +
   2.194 +
   2.195 +(** Observations from Kunen, page 28 **)
   2.196 +
   2.197 +goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i";
   2.198 +be (eqpoll_refl RS Least_le) 1;
   2.199 +val Ord_cardinal_le = result();
   2.200 +
   2.201 +goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> |i| = i";
   2.202 +be sym 1;
   2.203 +val Card_cardinal_eq = result();
   2.204 +
   2.205 +val prems = goalw Cardinal.thy [Card_def,cardinal_def]
   2.206 +    "[| Ord(i);  !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
   2.207 +br (Least_equality RS ssubst) 1;
   2.208 +by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
   2.209 +val CardI = result();
   2.210 +
   2.211 +goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)";
   2.212 +be ssubst 1;
   2.213 +br Ord_Least 1;
   2.214 +val Card_is_Ord = result();
   2.215 +
   2.216 +goalw Cardinal.thy [cardinal_def] "Ord( |i| )";
   2.217 +br Ord_Least 1;
   2.218 +val Ord_cardinal = result();
   2.219 +
   2.220 +(*Kunen's Lemma 10.5*)
   2.221 +goal Cardinal.thy "!!i j. [| |i| le j;  j le i |] ==> |j| = |i|";
   2.222 +br (eqpollI RS cardinal_cong) 1;
   2.223 +be (le_imp_subset RS subset_imp_lepoll) 1;
   2.224 +br lepoll_trans 1;
   2.225 +be (le_imp_subset RS subset_imp_lepoll) 2;
   2.226 +br (eqpoll_sym RS eqpoll_imp_lepoll) 1;
   2.227 +br Ord_cardinal_eqpoll 1;
   2.228 +by (REPEAT (eresolve_tac [ltE, Ord_succD] 1));
   2.229 +val cardinal_eq_lemma = result();
   2.230 +
   2.231 +goal Cardinal.thy "!!i j. i le j ==> |i| le |j|";
   2.232 +by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1);
   2.233 +by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
   2.234 +br cardinal_eq_lemma 1;
   2.235 +ba 2;
   2.236 +be le_trans 1;
   2.237 +be ltE 1;
   2.238 +be Ord_cardinal_le 1;
   2.239 +val cardinal_mono = result();
   2.240 +
   2.241 +(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
   2.242 +goal Cardinal.thy "!!i j. [| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j";
   2.243 +br Ord_linear2 1;
   2.244 +by (REPEAT_SOME assume_tac);
   2.245 +be (lt_trans2 RS lt_anti_refl) 1;
   2.246 +be cardinal_mono 1;
   2.247 +val cardinal_lt_imp_lt = result();
   2.248 +
   2.249 +goal Cardinal.thy "!!i j. [| |i| < k;  Ord(i);  Card(k) |] ==> i < k";
   2.250 +by (asm_simp_tac (ZF_ss addsimps 
   2.251 +		  [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1);
   2.252 +val Card_lt_imp_lt = result();
   2.253 +
   2.254 +
   2.255 +(** The swap operator [NOT USED] **)
   2.256 +
   2.257 +goalw Cardinal.thy [swap_def]
   2.258 +    "!!A. [| x:A;  y:A |] ==> swap(A,x,y) : A->A";
   2.259 +by (REPEAT (ares_tac [lam_type,if_type] 1));
   2.260 +val swap_type = result();
   2.261 +
   2.262 +goalw Cardinal.thy [swap_def]
   2.263 +    "!!A. [| x:A;  y:A;  z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z";
   2.264 +by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
   2.265 +val swap_swap_identity = result();
   2.266 +
   2.267 +goal Cardinal.thy "!!A. [| x:A;  y:A |] ==> swap(A,x,y) : bij(A,A)";
   2.268 +br nilpotent_imp_bijective 1;
   2.269 +by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2,
   2.270 +		      ballI, swap_swap_identity] 1));
   2.271 +val swap_bij = result();
   2.272 +
   2.273 +(*** The finite cardinals ***)
   2.274 +
   2.275 +(*Lemma suggested by Mike Fourman*)
   2.276 +val [prem] = goalw Cardinal.thy [inj_def]
   2.277 + "f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)";
   2.278 +br CollectI 1;
   2.279 +(*Proving it's in the function space m->n*)
   2.280 +by (cut_facts_tac [prem] 1);
   2.281 +br (if_type RS lam_type) 1;
   2.282 +by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1);
   2.283 +by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1);
   2.284 +(*Proving it's injective*)
   2.285 +by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
   2.286 +(*Adding  prem  earlier would cause the simplifier to loop*)
   2.287 +by (cut_facts_tac [prem] 1);
   2.288 +by (fast_tac (ZF_cs addSEs [mem_anti_refl]) 1);
   2.289 +val inj_succ_succD = result();
   2.290 +
   2.291 +val [prem] = goalw Cardinal.thy [lepoll_def]
   2.292 +    "m:nat ==> ALL n: nat. m lepoll n --> m le n";
   2.293 +by (nat_ind_tac "m" [prem] 1);
   2.294 +by (fast_tac (ZF_cs addSIs [nat_0_le]) 1);
   2.295 +br ballI 1;
   2.296 +by (eres_inst_tac [("n","n")] natE 1);
   2.297 +by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);
   2.298 +by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1);
   2.299 +val nat_lepoll_imp_le_lemma = result();
   2.300 +val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard;
   2.301 +
   2.302 +goal Cardinal.thy
   2.303 +    "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
   2.304 +br iffI 1;
   2.305 +by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
   2.306 +by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_asym] addSEs [eqpollE]) 1);
   2.307 +val nat_eqpoll_iff = result();
   2.308 +
   2.309 +goalw Cardinal.thy [Card_def,cardinal_def]
   2.310 +    "!!n. n: nat ==> Card(n)";
   2.311 +br (Least_equality RS ssubst) 1;
   2.312 +by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
   2.313 +by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
   2.314 +by (fast_tac (ZF_cs addSEs [lt_anti_refl]) 1);
   2.315 +val nat_into_Card = result();
   2.316 +
   2.317 +val Card_0 = nat_0I RS nat_into_Card;
   2.318 +
   2.319 +(*Part of Kunen's Lemma 10.6*)
   2.320 +goal Cardinal.thy "!!n. [| succ(n) lepoll n;  n:nat |] ==> P";
   2.321 +br (nat_lepoll_imp_le RS lt_anti_refl) 1;
   2.322 +by (REPEAT (ares_tac [nat_succI] 1));
   2.323 +val succ_lepoll_natE = result();
   2.324 +
   2.325 +
   2.326 +(*** The first infinite cardinal: Omega, or nat ***)
   2.327 +
   2.328 +(*This implies Kunen's Lemma 10.6*)
   2.329 +goal Cardinal.thy "!!n. [| n<i;  n:nat |] ==> ~ i lepoll n";
   2.330 +br notI 1;
   2.331 +by (rtac succ_lepoll_natE 1 THEN assume_tac 2);
   2.332 +by (rtac lepoll_trans 1 THEN assume_tac 2);
   2.333 +be ltE 1;
   2.334 +by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1));
   2.335 +val lt_not_lepoll = result();
   2.336 +
   2.337 +goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";
   2.338 +br (Least_equality RS ssubst) 1;
   2.339 +by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
   2.340 +be ltE 1;
   2.341 +by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
   2.342 +val Card_nat = result();
   2.343 +
   2.344 +goal Cardinal.thy "!!i n. [| Ord(i);  n:nat |] ==> i eqpoll n <-> i=n";
   2.345 +br iffI 1;
   2.346 +by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
   2.347 +by (rtac Ord_linear_lt 1);
   2.348 +by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord]));
   2.349 +by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN
   2.350 +    REPEAT (assume_tac 1));
   2.351 +by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1)));
   2.352 +be eqpoll_imp_lepoll 1;
   2.353 +val Ord_nat_eqpoll_iff = result();
   2.354 +
   2.355 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Cardinal.thy	Tue Jun 21 17:20:34 1994 +0200
     3.3 @@ -0,0 +1,33 @@
     3.4 +(*  Title: 	ZF/Cardinal.thy
     3.5 +    ID:         $Id$
     3.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1994  University of Cambridge
     3.8 +
     3.9 +Cardinals in Zermelo-Fraenkel Set Theory 
    3.10 +*)
    3.11 +
    3.12 +Cardinal = OrderType + Fixedpt + Nat + Sum + 
    3.13 +consts
    3.14 +  Least            :: "(i=>o) => i"    (binder "LEAST " 10)
    3.15 +  eqpoll, lepoll   :: "[i,i] => o"     (infixl 50)
    3.16 +  "cardinal"       :: "i=>i"           ("|_|")
    3.17 +  Card             :: "i=>o"
    3.18 +
    3.19 +  swap       :: "[i,i,i]=>i"     (*not used; useful??*)
    3.20 +
    3.21 +rules
    3.22 +
    3.23 +  (*least ordinal operator*)
    3.24 +  Least_def  "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
    3.25 +
    3.26 +  eqpoll_def "A eqpoll B == EX f. f: bij(A,B)"
    3.27 +
    3.28 +  lepoll_def "A lepoll B == EX f. f: inj(A,B)"
    3.29 +
    3.30 +  cardinal_def "|A| == LEAST i. i eqpoll A"
    3.31 +
    3.32 +  Card_def     "Card(i) == ( i = |i| )"
    3.33 +
    3.34 +  swap_def   "swap(A,x,y) == (lam z:A. if(z=x, y, if(z=y, x, z)))"
    3.35 +
    3.36 +end
     4.1 --- a/src/ZF/Fin.ML	Tue Jun 21 16:26:34 1994 +0200
     4.2 +++ b/src/ZF/Fin.ML	Tue Jun 21 17:20:34 1994 +0200
     4.3 @@ -1,12 +1,10 @@
     4.4 -(*  Title: 	ZF/ex/fin.ML
     4.5 +(*  Title: 	ZF/ex/Fin.ML
     4.6      ID:         $Id$
     4.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1993  University of Cambridge
     4.9  
    4.10  Finite powerset operator
    4.11  
    4.12 -could define cardinality?
    4.13 -
    4.14  prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n)
    4.15  	card(0)=0
    4.16  	[| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b))
     5.1 --- a/src/ZF/Fin.thy	Tue Jun 21 16:26:34 1994 +0200
     5.2 +++ b/src/ZF/Fin.thy	Tue Jun 21 17:20:34 1994 +0200
     5.3 @@ -1,3 +1,3 @@
     5.4  (*Dummy theory to document dependencies *)
     5.5  
     5.6 -fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
     5.7 +Fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
     6.1 --- a/src/ZF/List.ML	Tue Jun 21 16:26:34 1994 +0200
     6.2 +++ b/src/ZF/List.ML	Tue Jun 21 17:20:34 1994 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title: 	ZF/list.ML
     6.5 +(*  Title: 	ZF/List.ML
     6.6      ID:         $Id$
     6.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8      Copyright   1993  University of Cambridge
     6.9 @@ -36,6 +36,14 @@
    6.10  	   rename_last_tac a ["1"] (i+2),
    6.11  	   ares_tac prems i];
    6.12  
    6.13 +goal List.thy "list(A) = {0} + (A * list(A))";
    6.14 +by (rtac (List.unfold RS trans) 1);
    6.15 +bws List.con_defs;
    6.16 +by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
    6.17 +		     addDs [List.dom_subset RS subsetD]
    6.18 + 	             addEs [A_into_univ]) 1);
    6.19 +val list_unfold = result();
    6.20 +
    6.21  (**  Lemmas to justify using "list" in other recursive type definitions **)
    6.22  
    6.23  goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";
    6.24 @@ -54,6 +62,10 @@
    6.25  
    6.26  val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans);
    6.27  
    6.28 +goal List.thy "!!l A B. [| l: list(A);  A <= univ(B) |] ==> l: univ(B)";
    6.29 +by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
    6.30 +val list_into_univ = result();
    6.31 +
    6.32  val major::prems = goal List.thy
    6.33      "[| l: list(A);    \
    6.34  \       c: C(Nil);       \
     7.1 --- a/src/ZF/List.thy	Tue Jun 21 16:26:34 1994 +0200
     7.2 +++ b/src/ZF/List.thy	Tue Jun 21 17:20:34 1994 +0200
     7.3 @@ -1,3 +1,3 @@
     7.4  (*Dummy theory to document dependencies *)
     7.5  
     7.6 -list = Univ + "Datatype" + "intr_elim"
     7.7 +List = Univ + "Datatype" + "intr_elim"
     8.1 --- a/src/ZF/Makefile	Tue Jun 21 16:26:34 1994 +0200
     8.2 +++ b/src/ZF/Makefile	Tue Jun 21 17:20:34 1994 +0200
     8.3 @@ -22,8 +22,11 @@
     8.4  	func.ML simpdata.ML Bool.thy Bool.ML \
     8.5  	Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
     8.6  	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
     8.7 -	equalities.ML Perm.thy Perm.ML Trancl.thy Trancl.ML \
     8.8 -	WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \
     8.9 +	equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
    8.10 +	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
    8.11 +	OrderType.thy OrderType.ML OrderArith.thy OrderArith.ML \
    8.12 +	Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
    8.13 +	Nat.thy Nat.ML \
    8.14  	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
    8.15  	QUniv.thy QUniv.ML constructor.ML Datatype.ML  \
    8.16  	Fin.ML List.ML ListFn.thy ListFn.ML
    8.17 @@ -44,7 +47,8 @@
    8.18  	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
    8.19  		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
    8.20  	sml*)	echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
    8.21 -	*)	echo Bad value for ISABELLECOMP;;\
    8.22 +	*)	echo Bad value for ISABELLECOMP: \
    8.23 +                	$(COMP) is not poly or sml;;\
    8.24  	esac
    8.25  
    8.26  $(BIN)/FOL:
    8.27 @@ -54,7 +58,8 @@
    8.28  	case "$(COMP)" in \
    8.29  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\
    8.30  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\
    8.31 -	*)	echo Bad value for ISABELLECOMP;;\
    8.32 +	*)	echo Bad value for ISABELLECOMP: \
    8.33 +                	$(COMP) is not poly or sml;;\
    8.34  	esac
    8.35  
    8.36  .PRECIOUS:  $(BIN)/FOL $(BIN)/ZF 
     9.1 --- a/src/ZF/Nat.ML	Tue Jun 21 16:26:34 1994 +0200
     9.2 +++ b/src/ZF/Nat.ML	Tue Jun 21 17:20:34 1994 +0200
     9.3 @@ -68,10 +68,12 @@
     9.4  val prems = goal Nat.thy "n: nat ==> Ord(n)";
     9.5  by (nat_ind_tac "n" prems 1);
     9.6  by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
     9.7 -val naturals_are_ordinals = result();
     9.8 +val nat_into_Ord = result();
     9.9  
    9.10  (* i: nat ==> 0 le i *)
    9.11 -val nat_0_le = naturals_are_ordinals RS Ord_0_le;
    9.12 +val nat_0_le = nat_into_Ord RS Ord_0_le;
    9.13 +
    9.14 +val nat_le_refl = nat_into_Ord RS le_refl;
    9.15  
    9.16  goal Nat.thy "!!n. n: nat ==> n=0 | 0:n";
    9.17  by (etac nat_induct 1);
    9.18 @@ -81,18 +83,23 @@
    9.19  
    9.20  goal Nat.thy "Ord(nat)";
    9.21  by (rtac OrdI 1);
    9.22 -by (etac (naturals_are_ordinals RS Ord_is_Transset) 2);
    9.23 +by (etac (nat_into_Ord RS Ord_is_Transset) 2);
    9.24  by (rewtac Transset_def);
    9.25  by (rtac ballI 1);
    9.26  by (etac nat_induct 1);
    9.27  by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));
    9.28  val Ord_nat = result();
    9.29  
    9.30 +goalw Nat.thy [Limit_def] "Limit(nat)";
    9.31 +by (safe_tac (ZF_cs addSIs [ltI, nat_0I, nat_1I, nat_succI, Ord_nat]));
    9.32 +by (etac ltD 1);
    9.33 +val Limit_nat = result();
    9.34 +
    9.35  (* succ(i): nat ==> i: nat *)
    9.36  val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;
    9.37  
    9.38  (* [| succ(i): k;  k: nat |] ==> i: k *)
    9.39 -val succ_in_naturalD = [succI1, asm_rl, naturals_are_ordinals] MRS Ord_trans;
    9.40 +val succ_in_naturalD = [succI1, asm_rl, nat_into_Ord] MRS Ord_trans;
    9.41  
    9.42  goal Nat.thy "!!m n. [| m<n;  n: nat |] ==> m: nat";
    9.43  by (etac ltE 1);
    10.1 --- a/src/ZF/Nat.thy	Tue Jun 21 16:26:34 1994 +0200
    10.2 +++ b/src/ZF/Nat.thy	Tue Jun 21 17:20:34 1994 +0200
    10.3 @@ -1,12 +1,12 @@
    10.4 -(*  Title: 	ZF/nat.thy
    10.5 +(*  Title: 	ZF/Nat.thy
    10.6      ID:         $Id$
    10.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    10.8 -    Copyright   1992  University of Cambridge
    10.9 +    Copyright   1994  University of Cambridge
   10.10  
   10.11  Natural numbers in Zermelo-Fraenkel Set Theory 
   10.12  *)
   10.13  
   10.14 -Nat = Ord + Bool + "mono" +
   10.15 +Nat = Ordinal + Bool + "mono" +
   10.16  consts
   10.17      nat 	::      "i"
   10.18      nat_case    ::      "[i, i=>i, i]=>i"
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/ZF/Order.ML	Tue Jun 21 17:20:34 1994 +0200
    11.3 @@ -0,0 +1,185 @@
    11.4 +(*  Title: 	ZF/Order.ML
    11.5 +    ID:         $Id$
    11.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Copyright   1994  University of Cambridge
    11.8 +
    11.9 +For Order.thy.  Orders in Zermelo-Fraenkel Set Theory 
   11.10 +*)
   11.11 +
   11.12 +(*TO PURE/TACTIC.ML*)
   11.13 +fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   11.14 +
   11.15 +
   11.16 +open Order;
   11.17 +
   11.18 +val bij_apply_cs = ZF_cs addSEs [bij_converse_bij]
   11.19 +                         addIs  [bij_is_fun, apply_type];
   11.20 +
   11.21 +val bij_inverse_ss = 
   11.22 +    ZF_ss addsimps [bij_is_fun RS apply_type,
   11.23 +		    bij_converse_bij RS bij_is_fun RS apply_type,
   11.24 +		    left_inverse_bij, right_inverse_bij];
   11.25 +
   11.26 +(** Basic properties of the definitions **)
   11.27 +
   11.28 +(*needed????*)
   11.29 +goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def]
   11.30 +    "!!r. part_ord(A,r) ==> asym(r Int A*A)";
   11.31 +by (fast_tac ZF_cs 1);
   11.32 +val part_ord_Imp_asym = result();
   11.33 +
   11.34 +(** Order-isomorphisms **)
   11.35 +
   11.36 +goalw Order.thy [ord_iso_def] 
   11.37 +    "!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)";
   11.38 +by (etac CollectD1 1);
   11.39 +val ord_iso_is_bij = result();
   11.40 +
   11.41 +goalw Order.thy [ord_iso_def] 
   11.42 +    "!!f. [| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> \
   11.43 +\         <f`x, f`y> : s";
   11.44 +by (fast_tac ZF_cs 1);
   11.45 +val ord_iso_apply = result();
   11.46 +
   11.47 +goalw Order.thy [ord_iso_def] 
   11.48 +    "!!f. [| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] ==> \
   11.49 +\         <converse(f) ` x, converse(f) ` y> : r";
   11.50 +be CollectE 1;
   11.51 +be (bspec RS bspec RS iffD2) 1;
   11.52 +by (REPEAT (eresolve_tac [asm_rl, 
   11.53 +			  bij_converse_bij RS bij_is_fun RS apply_type] 1));
   11.54 +by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
   11.55 +val ord_iso_converse = result();
   11.56 +
   11.57 +val major::premx::premy::prems = goalw Order.thy [linear_def]
   11.58 +    "[| linear(A,r);  x:A;  y:A;  \
   11.59 +\       <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |] ==> P";
   11.60 +by (cut_facts_tac [major,premx,premy] 1);
   11.61 +by (REPEAT_FIRST (eresolve_tac [ballE,disjE]));
   11.62 +by (EVERY1 (map etac prems));
   11.63 +by (ALLGOALS contr_tac);
   11.64 +val linearE = result();
   11.65 +
   11.66 +(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*)
   11.67 +val linear_case_tac =
   11.68 +    SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1,
   11.69 +			REPEAT_SOME assume_tac]);
   11.70 +
   11.71 +(*Inductive argument for proving Kunen's Lemma 6.1*)
   11.72 +goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def, pred_def]
   11.73 +  "!!r. [| well_ord(A,r);  x: A;  f: ord_iso(A, r, pred(A,x,r), r);  y: A |] \
   11.74 +\       ==> f`y = y";
   11.75 +by (safe_tac ZF_cs);
   11.76 +by (wf_on_ind_tac "y" [] 1);
   11.77 +by (forward_tac [ord_iso_is_bij] 1);
   11.78 +by (subgoal_tac "f`y1 : {y: A . <y, x> : r}" 1);
   11.79 +by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]) 2);
   11.80 +(*Now we know f`y1 : A  and  <f`y1, x> : r  *)
   11.81 +by (etac CollectE 1);
   11.82 +by (linear_case_tac 1);
   11.83 +(*Case  <f`y1, y1> : r *)   (*use induction hyp*)
   11.84 +by (dtac bspec 1 THEN mp_tac 2 THEN assume_tac 1);
   11.85 +by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
   11.86 +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
   11.87 +(*The case  <y1, f`y1> : r  *)
   11.88 +by (subgoal_tac "<y1,x> : r" 1);
   11.89 +by (fast_tac (ZF_cs addSEs [trans_onD]) 2);
   11.90 +by (dtac ord_iso_converse 1 THEN assume_tac 1 THEN fast_tac ZF_cs 2);
   11.91 +by (fast_tac ZF_cs 1);
   11.92 +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
   11.93 +(*now use induction hyp*)
   11.94 +by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1);
   11.95 +by (dres_inst_tac [("t", "op `(f)")] subst_context 1);
   11.96 +by (asm_full_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
   11.97 +val not_well_ord_iso_pred_lemma = result();
   11.98 +
   11.99 +
  11.100 +(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
  11.101 +                     of a well-ordering*)
  11.102 +goal Order.thy
  11.103 +    "!!r. [| well_ord(A,r);  x:A |] ==> \
  11.104 +\         ALL f. f ~: ord_iso(A, r, pred(A,x,r), r)";
  11.105 +by (safe_tac ZF_cs);
  11.106 +by (metacut_tac not_well_ord_iso_pred_lemma 1);
  11.107 +by (REPEAT_SOME assume_tac);
  11.108 +(*Now we know f`x = x*)
  11.109 +by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type),
  11.110 +	     assume_tac]);
  11.111 +(*Now we know f`x : pred(A,x,r) *)
  11.112 +by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1);
  11.113 +by (fast_tac (ZF_cs addSEs [wf_on_not_refl RS notE]) 1);
  11.114 +val not_well_ord_iso_pred = result();
  11.115 +
  11.116 +
  11.117 +(*Inductive argument for proving Kunen's Lemma 6.2*)
  11.118 +goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def]
  11.119 +    "!!r. [| well_ord(A,r);  well_ord(B,s);  \
  11.120 +\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
  11.121 +\         ==> f`y = g`y";
  11.122 +by (safe_tac ZF_cs);
  11.123 +by (wf_on_ind_tac "y" [] 1);
  11.124 +by (subgoals_tac ["f: bij(A,B)", "g: bij(A,B)", "f`y1 : B", "g`y1 : B"] 1);
  11.125 +by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 2));
  11.126 +by (linear_case_tac 1);
  11.127 +(*The case  <f`y1, g`y1> : s  *)
  11.128 +by (forw_inst_tac [("f","g")] ord_iso_converse 1 THEN REPEAT (assume_tac 1));
  11.129 +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
  11.130 +by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1);
  11.131 +by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
  11.132 +by (dres_inst_tac [("t", "op `(g)")] subst_context 1);
  11.133 +by (asm_full_simp_tac bij_inverse_ss 1);
  11.134 +(*The case  <g`y1, f`y1> : s  *)
  11.135 +by (forw_inst_tac [("f","f")] ord_iso_converse 1 THEN REPEAT (assume_tac 1));
  11.136 +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
  11.137 +by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1);
  11.138 +by (dres_inst_tac [("t", "op `(converse(g))")] subst_context 1);
  11.139 +by (dres_inst_tac [("t", "op `(f)")] subst_context 1);
  11.140 +by (asm_full_simp_tac bij_inverse_ss 1);
  11.141 +val well_ord_iso_unique_lemma = result();
  11.142 +
  11.143 +
  11.144 +(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
  11.145 +goal Order.thy
  11.146 +    "!!r. [| well_ord(A,r);  well_ord(B,s);  \
  11.147 +\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
  11.148 +br fun_extension 1;
  11.149 +be (ord_iso_is_bij RS bij_is_fun) 1;
  11.150 +be (ord_iso_is_bij RS bij_is_fun) 1;
  11.151 +br well_ord_iso_unique_lemma 1;
  11.152 +by (REPEAT_SOME assume_tac);
  11.153 +val well_ord_iso_unique = result();
  11.154 +
  11.155 +
  11.156 +goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, 
  11.157 +		 trans_on_def, well_ord_def]
  11.158 +    "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)";
  11.159 +by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1);
  11.160 +by (safe_tac ZF_cs);
  11.161 +by (linear_case_tac 1);
  11.162 +(*case x=xb*)
  11.163 +by (fast_tac (ZF_cs addSEs [wf_on_anti_sym]) 1);
  11.164 +(*case x<xb*)
  11.165 +by (fast_tac (ZF_cs addSEs [wf_on_chain3]) 1);
  11.166 +val well_ordI = result();
  11.167 +
  11.168 +goalw Order.thy [well_ord_def]
  11.169 +    "!!r. well_ord(A,r) ==> wf[A](r)";
  11.170 +by (safe_tac ZF_cs);
  11.171 +val well_ord_is_wf = result();
  11.172 +
  11.173 +
  11.174 +(*** Derived rules for pred(A,x,r) ***)
  11.175 +
  11.176 +val [major,minor] = goalw Order.thy [pred_def]
  11.177 +    "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
  11.178 +br (major RS CollectE) 1;
  11.179 +by (REPEAT (ares_tac [minor] 1));
  11.180 +val predE = result();
  11.181 +
  11.182 +goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}";
  11.183 +by (fast_tac ZF_cs 1);
  11.184 +val pred_subset_under = result();
  11.185 +
  11.186 +goalw Order.thy [pred_def] "pred(A,x,r) <= A";
  11.187 +by (fast_tac ZF_cs 1);
  11.188 +val pred_subset = result();
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/ZF/Order.thy	Tue Jun 21 17:20:34 1994 +0200
    12.3 @@ -0,0 +1,31 @@
    12.4 +(*  Title: 	ZF/Order.thy
    12.5 +    ID:         $Id$
    12.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 +    Copyright   1994  University of Cambridge
    12.8 +
    12.9 +Orders in Zermelo-Fraenkel Set Theory 
   12.10 +*)
   12.11 +
   12.12 +Order = WF + Perm + 
   12.13 +consts
   12.14 +  part_ord        :: "[i,i]=>o"		(*Strict partial ordering*)
   12.15 +  linear, tot_ord :: "[i,i]=>o"		(*Strict total ordering*)
   12.16 +  well_ord        :: "[i,i]=>o"		(*Well-ordering*)
   12.17 +  ord_iso         :: "[i,i,i,i]=>i"	(*Order isomorphisms*)
   12.18 +  pred            :: "[i,i,i]=>i"	(*Set of predecessors*)
   12.19 +
   12.20 +rules
   12.21 +  part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
   12.22 +
   12.23 +  linear_def   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
   12.24 +
   12.25 +  tot_ord_def  "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
   12.26 +
   12.27 +  well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
   12.28 +
   12.29 +  ord_iso_def  "ord_iso(A,r,B,s) == \
   12.30 +\                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
   12.31 +
   12.32 +  pred_def     "pred(A,x,r) == {y:A. <y,x>:r}"
   12.33 +
   12.34 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/ZF/OrderType.ML	Tue Jun 21 17:20:34 1994 +0200
    13.3 @@ -0,0 +1,132 @@
    13.4 +(*  Title: 	ZF/OrderType.ML
    13.5 +    ID:         $Id$
    13.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   1994  University of Cambridge
    13.8 +
    13.9 +For OrderType.thy.  Order types in Zermelo-Fraenkel Set Theory 
   13.10 +*)
   13.11 +
   13.12 +
   13.13 +(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
   13.14 +goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
   13.15 +br well_ordI 1;
   13.16 +br (wf_Memrel RS wf_imp_wf_on) 1;
   13.17 +by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
   13.18 +by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
   13.19 +by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
   13.20 +val well_ord_Memrel = result();
   13.21 +
   13.22 +open OrderType;
   13.23 +
   13.24 +(** Unfolding of ordermap **)
   13.25 +
   13.26 +goalw OrderType.thy [ordermap_def, pred_def]
   13.27 +    "!!r. [| wf[A](r);  x:A |] ==> \
   13.28 +\         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
   13.29 +by (asm_simp_tac ZF_ss 1);
   13.30 +be (wfrec_on RS trans) 1;
   13.31 +ba 1;
   13.32 +by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
   13.33 +                                  vimage_singleton_iff]) 1);
   13.34 +val ordermap_pred_unfold = result();
   13.35 +
   13.36 +(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
   13.37 +val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
   13.38 +
   13.39 +goalw OrderType.thy [ordermap_def,ordertype_def]
   13.40 +    "ordermap(A,r) : A -> ordertype(A,r)";
   13.41 +br lam_type 1;
   13.42 +by (rtac (lamI RS imageI) 1);
   13.43 +by (REPEAT (assume_tac 1));
   13.44 +val ordermap_type = result();
   13.45 +
   13.46 +(** Showing that ordermap, ordertype yield ordinals **)
   13.47 +
   13.48 +fun ordermap_elim_tac i =
   13.49 +    EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
   13.50 +	   assume_tac (i+1),
   13.51 +	   assume_tac i];
   13.52 +
   13.53 +goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
   13.54 +    "!!r. [| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)";
   13.55 +by (safe_tac ZF_cs);
   13.56 +by (wf_on_ind_tac "x" [] 1);
   13.57 +by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
   13.58 +by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   13.59 +bws [pred_def,Transset_def];
   13.60 +by (fast_tac ZF_cs 2);
   13.61 +by (safe_tac ZF_cs);
   13.62 +by (ordermap_elim_tac 1);
   13.63 +by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
   13.64 +val Ord_ordermap = result();
   13.65 +
   13.66 +goalw OrderType.thy [ordertype_def]
   13.67 +    "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
   13.68 +by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
   13.69 +by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   13.70 +by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
   13.71 +bws [Transset_def,well_ord_def];
   13.72 +by (safe_tac ZF_cs);
   13.73 +by (ordermap_elim_tac 1);
   13.74 +by (fast_tac ZF_cs 1);
   13.75 +val Ord_ordertype = result();
   13.76 +
   13.77 +(** ordermap preserves the orderings in both directions **)
   13.78 +
   13.79 +goal OrderType.thy
   13.80 +    "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>	\
   13.81 +\         ordermap(A,r)`w : ordermap(A,r)`x";
   13.82 +by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
   13.83 +ba 1;
   13.84 +by (fast_tac ZF_cs 1);
   13.85 +val less_imp_ordermap_in = result();
   13.86 +
   13.87 +(*linearity of r is crucial here*)
   13.88 +goalw OrderType.thy [well_ord_def, tot_ord_def]
   13.89 +    "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r);  \
   13.90 +\            w: A; x: A |] ==> <w,x>: r";
   13.91 +by (safe_tac ZF_cs);
   13.92 +by (linear_case_tac 1);
   13.93 +by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
   13.94 +bd less_imp_ordermap_in 1;
   13.95 +by (REPEAT_SOME assume_tac);
   13.96 +be mem_anti_sym 1;
   13.97 +ba 1;
   13.98 +val ordermap_in_imp_less = result();
   13.99 +
  13.100 +val ordermap_surj = 
  13.101 +    (ordermap_type RS surj_image) |>
  13.102 +    rewrite_rule [symmetric ordertype_def] |> 
  13.103 +    standard;
  13.104 +
  13.105 +goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
  13.106 +    "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
  13.107 +by (safe_tac ZF_cs);
  13.108 +br ordermap_type 1;
  13.109 +br ordermap_surj 2;
  13.110 +by (linear_case_tac 1);
  13.111 +(*The two cases yield similar contradictions*)
  13.112 +by (ALLGOALS (dtac less_imp_ordermap_in));
  13.113 +by (REPEAT_SOME assume_tac);
  13.114 +by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
  13.115 +val ordertype_bij = result();
  13.116 +
  13.117 +goalw OrderType.thy [ord_iso_def]
  13.118 + "!!r. well_ord(A,r) ==> \
  13.119 +\      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
  13.120 +by (safe_tac ZF_cs);
  13.121 +br ordertype_bij 1;
  13.122 +ba 1;
  13.123 +by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
  13.124 +bw well_ord_def;
  13.125 +by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
  13.126 +			    ordermap_type RS apply_type]) 1);
  13.127 +val ordertype_ord_iso = result();
  13.128 +
  13.129 +
  13.130 +(** Unfolding of ordertype **)
  13.131 +
  13.132 +goalw OrderType.thy [ordertype_def]
  13.133 +    "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
  13.134 +by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
  13.135 +val ordertype_unfold = result();
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/ZF/OrderType.thy	Tue Jun 21 17:20:34 1994 +0200
    14.3 @@ -0,0 +1,22 @@
    14.4 +(*  Title: 	ZF/OrderType.thy
    14.5 +    ID:         $Id$
    14.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 +    Copyright   1994  University of Cambridge
    14.8 +
    14.9 +Order types.  
   14.10 +
   14.11 +The order type of a well-ordering is the least ordinal isomorphic to it.
   14.12 +*)
   14.13 +
   14.14 +OrderType = Order + Ordinal + 
   14.15 +consts
   14.16 +  ordermap  :: "[i,i]=>i"
   14.17 +  ordertype :: "[i,i]=>i"
   14.18 +
   14.19 +rules
   14.20 +  ordermap_def
   14.21 +      "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
   14.22 +
   14.23 +  ordertype_def "ordertype(A,r) == ordermap(A,r)``A"
   14.24 +
   14.25 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/ZF/Ordinal.ML	Tue Jun 21 17:20:34 1994 +0200
    15.3 @@ -0,0 +1,619 @@
    15.4 +(*  Title: 	ZF/Ordinal.thy
    15.5 +    ID:         $Id$
    15.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7 +    Copyright   1993  University of Cambridge
    15.8 +
    15.9 +For Ordinal.thy.  Ordinals in Zermelo-Fraenkel Set Theory 
   15.10 +*)
   15.11 +
   15.12 +open Ordinal;
   15.13 +
   15.14 +(*** Rules for Transset ***)
   15.15 +
   15.16 +(** Two neat characterisations of Transset **)
   15.17 +
   15.18 +goalw Ordinal.thy [Transset_def] "Transset(A) <-> A<=Pow(A)";
   15.19 +by (fast_tac ZF_cs 1);
   15.20 +val Transset_iff_Pow = result();
   15.21 +
   15.22 +goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
   15.23 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
   15.24 +val Transset_iff_Union_succ = result();
   15.25 +
   15.26 +(** Consequences of downwards closure **)
   15.27 +
   15.28 +goalw Ordinal.thy [Transset_def]
   15.29 +    "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C";
   15.30 +by (fast_tac ZF_cs 1);
   15.31 +val Transset_doubleton_D = result();
   15.32 +
   15.33 +val [prem1,prem2] = goalw Ordinal.thy [Pair_def]
   15.34 +    "[| Transset(C); <a,b>: C |] ==> a:C & b: C";
   15.35 +by (cut_facts_tac [prem2] 1);	
   15.36 +by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1);
   15.37 +val Transset_Pair_D = result();
   15.38 +
   15.39 +val prem1::prems = goal Ordinal.thy
   15.40 +    "[| Transset(C); A*B <= C; b: B |] ==> A <= C";
   15.41 +by (cut_facts_tac prems 1);
   15.42 +by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
   15.43 +val Transset_includes_domain = result();
   15.44 +
   15.45 +val prem1::prems = goal Ordinal.thy
   15.46 +    "[| Transset(C); A*B <= C; a: A |] ==> B <= C";
   15.47 +by (cut_facts_tac prems 1);
   15.48 +by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
   15.49 +val Transset_includes_range = result();
   15.50 +
   15.51 +val [prem1,prem2] = goalw (merge_theories(Ordinal.thy,Sum.thy)) [sum_def]
   15.52 +    "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
   15.53 +by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
   15.54 +by (REPEAT (etac (prem1 RS Transset_includes_range) 1
   15.55 +     ORELSE resolve_tac [conjI, singletonI] 1));
   15.56 +val Transset_includes_summands = result();
   15.57 +
   15.58 +val [prem] = goalw (merge_theories(Ordinal.thy,Sum.thy)) [sum_def]
   15.59 +    "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
   15.60 +by (rtac (Int_Un_distrib RS ssubst) 1);
   15.61 +by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
   15.62 +val Transset_sum_Int_subset = result();
   15.63 +
   15.64 +(** Closure properties **)
   15.65 +
   15.66 +goalw Ordinal.thy [Transset_def] "Transset(0)";
   15.67 +by (fast_tac ZF_cs 1);
   15.68 +val Transset_0 = result();
   15.69 +
   15.70 +goalw Ordinal.thy [Transset_def]
   15.71 +    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Un j)";
   15.72 +by (fast_tac ZF_cs 1);
   15.73 +val Transset_Un = result();
   15.74 +
   15.75 +goalw Ordinal.thy [Transset_def]
   15.76 +    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Int j)";
   15.77 +by (fast_tac ZF_cs 1);
   15.78 +val Transset_Int = result();
   15.79 +
   15.80 +goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))";
   15.81 +by (fast_tac ZF_cs 1);
   15.82 +val Transset_succ = result();
   15.83 +
   15.84 +goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))";
   15.85 +by (fast_tac ZF_cs 1);
   15.86 +val Transset_Pow = result();
   15.87 +
   15.88 +goalw Ordinal.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))";
   15.89 +by (fast_tac ZF_cs 1);
   15.90 +val Transset_Union = result();
   15.91 +
   15.92 +val [Transprem] = goalw Ordinal.thy [Transset_def]
   15.93 +    "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
   15.94 +by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
   15.95 +val Transset_Union_family = result();
   15.96 +
   15.97 +val [prem,Transprem] = goalw Ordinal.thy [Transset_def]
   15.98 +    "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
   15.99 +by (cut_facts_tac [prem] 1);
  15.100 +by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
  15.101 +val Transset_Inter_family = result();
  15.102 +
  15.103 +(*** Natural Deduction rules for Ord ***)
  15.104 +
  15.105 +val prems = goalw Ordinal.thy [Ord_def]
  15.106 +    "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i) ";
  15.107 +by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
  15.108 +val OrdI = result();
  15.109 +
  15.110 +val [major] = goalw Ordinal.thy [Ord_def]
  15.111 +    "Ord(i) ==> Transset(i)";
  15.112 +by (rtac (major RS conjunct1) 1);
  15.113 +val Ord_is_Transset = result();
  15.114 +
  15.115 +val [major,minor] = goalw Ordinal.thy [Ord_def]
  15.116 +    "[| Ord(i);  j:i |] ==> Transset(j) ";
  15.117 +by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
  15.118 +val Ord_contains_Transset = result();
  15.119 +
  15.120 +(*** Lemmas for ordinals ***)
  15.121 +
  15.122 +goalw Ordinal.thy [Ord_def,Transset_def] "!!i j.[| Ord(i);  j:i |] ==> Ord(j)";
  15.123 +by (fast_tac ZF_cs 1);
  15.124 +val Ord_in_Ord = result();
  15.125 +
  15.126 +(* Ord(succ(j)) ==> Ord(j) *)
  15.127 +val Ord_succD = succI1 RSN (2, Ord_in_Ord);
  15.128 +
  15.129 +goal Ordinal.thy "!!i j. [| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)";
  15.130 +by (REPEAT (ares_tac [OrdI] 1
  15.131 +     ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
  15.132 +val Ord_subset_Ord = result();
  15.133 +
  15.134 +goalw Ordinal.thy [Ord_def,Transset_def] "!!i j. [| j:i;  Ord(i) |] ==> j<=i";
  15.135 +by (fast_tac ZF_cs 1);
  15.136 +val OrdmemD = result();
  15.137 +
  15.138 +goal Ordinal.thy "!!i j k. [| i:j;  j:k;  Ord(k) |] ==> i:k";
  15.139 +by (REPEAT (ares_tac [OrdmemD RS subsetD] 1));
  15.140 +val Ord_trans = result();
  15.141 +
  15.142 +goal Ordinal.thy "!!i j. [| i:j;  Ord(j) |] ==> succ(i) <= j";
  15.143 +by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1));
  15.144 +val Ord_succ_subsetI = result();
  15.145 +
  15.146 +
  15.147 +(*** The construction of ordinals: 0, succ, Union ***)
  15.148 +
  15.149 +goal Ordinal.thy "Ord(0)";
  15.150 +by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1));
  15.151 +val Ord_0 = result();
  15.152 +
  15.153 +goal Ordinal.thy "!!i. Ord(i) ==> Ord(succ(i))";
  15.154 +by (REPEAT (ares_tac [OrdI,Transset_succ] 1
  15.155 +     ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset,
  15.156 +			  Ord_contains_Transset] 1));
  15.157 +val Ord_succ = result();
  15.158 +
  15.159 +goal Ordinal.thy "Ord(succ(i)) <-> Ord(i)";
  15.160 +by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
  15.161 +val Ord_succ_iff = result();
  15.162 +
  15.163 +goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
  15.164 +by (fast_tac (ZF_cs addSIs [Transset_Un]) 1);
  15.165 +val Ord_Un = result();
  15.166 +
  15.167 +goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
  15.168 +by (fast_tac (ZF_cs addSIs [Transset_Int]) 1);
  15.169 +val Ord_Int = result();
  15.170 +
  15.171 +val nonempty::prems = goal Ordinal.thy
  15.172 +    "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
  15.173 +by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
  15.174 +by (rtac Ord_is_Transset 1);
  15.175 +by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1
  15.176 +     ORELSE etac InterD 1));
  15.177 +val Ord_Inter = result();
  15.178 +
  15.179 +val jmemA::prems = goal Ordinal.thy
  15.180 +    "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))";
  15.181 +by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);
  15.182 +by (etac RepFunE 1);
  15.183 +by (etac ssubst 1);
  15.184 +by (eresolve_tac prems 1);
  15.185 +val Ord_INT = result();
  15.186 +
  15.187 +(*There is no set of all ordinals, for then it would contain itself*)
  15.188 +goal Ordinal.thy "~ (ALL i. i:X <-> Ord(i))";
  15.189 +by (rtac notI 1);
  15.190 +by (forw_inst_tac [("x", "X")] spec 1);
  15.191 +by (safe_tac (ZF_cs addSEs [mem_anti_refl]));
  15.192 +by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1);
  15.193 +by (fast_tac ZF_cs 2);
  15.194 +bw Transset_def;
  15.195 +by (safe_tac ZF_cs);
  15.196 +by (asm_full_simp_tac ZF_ss 1);
  15.197 +by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
  15.198 +val ON_class = result();
  15.199 +
  15.200 +(*** < is 'less than' for ordinals ***)
  15.201 +
  15.202 +goalw Ordinal.thy [lt_def] "!!i j. [| i:j;  Ord(j) |] ==> i<j";
  15.203 +by (REPEAT (ares_tac [conjI] 1));
  15.204 +val ltI = result();
  15.205 +
  15.206 +val major::prems = goalw Ordinal.thy [lt_def]
  15.207 +    "[| i<j;  [| i:j;  Ord(i);  Ord(j) |] ==> P |] ==> P";
  15.208 +by (rtac (major RS conjE) 1);
  15.209 +by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1));
  15.210 +val ltE = result();
  15.211 +
  15.212 +goal Ordinal.thy "!!i j. i<j ==> i:j";
  15.213 +by (etac ltE 1);
  15.214 +by (assume_tac 1);
  15.215 +val ltD = result();
  15.216 +
  15.217 +goalw Ordinal.thy [lt_def] "~ i<0";
  15.218 +by (fast_tac ZF_cs 1);
  15.219 +val not_lt0 = result();
  15.220 +
  15.221 +(* i<0 ==> R *)
  15.222 +val lt0E = standard (not_lt0 RS notE);
  15.223 +
  15.224 +goal Ordinal.thy "!!i j k. [| i<j;  j<k |] ==> i<k";
  15.225 +by (fast_tac (ZF_cs addSIs [ltI] addSEs [ltE, Ord_trans]) 1);
  15.226 +val lt_trans = result();
  15.227 +
  15.228 +goalw Ordinal.thy [lt_def] "!!i j. [| i<j;  j<i |] ==> P";
  15.229 +by (REPEAT (eresolve_tac [asm_rl, conjE, mem_anti_sym] 1));
  15.230 +val lt_anti_sym = result();
  15.231 +
  15.232 +val lt_anti_refl = prove_goal Ordinal.thy "i<i ==> P"
  15.233 + (fn [major]=> [ (rtac (major RS (major RS lt_anti_sym)) 1) ]);
  15.234 +
  15.235 +val lt_not_refl = prove_goal Ordinal.thy "~ i<i"
  15.236 + (fn _=> [ (rtac notI 1), (etac lt_anti_refl 1) ]);
  15.237 +
  15.238 +(** le is less than or equals;  recall  i le j  abbrevs  i<succ(j) !! **)
  15.239 +
  15.240 +goalw Ordinal.thy [lt_def] "i le j <-> i<j | (i=j & Ord(j))";
  15.241 +by (fast_tac (ZF_cs addSIs [Ord_succ] addSDs [Ord_succD]) 1);
  15.242 +val le_iff = result();
  15.243 +
  15.244 +goal Ordinal.thy "!!i j. i<j ==> i le j";
  15.245 +by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1);
  15.246 +val leI = result();
  15.247 +
  15.248 +goal Ordinal.thy "!!i. [| i=j;  Ord(j) |] ==> i le j";
  15.249 +by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1);
  15.250 +val le_eqI = result();
  15.251 +
  15.252 +val le_refl = refl RS le_eqI;
  15.253 +
  15.254 +val [prem] = goal Ordinal.thy "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
  15.255 +by (rtac (disjCI RS (le_iff RS iffD2)) 1);
  15.256 +by (etac prem 1);
  15.257 +val leCI = result();
  15.258 +
  15.259 +val major::prems = goal Ordinal.thy
  15.260 +    "[| i le j;  i<j ==> P;  [| i=j;  Ord(j) |] ==> P |] ==> P";
  15.261 +by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1);
  15.262 +by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1));
  15.263 +val leE = result();
  15.264 +
  15.265 +goal Ordinal.thy "!!i j. [| i le j;  j le i |] ==> i=j";
  15.266 +by (asm_full_simp_tac (ZF_ss addsimps [le_iff]) 1);
  15.267 +by (fast_tac (ZF_cs addEs [lt_anti_sym]) 1);
  15.268 +val le_asym = result();
  15.269 +
  15.270 +goal Ordinal.thy "i le 0 <-> i=0";
  15.271 +by (fast_tac (ZF_cs addSIs [Ord_0 RS le_refl] addSEs [leE, lt0E]) 1);
  15.272 +val le0_iff = result();
  15.273 +
  15.274 +val le0D = standard (le0_iff RS iffD1);
  15.275 +
  15.276 +val lt_cs = 
  15.277 +    ZF_cs addSIs [le_refl, leCI]
  15.278 +          addSDs [le0D]
  15.279 +          addSEs [lt_anti_refl, lt0E, leE];
  15.280 +
  15.281 +
  15.282 +(*** Natural Deduction rules for Memrel ***)
  15.283 +
  15.284 +goalw Ordinal.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A";
  15.285 +by (fast_tac ZF_cs 1);
  15.286 +val Memrel_iff = result();
  15.287 +
  15.288 +val prems = goal Ordinal.thy "[| a: b;  a: A;  b: A |] ==> <a,b> : Memrel(A)";
  15.289 +by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1));
  15.290 +val MemrelI = result();
  15.291 +
  15.292 +val [major,minor] = goal Ordinal.thy
  15.293 +    "[| <a,b> : Memrel(A);  \
  15.294 +\       [| a: A;  b: A;  a:b |]  ==> P \
  15.295 +\    |]  ==> P";
  15.296 +by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1);
  15.297 +by (etac conjE 1);
  15.298 +by (rtac minor 1);
  15.299 +by (REPEAT (assume_tac 1));
  15.300 +val MemrelE = result();
  15.301 +
  15.302 +(*The membership relation (as a set) is well-founded.
  15.303 +  Proof idea: show A<=B by applying the foundation axiom to A-B *)
  15.304 +goalw Ordinal.thy [wf_def] "wf(Memrel(A))";
  15.305 +by (EVERY1 [rtac (foundation RS disjE RS allI),
  15.306 +	    etac disjI1,
  15.307 +	    etac bexE, 
  15.308 +	    rtac (impI RS allI RS bexI RS disjI2),
  15.309 +	    etac MemrelE,
  15.310 +	    etac bspec,
  15.311 +	    REPEAT o assume_tac]);
  15.312 +val wf_Memrel = result();
  15.313 +
  15.314 +(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
  15.315 +goalw Ordinal.thy [Ord_def, Transset_def, trans_def]
  15.316 +    "!!i. Ord(i) ==> trans(Memrel(i))";
  15.317 +by (fast_tac (ZF_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
  15.318 +val trans_Memrel = result();
  15.319 +
  15.320 +(*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
  15.321 +goalw Ordinal.thy [Transset_def]
  15.322 +    "!!A. Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A";
  15.323 +by (fast_tac (ZF_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
  15.324 +val Transset_Memrel_iff = result();
  15.325 +
  15.326 +
  15.327 +(*** Transfinite induction ***)
  15.328 +
  15.329 +(*Epsilon induction over a transitive set*)
  15.330 +val major::prems = goalw Ordinal.thy [Transset_def]
  15.331 +    "[| i: k;  Transset(k);                          \
  15.332 +\       !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) \
  15.333 +\    |]  ==>  P(i)";
  15.334 +by (rtac (major RS (wf_Memrel RS wf_induct2)) 1);
  15.335 +by (fast_tac (ZF_cs addEs [MemrelE]) 1);
  15.336 +by (resolve_tac prems 1);
  15.337 +by (assume_tac 1);
  15.338 +by (cut_facts_tac prems 1);
  15.339 +by (fast_tac (ZF_cs addIs [MemrelI]) 1);
  15.340 +val Transset_induct = result();
  15.341 +
  15.342 +(*Induction over an ordinal*)
  15.343 +val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
  15.344 +
  15.345 +(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
  15.346 +val [major,indhyp] = goal Ordinal.thy
  15.347 +    "[| Ord(i); \
  15.348 +\       !!x.[| Ord(x);  ALL y:x. P(y) |] ==> P(x) \
  15.349 +\    |]  ==>  P(i)";
  15.350 +by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1);
  15.351 +by (rtac indhyp 1);
  15.352 +by (rtac (major RS Ord_succ RS Ord_in_Ord) 1);
  15.353 +by (REPEAT (assume_tac 1));
  15.354 +val trans_induct = result();
  15.355 +
  15.356 +(*Perform induction on i, then prove the Ord(i) subgoal using prems. *)
  15.357 +fun trans_ind_tac a prems i = 
  15.358 +    EVERY [res_inst_tac [("i",a)] trans_induct i,
  15.359 +	   rename_last_tac a ["1"] (i+1),
  15.360 +	   ares_tac prems i];
  15.361 +
  15.362 +
  15.363 +(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
  15.364 +
  15.365 +(*Finds contradictions for the following proof*)
  15.366 +val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac];
  15.367 +
  15.368 +(** Proving that < is a linear ordering on the ordinals **)
  15.369 +
  15.370 +val prems = goal Ordinal.thy
  15.371 +    "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
  15.372 +by (trans_ind_tac "i" prems 1);
  15.373 +by (rtac (impI RS allI) 1);
  15.374 +by (trans_ind_tac "j" [] 1);
  15.375 +by (DEPTH_SOLVE (step_tac eq_cs 1 ORELSE Ord_trans_tac 1));
  15.376 +val Ord_linear_lemma = result();
  15.377 +val Ord_linear = standard (Ord_linear_lemma RS spec RS mp);
  15.378 +
  15.379 +(*The trichotomy law for ordinals!*)
  15.380 +val ordi::ordj::prems = goalw Ordinal.thy [lt_def]
  15.381 +    "[| Ord(i);  Ord(j);  i<j ==> P;  i=j ==> P;  j<i ==> P |] ==> P";
  15.382 +by (rtac ([ordi,ordj] MRS Ord_linear RS disjE) 1);
  15.383 +by (etac disjE 2);
  15.384 +by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1));
  15.385 +val Ord_linear_lt = result();
  15.386 +
  15.387 +val prems = goal Ordinal.thy
  15.388 +    "[| Ord(i);  Ord(j);  i<j ==> P;  j le i ==> P |]  ==> P";
  15.389 +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
  15.390 +by (DEPTH_SOLVE (ares_tac ([leI, sym RS le_eqI] @ prems) 1));
  15.391 +val Ord_linear2 = result();
  15.392 +
  15.393 +val prems = goal Ordinal.thy
  15.394 +    "[| Ord(i);  Ord(j);  i le j ==> P;  j le i ==> P |]  ==> P";
  15.395 +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
  15.396 +by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1));
  15.397 +val Ord_linear_le = result();
  15.398 +
  15.399 +goal Ordinal.thy "!!i j. j le i ==> ~ i<j";
  15.400 +by (fast_tac (lt_cs addEs [lt_anti_sym]) 1);
  15.401 +val le_imp_not_lt = result();
  15.402 +
  15.403 +goal Ordinal.thy "!!i j. [| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i";
  15.404 +by (res_inst_tac [("i","i"),("j","j")] Ord_linear2 1);
  15.405 +by (REPEAT (SOMEGOAL assume_tac));
  15.406 +by (fast_tac (lt_cs addEs [lt_anti_sym]) 1);
  15.407 +val not_lt_imp_le = result();
  15.408 +
  15.409 +goal Ordinal.thy "!!i j. [| Ord(i);  Ord(j) |] ==> ~ i<j <-> j le i";
  15.410 +by (REPEAT (ares_tac [iffI, le_imp_not_lt, not_lt_imp_le] 1));
  15.411 +val not_lt_iff_le = result();
  15.412 +
  15.413 +goal Ordinal.thy "!!i j. [| Ord(i);  Ord(j) |] ==> ~ i le j <-> j<i";
  15.414 +by (asm_simp_tac (ZF_ss addsimps [not_lt_iff_le RS iff_sym]) 1);
  15.415 +val not_le_iff_lt = result();
  15.416 +
  15.417 +goal Ordinal.thy "!!i. Ord(i) ==> 0 le i";
  15.418 +by (etac (not_lt_iff_le RS iffD1) 1);
  15.419 +by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));
  15.420 +val Ord_0_le = result();
  15.421 +
  15.422 +goal Ordinal.thy "!!i. [| Ord(i);  i~=0 |] ==> 0<i";
  15.423 +by (etac (not_le_iff_lt RS iffD1) 1);
  15.424 +by (rtac Ord_0 1);
  15.425 +by (fast_tac lt_cs 1);
  15.426 +val Ord_0_lt = result();
  15.427 +
  15.428 +(*** Results about less-than or equals ***)
  15.429 +
  15.430 +(** For ordinals, j<=i (subset) implies j le i (less-than or equals) **)
  15.431 +
  15.432 +goal Ordinal.thy "!!i j. [| j<=i;  Ord(i);  Ord(j) |] ==> j le i";
  15.433 +by (rtac (not_lt_iff_le RS iffD1) 1);
  15.434 +by (assume_tac 1);
  15.435 +by (assume_tac 1);
  15.436 +by (fast_tac (ZF_cs addEs [ltE, mem_anti_refl]) 1);
  15.437 +val subset_imp_le = result();
  15.438 +
  15.439 +goal Ordinal.thy "!!i j. i le j ==> i<=j";
  15.440 +by (etac leE 1);
  15.441 +by (fast_tac ZF_cs 2);
  15.442 +by (fast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1);
  15.443 +val le_imp_subset = result();
  15.444 +
  15.445 +goal Ordinal.thy "j le i <-> j<=i & Ord(i) & Ord(j)";
  15.446 +by (fast_tac (ZF_cs addSEs [subset_imp_le, le_imp_subset]
  15.447 +	            addEs [ltE, make_elim Ord_succD]) 1);
  15.448 +val le_subset_iff = result();
  15.449 +
  15.450 +goal Ordinal.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
  15.451 +by (simp_tac (ZF_ss addsimps [le_iff]) 1);
  15.452 +by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
  15.453 +val le_succ_iff = result();
  15.454 +
  15.455 +(*Just a variant of subset_imp_le*)
  15.456 +val [ordi,ordj,minor] = goal Ordinal.thy
  15.457 +    "[| Ord(i);  Ord(j);  !!x. x<j ==> x<i |] ==> j le i";
  15.458 +by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj]));
  15.459 +be (minor RS lt_anti_refl) 1;
  15.460 +val all_lt_imp_le = result();
  15.461 +
  15.462 +(** Transitive laws **)
  15.463 +
  15.464 +goal Ordinal.thy "!!i j. [| i le j;  j<k |] ==> i<k";
  15.465 +by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1);
  15.466 +val lt_trans1 = result();
  15.467 +
  15.468 +goal Ordinal.thy "!!i j. [| i<j;  j le k |] ==> i<k";
  15.469 +by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1);
  15.470 +val lt_trans2 = result();
  15.471 +
  15.472 +goal Ordinal.thy "!!i j. [| i le j;  j le k |] ==> i le k";
  15.473 +by (REPEAT (ares_tac [lt_trans1] 1));
  15.474 +val le_trans = result();
  15.475 +
  15.476 +goal Ordinal.thy "!!i j. i<j ==> succ(i) le j";
  15.477 +by (rtac (not_lt_iff_le RS iffD1) 1);
  15.478 +by (fast_tac (lt_cs addEs [lt_anti_sym]) 3);
  15.479 +by (ALLGOALS (fast_tac (ZF_cs addEs [ltE] addIs [Ord_succ])));
  15.480 +val succ_leI = result();
  15.481 +
  15.482 +goal Ordinal.thy "!!i j. succ(i) le j ==> i<j";
  15.483 +by (rtac (not_le_iff_lt RS iffD1) 1);
  15.484 +by (fast_tac (lt_cs addEs [lt_anti_sym]) 3);
  15.485 +by (ALLGOALS (fast_tac (ZF_cs addEs [ltE, make_elim Ord_succD])));
  15.486 +val succ_leE = result();
  15.487 +
  15.488 +goal Ordinal.thy "succ(i) le j <-> i<j";
  15.489 +by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1));
  15.490 +val succ_le_iff = result();
  15.491 +
  15.492 +(** Union and Intersection **)
  15.493 +
  15.494 +goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i Un j";
  15.495 +by (rtac (Un_upper1 RS subset_imp_le) 1);
  15.496 +by (REPEAT (ares_tac [Ord_Un] 1));
  15.497 +val Un_upper1_le = result();
  15.498 +
  15.499 +goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> j le i Un j";
  15.500 +by (rtac (Un_upper2 RS subset_imp_le) 1);
  15.501 +by (REPEAT (ares_tac [Ord_Un] 1));
  15.502 +val Un_upper2_le = result();
  15.503 +
  15.504 +(*Replacing k by succ(k') yields the similar rule for le!*)
  15.505 +goal Ordinal.thy "!!i j k. [| i<k;  j<k |] ==> i Un j < k";
  15.506 +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
  15.507 +by (rtac (Un_commute RS ssubst) 4);
  15.508 +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4);
  15.509 +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 3);
  15.510 +by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
  15.511 +val Un_least_lt = result();
  15.512 +
  15.513 +goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> i Un j < k  <->  i<k & j<k";
  15.514 +by (safe_tac (ZF_cs addSIs [Un_least_lt]));
  15.515 +br (Un_upper2_le RS lt_trans1) 2;
  15.516 +br (Un_upper1_le RS lt_trans1) 1;
  15.517 +by (REPEAT_SOME assume_tac);
  15.518 +val Un_least_lt_iff = result();
  15.519 +
  15.520 +val [ordi,ordj,ordk] = goal Ordinal.thy
  15.521 +    "[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k  <->  i:k & j:k";
  15.522 +by (cut_facts_tac [[ordi,ordj] MRS 
  15.523 +		   read_instantiate [("k","k")] Un_least_lt_iff] 1);
  15.524 +by (asm_full_simp_tac (ZF_ss addsimps [lt_def,ordi,ordj,ordk]) 1);
  15.525 +val Un_least_mem_iff = result();
  15.526 +
  15.527 +(*Replacing k by succ(k') yields the similar rule for le!*)
  15.528 +goal Ordinal.thy "!!i j k. [| i<k;  j<k |] ==> i Int j < k";
  15.529 +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
  15.530 +by (rtac (Int_commute RS ssubst) 4);
  15.531 +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 4);
  15.532 +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 3);
  15.533 +by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
  15.534 +val Int_greatest_lt = result();
  15.535 +
  15.536 +(*FIXME: the Intersection duals are missing!*)
  15.537 +
  15.538 +
  15.539 +(*** Results about limits ***)
  15.540 +
  15.541 +val prems = goal Ordinal.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
  15.542 +by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);
  15.543 +by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));
  15.544 +val Ord_Union = result();
  15.545 +
  15.546 +val prems = goal Ordinal.thy
  15.547 +    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))";
  15.548 +by (rtac Ord_Union 1);
  15.549 +by (etac RepFunE 1);
  15.550 +by (etac ssubst 1);
  15.551 +by (eresolve_tac prems 1);
  15.552 +val Ord_UN = result();
  15.553 +
  15.554 +(* No < version; consider (UN i:nat.i)=nat *)
  15.555 +val [ordi,limit] = goal Ordinal.thy
  15.556 +    "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i";
  15.557 +by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1);
  15.558 +by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1));
  15.559 +val UN_least_le = result();
  15.560 +
  15.561 +val [jlti,limit] = goal Ordinal.thy
  15.562 +    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i";
  15.563 +by (rtac (jlti RS ltE) 1);
  15.564 +by (rtac (UN_least_le RS lt_trans2) 1);
  15.565 +by (REPEAT (ares_tac [jlti, succ_leI, limit] 1));
  15.566 +val UN_succ_least_lt = result();
  15.567 +
  15.568 +val prems = goal Ordinal.thy
  15.569 +    "[| a: A;  i le b(a);  !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))";
  15.570 +by (resolve_tac (prems RL [ltE]) 1);
  15.571 +by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1);
  15.572 +by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1));
  15.573 +val UN_upper_le = result();
  15.574 +
  15.575 +goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
  15.576 +by (fast_tac (eq_cs addEs [Ord_trans]) 1);
  15.577 +val Ord_equality = result();
  15.578 +
  15.579 +(*Holds for all transitive sets, not just ordinals*)
  15.580 +goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i";
  15.581 +by (fast_tac (ZF_cs addSEs [Ord_trans]) 1);
  15.582 +val Ord_Union_subset = result();
  15.583 +
  15.584 +
  15.585 +(*** Limit ordinals -- general properties ***)
  15.586 +
  15.587 +goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
  15.588 +by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
  15.589 +val Limit_Union_eq = result();
  15.590 +
  15.591 +goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
  15.592 +by (etac conjunct1 1);
  15.593 +val Limit_is_Ord = result();
  15.594 +
  15.595 +goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> 0 < i";
  15.596 +by (etac (conjunct2 RS conjunct1) 1);
  15.597 +val Limit_has_0 = result();
  15.598 +
  15.599 +goalw Ordinal.thy [Limit_def] "!!i. [| Limit(i);  j<i |] ==> succ(j) < i";
  15.600 +by (fast_tac ZF_cs 1);
  15.601 +val Limit_has_succ = result();
  15.602 +
  15.603 +goalw Ordinal.thy [Limit_def]
  15.604 +    "!!i. [| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
  15.605 +by (safe_tac subset_cs);
  15.606 +by (rtac (not_le_iff_lt RS iffD1) 2);
  15.607 +by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
  15.608 +by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
  15.609 +val non_succ_LimitI = result();
  15.610 +
  15.611 +goal Ordinal.thy "!!i. Limit(succ(i)) ==> P";
  15.612 +br lt_anti_refl 1;
  15.613 +br Limit_has_succ 1;
  15.614 +ba 1;
  15.615 +be (Limit_is_Ord RS Ord_succD RS le_refl) 1;
  15.616 +val succ_LimitE = result();
  15.617 +
  15.618 +goal Ordinal.thy "!!i. [| Limit(i);  i le succ(j) |] ==> i le j";
  15.619 +by (safe_tac (ZF_cs addSEs [succ_LimitE, leE]));
  15.620 +val Limit_le_succD = result();
  15.621 +
  15.622 +
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/ZF/Ordinal.thy	Tue Jun 21 17:20:34 1994 +0200
    16.3 @@ -0,0 +1,28 @@
    16.4 +(*  Title: 	ZF/Ordinal.thy
    16.5 +    ID:         $Id$
    16.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 +    Copyright   1994  University of Cambridge
    16.8 +
    16.9 +Ordinals in Zermelo-Fraenkel Set Theory 
   16.10 +*)
   16.11 +
   16.12 +Ordinal = WF + "simpdata" + "equalities" +
   16.13 +consts
   16.14 +  Memrel      	:: "i=>i"
   16.15 +  Transset,Ord  :: "i=>o"
   16.16 +  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
   16.17 +  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
   16.18 +  Limit         :: "i=>o"
   16.19 +
   16.20 +translations
   16.21 +  "x le y"      == "x < succ(y)"
   16.22 +
   16.23 +rules
   16.24 +  Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   16.25 +  Transset_def	"Transset(i) == ALL x:i. x<=i"
   16.26 +  Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
   16.27 +  lt_def        "i<j         == i:j & Ord(j)"
   16.28 +  Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
   16.29 +
   16.30 +
   16.31 +end
    17.1 --- a/src/ZF/Perm.ML	Tue Jun 21 16:26:34 1994 +0200
    17.2 +++ b/src/ZF/Perm.ML	Tue Jun 21 17:20:34 1994 +0200
    17.3 @@ -75,10 +75,13 @@
    17.4  by (rtac (prem RS lam_mono) 1);
    17.5  val id_mono = result();
    17.6  
    17.7 -goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
    17.8 +goalw Perm.thy [inj_def,id_def] "!!A B. A<=B ==> id(A): inj(A,B)";
    17.9  by (REPEAT (ares_tac [CollectI,lam_type] 1));
   17.10 +by (etac subsetD 1 THEN assume_tac 1);
   17.11  by (simp_tac ZF_ss 1);
   17.12 -val id_inj = result();
   17.13 +val id_subset_inj = result();
   17.14 +
   17.15 +val id_inj = subset_refl RS id_subset_inj;
   17.16  
   17.17  goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
   17.18  by (fast_tac (ZF_cs addIs [lam_type,beta]) 1);
   17.19 @@ -111,24 +114,32 @@
   17.20  by (fast_tac (ZF_cs addIs (prems@[apply_Pair,apply_equality,converseI])) 1);
   17.21  val left_inverse_lemma = result();
   17.22  
   17.23 -val prems = goal Perm.thy
   17.24 -    "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
   17.25 -by (fast_tac (ZF_cs addIs (prems@
   17.26 -       [left_inverse_lemma,inj_converse_fun,inj_is_fun])) 1);
   17.27 +goal Perm.thy
   17.28 +    "!!f. [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
   17.29 +by (fast_tac (ZF_cs addIs [left_inverse_lemma,inj_converse_fun,inj_is_fun]) 1);
   17.30  val left_inverse = result();
   17.31  
   17.32 +val left_inverse_bij = bij_is_inj RS left_inverse;
   17.33 +
   17.34  val prems = goal Perm.thy
   17.35      "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b";
   17.36  by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
   17.37  by (REPEAT (resolve_tac prems 1));
   17.38  val right_inverse_lemma = result();
   17.39  
   17.40 -val prems = goal Perm.thy
   17.41 -    "[| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b";
   17.42 +goal Perm.thy
   17.43 +    "!!f. [| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b";
   17.44  by (rtac right_inverse_lemma 1);
   17.45 -by (REPEAT (resolve_tac (prems@ [inj_converse_fun,inj_is_fun]) 1));
   17.46 +by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
   17.47  val right_inverse = result();
   17.48  
   17.49 +goalw Perm.thy [bij_def]
   17.50 +    "!!f. [| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b";
   17.51 +by (EVERY1 [etac IntE, etac right_inverse, 
   17.52 +	    etac (surj_range RS ssubst),
   17.53 +	    assume_tac]);
   17.54 +val right_inverse_bij = result();
   17.55 +
   17.56  val prems = goal Perm.thy
   17.57      "f: inj(A,B) ==> converse(f): inj(range(f), A)";
   17.58  bw inj_def;  (*rewrite subgoal but not prems!!*)
   17.59 @@ -236,22 +247,22 @@
   17.60  by (REPEAT (ares_tac [PiI,comp_rel,ex1I,compI] 1
   17.61       ORELSE eresolve_tac [fun_is_rel,apply_Pair,apply_type] 1));
   17.62  by (fast_tac (comp_cs addDs [apply_equality]) 1);
   17.63 -val comp_func = result();
   17.64 +val comp_fun = result();
   17.65  
   17.66  goal Perm.thy "!!f g. [| g: A->B;  f: B->C;  a:A |] ==> (f O g)`a = f`(g`a)";
   17.67 -by (REPEAT (ares_tac [comp_func,apply_equality,compI,
   17.68 +by (REPEAT (ares_tac [comp_fun,apply_equality,compI,
   17.69  		      apply_Pair,apply_type] 1));
   17.70 -val comp_func_apply = result();
   17.71 +val comp_fun_apply = result();
   17.72  
   17.73  goalw Perm.thy [inj_def]
   17.74      "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
   17.75  by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1
   17.76 -     ORELSE step_tac (ZF_cs addSIs [comp_func,apply_type,comp_func_apply]) 1));
   17.77 +     ORELSE step_tac (ZF_cs addSIs [comp_fun,apply_type,comp_fun_apply]) 1));
   17.78  val comp_inj = result();
   17.79  
   17.80  goalw Perm.thy [surj_def]
   17.81      "!!f g. [| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
   17.82 -by (best_tac (ZF_cs addSIs [comp_func,comp_func_apply]) 1);
   17.83 +by (best_tac (ZF_cs addSIs [comp_fun,comp_fun_apply]) 1);
   17.84  val comp_surj = result();
   17.85  
   17.86  goalw Perm.thy [bij_def]
   17.87 @@ -268,7 +279,7 @@
   17.88      "!!f g. [| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
   17.89  by (safe_tac comp_cs);
   17.90  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   17.91 -by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
   17.92 +by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1);
   17.93  val comp_mem_injD1 = result();
   17.94  
   17.95  goalw Perm.thy [inj_def,surj_def]
   17.96 @@ -280,24 +291,24 @@
   17.97  by (safe_tac comp_cs);
   17.98  by (res_inst_tac [("t", "op `(g)")] subst_context 1);
   17.99  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
  17.100 -by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
  17.101 +by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1);
  17.102  val comp_mem_injD2 = result();
  17.103  
  17.104  goalw Perm.thy [surj_def]
  17.105      "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)";
  17.106 -by (fast_tac (comp_cs addSIs [comp_func_apply RS sym, apply_type]) 1);
  17.107 +by (fast_tac (comp_cs addSIs [comp_fun_apply RS sym, apply_type]) 1);
  17.108  val comp_mem_surjD1 = result();
  17.109  
  17.110  goal Perm.thy
  17.111      "!!f g. [| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
  17.112 -by (REPEAT (ares_tac [comp_func_apply RS sym RS trans] 1));
  17.113 -val comp_func_applyD = result();
  17.114 +by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
  17.115 +val comp_fun_applyD = result();
  17.116  
  17.117  goalw Perm.thy [inj_def,surj_def]
  17.118      "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)";
  17.119  by (safe_tac comp_cs);
  17.120  by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
  17.121 -by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_func_applyD 1));
  17.122 +by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
  17.123  by (best_tac (comp_cs addSIs [apply_type]) 1);
  17.124  val comp_mem_surjD2 = result();
  17.125  
  17.126 @@ -325,6 +336,49 @@
  17.127  by (best_tac (comp_cs addIs [apply_Pair]) 1);
  17.128  val right_comp_inverse = result();
  17.129  
  17.130 +(** Proving that a function is a bijection **)
  17.131 +
  17.132 +val prems = 
  17.133 +goalw Perm.thy [bij_def, inj_def, surj_def]
  17.134 +    "[| !!x. x:A ==> c(x): B;		\
  17.135 +\       !!y. y:B ==> d(y): A;  		\
  17.136 +\       !!x. x:A ==> d(c(x)) = x;      	\
  17.137 +\       !!y. y:B ==> c(d(y)) = y	\
  17.138 +\    |] ==> (lam x:A.c(x)) : bij(A,B)";
  17.139 +by (simp_tac (ZF_ss addsimps ([lam_type]@prems)) 1);
  17.140 +by (safe_tac ZF_cs);
  17.141 +(*Apply d to both sides then simplify (type constraint is essential) *)
  17.142 +by (dres_inst_tac [("t", "d::i=>i")] subst_context 1);
  17.143 +by (asm_full_simp_tac (ZF_ss addsimps prems) 1);
  17.144 +by (fast_tac (ZF_cs addIs prems) 1);
  17.145 +val lam_bijective = result();
  17.146 +
  17.147 +goalw Perm.thy [id_def]
  17.148 +    "!!f A B. [| f: A->B;  g: B->A |] ==> \
  17.149 +\             f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
  17.150 +by (safe_tac ZF_cs);
  17.151 +by (dres_inst_tac [("t", "%h.h`y ")] subst_context 1);
  17.152 +by (asm_full_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
  17.153 +br fun_extension 1;
  17.154 +by (REPEAT (ares_tac [comp_fun, lam_type] 1));
  17.155 +by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
  17.156 +val comp_eq_id_iff = result();
  17.157 +
  17.158 +goalw Perm.thy [bij_def, inj_def, surj_def]
  17.159 +    "!!f A B. [| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) \
  17.160 +\             |] ==> f : bij(A,B)";
  17.161 +by (asm_full_simp_tac (ZF_ss addsimps [comp_eq_id_iff]) 1);
  17.162 +by (safe_tac ZF_cs);
  17.163 +(*Apply g to both sides then simplify*)
  17.164 +by (dres_inst_tac [("t", "op `(g)"), ("a", "f`x")] subst_context 1);
  17.165 +by (asm_full_simp_tac ZF_ss 1);
  17.166 +by (fast_tac (ZF_cs addIs [apply_type]) 1);
  17.167 +val fg_imp_bijective = result();
  17.168 +
  17.169 +goal Perm.thy "!!f A. [| f: A->A;  f O f = id(A) |] ==> f : bij(A,A)";
  17.170 +by (REPEAT (ares_tac [fg_imp_bijective] 1));
  17.171 +val nilpotent_imp_bijective = result();
  17.172 +
  17.173  (*Injective case applies converse(f) to both sides then simplifies
  17.174      using left_inverse_lemma*)
  17.175  goalw Perm.thy [bij_def,inj_def,surj_def]
    18.1 --- a/src/ZF/QPair.thy	Tue Jun 21 16:26:34 1994 +0200
    18.2 +++ b/src/ZF/QPair.thy	Tue Jun 21 17:20:34 1994 +0200
    18.3 @@ -18,7 +18,7 @@
    18.4    qfsplit   :: "[[i,i] => o, i] => o"
    18.5    qconverse :: "i => i"
    18.6    "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
    18.7 -  " <*>"    :: "[i, i] => i"         		("(_ <*>/ _)" [81, 80] 80)
    18.8 +  "<*>"     :: "[i, i] => i"         		("(_ <*>/ _)" [81, 80] 80)
    18.9    QSigma    :: "[i, i => i] => i"
   18.10  
   18.11    "<+>"     :: "[i,i]=>i"      			(infixr 65)
    19.1 --- a/src/ZF/ROOT.ML	Tue Jun 21 16:26:34 1994 +0200
    19.2 +++ b/src/ZF/ROOT.ML	Tue Jun 21 17:20:34 1994 +0200
    19.3 @@ -28,6 +28,7 @@
    19.4  
    19.5  print_depth 1;
    19.6  
    19.7 +use_thy "CardinalArith";
    19.8  use_thy "Fin";
    19.9  use_thy "ListFn";
   19.10  
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/ZF/Rel.ML	Tue Jun 21 17:20:34 1994 +0200
    20.3 @@ -0,0 +1,60 @@
    20.4 +(*  Title: 	ZF/Rel.ML
    20.5 +    ID:         $Id$
    20.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    20.7 +    Copyright   1994  University of Cambridge
    20.8 +
    20.9 +For Rel.thy.  Relations in Zermelo-Fraenkel Set Theory 
   20.10 +*)
   20.11 +
   20.12 +open Rel;
   20.13 +
   20.14 +(*** Some properties of relations -- useful? ***)
   20.15 +
   20.16 +(* irreflexivity *)
   20.17 +
   20.18 +val prems = goalw Rel.thy [irrefl_def]
   20.19 +    "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
   20.20 +by (REPEAT (ares_tac (prems @ [ballI]) 1));
   20.21 +val irreflI = result();
   20.22 +
   20.23 +val prems = goalw Rel.thy [irrefl_def]
   20.24 +    "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r";
   20.25 +by (rtac (prems MRS bspec) 1);
   20.26 +val irreflE = result();
   20.27 +
   20.28 +(* symmetry *)
   20.29 +
   20.30 +val prems = goalw Rel.thy [sym_def]
   20.31 +     "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
   20.32 +by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
   20.33 +val symI = result();
   20.34 +
   20.35 +goalw Rel.thy [sym_def] "!!r. [| sym(r); <x,y>: r |]  ==>  <y,x>: r";
   20.36 +by (fast_tac ZF_cs 1);
   20.37 +val symE = result();
   20.38 +
   20.39 +(* antisymmetry *)
   20.40 +
   20.41 +val prems = goalw Rel.thy [antisym_def]
   20.42 +     "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> \
   20.43 +\     antisym(r)";
   20.44 +by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
   20.45 +val antisymI = result();
   20.46 +
   20.47 +val prems = goalw Rel.thy [antisym_def]
   20.48 +     "!!r. [| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y";
   20.49 +by (fast_tac ZF_cs 1);
   20.50 +val antisymE = result();
   20.51 +
   20.52 +(* transitivity *)
   20.53 +
   20.54 +goalw Rel.thy [trans_def]
   20.55 +    "!!r. [| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
   20.56 +by (fast_tac ZF_cs 1);
   20.57 +val transD = result();
   20.58 +
   20.59 +goalw Rel.thy [trans_on_def]
   20.60 +    "!!r. [| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r";
   20.61 +by (fast_tac ZF_cs 1);
   20.62 +val trans_onD = result();
   20.63 +
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/ZF/Rel.thy	Tue Jun 21 17:20:34 1994 +0200
    21.3 @@ -0,0 +1,33 @@
    21.4 +(*  Title: 	ZF/Rel.thy
    21.5 +    ID:         $Id$
    21.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    21.7 +    Copyright   1994  University of Cambridge
    21.8 +
    21.9 +Relations in Zermelo-Fraenkel Set Theory 
   21.10 +*)
   21.11 +
   21.12 +Rel = ZF +
   21.13 +consts
   21.14 +    refl,irrefl,equiv      :: "[i,i]=>o"
   21.15 +    sym,asym,antisym,trans :: "i=>o"
   21.16 +    trans_on               :: "[i,i]=>o"	("trans[_]'(_')")
   21.17 +
   21.18 +rules
   21.19 +  refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
   21.20 +
   21.21 +  irrefl_def   "irrefl(A,r) == ALL x: A. <x,x> ~: r"
   21.22 +
   21.23 +  sym_def      "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
   21.24 +
   21.25 +  asym_def     "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
   21.26 +
   21.27 +  antisym_def  "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
   21.28 +
   21.29 +  trans_def    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
   21.30 +
   21.31 +  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	\
   21.32 +\                          <x,y>: r --> <y,z>: r --> <x,z>: r"
   21.33 +
   21.34 +  equiv_def    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
   21.35 +
   21.36 +end
    22.1 --- a/src/ZF/Sum.ML	Tue Jun 21 16:26:34 1994 +0200
    22.2 +++ b/src/ZF/Sum.ML	Tue Jun 21 17:20:34 1994 +0200
    22.3 @@ -35,19 +35,19 @@
    22.4  (** Injection and freeness equivalences, for rewriting **)
    22.5  
    22.6  goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
    22.7 -by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
    22.8 +by (simp_tac ZF_ss 1);
    22.9  val Inl_iff = result();
   22.10  
   22.11  goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
   22.12 -by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
   22.13 +by (simp_tac ZF_ss 1);
   22.14  val Inr_iff = result();
   22.15  
   22.16  goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
   22.17 -by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1);
   22.18 +by (simp_tac (ZF_ss addsimps [one_not_0 RS not_sym]) 1);
   22.19  val Inl_Inr_iff = result();
   22.20  
   22.21  goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
   22.22 -by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1);
   22.23 +by (simp_tac (ZF_ss addsimps [one_not_0]) 1);
   22.24  val Inr_Inl_iff = result();
   22.25  
   22.26  (*Injection and freeness rules*)
   22.27 @@ -60,6 +60,9 @@
   22.28  val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
   22.29                     addSDs [Inl_inject,Inr_inject];
   22.30  
   22.31 +val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
   22.32 +			     Inl_Inr_iff, Inr_Inl_iff];
   22.33 +
   22.34  goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
   22.35  by (fast_tac sum_cs 1);
   22.36  val InlD = result();
   22.37 @@ -104,6 +107,19 @@
   22.38  			    (prems@[case_Inl,case_Inr]))));
   22.39  val case_type = result();
   22.40  
   22.41 +goal Sum.thy
   22.42 +  "!!u. u: A+B ==>   \
   22.43 +\       R(case(c,d,u)) <-> \
   22.44 +\       ((ALL x:A. u = Inl(x) --> R(c(x))) & \
   22.45 +\       (ALL y:B. u = Inr(y) --> R(d(y))))";
   22.46 +by (etac sumE 1);
   22.47 +by (asm_simp_tac (ZF_ss addsimps [case_Inl]) 1);
   22.48 +by (fast_tac sum_cs 1);
   22.49 +by (asm_simp_tac (ZF_ss addsimps [case_Inr]) 1);
   22.50 +by (fast_tac sum_cs 1);
   22.51 +val expand_case = result();
   22.52 +
   22.53 +
   22.54  (** Rules for the Part primitive **)
   22.55  
   22.56  goalw Sum.thy [Part_def]
    23.1 --- a/src/ZF/Trancl.ML	Tue Jun 21 16:26:34 1994 +0200
    23.2 +++ b/src/ZF/Trancl.ML	Tue Jun 21 17:20:34 1994 +0200
    23.3 @@ -8,12 +8,6 @@
    23.4  
    23.5  open Trancl;
    23.6  
    23.7 -val major::prems = goalw Trancl.thy [trans_def]
    23.8 -    "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
    23.9 -by (rtac (major RS spec RS spec RS spec RS mp RS mp) 1);
   23.10 -by (REPEAT (resolve_tac prems 1));
   23.11 -val transD = result();
   23.12 -
   23.13  goal Trancl.thy "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))";
   23.14  by (rtac bnd_monoI 1);
   23.15  by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2));
    24.1 --- a/src/ZF/Trancl.thy	Tue Jun 21 16:26:34 1994 +0200
    24.2 +++ b/src/ZF/Trancl.thy	Tue Jun 21 17:20:34 1994 +0200
    24.3 @@ -6,16 +6,12 @@
    24.4  Transitive closure of a relation
    24.5  *)
    24.6  
    24.7 -Trancl = Fixedpt + Perm + "mono" +
    24.8 +Trancl = Fixedpt + Perm + "mono" + Rel + 
    24.9  consts
   24.10 -    "rtrancl"	:: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
   24.11 -    "trancl"    :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
   24.12 -    "trans"	:: "i=>o"  			(*transitivity predicate*)
   24.13 +    rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
   24.14 +    trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
   24.15  
   24.16  rules
   24.17 -    trans_def   "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
   24.18 -
   24.19      rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
   24.20 -
   24.21      trancl_def  "r^+ == r O r^*"
   24.22  end
    25.1 --- a/src/ZF/Univ.ML	Tue Jun 21 16:26:34 1994 +0200
    25.2 +++ b/src/ZF/Univ.ML	Tue Jun 21 17:20:34 1994 +0200
    25.3 @@ -1,7 +1,7 @@
    25.4 -(*  Title: 	ZF/univ
    25.5 +(*  Title: 	ZF/Univ
    25.6      ID:         $Id$
    25.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    25.8 -    Copyright   1992  University of Cambridge
    25.9 +    Copyright   1994  University of Cambridge
   25.10  
   25.11  The cumulative hierarchy and a small universe for recursive types
   25.12  *)
   25.13 @@ -161,37 +161,6 @@
   25.14  by (fast_tac ZF_cs 1);
   25.15  val Vfrom_Union = result();
   25.16  
   25.17 -(*** Limit ordinals -- general properties ***)
   25.18 -
   25.19 -goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
   25.20 -by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
   25.21 -val Limit_Union_eq = result();
   25.22 -
   25.23 -goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
   25.24 -by (etac conjunct1 1);
   25.25 -val Limit_is_Ord = result();
   25.26 -
   25.27 -goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 < i";
   25.28 -by (etac (conjunct2 RS conjunct1) 1);
   25.29 -val Limit_has_0 = result();
   25.30 -
   25.31 -goalw Univ.thy [Limit_def] "!!i. [| Limit(i);  j<i |] ==> succ(j) < i";
   25.32 -by (fast_tac ZF_cs 1);
   25.33 -val Limit_has_succ = result();
   25.34 -
   25.35 -goalw Univ.thy [Limit_def] "Limit(nat)";
   25.36 -by (safe_tac (ZF_cs addSIs (ltI::nat_typechecks)));
   25.37 -by (etac ltD 1);
   25.38 -val Limit_nat = result();
   25.39 -
   25.40 -goalw Univ.thy [Limit_def]
   25.41 -    "!!i. [| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
   25.42 -by (safe_tac subset_cs);
   25.43 -by (rtac (not_le_iff_lt RS iffD1) 2);
   25.44 -by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
   25.45 -by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
   25.46 -val non_succ_LimitI = result();
   25.47 -
   25.48  goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
   25.49  by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1);
   25.50  val Ord_cases_lemma = result();
   25.51 @@ -284,7 +253,7 @@
   25.52  by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
   25.53  val Transset_Vfrom_succ = result();
   25.54  
   25.55 -goalw Ord.thy [Pair_def,Transset_def]
   25.56 +goalw Ordinal.thy [Pair_def,Transset_def]
   25.57      "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
   25.58  by (fast_tac ZF_cs 1);
   25.59  val Transset_Pair_subset = result();
    26.1 --- a/src/ZF/Univ.thy	Tue Jun 21 16:26:34 1994 +0200
    26.2 +++ b/src/ZF/Univ.thy	Tue Jun 21 17:20:34 1994 +0200
    26.3 @@ -10,18 +10,15 @@
    26.4  
    26.5  Univ = Arith + Sum + "mono" +
    26.6  consts
    26.7 -    Limit       ::      "i=>o"
    26.8 -    Vfrom       ::      "[i,i]=>i"
    26.9 -    Vset        ::      "i=>i"
   26.10 -    Vrec        ::      "[i, [i,i]=>i] =>i"
   26.11 -    univ        ::      "i=>i"
   26.12 +    Vfrom       :: "[i,i]=>i"
   26.13 +    Vset        :: "i=>i"
   26.14 +    Vrec        :: "[i, [i,i]=>i] =>i"
   26.15 +    univ        :: "i=>i"
   26.16  
   26.17  translations
   26.18      "Vset(x)"   == 	"Vfrom(0,x)"
   26.19  
   26.20  rules
   26.21 -    Limit_def   "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
   26.22 -
   26.23      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
   26.24  
   26.25      Vrec_def
    27.1 --- a/src/ZF/WF.ML	Tue Jun 21 16:26:34 1994 +0200
    27.2 +++ b/src/ZF/WF.ML	Tue Jun 21 17:20:34 1994 +0200
    27.3 @@ -22,33 +22,52 @@
    27.4  
    27.5  (*** Well-founded relations ***)
    27.6  
    27.7 -(*Are these two theorems at all useful??*)
    27.8 +(** Equivalences between wf and wf_on **)
    27.9 +
   27.10 +goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
   27.11 +by (fast_tac ZF_cs 1);
   27.12 +val wf_imp_wf_on = result();
   27.13 +
   27.14 +goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
   27.15 +by (fast_tac ZF_cs 1);
   27.16 +val wf_on_field_imp_wf = result();
   27.17 +
   27.18 +goal WF.thy "wf(r) <-> wf[field(r)](r)";
   27.19 +by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
   27.20 +val wf_iff_wf_on_field = result();
   27.21  
   27.22 -(*If every subset of field(r) possesses an r-minimal element then wf(r).
   27.23 -  Seems impossible to prove this for domain(r) or range(r) instead...
   27.24 -  Consider in particular finite wf relations!*)
   27.25 -val [prem1,prem2] = goalw WF.thy [wf_def]
   27.26 -    "[| field(r)<=A;  \
   27.27 -\       !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
   27.28 -\    ==>  wf(r)";
   27.29 +goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r);  B<=A |] ==> wf[B](r)";
   27.30 +by (fast_tac ZF_cs 1);
   27.31 +val wf_on_subset_A = result();
   27.32 +
   27.33 +goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r);  s<=r |] ==> wf[A](s)";
   27.34 +by (fast_tac ZF_cs 1);
   27.35 +val wf_on_subset_r = result();
   27.36 +
   27.37 +(** Introduction rules for wf_on **)
   27.38 +
   27.39 +(*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
   27.40 +val [prem] = goalw WF.thy [wf_on_def, wf_def]
   27.41 +    "[| !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
   27.42 +\    ==>  wf[A](r)";
   27.43  by (rtac (equals0I RS disjCI RS allI) 1);
   27.44 -by (rtac prem2 1);
   27.45 -by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1);
   27.46 -by (fast_tac ZF_cs 1);
   27.47 -by (fast_tac ZF_cs 1);
   27.48 -val wfI = result();
   27.49 +by (res_inst_tac [ ("Z", "Z") ] prem 1);
   27.50 +by (ALLGOALS (fast_tac ZF_cs));
   27.51 +val wf_onI = result();
   27.52  
   27.53 -(*If r allows well-founded induction then wf(r)*)
   27.54 -val [prem1,prem2] = goal WF.thy
   27.55 -    "[| field(r)<=A;  \
   27.56 -\       !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B |]  \
   27.57 -\    ==>  wf(r)";
   27.58 -by (rtac (prem1 RS wfI) 1);
   27.59 -by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
   27.60 -by (fast_tac ZF_cs 3);
   27.61 +(*If r allows well-founded induction over A then wf[A](r)
   27.62 +  Premise is equivalent to 
   27.63 +  !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B  *)
   27.64 +val [prem] = goal WF.thy
   27.65 +    "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
   27.66 +\              |] ==> y:B |] \
   27.67 +\    ==>  wf[A](r)";
   27.68 +br wf_onI 1;
   27.69 +by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
   27.70 +by (contr_tac 3);
   27.71  by (fast_tac ZF_cs 2);
   27.72  by (fast_tac ZF_cs 1);
   27.73 -val wfI2 = result();
   27.74 +val wf_onI2 = result();
   27.75  
   27.76  
   27.77  (** Well-founded Induction **)
   27.78 @@ -88,29 +107,100 @@
   27.79  by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
   27.80  val wf_induct2 = result();
   27.81  
   27.82 -val prems = goal WF.thy "[| wf(r);  <a,x>:r;  <x,a>:r |] ==> False";
   27.83 -by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> False" 1);
   27.84 -by (wf_ind_tac "a" prems 2);
   27.85 +goal ZF.thy "!!r A. field(r Int A*A) <= A";
   27.86 +by (fast_tac ZF_cs 1);
   27.87 +val field_Int_square = result();
   27.88 +
   27.89 +val wfr::amem::prems = goalw WF.thy [wf_on_def]
   27.90 +    "[| wf[A](r);  a:A;  					\
   27.91 +\       !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x) 	\
   27.92 +\    |]  ==>  P(a)";
   27.93 +by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
   27.94 +by (REPEAT (ares_tac prems 1));
   27.95 +by (fast_tac ZF_cs 1);
   27.96 +val wf_on_induct = result();
   27.97 +
   27.98 +fun wf_on_ind_tac a prems i = 
   27.99 +    EVERY [res_inst_tac [("a",a)] wf_on_induct i,
  27.100 +	   rename_last_tac a ["1"] (i+2),
  27.101 +	   REPEAT (ares_tac prems i)];
  27.102 +
  27.103 +(*If r allows well-founded induction then wf(r)*)
  27.104 +val [subs,indhyp] = goal WF.thy
  27.105 +    "[| field(r)<=A;  \
  27.106 +\       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
  27.107 +\              |] ==> y:B |] \
  27.108 +\    ==>  wf(r)";
  27.109 +br ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1;
  27.110 +by (REPEAT (ares_tac [indhyp] 1));
  27.111 +val wfI2 = result();
  27.112 +
  27.113 +
  27.114 +(*** Properties of well-founded relations ***)
  27.115 +
  27.116 +goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
  27.117 +by (wf_ind_tac "a" [] 1);
  27.118 +by (fast_tac ZF_cs 1);
  27.119 +val wf_not_refl = result();
  27.120 +
  27.121 +goal WF.thy "!!r. [| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
  27.122 +by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
  27.123 +by (wf_ind_tac "a" [] 2);
  27.124  by (fast_tac ZF_cs 2);
  27.125 -by (fast_tac (FOL_cs addIs prems) 1);
  27.126 +by (fast_tac FOL_cs 1);
  27.127  val wf_anti_sym = result();
  27.128  
  27.129 -(*transitive closure of a WF relation is WF!*)
  27.130 -val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
  27.131 -by (rtac (trancl_type RS field_rel_subset RS wfI2) 1);
  27.132 -by (rtac subsetI 1);
  27.133 -(*must retain the universal formula for later use!*)
  27.134 -by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1);
  27.135 -by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1);
  27.136 -by (rtac subset_refl 1);
  27.137 -by (rtac (impI RS allI) 1);
  27.138 +goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
  27.139 +by (wf_on_ind_tac "a" [] 1);
  27.140 +by (fast_tac ZF_cs 1);
  27.141 +val wf_on_not_refl = result();
  27.142 +
  27.143 +goal WF.thy "!!r. [| wf[A](r);  <a,b>:r;  <b,a>:r;  a:A;  b:A |] ==> P";
  27.144 +by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
  27.145 +by (wf_on_ind_tac "a" [] 2);
  27.146 +by (fast_tac ZF_cs 2);
  27.147 +by (fast_tac ZF_cs 1);
  27.148 +val wf_on_anti_sym = result();
  27.149 +
  27.150 +(*Needed to prove well_ordI.  Could also reason that wf[A](r) means
  27.151 +  wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
  27.152 +goal WF.thy
  27.153 +    "!!r. [| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P";
  27.154 +by (subgoal_tac
  27.155 +    "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
  27.156 +by (wf_on_ind_tac "a" [] 2);
  27.157 +by (fast_tac ZF_cs 2);
  27.158 +by (fast_tac ZF_cs 1);
  27.159 +val wf_on_chain3 = result();
  27.160 +
  27.161 +
  27.162 +(*retains the universal formula for later use!*)
  27.163 +val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ];
  27.164 +
  27.165 +(*transitive closure of a WF relation is WF provided A is downwards closed*)
  27.166 +val [wfr,subs] = goal WF.thy
  27.167 +    "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)";
  27.168 +br wf_onI2 1;
  27.169 +by (bchain_tac 1);
  27.170 +by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
  27.171 +by (rtac (impI RS ballI) 1);
  27.172  by (etac tranclE 1);
  27.173 -by (etac (bspec RS mp) 1);
  27.174 -by (etac fieldI1 1);
  27.175 +by (etac (bspec RS mp) 1 THEN assume_tac 1);
  27.176  by (fast_tac ZF_cs 1);
  27.177 +by (cut_facts_tac [subs] 1);
  27.178 +(*astar_tac is slightly faster*)
  27.179 +by (best_tac ZF_cs 1);
  27.180 +val wf_on_trancl = result();
  27.181 +
  27.182 +goal WF.thy "!!r. wf(r) ==> wf(r^+)";
  27.183 +by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
  27.184 +br (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1;
  27.185 +be wf_on_trancl 1;
  27.186  by (fast_tac ZF_cs 1);
  27.187  val wf_trancl = result();
  27.188  
  27.189 +
  27.190 +
  27.191  (** r-``{a} is the set of everything under a in r **)
  27.192  
  27.193  val underI = standard (vimage_singleton_iff RS iffD2);
  27.194 @@ -247,3 +337,12 @@
  27.195  by (REPEAT (ares_tac (prems@[lam_type]) 1
  27.196       ORELSE eresolve_tac [spec RS mp, underD] 1));
  27.197  val wfrec_type = result();
  27.198 +
  27.199 +
  27.200 +goalw WF.thy [wf_on_def, wfrec_on_def]
  27.201 + "!!A r. [| wf[A](r);  a: A |] ==> \
  27.202 +\        wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))";
  27.203 +be (wfrec RS trans) 1;
  27.204 +by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1);
  27.205 +val wfrec_on = result();
  27.206 +
    28.1 --- a/src/ZF/WF.thy	Tue Jun 21 16:26:34 1994 +0200
    28.2 +++ b/src/ZF/WF.thy	Tue Jun 21 17:20:34 1994 +0200
    28.3 @@ -1,22 +1,28 @@
    28.4  (*  Title: 	ZF/wf.thy
    28.5      ID:         $Id$
    28.6      Author: 	Tobias Nipkow and Lawrence C Paulson
    28.7 -    Copyright   1992  University of Cambridge
    28.8 +    Copyright   1994  University of Cambridge
    28.9  
   28.10  Well-founded Recursion
   28.11  *)
   28.12  
   28.13 -WF = Trancl + "mono" +
   28.14 +WF = Trancl + "mono" + "equalities" +
   28.15  consts
   28.16 -    wf		 ::      "i=>o"
   28.17 -    wftrec,wfrec ::      "[i, i, [i,i]=>i] =>i"
   28.18 -    is_recfun    ::      "[i, i, [i,i]=>i, i] =>o"
   28.19 -    the_recfun   ::      "[i, i, [i,i]=>i] =>i"
   28.20 +  wf           :: "i=>o"
   28.21 +  wf_on        :: "[i,i]=>o"			("wf[_]'(_')")
   28.22 +
   28.23 +  wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
   28.24 +  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"	("wfrec[_]'(_,_,_')")
   28.25 +  is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
   28.26 +  the_recfun   :: "[i, i, [i,i]=>i] =>i"
   28.27  
   28.28  rules
   28.29    (*r is a well-founded relation*)
   28.30    wf_def	 "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
   28.31  
   28.32 +  (*r is well-founded relation over A*)
   28.33 +  wf_on_def      "wf_on(A,r) == wf(r Int A*A)"
   28.34 +
   28.35    is_recfun_def  "is_recfun(r,a,H,f) == \
   28.36  \   			(f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
   28.37  
   28.38 @@ -27,4 +33,6 @@
   28.39    (*public version.  Does not require r to be transitive*)
   28.40    wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
   28.41  
   28.42 +  wfrec_on_def   "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
   28.43 +
   28.44  end
    29.1 --- a/src/ZF/ZF.ML	Tue Jun 21 16:26:34 1994 +0200
    29.2 +++ b/src/ZF/ZF.ML	Tue Jun 21 17:20:34 1994 +0200
    29.3 @@ -1,7 +1,7 @@
    29.4  (*  Title: 	ZF/zf.ML
    29.5      ID:         $Id$
    29.6      Author: 	Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    29.7 -    Copyright   1992  University of Cambridge
    29.8 +    Copyright   1994  University of Cambridge
    29.9  
   29.10  Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory 
   29.11  *)
   29.12 @@ -10,63 +10,66 @@
   29.13  
   29.14  signature ZF_LEMMAS = 
   29.15    sig
   29.16 -  val ballE : thm
   29.17 -  val ballI : thm
   29.18 -  val ball_cong : thm
   29.19 -  val ball_simp : thm
   29.20 -  val ball_tac : int -> tactic
   29.21 -  val bexCI : thm
   29.22 -  val bexE : thm
   29.23 -  val bexI : thm
   29.24 -  val bex_cong : thm
   29.25 -  val bspec : thm
   29.26 -  val CollectD1 : thm
   29.27 -  val CollectD2 : thm
   29.28 -  val CollectE : thm
   29.29 -  val CollectI : thm
   29.30 -  val Collect_cong : thm
   29.31 -  val emptyE : thm
   29.32 -  val empty_subsetI : thm
   29.33 -  val equalityCE : thm
   29.34 -  val equalityD1 : thm
   29.35 -  val equalityD2 : thm
   29.36 -  val equalityE : thm
   29.37 -  val equalityI : thm
   29.38 -  val equality_iffI : thm
   29.39 -  val equals0D : thm
   29.40 -  val equals0I : thm
   29.41 -  val ex1_functional : thm
   29.42 -  val InterD : thm
   29.43 -  val InterE : thm
   29.44 -  val InterI : thm
   29.45 -  val INT_E : thm
   29.46 -  val INT_I : thm
   29.47 -  val lemmas_cs : claset
   29.48 -  val PowD : thm
   29.49 -  val PowI : thm
   29.50 -  val RepFunE : thm
   29.51 -  val RepFunI : thm
   29.52 -  val RepFun_eqI : thm
   29.53 -  val RepFun_cong : thm
   29.54 -  val ReplaceE : thm
   29.55 -  val ReplaceI : thm
   29.56 -  val Replace_iff : thm
   29.57 -  val Replace_cong : thm
   29.58 -  val rev_ballE : thm
   29.59 -  val rev_bspec : thm
   29.60 -  val rev_subsetD : thm
   29.61 -  val separation : thm
   29.62 -  val setup_induction : thm
   29.63 -  val set_mp_tac : int -> tactic
   29.64 -  val subsetCE : thm
   29.65 -  val subsetD : thm
   29.66 -  val subsetI : thm
   29.67 -  val subset_refl : thm
   29.68 -  val subset_trans : thm
   29.69 -  val UnionE : thm
   29.70 -  val UnionI : thm
   29.71 -  val UN_E : thm
   29.72 -  val UN_I : thm
   29.73 +  val ballE	: thm
   29.74 +  val ballI	: thm
   29.75 +  val ball_cong	: thm
   29.76 +  val ball_simp	: thm
   29.77 +  val ball_tac	: int -> tactic
   29.78 +  val bexCI	: thm
   29.79 +  val bexE	: thm
   29.80 +  val bexI	: thm
   29.81 +  val bex_cong	: thm
   29.82 +  val bspec	: thm
   29.83 +  val CollectD1	: thm
   29.84 +  val CollectD2	: thm
   29.85 +  val CollectE	: thm
   29.86 +  val CollectI	: thm
   29.87 +  val Collect_cong	: thm
   29.88 +  val emptyE	: thm
   29.89 +  val empty_subsetI	: thm
   29.90 +  val equalityCE	: thm
   29.91 +  val equalityD1	: thm
   29.92 +  val equalityD2	: thm
   29.93 +  val equalityE	: thm
   29.94 +  val equalityI	: thm
   29.95 +  val equality_iffI	: thm
   29.96 +  val equals0D	: thm
   29.97 +  val equals0I	: thm
   29.98 +  val ex1_functional	: thm
   29.99 +  val InterD	: thm
  29.100 +  val InterE	: thm
  29.101 +  val InterI	: thm
  29.102 +  val INT_E	: thm
  29.103 +  val INT_I	: thm
  29.104 +  val INT_cong	: thm
  29.105 +  val lemmas_cs	: claset
  29.106 +  val PowD	: thm
  29.107 +  val PowI	: thm
  29.108 +  val RepFunE	: thm
  29.109 +  val RepFunI	: thm
  29.110 +  val RepFun_eqI	: thm
  29.111 +  val RepFun_cong	: thm
  29.112 +  val ReplaceE	: thm
  29.113 +  val ReplaceI	: thm
  29.114 +  val Replace_iff	: thm
  29.115 +  val Replace_cong	: thm
  29.116 +  val rev_ballE	: thm
  29.117 +  val rev_bspec	: thm
  29.118 +  val rev_subsetD	: thm
  29.119 +  val separation	: thm
  29.120 +  val setup_induction	: thm
  29.121 +  val set_mp_tac	: int -> tactic
  29.122 +  val subsetCE	: thm
  29.123 +  val subsetD	: thm
  29.124 +  val subsetI	: thm
  29.125 +  val subset_iff	: thm
  29.126 +  val subset_refl	: thm
  29.127 +  val subset_trans	: thm
  29.128 +  val UnionE	: thm
  29.129 +  val UnionI	: thm
  29.130 +  val UN_E	: thm
  29.131 +  val UN_I	: thm
  29.132 +  val UN_cong	: thm
  29.133    end;
  29.134  
  29.135  
  29.136 @@ -175,6 +178,11 @@
  29.137  val subset_trans = prove_goal ZF.thy "[| A<=B;  B<=C |] ==> A<=C"
  29.138   (fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]);
  29.139  
  29.140 +(*Useful for proving A<=B by rewriting in some cases*)
  29.141 +val subset_iff = prove_goalw ZF.thy [subset_def,Ball_def]
  29.142 +     "A<=B <-> (ALL x. x:A --> x:B)"
  29.143 + (fn _=> [ (rtac iff_refl 1) ]);
  29.144 +
  29.145  
  29.146  (*** Rules for equality ***)
  29.147  
  29.148 @@ -379,6 +387,10 @@
  29.149    [ (rtac (major RS UnionE) 1),
  29.150      (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
  29.151  
  29.152 +val UN_cong = prove_goal ZF.thy
  29.153 +    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))"
  29.154 + (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]);
  29.155 +
  29.156  
  29.157  (*** Rules for Intersections of families ***)
  29.158  (* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
  29.159 @@ -395,6 +407,10 @@
  29.160    [ (rtac (major RS InterD) 1),
  29.161      (rtac (minor RS RepFunI) 1) ]);
  29.162  
  29.163 +val INT_cong = prove_goal ZF.thy
  29.164 +    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))"
  29.165 + (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]);
  29.166 +
  29.167  
  29.168  (*** Rules for Powersets ***)
  29.169  
    30.1 --- a/src/ZF/equalities.ML	Tue Jun 21 16:26:34 1994 +0200
    30.2 +++ b/src/ZF/equalities.ML	Tue Jun 21 17:20:34 1994 +0200
    30.3 @@ -58,6 +58,10 @@
    30.4  by (fast_tac (eq_cs addSEs [equalityE]) 1);
    30.5  val subset_Int_iff = result();
    30.6  
    30.7 +goal ZF.thy "A<=B <-> B Int A = A";
    30.8 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
    30.9 +val subset_Int_iff2 = result();
   30.10 +
   30.11  (** Binary Union **)
   30.12  
   30.13  goal ZF.thy "0 Un A = A";
   30.14 @@ -88,6 +92,10 @@
   30.15  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   30.16  val subset_Un_iff = result();
   30.17  
   30.18 +goal ZF.thy "A<=B <-> B Un A = B";
   30.19 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
   30.20 +val subset_Un_iff2 = result();
   30.21 +
   30.22  (** Simple properties of Diff -- set difference **)
   30.23  
   30.24  goal ZF.thy "A-A = 0";
   30.25 @@ -161,6 +169,10 @@
   30.26  by (fast_tac eq_cs 1);
   30.27  val Union_Un_distrib = result();
   30.28  
   30.29 +goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";
   30.30 +by (fast_tac ZF_cs 1);
   30.31 +val Union_Int_subset = result();
   30.32 +
   30.33  goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
   30.34  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   30.35  val Union_disjoint = result();
   30.36 @@ -208,15 +220,13 @@
   30.37  by (fast_tac eq_cs 1);
   30.38  val Un_INT_distrib2 = result();
   30.39  
   30.40 -goal ZF.thy "!!A. [| a: A;  ALL y:A. b(y)=b(a) |] ==> (UN y:A. b(y)) = b(a)";
   30.41 -by (fast_tac (eq_cs addSEs [equalityE]) 1);
   30.42 -val UN_singleton_lemma = result();
   30.43 -val UN_singleton = ballI RSN (2,UN_singleton_lemma);
   30.44 +goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";
   30.45 +by (fast_tac eq_cs 1);
   30.46 +val UN_constant = result();
   30.47  
   30.48 -goal ZF.thy "!!A. [| a: A;  ALL y:A. b(y)=b(a) |] ==> (INT y:A. b(y)) = b(a)";
   30.49 -by (fast_tac (eq_cs addSEs [equalityE]) 1);
   30.50 -val INT_singleton_lemma = result();
   30.51 -val INT_singleton = ballI RSN (2,INT_singleton_lemma);
   30.52 +goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";
   30.53 +by (fast_tac eq_cs 1);
   30.54 +val INT_constant = result();
   30.55  
   30.56  (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
   30.57      Union of a family of unions **)
   30.58 @@ -292,7 +302,7 @@
   30.59  val range_Un_eq = result();
   30.60  
   30.61  goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
   30.62 -by (fast_tac eq_cs 1);
   30.63 +by (fast_tac ZF_cs 1);
   30.64  val range_Int_subset = result();
   30.65  
   30.66  goal ZF.thy "range(A) - range(B) <= range(A - B)";
   30.67 @@ -312,6 +322,52 @@
   30.68  val field_diff_subset = result();
   30.69  
   30.70  
   30.71 +(** Image **)
   30.72 +
   30.73 +goal ZF.thy "r``0 = 0";
   30.74 +by (fast_tac eq_cs 1);
   30.75 +val image_empty = result();
   30.76 +
   30.77 +goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
   30.78 +by (fast_tac eq_cs 1);
   30.79 +val image_Un = result();
   30.80 +
   30.81 +goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";
   30.82 +by (fast_tac ZF_cs 1);
   30.83 +val image_Int_subset = result();
   30.84 +
   30.85 +goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";
   30.86 +by (fast_tac ZF_cs 1);
   30.87 +val image_Int_square_subset = result();
   30.88 +
   30.89 +goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
   30.90 +by (fast_tac eq_cs 1);
   30.91 +val image_Int_square = result();
   30.92 +
   30.93 +
   30.94 +(** Inverse Image **)
   30.95 +
   30.96 +goal ZF.thy "r-``0 = 0";
   30.97 +by (fast_tac eq_cs 1);
   30.98 +val vimage_empty = result();
   30.99 +
  30.100 +goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
  30.101 +by (fast_tac eq_cs 1);
  30.102 +val vimage_Un = result();
  30.103 +
  30.104 +goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
  30.105 +by (fast_tac ZF_cs 1);
  30.106 +val vimage_Int_subset = result();
  30.107 +
  30.108 +goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
  30.109 +by (fast_tac ZF_cs 1);
  30.110 +val vimage_Int_square_subset = result();
  30.111 +
  30.112 +goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
  30.113 +by (fast_tac eq_cs 1);
  30.114 +val vimage_Int_square = result();
  30.115 +
  30.116 +
  30.117  (** Converse **)
  30.118  
  30.119  goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
  30.120 @@ -351,3 +407,4 @@
  30.121  goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
  30.122  by (fast_tac eq_cs 1);
  30.123  val INT_Pow_subset = result();
  30.124 +
    31.1 --- a/src/ZF/func.ML	Tue Jun 21 16:26:34 1994 +0200
    31.2 +++ b/src/ZF/func.ML	Tue Jun 21 17:20:34 1994 +0200
    31.3 @@ -223,6 +223,19 @@
    31.4  val Pi_lamE = result();
    31.5  
    31.6  
    31.7 +(** Images of functions **)
    31.8 +
    31.9 +goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
   31.10 +by (fast_tac eq_cs 1);
   31.11 +val image_lam = result();
   31.12 +
   31.13 +goal ZF.thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
   31.14 +be (eta RS subst) 1;
   31.15 +by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
   31.16 +                              addcongs [RepFun_cong]) 1);
   31.17 +val image_fun = result();
   31.18 +
   31.19 +
   31.20  (*** properties of "restrict" ***)
   31.21  
   31.22  goalw ZF.thy [restrict_def,lam_def]
    32.1 --- a/src/ZF/ind_syntax.ML	Tue Jun 21 16:26:34 1994 +0200
    32.2 +++ b/src/ZF/ind_syntax.ML	Tue Jun 21 17:20:34 1994 +0200
    32.3 @@ -89,7 +89,6 @@
    32.4  
    32.5  val Trueprop = Const("Trueprop",oT-->propT);
    32.6  fun mk_tprop P = Trueprop $ P;
    32.7 -fun dest_tprop (Const("Trueprop",_) $ P) = P;
    32.8  
    32.9  (*Prove a goal stated as a term, with exception handling*)
   32.10  fun prove_term sign defs (P,tacsf) = 
   32.11 @@ -113,9 +112,14 @@
   32.12  
   32.13  (*Return the conclusion of a rule, of the form t:X*)
   32.14  fun rule_concl rl = 
   32.15 -    case dest_tprop (Logic.strip_imp_concl rl) of
   32.16 -        Const("op :",_) $ t $ X => (t,X) 
   32.17 -      | _ => error "Conclusion of rule should be a set membership";
   32.18 +    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
   32.19 +		Logic.strip_imp_concl rl
   32.20 +    in  (t,X)  end;
   32.21 +
   32.22 +(*As above, but return error message if bad*)
   32.23 +fun rule_concl_msg sign rl = rule_concl rl
   32.24 +    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
   32.25 +			  Sign.string_of_term sign rl);
   32.26  
   32.27  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   32.28    read_instantiate replaces a propositional variable by a formula variable*)
    33.1 --- a/src/ZF/intr_elim.ML	Tue Jun 21 16:26:34 1994 +0200
    33.2 +++ b/src/ZF/intr_elim.ML	Tue Jun 21 17:20:34 1994 +0200
    33.3 @@ -119,7 +119,7 @@
    33.4  val intr_tms = map (term_of o rd propT) sintrs;
    33.5  
    33.6  local (*Checking the introduction rules*)
    33.7 -  val intr_sets = map (#2 o rule_concl) intr_tms;
    33.8 +  val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
    33.9  
   33.10    fun intr_ok set =
   33.11        case head_of set of Const(a,recT) => a mem rec_names | _ => false;
   33.12 @@ -154,6 +154,10 @@
   33.13    | chk_prem rec_hd t = 
   33.14  	deny (rec_hd occs t) "Recursion term in side formula";
   33.15  
   33.16 +fun dest_tprop (Const("Trueprop",_) $ P) = P
   33.17 +  | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
   33.18 +			  Sign.string_of_term sign Q);
   33.19 +
   33.20  (*Makes a disjunct from an introduction rule*)
   33.21  fun lfp_part intr = (*quantify over rule's free vars except parameters*)
   33.22    let val prems = map dest_tprop (strip_imp_prems intr)
   33.23 @@ -213,7 +217,7 @@
   33.24  val prove = prove_term (sign_of thy);
   33.25  
   33.26  (********)
   33.27 -val dummy = writeln "Proving monotonocity...";
   33.28 +val dummy = writeln "Proving monotonicity...";
   33.29  
   33.30  val bnd_mono = 
   33.31      prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), 
    34.1 --- a/src/ZF/pair.ML	Tue Jun 21 16:26:34 1994 +0200
    34.2 +++ b/src/ZF/pair.ML	Tue Jun 21 17:20:34 1994 +0200
    34.3 @@ -103,7 +103,7 @@
    34.4  val split = prove_goalw ZF.thy [split_def]
    34.5      "split(%x y.c(x,y), <a,b>) = c(a,b)"
    34.6   (fn _ =>
    34.7 -  [ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]);
    34.8 +  [ (fast_tac (upair_cs addIs [the_equality] addSEs [Pair_inject]) 1) ]);
    34.9  
   34.10  val split_type = prove_goal ZF.thy
   34.11      "[|  p:Sigma(A,B);   \
   34.12 @@ -114,6 +114,16 @@
   34.13      (etac ssubst 1),
   34.14      (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
   34.15  
   34.16 +
   34.17 +goal ZF.thy
   34.18 +  "!!u. u: A*B ==>   \
   34.19 +\       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
   34.20 +by (etac SigmaE 1);
   34.21 +by (asm_simp_tac (FOL_ss addsimps [split]) 1);
   34.22 +by (fast_tac (upair_cs addSEs [Pair_inject]) 1);
   34.23 +val expand_split = result();
   34.24 +
   34.25 +
   34.26  (*** conversions for fst and snd ***)
   34.27  
   34.28  val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
    35.1 --- a/src/ZF/simpdata.ML	Tue Jun 21 16:26:34 1994 +0200
    35.2 +++ b/src/ZF/simpdata.ML	Tue Jun 21 17:20:34 1994 +0200
    35.3 @@ -79,15 +79,18 @@
    35.4  		     Some rls => flat (map atomize ([th] RL rls))
    35.5  		   | None     => [th])
    35.6  	    | _ => [th]
    35.7 -  in case concl_of th of (*The operator below is Trueprop*)
    35.8 -	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
    35.9 -      | _ $ (Const("True",_)) => []	(*True is DELETED*)
   35.10 -      | _ $ (Const("False",_)) => []	(*should False do something??*)
   35.11 -      | _ $ A => tryrules atomize_pairs A
   35.12 +  in case concl_of th of 
   35.13 +       Const("Trueprop",_) $ P => 
   35.14 +	  (case P of
   35.15 +	       Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b
   35.16 +	     | Const("True",_)         => []
   35.17 +	     | Const("False",_)        => []
   35.18 +	     | A => tryrules atomize_pairs A)
   35.19 +     | _                       => [th]
   35.20    end;
   35.21  
   35.22  val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
   35.23 -		beta, eta, restrict, fst_conv, snd_conv, split];
   35.24 +		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff];
   35.25  
   35.26  (*Sigma_cong, Pi_cong NOT included by default since they cause
   35.27    flex-flex pairs and the "Check your prover" error -- because most
    36.1 --- a/src/ZF/upair.ML	Tue Jun 21 16:26:34 1994 +0200
    36.2 +++ b/src/ZF/upair.ML	Tue Jun 21 17:20:34 1994 +0200
    36.3 @@ -167,6 +167,15 @@
    36.4      (resolve_tac [major RS the_equality2 RS ssubst] 1),
    36.5      (REPEAT (assume_tac 1)) ]);
    36.6  
    36.7 +(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
    36.8 +  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
    36.9 +
   36.10 +(*If it's "undefined", it's zero!*)
   36.11 +val the_0 = prove_goalw ZF.thy [the_def]
   36.12 +    "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
   36.13 + (fn _ =>
   36.14 +  [ (fast_tac (lemmas_cs addIs [equalityI]) 1) ]);
   36.15 +
   36.16  
   36.17  (*** if -- a conditional expression for formulae ***)
   36.18  
   36.19 @@ -226,6 +235,10 @@
   36.20  val mem_not_refl = prove_goal ZF.thy "a~:a"
   36.21   (K [ (rtac notI 1), (etac mem_anti_refl 1) ]);
   36.22  
   36.23 +(*Good for proving inequalities by rewriting*)
   36.24 +val mem_imp_not_eq = prove_goal ZF.thy "!!a A. a:A ==> a ~= A"
   36.25 + (fn _=> [ fast_tac (lemmas_cs addSEs [mem_anti_refl]) 1 ]);
   36.26 +
   36.27  (*** Rules for succ ***)
   36.28  
   36.29  val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"