modifications for cardinal arithmetic
authorlcp
Thu Jun 23 17:38:12 1994 +0200 (1994-06-23 ago)
changeset 437435875e4b21d
parent 436 0cdc840297bb
child 438 52e8393ccd77
modifications for cardinal arithmetic
src/ZF/Arith.ML
src/ZF/Cardinal.ML
src/ZF/CardinalArith.ML
src/ZF/CardinalArith.thy
src/ZF/Epsilon.ML
src/ZF/Fin.ML
src/ZF/Order.ML
src/ZF/OrderArith.ML
src/ZF/OrderArith.thy
src/ZF/OrderType.ML
src/ZF/Ordinal.ML
src/ZF/Perm.ML
src/ZF/WF.ML
src/ZF/func.ML
src/ZF/pair.ML
src/ZF/upair.ML
     1.1 --- a/src/ZF/Arith.ML	Thu Jun 23 16:44:57 1994 +0200
     1.2 +++ b/src/ZF/Arith.ML	Thu Jun 23 17:38:12 1994 +0200
     1.3 @@ -156,19 +156,17 @@
     1.4      (ALLGOALS
     1.5       (asm_simp_tac (arith_ss addsimps [add_0_right, add_succ_right]))) ]);
     1.6  
     1.7 +(*for a/c rewriting*)
     1.8  val add_left_commute = prove_goal Arith.thy
     1.9 -    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> m#+(n#+k)=n#+(m#+k)"
    1.10 - (fn _ => [rtac (add_commute RS trans) 1, 
    1.11 -           rtac (add_assoc RS trans) 3, 
    1.12 -	   rtac (add_commute RS subst_context) 4,
    1.13 -	   REPEAT (ares_tac [add_type] 1)]);
    1.14 +    "!!m n k. [| m:nat;  n:nat |] ==> m#+(n#+k)=n#+(m#+k)"
    1.15 + (fn _ => [asm_simp_tac (ZF_ss addsimps [add_assoc RS sym, add_commute]) 1]);
    1.16  
    1.17  (*Addition is an AC-operator*)
    1.18  val add_ac = [add_assoc, add_commute, add_left_commute];
    1.19  
    1.20  (*Cancellation law on the left*)
    1.21 -val [knat,eqn] = goal Arith.thy 
    1.22 -    "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
    1.23 +val [eqn,knat] = goal Arith.thy 
    1.24 +    "[| k #+ m = k #+ n;  k:nat |] ==> m=n";
    1.25  by (rtac (eqn RS rev_mp) 1);
    1.26  by (nat_ind_tac "k" [knat] 1);
    1.27  by (ALLGOALS (simp_tac arith_ss));
    1.28 @@ -221,6 +219,16 @@
    1.29    [ (etac nat_induct 1),
    1.30      (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
    1.31  
    1.32 +(*for a/c rewriting*)
    1.33 +val mult_left_commute = prove_goal Arith.thy 
    1.34 +    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> m #* (n #* k) = n #* (m #* k)"
    1.35 + (fn _ => [rtac (mult_commute RS trans) 1, 
    1.36 +           rtac (mult_assoc RS trans) 3, 
    1.37 +	   rtac (mult_commute RS subst_context) 6,
    1.38 +	   REPEAT (ares_tac [mult_type] 1)]);
    1.39 +
    1.40 +val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
    1.41 +
    1.42  
    1.43  (*** Difference ***)
    1.44  
    1.45 @@ -241,11 +249,17 @@
    1.46  
    1.47  (*Subtraction is the inverse of addition. *)
    1.48  val [mnat,nnat] = goal Arith.thy
    1.49 -    "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
    1.50 +    "[| m:nat;  n:nat |] ==> (n#+m) #- n = m";
    1.51  by (rtac (nnat RS nat_induct) 1);
    1.52  by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
    1.53  val diff_add_inverse = result();
    1.54  
    1.55 +goal Arith.thy
    1.56 +    "!!m n. [| m:nat;  n:nat |] ==> (m#+n) #- n = m";
    1.57 +by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
    1.58 +by (REPEAT (ares_tac [diff_add_inverse] 1));
    1.59 +val diff_add_inverse2 = result();
    1.60 +
    1.61  val [mnat,nnat] = goal Arith.thy
    1.62      "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
    1.63  by (rtac (nnat RS nat_induct) 1);
    1.64 @@ -311,7 +325,7 @@
    1.65  goal Arith.thy
    1.66      "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
    1.67  by (etac complete_induct 1);
    1.68 -by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
    1.69 +by (excluded_middle_tac "x<n" 1);
    1.70  (*case x<n*)
    1.71  by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
    1.72  (*case n le x*)
     2.1 --- a/src/ZF/Cardinal.ML	Thu Jun 23 16:44:57 1994 +0200
     2.2 +++ b/src/ZF/Cardinal.ML	Thu Jun 23 17:38:12 1994 +0200
     2.3 @@ -55,8 +55,8 @@
     2.4  (** Equipollence is an equivalence relation **)
     2.5  
     2.6  goalw Cardinal.thy [eqpoll_def] "X eqpoll X";
     2.7 -br exI 1;
     2.8 -br id_bij 1;
     2.9 +by (rtac exI 1);
    2.10 +by (rtac id_bij 1);
    2.11  val eqpoll_refl = result();
    2.12  
    2.13  goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X";
    2.14 @@ -71,8 +71,8 @@
    2.15  (** Le-pollence is a partial ordering **)
    2.16  
    2.17  goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y";
    2.18 -br exI 1;
    2.19 -be id_subset_inj 1;
    2.20 +by (rtac exI 1);
    2.21 +by (etac id_subset_inj 1);
    2.22  val subset_imp_lepoll = result();
    2.23  
    2.24  val lepoll_refl = subset_refl RS subset_imp_lepoll;
    2.25 @@ -97,7 +97,7 @@
    2.26  
    2.27  val [major,minor] = goal Cardinal.thy
    2.28      "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P";
    2.29 -br minor 1;
    2.30 +by (rtac minor 1);
    2.31  by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));
    2.32  val eqpollE = result();
    2.33  
    2.34 @@ -113,7 +113,7 @@
    2.35  by (rtac the_equality 1);
    2.36  by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1);
    2.37  by (REPEAT (etac conjE 1));
    2.38 -be (premOrd RS Ord_linear_lt) 1;
    2.39 +by (etac (premOrd RS Ord_linear_lt) 1);
    2.40  by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot])));
    2.41  val Least_equality = result();
    2.42  
    2.43 @@ -140,18 +140,24 @@
    2.44  
    2.45  (*LEAST really is the smallest*)
    2.46  goal Cardinal.thy "!!i. [| P(i);  i < (LEAST x.P(x)) |] ==> Q";
    2.47 -br (Least_le RSN (2,lt_trans2) RS lt_anti_refl) 1;
    2.48 +by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1);
    2.49  by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
    2.50  val less_LeastE = result();
    2.51  
    2.52 +(*If there is no such P then LEAST is vacuously 0*)
    2.53 +goalw Cardinal.thy [Least_def]
    2.54 +    "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0";
    2.55 +by (rtac the_0 1);
    2.56 +by (fast_tac ZF_cs 1);
    2.57 +val Least_0 = result();
    2.58 +
    2.59  goal Cardinal.thy "Ord(LEAST x.P(x))";
    2.60 -by (res_inst_tac [("Q","EX i. Ord(i) & P(i)")] (excluded_middle RS disjE) 1);
    2.61 +by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);
    2.62  by (safe_tac ZF_cs);
    2.63 -br (Least_le RS ltE) 2;
    2.64 +by (rtac (Least_le RS ltE) 2);
    2.65  by (REPEAT_SOME assume_tac);
    2.66 -bw Least_def;
    2.67 -by (rtac (the_0 RS ssubst) 1 THEN rtac Ord_0 2);
    2.68 -by (fast_tac FOL_cs 1);
    2.69 +by (etac (Least_0 RS ssubst) 1);
    2.70 +by (rtac Ord_0 1);
    2.71  val Ord_Least = result();
    2.72  
    2.73  
    2.74 @@ -165,17 +171,17 @@
    2.75  
    2.76  (*Need AC to prove   X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le  *)
    2.77  goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
    2.78 -br Least_cong 1;
    2.79 +by (rtac Least_cong 1);
    2.80  by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1);
    2.81  val cardinal_cong = result();
    2.82  
    2.83  (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
    2.84  goalw Cardinal.thy [eqpoll_def, cardinal_def]
    2.85      "!!A. well_ord(A,r) ==> |A| eqpoll A";
    2.86 -br LeastI 1;
    2.87 -be Ord_ordertype 2;
    2.88 -br exI 1;
    2.89 -be (ordertype_bij RS bij_converse_bij) 1;
    2.90 +by (rtac LeastI 1);
    2.91 +by (etac Ord_ordertype 2);
    2.92 +by (rtac exI 1);
    2.93 +by (etac (ordertype_bij RS bij_converse_bij) 1);
    2.94  val well_ord_cardinal_eqpoll = result();
    2.95  
    2.96  val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll 
    2.97 @@ -183,8 +189,8 @@
    2.98  
    2.99  goal Cardinal.thy
   2.100      "!!X Y. [| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X eqpoll Y";
   2.101 -br (eqpoll_sym RS eqpoll_trans) 1;
   2.102 -be well_ord_cardinal_eqpoll 1;
   2.103 +by (rtac (eqpoll_sym RS eqpoll_trans) 1);
   2.104 +by (etac well_ord_cardinal_eqpoll 1);
   2.105  by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1);
   2.106  val well_ord_cardinal_eqE = result();
   2.107  
   2.108 @@ -192,55 +198,71 @@
   2.109  (** Observations from Kunen, page 28 **)
   2.110  
   2.111  goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i";
   2.112 -be (eqpoll_refl RS Least_le) 1;
   2.113 +by (etac (eqpoll_refl RS Least_le) 1);
   2.114  val Ord_cardinal_le = result();
   2.115  
   2.116  goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> |i| = i";
   2.117 -be sym 1;
   2.118 +by (etac sym 1);
   2.119  val Card_cardinal_eq = result();
   2.120  
   2.121  val prems = goalw Cardinal.thy [Card_def,cardinal_def]
   2.122      "[| Ord(i);  !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
   2.123 -br (Least_equality RS ssubst) 1;
   2.124 +by (rtac (Least_equality RS ssubst) 1);
   2.125  by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
   2.126  val CardI = result();
   2.127  
   2.128  goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)";
   2.129 -be ssubst 1;
   2.130 -br Ord_Least 1;
   2.131 +by (etac ssubst 1);
   2.132 +by (rtac Ord_Least 1);
   2.133  val Card_is_Ord = result();
   2.134  
   2.135 -goalw Cardinal.thy [cardinal_def] "Ord( |i| )";
   2.136 -br Ord_Least 1;
   2.137 +goalw Cardinal.thy [cardinal_def] "Ord( |A| )";
   2.138 +by (rtac Ord_Least 1);
   2.139  val Ord_cardinal = result();
   2.140  
   2.141 +goal Cardinal.thy "Card(0)";
   2.142 +by (rtac (Ord_0 RS CardI) 1);
   2.143 +by (fast_tac (ZF_cs addSEs [ltE]) 1);
   2.144 +val Card_0 = result();
   2.145 +
   2.146 +goalw Cardinal.thy [cardinal_def] "Card( |A| )";
   2.147 +by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);
   2.148 +by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);
   2.149 +by (rtac (Ord_Least RS CardI) 1);
   2.150 +by (safe_tac ZF_cs);
   2.151 +by (rtac less_LeastE 1);
   2.152 +by (assume_tac 2);
   2.153 +by (etac eqpoll_trans 1);
   2.154 +by (REPEAT (ares_tac [LeastI] 1));
   2.155 +val Card_cardinal = result();
   2.156 +
   2.157  (*Kunen's Lemma 10.5*)
   2.158  goal Cardinal.thy "!!i j. [| |i| le j;  j le i |] ==> |j| = |i|";
   2.159 -br (eqpollI RS cardinal_cong) 1;
   2.160 -be (le_imp_subset RS subset_imp_lepoll) 1;
   2.161 -br lepoll_trans 1;
   2.162 -be (le_imp_subset RS subset_imp_lepoll) 2;
   2.163 -br (eqpoll_sym RS eqpoll_imp_lepoll) 1;
   2.164 -br Ord_cardinal_eqpoll 1;
   2.165 +by (rtac (eqpollI RS cardinal_cong) 1);
   2.166 +by (etac (le_imp_subset RS subset_imp_lepoll) 1);
   2.167 +by (rtac lepoll_trans 1);
   2.168 +by (etac (le_imp_subset RS subset_imp_lepoll) 2);
   2.169 +by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1);
   2.170 +by (rtac Ord_cardinal_eqpoll 1);
   2.171  by (REPEAT (eresolve_tac [ltE, Ord_succD] 1));
   2.172  val cardinal_eq_lemma = result();
   2.173  
   2.174  goal Cardinal.thy "!!i j. i le j ==> |i| le |j|";
   2.175  by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1);
   2.176  by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
   2.177 -br cardinal_eq_lemma 1;
   2.178 -ba 2;
   2.179 -be le_trans 1;
   2.180 -be ltE 1;
   2.181 -be Ord_cardinal_le 1;
   2.182 +by (rtac cardinal_eq_lemma 1);
   2.183 +by (assume_tac 2);
   2.184 +by (etac le_trans 1);
   2.185 +by (etac ltE 1);
   2.186 +by (etac Ord_cardinal_le 1);
   2.187  val cardinal_mono = result();
   2.188  
   2.189  (*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
   2.190  goal Cardinal.thy "!!i j. [| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j";
   2.191 -br Ord_linear2 1;
   2.192 +by (rtac Ord_linear2 1);
   2.193  by (REPEAT_SOME assume_tac);
   2.194 -be (lt_trans2 RS lt_anti_refl) 1;
   2.195 -be cardinal_mono 1;
   2.196 +by (etac (lt_trans2 RS lt_irrefl) 1);
   2.197 +by (etac cardinal_mono 1);
   2.198  val cardinal_lt_imp_lt = result();
   2.199  
   2.200  goal Cardinal.thy "!!i j. [| |i| < k;  Ord(i);  Card(k) |] ==> i < k";
   2.201 @@ -262,7 +284,7 @@
   2.202  val swap_swap_identity = result();
   2.203  
   2.204  goal Cardinal.thy "!!A. [| x:A;  y:A |] ==> swap(A,x,y) : bij(A,A)";
   2.205 -br nilpotent_imp_bijective 1;
   2.206 +by (rtac nilpotent_imp_bijective 1);
   2.207  by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2,
   2.208  		      ballI, swap_swap_identity] 1));
   2.209  val swap_bij = result();
   2.210 @@ -272,24 +294,24 @@
   2.211  (*Lemma suggested by Mike Fourman*)
   2.212  val [prem] = goalw Cardinal.thy [inj_def]
   2.213   "f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)";
   2.214 -br CollectI 1;
   2.215 +by (rtac CollectI 1);
   2.216  (*Proving it's in the function space m->n*)
   2.217  by (cut_facts_tac [prem] 1);
   2.218 -br (if_type RS lam_type) 1;
   2.219 -by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1);
   2.220 -by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1);
   2.221 +by (rtac (if_type RS lam_type) 1);
   2.222 +by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1);
   2.223 +by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1);
   2.224  (*Proving it's injective*)
   2.225  by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
   2.226  (*Adding  prem  earlier would cause the simplifier to loop*)
   2.227  by (cut_facts_tac [prem] 1);
   2.228 -by (fast_tac (ZF_cs addSEs [mem_anti_refl]) 1);
   2.229 +by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1);
   2.230  val inj_succ_succD = result();
   2.231  
   2.232  val [prem] = goalw Cardinal.thy [lepoll_def]
   2.233      "m:nat ==> ALL n: nat. m lepoll n --> m le n";
   2.234  by (nat_ind_tac "m" [prem] 1);
   2.235  by (fast_tac (ZF_cs addSIs [nat_0_le]) 1);
   2.236 -br ballI 1;
   2.237 +by (rtac ballI 1);
   2.238  by (eres_inst_tac [("n","n")] natE 1);
   2.239  by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);
   2.240  by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1);
   2.241 @@ -298,24 +320,23 @@
   2.242  
   2.243  goal Cardinal.thy
   2.244      "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
   2.245 -br iffI 1;
   2.246 +by (rtac iffI 1);
   2.247  by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
   2.248 -by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_asym] addSEs [eqpollE]) 1);
   2.249 +by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] 
   2.250 +                    addSEs [eqpollE]) 1);
   2.251  val nat_eqpoll_iff = result();
   2.252  
   2.253  goalw Cardinal.thy [Card_def,cardinal_def]
   2.254      "!!n. n: nat ==> Card(n)";
   2.255 -br (Least_equality RS ssubst) 1;
   2.256 +by (rtac (Least_equality RS ssubst) 1);
   2.257  by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
   2.258  by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
   2.259 -by (fast_tac (ZF_cs addSEs [lt_anti_refl]) 1);
   2.260 +by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1);
   2.261  val nat_into_Card = result();
   2.262  
   2.263 -val Card_0 = nat_0I RS nat_into_Card;
   2.264 -
   2.265  (*Part of Kunen's Lemma 10.6*)
   2.266  goal Cardinal.thy "!!n. [| succ(n) lepoll n;  n:nat |] ==> P";
   2.267 -br (nat_lepoll_imp_le RS lt_anti_refl) 1;
   2.268 +by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1);
   2.269  by (REPEAT (ares_tac [nat_succI] 1));
   2.270  val succ_lepoll_natE = result();
   2.271  
   2.272 @@ -324,29 +345,34 @@
   2.273  
   2.274  (*This implies Kunen's Lemma 10.6*)
   2.275  goal Cardinal.thy "!!n. [| n<i;  n:nat |] ==> ~ i lepoll n";
   2.276 -br notI 1;
   2.277 +by (rtac notI 1);
   2.278  by (rtac succ_lepoll_natE 1 THEN assume_tac 2);
   2.279  by (rtac lepoll_trans 1 THEN assume_tac 2);
   2.280 -be ltE 1;
   2.281 +by (etac ltE 1);
   2.282  by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1));
   2.283  val lt_not_lepoll = result();
   2.284  
   2.285 -goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";
   2.286 -br (Least_equality RS ssubst) 1;
   2.287 -by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
   2.288 -be ltE 1;
   2.289 -by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
   2.290 -val Card_nat = result();
   2.291 -
   2.292  goal Cardinal.thy "!!i n. [| Ord(i);  n:nat |] ==> i eqpoll n <-> i=n";
   2.293 -br iffI 1;
   2.294 +by (rtac iffI 1);
   2.295  by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
   2.296  by (rtac Ord_linear_lt 1);
   2.297  by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord]));
   2.298  by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN
   2.299      REPEAT (assume_tac 1));
   2.300  by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1)));
   2.301 -be eqpoll_imp_lepoll 1;
   2.302 +by (etac eqpoll_imp_lepoll 1);
   2.303  val Ord_nat_eqpoll_iff = result();
   2.304  
   2.305 +goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";
   2.306 +by (rtac (Least_equality RS ssubst) 1);
   2.307 +by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
   2.308 +by (etac ltE 1);
   2.309 +by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
   2.310 +val Card_nat = result();
   2.311  
   2.312 +(*Allows showing that |i| is a limit cardinal*)
   2.313 +goal Cardinal.thy  "!!i. nat le i ==> nat le |i|";
   2.314 +by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1);
   2.315 +by (etac cardinal_mono 1);
   2.316 +val nat_le_cardinal = result();
   2.317 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/CardinalArith.ML	Thu Jun 23 17:38:12 1994 +0200
     3.3 @@ -0,0 +1,508 @@
     3.4 +(*  Title: 	ZF/CardinalArith.ML
     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 +Cardinal arithmetic -- WITHOUT the Axiom of Choice
    3.10 +*)
    3.11 +
    3.12 +open CardinalArith;
    3.13 +
    3.14 +(*Use AC to discharge first premise*)
    3.15 +goal CardinalArith.thy
    3.16 +    "!!A B. [| well_ord(B,r);  A lepoll B |] ==> |A| le |B|";
    3.17 +by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1);
    3.18 +by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
    3.19 +by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1);
    3.20 +by (rtac lepoll_trans 1);
    3.21 +by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll) 1);
    3.22 +by (assume_tac 1);
    3.23 +by (etac (le_imp_subset RS subset_imp_lepoll RS lepoll_trans) 1);
    3.24 +by (rtac eqpoll_imp_lepoll 1);
    3.25 +by (rewtac lepoll_def);
    3.26 +by (etac exE 1);
    3.27 +by (rtac well_ord_cardinal_eqpoll 1);
    3.28 +by (etac well_ord_rvimage 1);
    3.29 +by (assume_tac 1);
    3.30 +val well_ord_lepoll_imp_le = result();
    3.31 +
    3.32 +val case_ss = ZF_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff,
    3.33 +			      case_Inl, case_Inr, InlI, InrI];
    3.34 +
    3.35 +
    3.36 +(** Congruence laws for successor, cardinal addition and multiplication **)
    3.37 +
    3.38 +val bij_inverse_ss =
    3.39 +    case_ss addsimps [bij_is_fun RS apply_type,
    3.40 +		      bij_converse_bij RS bij_is_fun RS apply_type,
    3.41 +		      left_inverse_bij, right_inverse_bij];
    3.42 +
    3.43 +
    3.44 +(*Congruence law for  succ  under equipollence*)
    3.45 +goalw CardinalArith.thy [eqpoll_def]
    3.46 +    "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";
    3.47 +by (safe_tac ZF_cs);
    3.48 +by (rtac exI 1);
    3.49 +by (res_inst_tac [("c", "%z.if(z=A,B,f`z)"), 
    3.50 +                  ("d", "%z.if(z=B,A,converse(f)`z)")] lam_bijective 1);
    3.51 +by (ALLGOALS
    3.52 +    (asm_simp_tac (bij_inverse_ss addsimps [succI2, mem_imp_not_eq]
    3.53 + 		                  setloop etac succE )));
    3.54 +val succ_eqpoll_cong = result();
    3.55 +
    3.56 +(*Congruence law for + under equipollence*)
    3.57 +goalw CardinalArith.thy [eqpoll_def]
    3.58 +    "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A+B eqpoll C+D";
    3.59 +by (safe_tac ZF_cs);
    3.60 +by (rtac exI 1);
    3.61 +by (res_inst_tac [("c", "case(%x. Inl(f`x), %y. Inr(fa`y))"),
    3.62 +	 ("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")] 
    3.63 +    lam_bijective 1);
    3.64 +by (safe_tac (ZF_cs addSEs [sumE]));
    3.65 +by (ALLGOALS (asm_simp_tac bij_inverse_ss));
    3.66 +val sum_eqpoll_cong = result();
    3.67 +
    3.68 +(*Congruence law for * under equipollence*)
    3.69 +goalw CardinalArith.thy [eqpoll_def]
    3.70 +    "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A*B eqpoll C*D";
    3.71 +by (safe_tac ZF_cs);
    3.72 +by (rtac exI 1);
    3.73 +by (res_inst_tac [("c", "split(%x y. <f`x, fa`y>)"),
    3.74 +		  ("d", "split(%x y. <converse(f)`x, converse(fa)`y>)")] 
    3.75 +    lam_bijective 1);
    3.76 +by (safe_tac ZF_cs);
    3.77 +by (ALLGOALS (asm_simp_tac bij_inverse_ss));
    3.78 +val prod_eqpoll_cong = result();
    3.79 +
    3.80 +
    3.81 +(*** Cardinal addition ***)
    3.82 +
    3.83 +(** Cardinal addition is commutative **)
    3.84 +
    3.85 +(*Easier to prove the two directions separately*)
    3.86 +goalw CardinalArith.thy [eqpoll_def] "A+B eqpoll B+A";
    3.87 +by (rtac exI 1);
    3.88 +by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")] 
    3.89 +    lam_bijective 1);
    3.90 +by (safe_tac (ZF_cs addSEs [sumE]));
    3.91 +by (ALLGOALS (asm_simp_tac case_ss));
    3.92 +val sum_commute_eqpoll = result();
    3.93 +
    3.94 +goalw CardinalArith.thy [cadd_def] "i |+| j = j |+| i";
    3.95 +by (rtac (sum_commute_eqpoll RS cardinal_cong) 1);
    3.96 +val cadd_commute = result();
    3.97 +
    3.98 +(** Cardinal addition is associative **)
    3.99 +
   3.100 +goalw CardinalArith.thy [eqpoll_def] "(A+B)+C eqpoll A+(B+C)";
   3.101 +by (rtac exI 1);
   3.102 +by (res_inst_tac [("c", "case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)))"),
   3.103 +		  ("d", "case(%x.Inl(Inl(x)), case(%x.Inl(Inr(x)), Inr))")] 
   3.104 +    lam_bijective 1);
   3.105 +by (ALLGOALS (asm_simp_tac (case_ss setloop etac sumE)));
   3.106 +val sum_assoc_eqpoll = result();
   3.107 +
   3.108 +(*Unconditional version requires AC*)
   3.109 +goalw CardinalArith.thy [cadd_def]
   3.110 +    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==>	\
   3.111 +\             (i |+| j) |+| k = i |+| (j |+| k)";
   3.112 +by (rtac cardinal_cong 1);
   3.113 +br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS
   3.114 +    eqpoll_trans) 1;
   3.115 +by (rtac (sum_assoc_eqpoll RS eqpoll_trans) 2);
   3.116 +br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS
   3.117 +    eqpoll_sym) 2;
   3.118 +by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));
   3.119 +val Ord_cadd_assoc = result();
   3.120 +
   3.121 +(** 0 is the identity for addition **)
   3.122 +
   3.123 +goalw CardinalArith.thy [eqpoll_def] "0+A eqpoll A";
   3.124 +by (rtac exI 1);
   3.125 +by (res_inst_tac [("c", "case(%x.x, %y.y)"), ("d", "Inr")] 
   3.126 +    lam_bijective 1);
   3.127 +by (ALLGOALS (asm_simp_tac (case_ss setloop eresolve_tac [sumE,emptyE])));
   3.128 +val sum_0_eqpoll = result();
   3.129 +
   3.130 +goalw CardinalArith.thy [cadd_def] "!!i. Card(i) ==> 0 |+| i = i";
   3.131 +by (asm_simp_tac (ZF_ss addsimps [sum_0_eqpoll RS cardinal_cong, 
   3.132 +				  Card_cardinal_eq]) 1);
   3.133 +val cadd_0 = result();
   3.134 +
   3.135 +(** Addition of finite cardinals is "ordinary" addition **)
   3.136 +
   3.137 +goalw CardinalArith.thy [eqpoll_def] "succ(A)+B eqpoll succ(A+B)";
   3.138 +by (rtac exI 1);
   3.139 +by (res_inst_tac [("c", "%z.if(z=Inl(A),A+B,z)"), 
   3.140 +		  ("d", "%z.if(z=A+B,Inl(A),z)")] 
   3.141 +    lam_bijective 1);
   3.142 +by (ALLGOALS
   3.143 +    (asm_simp_tac (case_ss addsimps [succI2, mem_imp_not_eq]
   3.144 +		           setloop eresolve_tac [sumE,succE])));
   3.145 +val sum_succ_eqpoll = result();
   3.146 +
   3.147 +(*Pulling the  succ(...)  outside the |...| requires m, n: nat  *)
   3.148 +(*Unconditional version requires AC*)
   3.149 +goalw CardinalArith.thy [cadd_def]
   3.150 +    "!!m n. [| Ord(m);  Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|";
   3.151 +by (rtac (sum_succ_eqpoll RS cardinal_cong RS trans) 1);
   3.152 +by (rtac (succ_eqpoll_cong RS cardinal_cong) 1);
   3.153 +by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1);
   3.154 +by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));
   3.155 +val cadd_succ_lemma = result();
   3.156 +
   3.157 +val [mnat,nnat] = goal CardinalArith.thy
   3.158 +    "[| m: nat;  n: nat |] ==> m |+| n = m#+n";
   3.159 +by (cut_facts_tac [nnat] 1);
   3.160 +by (nat_ind_tac "m" [mnat] 1);
   3.161 +by (asm_simp_tac (arith_ss addsimps [nat_into_Card RS cadd_0]) 1);
   3.162 +by (asm_simp_tac (arith_ss addsimps [nat_into_Ord, cadd_succ_lemma,
   3.163 +				     nat_into_Card RS Card_cardinal_eq]) 1);
   3.164 +val nat_cadd_eq_add = result();
   3.165 +
   3.166 +
   3.167 +(*** Cardinal multiplication ***)
   3.168 +
   3.169 +(** Cardinal multiplication is commutative **)
   3.170 +
   3.171 +(*Easier to prove the two directions separately*)
   3.172 +goalw CardinalArith.thy [eqpoll_def] "A*B eqpoll B*A";
   3.173 +by (rtac exI 1);
   3.174 +by (res_inst_tac [("c", "split(%x y.<y,x>)"), ("d", "split(%x y.<y,x>)")] 
   3.175 +    lam_bijective 1);
   3.176 +by (safe_tac ZF_cs);
   3.177 +by (ALLGOALS (asm_simp_tac ZF_ss));
   3.178 +val prod_commute_eqpoll = result();
   3.179 +
   3.180 +goalw CardinalArith.thy [cmult_def] "i |*| j = j |*| i";
   3.181 +by (rtac (prod_commute_eqpoll RS cardinal_cong) 1);
   3.182 +val cmult_commute = result();
   3.183 +
   3.184 +(** Cardinal multiplication is associative **)
   3.185 +
   3.186 +goalw CardinalArith.thy [eqpoll_def] "(A*B)*C eqpoll A*(B*C)";
   3.187 +by (rtac exI 1);
   3.188 +by (res_inst_tac [("c", "split(%w z. split(%x y. <x,<y,z>>, w))"),
   3.189 +		  ("d", "split(%x.   split(%y z. <<x,y>, z>))")] 
   3.190 +    lam_bijective 1);
   3.191 +by (safe_tac ZF_cs);
   3.192 +by (ALLGOALS (asm_simp_tac ZF_ss));
   3.193 +val prod_assoc_eqpoll = result();
   3.194 +
   3.195 +(*Unconditional version requires AC*)
   3.196 +goalw CardinalArith.thy [cmult_def]
   3.197 +    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==>	\
   3.198 +\             (i |*| j) |*| k = i |*| (j |*| k)";
   3.199 +by (rtac cardinal_cong 1);
   3.200 +br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS
   3.201 +    eqpoll_trans) 1;
   3.202 +by (rtac (prod_assoc_eqpoll RS eqpoll_trans) 2);
   3.203 +br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS prod_eqpoll_cong RS
   3.204 +    eqpoll_sym) 2;
   3.205 +by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
   3.206 +val Ord_cmult_assoc = result();
   3.207 +
   3.208 +(** Cardinal multiplication distributes over addition **)
   3.209 +
   3.210 +goalw CardinalArith.thy [eqpoll_def] "(A+B)*C eqpoll (A*C)+(B*C)";
   3.211 +by (rtac exI 1);
   3.212 +by (res_inst_tac
   3.213 +    [("c", "split(%x z. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x))"),
   3.214 +     ("d", "case(split(%x y.<Inl(x),y>), split(%x y.<Inr(x),y>))")] 
   3.215 +    lam_bijective 1);
   3.216 +by (safe_tac (ZF_cs addSEs [sumE]));
   3.217 +by (ALLGOALS (asm_simp_tac case_ss));
   3.218 +val sum_prod_distrib_eqpoll = result();
   3.219 +
   3.220 +goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A*A";
   3.221 +by (res_inst_tac [("x", "lam x:A. <x,x>")] exI 1);
   3.222 +by (simp_tac (ZF_ss addsimps [lam_type]) 1);
   3.223 +val prod_square_lepoll = result();
   3.224 +
   3.225 +goalw CardinalArith.thy [cmult_def] "!!k. Card(k) ==> k le k |*| k";
   3.226 +by (rtac le_trans 1);
   3.227 +by (rtac well_ord_lepoll_imp_le 2);
   3.228 +by (rtac prod_square_lepoll 3);
   3.229 +by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord] 2));
   3.230 +by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);
   3.231 +val cmult_square_le = result();
   3.232 +
   3.233 +(** Multiplication by 0 yields 0 **)
   3.234 +
   3.235 +goalw CardinalArith.thy [eqpoll_def] "0*A eqpoll 0";
   3.236 +by (rtac exI 1);
   3.237 +by (rtac lam_bijective 1);
   3.238 +by (safe_tac ZF_cs);
   3.239 +val prod_0_eqpoll = result();
   3.240 +
   3.241 +goalw CardinalArith.thy [cmult_def] "0 |*| i = 0";
   3.242 +by (asm_simp_tac (ZF_ss addsimps [prod_0_eqpoll RS cardinal_cong, 
   3.243 +				  Card_0 RS Card_cardinal_eq]) 1);
   3.244 +val cmult_0 = result();
   3.245 +
   3.246 +(** 1 is the identity for multiplication **)
   3.247 +
   3.248 +goalw CardinalArith.thy [eqpoll_def] "{x}*A eqpoll A";
   3.249 +by (rtac exI 1);
   3.250 +by (res_inst_tac [("c", "snd"), ("d", "%z.<x,z>")] lam_bijective 1);
   3.251 +by (safe_tac ZF_cs);
   3.252 +by (ALLGOALS (asm_simp_tac ZF_ss));
   3.253 +val prod_singleton_eqpoll = result();
   3.254 +
   3.255 +goalw CardinalArith.thy [cmult_def, succ_def] "!!i. Card(i) ==> 1 |*| i = i";
   3.256 +by (asm_simp_tac (ZF_ss addsimps [prod_singleton_eqpoll RS cardinal_cong, 
   3.257 +				  Card_cardinal_eq]) 1);
   3.258 +val cmult_1 = result();
   3.259 +
   3.260 +(** Multiplication of finite cardinals is "ordinary" multiplication **)
   3.261 +
   3.262 +goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B";
   3.263 +by (rtac exI 1);
   3.264 +by (res_inst_tac [("c", "split(%x y. if(x=A, Inl(y), Inr(<x,y>)))"), 
   3.265 +		  ("d", "case(%y. <A,y>, %z.z)")] 
   3.266 +    lam_bijective 1);
   3.267 +by (safe_tac (ZF_cs addSEs [sumE]));
   3.268 +by (ALLGOALS
   3.269 +    (asm_simp_tac (case_ss addsimps [succI2, if_type, mem_imp_not_eq])));
   3.270 +val prod_succ_eqpoll = result();
   3.271 +
   3.272 +
   3.273 +(*Unconditional version requires AC*)
   3.274 +goalw CardinalArith.thy [cmult_def, cadd_def]
   3.275 +    "!!m n. [| Ord(m);  Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)";
   3.276 +by (rtac (prod_succ_eqpoll RS cardinal_cong RS trans) 1);
   3.277 +by (rtac (cardinal_cong RS sym) 1);
   3.278 +by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong) 1);
   3.279 +by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
   3.280 +val cmult_succ_lemma = result();
   3.281 +
   3.282 +val [mnat,nnat] = goal CardinalArith.thy
   3.283 +    "[| m: nat;  n: nat |] ==> m |*| n = m#*n";
   3.284 +by (cut_facts_tac [nnat] 1);
   3.285 +by (nat_ind_tac "m" [mnat] 1);
   3.286 +by (asm_simp_tac (arith_ss addsimps [cmult_0]) 1);
   3.287 +by (asm_simp_tac (arith_ss addsimps [nat_into_Ord, cmult_succ_lemma,
   3.288 +				     nat_cadd_eq_add]) 1);
   3.289 +val nat_cmult_eq_mult = result();
   3.290 +
   3.291 +
   3.292 +(*** Infinite Cardinals are Limit Ordinals ***)
   3.293 +
   3.294 +goalw CardinalArith.thy [lepoll_def, inj_def]
   3.295 +    "!!i. nat <= A ==> succ(A) lepoll A";
   3.296 +by (res_inst_tac [("x",
   3.297 +   "lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
   3.298 +by (rtac (lam_type RS CollectI) 1);
   3.299 +by (rtac if_type 1);
   3.300 +by (etac ([asm_rl, nat_0I] MRS subsetD) 1);
   3.301 +by (etac succE 1);
   3.302 +by (contr_tac 1);
   3.303 +by (rtac if_type 1);
   3.304 +by (assume_tac 2);
   3.305 +by (etac ([asm_rl, nat_succI] MRS subsetD) 1 THEN assume_tac 1);
   3.306 +by (REPEAT (rtac ballI 1));
   3.307 +by (asm_simp_tac 
   3.308 +    (ZF_ss addsimps [succ_inject_iff, succ_not_0, succ_not_0 RS not_sym]
   3.309 +           setloop split_tac [expand_if]) 1);
   3.310 +by (safe_tac (ZF_cs addSIs [nat_0I, nat_succI]));
   3.311 +val nat_succ_lepoll = result();
   3.312 +
   3.313 +goal CardinalArith.thy "!!i. nat <= A ==> succ(A) eqpoll A";
   3.314 +by (etac (nat_succ_lepoll RS eqpollI) 1);
   3.315 +by (rtac (subset_succI RS subset_imp_lepoll) 1);
   3.316 +val nat_succ_eqpoll = result();
   3.317 +
   3.318 +goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Card(i)";
   3.319 +by (etac conjunct1 1);
   3.320 +val InfCard_is_Card = result();
   3.321 +
   3.322 +(*Kunen's Lemma 10.11*)
   3.323 +goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Limit(i)";
   3.324 +by (etac conjE 1);
   3.325 +by (rtac (ltI RS non_succ_LimitI) 1);
   3.326 +by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1);
   3.327 +by (etac Card_is_Ord 1);
   3.328 +by (safe_tac (ZF_cs addSDs [Limit_nat RS Limit_le_succD]));
   3.329 +by (forward_tac [Card_is_Ord RS Ord_succD] 1);
   3.330 +by (rewtac Card_def);
   3.331 +by (res_inst_tac [("i", "succ(y)")] lt_irrefl 1);
   3.332 +by (dtac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1);
   3.333 +(*Tricky combination of substitutions; backtracking needed*)
   3.334 +by (etac ssubst 1 THEN etac ssubst 1 THEN rtac Ord_cardinal_le 1);
   3.335 +by (assume_tac 1);
   3.336 +val InfCard_is_Limit = result();
   3.337 +
   3.338 +
   3.339 +
   3.340 +(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)
   3.341 +
   3.342 +(*A general fact about ordermap*)
   3.343 +goalw Cardinal.thy [eqpoll_def]
   3.344 +    "!!A. [| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
   3.345 +by (rtac exI 1);
   3.346 +by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, well_ord_is_wf]) 1);
   3.347 +by (etac (ordertype_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
   3.348 +by (rtac pred_subset 1);
   3.349 +val ordermap_eqpoll_pred = result();
   3.350 +
   3.351 +(** Establishing the well-ordering **)
   3.352 +
   3.353 +goalw CardinalArith.thy [inj_def]
   3.354 + "!!k. Ord(k) ==>	\
   3.355 +\ (lam z:k*k. split(%x y. <x Un y, <x, y>>, z)) : inj(k*k, k*k*k)";
   3.356 +by (safe_tac ZF_cs);
   3.357 +by (fast_tac (ZF_cs addIs [lam_type, Un_least_lt RS ltD, ltI]
   3.358 +                    addSEs [split_type]) 1);
   3.359 +by (asm_full_simp_tac ZF_ss 1);
   3.360 +val csquare_lam_inj = result();
   3.361 +
   3.362 +goalw CardinalArith.thy [csquare_rel_def]
   3.363 + "!!k. Ord(k) ==> well_ord(k*k, csquare_rel(k))";
   3.364 +by (rtac (csquare_lam_inj RS well_ord_rvimage) 1);
   3.365 +by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
   3.366 +val well_ord_csquare = result();
   3.367 +
   3.368 +(** Characterising initial segments of the well-ordering **)
   3.369 +
   3.370 +goalw CardinalArith.thy [csquare_rel_def]
   3.371 + "!!k. [| x<k;  y<k;  z<k |] ==> \
   3.372 +\      <<x,y>, <z,z>> : csquare_rel(k) --> x le z & y le z";
   3.373 +by (REPEAT (etac ltE 1));
   3.374 +by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,
   3.375 +                                  Un_absorb, Un_least_mem_iff, ltD]) 1);
   3.376 +by (safe_tac (ZF_cs addSEs [mem_irrefl] 
   3.377 +                    addSIs [Un_upper1_le, Un_upper2_le]));
   3.378 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [lt_def, succI2, Ord_succ])));
   3.379 +val csquareD_lemma = result();
   3.380 +val csquareD = csquareD_lemma RS mp |> standard;
   3.381 +
   3.382 +goalw CardinalArith.thy [pred_def]
   3.383 + "!!k. z<k ==> pred(k*k, <z,z>, csquare_rel(k)) <= succ(z)*succ(z)";
   3.384 +by (safe_tac (lemmas_cs addSEs [SigmaE]));	(*avoids using succCI*)
   3.385 +by (rtac (csquareD RS conjE) 1);
   3.386 +by (rewtac lt_def);
   3.387 +by (assume_tac 4);
   3.388 +by (ALLGOALS (fast_tac ZF_cs));
   3.389 +val pred_csquare_subset = result();
   3.390 +
   3.391 +goalw CardinalArith.thy [csquare_rel_def]
   3.392 + "!!k. [| x<z;  y<z;  z<k |] ==> \
   3.393 +\      <<x,y>, <z,z>> : csquare_rel(k)";
   3.394 +by (subgoals_tac ["x<k", "y<k"] 1);
   3.395 +by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));
   3.396 +by (REPEAT (etac ltE 1));
   3.397 +by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,
   3.398 +                                  Un_absorb, Un_least_mem_iff, ltD]) 1);
   3.399 +val csquare_ltI = result();
   3.400 +
   3.401 +(*Part of the traditional proof.  UNUSED since it's harder to prove & apply *)
   3.402 +goalw CardinalArith.thy [csquare_rel_def]
   3.403 + "!!k. [| x le z;  y le z;  z<k |] ==> \
   3.404 +\      <<x,y>, <z,z>> : csquare_rel(k) | x=z & y=z";
   3.405 +by (subgoals_tac ["x<k", "y<k"] 1);
   3.406 +by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2));
   3.407 +by (REPEAT (etac ltE 1));
   3.408 +by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,
   3.409 +                                  Un_absorb, Un_least_mem_iff, ltD]) 1);
   3.410 +by (REPEAT_FIRST (etac succE));
   3.411 +by (ALLGOALS
   3.412 +    (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iff_sym, 
   3.413 +				   subset_Un_iff2 RS iff_sym, OrdmemD])));
   3.414 +val csquare_or_eqI = result();
   3.415 +
   3.416 +(** The cardinality of initial segments **)
   3.417 +
   3.418 +goal CardinalArith.thy
   3.419 +    "!!k. [| InfCard(k);  x<k;  y<k;  z=succ(x Un y) |] ==> \
   3.420 +\         ordermap(k*k, csquare_rel(k)) ` <x,y> lepoll 		\
   3.421 +\         ordermap(k*k, csquare_rel(k)) ` <z,z>";
   3.422 +by (subgoals_tac ["z<k", "well_ord(k*k, csquare_rel(k))"] 1);
   3.423 +by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 2);
   3.424 +by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, Limit_has_succ]) 2);
   3.425 +by (rtac (OrdmemD RS subset_imp_lepoll) 1);
   3.426 +by (res_inst_tac [("z1","z")] (csquare_ltI RS less_imp_ordermap_in) 1);
   3.427 +by (etac well_ord_is_wf 4);
   3.428 +by (ALLGOALS 
   3.429 +    (fast_tac (ZF_cs addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap] 
   3.430 +                     addSEs [ltE])));
   3.431 +val ordermap_z_lepoll = result();
   3.432 +
   3.433 +(*Kunen: "each <x,y>: k*k has no more than z*z predecessors..." (page 29) *)
   3.434 +goalw CardinalArith.thy [cmult_def]
   3.435 +  "!!k. [| InfCard(k);  x<k;  y<k;  z=succ(x Un y) |] ==> \
   3.436 +\       | ordermap(k*k, csquare_rel(k)) ` <x,y> | le  |succ(z)| |*| |succ(z)|";
   3.437 +by (rtac (well_ord_rmult RS well_ord_lepoll_imp_le) 1);
   3.438 +by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1));
   3.439 +by (subgoals_tac ["z<k"] 1);
   3.440 +by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, 
   3.441 +                            Limit_has_succ]) 2);
   3.442 +by (rtac (ordermap_z_lepoll RS lepoll_trans) 1);
   3.443 +by (REPEAT_SOME assume_tac);
   3.444 +by (rtac (ordermap_eqpoll_pred RS eqpoll_imp_lepoll RS lepoll_trans) 1);
   3.445 +by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 1);
   3.446 +by (fast_tac (ZF_cs addIs [ltD]) 1);
   3.447 +by (rtac (pred_csquare_subset RS subset_imp_lepoll RS lepoll_trans) 1 THEN
   3.448 +    assume_tac 1);
   3.449 +by (REPEAT_FIRST (etac ltE));
   3.450 +by (rtac (prod_eqpoll_cong RS eqpoll_sym RS eqpoll_imp_lepoll) 1);
   3.451 +by (REPEAT_FIRST (etac (Ord_succ RS Ord_cardinal_eqpoll)));
   3.452 +val ordermap_csquare_le = result();
   3.453 +
   3.454 +(*Kunen: "... so the order type <= k" *)
   3.455 +goal CardinalArith.thy
   3.456 +    "!!k. [| InfCard(k);  ALL y:k. InfCard(y) --> y |*| y = y |]  ==>  \
   3.457 +\         ordertype(k*k, csquare_rel(k)) le k";
   3.458 +by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
   3.459 +by (rtac all_lt_imp_le 1);
   3.460 +by (assume_tac 1);
   3.461 +by (etac (well_ord_csquare RS Ord_ordertype) 1);
   3.462 +by (rtac Card_lt_imp_lt 1);
   3.463 +by (etac InfCard_is_Card 3);
   3.464 +by (etac ltE 2 THEN assume_tac 2);
   3.465 +by (asm_full_simp_tac (ZF_ss addsimps [ordertype_unfold]) 1);
   3.466 +by (safe_tac (ZF_cs addSEs [ltE]));
   3.467 +by (subgoals_tac ["Ord(xb)", "Ord(y)"] 1);
   3.468 +by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 2));
   3.469 +by (rtac (ordermap_csquare_le RS lt_trans1) 1  THEN
   3.470 +    REPEAT (ares_tac [refl] 1 ORELSE etac ltI 1));
   3.471 +by (res_inst_tac [("i","xb Un y"), ("j","nat")] Ord_linear2 1  THEN
   3.472 +    REPEAT (ares_tac [Ord_Un, Ord_nat] 1));
   3.473 +(*the finite case: xb Un y < nat *)
   3.474 +by (res_inst_tac [("j", "nat")] lt_trans2 1);
   3.475 +by (asm_full_simp_tac (FOL_ss addsimps [InfCard_def]) 2);
   3.476 +by (asm_full_simp_tac
   3.477 +    (ZF_ss addsimps [lt_def, nat_cmult_eq_mult, nat_succI, mult_type,
   3.478 +		     nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1);
   3.479 +(*case nat le (xb Un y), equivalently InfCard(xb Un y)  *)
   3.480 +by (asm_full_simp_tac
   3.481 +    (ZF_ss addsimps [le_imp_subset RS nat_succ_eqpoll RS cardinal_cong,
   3.482 +		     le_succ_iff, InfCard_def, Card_cardinal, Un_least_lt, 
   3.483 +		     Ord_Un, ltI, nat_le_cardinal,
   3.484 +		     Ord_cardinal_le RS lt_trans1 RS ltD]) 1);
   3.485 +val ordertype_csquare_le = result();
   3.486 +
   3.487 +(*This lemma can easily be generalized to premise well_ord(A*A,r) *)
   3.488 +goalw CardinalArith.thy [cmult_def]
   3.489 +    "!!k. Ord(k) ==> k |*| k  =  |ordertype(k*k, csquare_rel(k))|";
   3.490 +by (rtac cardinal_cong 1);
   3.491 +by (rewtac eqpoll_def);
   3.492 +by (rtac exI 1);
   3.493 +by (etac (well_ord_csquare RS ordertype_bij) 1);
   3.494 +val csquare_eq_ordertype = result();
   3.495 +
   3.496 +(*Main result: Kunen's Theorem 10.12*)
   3.497 +goal CardinalArith.thy
   3.498 +    "!!k. InfCard(k) ==> k |*| k = k";
   3.499 +by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
   3.500 +by (etac rev_mp 1);
   3.501 +by (trans_ind_tac "k" [] 1);
   3.502 +by (rtac impI 1);
   3.503 +by (rtac le_anti_sym 1);
   3.504 +by (etac (InfCard_is_Card RS cmult_square_le) 2);
   3.505 +by (rtac (ordertype_csquare_le RSN (2, le_trans)) 1);
   3.506 +by (assume_tac 2);
   3.507 +by (assume_tac 2);
   3.508 +by (asm_simp_tac 
   3.509 +    (ZF_ss addsimps [csquare_eq_ordertype, Ord_cardinal_le,
   3.510 +                     well_ord_csquare RS Ord_ordertype]) 1);
   3.511 +val InfCard_csquare_eq = result();
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/CardinalArith.thy	Thu Jun 23 17:38:12 1994 +0200
     4.3 @@ -0,0 +1,29 @@
     4.4 +(*  Title: 	ZF/CardinalArith.thy
     4.5 +    ID:         $Id$
     4.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1994  University of Cambridge
     4.8 +
     4.9 +Cardinal Arithmetic
    4.10 +*)
    4.11 +
    4.12 +CardinalArith = Cardinal + OrderArith + Arith + 
    4.13 +consts
    4.14 +  InfCard     :: "i=>o"
    4.15 +  "|*|"       :: "[i,i]=>i"       (infixl 70)
    4.16 +  "|+|"       :: "[i,i]=>i"       (infixl 65)
    4.17 +  csquare_rel :: "i=>i"
    4.18 +
    4.19 +rules
    4.20 +
    4.21 +  InfCard_def  "InfCard(i) == Card(i) & nat le i"
    4.22 +
    4.23 +  cadd_def     "i |+| j == | i+j |"
    4.24 +
    4.25 +  cmult_def    "i |*| j == | i*j |"
    4.26 +
    4.27 +  csquare_rel_def
    4.28 +  "csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \
    4.29 +\                            rmult(k,Memrel(k), k*k, 	\
    4.30 +\                                  rmult(k,Memrel(k), k,Memrel(k))))"
    4.31 +
    4.32 +end
     5.1 --- a/src/ZF/Epsilon.ML	Thu Jun 23 16:44:57 1994 +0200
     5.2 +++ b/src/ZF/Epsilon.ML	Thu Jun 23 17:38:12 1994 +0200
     5.3 @@ -219,7 +219,7 @@
     5.4  
     5.5  goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
     5.6  by (rtac (rank RS trans) 1);
     5.7 -by (rtac le_asym 1);
     5.8 +by (rtac le_anti_sym 1);
     5.9  by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le),
    5.10  	     etac (PowD RS rank_mono RS succ_leI)] 1);
    5.11  by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le),
    5.12 @@ -252,7 +252,7 @@
    5.13  val rank_Union = result();
    5.14  
    5.15  goal Epsilon.thy "rank(eclose(a)) = rank(a)";
    5.16 -by (rtac le_asym 1);
    5.17 +by (rtac le_anti_sym 1);
    5.18  by (rtac (arg_subset_eclose RS rank_mono) 2);
    5.19  by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
    5.20  by (rtac (Ord_rank RS UN_least_le) 1);
     6.1 --- a/src/ZF/Fin.ML	Thu Jun 23 16:44:57 1994 +0200
     6.2 +++ b/src/ZF/Fin.ML	Thu Jun 23 17:38:12 1994 +0200
     6.3 @@ -48,7 +48,7 @@
     6.4  \       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
     6.5  \    |] ==> P(b)";
     6.6  by (rtac (major RS Fin.induct) 1);
     6.7 -by (res_inst_tac [("Q","a:b")] (excluded_middle RS disjE) 2);
     6.8 +by (excluded_middle_tac "a:b" 2);
     6.9  by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
    6.10  by (REPEAT (ares_tac prems 1));
    6.11  val Fin_induct = result();
     7.1 --- a/src/ZF/Order.ML	Thu Jun 23 16:44:57 1994 +0200
     7.2 +++ b/src/ZF/Order.ML	Thu Jun 23 17:38:12 1994 +0200
     7.3 @@ -6,9 +6,6 @@
     7.4  For Order.thy.  Orders in Zermelo-Fraenkel Set Theory 
     7.5  *)
     7.6  
     7.7 -(*TO PURE/TACTIC.ML*)
     7.8 -fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
     7.9 -
    7.10  
    7.11  open Order;
    7.12  
    7.13 @@ -44,8 +41,8 @@
    7.14  goalw Order.thy [ord_iso_def] 
    7.15      "!!f. [| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] ==> \
    7.16  \         <converse(f) ` x, converse(f) ` y> : r";
    7.17 -be CollectE 1;
    7.18 -be (bspec RS bspec RS iffD2) 1;
    7.19 +by (etac CollectE 1);
    7.20 +by (etac (bspec RS bspec RS iffD2) 1);
    7.21  by (REPEAT (eresolve_tac [asm_rl, 
    7.22  			  bij_converse_bij RS bij_is_fun RS apply_type] 1));
    7.23  by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
    7.24 @@ -142,10 +139,10 @@
    7.25  goal Order.thy
    7.26      "!!r. [| well_ord(A,r);  well_ord(B,s);  \
    7.27  \            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
    7.28 -br fun_extension 1;
    7.29 -be (ord_iso_is_bij RS bij_is_fun) 1;
    7.30 -be (ord_iso_is_bij RS bij_is_fun) 1;
    7.31 -br well_ord_iso_unique_lemma 1;
    7.32 +by (rtac fun_extension 1);
    7.33 +by (etac (ord_iso_is_bij RS bij_is_fun) 1);
    7.34 +by (etac (ord_iso_is_bij RS bij_is_fun) 1);
    7.35 +by (rtac well_ord_iso_unique_lemma 1);
    7.36  by (REPEAT_SOME assume_tac);
    7.37  val well_ord_iso_unique = result();
    7.38  
    7.39 @@ -157,7 +154,7 @@
    7.40  by (safe_tac ZF_cs);
    7.41  by (linear_case_tac 1);
    7.42  (*case x=xb*)
    7.43 -by (fast_tac (ZF_cs addSEs [wf_on_anti_sym]) 1);
    7.44 +by (fast_tac (ZF_cs addSEs [wf_on_asym]) 1);
    7.45  (*case x<xb*)
    7.46  by (fast_tac (ZF_cs addSEs [wf_on_chain3]) 1);
    7.47  val well_ordI = result();
    7.48 @@ -172,7 +169,7 @@
    7.49  
    7.50  val [major,minor] = goalw Order.thy [pred_def]
    7.51      "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
    7.52 -br (major RS CollectE) 1;
    7.53 +by (rtac (major RS CollectE) 1);
    7.54  by (REPEAT (ares_tac [minor] 1));
    7.55  val predE = result();
    7.56  
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/ZF/OrderArith.ML	Thu Jun 23 17:38:12 1994 +0200
     8.3 @@ -0,0 +1,246 @@
     8.4 +(*  Title: 	ZF/OrderArith.ML
     8.5 +    ID:         $Id$
     8.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 +    Copyright   1994  University of Cambridge
     8.8 +
     8.9 +Towards ordinal arithmetic 
    8.10 +*)
    8.11 +
    8.12 +(*for deleting an unwanted assumption*)
    8.13 +val thin = prove_goal pure_thy "[| PROP P; PROP Q |] ==> PROP Q"
    8.14 +     (fn prems => [resolve_tac prems 1]);
    8.15 +
    8.16 +open OrderArith;
    8.17 +
    8.18 +
    8.19 +(**** Addition of relations -- disjoint sum ****)
    8.20 +
    8.21 +(** Rewrite rules.  Can be used to obtain introduction rules **)
    8.22 +
    8.23 +goalw OrderArith.thy [radd_def] 
    8.24 +    "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B";
    8.25 +by (fast_tac sum_cs 1);
    8.26 +val radd_Inl_Inr_iff = result();
    8.27 +
    8.28 +goalw OrderArith.thy [radd_def] 
    8.29 +    "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  <a',a>:r & a':A & a:A";
    8.30 +by (fast_tac sum_cs 1);
    8.31 +val radd_Inl_iff = result();
    8.32 +
    8.33 +goalw OrderArith.thy [radd_def] 
    8.34 +    "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  <b',b>:s & b':B & b:B";
    8.35 +by (fast_tac sum_cs 1);
    8.36 +val radd_Inr_iff = result();
    8.37 +
    8.38 +goalw OrderArith.thy [radd_def] 
    8.39 +    "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False";
    8.40 +by (fast_tac sum_cs 1);
    8.41 +val radd_Inr_Inl_iff = result();
    8.42 +
    8.43 +(** Elimination Rule **)
    8.44 +
    8.45 +val major::prems = goalw OrderArith.thy [radd_def]
    8.46 +    "[| <p',p> : radd(A,r,B,s);			\
    8.47 +\       !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q;	\
    8.48 +\       !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;	\
    8.49 +\       !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q	\
    8.50 +\    |] ==> Q";
    8.51 +by (cut_facts_tac [major] 1);
    8.52 +(*Split into the three cases*)
    8.53 +by (REPEAT_FIRST
    8.54 +    (eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE]));
    8.55 +(*Apply each premise to correct subgoal; can't just use fast_tac
    8.56 +  because hyp_subst_tac would delete equalities too quickly*)
    8.57 +by (EVERY (map (fn prem => 
    8.58 +		EVERY1 [rtac prem, assume_tac, REPEAT o fast_tac sum_cs])
    8.59 +	   prems));
    8.60 +val raddE = result();
    8.61 +
    8.62 +(** Type checking **)
    8.63 +
    8.64 +goalw OrderArith.thy [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)";
    8.65 +by (rtac Collect_subset 1);
    8.66 +val radd_type = result();
    8.67 +
    8.68 +val field_radd = standard (radd_type RS field_rel_subset);
    8.69 +
    8.70 +(** Linearity **)
    8.71 +
    8.72 +val sum_ss = ZF_ss addsimps [Pair_iff, InlI, InrI, Inl_iff, Inr_iff, 
    8.73 +			     Inl_Inr_iff, Inr_Inl_iff];
    8.74 +
    8.75 +val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, 
    8.76 +			       radd_Inl_Inr_iff, radd_Inr_Inl_iff];
    8.77 +
    8.78 +goalw OrderArith.thy [linear_def]
    8.79 +    "!!r s. [| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
    8.80 +by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE));
    8.81 +by (ALLGOALS (asm_simp_tac radd_ss));
    8.82 +val linear_radd = result();
    8.83 +
    8.84 +
    8.85 +(** Well-foundedness **)
    8.86 +
    8.87 +goal OrderArith.thy
    8.88 +    "!!r s. [| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
    8.89 +by (rtac wf_onI2 1);
    8.90 +by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
    8.91 +(*Proving the lemma, which is needed twice!*)
    8.92 +by (eres_inst_tac [("P", "y : A + B")] thin 2);
    8.93 +by (rtac ballI 2);
    8.94 +by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
    8.95 +by (etac (bspec RS mp) 2);
    8.96 +by (fast_tac sum_cs 2);
    8.97 +by (best_tac (sum_cs addSEs [raddE]) 2);
    8.98 +(*Returning to main part of proof*)
    8.99 +by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
   8.100 +by (best_tac sum_cs 1);
   8.101 +by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
   8.102 +by (etac (bspec RS mp) 1);
   8.103 +by (fast_tac sum_cs 1);
   8.104 +by (best_tac (sum_cs addSEs [raddE]) 1);
   8.105 +val wf_on_radd = result();
   8.106 +
   8.107 +goal OrderArith.thy
   8.108 +     "!!r s. [| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
   8.109 +by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
   8.110 +by (rtac (field_radd RSN (2, wf_on_subset_A)) 1);
   8.111 +by (REPEAT (ares_tac [wf_on_radd] 1));
   8.112 +val wf_radd = result();
   8.113 +
   8.114 +goal OrderArith.thy 
   8.115 +    "!!r s. [| well_ord(A,r);  well_ord(B,s) |] ==> \
   8.116 +\           well_ord(A+B, radd(A,r,B,s))";
   8.117 +by (rtac well_ordI 1);
   8.118 +by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_radd]) 1);
   8.119 +by (asm_full_simp_tac 
   8.120 +    (ZF_ss addsimps [well_ord_def, tot_ord_def, linear_radd]) 1);
   8.121 +val well_ord_radd = result();
   8.122 +
   8.123 +
   8.124 +(**** Multiplication of relations -- lexicographic product ****)
   8.125 +
   8.126 +(** Rewrite rule.  Can be used to obtain introduction rules **)
   8.127 +
   8.128 +goalw OrderArith.thy [rmult_def] 
   8.129 +    "!!r s. <<a',b'>, <a,b>> : rmult(A,r,B,s) <-> 	\
   8.130 +\           (<a',a>: r  & a':A & a:A & b': B & b: B) | 	\
   8.131 +\           (<b',b>: s  & a'=a & a:A & b': B & b: B)";
   8.132 +by (fast_tac ZF_cs 1);
   8.133 +val rmult_iff = result();
   8.134 +
   8.135 +val major::prems = goal OrderArith.thy
   8.136 +    "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);		\
   8.137 +\       [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;	\
   8.138 +\       [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q	\
   8.139 +\    |] ==> Q";
   8.140 +by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1);
   8.141 +by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1));
   8.142 +val rmultE = result();
   8.143 +
   8.144 +(** Type checking **)
   8.145 +
   8.146 +goalw OrderArith.thy [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)";
   8.147 +by (rtac Collect_subset 1);
   8.148 +val rmult_type = result();
   8.149 +
   8.150 +val field_rmult = standard (rmult_type RS field_rel_subset);
   8.151 +
   8.152 +(** Linearity **)
   8.153 +
   8.154 +val [lina,linb] = goal OrderArith.thy
   8.155 +    "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))";
   8.156 +by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
   8.157 +by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE));
   8.158 +by (asm_simp_tac (ZF_ss addsimps [rmult_iff]) 1);
   8.159 +by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1);
   8.160 +by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4);
   8.161 +by (REPEAT_SOME (fast_tac ZF_cs));
   8.162 +val linear_rmult = result();
   8.163 +
   8.164 +
   8.165 +(** Well-foundedness **)
   8.166 +
   8.167 +goal OrderArith.thy
   8.168 +    "!!r s. [| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
   8.169 +by (rtac wf_onI2 1);
   8.170 +by (etac SigmaE 1);
   8.171 +by (etac ssubst 1);
   8.172 +by (subgoal_tac "ALL b:B. <x,b>: Ba" 1);
   8.173 +by (fast_tac ZF_cs 1);
   8.174 +by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1);
   8.175 +by (rtac ballI 1);
   8.176 +by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1);
   8.177 +by (etac (bspec RS mp) 1);
   8.178 +by (fast_tac ZF_cs 1);
   8.179 +by (best_tac (ZF_cs addSEs [rmultE]) 1);
   8.180 +val wf_on_rmult = result();
   8.181 +
   8.182 +
   8.183 +goal OrderArith.thy
   8.184 +    "!!r s. [| wf(r);  wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
   8.185 +by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
   8.186 +by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1);
   8.187 +by (REPEAT (ares_tac [wf_on_rmult] 1));
   8.188 +val wf_rmult = result();
   8.189 +
   8.190 +goal OrderArith.thy 
   8.191 +    "!!r s. [| well_ord(A,r);  well_ord(B,s) |] ==> \
   8.192 +\           well_ord(A*B, rmult(A,r,B,s))";
   8.193 +by (rtac well_ordI 1);
   8.194 +by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_rmult]) 1);
   8.195 +by (asm_full_simp_tac 
   8.196 +    (ZF_ss addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1);
   8.197 +val well_ord_rmult = result();
   8.198 +
   8.199 +
   8.200 +(**** Inverse image of a relation ****)
   8.201 +
   8.202 +(** Rewrite rule **)
   8.203 +
   8.204 +goalw OrderArith.thy [rvimage_def] 
   8.205 +    "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
   8.206 +by (fast_tac ZF_cs 1);
   8.207 +val rvimage_iff = result();
   8.208 +
   8.209 +(** Type checking **)
   8.210 +
   8.211 +goalw OrderArith.thy [rvimage_def] "rvimage(A,f,r) <= A*A";
   8.212 +by (rtac Collect_subset 1);
   8.213 +val rvimage_type = result();
   8.214 +
   8.215 +val field_rvimage = standard (rvimage_type RS field_rel_subset);
   8.216 +
   8.217 +
   8.218 +(** Linearity **)
   8.219 +
   8.220 +val [finj,lin] = goalw OrderArith.thy [inj_def]
   8.221 +    "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
   8.222 +by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
   8.223 +by (REPEAT_FIRST (ares_tac [ballI]));
   8.224 +by (asm_simp_tac (ZF_ss addsimps [rvimage_iff]) 1);
   8.225 +by (cut_facts_tac [finj] 1);
   8.226 +by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
   8.227 +by (REPEAT_SOME (fast_tac (ZF_cs addSIs [apply_type])));
   8.228 +val linear_rvimage = result();
   8.229 +
   8.230 +
   8.231 +(** Well-foundedness **)
   8.232 +
   8.233 +goal OrderArith.thy
   8.234 +    "!!r. [| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
   8.235 +by (rtac wf_onI2 1);
   8.236 +by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
   8.237 +by (fast_tac ZF_cs 1);
   8.238 +by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
   8.239 +by (fast_tac (ZF_cs addSIs [apply_type]) 1);
   8.240 +by (best_tac (ZF_cs addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1);
   8.241 +val wf_on_rvimage = result();
   8.242 +
   8.243 +goal OrderArith.thy 
   8.244 +    "!!r. [| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
   8.245 +by (rtac well_ordI 1);
   8.246 +by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
   8.247 +by (fast_tac (ZF_cs addSIs [wf_on_rvimage, inj_is_fun]) 1);
   8.248 +by (fast_tac (ZF_cs addSIs [linear_rvimage]) 1);
   8.249 +val well_ord_rvimage = result();
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/ZF/OrderArith.thy	Thu Jun 23 17:38:12 1994 +0200
     9.3 @@ -0,0 +1,31 @@
     9.4 +(*  Title: 	ZF/OrderArith.thy
     9.5 +    ID:         $Id$
     9.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   1994  University of Cambridge
     9.8 +
     9.9 +Towards ordinal arithmetic 
    9.10 +*)
    9.11 +
    9.12 +OrderArith = Order + Sum + 
    9.13 +consts
    9.14 +  radd, rmult      :: "[i,i,i,i]=>i"
    9.15 +  rvimage          :: "[i,i,i]=>i"
    9.16 +
    9.17 +rules
    9.18 +  (*disjoint sum of two relations; underlies ordinal addition*)
    9.19 +  radd_def "radd(A,r,B,s) == \
    9.20 +\                {z: (A+B) * (A+B).  \
    9.21 +\                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 \
    9.22 +\                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 \
    9.23 +\                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
    9.24 +
    9.25 +  (*lexicographic product of two relations; underlies ordinal multiplication*)
    9.26 +  rmult_def "rmult(A,r,B,s) == \
    9.27 +\                {z: (A*B) * (A*B).  \
    9.28 +\                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 \
    9.29 +\                       (<x',x>: r | (x'=x & <y',y>: s))}"
    9.30 +
    9.31 +  (*inverse image of a relation*)
    9.32 +  rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
    9.33 +
    9.34 +end
    10.1 --- a/src/ZF/OrderType.ML	Thu Jun 23 16:44:57 1994 +0200
    10.2 +++ b/src/ZF/OrderType.ML	Thu Jun 23 17:38:12 1994 +0200
    10.3 @@ -9,8 +9,8 @@
    10.4  
    10.5  (*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
    10.6  goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
    10.7 -br well_ordI 1;
    10.8 -br (wf_Memrel RS wf_imp_wf_on) 1;
    10.9 +by (rtac well_ordI 1);
   10.10 +by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
   10.11  by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
   10.12  by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
   10.13  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
   10.14 @@ -18,28 +18,36 @@
   10.15  
   10.16  open OrderType;
   10.17  
   10.18 +goalw OrderType.thy [ordermap_def,ordertype_def]
   10.19 +    "ordermap(A,r) : A -> ordertype(A,r)";
   10.20 +by (rtac lam_type 1);
   10.21 +by (rtac (lamI RS imageI) 1);
   10.22 +by (REPEAT (assume_tac 1));
   10.23 +val ordermap_type = result();
   10.24 +
   10.25  (** Unfolding of ordermap **)
   10.26  
   10.27 +(*Useful for cardinality reasoning; see CardinalArith.ML*)
   10.28  goalw OrderType.thy [ordermap_def, pred_def]
   10.29      "!!r. [| wf[A](r);  x:A |] ==> \
   10.30 +\         ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)";
   10.31 +by (asm_simp_tac ZF_ss 1);
   10.32 +by (etac (wfrec_on RS trans) 1);
   10.33 +by (assume_tac 1);
   10.34 +by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
   10.35 +                                  vimage_singleton_iff]) 1);
   10.36 +val ordermap_eq_image = result();
   10.37 +
   10.38 +goal OrderType.thy 
   10.39 +    "!!r. [| wf[A](r);  x:A |] ==> \
   10.40  \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
   10.41 -by (asm_simp_tac ZF_ss 1);
   10.42 -be (wfrec_on RS trans) 1;
   10.43 -ba 1;
   10.44 -by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
   10.45 -                                  vimage_singleton_iff]) 1);
   10.46 +by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
   10.47 +				  ordermap_type RS image_fun]) 1);
   10.48  val ordermap_pred_unfold = result();
   10.49  
   10.50  (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
   10.51  val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
   10.52  
   10.53 -goalw OrderType.thy [ordermap_def,ordertype_def]
   10.54 -    "ordermap(A,r) : A -> ordertype(A,r)";
   10.55 -br lam_type 1;
   10.56 -by (rtac (lamI RS imageI) 1);
   10.57 -by (REPEAT (assume_tac 1));
   10.58 -val ordermap_type = result();
   10.59 -
   10.60  (** Showing that ordermap, ordertype yield ordinals **)
   10.61  
   10.62  fun ordermap_elim_tac i =
   10.63 @@ -53,7 +61,7 @@
   10.64  by (wf_on_ind_tac "x" [] 1);
   10.65  by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
   10.66  by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   10.67 -bws [pred_def,Transset_def];
   10.68 +by (rewrite_goals_tac [pred_def,Transset_def]);
   10.69  by (fast_tac ZF_cs 2);
   10.70  by (safe_tac ZF_cs);
   10.71  by (ordermap_elim_tac 1);
   10.72 @@ -65,7 +73,7 @@
   10.73  by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
   10.74  by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   10.75  by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
   10.76 -bws [Transset_def,well_ord_def];
   10.77 +by (rewrite_goals_tac [Transset_def,well_ord_def]);
   10.78  by (safe_tac ZF_cs);
   10.79  by (ordermap_elim_tac 1);
   10.80  by (fast_tac ZF_cs 1);
   10.81 @@ -77,7 +85,7 @@
   10.82      "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>	\
   10.83  \         ordermap(A,r)`w : ordermap(A,r)`x";
   10.84  by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
   10.85 -ba 1;
   10.86 +by (assume_tac 1);
   10.87  by (fast_tac ZF_cs 1);
   10.88  val less_imp_ordermap_in = result();
   10.89  
   10.90 @@ -88,10 +96,10 @@
   10.91  by (safe_tac ZF_cs);
   10.92  by (linear_case_tac 1);
   10.93  by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
   10.94 -bd less_imp_ordermap_in 1;
   10.95 +by (dtac less_imp_ordermap_in 1);
   10.96  by (REPEAT_SOME assume_tac);
   10.97 -be mem_anti_sym 1;
   10.98 -ba 1;
   10.99 +by (etac mem_asym 1);
  10.100 +by (assume_tac 1);
  10.101  val ordermap_in_imp_less = result();
  10.102  
  10.103  val ordermap_surj = 
  10.104 @@ -102,8 +110,8 @@
  10.105  goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
  10.106      "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
  10.107  by (safe_tac ZF_cs);
  10.108 -br ordermap_type 1;
  10.109 -br ordermap_surj 2;
  10.110 +by (rtac ordermap_type 1);
  10.111 +by (rtac ordermap_surj 2);
  10.112  by (linear_case_tac 1);
  10.113  (*The two cases yield similar contradictions*)
  10.114  by (ALLGOALS (dtac less_imp_ordermap_in));
  10.115 @@ -115,10 +123,10 @@
  10.116   "!!r. well_ord(A,r) ==> \
  10.117  \      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
  10.118  by (safe_tac ZF_cs);
  10.119 -br ordertype_bij 1;
  10.120 -ba 1;
  10.121 +by (rtac ordertype_bij 1);
  10.122 +by (assume_tac 1);
  10.123  by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
  10.124 -bw well_ord_def;
  10.125 +by (rewtac well_ord_def);
  10.126  by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
  10.127  			    ordermap_type RS apply_type]) 1);
  10.128  val ordertype_ord_iso = result();
    11.1 --- a/src/ZF/Ordinal.ML	Thu Jun 23 16:44:57 1994 +0200
    11.2 +++ b/src/ZF/Ordinal.ML	Thu Jun 23 17:38:12 1994 +0200
    11.3 @@ -185,10 +185,10 @@
    11.4  goal Ordinal.thy "~ (ALL i. i:X <-> Ord(i))";
    11.5  by (rtac notI 1);
    11.6  by (forw_inst_tac [("x", "X")] spec 1);
    11.7 -by (safe_tac (ZF_cs addSEs [mem_anti_refl]));
    11.8 +by (safe_tac (ZF_cs addSEs [mem_irrefl]));
    11.9  by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1);
   11.10  by (fast_tac ZF_cs 2);
   11.11 -bw Transset_def;
   11.12 +by (rewtac Transset_def);
   11.13  by (safe_tac ZF_cs);
   11.14  by (asm_full_simp_tac ZF_ss 1);
   11.15  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
   11.16 @@ -223,14 +223,14 @@
   11.17  val lt_trans = result();
   11.18  
   11.19  goalw Ordinal.thy [lt_def] "!!i j. [| i<j;  j<i |] ==> P";
   11.20 -by (REPEAT (eresolve_tac [asm_rl, conjE, mem_anti_sym] 1));
   11.21 -val lt_anti_sym = result();
   11.22 +by (REPEAT (eresolve_tac [asm_rl, conjE, mem_asym] 1));
   11.23 +val lt_asym = result();
   11.24  
   11.25 -val lt_anti_refl = prove_goal Ordinal.thy "i<i ==> P"
   11.26 - (fn [major]=> [ (rtac (major RS (major RS lt_anti_sym)) 1) ]);
   11.27 +val lt_irrefl = prove_goal Ordinal.thy "i<i ==> P"
   11.28 + (fn [major]=> [ (rtac (major RS (major RS lt_asym)) 1) ]);
   11.29  
   11.30  val lt_not_refl = prove_goal Ordinal.thy "~ i<i"
   11.31 - (fn _=> [ (rtac notI 1), (etac lt_anti_refl 1) ]);
   11.32 + (fn _=> [ (rtac notI 1), (etac lt_irrefl 1) ]);
   11.33  
   11.34  (** le is less than or equals;  recall  i le j  abbrevs  i<succ(j) !! **)
   11.35  
   11.36 @@ -261,8 +261,8 @@
   11.37  
   11.38  goal Ordinal.thy "!!i j. [| i le j;  j le i |] ==> i=j";
   11.39  by (asm_full_simp_tac (ZF_ss addsimps [le_iff]) 1);
   11.40 -by (fast_tac (ZF_cs addEs [lt_anti_sym]) 1);
   11.41 -val le_asym = result();
   11.42 +by (fast_tac (ZF_cs addEs [lt_asym]) 1);
   11.43 +val le_anti_sym = result();
   11.44  
   11.45  goal Ordinal.thy "i le 0 <-> i=0";
   11.46  by (fast_tac (ZF_cs addSIs [Ord_0 RS le_refl] addSEs [leE, lt0E]) 1);
   11.47 @@ -273,7 +273,7 @@
   11.48  val lt_cs = 
   11.49      ZF_cs addSIs [le_refl, leCI]
   11.50            addSDs [le0D]
   11.51 -          addSEs [lt_anti_refl, lt0E, leE];
   11.52 +          addSEs [lt_irrefl, lt0E, leE];
   11.53  
   11.54  
   11.55  (*** Natural Deduction rules for Memrel ***)
   11.56 @@ -394,13 +394,13 @@
   11.57  val Ord_linear_le = result();
   11.58  
   11.59  goal Ordinal.thy "!!i j. j le i ==> ~ i<j";
   11.60 -by (fast_tac (lt_cs addEs [lt_anti_sym]) 1);
   11.61 +by (fast_tac (lt_cs addEs [lt_asym]) 1);
   11.62  val le_imp_not_lt = result();
   11.63  
   11.64  goal Ordinal.thy "!!i j. [| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i";
   11.65  by (res_inst_tac [("i","i"),("j","j")] Ord_linear2 1);
   11.66  by (REPEAT (SOMEGOAL assume_tac));
   11.67 -by (fast_tac (lt_cs addEs [lt_anti_sym]) 1);
   11.68 +by (fast_tac (lt_cs addEs [lt_asym]) 1);
   11.69  val not_lt_imp_le = result();
   11.70  
   11.71  goal Ordinal.thy "!!i j. [| Ord(i);  Ord(j) |] ==> ~ i<j <-> j le i";
   11.72 @@ -430,7 +430,7 @@
   11.73  by (rtac (not_lt_iff_le RS iffD1) 1);
   11.74  by (assume_tac 1);
   11.75  by (assume_tac 1);
   11.76 -by (fast_tac (ZF_cs addEs [ltE, mem_anti_refl]) 1);
   11.77 +by (fast_tac (ZF_cs addEs [ltE, mem_irrefl]) 1);
   11.78  val subset_imp_le = result();
   11.79  
   11.80  goal Ordinal.thy "!!i j. i le j ==> i<=j";
   11.81 @@ -453,7 +453,7 @@
   11.82  val [ordi,ordj,minor] = goal Ordinal.thy
   11.83      "[| Ord(i);  Ord(j);  !!x. x<j ==> x<i |] ==> j le i";
   11.84  by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj]));
   11.85 -be (minor RS lt_anti_refl) 1;
   11.86 +by (etac (minor RS lt_irrefl) 1);
   11.87  val all_lt_imp_le = result();
   11.88  
   11.89  (** Transitive laws **)
   11.90 @@ -472,13 +472,13 @@
   11.91  
   11.92  goal Ordinal.thy "!!i j. i<j ==> succ(i) le j";
   11.93  by (rtac (not_lt_iff_le RS iffD1) 1);
   11.94 -by (fast_tac (lt_cs addEs [lt_anti_sym]) 3);
   11.95 +by (fast_tac (lt_cs addEs [lt_asym]) 3);
   11.96  by (ALLGOALS (fast_tac (ZF_cs addEs [ltE] addIs [Ord_succ])));
   11.97  val succ_leI = result();
   11.98  
   11.99  goal Ordinal.thy "!!i j. succ(i) le j ==> i<j";
  11.100  by (rtac (not_le_iff_lt RS iffD1) 1);
  11.101 -by (fast_tac (lt_cs addEs [lt_anti_sym]) 3);
  11.102 +by (fast_tac (lt_cs addEs [lt_asym]) 3);
  11.103  by (ALLGOALS (fast_tac (ZF_cs addEs [ltE, make_elim Ord_succD])));
  11.104  val succ_leE = result();
  11.105  
  11.106 @@ -509,8 +509,8 @@
  11.107  
  11.108  goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> i Un j < k  <->  i<k & j<k";
  11.109  by (safe_tac (ZF_cs addSIs [Un_least_lt]));
  11.110 -br (Un_upper2_le RS lt_trans1) 2;
  11.111 -br (Un_upper1_le RS lt_trans1) 1;
  11.112 +by (rtac (Un_upper2_le RS lt_trans1) 2);
  11.113 +by (rtac (Un_upper1_le RS lt_trans1) 1);
  11.114  by (REPEAT_SOME assume_tac);
  11.115  val Un_least_lt_iff = result();
  11.116  
  11.117 @@ -601,15 +601,15 @@
  11.118      "!!i. [| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
  11.119  by (safe_tac subset_cs);
  11.120  by (rtac (not_le_iff_lt RS iffD1) 2);
  11.121 -by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
  11.122 +by (fast_tac (lt_cs addEs [lt_asym]) 4);
  11.123  by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
  11.124  val non_succ_LimitI = result();
  11.125  
  11.126  goal Ordinal.thy "!!i. Limit(succ(i)) ==> P";
  11.127 -br lt_anti_refl 1;
  11.128 -br Limit_has_succ 1;
  11.129 -ba 1;
  11.130 -be (Limit_is_Ord RS Ord_succD RS le_refl) 1;
  11.131 +by (rtac lt_irrefl 1);
  11.132 +by (rtac Limit_has_succ 1);
  11.133 +by (assume_tac 1);
  11.134 +by (etac (Limit_is_Ord RS Ord_succD RS le_refl) 1);
  11.135  val succ_LimitE = result();
  11.136  
  11.137  goal Ordinal.thy "!!i. [| Limit(i);  i le succ(j) |] ==> i le j";
    12.1 --- a/src/ZF/Perm.ML	Thu Jun 23 16:44:57 1994 +0200
    12.2 +++ b/src/ZF/Perm.ML	Thu Jun 23 17:38:12 1994 +0200
    12.3 @@ -142,7 +142,7 @@
    12.4  
    12.5  val prems = goal Perm.thy
    12.6      "f: inj(A,B) ==> converse(f): inj(range(f), A)";
    12.7 -bw inj_def;  (*rewrite subgoal but not prems!!*)
    12.8 +by (rewtac inj_def);  (*rewrite subgoal but not prems!!*)
    12.9  by (cut_facts_tac prems 1);
   12.10  by (safe_tac ZF_cs);
   12.11  (*apply f to both sides and simplify using right_inverse
   12.12 @@ -359,7 +359,7 @@
   12.13  by (safe_tac ZF_cs);
   12.14  by (dres_inst_tac [("t", "%h.h`y ")] subst_context 1);
   12.15  by (asm_full_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
   12.16 -br fun_extension 1;
   12.17 +by (rtac fun_extension 1);
   12.18  by (REPEAT (ares_tac [comp_fun, lam_type] 1));
   12.19  by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
   12.20  val comp_eq_id_iff = result();
   12.21 @@ -475,7 +475,7 @@
   12.22  by (assume_tac 1);
   12.23  by (dtac apply_equality 1);
   12.24  by (assume_tac 1);
   12.25 -by (res_inst_tac [("a","m")] mem_anti_refl 1);
   12.26 +by (res_inst_tac [("a","m")] mem_irrefl 1);
   12.27  by (fast_tac ZF_cs 1);
   12.28  val inj_succ_restrict = result();
   12.29  
    13.1 --- a/src/ZF/WF.ML	Thu Jun 23 16:44:57 1994 +0200
    13.2 +++ b/src/ZF/WF.ML	Thu Jun 23 17:38:12 1994 +0200
    13.3 @@ -62,7 +62,7 @@
    13.4      "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
    13.5  \              |] ==> y:B |] \
    13.6  \    ==>  wf[A](r)";
    13.7 -br wf_onI 1;
    13.8 +by (rtac wf_onI 1);
    13.9  by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
   13.10  by (contr_tac 3);
   13.11  by (fast_tac ZF_cs 2);
   13.12 @@ -131,7 +131,7 @@
   13.13  \       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
   13.14  \              |] ==> y:B |] \
   13.15  \    ==>  wf(r)";
   13.16 -br ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1;
   13.17 +by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
   13.18  by (REPEAT (ares_tac [indhyp] 1));
   13.19  val wfI2 = result();
   13.20  
   13.21 @@ -148,7 +148,7 @@
   13.22  by (wf_ind_tac "a" [] 2);
   13.23  by (fast_tac ZF_cs 2);
   13.24  by (fast_tac FOL_cs 1);
   13.25 -val wf_anti_sym = result();
   13.26 +val wf_asym = result();
   13.27  
   13.28  goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
   13.29  by (wf_on_ind_tac "a" [] 1);
   13.30 @@ -160,7 +160,7 @@
   13.31  by (wf_on_ind_tac "a" [] 2);
   13.32  by (fast_tac ZF_cs 2);
   13.33  by (fast_tac ZF_cs 1);
   13.34 -val wf_on_anti_sym = result();
   13.35 +val wf_on_asym = result();
   13.36  
   13.37  (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   13.38    wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
   13.39 @@ -180,7 +180,7 @@
   13.40  (*transitive closure of a WF relation is WF provided A is downwards closed*)
   13.41  val [wfr,subs] = goal WF.thy
   13.42      "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)";
   13.43 -br wf_onI2 1;
   13.44 +by (rtac wf_onI2 1);
   13.45  by (bchain_tac 1);
   13.46  by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
   13.47  by (rtac (impI RS ballI) 1);
   13.48 @@ -194,8 +194,8 @@
   13.49  
   13.50  goal WF.thy "!!r. wf(r) ==> wf(r^+)";
   13.51  by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
   13.52 -br (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1;
   13.53 -be wf_on_trancl 1;
   13.54 +by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1);
   13.55 +by (etac wf_on_trancl 1);
   13.56  by (fast_tac ZF_cs 1);
   13.57  val wf_trancl = result();
   13.58  
   13.59 @@ -342,7 +342,7 @@
   13.60  goalw WF.thy [wf_on_def, wfrec_on_def]
   13.61   "!!A r. [| wf[A](r);  a: A |] ==> \
   13.62  \        wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))";
   13.63 -be (wfrec RS trans) 1;
   13.64 +by (etac (wfrec RS trans) 1);
   13.65  by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1);
   13.66  val wfrec_on = result();
   13.67  
    14.1 --- a/src/ZF/func.ML	Thu Jun 23 16:44:57 1994 +0200
    14.2 +++ b/src/ZF/func.ML	Thu Jun 23 17:38:12 1994 +0200
    14.3 @@ -230,7 +230,7 @@
    14.4  val image_lam = result();
    14.5  
    14.6  goal ZF.thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
    14.7 -be (eta RS subst) 1;
    14.8 +by (etac (eta RS subst) 1);
    14.9  by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
   14.10                                addcongs [RepFun_cong]) 1);
   14.11  val image_fun = result();
    15.1 --- a/src/ZF/pair.ML	Thu Jun 23 16:44:57 1994 +0200
    15.2 +++ b/src/ZF/pair.ML	Thu Jun 23 17:38:12 1994 +0200
    15.3 @@ -35,13 +35,13 @@
    15.4  
    15.5  val Pair_neq_fst = prove_goalw ZF.thy [Pair_def] "<a,b>=a ==> P"
    15.6   (fn [major]=>
    15.7 -  [ (rtac (consI1 RS mem_anti_sym RS FalseE) 1),
    15.8 +  [ (rtac (consI1 RS mem_asym RS FalseE) 1),
    15.9      (rtac (major RS subst) 1),
   15.10      (rtac consI1 1) ]);
   15.11  
   15.12  val Pair_neq_snd = prove_goalw ZF.thy [Pair_def] "<a,b>=b ==> P"
   15.13   (fn [major]=>
   15.14 -  [ (rtac (consI1 RS consI2 RS mem_anti_sym RS FalseE) 1),
   15.15 +  [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
   15.16      (rtac (major RS subst) 1),
   15.17      (rtac (consI1 RS consI2) 1) ]);
   15.18  
    16.1 --- a/src/ZF/upair.ML	Thu Jun 23 16:44:57 1994 +0200
    16.2 +++ b/src/ZF/upair.ML	Thu Jun 23 17:38:12 1994 +0200
    16.3 @@ -207,20 +207,21 @@
    16.4  
    16.5  val expand_if = prove_goal ZF.thy
    16.6      "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
    16.7 - (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
    16.8 + (fn _=> [ (excluded_middle_tac "Q" 1),
    16.9  	   (asm_simp_tac if_ss 1),
   16.10  	   (asm_simp_tac if_ss 1) ]);
   16.11  
   16.12  val prems = goal ZF.thy
   16.13      "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";
   16.14 -by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);
   16.15 +by (excluded_middle_tac "P" 1);
   16.16  by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
   16.17  val if_type = result();
   16.18  
   16.19  
   16.20  (*** Foundation lemmas ***)
   16.21  
   16.22 -val mem_anti_sym = prove_goal ZF.thy "[| a:b;  b:a |] ==> P"
   16.23 +(*was called mem_anti_sym*)
   16.24 +val mem_asym = prove_goal ZF.thy "[| a:b;  b:a |] ==> P"
   16.25   (fn prems=>
   16.26    [ (rtac disjE 1),
   16.27      (res_inst_tac [("A","{a,b}")] foundation 1),
   16.28 @@ -229,15 +230,16 @@
   16.29      (fast_tac (lemmas_cs addIs (prems@[consI1,consI2]) 
   16.30  		         addSEs [consE,equalityE]) 1) ]);
   16.31  
   16.32 -val mem_anti_refl = prove_goal ZF.thy "a:a ==> P"
   16.33 - (fn [major]=> [ (rtac (major RS (major RS mem_anti_sym)) 1) ]);
   16.34 +(*was called mem_anti_refl*)
   16.35 +val mem_irrefl = prove_goal ZF.thy "a:a ==> P"
   16.36 + (fn [major]=> [ (rtac (major RS (major RS mem_asym)) 1) ]);
   16.37  
   16.38 -val mem_not_refl = prove_goal ZF.thy "a~:a"
   16.39 - (K [ (rtac notI 1), (etac mem_anti_refl 1) ]);
   16.40 +val mem_not_refl = prove_goal ZF.thy "a ~: a"
   16.41 + (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
   16.42  
   16.43  (*Good for proving inequalities by rewriting*)
   16.44  val mem_imp_not_eq = prove_goal ZF.thy "!!a A. a:A ==> a ~= A"
   16.45 - (fn _=> [ fast_tac (lemmas_cs addSEs [mem_anti_refl]) 1 ]);
   16.46 + (fn _=> [ fast_tac (lemmas_cs addSEs [mem_irrefl]) 1 ]);
   16.47  
   16.48  (*** Rules for succ ***)
   16.49  
   16.50 @@ -279,12 +281,12 @@
   16.51   (fn [major]=>
   16.52    [ (rtac (major RS equalityE) 1),
   16.53      (REPEAT (eresolve_tac [asm_rl, sym, succE, make_elim succ_subsetD,
   16.54 -			   mem_anti_sym] 1)) ]);
   16.55 +			   mem_asym] 1)) ]);
   16.56  
   16.57  val succ_inject_iff = prove_goal ZF.thy "succ(m) = succ(n) <-> m=n"
   16.58   (fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]);
   16.59  
   16.60 -(*UpairI1/2 should become UpairCI;  mem_anti_refl as a hazE? *)
   16.61 +(*UpairI1/2 should become UpairCI;  mem_irrefl as a hazE? *)
   16.62  val upair_cs = lemmas_cs
   16.63    addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2]
   16.64    addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE];