--- a/src/ZF/AC/WO6_WO1.ML Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Fri Jan 03 15:01:55 1997 +0100
@@ -16,12 +16,12 @@
by (res_inst_tac [("i","k"),("j","i")] Ord_linear2 1);
by (dtac odiff_lt_mono2 4 THEN assume_tac 4);
by (asm_full_simp_tac
- (ZF_ss addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4);
-by (safe_tac (ZF_cs addSEs [lt_Ord]));
+ (!simpset addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4);
+by (safe_tac (!claset addSEs [lt_Ord]));
val lt_oadd_odiff_disj = result();
(*The corresponding elimination rule*)
-val lt_oadd_odiff_cases = rule_by_tactic (safe_tac ZF_cs)
+val lt_oadd_odiff_cases = rule_by_tactic (safe_tac (!claset))
(lt_oadd_odiff_disj RS disjE);
(* ********************************************************************** *)
@@ -33,25 +33,25 @@
(* ********************************************************************** *)
goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
val domain_uu_subset = result();
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
+by (fast_tac (!claset addSEs
[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";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
val uu_subset1 = result();
goalw thy [uu_def] "uu(f,b,g,d) <= f`d";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
val uu_subset2 = result();
goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
-by (fast_tac (AC_cs
+by (fast_tac (!claset
addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
val uu_lepoll_m = result();
@@ -64,15 +64,15 @@
\ 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))";
-by (asm_simp_tac OrdQuant_ss 1);
-by (fast_tac AC_cs 1);
+by (Asm_simp_tac 1);
+by (Fast_tac 1);
val cases = result();
(* ********************************************************************** *)
(* 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]
+by (fast_tac (!claset addSIs [equalityI] addIs [ltI]
addSDs [lt_oadd_disj]
addSEs [lt_oadd1, oadd_lt_mono2]) 1);
val UN_oadd = result();
@@ -85,7 +85,7 @@
goalw thy [vv1_def] "vv1(f,m,b) <= f`b";
by (rtac (LetI RS LetI) 1);
by (split_tac [expand_if] 1);
-by (simp_tac (ZF_ss addsimps [domain_uu_subset]) 1);
+by (simp_tac (!simpset addsimps [domain_uu_subset]) 1);
val vv1_subset = result();
(* ********************************************************************** *)
@@ -95,14 +95,14 @@
"!! 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,
+ (!simpset 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);
val UN_gg1_eq = result();
goal thy "domain(gg1(f,a,m)) = a++a";
-by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1);
+by (simp_tac (!simpset addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1);
val domain_gg1 = result();
(* ********************************************************************** *)
@@ -113,7 +113,7 @@
\ ==> 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));
+by (REPEAT (fast_tac (!claset addSEs [LeastI]) 1));
val nested_LeastI = result();
val nested_Least_instance =
@@ -129,24 +129,24 @@
\ 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]));
+by (Asm_simp_tac 1);
+by (safe_tac (!claset 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]
+by (asm_simp_tac (!simpset addsimps [vv1_def, Let_def]
setloop split_tac [expand_if]) 1);
-by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2]
+by (fast_tac (!claset addIs [nested_Least_instance RS conjunct2]
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 (asm_simp_tac (!simpset addsimps [ww1_def]) 1);
by (excluded_middle_tac "f`(b--a) = 0" 1);
-by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
+by (asm_simp_tac (!simpset addsimps [empty_lepollI]) 2);
by (rtac Diff_lepoll 1);
-by (fast_tac AC_cs 1);
+by (Fast_tac 1);
by (rtac vv1_subset 1);
by (dtac (ospec RS mp) 1);
by (REPEAT (eresolve_tac [asm_rl, oexE] 1));
-by (asm_simp_tac (ZF_ss
+by (asm_simp_tac (!simpset
addsimps [vv1_def, Let_def, lt_Ord,
nested_Least_instance RS conjunct1]) 1);
val gg1_lepoll_m = result();
@@ -162,7 +162,7 @@
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]
+by (fast_tac (!claset addSIs [not_emptyI]
addSDs [SigmaI RSN (2, subsetD)]
addSEs [not_emptyE]) 1);
val ex_d_uu_not_empty = result();
@@ -171,10 +171,10 @@
\ 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);
+by (fast_tac (!claset addSEs [LeastI, lt_Ord]) 1);
val uu_not_empty = result();
-goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
+goal upair.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));
val not_empty_rel_imp_domain = result();
@@ -188,14 +188,14 @@
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}";
-by (fast_tac ZF_cs 1);
+goal upair.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
+by (Fast_tac 1);
val subset_Diff_sing = result();
(*Could this be proved more directly?*)
goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
by (etac natE 1);
-by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
+by (fast_tac (!claset addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
by (hyp_subst_tac 1);
by (rtac equalityI 1);
by (assume_tac 2);
@@ -222,7 +222,7 @@
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));
+by (REPEAT (fast_tac (!claset addSIs [domain_uu_subset, nat_succI]) 1));
val uu_Least_is_fun = result();
goalw thy [vv2_def]
@@ -232,9 +232,9 @@
\ (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);
+by (Step_tac 1);
+be (uu_Least_is_fun RS apply_type) 1;
+by (REPEAT_SOME (fast_tac (!claset addSIs [not_emptyI, singleton_subsetI])));
val vv2_subset = result();
(* ********************************************************************** *)
@@ -248,14 +248,14 @@
\ |] ==> (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,
+ (!simpset 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);
val UN_gg2_eq = result();
goal thy "domain(gg2(f,a,b,s)) = a++a";
-by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1);
+by (simp_tac (!simpset addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1);
val domain_gg2 = result();
(* ********************************************************************** *)
@@ -264,9 +264,9 @@
goalw thy [vv2_def]
"!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
-by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]
+by (asm_simp_tac (!simpset addsimps [empty_lepollI]
setloop split_tac [expand_if]) 1);
-by (fast_tac (AC_cs
+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,
@@ -277,11 +277,11 @@
"!!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 (OrdQuant_ss addsimps [empty_lepollI]) 2);
+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 (OrdQuant_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
+by (asm_simp_tac (!simpset addsimps [vv2_def, expand_if, not_emptyI]) 1);
val ww2_lepoll = result();
goalw thy [gg2_def]
@@ -290,10 +290,10 @@
\ 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]));
-by (asm_simp_tac (OrdQuant_ss addsimps [vv2_lepoll]) 1);
-by (asm_simp_tac (ZF_ss addsimps [ww2_lepoll, vv2_subset]) 1);
+by (Asm_simp_tac 1);
+by (safe_tac (!claset addSEs [lt_oadd_odiff_cases, lt_Ord2]));
+by (asm_simp_tac (!simpset addsimps [vv2_lepoll]) 1);
+by (asm_simp_tac (!simpset addsimps [ww2_lepoll, vv2_subset]) 1);
val gg2_lepoll_m = result();
(* ********************************************************************** *)
@@ -305,9 +305,9 @@
by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
THEN (assume_tac 1));
(* case 1 *)
-by (asm_full_simp_tac (ZF_ss addsimps [lesspoll_succ_iff]) 1);
+by (asm_full_simp_tac (!simpset 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,
+by (fast_tac (!claset addSIs [Ord_oadd, domain_gg1, UN_gg1_eq,
gg1_lepoll_m]) 1);
(* case 2 *)
by (REPEAT (eresolve_tac [oexE, conjE] 1));
@@ -318,7 +318,7 @@
by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1);
(*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
+by (asm_simp_tac (!simpset addsimps
[Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1);
val lemma_ii = result();
@@ -333,14 +333,14 @@
goal thy "ALL n:nat. rec(n, x, %k r. r Un r*r) <= \
\ rec(succ(n), x, %k r. r Un r*r)";
-by (fast_tac (ZF_cs addIs [rec_succ RS ssubst]) 1);
+by (fast_tac (!claset addIs [rec_succ RS ssubst]) 1);
val z_n_subset_z_succ_n = result();
goal thy "!!n. [| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |] \
\ ==> f(n)<=f(m)";
-by (res_inst_tac [("P","n le m")] impE 1 THEN (REPEAT (assume_tac 2)));
+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 lt_cs 1));
+by (REPEAT (fast_tac le_cs 1));
val le_subsets = result();
goal thy "!!n m. [| n le m; m:nat |] ==> \
@@ -353,13 +353,14 @@
goal thy "EX y. x Un y*y <= y";
by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
-by (safe_tac ZF_cs);
-by (fast_tac (ZF_cs addSIs [nat_0I] addss nat_ss) 1);
+by (safe_tac (!claset));
+br (nat_0I RS UN_I) 1;
+by (Asm_simp_tac 1);
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);
+ addSEs [nat_into_Ord] addss (!simpset)) 1);
val lemma_iv = result();
(* ********************************************************************** *)
@@ -387,13 +388,13 @@
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}";
-by (fast_tac (AC_cs addSEs [lepoll_1_is_sing]) 1);
+by (fast_tac (!claset 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}";
by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1);
+by (fast_tac (!claset addSEs [lt_Ord] addIs [LeastI]) 1);
val lemma2 = result();
goalw thy [NN_def] "!!y. 1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)";
@@ -404,14 +405,14 @@
by (rtac conjI 1 THEN (assume_tac 1));
by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1);
by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (AC_cs addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
+by (fast_tac (!claset addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (ZF_cs addSIs [the_equality]) 1);
+by (fast_tac (!claset addSIs [the_equality]) 1);
val NN_imp_ex_inj = result();
goal thy "!!y. [| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
by (dtac NN_imp_ex_inj 1);
-by (fast_tac (ZF_cs addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1);
+by (fast_tac (!claset addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1);
val y_well_ord = result();
(* ********************************************************************** *)
@@ -423,10 +424,10 @@
\ ==> 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);
+by (Fast_tac 1);
by (excluded_middle_tac "x=0" 1);
-by (fast_tac ZF_cs 2);
-by (fast_tac (ZF_cs addSIs [prem2]) 1);
+by (Fast_tac 2);
+by (fast_tac (!claset addSIs [prem2]) 1);
val rev_induct_lemma = result();
val prems = goal thy
@@ -453,21 +454,21 @@
(* another helpful lemma *)
goalw thy [NN_def] "!!y. 0:NN(y) ==> y=0";
-by (fast_tac (AC_cs addSIs [equalityI]
+by (fast_tac (!claset addSIs [equalityI]
addSDs [lepoll_0_is_0] addEs [subst]) 1);
val NN_y_0 = result();
goalw thy [WO1_def] "!!Z. WO6 ==> WO1";
by (rtac allI 1);
by (excluded_middle_tac "A=0" 1);
-by (fast_tac (ZF_cs addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2);
+by (fast_tac (!claset addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2);
by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1);
by (etac exE 1);
by (dtac WO6_imp_NN_not_empty 1);
by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1);
by (eres_inst_tac [("A","NN(y)")] not_emptyE 1);
by (forward_tac [y_well_ord] 1);
-by (fast_tac (ZF_cs addEs [well_ord_subset]) 2);
-by (fast_tac (ZF_cs addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1);
+by (fast_tac (!claset addEs [well_ord_subset]) 2);
+by (fast_tac (!claset addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1);
qed "WO6_imp_WO1";