src/ZF/AC/WO6_WO1.ML

 (* ********************************************************************** *)
 (* Case 2 : vv2_subset                                                    *)
 (* ********************************************************************** *)
 
 Goalw [uu_def] "[| b<a;  g<a;  f`b~=0;  f`g~=0;        \
-\                           y*y <= y;  (UN b<a. f`b)=y          \
-\                        |] ==> EX d<a. uu(f,b,g,d) ~= 0";
+\                  y*y <= y;  (UN b<a. f`b)=y          \
+\               |] ==> EX d<a. uu(f,b,g,d) ~= 0";
 by (fast_tac (claset() addSIs [not_emptyI] 
                     addSDs [SigmaI RSN (2, subsetD)]
                     addSEs [not_emptyE]) 1);
 qed "ex_d_uu_not_empty";
 
 Goal "[| b<a; g<a; f`b~=0; f`g~=0;  \
-\                       y*y<=y; (UN b<a. f`b)=y |]  \
-\               ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
+\        y*y<=y; (UN b<a. f`b)=y |]  \
+\     ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
 by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
 qed "uu_not_empty";
 
 goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
 by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, 
                 sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
 qed "not_empty_rel_imp_domain";
 
 Goal "[| b<a; g<a; f`b~=0; f`g~=0;  \
-\                       y*y <= y; (UN b<a. f`b)=y |]  \
-\               ==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
+\        y*y <= y; (UN b<a. f`b)=y |]  \
+\     ==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
 by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1
         THEN REPEAT (assume_tac 1));
 by (resolve_tac [Least_le RS lt_trans1] 1
         THEN (REPEAT (ares_tac [lt_Ord] 1)));
 qed "Least_uu_not_empty_lt_a";

 
 (* ********************************************************************** *)
 (* every value of defined function is less than or equipollent to m       *)
 (* ********************************************************************** *)
 
-Goalw [vv2_def]
-    "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
+Goalw [vv2_def] "[| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
 by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 1);
 by (fast_tac (claset()
         addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
         addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
                 not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll,
                 nat_into_Ord, nat_1I]) 1);
 qed "vv2_lepoll";
 
 Goalw [ww2_def]
-    "!!m. [| ALL b<a. f`b lepoll succ(m);  g<a;  m:nat;  vv2(f,b,g,d) <= f`g  \
-\         |] ==> ww2(f,b,g,d) lepoll m";
+    "[| ALL b<a. f`b lepoll succ(m);  g<a;  m:nat;  vv2(f,b,g,d) <= f`g |] \
+\    ==> ww2(f,b,g,d) lepoll m";
 by (excluded_middle_tac "f`g = 0" 1);
 by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2);
 by (dtac ospec 1 THEN (assume_tac 1));
 by (rtac Diff_lepoll 1 THEN (TRYALL assume_tac));
 by (asm_simp_tac (simpset() addsimps [vv2_def, not_emptyI]) 1);

 qed "gg2_lepoll_m";
 
 (* ********************************************************************** *)
 (* lemma ii                                                               *)
 (* ********************************************************************** *)
-Goalw [NN_def]
-        "!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
+Goalw [NN_def] "[| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1));
 by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
     THEN (assume_tac 1));
 (* case 1 *)
 by (asm_full_simp_tac (simpset() addsimps [lesspoll_succ_iff]) 1);

 \                    rec(succ(n), x, %k r. r Un r*r)";
 by (fast_tac (claset() addIs [rec_succ RS ssubst]) 1);
 qed "z_n_subset_z_succ_n";
 
 Goal "[| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |]  \
-\              ==> f(n)<=f(m)";
+\     ==> f(n)<=f(m)";
 by (eres_inst_tac [("P","n le m")] rev_mp 1);
 by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1);
 by (REPEAT (fast_tac le_cs 1));
 qed "le_subsets";
 

 
 (* ********************************************************************** *)
 (*      WO6 ==> NN(y) ~= 0                                                *)
 (* ********************************************************************** *)
 
-Goalw [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
+Goalw [WO6_def, NN_def] "WO6 ==> NN(y) ~= 0";
 by (fast_tac ZF_cs 1);  (*SLOW if current claset is used*)
 qed "WO6_imp_NN_not_empty";
 
 (* ********************************************************************** *)
 (*      1 : NN(y) ==> y can be well-ordered                               *)
 (* ********************************************************************** *)
 
 Goal "[| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |]  \
-\               ==> EX c<a. f`c = {x}";
+\     ==> EX c<a. f`c = {x}";
 by (fast_tac (claset() addSEs [lepoll_1_is_sing]) 1);
 val lemma1 = result();
 
 Goal "[| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |]  \
-\               ==> f` (LEAST i. f`i = {x}) = {x}";
+\     ==> f` (LEAST i. f`i = {x}) = {x}";
 by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
 by (fast_tac (claset() addSEs [lt_Ord] addIs [LeastI]) 1);
 val lemma2 = result();
 
 Goalw [NN_def] "1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)";

 by (excluded_middle_tac "x=0" 1);
 by (Blast_tac 2);
 by (fast_tac (claset() addSIs [prem2]) 1);
 qed "rev_induct_lemma";
 
-val prems = goal thy
-        "[| P(n); n:nat; n~=0;  \
-\       !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
-\       ==> P(1)";
+val prems = 
+Goal    "[| P(n); n:nat; n~=0;  \
+\           !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
+\        ==> P(1)";
 by (resolve_tac [rev_induct_lemma RS impE] 1);
 by (etac impE 4 THEN (assume_tac 5));
 by (REPEAT (ares_tac prems 1));
 qed "rev_induct";
 

 (* ********************************************************************** *)
 
 (* another helpful lemma *)
 Goalw [NN_def] "0:NN(y) ==> y=0";
 by (fast_tac (claset() addSIs [equalityI] 
-                    addSDs [lepoll_0_is_0] addEs [subst]) 1);
+                       addSDs [lepoll_0_is_0] addEs [subst]) 1);
 qed "NN_y_0";
 
 Goalw [WO1_def] "WO6 ==> WO1";
 by (rtac allI 1);
 by (excluded_middle_tac "A=0" 1);