1.1 --- a/src/ZF/AC/Cardinal_aux.ML Thu Aug 13 18:07:38 1998 +0200
1.2 +++ b/src/ZF/AC/Cardinal_aux.ML Thu Aug 13 18:07:56 1998 +0200
1.3 @@ -57,8 +57,7 @@
1.4 qed "Un_eqpoll_Inf_Ord";
1.5
1.6
1.7 -(*bijection is inferred!*)
1.8 -Goal "(lam u:{{y,z} . y: x}. THE y. {y,z} = u) : bij({{y,z}. y:x}, x)";
1.9 +Goal "?f : bij({{y,z}. y:x}, x)";
1.10 by (rtac RepFun_bijective 1);
1.11 by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1);
1.12 by (Blast_tac 1);
2.1 --- a/src/ZF/AC/WO2_AC16.ML Thu Aug 13 18:07:38 1998 +0200
2.2 +++ b/src/ZF/AC/WO2_AC16.ML Thu Aug 13 18:07:56 1998 +0200
2.3 @@ -601,8 +601,7 @@
2.4 (* ********************************************************************** *)
2.5
2.6
2.7 -Goalw [AC16_def]
2.8 - "!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
2.9 +Goalw [AC16_def] "[| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
2.10 by (rtac allI 1);
2.11 by (rtac impI 1);
2.12 by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1
3.1 --- a/src/ZF/AC/WO6_WO1.ML Thu Aug 13 18:07:38 1998 +0200
3.2 +++ b/src/ZF/AC/WO6_WO1.ML Thu Aug 13 18:07:56 1998 +0200
3.3 @@ -158,16 +158,16 @@
3.4 (* ********************************************************************** *)
3.5
3.6 Goalw [uu_def] "[| b<a; g<a; f`b~=0; f`g~=0; \
3.7 -\ y*y <= y; (UN b<a. f`b)=y \
3.8 -\ |] ==> EX d<a. uu(f,b,g,d) ~= 0";
3.9 +\ y*y <= y; (UN b<a. f`b)=y \
3.10 +\ |] ==> EX d<a. uu(f,b,g,d) ~= 0";
3.11 by (fast_tac (claset() addSIs [not_emptyI]
3.12 addSDs [SigmaI RSN (2, subsetD)]
3.13 addSEs [not_emptyE]) 1);
3.14 qed "ex_d_uu_not_empty";
3.15
3.16 Goal "[| b<a; g<a; f`b~=0; f`g~=0; \
3.17 -\ y*y<=y; (UN b<a. f`b)=y |] \
3.18 -\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
3.19 +\ y*y<=y; (UN b<a. f`b)=y |] \
3.20 +\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
3.21 by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1));
3.22 by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
3.23 qed "uu_not_empty";
3.24 @@ -178,8 +178,8 @@
3.25 qed "not_empty_rel_imp_domain";
3.26
3.27 Goal "[| b<a; g<a; f`b~=0; f`g~=0; \
3.28 -\ y*y <= y; (UN b<a. f`b)=y |] \
3.29 -\ ==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
3.30 +\ y*y <= y; (UN b<a. f`b)=y |] \
3.31 +\ ==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
3.32 by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1
3.33 THEN REPEAT (assume_tac 1));
3.34 by (resolve_tac [Least_le RS lt_trans1] 1
3.35 @@ -259,8 +259,7 @@
3.36 (* every value of defined function is less than or equipollent to m *)
3.37 (* ********************************************************************** *)
3.38
3.39 -Goalw [vv2_def]
3.40 - "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
3.41 +Goalw [vv2_def] "[| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
3.42 by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 1);
3.43 by (fast_tac (claset()
3.44 addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
3.45 @@ -270,8 +269,8 @@
3.46 qed "vv2_lepoll";
3.47
3.48 Goalw [ww2_def]
3.49 - "!!m. [| ALL b<a. f`b lepoll succ(m); g<a; m:nat; vv2(f,b,g,d) <= f`g \
3.50 -\ |] ==> ww2(f,b,g,d) lepoll m";
3.51 + "[| ALL b<a. f`b lepoll succ(m); g<a; m:nat; vv2(f,b,g,d) <= f`g |] \
3.52 +\ ==> ww2(f,b,g,d) lepoll m";
3.53 by (excluded_middle_tac "f`g = 0" 1);
3.54 by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2);
3.55 by (dtac ospec 1 THEN (assume_tac 1));
3.56 @@ -294,8 +293,7 @@
3.57 (* ********************************************************************** *)
3.58 (* lemma ii *)
3.59 (* ********************************************************************** *)
3.60 -Goalw [NN_def]
3.61 - "!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
3.62 +Goalw [NN_def] "[| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
3.63 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1));
3.64 by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
3.65 THEN (assume_tac 1));
3.66 @@ -332,7 +330,7 @@
3.67 qed "z_n_subset_z_succ_n";
3.68
3.69 Goal "[| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |] \
3.70 -\ ==> f(n)<=f(m)";
3.71 +\ ==> f(n)<=f(m)";
3.72 by (eres_inst_tac [("P","n le m")] rev_mp 1);
3.73 by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1);
3.74 by (REPEAT (fast_tac le_cs 1));
3.75 @@ -373,7 +371,7 @@
3.76 (* WO6 ==> NN(y) ~= 0 *)
3.77 (* ********************************************************************** *)
3.78
3.79 -Goalw [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
3.80 +Goalw [WO6_def, NN_def] "WO6 ==> NN(y) ~= 0";
3.81 by (fast_tac ZF_cs 1); (*SLOW if current claset is used*)
3.82 qed "WO6_imp_NN_not_empty";
3.83
3.84 @@ -382,12 +380,12 @@
3.85 (* ********************************************************************** *)
3.86
3.87 Goal "[| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \
3.88 -\ ==> EX c<a. f`c = {x}";
3.89 +\ ==> EX c<a. f`c = {x}";
3.90 by (fast_tac (claset() addSEs [lepoll_1_is_sing]) 1);
3.91 val lemma1 = result();
3.92
3.93 Goal "[| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \
3.94 -\ ==> f` (LEAST i. f`i = {x}) = {x}";
3.95 +\ ==> f` (LEAST i. f`i = {x}) = {x}";
3.96 by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
3.97 by (fast_tac (claset() addSEs [lt_Ord] addIs [LeastI]) 1);
3.98 val lemma2 = result();
3.99 @@ -425,10 +423,10 @@
3.100 by (fast_tac (claset() addSIs [prem2]) 1);
3.101 qed "rev_induct_lemma";
3.102
3.103 -val prems = goal thy
3.104 - "[| P(n); n:nat; n~=0; \
3.105 -\ !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
3.106 -\ ==> P(1)";
3.107 +val prems =
3.108 +Goal "[| P(n); n:nat; n~=0; \
3.109 +\ !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
3.110 +\ ==> P(1)";
3.111 by (resolve_tac [rev_induct_lemma RS impE] 1);
3.112 by (etac impE 4 THEN (assume_tac 5));
3.113 by (REPEAT (ares_tac prems 1));
3.114 @@ -450,7 +448,7 @@
3.115 (* another helpful lemma *)
3.116 Goalw [NN_def] "0:NN(y) ==> y=0";
3.117 by (fast_tac (claset() addSIs [equalityI]
3.118 - addSDs [lepoll_0_is_0] addEs [subst]) 1);
3.119 + addSDs [lepoll_0_is_0] addEs [subst]) 1);
3.120 qed "NN_y_0";
3.121
3.122 Goalw [WO1_def] "WO6 ==> WO1";