Axiom of choice, cardinality results, etc.
authorlcp
Tue Jul 26 13:21:20 1994 +0200 (1994-07-26)
changeset 48470b789956bd3
parent 483 4d1614d8f119
child 485 5e00a676a211
Axiom of choice, cardinality results, etc.
src/ZF/AC.ML
src/ZF/AC.thy
src/ZF/Cardinal.ML
src/ZF/CardinalArith.ML
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.ML
src/ZF/Cardinal_AC.thy
src/ZF/Fin.ML
src/ZF/Fin.thy
src/ZF/Fixedpt.ML
src/ZF/List.ML
src/ZF/Makefile
src/ZF/Nat.ML
src/ZF/Order.ML
src/ZF/Perm.ML
src/ZF/ROOT.ML
src/ZF/Univ.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/AC.ML	Tue Jul 26 13:21:20 1994 +0200
     1.3 @@ -0,0 +1,61 @@
     1.4 +(*  Title: 	ZF/AC.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +For AC.thy.  The Axiom of Choice
    1.10 +*)
    1.11 +
    1.12 +open AC;
    1.13 +
    1.14 +(*The same as AC, but no premise a:A*)
    1.15 +val [nonempty] = goal AC.thy
    1.16 +     "[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)";
    1.17 +by (excluded_middle_tac "A=0" 1);
    1.18 +by (asm_simp_tac (ZF_ss addsimps [Pi_empty1]) 2 THEN fast_tac ZF_cs 2);
    1.19 +(*The non-trivial case*)
    1.20 +by (safe_tac eq_cs);
    1.21 +by (fast_tac (ZF_cs addSIs [AC, nonempty]) 1);
    1.22 +val AC_Pi = result();
    1.23 +
    1.24 +(*Using dtac, this has the advantage of DELETING the universal quantifier*)
    1.25 +goal AC.thy "!!A B. ALL x:A. EX y. y:B(x) ==> EX y. y : Pi(A,B)";
    1.26 +by (resolve_tac [AC_Pi] 1);
    1.27 +by (eresolve_tac [bspec] 1);
    1.28 +by (assume_tac 1);
    1.29 +val AC_ball_Pi = result();
    1.30 +
    1.31 +goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";
    1.32 +by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
    1.33 +by (etac exI 2);
    1.34 +by (fast_tac eq_cs 1);
    1.35 +val AC_Pi_Pow = result();
    1.36 +
    1.37 +val [nonempty] = goal AC.thy
    1.38 +     "[| !!x. x:A ==> (EX y. y:x)	\
    1.39 +\     |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
    1.40 +by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
    1.41 +by (etac nonempty 1);
    1.42 +by (fast_tac (ZF_cs addDs [apply_type] addIs [Pi_type]) 1);
    1.43 +val AC_func = result();
    1.44 +
    1.45 +goal AC.thy "!!x A. [| 0 ~: A;  x: A |] ==> EX y. y:x";
    1.46 +by (resolve_tac [exCI] 1);
    1.47 +by (eresolve_tac [notE] 1);
    1.48 +by (resolve_tac [equals0I RS subst] 1);
    1.49 +by (eresolve_tac [spec RS notE] 1 THEN REPEAT (assume_tac 1));
    1.50 +val non_empty_family = result();
    1.51 +
    1.52 +goal AC.thy "!!A. 0 ~: A ==> EX f: A->Union(A). ALL x:A. f`x : x";
    1.53 +by (rtac AC_func 1);
    1.54 +by (REPEAT (ares_tac [non_empty_family] 1));
    1.55 +val AC_func0 = result();
    1.56 +
    1.57 +goal AC.thy "EX f: (Pow(C)-{0}) -> C. ALL x:(Pow(C)-{0}). f`x : x";
    1.58 +by (resolve_tac [AC_func0 RS bexE] 1);
    1.59 +by (rtac bexI 2);
    1.60 +by (assume_tac 2);
    1.61 +by (eresolve_tac [fun_weaken_type] 2);
    1.62 +by (ALLGOALS (fast_tac ZF_cs));
    1.63 +val AC_func_Pow = result();
    1.64 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/AC.thy	Tue Jul 26 13:21:20 1994 +0200
     2.3 @@ -0,0 +1,14 @@
     2.4 +(*  Title: 	ZF/AC.thy
     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 +The Axiom of Choice
    2.10 +
    2.11 +This definition comes from Halmos (1960), page 59.
    2.12 +*)
    2.13 +
    2.14 +AC = ZF + "func" +
    2.15 +rules
    2.16 +  AC	"[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    2.17 +end
     3.1 --- a/src/ZF/Cardinal.ML	Thu Jul 21 16:51:26 1994 +0200
     3.2 +++ b/src/ZF/Cardinal.ML	Tue Jul 26 13:21:20 1994 +0200
     3.3 @@ -201,7 +201,7 @@
     3.4  by (etac (eqpoll_refl RS Least_le) 1);
     3.5  val Ord_cardinal_le = result();
     3.6  
     3.7 -goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> |i| = i";
     3.8 +goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> |K| = K";
     3.9  by (etac sym 1);
    3.10  val Card_cardinal_eq = result();
    3.11  
    3.12 @@ -216,7 +216,7 @@
    3.13  by (rtac Ord_Least 1);
    3.14  val Card_is_Ord = result();
    3.15  
    3.16 -goalw Cardinal.thy [cardinal_def] "Ord( |A| )";
    3.17 +goalw Cardinal.thy [cardinal_def] "Ord(|A|)";
    3.18  by (rtac Ord_Least 1);
    3.19  val Ord_cardinal = result();
    3.20  
    3.21 @@ -225,7 +225,7 @@
    3.22  by (fast_tac (ZF_cs addSEs [ltE]) 1);
    3.23  val Card_0 = result();
    3.24  
    3.25 -goalw Cardinal.thy [cardinal_def] "Card( |A| )";
    3.26 +goalw Cardinal.thy [cardinal_def] "Card(|A|)";
    3.27  by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);
    3.28  by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);
    3.29  by (rtac (Ord_Least RS CardI) 1);
    3.30 @@ -265,11 +265,21 @@
    3.31  by (etac cardinal_mono 1);
    3.32  val cardinal_lt_imp_lt = result();
    3.33  
    3.34 -goal Cardinal.thy "!!i j. [| |i| < k;  Ord(i);  Card(k) |] ==> i < k";
    3.35 +goal Cardinal.thy "!!i j. [| |i| < K;  Ord(i);  Card(K) |] ==> i < K";
    3.36  by (asm_simp_tac (ZF_ss addsimps 
    3.37  		  [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1);
    3.38  val Card_lt_imp_lt = result();
    3.39  
    3.40 +goal Cardinal.thy "!!i j. [| Ord(i);  Card(K) |] ==> (|i| < K) <-> (i < K)";
    3.41 +by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1);
    3.42 +val Card_lt_iff = result();
    3.43 +
    3.44 +goal Cardinal.thy "!!i j. [| Ord(i);  Card(K) |] ==> (K le |i|) <-> (K le i)";
    3.45 +by (asm_simp_tac (ZF_ss addsimps 
    3.46 +		  [Card_lt_iff, Card_is_Ord, Ord_cardinal, 
    3.47 +		   not_lt_iff_le RS iff_sym]) 1);
    3.48 +val Card_le_iff = result();
    3.49 +
    3.50  
    3.51  (** The swap operator [NOT USED] **)
    3.52  
     4.1 --- a/src/ZF/CardinalArith.ML	Thu Jul 21 16:51:26 1994 +0200
     4.2 +++ b/src/ZF/CardinalArith.ML	Tue Jul 26 13:21:20 1994 +0200
     4.3 @@ -8,26 +8,7 @@
     4.4  
     4.5  open CardinalArith;
     4.6  
     4.7 -goalw CardinalArith.thy [jump_cardinal_def]
     4.8 -    "Ord(jump_cardinal(K))";
     4.9 -by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
    4.10 -by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
    4.11 -
    4.12 -bw Transset_def;
    4.13 -by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
    4.14 -br (ordertype_subset RS exE) 1;
    4.15 -ba 1;
    4.16 -ba 1;
    4.17 -by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
    4.18 -fr UN_I;
    4.19 -br ReplaceI 2;
    4.20 -by (fast_tac ZF_cs 4);
    4.21 -by (fast_tac ZF_cs 1);
    4.22 -
    4.23 -(****************************************************************)
    4.24 -
    4.25 -
    4.26 -
    4.27 +(*** Elementary properties ***)
    4.28  
    4.29  (*Use AC to discharge first premise*)
    4.30  goal CardinalArith.thy
    4.31 @@ -59,18 +40,37 @@
    4.32  		      left_inverse_bij, right_inverse_bij];
    4.33  
    4.34  
    4.35 -(*Congruence law for  succ  under equipollence*)
    4.36 +(*Congruence law for  cons  under equipollence*)
    4.37  goalw CardinalArith.thy [eqpoll_def]
    4.38 -    "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";
    4.39 +    "!!A B. [| A eqpoll B;  a ~: A;  b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
    4.40  by (safe_tac ZF_cs);
    4.41  by (rtac exI 1);
    4.42 -by (res_inst_tac [("c", "%z.if(z=A,B,f`z)"), 
    4.43 -                  ("d", "%z.if(z=B,A,converse(f)`z)")] lam_bijective 1);
    4.44 +by (res_inst_tac [("c", "%z.if(z=a,b,f`z)"), 
    4.45 +                  ("d", "%z.if(z=b,a,converse(f)`z)")] lam_bijective 1);
    4.46  by (ALLGOALS
    4.47 -    (asm_simp_tac (bij_inverse_ss addsimps [succI2, mem_imp_not_eq]
    4.48 - 		                  setloop etac succE )));
    4.49 +    (asm_simp_tac (bij_inverse_ss addsimps [consI2]
    4.50 + 		                  setloop (etac consE ORELSE' 
    4.51 +				           split_tac [expand_if]))));
    4.52 +by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1);
    4.53 +by (fast_tac (ZF_cs addIs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
    4.54 +val cons_eqpoll_cong = result();
    4.55 +
    4.56 +(*Congruence law for  succ  under equipollence*)
    4.57 +goalw CardinalArith.thy [succ_def]
    4.58 +    "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";
    4.59 +by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1));
    4.60  val succ_eqpoll_cong = result();
    4.61  
    4.62 +(*Each element of Fin(A) is equivalent to a natural number*)
    4.63 +goal CardinalArith.thy
    4.64 +    "!!X A. X: Fin(A) ==> EX n:nat. X eqpoll n";
    4.65 +by (eresolve_tac [Fin_induct] 1);
    4.66 +by (fast_tac (ZF_cs addIs [eqpoll_refl, nat_0I]) 1);
    4.67 +by (fast_tac (ZF_cs addSIs [cons_eqpoll_cong, 
    4.68 +			    rewrite_rule [succ_def] nat_succI] 
    4.69 +                            addSEs [mem_irrefl]) 1);
    4.70 +val Fin_eqpoll = result();
    4.71 +
    4.72  (*Congruence law for + under equipollence*)
    4.73  goalw CardinalArith.thy [eqpoll_def]
    4.74      "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A+B eqpoll C+D";
    4.75 @@ -125,7 +125,7 @@
    4.76  
    4.77  (*Unconditional version requires AC*)
    4.78  goalw CardinalArith.thy [cadd_def]
    4.79 -    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==>	\
    4.80 +    "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==>	\
    4.81  \             (i |+| j) |+| k = i |+| (j |+| k)";
    4.82  by (rtac cardinal_cong 1);
    4.83  br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS
    4.84 @@ -133,8 +133,8 @@
    4.85  by (rtac (sum_assoc_eqpoll RS eqpoll_trans) 2);
    4.86  br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS
    4.87      eqpoll_sym) 2;
    4.88 -by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));
    4.89 -val Ord_cadd_assoc = result();
    4.90 +by (REPEAT (ares_tac [well_ord_radd] 1));
    4.91 +val well_ord_cadd_assoc = result();
    4.92  
    4.93  (** 0 is the identity for addition **)
    4.94  
    4.95 @@ -145,7 +145,7 @@
    4.96  by (ALLGOALS (asm_simp_tac (case_ss setloop eresolve_tac [sumE,emptyE])));
    4.97  val sum_0_eqpoll = result();
    4.98  
    4.99 -goalw CardinalArith.thy [cadd_def] "!!i. Card(i) ==> 0 |+| i = i";
   4.100 +goalw CardinalArith.thy [cadd_def] "!!K. Card(K) ==> 0 |+| K = K";
   4.101  by (asm_simp_tac (ZF_ss addsimps [sum_0_eqpoll RS cardinal_cong, 
   4.102  				  Card_cardinal_eq]) 1);
   4.103  val cadd_0 = result();
   4.104 @@ -212,7 +212,7 @@
   4.105  
   4.106  (*Unconditional version requires AC*)
   4.107  goalw CardinalArith.thy [cmult_def]
   4.108 -    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==>	\
   4.109 +    "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==>	\
   4.110  \             (i |*| j) |*| k = i |*| (j |*| k)";
   4.111  by (rtac cardinal_cong 1);
   4.112  br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS
   4.113 @@ -220,8 +220,8 @@
   4.114  by (rtac (prod_assoc_eqpoll RS eqpoll_trans) 2);
   4.115  br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS prod_eqpoll_cong RS
   4.116      eqpoll_sym) 2;
   4.117 -by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
   4.118 -val Ord_cmult_assoc = result();
   4.119 +by (REPEAT (ares_tac [well_ord_rmult] 1));
   4.120 +val well_ord_cmult_assoc = result();
   4.121  
   4.122  (** Cardinal multiplication distributes over addition **)
   4.123  
   4.124 @@ -240,7 +240,7 @@
   4.125  by (simp_tac (ZF_ss addsimps [lam_type]) 1);
   4.126  val prod_square_lepoll = result();
   4.127  
   4.128 -goalw CardinalArith.thy [cmult_def] "!!k. Card(k) ==> k le k |*| k";
   4.129 +goalw CardinalArith.thy [cmult_def] "!!K. Card(K) ==> K le K |*| K";
   4.130  by (rtac le_trans 1);
   4.131  by (rtac well_ord_lepoll_imp_le 2);
   4.132  by (rtac prod_square_lepoll 3);
   4.133 @@ -270,7 +270,7 @@
   4.134  by (ALLGOALS (asm_simp_tac ZF_ss));
   4.135  val prod_singleton_eqpoll = result();
   4.136  
   4.137 -goalw CardinalArith.thy [cmult_def, succ_def] "!!i. Card(i) ==> 1 |*| i = i";
   4.138 +goalw CardinalArith.thy [cmult_def, succ_def] "!!K. Card(K) ==> 1 |*| K = K";
   4.139  by (asm_simp_tac (ZF_ss addsimps [prod_singleton_eqpoll RS cardinal_cong, 
   4.140  				  Card_cardinal_eq]) 1);
   4.141  val cmult_1 = result();
   4.142 @@ -309,6 +309,7 @@
   4.143  
   4.144  (*** Infinite Cardinals are Limit Ordinals ***)
   4.145  
   4.146 +(*Using lam_injective might simplify this proof!*)
   4.147  goalw CardinalArith.thy [lepoll_def, inj_def]
   4.148      "!!i. nat <= A ==> succ(A) lepoll A";
   4.149  by (res_inst_tac [("x",
   4.150 @@ -333,12 +334,12 @@
   4.151  by (rtac (subset_succI RS subset_imp_lepoll) 1);
   4.152  val nat_succ_eqpoll = result();
   4.153  
   4.154 -goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Card(i)";
   4.155 +goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)";
   4.156  by (etac conjunct1 1);
   4.157  val InfCard_is_Card = result();
   4.158  
   4.159  (*Kunen's Lemma 10.11*)
   4.160 -goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Limit(i)";
   4.161 +goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Limit(K)";
   4.162  by (etac conjE 1);
   4.163  by (rtac (ltI RS non_succ_LimitI) 1);
   4.164  by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1);
   4.165 @@ -369,8 +370,8 @@
   4.166  (** Establishing the well-ordering **)
   4.167  
   4.168  goalw CardinalArith.thy [inj_def]
   4.169 - "!!k. Ord(k) ==>	\
   4.170 -\ (lam z:k*k. split(%x y. <x Un y, <x, y>>, z)) : inj(k*k, k*k*k)";
   4.171 + "!!K. Ord(K) ==>	\
   4.172 +\ (lam z:K*K. split(%x y. <x Un y, <x, y>>, z)) : inj(K*K, K*K*K)";
   4.173  by (safe_tac ZF_cs);
   4.174  by (fast_tac (ZF_cs addIs [lam_type, Un_least_lt RS ltD, ltI]
   4.175                      addSEs [split_type]) 1);
   4.176 @@ -378,7 +379,7 @@
   4.177  val csquare_lam_inj = result();
   4.178  
   4.179  goalw CardinalArith.thy [csquare_rel_def]
   4.180 - "!!k. Ord(k) ==> well_ord(k*k, csquare_rel(k))";
   4.181 + "!!K. Ord(K) ==> well_ord(K*K, csquare_rel(K))";
   4.182  by (rtac (csquare_lam_inj RS well_ord_rvimage) 1);
   4.183  by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
   4.184  val well_ord_csquare = result();
   4.185 @@ -386,8 +387,8 @@
   4.186  (** Characterising initial segments of the well-ordering **)
   4.187  
   4.188  goalw CardinalArith.thy [csquare_rel_def]
   4.189 - "!!k. [| x<k;  y<k;  z<k |] ==> \
   4.190 -\      <<x,y>, <z,z>> : csquare_rel(k) --> x le z & y le z";
   4.191 + "!!K. [| x<K;  y<K;  z<K |] ==> \
   4.192 +\      <<x,y>, <z,z>> : csquare_rel(K) --> x le z & y le z";
   4.193  by (REPEAT (etac ltE 1));
   4.194  by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,
   4.195                                    Un_absorb, Un_least_mem_iff, ltD]) 1);
   4.196 @@ -398,7 +399,7 @@
   4.197  val csquareD = csquareD_lemma RS mp |> standard;
   4.198  
   4.199  goalw CardinalArith.thy [pred_def]
   4.200 - "!!k. z<k ==> pred(k*k, <z,z>, csquare_rel(k)) <= succ(z)*succ(z)";
   4.201 + "!!K. z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
   4.202  by (safe_tac (lemmas_cs addSEs [SigmaE]));	(*avoids using succCI*)
   4.203  by (rtac (csquareD RS conjE) 1);
   4.204  by (rewtac lt_def);
   4.205 @@ -407,9 +408,9 @@
   4.206  val pred_csquare_subset = result();
   4.207  
   4.208  goalw CardinalArith.thy [csquare_rel_def]
   4.209 - "!!k. [| x<z;  y<z;  z<k |] ==> \
   4.210 -\      <<x,y>, <z,z>> : csquare_rel(k)";
   4.211 -by (subgoals_tac ["x<k", "y<k"] 1);
   4.212 + "!!K. [| x<z;  y<z;  z<K |] ==> \
   4.213 +\      <<x,y>, <z,z>> : csquare_rel(K)";
   4.214 +by (subgoals_tac ["x<K", "y<K"] 1);
   4.215  by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));
   4.216  by (REPEAT (etac ltE 1));
   4.217  by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,
   4.218 @@ -418,9 +419,9 @@
   4.219  
   4.220  (*Part of the traditional proof.  UNUSED since it's harder to prove & apply *)
   4.221  goalw CardinalArith.thy [csquare_rel_def]
   4.222 - "!!k. [| x le z;  y le z;  z<k |] ==> \
   4.223 -\      <<x,y>, <z,z>> : csquare_rel(k) | x=z & y=z";
   4.224 -by (subgoals_tac ["x<k", "y<k"] 1);
   4.225 + "!!K. [| x le z;  y le z;  z<K |] ==> \
   4.226 +\      <<x,y>, <z,z>> : csquare_rel(K) | x=z & y=z";
   4.227 +by (subgoals_tac ["x<K", "y<K"] 1);
   4.228  by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2));
   4.229  by (REPEAT (etac ltE 1));
   4.230  by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,
   4.231 @@ -434,10 +435,10 @@
   4.232  (** The cardinality of initial segments **)
   4.233  
   4.234  goal CardinalArith.thy
   4.235 -    "!!k. [| InfCard(k);  x<k;  y<k;  z=succ(x Un y) |] ==> \
   4.236 -\         ordermap(k*k, csquare_rel(k)) ` <x,y> lepoll 		\
   4.237 -\         ordermap(k*k, csquare_rel(k)) ` <z,z>";
   4.238 -by (subgoals_tac ["z<k", "well_ord(k*k, csquare_rel(k))"] 1);
   4.239 +    "!!K. [| InfCard(K);  x<K;  y<K;  z=succ(x Un y) |] ==> \
   4.240 +\         ordermap(K*K, csquare_rel(K)) ` <x,y> lepoll 		\
   4.241 +\         ordermap(K*K, csquare_rel(K)) ` <z,z>";
   4.242 +by (subgoals_tac ["z<K", "well_ord(K*K, csquare_rel(K))"] 1);
   4.243  by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 2);
   4.244  by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, Limit_has_succ]) 2);
   4.245  by (rtac (OrdmemD RS subset_imp_lepoll) 1);
   4.246 @@ -448,13 +449,13 @@
   4.247                       addSEs [ltE])));
   4.248  val ordermap_z_lepoll = result();
   4.249  
   4.250 -(*Kunen: "each <x,y>: k*k has no more than z*z predecessors..." (page 29) *)
   4.251 +(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
   4.252  goalw CardinalArith.thy [cmult_def]
   4.253 -  "!!k. [| InfCard(k);  x<k;  y<k;  z=succ(x Un y) |] ==> \
   4.254 -\       | ordermap(k*k, csquare_rel(k)) ` <x,y> | le  |succ(z)| |*| |succ(z)|";
   4.255 +  "!!K. [| InfCard(K);  x<K;  y<K;  z=succ(x Un y) |] ==> \
   4.256 +\       | ordermap(K*K, csquare_rel(K)) ` <x,y> | le  |succ(z)| |*| |succ(z)|";
   4.257  by (rtac (well_ord_rmult RS well_ord_lepoll_imp_le) 1);
   4.258  by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1));
   4.259 -by (subgoals_tac ["z<k"] 1);
   4.260 +by (subgoals_tac ["z<K"] 1);
   4.261  by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, 
   4.262                              Limit_has_succ]) 2);
   4.263  by (rtac (ordermap_z_lepoll RS lepoll_trans) 1);
   4.264 @@ -469,10 +470,10 @@
   4.265  by (REPEAT_FIRST (etac (Ord_succ RS Ord_cardinal_eqpoll)));
   4.266  val ordermap_csquare_le = result();
   4.267  
   4.268 -(*Kunen: "... so the order type <= k" *)
   4.269 +(*Kunen: "... so the order type <= K" *)
   4.270  goal CardinalArith.thy
   4.271 -    "!!k. [| InfCard(k);  ALL y:k. InfCard(y) --> y |*| y = y |]  ==>  \
   4.272 -\         ordertype(k*k, csquare_rel(k)) le k";
   4.273 +    "!!K. [| InfCard(K);  ALL y:K. InfCard(y) --> y |*| y = y |]  ==>  \
   4.274 +\         ordertype(K*K, csquare_rel(K)) le K";
   4.275  by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
   4.276  by (rtac all_lt_imp_le 1);
   4.277  by (assume_tac 1);
   4.278 @@ -504,7 +505,7 @@
   4.279  
   4.280  (*This lemma can easily be generalized to premise well_ord(A*A,r) *)
   4.281  goalw CardinalArith.thy [cmult_def]
   4.282 -    "!!k. Ord(k) ==> k |*| k  =  |ordertype(k*k, csquare_rel(k))|";
   4.283 +    "!!K. Ord(K) ==> K |*| K  =  |ordertype(K*K, csquare_rel(K))|";
   4.284  by (rtac cardinal_cong 1);
   4.285  by (rewtac eqpoll_def);
   4.286  by (rtac exI 1);
   4.287 @@ -512,11 +513,10 @@
   4.288  val csquare_eq_ordertype = result();
   4.289  
   4.290  (*Main result: Kunen's Theorem 10.12*)
   4.291 -goal CardinalArith.thy
   4.292 -    "!!k. InfCard(k) ==> k |*| k = k";
   4.293 +goal CardinalArith.thy "!!K. InfCard(K) ==> K |*| K = K";
   4.294  by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
   4.295  by (etac rev_mp 1);
   4.296 -by (trans_ind_tac "k" [] 1);
   4.297 +by (trans_ind_tac "K" [] 1);
   4.298  by (rtac impI 1);
   4.299  by (rtac le_anti_sym 1);
   4.300  by (etac (InfCard_is_Card RS cmult_square_le) 2);
   4.301 @@ -527,3 +527,111 @@
   4.302      (ZF_ss addsimps [csquare_eq_ordertype, Ord_cardinal_le,
   4.303                       well_ord_csquare RS Ord_ordertype]) 1);
   4.304  val InfCard_csquare_eq = result();
   4.305 +
   4.306 +
   4.307 +goal CardinalArith.thy
   4.308 +    "!!A. [| well_ord(A,r);  InfCard(|A|) |] ==> A*A eqpoll A";
   4.309 +by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1);
   4.310 +by (REPEAT (etac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1));
   4.311 +by (resolve_tac [well_ord_cardinal_eqE] 1);
   4.312 +by (REPEAT (ares_tac [Ord_cardinal, well_ord_rmult, well_ord_Memrel] 1));
   4.313 +by (asm_simp_tac (ZF_ss addsimps [symmetric cmult_def, InfCard_csquare_eq]) 1);
   4.314 +val well_ord_InfCard_square_eq = result();
   4.315 +
   4.316 +
   4.317 +(*** For every cardinal number there exists a greater one
   4.318 +     [Kunen's Theorem 10.16, which would be trivial using AC] ***)
   4.319 +
   4.320 +goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))";
   4.321 +by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   4.322 +by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
   4.323 +bw Transset_def;
   4.324 +by (safe_tac ZF_cs);
   4.325 +by (rtac (ordertype_subset RS exE) 1 THEN REPEAT (assume_tac 1));
   4.326 +by (resolve_tac [UN_I] 1);
   4.327 +by (resolve_tac [ReplaceI] 2);
   4.328 +by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset])));
   4.329 +val Ord_jump_cardinal = result();
   4.330 +
   4.331 +(*Allows selective unfolding.  Less work than deriving intro/elim rules*)
   4.332 +goalw CardinalArith.thy [jump_cardinal_def]
   4.333 +     "i : jump_cardinal(K) <->   \
   4.334 +\         (EX r X. r <= K*K & X <= K & well_ord(X,r) & i = ordertype(X,r))";
   4.335 +by (fast_tac subset_cs 1);	(*It's vital to avoid reasoning about <=*)
   4.336 +val jump_cardinal_iff = result();
   4.337 +
   4.338 +(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*)
   4.339 +goal CardinalArith.thy "!!K. Ord(K) ==> K < jump_cardinal(K)";
   4.340 +by (resolve_tac [Ord_jump_cardinal RSN (2,ltI)] 1);
   4.341 +by (resolve_tac [jump_cardinal_iff RS iffD2] 1);
   4.342 +by (REPEAT_FIRST (ares_tac [exI, conjI, well_ord_Memrel]));
   4.343 +by (resolve_tac [subset_refl] 2);
   4.344 +by (asm_simp_tac (ZF_ss addsimps [Memrel_def, subset_iff]) 1);
   4.345 +by (asm_simp_tac (ZF_ss addsimps [ordertype_Memrel]) 1);
   4.346 +val K_lt_jump_cardinal = result();
   4.347 +
   4.348 +(*The proof by contradiction: the bijection f yields a wellordering of X
   4.349 +  whose ordertype is jump_cardinal(K).  *)
   4.350 +goal CardinalArith.thy
   4.351 +    "!!K. [| well_ord(X,r);  r <= K * K;  X <= K;	\
   4.352 +\            f : bij(ordertype(X,r), jump_cardinal(K)) 	\
   4.353 +\	  |] ==> jump_cardinal(K) : jump_cardinal(K)";
   4.354 +by (subgoal_tac "f O ordermap(X,r): bij(X, jump_cardinal(K))" 1);
   4.355 +by (REPEAT (ares_tac [comp_bij, ordermap_bij] 2));
   4.356 +by (resolve_tac [jump_cardinal_iff RS iffD2] 1);
   4.357 +by (REPEAT_FIRST (resolve_tac [exI, conjI]));
   4.358 +by (rtac ([rvimage_type, Sigma_mono] MRS subset_trans) 1);
   4.359 +by (REPEAT (assume_tac 1));
   4.360 +by (etac (bij_is_inj RS well_ord_rvimage) 1);
   4.361 +by (rtac (Ord_jump_cardinal RS well_ord_Memrel) 1);
   4.362 +by (asm_simp_tac
   4.363 +    (ZF_ss addsimps [well_ord_Memrel RSN (2, bij_ordertype_vimage), 
   4.364 +		     ordertype_Memrel, Ord_jump_cardinal]) 1);
   4.365 +val Card_jump_cardinal_lemma = result();
   4.366 +
   4.367 +(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*)
   4.368 +goal CardinalArith.thy "Card(jump_cardinal(K))";
   4.369 +by (rtac (Ord_jump_cardinal RS CardI) 1);
   4.370 +by (rewrite_goals_tac [eqpoll_def]);
   4.371 +by (safe_tac (ZF_cs addSDs [ltD, jump_cardinal_iff RS iffD1]));
   4.372 +by (REPEAT (ares_tac [Card_jump_cardinal_lemma RS mem_irrefl] 1));
   4.373 +val Card_jump_cardinal = result();
   4.374 +
   4.375 +(*** Basic properties of successor cardinals ***)
   4.376 +
   4.377 +goalw CardinalArith.thy [csucc_def]
   4.378 +    "!!K. Ord(K) ==> Card(csucc(K)) & K < csucc(K)";
   4.379 +by (rtac LeastI 1);
   4.380 +by (REPEAT (ares_tac [conjI, Card_jump_cardinal, K_lt_jump_cardinal,
   4.381 +		      Ord_jump_cardinal] 1));
   4.382 +val csucc_basic = result();
   4.383 +
   4.384 +val Card_csucc = csucc_basic RS conjunct1 |> standard;
   4.385 +
   4.386 +val lt_csucc = csucc_basic RS conjunct2 |> standard;
   4.387 +
   4.388 +goalw CardinalArith.thy [csucc_def]
   4.389 +    "!!K L. [| Card(L);  K<L |] ==> csucc(K) le L";
   4.390 +by (rtac Least_le 1);
   4.391 +by (REPEAT (ares_tac [conjI, Card_is_Ord] 1));
   4.392 +val csucc_le = result();
   4.393 +
   4.394 +goal CardinalArith.thy
   4.395 +    "!!K. [| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K";
   4.396 +by (resolve_tac [iffI] 1);
   4.397 +by (resolve_tac [Card_lt_imp_lt] 2);
   4.398 +by (eresolve_tac [lt_trans1] 2);
   4.399 +by (REPEAT (ares_tac [lt_csucc, Card_csucc, Card_is_Ord] 2));
   4.400 +by (resolve_tac [notI RS not_lt_imp_le] 1);
   4.401 +by (resolve_tac [Card_cardinal RS csucc_le RS lt_trans1 RS lt_irrefl] 1);
   4.402 +by (assume_tac 1);
   4.403 +by (resolve_tac [Ord_cardinal_le RS lt_trans1] 1);
   4.404 +by (REPEAT (ares_tac [Ord_cardinal] 1
   4.405 +     ORELSE eresolve_tac [ltE, Card_is_Ord] 1));
   4.406 +val lt_csucc_iff = result();
   4.407 +
   4.408 +goal CardinalArith.thy
   4.409 +    "!!K' K. [| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K";
   4.410 +by (asm_simp_tac 
   4.411 +    (ZF_ss addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1);
   4.412 +val Card_lt_csucc_iff = result();
     5.1 --- a/src/ZF/CardinalArith.thy	Thu Jul 21 16:51:26 1994 +0200
     5.2 +++ b/src/ZF/CardinalArith.thy	Tue Jul 26 13:21:20 1994 +0200
     5.3 @@ -6,22 +6,18 @@
     5.4  Cardinal Arithmetic
     5.5  *)
     5.6  
     5.7 -CardinalArith = Cardinal + OrderArith + Arith + 
     5.8 +CardinalArith = Cardinal + OrderArith + Arith + Fin + 
     5.9  consts
    5.10 -  jump_cardinal :: "i=>i"
    5.11  
    5.12    InfCard     :: "i=>o"
    5.13    "|*|"       :: "[i,i]=>i"       (infixl 70)
    5.14    "|+|"       :: "[i,i]=>i"       (infixl 65)
    5.15    csquare_rel :: "i=>i"
    5.16 +  jump_cardinal :: "i=>i"
    5.17 +  csucc       :: "i=>i"
    5.18  
    5.19  rules
    5.20  
    5.21 -  jump_cardinal_def
    5.22 -      "jump_cardinal(K) ==   \
    5.23 -\         UN X:Pow(K). {z. r: Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}"
    5.24 -
    5.25 -
    5.26    InfCard_def  "InfCard(i) == Card(i) & nat le i"
    5.27  
    5.28    cadd_def     "i |+| j == | i+j |"
    5.29 @@ -33,4 +29,13 @@
    5.30  \                            rmult(k,Memrel(k), k*k, 	\
    5.31  \                                  rmult(k,Memrel(k), k,Memrel(k))))"
    5.32  
    5.33 +  (*This def is more complex than Kunen's but it more easily proved to
    5.34 +    be a cardinal*)
    5.35 +  jump_cardinal_def
    5.36 +      "jump_cardinal(K) ==   \
    5.37 +\         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
    5.38 +
    5.39 +  (*needed because jump_cardinal(K) might not be the successor of K*)
    5.40 +  csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
    5.41 +
    5.42  end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/ZF/Cardinal_AC.ML	Tue Jul 26 13:21:20 1994 +0200
     6.3 @@ -0,0 +1,125 @@
     6.4 +(*  Title: 	ZF/Cardinal_AC.ML
     6.5 +    ID:         $Id$
     6.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1994  University of Cambridge
     6.8 +
     6.9 +Cardinal arithmetic WITH the Axiom of Choice
    6.10 +*)
    6.11 +
    6.12 +open Cardinal_AC;
    6.13 +
    6.14 +(*** Strengthened versions of existing theorems about cardinals ***)
    6.15 +
    6.16 +goal Cardinal_AC.thy "|A| eqpoll A";
    6.17 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.18 +by (eresolve_tac [well_ord_cardinal_eqpoll] 1);
    6.19 +val cardinal_eqpoll = result();
    6.20 +
    6.21 +val cardinal_idem = cardinal_eqpoll RS cardinal_cong;
    6.22 +
    6.23 +goal Cardinal_AC.thy "!!X Y. |X| = |Y| ==> X eqpoll Y";
    6.24 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.25 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.26 +by (resolve_tac [well_ord_cardinal_eqE] 1);
    6.27 +by (REPEAT_SOME assume_tac);
    6.28 +val cardinal_eqE = result();
    6.29 +
    6.30 +goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";
    6.31 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.32 +by (eresolve_tac [well_ord_lepoll_imp_le] 1);
    6.33 +by (assume_tac 1);
    6.34 +val lepoll_imp_le = result();
    6.35 +
    6.36 +goal Cardinal_AC.thy "(i |+| j) |+| k = i |+| (j |+| k)";
    6.37 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.38 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.39 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.40 +by (resolve_tac [well_ord_cadd_assoc] 1);
    6.41 +by (REPEAT_SOME assume_tac);
    6.42 +val cadd_assoc = result();
    6.43 +
    6.44 +goal Cardinal_AC.thy "(i |*| j) |*| k = i |*| (j |*| k)";
    6.45 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.46 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.47 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.48 +by (resolve_tac [well_ord_cmult_assoc] 1);
    6.49 +by (REPEAT_SOME assume_tac);
    6.50 +val cmult_assoc = result();
    6.51 +
    6.52 +goal Cardinal_AC.thy "!!A. InfCard(|A|) ==> A*A eqpoll A";
    6.53 +by (resolve_tac [AC_well_ord RS exE] 1);
    6.54 +by (eresolve_tac [well_ord_InfCard_square_eq] 1);
    6.55 +by (assume_tac 1);
    6.56 +val InfCard_square_eq = result();
    6.57 +
    6.58 +
    6.59 +(*** Other applications of AC ***)
    6.60 +
    6.61 +goal Cardinal_AC.thy "!!A B. |A| le |B| ==> A lepoll B";
    6.62 +by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS 
    6.63 +		 lepoll_trans] 1);
    6.64 +by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1);
    6.65 +by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1);
    6.66 +val le_imp_lepoll = result();
    6.67 +
    6.68 +goal Cardinal_AC.thy "!!A K. Card(K) ==> |A| le K <-> A lepoll K";
    6.69 +by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN
    6.70 +    rtac iffI 1 THEN
    6.71 +    DEPTH_SOLVE (eresolve_tac [le_imp_lepoll,lepoll_imp_le] 1));
    6.72 +val le_Card_iff = result();
    6.73 +
    6.74 +goalw Cardinal_AC.thy [surj_def] "!!f. f: surj(X,Y) ==> EX g. g: inj(Y,X)";
    6.75 +by (etac CollectE 1);
    6.76 +by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1);
    6.77 +by (fast_tac (ZF_cs addSEs [apply_Pair]) 1);
    6.78 +by (resolve_tac [exI] 1);
    6.79 +by (rtac f_imp_injective 1);
    6.80 +by (resolve_tac [Pi_type] 1 THEN assume_tac 1);
    6.81 +by (fast_tac (ZF_cs addDs [apply_type] addEs [memberPiE]) 1);
    6.82 +by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1);
    6.83 +val surj_implies_inj = result();
    6.84 +
    6.85 +(*Kunen's Lemma 10.20*)
    6.86 +goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> |Y| le |X|";
    6.87 +by (resolve_tac [lepoll_imp_le] 1);
    6.88 +by (eresolve_tac [surj_implies_inj RS exE] 1);
    6.89 +by (rewtac lepoll_def);
    6.90 +by (eresolve_tac [exI] 1);
    6.91 +val surj_implies_cardinal_le = result();
    6.92 +
    6.93 +(*Kunen's Lemma 10.21*)
    6.94 +goal Cardinal_AC.thy
    6.95 +    "!!K. [| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K";
    6.96 +by (asm_full_simp_tac (ZF_ss addsimps [InfCard_is_Card, le_Card_iff]) 1);
    6.97 +by (resolve_tac [lepoll_trans] 1);
    6.98 +by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2);
    6.99 +by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2);
   6.100 +by (rewrite_goals_tac [lepoll_def]);
   6.101 +by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
   6.102 +by (etac (AC_ball_Pi RS exE) 1);
   6.103 +by (resolve_tac [exI] 1);
   6.104 +(*Lemma needed in both subgoals, for a fixed z*)
   6.105 +by (subgoal_tac
   6.106 +    "ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);
   6.107 +by (fast_tac (ZF_cs addSIs [Least_le RS lt_trans1 RS ltD, ltI]
   6.108 +                    addSEs [LeastI, Ord_in_Ord]) 2);
   6.109 +by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
   6.110 +		  ("d", "split(%i j. converse(f`i) ` j)")] 
   6.111 +	lam_injective 1);
   6.112 +(*Instantiate the lemma proved above*)
   6.113 +by (ALLGOALS ball_tac);
   6.114 +by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type]
   6.115 +                    addDs [apply_type]) 1);
   6.116 +by (dresolve_tac [apply_type] 1);
   6.117 +by (eresolve_tac [conjunct2] 1);
   6.118 +by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
   6.119 +val cardinal_UN_le = result();
   6.120 +
   6.121 +
   6.122 +goal Cardinal_AC.thy
   6.123 +    "!!K. [| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |] ==> \
   6.124 +\         |UN i:K. X(i)| < csucc(K)";
   6.125 +by (asm_full_simp_tac 
   6.126 +    (ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 
   6.127 +		     InfCard_is_Card, Card_cardinal]) 1);
   6.128 +val cardinal_UN_lt_csucc = result();
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/Cardinal_AC.thy	Tue Jul 26 13:21:20 1994 +0200
     7.3 @@ -0,0 +1,9 @@
     7.4 +(*  Title: 	ZF/Cardinal_AC.thy
     7.5 +    ID:         $Id$
     7.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   1994  University of Cambridge
     7.8 +
     7.9 +Cardinal Arithmetic WITH the Axiom of Choice
    7.10 +*)
    7.11 +
    7.12 +Cardinal_AC = CardinalArith + Zorn
     8.1 --- a/src/ZF/Fin.ML	Thu Jul 21 16:51:26 1994 +0200
     8.2 +++ b/src/ZF/Fin.ML	Tue Jul 26 13:21:20 1994 +0200
     8.3 @@ -1,18 +1,13 @@
     8.4  (*  Title: 	ZF/ex/Fin.ML
     8.5      ID:         $Id$
     8.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1993  University of Cambridge
     8.8 +    Copyright   1994  University of Cambridge
     8.9  
    8.10  Finite powerset operator
    8.11  
    8.12 -prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n)
    8.13 -	card(0)=0
    8.14 -	[| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b))
    8.15 +prove X:Fin(A) ==> |X| < nat
    8.16  
    8.17 -b: Fin(A) ==> inj(b,b)<=surj(b,b)
    8.18 -
    8.19 -Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j))
    8.20 -Fin(univ(A)) <= univ(A)
    8.21 +prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
    8.22  *)
    8.23  
    8.24  structure Fin = Inductive_Fun
    8.25 @@ -101,3 +96,11 @@
    8.26  by (rtac (Fin_0_induct_lemma RS mp) 1);
    8.27  by (REPEAT (ares_tac (subset_refl::prems) 1));
    8.28  val Fin_0_induct = result();
    8.29 +
    8.30 +(*Functions from a finite ordinal*)
    8.31 +val prems = goal Fin.thy "n: nat ==> n->A <= Fin(nat*A)";
    8.32 +by (nat_ind_tac "n" prems 1);
    8.33 +by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin_0I, subset_iff, cons_iff]) 1);
    8.34 +by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
    8.35 +by (fast_tac (ZF_cs addSIs [Fin_consI]) 1);
    8.36 +val nat_fun_subset_Fin = result();
     9.1 --- a/src/ZF/Fin.thy	Thu Jul 21 16:51:26 1994 +0200
     9.2 +++ b/src/ZF/Fin.thy	Tue Jul 26 13:21:20 1994 +0200
     9.3 @@ -1,3 +1,3 @@
     9.4  (*Dummy theory to document dependencies *)
     9.5  
     9.6 -Fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
     9.7 +Fin = Arith + "inductive" + "equalities"
    10.1 --- a/src/ZF/Fixedpt.ML	Thu Jul 21 16:51:26 1994 +0200
    10.2 +++ b/src/ZF/Fixedpt.ML	Tue Jul 26 13:21:20 1994 +0200
    10.3 @@ -74,7 +74,7 @@
    10.4  val subset0_cs = FOL_cs
    10.5    addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]
    10.6    addIs [bexI, UnionI, ReplaceI, RepFunI]
    10.7 -  addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE,
    10.8 +  addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE,
    10.9  	  CollectE, emptyE]
   10.10    addEs [rev_ballE, InterD, make_elim InterD, subsetD];
   10.11  
    11.1 --- a/src/ZF/List.ML	Thu Jul 21 16:51:26 1994 +0200
    11.2 +++ b/src/ZF/List.ML	Tue Jul 26 13:21:20 1994 +0200
    11.3 @@ -10,8 +10,8 @@
    11.4   (val thy        = Univ.thy
    11.5    val thy_name   = "List"
    11.6    val rec_specs  = [("list", "univ(A)",
    11.7 -                      [(["Nil"],    "i", NoSyn), 
    11.8 -                       (["Cons"],   "[i,i]=>i", NoSyn)])]
    11.9 +                      [(["Nil"],    "i", 	NoSyn), 
   11.10 +                       (["Cons"],   "[i,i]=>i",	NoSyn)])]
   11.11    val rec_styp   = "i=>i"
   11.12    val sintrs     = ["Nil : list(A)",
   11.13                      "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
    12.1 --- a/src/ZF/Makefile	Thu Jul 21 16:51:26 1994 +0200
    12.2 +++ b/src/ZF/Makefile	Tue Jul 26 13:21:20 1994 +0200
    12.3 @@ -19,17 +19,18 @@
    12.4  BIN = $(ISABELLEBIN)
    12.5  COMP = $(ISABELLECOMP)
    12.6  FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \
    12.7 -	func.ML simpdata.ML Bool.thy Bool.ML \
    12.8 +	func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \
    12.9  	Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
   12.10  	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
   12.11  	equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
   12.12  	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
   12.13  	OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \
   12.14  	Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
   12.15 -	Nat.thy Nat.ML \
   12.16 +	Cardinal_AC.thy Cardinal_AC.ML \
   12.17 +	Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \
   12.18  	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
   12.19  	QUniv.thy QUniv.ML constructor.ML Datatype.ML  \
   12.20 -	Fin.ML List.ML ListFn.thy ListFn.ML
   12.21 +	List.ML ListFn.thy ListFn.ML
   12.22  
   12.23  IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\
   12.24              IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
   12.25 @@ -44,8 +45,9 @@
   12.26  	   ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\
   12.27  	   ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\
   12.28  	   ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\
   12.29 -	   ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy ex/TF.ML\
   12.30 -	   ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
   12.31 +	   ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \
   12.32 +	   ex/Ntree.ML ex/Ntree.thy \
   12.33 +	   ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
   12.34  
   12.35  #Uses cp rather than make_database because Poly/ML allows only 3 levels
   12.36  $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
    13.1 --- a/src/ZF/Nat.ML	Thu Jul 21 16:51:26 1994 +0200
    13.2 +++ b/src/ZF/Nat.ML	Tue Jul 26 13:21:20 1994 +0200
    13.3 @@ -95,6 +95,15 @@
    13.4  by (etac ltD 1);
    13.5  val Limit_nat = result();
    13.6  
    13.7 +goal Nat.thy "!!i. Limit(i) ==> nat le i";
    13.8 +by (resolve_tac [subset_imp_le] 1);
    13.9 +by (rtac subsetI 1);
   13.10 +by (eresolve_tac [nat_induct] 1);
   13.11 +by (fast_tac (ZF_cs addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
   13.12 +by (REPEAT (ares_tac [Limit_has_0 RS ltD,
   13.13 +		      Ord_nat, Limit_is_Ord] 1));
   13.14 +val nat_le_Limit = result();
   13.15 +
   13.16  (* succ(i): nat ==> i: nat *)
   13.17  val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;
   13.18  
    14.1 --- a/src/ZF/Order.ML	Thu Jul 21 16:51:26 1994 +0200
    14.2 +++ b/src/ZF/Order.ML	Tue Jul 26 13:21:20 1994 +0200
    14.3 @@ -25,6 +25,31 @@
    14.4  by (fast_tac ZF_cs 1);
    14.5  val part_ord_Imp_asym = result();
    14.6  
    14.7 +(** Subset properties for the various forms of relation **)
    14.8 +
    14.9 +
   14.10 +(*Note: a relation s such that s<=r need not be a partial ordering*)
   14.11 +goalw Order.thy [part_ord_def, irrefl_def, trans_on_def]
   14.12 +    "!!A B r. [| part_ord(A,r);  B<=A |] ==> part_ord(B,r)";
   14.13 +by (fast_tac ZF_cs 1);
   14.14 +val part_ord_subset = result();
   14.15 +
   14.16 +goalw Order.thy [linear_def]
   14.17 +    "!!A B r. [| linear(A,r);  B<=A |] ==> linear(B,r)";
   14.18 +by (fast_tac ZF_cs 1);
   14.19 +val linear_subset = result();
   14.20 +
   14.21 +goalw Order.thy [tot_ord_def]
   14.22 +    "!!A B r. [| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)";
   14.23 +by (fast_tac (ZF_cs addSEs [part_ord_subset, linear_subset]) 1);
   14.24 +val tot_ord_subset = result();
   14.25 +
   14.26 +goalw Order.thy [well_ord_def]
   14.27 +    "!!A B r. [| well_ord(A,r);  B<=A |] ==> well_ord(B,r)";
   14.28 +by (fast_tac (ZF_cs addSEs [tot_ord_subset, wf_on_subset_A]) 1);
   14.29 +val well_ord_subset = result();
   14.30 +
   14.31 +
   14.32  (** Order-isomorphisms **)
   14.33  
   14.34  goalw Order.thy [ord_iso_def] 
   14.35 @@ -169,7 +194,6 @@
   14.36  by (safe_tac ZF_cs);
   14.37  val well_ord_is_trans_on = result();
   14.38  
   14.39 -
   14.40  (*** Derived rules for pred(A,x,r) ***)
   14.41  
   14.42  val [major,minor] = goalw Order.thy [pred_def]
    15.1 --- a/src/ZF/Perm.ML	Thu Jul 21 16:51:26 1994 +0200
    15.2 +++ b/src/ZF/Perm.ML	Tue Jul 26 13:21:20 1994 +0200
    15.3 @@ -39,7 +39,25 @@
    15.4  by (fast_tac ZF_cs 1);
    15.5  val inj_equality = result();
    15.6  
    15.7 -(** Bijections -- simple lemmas but no intro/elim rules -- use unfolding **)
    15.8 +(** A function with a left inverse is an injection **)
    15.9 +
   15.10 +val prems = goal Perm.thy
   15.11 +    "[| f: A->B;  !!x. x:A ==> d(f`x)=x |] ==> f: inj(A,B)";
   15.12 +by (asm_simp_tac (ZF_ss addsimps ([inj_def] @ prems)) 1);
   15.13 +by (safe_tac ZF_cs);
   15.14 +by (eresolve_tac [subst_context RS box_equals] 1);
   15.15 +by (REPEAT (ares_tac prems 1));
   15.16 +val f_imp_injective = result();
   15.17 +
   15.18 +val prems = goal Perm.thy
   15.19 +    "[| !!x. x:A ==> c(x): B;		\
   15.20 +\       !!x. x:A ==> d(c(x)) = x      	\
   15.21 +\    |] ==> (lam x:A.c(x)) : inj(A,B)";
   15.22 +by (res_inst_tac [("d", "d")] f_imp_injective 1);
   15.23 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([lam_type]@prems)) ));
   15.24 +val lam_injective = result();
   15.25 +
   15.26 +(** Bijections **)
   15.27  
   15.28  goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: inj(A,B)";
   15.29  by (etac IntD1 1);
   15.30 @@ -347,9 +365,8 @@
   15.31  \    |] ==> (lam x:A.c(x)) : bij(A,B)";
   15.32  by (simp_tac (ZF_ss addsimps ([lam_type]@prems)) 1);
   15.33  by (safe_tac ZF_cs);
   15.34 -(*Apply d to both sides then simplify (type constraint is essential) *)
   15.35 -by (dres_inst_tac [("t", "d::i=>i")] subst_context 1);
   15.36 -by (asm_full_simp_tac (ZF_ss addsimps prems) 1);
   15.37 +by (eresolve_tac [subst_context RS box_equals] 1);
   15.38 +by (REPEAT (ares_tac prems 1));
   15.39  by (fast_tac (ZF_cs addIs prems) 1);
   15.40  val lam_bijective = result();
   15.41  
    16.1 --- a/src/ZF/ROOT.ML	Thu Jul 21 16:51:26 1994 +0200
    16.2 +++ b/src/ZF/ROOT.ML	Tue Jul 26 13:21:20 1994 +0200
    16.3 @@ -28,8 +28,7 @@
    16.4  
    16.5  print_depth 1;
    16.6  
    16.7 -use_thy "CardinalArith";
    16.8 -use_thy "Fin";
    16.9 +use_thy "Cardinal_AC";
   16.10  use_thy "ListFn";
   16.11  
   16.12  (*printing functions are inherited from FOL*)
    17.1 --- a/src/ZF/Univ.ML	Thu Jul 21 16:51:26 1994 +0200
    17.2 +++ b/src/ZF/Univ.ML	Tue Jul 26 13:21:20 1994 +0200
    17.3 @@ -200,12 +200,14 @@
    17.4  by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
    17.5  val Limit_VfromE = result();
    17.6  
    17.7 +val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom;
    17.8 +
    17.9  val [major,limiti] = goal Univ.thy
   17.10      "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
   17.11  by (rtac ([major,limiti] MRS Limit_VfromE) 1);
   17.12  by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
   17.13  by (etac (limiti RS Limit_has_succ) 1);
   17.14 -val singleton_in_Vfrom_limit = result();
   17.15 +val singleton_in_Vfrom_Limit = result();
   17.16  
   17.17  val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
   17.18  and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
   17.19 @@ -220,7 +222,7 @@
   17.20  by (etac Vfrom_UnI1 1);
   17.21  by (etac Vfrom_UnI2 1);
   17.22  by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
   17.23 -val doubleton_in_Vfrom_limit = result();
   17.24 +val doubleton_in_Vfrom_Limit = result();
   17.25  
   17.26  val [aprem,bprem,limiti] = goal Univ.thy
   17.27      "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   17.28 @@ -233,7 +235,82 @@
   17.29  by (etac Vfrom_UnI1 1);
   17.30  by (etac Vfrom_UnI2 1);
   17.31  by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
   17.32 -val Pair_in_Vfrom_limit = result();
   17.33 +val Pair_in_Vfrom_Limit = result();
   17.34 +
   17.35 +goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
   17.36 +by (REPEAT (ares_tac [subsetI,Pair_in_Vfrom_Limit] 1
   17.37 +     ORELSE eresolve_tac [SigmaE, ssubst] 1));
   17.38 +val product_Vfrom_Limit = result();
   17.39 +
   17.40 +val Sigma_subset_Vfrom_Limit = 
   17.41 +    [Sigma_mono, product_Vfrom_Limit] MRS subset_trans |> standard;
   17.42 +
   17.43 +val nat_subset_Vfrom_Limit = 
   17.44 +    [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans 
   17.45 +	|> standard;
   17.46 +
   17.47 +val nat_into_Vfrom_Limit = standard (nat_subset_Vfrom_Limit RS subsetD);
   17.48 +
   17.49 +(** Closure under disjoint union **)
   17.50 +
   17.51 +val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard;
   17.52 +
   17.53 +goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
   17.54 +by (REPEAT (ares_tac [nat_into_Vfrom_Limit, nat_0I, nat_succI] 1));
   17.55 +val one_in_Vfrom_Limit = result();
   17.56 +
   17.57 +goalw Univ.thy [Inl_def]
   17.58 +    "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
   17.59 +by (REPEAT (ares_tac [zero_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1));
   17.60 +val Inl_in_Vfrom_Limit = result();
   17.61 +
   17.62 +goalw Univ.thy [Inr_def]
   17.63 +    "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
   17.64 +by (REPEAT (ares_tac [one_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1));
   17.65 +val Inr_in_Vfrom_Limit = result();
   17.66 +
   17.67 +goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
   17.68 +by (fast_tac (sum_cs addSIs [Inl_in_Vfrom_Limit, Inr_in_Vfrom_Limit]) 1);
   17.69 +val sum_Vfrom_Limit = result();
   17.70 +
   17.71 +val sum_subset_Vfrom_Limit = 
   17.72 +    [sum_mono, sum_Vfrom_Limit] MRS subset_trans |> standard;
   17.73 +
   17.74 +
   17.75 +(** Closure under finite powerset **)
   17.76 +
   17.77 +goal Univ.thy
   17.78 +   "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
   17.79 +by (eresolve_tac [Fin_induct] 1);
   17.80 +by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
   17.81 +by (safe_tac ZF_cs);
   17.82 +by (eresolve_tac [Limit_VfromE] 1);
   17.83 +by (assume_tac 1);
   17.84 +by (res_inst_tac [("x", "xa Un j")] exI 1);
   17.85 +by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
   17.86 +			   Un_least_lt]) 1);
   17.87 +val Fin_Vfrom_lemma = result();
   17.88 +
   17.89 +goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
   17.90 +by (rtac subsetI 1);
   17.91 +by (dresolve_tac [Fin_Vfrom_lemma] 1);
   17.92 +by (safe_tac ZF_cs);
   17.93 +by (resolve_tac [Vfrom RS ssubst] 1);
   17.94 +by (fast_tac (ZF_cs addSDs [ltD]) 1);
   17.95 +val Fin_Vfrom_Limit = result();
   17.96 +
   17.97 +val Fin_subset_Vfrom_Limit = 
   17.98 +    [Fin_mono, Fin_Vfrom_Limit] MRS subset_trans |> standard;
   17.99 +
  17.100 +goal Univ.thy "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
  17.101 +by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
  17.102 +by (REPEAT (ares_tac [Fin_subset_Vfrom_Limit, Sigma_subset_Vfrom_Limit,
  17.103 +		      nat_subset_Vfrom_Limit, subset_refl] 1));
  17.104 +val nat_fun_Vfrom_Limit = result();
  17.105 +
  17.106 +val nat_fun_subset_Vfrom_Limit = 
  17.107 +    [Pi_mono, nat_fun_Vfrom_Limit] MRS subset_trans |> standard;
  17.108 +
  17.109  
  17.110  
  17.111  (*** Properties assuming Transset(A) ***)
  17.112 @@ -263,8 +340,8 @@
  17.113  \          <a,b> : Vfrom(A,i)";
  17.114  by (etac (Transset_Pair_subset RS conjE) 1);
  17.115  by (etac Transset_Vfrom 1);
  17.116 -by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
  17.117 -val Transset_Pair_subset_Vfrom_limit = result();
  17.118 +by (REPEAT (ares_tac [Pair_in_Vfrom_Limit] 1));
  17.119 +val Transset_Pair_subset_Vfrom_Limit = result();
  17.120  
  17.121  
  17.122  (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
  17.123 @@ -287,7 +364,7 @@
  17.124  by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
  17.125  by (rtac (succI1 RS UnI2) 2);
  17.126  by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
  17.127 -val in_Vfrom_limit = result();
  17.128 +val in_Vfrom_Limit = result();
  17.129  
  17.130  (** products **)
  17.131  
  17.132 @@ -303,10 +380,10 @@
  17.133  val [aprem,bprem,limiti,transset] = goal Univ.thy
  17.134    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
  17.135  \  a*b : Vfrom(A,i)";
  17.136 -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1);
  17.137 +by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
  17.138  by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
  17.139  		      limiti RS Limit_has_succ] 1));
  17.140 -val prod_in_Vfrom_limit = result();
  17.141 +val prod_in_Vfrom_Limit = result();
  17.142  
  17.143  (** Disjoint sums, aka Quine ordered pairs **)
  17.144  
  17.145 @@ -323,10 +400,10 @@
  17.146  val [aprem,bprem,limiti,transset] = goal Univ.thy
  17.147    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
  17.148  \  a+b : Vfrom(A,i)";
  17.149 -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1);
  17.150 +by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
  17.151  by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
  17.152  		      limiti RS Limit_has_succ] 1));
  17.153 -val sum_in_Vfrom_limit = result();
  17.154 +val sum_in_Vfrom_Limit = result();
  17.155  
  17.156  (** function space! **)
  17.157  
  17.158 @@ -348,10 +425,10 @@
  17.159  val [aprem,bprem,limiti,transset] = goal Univ.thy
  17.160    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
  17.161  \  a->b : Vfrom(A,i)";
  17.162 -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1);
  17.163 +by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
  17.164  by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
  17.165  		      limiti RS Limit_has_succ] 1));
  17.166 -val fun_in_Vfrom_limit = result();
  17.167 +val fun_in_Vfrom_Limit = result();
  17.168  
  17.169  
  17.170  (*** The set Vset(i) ***)
  17.171 @@ -513,33 +590,29 @@
  17.172  (** Closure under unordered and ordered pairs **)
  17.173  
  17.174  goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
  17.175 -by (rtac singleton_in_Vfrom_limit 1);
  17.176 -by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
  17.177 +by (REPEAT (ares_tac [singleton_in_Vfrom_Limit, Limit_nat] 1));
  17.178  val singleton_in_univ = result();
  17.179  
  17.180  goalw Univ.thy [univ_def] 
  17.181      "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
  17.182 -by (rtac doubleton_in_Vfrom_limit 1);
  17.183 -by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
  17.184 +by (REPEAT (ares_tac [doubleton_in_Vfrom_Limit, Limit_nat] 1));
  17.185  val doubleton_in_univ = result();
  17.186  
  17.187  goalw Univ.thy [univ_def]
  17.188      "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
  17.189 -by (rtac Pair_in_Vfrom_limit 1);
  17.190 -by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
  17.191 +by (REPEAT (ares_tac [Pair_in_Vfrom_Limit, Limit_nat] 1));
  17.192  val Pair_in_univ = result();
  17.193  
  17.194 -goal Univ.thy "univ(A)*univ(A) <= univ(A)";
  17.195 -by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1
  17.196 -     ORELSE eresolve_tac [SigmaE, ssubst] 1));
  17.197 +goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)";
  17.198 +by (rtac (Limit_nat RS product_Vfrom_Limit) 1);
  17.199  val product_univ = result();
  17.200  
  17.201 -val Sigma_subset_univ = standard
  17.202 -    (Sigma_mono RS (product_univ RSN (2,subset_trans)));
  17.203 +val Sigma_subset_univ = 
  17.204 +    [Sigma_mono, product_univ] MRS subset_trans |> standard;
  17.205  
  17.206  goalw Univ.thy [univ_def]
  17.207      "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
  17.208 -by (etac Transset_Pair_subset_Vfrom_limit 1);
  17.209 +by (etac Transset_Pair_subset_Vfrom_Limit 1);
  17.210  by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
  17.211  val Transset_Pair_subset_univ = result();
  17.212  
  17.213 @@ -555,8 +628,8 @@
  17.214  
  17.215  (** instances for 1 and 2 **)
  17.216  
  17.217 -goal Univ.thy "1 : univ(A)";
  17.218 -by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
  17.219 +goalw Univ.thy [univ_def] "1 : univ(A)";
  17.220 +by (rtac (Limit_nat RS one_in_Vfrom_Limit) 1);
  17.221  val one_in_univ = result();
  17.222  
  17.223  (*unused!*)
  17.224 @@ -573,25 +646,39 @@
  17.225  
  17.226  (** Closure under disjoint union **)
  17.227  
  17.228 -goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
  17.229 -by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1));
  17.230 +goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
  17.231 +by (etac (Limit_nat RSN (2,Inl_in_Vfrom_Limit)) 1);
  17.232  val Inl_in_univ = result();
  17.233  
  17.234 -goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
  17.235 -by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1));
  17.236 +goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
  17.237 +by (etac (Limit_nat RSN (2,Inr_in_Vfrom_Limit)) 1);
  17.238  val Inr_in_univ = result();
  17.239  
  17.240 -goal Univ.thy "univ(C)+univ(C) <= univ(C)";
  17.241 -by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1
  17.242 -     ORELSE eresolve_tac [sumE, ssubst] 1));
  17.243 +goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)";
  17.244 +by (rtac (Limit_nat RS sum_Vfrom_Limit) 1);
  17.245  val sum_univ = result();
  17.246  
  17.247 -val sum_subset_univ = standard
  17.248 -    (sum_mono RS (sum_univ RSN (2,subset_trans)));
  17.249 +val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard;
  17.250 +
  17.251 +
  17.252 +(** Closure under finite powerset **)
  17.253 +
  17.254 +goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";
  17.255 +by (rtac (Limit_nat RS Fin_Vfrom_Limit) 1);
  17.256 +val Fin_univ = result();
  17.257  
  17.258 +val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
  17.259 +
  17.260 +goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
  17.261 +by (etac (Limit_nat RSN (2,nat_fun_Vfrom_Limit)) 1);
  17.262 +val nat_fun_univ = result();
  17.263 +
  17.264 +val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard;
  17.265 +
  17.266 +goal Univ.thy "!!f. [| f: n -> B;  B <= univ(A);  n : nat |] ==> f : univ(A)";
  17.267 +by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1));
  17.268 +val nat_fun_into_univ = result();
  17.269  
  17.270  (** Closure under binary union -- use Un_least **)
  17.271  (** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
  17.272  (** Closure under RepFun -- use   RepFun_subset  **)
  17.273 -
  17.274 -