--- a/src/ZF/AC/WO6_WO1.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/WO6_WO1.ML
+(* Title: ZF/AC/WO6_WO1.ML
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
The proof of "WO6 ==> WO1". Simplified by L C Paulson.
@@ -25,11 +25,11 @@
(lt_oadd_odiff_disj RS disjE);
(* ********************************************************************** *)
-(* The most complicated part of the proof - lemma ii - p. 2-4 *)
+(* The most complicated part of the proof - lemma ii - p. 2-4 *)
(* ********************************************************************** *)
(* ********************************************************************** *)
-(* some properties of relation uu(beta, gamma, delta) - p. 2 *)
+(* some properties of relation uu(beta, gamma, delta) - p. 2 *)
(* ********************************************************************** *)
goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b";
@@ -39,7 +39,7 @@
goal thy "!! a. ALL b<a. f`b lepoll m ==> \
\ ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m";
by (fast_tac (AC_cs addSEs
- [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
+ [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
val quant_domain_uu_lepoll_m = result();
goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g";
@@ -52,24 +52,24 @@
goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
by (fast_tac (AC_cs
- addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
+ addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
val uu_lepoll_m = result();
(* ********************************************************************** *)
-(* Two cases for lemma ii *)
+(* Two cases for lemma ii *)
(* ********************************************************************** *)
goalw thy [lesspoll_def]
"!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==> \
\ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & \
-\ u(f,b,g,d) lesspoll m)) | \
+\ u(f,b,g,d) lesspoll m)) | \
\ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \
-\ u(f,b,g,d) eqpoll m))";
+\ u(f,b,g,d) eqpoll m))";
by (asm_simp_tac OrdQuant_ss 1);
by (fast_tac AC_cs 1);
val cases = result();
(* ********************************************************************** *)
-(* Lemmas used in both cases *)
+(* Lemmas used in both cases *)
(* ********************************************************************** *)
goal thy "!!a C. Ord(a) ==> (UN b<a++a. C(b)) = (UN b<a. C(b) Un C(a++b))";
by (fast_tac (AC_cs addSIs [equalityI] addIs [ltI]
@@ -79,7 +79,7 @@
(* ********************************************************************** *)
-(* Case 1 : lemmas *)
+(* Case 1 : lemmas *)
(* ********************************************************************** *)
goalw thy [vv1_def] "vv1(f,m,b) <= f`b";
@@ -89,16 +89,16 @@
val vv1_subset = result();
(* ********************************************************************** *)
-(* Case 1 : Union of images is the whole "y" *)
+(* Case 1 : Union of images is the whole "y" *)
(* ********************************************************************** *)
goalw thy [gg1_def]
- "!! a f y. [| Ord(a); m:nat |] ==> \
-\ (UN b<a++a. gg1(f,a,m)`b) = (UN b<a. f`b)";
+ "!! a f y. [| Ord(a); m:nat |] ==> \
+\ (UN b<a++a. gg1(f,a,m)`b) = (UN b<a. f`b)";
by (asm_simp_tac
(OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
- oadd_le_self RS le_imp_not_lt, lt_Ord,
- odiff_oadd_inverse, ltD,
- vv1_subset RS Diff_partition, ww1_def]) 1);
+ oadd_le_self RS le_imp_not_lt, lt_Ord,
+ odiff_oadd_inverse, ltD,
+ vv1_subset RS Diff_partition, ww1_def]) 1);
val UN_gg1_eq = result();
goal thy "domain(gg1(f,a,m)) = a++a";
@@ -106,11 +106,11 @@
val domain_gg1 = result();
(* ********************************************************************** *)
-(* every value of defined function is less than or equipollent to m *)
+(* every value of defined function is less than or equipollent to m *)
(* ********************************************************************** *)
goal thy "!!a b. [| P(a, b); Ord(a); Ord(b); \
-\ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \
-\ ==> P(Least_a, LEAST b. P(Least_a, b))";
+\ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \
+\ ==> P(Least_a, LEAST b. P(Least_a, b))";
by (etac ssubst 1);
by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1));
@@ -119,24 +119,24 @@
val nested_Least_instance =
standard
(read_instantiate
- [("P","%g d. domain(uu(f,b,g,d)) ~= 0 & \
-\ domain(uu(f,b,g,d)) lepoll m")] nested_LeastI);
+ [("P","%g d. domain(uu(f,b,g,d)) ~= 0 & \
+\ domain(uu(f,b,g,d)) lepoll m")] nested_LeastI);
goalw thy [gg1_def]
"!!a. [| Ord(a); m:nat; \
-\ ALL b<a. f`b ~=0 --> \
-\ (EX g<a. EX d<a. domain(uu(f,b,g,d)) ~= 0 & \
-\ domain(uu(f,b,g,d)) lepoll m); \
-\ ALL b<a. f`b lepoll succ(m); b<a++a \
-\ |] ==> gg1(f,a,m)`b lepoll m";
+\ ALL b<a. f`b ~=0 --> \
+\ (EX g<a. EX d<a. domain(uu(f,b,g,d)) ~= 0 & \
+\ domain(uu(f,b,g,d)) lepoll m); \
+\ ALL b<a. f`b lepoll succ(m); b<a++a \
+\ |] ==> gg1(f,a,m)`b lepoll m";
by (asm_simp_tac OrdQuant_ss 1);
by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases]));
(*Case b<a : show vv1(f,m,b) lepoll m *)
by (asm_simp_tac (ZF_ss addsimps [vv1_def, Let_def]
setloop split_tac [expand_if]) 1);
by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2]
- addSEs [lt_Ord]
- addSIs [empty_lepollI]) 1);
+ addSEs [lt_Ord]
+ addSIs [empty_lepollI]) 1);
(*Case a le b: show ww1(f,m,b--a) lepoll m *)
by (asm_simp_tac (ZF_ss addsimps [ww1_def]) 1);
by (excluded_middle_tac "f`(b--a) = 0" 1);
@@ -147,45 +147,45 @@
by (dtac (ospec RS mp) 1);
by (REPEAT (eresolve_tac [asm_rl, oexE] 1));
by (asm_simp_tac (ZF_ss
- addsimps [vv1_def, Let_def, lt_Ord,
- nested_Least_instance RS conjunct1]) 1);
+ addsimps [vv1_def, Let_def, lt_Ord,
+ nested_Least_instance RS conjunct1]) 1);
val gg1_lepoll_m = result();
(* ********************************************************************** *)
-(* Case 2 : lemmas *)
+(* Case 2 : lemmas *)
(* ********************************************************************** *)
(* ********************************************************************** *)
-(* Case 2 : vv2_subset *)
+(* Case 2 : vv2_subset *)
(* ********************************************************************** *)
-goalw thy [uu_def] "!!f. [| 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";
+goalw thy [uu_def] "!!f. [| 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";
by (fast_tac (AC_cs addSIs [not_emptyI]
- addSDs [SigmaI RSN (2, subsetD)]
- addSEs [not_emptyE]) 1);
+ addSDs [SigmaI RSN (2, subsetD)]
+ addSEs [not_emptyE]) 1);
val ex_d_uu_not_empty = result();
goal thy "!!f. [| 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 (AC_cs addSEs [LeastI, lt_Ord]) 1);
val uu_not_empty = result();
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));
+ sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
val not_empty_rel_imp_domain = result();
goal thy "!!f. [| 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));
+ THEN REPEAT (assume_tac 1));
by (resolve_tac [Least_le RS lt_trans1] 1
- THEN (REPEAT (ares_tac [lt_Ord] 1)));
+ THEN (REPEAT (ares_tac [lt_Ord] 1)));
val Least_uu_not_empty_lt_a = result();
goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
@@ -202,56 +202,56 @@
by (rtac subsetI 1);
by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2,
- Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
- succ_lepoll_natE] 1
- THEN REPEAT (assume_tac 1));
+ Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
+ succ_lepoll_natE] 1
+ THEN REPEAT (assume_tac 1));
val supset_lepoll_imp_eq = result();
goal thy
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
-\ domain(uu(f, b, g, d)) eqpoll succ(m); \
-\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
-\ (UN b<a. f`b)=y; b<a; g<a; d<a; \
-\ f`b~=0; f`g~=0; m:nat; s:f`b \
+ "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
+\ domain(uu(f, b, g, d)) eqpoll succ(m); \
+\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
+\ (UN b<a. f`b)=y; b<a; g<a; d<a; \
+\ f`b~=0; f`g~=0; m:nat; s:f`b \
\ |] ==> uu(f, b, g, LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g";
by (dres_inst_tac [("x2","g")] (ospec RS ospec RS mp) 1);
by (rtac ([uu_subset1, uu_not_empty] MRS not_empty_rel_imp_domain) 3);
by (rtac Least_uu_not_empty_lt_a 2 THEN TRYALL assume_tac);
by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS
- (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2,
- uu_subset1 RSN (4, rel_is_fun)))] 1
- THEN TRYALL assume_tac);
+ (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2,
+ uu_subset1 RSN (4, rel_is_fun)))] 1
+ THEN TRYALL assume_tac);
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1);
by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1));
val uu_Least_is_fun = result();
goalw thy [vv2_def]
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
-\ domain(uu(f, b, g, d)) eqpoll succ(m); \
-\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
-\ (UN b<a. f`b)=y; b<a; g<a; m:nat; s:f`b \
-\ |] ==> vv2(f,b,g,s) <= f`g";
+ "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
+\ domain(uu(f, b, g, d)) eqpoll succ(m); \
+\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
+\ (UN b<a. f`b)=y; b<a; g<a; m:nat; s:f`b \
+\ |] ==> vv2(f,b,g,s) <= f`g";
by (split_tac [expand_if] 1);
by (fast_tac (FOL_cs addSEs [uu_Least_is_fun]
- addSIs [empty_subsetI, not_emptyI,
- singleton_subsetI, apply_type]) 1);
+ addSIs [empty_subsetI, not_emptyI,
+ singleton_subsetI, apply_type]) 1);
val vv2_subset = result();
(* ********************************************************************** *)
-(* Case 2 : Union of images is the whole "y" *)
+(* Case 2 : Union of images is the whole "y" *)
(* ********************************************************************** *)
goalw thy [gg2_def]
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
-\ domain(uu(f,b,g,d)) eqpoll succ(m); \
-\ ALL b<a. f`b lepoll succ(m); y*y<=y; \
-\ (UN b<a.f`b)=y; Ord(a); m:nat; s:f`b; b<a \
-\ |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
+ "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
+\ domain(uu(f,b,g,d)) eqpoll succ(m); \
+\ ALL b<a. f`b lepoll succ(m); y*y<=y; \
+\ (UN b<a.f`b)=y; Ord(a); m:nat; s:f`b; b<a \
+\ |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
by (dtac sym 1);
by (asm_simp_tac
(OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
- oadd_le_self RS le_imp_not_lt, lt_Ord,
- odiff_oadd_inverse, ww2_def,
- vv2_subset RS Diff_partition]) 1);
+ oadd_le_self RS le_imp_not_lt, lt_Ord,
+ odiff_oadd_inverse, ww2_def,
+ vv2_subset RS Diff_partition]) 1);
val UN_gg2_eq = result();
goal thy "domain(gg2(f,a,b,s)) = a++a";
@@ -259,7 +259,7 @@
val domain_gg2 = result();
(* ********************************************************************** *)
-(* every value of defined function is less than or equipollent to m *)
+(* every value of defined function is less than or equipollent to m *)
(* ********************************************************************** *)
goalw thy [vv2_def]
@@ -267,28 +267,28 @@
by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]
setloop split_tac [expand_if]) 1);
by (fast_tac (AC_cs
- 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);
+ 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);
val vv2_lepoll = result();
goalw thy [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";
+\ |] ==> ww2(f,b,g,d) lepoll m";
by (excluded_middle_tac "f`g = 0" 1);
by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
by (dtac ospec 1 THEN (assume_tac 1));
by (rtac Diff_lepoll 1
- THEN (TRYALL assume_tac));
+ THEN (TRYALL assume_tac));
by (asm_simp_tac (OrdQuant_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
val ww2_lepoll = result();
goalw thy [gg2_def]
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
-\ domain(uu(f,b,g,d)) eqpoll succ(m); \
-\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
-\ (UN b<a. f`b)=y; b<a; s:f`b; m:nat; m~= 0; g<a++a \
+ "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
+\ domain(uu(f,b,g,d)) eqpoll succ(m); \
+\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
+\ (UN b<a. f`b)=y; b<a; s:f`b; m:nat; m~= 0; g<a++a \
\ |] ==> gg2(f,a,b,s) ` g lepoll m";
by (asm_simp_tac OrdQuant_ss 1);
by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases, lt_Ord2]));
@@ -297,10 +297,10 @@
val gg2_lepoll_m = result();
(* ********************************************************************** *)
-(* lemma ii *)
+(* lemma ii *)
(* ********************************************************************** *)
goalw thy [NN_def]
- "!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
+ "!!y. [| 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));
@@ -308,7 +308,7 @@
by (asm_full_simp_tac (ZF_ss addsimps [lesspoll_succ_iff]) 1);
by (res_inst_tac [("x","a++a")] exI 1);
by (fast_tac (OrdQuant_cs addSIs [Ord_oadd, domain_gg1, UN_gg1_eq,
- gg1_lepoll_m]) 1);
+ gg1_lepoll_m]) 1);
(* case 2 *)
by (REPEAT (eresolve_tac [oexE, conjE] 1));
by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1));
@@ -319,7 +319,7 @@
(*Calling fast_tac might get rid of the res_inst_tac calls, but it
is just too slow.*)
by (asm_simp_tac (OrdQuant_ss addsimps
- [Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1);
+ [Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1);
val lemma_ii = result();
@@ -344,7 +344,7 @@
val le_subsets = result();
goal thy "!!n m. [| n le m; m:nat |] ==> \
-\ rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)";
+\ rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)";
by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1
THEN (TRYALL assume_tac));
by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1
@@ -358,23 +358,23 @@
by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1));
by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD]
- addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type]
- addSEs [nat_into_Ord] addss nat_ss) 1);
+ addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type]
+ addSEs [nat_into_Ord] addss nat_ss) 1);
val lemma_iv = result();
(* ********************************************************************** *)
-(* Rubin & Rubin wrote : *)
+(* Rubin & Rubin wrote : *)
(* "It follows from (ii) and mathematical induction that if y*y <= y then *)
-(* y can be well-ordered" *)
+(* y can be well-ordered" *)
-(* In fact we have to prove : *)
-(* * WO6 ==> NN(y) ~= 0 *)
-(* * reverse induction which lets us infer that 1 : NN(y) *)
-(* * 1 : NN(y) ==> y can be well-ordered *)
+(* In fact we have to prove : *)
+(* * WO6 ==> NN(y) ~= 0 *)
+(* * reverse induction which lets us infer that 1 : NN(y) *)
+(* * 1 : NN(y) ==> y can be well-ordered *)
(* ********************************************************************** *)
(* ********************************************************************** *)
-(* WO6 ==> NN(y) ~= 0 *)
+(* WO6 ==> NN(y) ~= 0 *)
(* ********************************************************************** *)
goalw thy [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
@@ -382,16 +382,16 @@
val WO6_imp_NN_not_empty = result();
(* ********************************************************************** *)
-(* 1 : NN(y) ==> y can be well-ordered *)
+(* 1 : NN(y) ==> y can be well-ordered *)
(* ********************************************************************** *)
goal thy "!!f. [| (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 (AC_cs addSEs [lepoll_1_is_sing]) 1);
val lemma1 = result();
goal thy "!!f. [| (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 (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1);
val lemma2 = result();
@@ -415,12 +415,12 @@
val y_well_ord = result();
(* ********************************************************************** *)
-(* reverse induction which lets us infer that 1 : NN(y) *)
+(* reverse induction which lets us infer that 1 : NN(y) *)
(* ********************************************************************** *)
val [prem1, prem2] = goal thy
- "[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
-\ ==> n~=0 --> P(n) --> P(1)";
+ "[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
+\ ==> n~=0 --> P(n) --> P(1)";
by (res_inst_tac [("n","n")] nat_induct 1);
by (rtac prem1 1);
by (fast_tac ZF_cs 1);
@@ -430,9 +430,9 @@
val rev_induct_lemma = result();
val prems = goal thy
- "[| P(n); n:nat; n~=0; \
-\ !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
-\ ==> P(1)";
+ "[| 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));
@@ -448,7 +448,7 @@
val lemma3 = result();
(* ********************************************************************** *)
-(* Main theorem "WO6 ==> WO1" *)
+(* Main theorem "WO6 ==> WO1" *)
(* ********************************************************************** *)
(* another helpful lemma *)