--- a/src/ZF/CardinalArith.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/CardinalArith.ML Wed Apr 09 12:37:44 1997 +0200
@@ -296,8 +296,9 @@
goal CardinalArith.thy "!!m n. Card(n) ==> 2 |*| n = n |+| n";
by (asm_simp_tac
- (!simpset addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, Card_is_Ord,
- read_instantiate [("j","0")] cadd_commute, cadd_0]) 1);
+ (!simpset addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma,
+ Card_is_Ord,
+ read_instantiate [("j","0")] cadd_commute, cadd_0]) 1);
qed "cmult_2";
@@ -316,8 +317,8 @@
by (res_inst_tac [("d", "%y. if(y: range(f), \
\ nat_case(u, %z.f`z, converse(f)`y), y)")]
lam_injective 1);
-by (fast_tac (!claset addSIs [if_type, nat_0I, nat_succI, apply_type]
- addIs [inj_is_fun, inj_converse_fun]) 1);
+by (fast_tac (!claset addSIs [if_type, nat_succI, apply_type]
+ addIs [inj_is_fun, inj_converse_fun]) 1);
by (asm_simp_tac
(!simpset addsimps [inj_is_fun RS apply_rangeI,
inj_converse_fun RS apply_rangeI,
@@ -338,7 +339,7 @@
qed "nat_succ_eqpoll";
goalw CardinalArith.thy [InfCard_def] "InfCard(nat)";
-by (fast_tac (!claset addIs [Card_nat, le_refl, Card_is_Ord]) 1);
+by (blast_tac (!claset addIs [Card_nat, le_refl, Card_is_Ord]) 1);
qed "InfCard_nat";
goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)";
@@ -412,7 +413,7 @@
by (rtac (csquareD RS conjE) 1);
by (rewtac lt_def);
by (assume_tac 4);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "pred_csquare_subset";
goalw CardinalArith.thy [csquare_rel_def]
@@ -447,11 +448,11 @@
\ ordermap(K*K, csquare_rel(K)) ` <z,z>";
by (subgoals_tac ["z<K", "well_ord(K*K, csquare_rel(K))"] 1);
by (etac (Limit_is_Ord RS well_ord_csquare) 2);
-by (fast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
+by (blast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
by (rtac (csquare_ltI RS ordermap_mono RS ltI) 1);
by (etac well_ord_is_wf 4);
by (ALLGOALS
- (fast_tac (!claset addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap]
+ (blast_tac (!claset addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap]
addSEs [ltE])));
qed "ordermap_z_lt";
@@ -462,12 +463,12 @@
by (rtac (well_ord_rmult RS well_ord_lepoll_imp_Card_le) 1);
by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1));
by (subgoals_tac ["z<K"] 1);
-by (fast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
+by (blast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2);
by (rtac (ordermap_z_lt RS leI RS le_imp_lepoll RS lepoll_trans) 1);
by (REPEAT_SOME assume_tac);
by (rtac (ordermap_eqpoll_pred RS eqpoll_imp_lepoll RS lepoll_trans) 1);
by (etac (Limit_is_Ord RS well_ord_csquare) 1);
-by (fast_tac (!claset addIs [ltD]) 1);
+by (blast_tac (!claset addIs [ltD]) 1);
by (rtac (pred_csquare_subset RS subset_imp_lepoll RS lepoll_trans) 1 THEN
assume_tac 1);
by (REPEAT_FIRST (etac ltE));
@@ -601,14 +602,14 @@
goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))";
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (fast_tac (!claset addSIs [Ord_ordertype]) 2);
+by (blast_tac (!claset addSIs [Ord_ordertype]) 2);
by (rewtac Transset_def);
by (safe_tac subset_cs);
by (asm_full_simp_tac (!simpset addsimps [ordertype_pred_unfold]) 1);
by (safe_tac (!claset));
by (rtac UN_I 1);
by (rtac ReplaceI 2);
-by (ALLGOALS (fast_tac (!claset addSEs [well_ord_subset, predE])));
+by (ALLGOALS (blast_tac (!claset addIs [well_ord_subset] addSEs [predE])));
qed "Ord_jump_cardinal";
(*Allows selective unfolding. Less work than deriving intro/elim rules*)
@@ -721,15 +722,15 @@
by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1);
by (assume_tac 1);
by (resolve_tac [Fin.consI] 1);
-by (Fast_tac 1);
-by (fast_tac (!claset addIs [subset_consI RS Fin_mono RS subsetD]) 1);
+by (Blast_tac 1);
+by (blast_tac (!claset addIs [subset_consI RS Fin_mono RS subsetD]) 1);
(*Now for the lemma assumed above*)
by (rewtac eqpoll_def);
-by (best_tac (!claset addSEs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
+by (blast_tac (!claset addIs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
val lemma = result();
goalw CardinalArith.thy [Finite_def] "!!A. Finite(A) ==> A : Fin(A)";
-by (fast_tac (!claset addIs [lemma RS spec RS mp]) 1);
+by (blast_tac (!claset addIs [lemma RS spec RS mp]) 1);
qed "Finite_into_Fin";
goal CardinalArith.thy "!!A. A : Fin(U) ==> Finite(A)";
@@ -737,15 +738,15 @@
qed "Fin_into_Finite";
goal CardinalArith.thy "Finite(A) <-> A : Fin(A)";
-by (fast_tac (!claset addIs [Finite_into_Fin] addEs [Fin_into_Finite]) 1);
+by (blast_tac (!claset addIs [Finite_into_Fin, Fin_into_Finite]) 1);
qed "Finite_Fin_iff";
goal CardinalArith.thy
"!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)";
-by (fast_tac (!claset addSIs [Fin_into_Finite, Fin_UnI]
- addSDs [Finite_into_Fin]
- addSEs [Un_upper1 RS Fin_mono RS subsetD,
- Un_upper2 RS Fin_mono RS subsetD]) 1);
+by (blast_tac (!claset addSIs [Fin_into_Finite, Fin_UnI]
+ addSDs [Finite_into_Fin]
+ addIs [Un_upper1 RS Fin_mono RS subsetD,
+ Un_upper2 RS Fin_mono RS subsetD]) 1);
qed "Finite_Un";
@@ -757,8 +758,8 @@
by (simp_tac (!simpset addsimps [lepoll_0_iff]) 1);
by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1);
by (Asm_simp_tac 1);
-by (fast_tac (!claset addSDs [cons_lepoll_consD]) 1);
-by (Fast_tac 1);
+by (blast_tac (!claset addSDs [cons_lepoll_consD]) 1);
+by (Blast_tac 1);
qed "Fin_imp_not_cons_lepoll";
goal CardinalArith.thy
@@ -767,17 +768,17 @@
by (rtac Least_equality 1);
by (fold_tac [cardinal_def]);
by (simp_tac (!simpset addsimps [succ_def]) 1);
-by (fast_tac (!claset addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll]
+by (blast_tac (!claset addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll]
addSEs [mem_irrefl]
addSDs [Finite_imp_well_ord]) 1);
-by (fast_tac (!claset addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1);
+by (blast_tac (!claset addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1);
by (rtac notI 1);
by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1);
by (assume_tac 1);
by (assume_tac 1);
by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] 1);
by (eresolve_tac [le_imp_lepoll RS lepoll_trans] 1);
-by (fast_tac (!claset addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll]
+by (blast_tac (!claset addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll]
addSDs [Finite_imp_well_ord]) 1);
qed "Finite_imp_cardinal_cons";
@@ -812,7 +813,7 @@
qed "nat_sum_eqpoll_sum";
goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat";
-by (fast_tac (!claset addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))]
+by (blast_tac (!claset addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))]
addSEs [ltE]) 1);
qed "le_in_nat";
--- a/src/ZF/Order.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Order.ML Wed Apr 09 12:37:44 1997 +0200
@@ -18,7 +18,7 @@
(*needed?*)
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def]
"!!r. part_ord(A,r) ==> asym(r Int A*A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "part_ord_Imp_asym";
val major::premx::premy::prems = goalw Order.thy [linear_def]
@@ -56,14 +56,14 @@
goalw Order.thy [well_ord_def, tot_ord_def]
"!!r. well_ord(A,r) ==> linear(A,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "well_ord_is_linear";
(** Derived rules for pred(A,x,r) **)
goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "pred_iff";
bind_thm ("predI", conjI RS (pred_iff RS iffD2));
@@ -75,22 +75,22 @@
qed "predE";
goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "pred_subset_under";
goalw Order.thy [pred_def] "pred(A,x,r) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "pred_subset";
goalw Order.thy [pred_def]
"pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "pred_pred_eq";
goalw Order.thy [trans_on_def, pred_def]
"!!r. [| trans[A](r); <y,x>:r; x:A; y:A \
\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "trans_pred_pred_eq";
@@ -100,12 +100,12 @@
(*Note: a relation s such that s<=r need not be a partial ordering*)
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def]
"!!A B r. [| part_ord(A,r); B<=A |] ==> part_ord(B,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "part_ord_subset";
goalw Order.thy [linear_def]
"!!A B r. [| linear(A,r); B<=A |] ==> linear(B,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "linear_subset";
goalw Order.thy [tot_ord_def]
@@ -122,11 +122,11 @@
(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
goalw Order.thy [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "irrefl_Int_iff";
goalw Order.thy [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "trans_on_Int_iff";
goalw Order.thy [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)";
@@ -134,7 +134,7 @@
qed "part_ord_Int_iff";
goalw Order.thy [linear_def] "linear(A,r Int A*A) <-> linear(A,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "linear_Int_iff";
goalw Order.thy [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)";
@@ -142,7 +142,7 @@
qed "tot_ord_Int_iff";
goalw Order.thy [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_on_Int_iff";
goalw Order.thy [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
@@ -153,11 +153,11 @@
(** Relations over the Empty Set **)
goalw Order.thy [irrefl_def] "irrefl(0,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "irrefl_0";
goalw Order.thy [trans_on_def] "trans[0](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "trans_on_0";
goalw Order.thy [part_ord_def] "part_ord(0,r)";
@@ -165,7 +165,7 @@
qed "part_ord_0";
goalw Order.thy [linear_def] "linear(0,r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "linear_0";
goalw Order.thy [tot_ord_def] "tot_ord(0,r)";
@@ -173,7 +173,7 @@
qed "tot_ord_0";
goalw Order.thy [wf_on_def, wf_def] "wf[0](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_on_0";
goalw Order.thy [well_ord_def] "well_ord(0,r)";
@@ -206,12 +206,12 @@
"[| f: bij(A, B); \
\ !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
\ |] ==> f: ord_iso(A,r,B,s)";
-by (fast_tac (!claset addSIs prems) 1);
+by (blast_tac (!claset addSIs prems) 1);
qed "ord_isoI";
goalw Order.thy [ord_iso_def, mono_map_def]
"!!f. f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)";
-by (fast_tac (!claset addSDs [bij_is_fun]) 1);
+by (blast_tac (!claset addSDs [bij_is_fun]) 1);
qed "ord_iso_is_mono_map";
goalw Order.thy [ord_iso_def]
@@ -223,7 +223,7 @@
goalw Order.thy [ord_iso_def]
"!!f. [| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> \
\ <f`x, f`y> : s";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ord_iso_apply";
goalw Order.thy [ord_iso_def]
@@ -278,9 +278,9 @@
\ f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
by (safe_tac (!claset));
by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
-by (Fast_tac 1);
+by (Blast_tac 1);
by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
-by (fast_tac (!claset addIs [apply_type] addSEs [bspec RS bspec RS mp]) 2);
+by (blast_tac (!claset addIs [apply_funtype]) 2);
by (asm_full_simp_tac (!simpset addsimps [comp_eq_id_iff RS iffD1]) 1);
qed "mono_ord_isoI";
@@ -321,9 +321,8 @@
by (safe_tac (!claset));
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
by (safe_tac (!claset addSIs [equalityI]));
-by (dtac equalityD1 1);
-by (fast_tac (!claset addSIs [bexI]) 1);
-by (fast_tac (!claset addSIs [bexI] addIs [bij_is_fun RS apply_type]) 1);
+by (ALLGOALS (blast_tac
+ (!claset addSDs [equalityD1] addIs [bij_is_fun RS apply_type])));
qed "wf_on_ord_iso";
goalw Order.thy [well_ord_def, tot_ord_def]
@@ -344,7 +343,7 @@
by (wf_on_ind_tac "y" [] 1);
by (dres_inst_tac [("a","y1")] (bij_is_fun RS apply_type) 1);
by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "well_ord_iso_subset_lemma";
(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
@@ -371,7 +370,7 @@
by (REPEAT (*because there are two symmetric cases*)
(EVERY [eresolve_tac [pred_subset RSN (2, well_ord_subset) RS
well_ord_iso_predE] 1,
- fast_tac (!claset addSIs [predI]) 2,
+ blast_tac (!claset addSIs [predI]) 2,
asm_simp_tac (!simpset addsimps [trans_pred_pred_eq]) 1]));
qed "well_ord_iso_pred_eq";
@@ -385,7 +384,7 @@
by (rtac equalityI 1);
by (safe_tac (!claset addSEs [bij_is_fun RS apply_type]));
by (rtac RepFun_eqI 1);
-by (fast_tac (!claset addSIs [right_inverse_bij RS sym]) 1);
+by (blast_tac (!claset addSIs [right_inverse_bij RS sym]) 1);
by (asm_simp_tac bij_inverse_ss 1);
qed "ord_iso_image_pred";
@@ -422,8 +421,8 @@
by (assume_tac 1);
qed "well_ord_iso_preserving";
-val bij_apply_cs = !claset addSEs [bij_converse_bij, ord_iso_is_bij]
- addIs [bij_is_fun, apply_type];
+val bij_apply_cs = !claset addSIs [bij_converse_bij]
+ addIs [ord_iso_is_bij, bij_is_fun, apply_funtype];
(*See Halmos, page 72*)
goal Order.thy
@@ -435,7 +434,7 @@
by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
by (safe_tac (!claset));
by (forward_tac [ord_iso_converse] 1);
-by (REPEAT (fast_tac bij_apply_cs 1));
+by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
by (asm_full_simp_tac bij_inverse_ss 1);
qed "well_ord_iso_unique_lemma";
@@ -446,7 +445,7 @@
by (rtac fun_extension 1);
by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
-by (REPEAT (fast_tac bij_apply_cs 3));
+by (REPEAT (blast_tac bij_apply_cs 3));
by (dtac well_ord_ord_iso 2 THEN etac ord_iso_sym 2);
by (asm_full_simp_tac (!simpset addsimps [tot_ord_def, well_ord_def]) 2);
by (linear_case_tac 1);
@@ -456,33 +455,27 @@
(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
-goalw Order.thy [ord_iso_map_def]
- "ord_iso_map(A,r,B,s) <= A*B";
-by (Fast_tac 1);
+goalw Order.thy [ord_iso_map_def] "ord_iso_map(A,r,B,s) <= A*B";
+by (Blast_tac 1);
qed "ord_iso_map_subset";
-goalw Order.thy [ord_iso_map_def]
- "domain(ord_iso_map(A,r,B,s)) <= A";
-by (Fast_tac 1);
+goalw Order.thy [ord_iso_map_def] "domain(ord_iso_map(A,r,B,s)) <= A";
+by (Blast_tac 1);
qed "domain_ord_iso_map";
-goalw Order.thy [ord_iso_map_def]
- "range(ord_iso_map(A,r,B,s)) <= B";
-by (Fast_tac 1);
+goalw Order.thy [ord_iso_map_def] "range(ord_iso_map(A,r,B,s)) <= B";
+by (Blast_tac 1);
qed "range_ord_iso_map";
goalw Order.thy [ord_iso_map_def]
"converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
-by (fast_tac (!claset addIs [ord_iso_sym]) 1);
+by (blast_tac (!claset addIs [ord_iso_sym]) 1);
qed "converse_ord_iso_map";
goalw Order.thy [ord_iso_map_def, function_def]
"!!B. well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))";
-by (safe_tac (!claset));
-by (rtac well_ord_iso_pred_eq 1);
-by (REPEAT_SOME assume_tac);
-by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1);
-by (assume_tac 1);
+by (blast_tac (!claset addIs [well_ord_iso_pred_eq,
+ ord_iso_sym, ord_iso_trans]) 1);
qed "function_ord_iso_map";
goal Order.thy
@@ -501,8 +494,9 @@
by (safe_tac (!claset));
by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
by (REPEAT
- (fast_tac (!claset addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
-by (asm_simp_tac (!simpset addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
+ (blast_tac (!claset addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
+by (asm_simp_tac
+ (!simpset addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
by (rewtac ord_iso_map_def);
by (safe_tac (!claset addSEs [UN_E]));
by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
@@ -531,7 +525,7 @@
by (forw_inst_tac [("A","A")] well_ord_is_linear 1);
by (linear_case_tac 1);
(*Trivial case: a=xa*)
-by (Fast_tac 2);
+by (Blast_tac 2);
(*Harder case: <a, xa>: r*)
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN
REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
@@ -539,7 +533,7 @@
REPEAT1 (eresolve_tac [asm_rl, predI] 1));
by (asm_full_simp_tac
(!simpset addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "domain_ord_iso_map_subset";
(*For the 4-way case analysis in the main result*)
@@ -559,7 +553,7 @@
by (assume_tac 2);
by (rtac equalityI 1);
(*not (!claset) below; that would use rules like domainE!*)
-by (fast_tac (!claset addSEs [predE]) 2);
+by (blast_tac (!claset addSEs [predE]) 2);
by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1));
qed "domain_ord_iso_map_cases";
@@ -591,7 +585,7 @@
by (dtac rangeI 1);
by (asm_full_simp_tac (!simpset addsimps [pred_def]) 1);
by (rewtac ord_iso_map_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "well_ord_trichotomy";
@@ -599,27 +593,27 @@
goalw Order.thy [irrefl_def]
"!!A. irrefl(A,r) ==> irrefl(A,converse(r))";
-by (fast_tac (!claset addSIs [converseI]) 1);
+by (blast_tac (!claset addSIs [converseI]) 1);
qed "irrefl_converse";
goalw Order.thy [trans_on_def]
"!!A. trans[A](r) ==> trans[A](converse(r))";
-by (fast_tac (!claset addSIs [converseI]) 1);
+by (blast_tac (!claset addSIs [converseI]) 1);
qed "trans_on_converse";
goalw Order.thy [part_ord_def]
"!!A. part_ord(A,r) ==> part_ord(A,converse(r))";
-by (fast_tac (!claset addSIs [irrefl_converse, trans_on_converse]) 1);
+by (blast_tac (!claset addSIs [irrefl_converse, trans_on_converse]) 1);
qed "part_ord_converse";
goalw Order.thy [linear_def]
"!!A. linear(A,r) ==> linear(A,converse(r))";
-by (fast_tac (!claset addSIs [converseI]) 1);
+by (blast_tac (!claset addSIs [converseI]) 1);
qed "linear_converse";
goalw Order.thy [tot_ord_def]
"!!A. tot_ord(A,r) ==> tot_ord(A,converse(r))";
-by (fast_tac (!claset addSIs [part_ord_converse, linear_converse]) 1);
+by (blast_tac (!claset addSIs [part_ord_converse, linear_converse]) 1);
qed "tot_ord_converse";
@@ -627,7 +621,7 @@
Lemmas involving the first element of a well ordered set **)
goalw thy [first_def] "!!b. first(b,B,r) ==> b:B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "first_is_elem";
goalw thy [well_ord_def, wf_on_def, wf_def, first_def]
@@ -636,9 +630,9 @@
by (contr_tac 1);
by (etac bexE 1);
by (res_inst_tac [("a","x")] ex1I 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (rewrite_goals_tac [tot_ord_def, linear_def]);
-by (Fast_tac 1);
+by (Blast.depth_tac (!claset) 7 1);
qed "well_ord_imp_ex1_first";
goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B";
--- a/src/ZF/OrderArith.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/OrderArith.ML Wed Apr 09 12:37:44 1997 +0200
@@ -15,22 +15,22 @@
goalw OrderArith.thy [radd_def]
"<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "radd_Inl_Inr_iff";
goalw OrderArith.thy [radd_def]
"<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "radd_Inl_iff";
goalw OrderArith.thy [radd_def]
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "radd_Inr_iff";
goalw OrderArith.thy [radd_def]
"<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "radd_Inr_Inl_iff";
(** Elimination Rule **)
@@ -43,7 +43,7 @@
\ |] ==> Q";
by (cut_facts_tac [major] 1);
(*Split into the three cases*)
-by (REPEAT_FIRST
+by (REPEAT_FIRST (*can't use safe_tac: don't want hyp_subst_tac*)
(eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE]));
(*Apply each premise to correct subgoal; can't just use fast_tac
because hyp_subst_tac would delete equalities too quickly*)
@@ -83,14 +83,14 @@
by (rtac ballI 2);
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
by (etac (bspec RS mp) 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (best_tac (!claset addSEs [raddE]) 2);
(*Returning to main part of proof*)
by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
by (Best_tac 1);
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
by (etac (bspec RS mp) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (best_tac (!claset addSEs [raddE]) 1);
qed "wf_on_radd";
@@ -143,11 +143,11 @@
\ (lam z:A+B. case(%x.x, %y.y, z)) : bij(A+B, A Un B)";
by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")]
lam_bijective 1);
-by (fast_tac (!claset addSIs [if_type]) 2);
+by (blast_tac (!claset addSIs [if_type]) 2);
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
by (safe_tac (!claset));
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
qed "sum_disjoint_bij";
(** Associativity **)
@@ -178,7 +178,7 @@
"!!r s. <<a',b'>, <a,b>> : rmult(A,r,B,s) <-> \
\ (<a',a>: r & a':A & a:A & b': B & b: B) | \
\ (<b',b>: s & a'=a & a:A & b': B & b: B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rmult_iff";
Addsimps [rmult_iff];
@@ -209,7 +209,7 @@
by (Asm_simp_tac 1);
by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1);
by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4);
-by (REPEAT_SOME (Fast_tac));
+by (REPEAT_SOME (Blast_tac));
qed "linear_rmult";
@@ -221,12 +221,12 @@
by (etac SigmaE 1);
by (etac ssubst 1);
by (subgoal_tac "ALL b:B. <x,b>: Ba" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1);
by (rtac ballI 1);
by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1);
by (etac (bspec RS mp) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (best_tac (!claset addSEs [rmultE]) 1);
qed "wf_on_rmult";
@@ -266,7 +266,7 @@
by (safe_tac (!claset addSIs [prod_bij]));
by (ALLGOALS
(asm_full_simp_tac (!simpset addsimps [bij_is_fun RS apply_type])));
-by (Fast_tac 1);
+by (Blast_tac 1);
by (fast_tac (!claset addSEs [bij_is_inj RS inj_apply_equality]) 1);
qed "prod_ord_iso_cong";
@@ -282,7 +282,7 @@
\ (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
by (Asm_simp_tac 1);
-by (fast_tac (!claset addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1);
+by (blast_tac (!claset addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1);
qed "singleton_prod_ord_iso";
(*Here we build a complicated function term, then simplify it using
@@ -295,7 +295,7 @@
by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
by (rtac singleton_prod_bij 1);
by (rtac sum_disjoint_bij 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (asm_simp_tac (!simpset addcongs [case_cong] addsimps [id_conv]) 1);
by (resolve_tac [comp_lam RS trans RS sym] 1);
by (fast_tac (!claset addSEs [case_type]) 1);
@@ -352,7 +352,7 @@
by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
by (REPEAT_FIRST (eresolve_tac [SigmaE, ssubst]));
by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "prod_assoc_ord_iso";
(**** Inverse image of a relation ****)
@@ -361,7 +361,7 @@
goalw OrderArith.thy [rvimage_def]
"<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rvimage_iff";
(** Type checking **)
@@ -374,7 +374,7 @@
goalw OrderArith.thy [rvimage_def]
"rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rvimage_converse";
@@ -382,17 +382,17 @@
goalw OrderArith.thy [irrefl_def, rvimage_def]
"!!A B. [| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))";
-by (fast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
qed "irrefl_rvimage";
goalw OrderArith.thy [trans_on_def, rvimage_def]
"!!A B. [| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))";
-by (fast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type]) 1);
qed "trans_on_rvimage";
goalw OrderArith.thy [part_ord_def]
"!!A B. [| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))";
-by (fast_tac (!claset addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
+by (blast_tac (!claset addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
qed "part_ord_rvimage";
(** Linearity **)
@@ -404,12 +404,12 @@
by (asm_simp_tac (!simpset addsimps [rvimage_iff]) 1);
by (cut_facts_tac [finj] 1);
by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
-by (REPEAT_SOME (fast_tac (!claset addSIs [apply_type])));
+by (REPEAT_SOME (blast_tac (!claset addIs [apply_funtype])));
qed "linear_rvimage";
goalw OrderArith.thy [tot_ord_def]
"!!A B. [| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))";
-by (fast_tac (!claset addSIs [part_ord_rvimage, linear_rvimage]) 1);
+by (blast_tac (!claset addSIs [part_ord_rvimage, linear_rvimage]) 1);
qed "tot_ord_rvimage";
@@ -419,10 +419,11 @@
"!!r. [| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
by (rtac wf_onI2 1);
by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
-by (fast_tac (!claset addSIs [apply_type]) 1);
-by (best_tac (!claset addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1);
+by (blast_tac (!claset addSIs [apply_funtype]) 1);
+by (blast_tac (!claset addSIs [apply_funtype]
+ addSDs [rvimage_iff RS iffD1]) 1);
qed "wf_on_rvimage";
(*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
@@ -430,8 +431,8 @@
"!!r. [| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
by (rtac well_ordI 1);
by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
-by (fast_tac (!claset addSIs [wf_on_rvimage, inj_is_fun]) 1);
-by (fast_tac (!claset addSIs [linear_rvimage]) 1);
+by (blast_tac (!claset addSIs [wf_on_rvimage, inj_is_fun]) 1);
+by (blast_tac (!claset addSIs [linear_rvimage]) 1);
qed "well_ord_rvimage";
goalw OrderArith.thy [ord_iso_def]
--- a/src/ZF/OrderType.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/OrderType.ML Wed Apr 09 12:37:44 1997 +0200
@@ -32,12 +32,12 @@
goalw OrderType.thy [pred_def, lt_def]
"!!i j. j<i ==> pred(i, j, Memrel(i)) = j";
by (asm_simp_tac (!simpset addsimps [Memrel_iff]) 1);
-by (fast_tac (!claset addEs [Ord_trans]) 1);
+by (blast_tac (!claset addIs [Ord_trans]) 1);
qed "lt_pred_Memrel";
goalw OrderType.thy [pred_def,Memrel_def]
"!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "pred_Memrel";
goal OrderType.thy
@@ -108,7 +108,7 @@
by (asm_simp_tac (!simpset addsimps [ordermap_pred_unfold]) 1);
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
by (rewrite_goals_tac [pred_def,Transset_def]);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (safe_tac (!claset));
by (ordermap_elim_tac 1);
by (fast_tac (!claset addSEs [trans_onD]) 1);
@@ -118,11 +118,11 @@
"!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (fast_tac (!claset addIs [Ord_ordermap]) 2);
+by (blast_tac (!claset addIs [Ord_ordermap]) 2);
by (rewrite_goals_tac [Transset_def,well_ord_def]);
by (safe_tac (!claset));
by (ordermap_elim_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Ord_ordertype";
(*** ordermap preserves the orderings in both directions ***)
@@ -132,7 +132,7 @@
\ ordermap(A,r)`w : ordermap(A,r)`x";
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ordermap_mono";
(*linearity of r is crucial here*)
@@ -141,7 +141,7 @@
\ w: A; x: A |] ==> <w,x>: r";
by (safe_tac (!claset));
by (linear_case_tac 1);
-by (fast_tac (!claset addSEs [mem_not_refl RS notE]) 1);
+by (blast_tac (!claset addSEs [mem_not_refl RS notE]) 1);
by (dtac ordermap_mono 1);
by (REPEAT_SOME assume_tac);
by (etac mem_asym 1);
@@ -165,13 +165,10 @@
goalw OrderType.thy [ord_iso_def]
"!!r. well_ord(A,r) ==> \
\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
-by (safe_tac (!claset));
-by (rtac ordermap_bij 1);
-by (assume_tac 1);
-by (fast_tac (!claset addSEs [MemrelE, converse_ordermap_mono]) 2);
-by (rewtac well_ord_def);
-by (fast_tac (!claset addSIs [MemrelI, ordermap_mono,
- ordermap_type RS apply_type]) 1);
+by (safe_tac (!claset addSEs [well_ord_is_wf]
+ addSIs [ordermap_type RS apply_type,
+ ordermap_mono, ordermap_bij]));
+by (blast_tac (!claset addSDs [converse_ordermap_mono]) 1);
qed "ordertype_ord_iso";
goal OrderType.thy
@@ -252,12 +249,12 @@
(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
goal OrderType.thy
- "!!r. [| well_ord(A,r); x:A |] ==> \
+ "!!r. [| well_ord(A,r); x:A |] ==> \
\ ordertype(pred(A,x,r),r) <= ordertype(A,r)";
by (asm_simp_tac (!simpset addsimps [ordertype_unfold,
pred_subset RSN (2, well_ord_subset)]) 1);
-by (fast_tac (!claset addIs [ordermap_pred_eq_ordermap, RepFun_eqI]
- addEs [predE]) 1);
+by (fast_tac (!claset addIs [ordermap_pred_eq_ordermap]
+ addEs [predE]) 1);
qed "ordertype_pred_subset";
goal OrderType.thy
@@ -295,7 +292,7 @@
by (rtac conjI 1);
by (etac well_ord_Memrel 1);
by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (Fast_tac 1);
+by (Blast.depth_tac (!claset) 8 1);
qed "Ord_is_Ord_alt";
(*proof by lcp*)
@@ -303,12 +300,7 @@
tot_ord_def, part_ord_def, trans_on_def]
"!!i. Ord_alt(i) ==> Ord(i)";
by (asm_full_simp_tac (!simpset addsimps [Memrel_iff, pred_Memrel]) 1);
-by (safe_tac (!claset));
-by (fast_tac (!claset addSDs [equalityD1]) 1);
-by (subgoal_tac "xa: i" 1);
-by (fast_tac (!claset addSDs [equalityD1]) 2);
-by (fast_tac (!claset addSDs [equalityD1]
- addSEs [bspec RS bspec RS bspec RS mp RS mp]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
qed "Ord_alt_is_Ord";
@@ -321,7 +313,7 @@
goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
by (res_inst_tac [("d", "Inl")] lam_bijective 1);
by (safe_tac (!claset));
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "bij_sum_0";
goal OrderType.thy
@@ -334,7 +326,7 @@
goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
by (res_inst_tac [("d", "Inr")] lam_bijective 1);
by (safe_tac (!claset));
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "bij_0_sum";
goal OrderType.thy
@@ -433,7 +425,7 @@
"!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
by (resolve_tac [id_bij RS ord_isoI] 1);
by (asm_simp_tac (!simpset addsimps [id_conv, Memrel_iff]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "id_ord_iso_Memrel";
goal OrderType.thy
@@ -517,13 +509,13 @@
by (REPEAT (ares_tac [Ord_oadd] 1));
by (fast_tac (!claset addIs [lt_oadd1, oadd_lt_mono2]
addss (!simpset addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
-by (Fast_tac 2);
-by (fast_tac (!claset addSEs [ltE]) 1);
+by (Blast_tac 2);
+by (blast_tac (!claset addSEs [ltE]) 1);
qed "oadd_unfold";
goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
by (asm_simp_tac (!simpset addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "oadd_1";
goal OrderType.thy
@@ -539,7 +531,7 @@
val prems = goal OrderType.thy
"[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \
\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (fast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd,
+by (blast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd,
lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
qed "oadd_UN";
@@ -561,7 +553,7 @@
by (asm_simp_tac (!simpset addsimps [oadd_Limit]) 1);
by (rtac le_trans 1);
by (rtac le_implies_UN_le_UN 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq,
le_refl, Limit_is_Ord]) 1);
qed "oadd_le_self2";
@@ -574,7 +566,7 @@
by (asm_simp_tac (!simpset addsimps [oadd_succ, succ_le_iff]) 1);
by (asm_simp_tac (!simpset addsimps [oadd_Limit]) 1);
by (rtac le_implies_UN_le_UN 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "oadd_le_mono1";
goal OrderType.thy "!!i j. [| i' le i; j'<j |] ==> i'++j' < i++j";
@@ -601,7 +593,7 @@
goal OrderType.thy
"!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (fast_tac (!claset addSIs [if_type]) 1);
+by (blast_tac (!claset addSIs [if_type]) 1);
by (fast_tac (!claset addSIs [case_type]) 1);
by (etac sumE 2);
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
@@ -620,7 +612,7 @@
by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
by (asm_simp_tac (!simpset addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
-by (fast_tac (!claset addEs [lt_trans2, lt_trans]) 1);
+by (blast_tac (!claset addIs [lt_trans2, lt_trans]) 1);
qed "ordertype_sum_Diff";
goalw OrderType.thy [oadd_def, odiff_def]
@@ -681,7 +673,7 @@
by (rtac equalityI 1);
by (safe_tac (!claset));
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [rmult_iff])));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
qed "pred_Pair_eq";
goal OrderType.thy
@@ -693,7 +685,7 @@
by (resolve_tac [ordertype_eq RS sym] 1);
by (rtac prod_sum_singleton_ord_iso 1);
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
-by (fast_tac (!claset addSEs [predE]) 1);
+by (blast_tac (!claset addSEs [predE]) 1);
qed "ordertype_pred_Pair_eq";
goalw OrderType.thy [oadd_def, omult_def]
@@ -724,7 +716,7 @@
by (step_tac (!claset addSEs [ltE]) 1);
by (asm_simp_tac (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
symmetric omult_def]) 1);
-by (fast_tac (!claset addIs [ltI]) 1);
+by (blast_tac (!claset addIs [ltI]) 1);
qed "lt_omult";
goalw OrderType.thy [omult_def]
@@ -737,7 +729,7 @@
(!simpset addsimps [ordertype_pred_unfold,
well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
by (rtac bexI 1);
-by (fast_tac (!claset addSEs [ltE]) 2);
+by (blast_tac (!claset addSEs [ltE]) 2);
by (asm_simp_tac
(!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
symmetric omult_def]) 1);
@@ -749,8 +741,8 @@
by (resolve_tac [lt_omult RS exE] 1);
by (etac ltI 3);
by (REPEAT (ares_tac [Ord_omult] 1));
-by (fast_tac (!claset addSEs [ltE]) 1);
-by (fast_tac (!claset addIs [omult_oadd_lt RS ltD, ltI]) 1);
+by (blast_tac (!claset addSEs [ltE]) 1);
+by (blast_tac (!claset addIs [omult_oadd_lt RS ltD, ltI]) 1);
qed "omult_unfold";
(*** Basic laws for ordinal multiplication ***)
@@ -832,7 +824,7 @@
"[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \
\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
by (asm_simp_tac (!simpset addsimps (prems@[Ord_UN, omult_unfold])) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "omult_UN";
goal OrderType.thy
@@ -866,7 +858,7 @@
by (asm_simp_tac (!simpset addsimps [omult_succ, oadd_le_mono]) 1);
by (asm_simp_tac (!simpset addsimps [omult_Limit]) 1);
by (rtac le_implies_UN_le_UN 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "omult_le_mono1";
goal OrderType.thy "!!i j k. [| k<j; 0<i |] ==> i**k < i**j";
@@ -909,7 +901,7 @@
by (asm_simp_tac (!simpset addsimps [omult_Limit]) 1);
by (rtac le_trans 1);
by (rtac le_implies_UN_le_UN 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq,
Limit_is_Ord RS le_refl]) 1);
qed "omult_le_self2";
--- a/src/ZF/Ordinal.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Ordinal.ML Wed Apr 09 12:37:44 1997 +0200
@@ -13,75 +13,75 @@
(** Two neat characterisations of Transset **)
goalw Ordinal.thy [Transset_def] "Transset(A) <-> A<=Pow(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_iff_Pow";
goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
qed "Transset_iff_Union_succ";
(** Consequences of downwards closure **)
goalw Ordinal.thy [Transset_def]
"!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_doubleton_D";
val [prem1,prem2] = goalw Ordinal.thy [Pair_def]
"[| Transset(C); <a,b>: C |] ==> a:C & b: C";
by (cut_facts_tac [prem2] 1);
-by (fast_tac (!claset addSDs [prem1 RS Transset_doubleton_D]) 1);
+by (blast_tac (!claset addSDs [prem1 RS Transset_doubleton_D]) 1);
qed "Transset_Pair_D";
val prem1::prems = goal Ordinal.thy
"[| Transset(C); A*B <= C; b: B |] ==> A <= C";
by (cut_facts_tac prems 1);
-by (fast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
+by (blast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
qed "Transset_includes_domain";
val prem1::prems = goal Ordinal.thy
"[| Transset(C); A*B <= C; a: A |] ==> B <= C";
by (cut_facts_tac prems 1);
-by (fast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
+by (blast_tac (!claset addSDs [prem1 RS Transset_Pair_D]) 1);
qed "Transset_includes_range";
(** Closure properties **)
goalw Ordinal.thy [Transset_def] "Transset(0)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_0";
goalw Ordinal.thy [Transset_def]
"!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Un j)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_Un";
goalw Ordinal.thy [Transset_def]
"!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Int j)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_Int";
goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_succ";
goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_Pow";
goalw Ordinal.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Transset_Union";
val [Transprem] = goalw Ordinal.thy [Transset_def]
"[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
-by (fast_tac (!claset addEs [Transprem RS bspec RS subsetD]) 1);
+by (blast_tac (!claset addDs [Transprem RS bspec RS subsetD]) 1);
qed "Transset_Union_family";
val [prem,Transprem] = goalw Ordinal.thy [Transset_def]
"[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
by (cut_facts_tac [prem] 1);
-by (fast_tac (!claset addEs [Transprem RS bspec RS subsetD]) 1);
+by (blast_tac (!claset addDs [Transprem RS bspec RS subsetD]) 1);
qed "Transset_Inter_family";
(*** Natural Deduction rules for Ord ***)
@@ -104,7 +104,7 @@
(*** Lemmas for ordinals ***)
goalw Ordinal.thy [Ord_def,Transset_def] "!!i j.[| Ord(i); j:i |] ==> Ord(j)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Ord_in_Ord";
(* Ord(succ(j)) ==> Ord(j) *)
@@ -116,7 +116,7 @@
qed "Ord_subset_Ord";
goalw Ordinal.thy [Ord_def,Transset_def] "!!i j. [| j:i; Ord(i) |] ==> j<=i";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "OrdmemD";
goal Ordinal.thy "!!i j k. [| i:j; j:k; Ord(k) |] ==> i:k";
@@ -143,18 +143,18 @@
bind_thm ("Ord_1", Ord_0 RS Ord_succ);
goal Ordinal.thy "Ord(succ(i)) <-> Ord(i)";
-by (fast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
+by (blast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
qed "Ord_succ_iff";
Addsimps [Ord_0, Ord_succ_iff];
AddSIs [Ord_0, Ord_succ];
goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
-by (fast_tac (!claset addSIs [Transset_Un]) 1);
+by (blast_tac (!claset addSIs [Transset_Un]) 1);
qed "Ord_Un";
goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
-by (fast_tac (!claset addSIs [Transset_Int]) 1);
+by (blast_tac (!claset addSIs [Transset_Int]) 1);
qed "Ord_Int";
val nonempty::prems = goal Ordinal.thy
@@ -179,7 +179,7 @@
by (forw_inst_tac [("x", "X")] spec 1);
by (safe_tac (!claset addSEs [mem_irrefl]));
by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (rewtac Transset_def);
by (safe_tac (!claset));
by (Asm_full_simp_tac 1);
@@ -204,7 +204,7 @@
qed "ltD";
goalw Ordinal.thy [lt_def] "~ i<0";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "not_lt0";
Addsimps [not_lt0];
@@ -224,7 +224,7 @@
bind_thm ("lt0E", not_lt0 RS notE);
goal Ordinal.thy "!!i j k. [| i<j; j<k |] ==> i<k";
-by (fast_tac (!claset addSIs [ltI] addSEs [ltE, Ord_trans]) 1);
+by (blast_tac (!claset addSIs [ltI] addSEs [ltE] addIs [Ord_trans]) 1);
qed "lt_trans";
goalw Ordinal.thy [lt_def] "!!i j. [| i<j; j<i |] ==> P";
@@ -242,7 +242,7 @@
(** le is less than or equals; recall i le j abbrevs i<succ(j) !! **)
goalw Ordinal.thy [lt_def] "i le j <-> i<j | (i=j & Ord(j))";
-by (fast_tac (!claset addSIs [Ord_succ] addSDs [Ord_succD]) 1);
+by (blast_tac (!claset addSIs [Ord_succ] addSDs [Ord_succD]) 1);
qed "le_iff";
(*Equivalently, i<j ==> i < succ(j)*)
@@ -269,11 +269,11 @@
goal Ordinal.thy "!!i j. [| i le j; j le i |] ==> i=j";
by (asm_full_simp_tac (!simpset addsimps [le_iff]) 1);
-by (fast_tac (!claset addEs [lt_asym]) 1);
+by (blast_tac (!claset addEs [lt_asym]) 1);
qed "le_anti_sym";
goal Ordinal.thy "i le 0 <-> i=0";
-by (fast_tac (!claset addSIs [Ord_0 RS le_refl] addSEs [leE]) 1);
+by (blast_tac (!claset addSIs [Ord_0 RS le_refl] addSEs [leE]) 1);
qed "le0_iff";
bind_thm ("le0D", le0_iff RS iffD1);
@@ -282,17 +282,18 @@
AddSDs [le0D];
Addsimps [le0_iff];
+(*blast_tac will NOT see lt_asym*)
val le_cs = !claset addSIs [leCI] addSEs [leE] addEs [lt_asym];
(*** Natural Deduction rules for Memrel ***)
goalw Ordinal.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Memrel_iff";
-val prems = goal Ordinal.thy "[| a: b; a: A; b: A |] ==> <a,b> : Memrel(A)";
-by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1));
+goal Ordinal.thy "!!A. [| a: b; a: A; b: A |] ==> <a,b> : Memrel(A)";
+by (REPEAT (ares_tac [conjI, Memrel_iff RS iffD2] 1));
qed "MemrelI";
val [major,minor] = goal Ordinal.thy
@@ -305,20 +306,23 @@
by (REPEAT (assume_tac 1));
qed "MemrelE";
+AddSIs [MemrelI];
+AddSEs [MemrelE];
+
goalw Ordinal.thy [Memrel_def] "Memrel(A) <= A*A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Memrel_type";
goalw Ordinal.thy [Memrel_def] "!!A B. A<=B ==> Memrel(A) <= Memrel(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Memrel_mono";
goalw Ordinal.thy [Memrel_def] "Memrel(0) = 0";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Memrel_0";
goalw Ordinal.thy [Memrel_def] "Memrel(1) = 0";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Memrel_1";
Addsimps [Memrel_0, Memrel_1];
@@ -338,13 +342,13 @@
(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
goalw Ordinal.thy [Ord_def, Transset_def, trans_def]
"!!i. Ord(i) ==> trans(Memrel(i))";
-by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (Blast_tac 1);
qed "trans_Memrel";
(*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
goalw Ordinal.thy [Transset_def]
"!!A. Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A";
-by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (Blast_tac 1);
qed "Transset_Memrel_iff";
@@ -356,11 +360,11 @@
\ !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) \
\ |] ==> P(i)";
by (rtac (major RS (wf_Memrel RS wf_induct2)) 1);
-by (fast_tac (!claset addEs [MemrelE]) 1);
+by (Blast_tac 1);
by (resolve_tac prems 1);
by (assume_tac 1);
by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs [MemrelI]) 1);
+by (Blast_tac 1);
qed "Transset_induct";
(*Induction over an ordinal*)
@@ -423,19 +427,19 @@
qed "Ord_linear_le";
goal Ordinal.thy "!!i j. j le i ==> ~ i<j";
-by (fast_tac le_cs 1);
+by (blast_tac le_cs 1);
qed "le_imp_not_lt";
goal Ordinal.thy "!!i j. [| ~ i<j; Ord(i); Ord(j) |] ==> j le i";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear2 1);
by (REPEAT (SOMEGOAL assume_tac));
-by (fast_tac le_cs 1);
+by (blast_tac le_cs 1);
qed "not_lt_imp_le";
(** Some rewrite rules for <, le **)
goalw Ordinal.thy [lt_def] "!!i j. Ord(j) ==> i:j <-> i<j";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Ord_mem_iff_lt";
goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> ~ i<j <-> j le i";
@@ -455,7 +459,7 @@
goal Ordinal.thy "!!i. [| Ord(i); i~=0 |] ==> 0<i";
by (etac (not_le_iff_lt RS iffD1) 1);
by (rtac Ord_0 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Ord_0_lt";
(*** Results about less-than or equals ***)
@@ -466,23 +470,23 @@
by (rtac (not_lt_iff_le RS iffD1) 1);
by (assume_tac 1);
by (assume_tac 1);
-by (fast_tac (!claset addEs [ltE, mem_irrefl]) 1);
+by (blast_tac (!claset addEs [ltE, mem_irrefl]) 1);
qed "subset_imp_le";
goal Ordinal.thy "!!i j. i le j ==> i<=j";
by (etac leE 1);
-by (Fast_tac 2);
-by (fast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1);
+by (Blast_tac 2);
+by (blast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1);
qed "le_imp_subset";
goal Ordinal.thy "j le i <-> j<=i & Ord(i) & Ord(j)";
by (fast_tac (!claset addSEs [subset_imp_le, le_imp_subset]
- addEs [ltE, make_elim Ord_succD]) 1);
+ addEs [ltE, make_elim Ord_succD]) 1);
qed "le_subset_iff";
goal Ordinal.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
by (simp_tac (!simpset addsimps [le_iff]) 1);
-by (fast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
+by (blast_tac (!claset addIs [Ord_succ] addDs [Ord_succD]) 1);
qed "le_succ_iff";
(*Just a variant of subset_imp_le*)
@@ -495,11 +499,11 @@
(** Transitive laws **)
goal Ordinal.thy "!!i j. [| i le j; j<k |] ==> i<k";
-by (fast_tac (!claset addEs [leE, lt_trans]) 1);
+by (blast_tac (!claset addSEs [leE] addIs [lt_trans]) 1);
qed "lt_trans1";
goal Ordinal.thy "!!i j. [| i<j; j le k |] ==> i<k";
-by (fast_tac (!claset addEs [leE, lt_trans]) 1);
+by (blast_tac (!claset addSEs [leE] addIs [lt_trans]) 1);
qed "lt_trans2";
goal Ordinal.thy "!!i j. [| i le j; j le k |] ==> i le k";
@@ -508,15 +512,15 @@
goal Ordinal.thy "!!i j. i<j ==> succ(i) le j";
by (rtac (not_lt_iff_le RS iffD1) 1);
-by (fast_tac le_cs 3);
-by (ALLGOALS (fast_tac (!claset addEs [ltE] addIs [Ord_succ])));
+by (blast_tac le_cs 3);
+by (ALLGOALS (blast_tac (!claset addEs [ltE] addIs [Ord_succ])));
qed "succ_leI";
(*Identical to succ(i) < succ(j) ==> i<j *)
goal Ordinal.thy "!!i j. succ(i) le j ==> i<j";
by (rtac (not_le_iff_lt RS iffD1) 1);
by (fast_tac le_cs 3);
-by (ALLGOALS (fast_tac (!claset addEs [ltE, make_elim Ord_succD])));
+by (ALLGOALS (blast_tac (!claset addEs [ltE, make_elim Ord_succD])));
qed "succ_leE";
goal Ordinal.thy "succ(i) le j <-> i<j";
@@ -526,7 +530,7 @@
Addsimps [succ_le_iff];
goal Ordinal.thy "!!i j. succ(i) le succ(j) ==> i le j";
-by (fast_tac (!claset addSEs [succ_leE]) 1);
+by (blast_tac (!claset addSDs [succ_leE]) 1);
qed "succ_le_imp_le";
(** Union and Intersection **)
@@ -647,14 +651,14 @@
qed "Limit_has_0";
goalw Ordinal.thy [Limit_def] "!!i. [| Limit(i); j<i |] ==> succ(j) < i";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Limit_has_succ";
goalw Ordinal.thy [Limit_def]
"!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)";
by (safe_tac subset_cs);
by (rtac (not_le_iff_lt RS iffD1) 2);
-by (fast_tac le_cs 4);
+by (blast_tac le_cs 4);
by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
qed "non_succ_LimitI";
@@ -672,7 +676,7 @@
(** Traditional 3-way case analysis on ordinals **)
goal Ordinal.thy "!!i. Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)";
-by (fast_tac (!claset addSIs [non_succ_LimitI, Ord_0_lt]
+by (blast_tac (!claset addSIs [non_succ_LimitI, Ord_0_lt]
addSDs [Ord_succD]) 1);
qed "Ord_cases_disj";
@@ -694,5 +698,5 @@
\ |] ==> P(i)";
by (resolve_tac [major RS trans_induct] 1);
by (etac Ord_cases 1);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
+by (ALLGOALS (blast_tac (!claset addIs prems)));
qed "trans_induct3";
--- a/src/ZF/Sum.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Sum.ML Wed Apr 09 12:37:44 1997 +0200
@@ -17,7 +17,7 @@
goalw Sum.thy [Part_def]
"!!a b A h. [| a : A; a=h(b) |] ==> a : Part(A,h)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_eqI";
val PartI = refl RSN (2,Part_eqI);
@@ -30,7 +30,7 @@
by (REPEAT (ares_tac prems 1));
qed "PartE";
-AddSIs [PartI];
+AddIs [Part_eqI];
AddSEs [PartE];
goalw Sum.thy [Part_def] "Part(A,h) <= A";
@@ -43,17 +43,17 @@
val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Sigma_bool";
(** Introduction rules for the injections **)
goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "InlI";
goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "InrI";
(** Elimination rules **)
@@ -104,28 +104,28 @@
Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "InlD";
goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "InrD";
goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "sum_iff";
goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "sum_subset_iff";
goal Sum.thy "A+B = C+D <-> A=C & B=D";
by (simp_tac (!simpset addsimps [extension,sum_subset_iff]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "sum_equal_iff";
goalw Sum.thy [sum_def] "A+A = 2*A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "sum_eq_2_times";
@@ -179,21 +179,21 @@
(*** More rules for Part(A,h) ***)
goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_mono";
goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Collect";
bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Inl";
goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Inr";
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
@@ -201,13 +201,13 @@
qed "PartD1";
goal Sum.thy "Part(A,%x.x) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_id";
goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Inr2";
goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_sum_equality";
--- a/src/ZF/Univ.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Univ.ML Wed Apr 09 12:37:44 1997 +0200
@@ -40,7 +40,7 @@
by (eps_ind_tac "x" 1);
by (stac Vfrom 1);
by (stac Vfrom 1);
-by (fast_tac (!claset addSIs [rank_lt RS ltD]) 1);
+by (blast_tac (!claset addSIs [rank_lt RS ltD]) 1);
qed "Vfrom_rank_subset1";
goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
@@ -71,13 +71,13 @@
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "zero_in_Vfrom";
goal Univ.thy "i <= Vfrom(A,i)";
by (eps_ind_tac "i" 1);
by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "i_subset_Vfrom";
goal Univ.thy "A <= Vfrom(A,i)";
@@ -89,7 +89,7 @@
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "subset_mem_Vfrom";
(** Finite sets and ordered pairs **)
@@ -122,7 +122,7 @@
goal Univ.thy "Vfrom(A,0) = A";
by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Vfrom_0";
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
@@ -160,7 +160,7 @@
(*opposite inclusion*)
by (rtac UN_least 1);
by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Vfrom_Union";
(*** Vfrom applied to Limit ordinals ***)
@@ -258,7 +258,7 @@
qed "Inr_in_VLimit";
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
-by (fast_tac (!claset addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
+by (blast_tac (!claset addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
qed "sum_VLimit";
bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
@@ -270,7 +270,7 @@
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
by (eps_ind_tac "i" 1);
by (stac Vfrom 1);
-by (fast_tac (!claset addSIs [Transset_Union_family, Transset_Un,
+by (blast_tac (!claset addSIs [Transset_Union_family, Transset_Un,
Transset_Pow]) 1);
qed "Transset_Vfrom";
@@ -284,7 +284,7 @@
goalw Ordinal.thy [Pair_def,Transset_def]
"!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
-by (Best_tac 1);
+by (Blast_tac 1);
qed "Transset_Pair_subset";
goal Univ.thy
@@ -326,7 +326,7 @@
by (dtac Transset_Vfrom 1);
by (rtac subset_mem_Vfrom 1);
by (rewtac Transset_def);
-by (fast_tac (!claset addIs [Pair_in_Vfrom]) 1);
+by (blast_tac (!claset addIs [Pair_in_Vfrom]) 1);
qed "prod_in_Vfrom";
val [aprem,bprem,limiti,transset] = goal Univ.thy
@@ -345,7 +345,7 @@
by (dtac Transset_Vfrom 1);
by (rtac subset_mem_Vfrom 1);
by (rewtac Transset_def);
-by (fast_tac (!claset addIs [zero_in_Vfrom, Pair_in_Vfrom,
+by (blast_tac (!claset addIs [zero_in_Vfrom, Pair_in_Vfrom,
i_subset_Vfrom RS subsetD]) 1);
qed "sum_in_Vfrom";
@@ -371,7 +371,7 @@
by (rtac (succI1 RS UN_upper) 2);
by (rtac Pow_mono 1);
by (rewtac Transset_def);
-by (fast_tac (!claset addIs [Pair_in_Vfrom]) 1);
+by (blast_tac (!claset addIs [Pair_in_Vfrom]) 1);
qed "fun_in_Vfrom";
val [aprem,bprem,limiti,transset] = goal Univ.thy
@@ -387,7 +387,7 @@
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
by (stac Vfrom 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Vset";
val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
@@ -402,7 +402,7 @@
by (safe_tac (!claset));
by (stac rank 1);
by (rtac UN_succ_least_lt 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (REPEAT (ares_tac [ltI] 1));
qed "Vset_rank_imp1";
@@ -413,7 +413,7 @@
by (rtac (ordi RS trans_induct) 1);
by (rtac allI 1);
by (stac Vset 1);
-by (fast_tac (!claset addSIs [rank_lt RS ltD]) 1);
+by (blast_tac (!claset addSIs [rank_lt RS ltD]) 1);
qed "Vset_rank_imp2";
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
@@ -579,7 +579,7 @@
qed "two_in_univ";
goalw Univ.thy [bool_def] "bool <= univ(A)";
-by (fast_tac (!claset addSIs [zero_in_univ,one_in_univ]) 1);
+by (blast_tac (!claset addSIs [zero_in_univ,one_in_univ]) 1);
qed "bool_subset_univ";
bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
@@ -614,13 +614,13 @@
goal Univ.thy
"!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
by (etac Fin_induct 1);
-by (fast_tac (!claset addSDs [Limit_has_0]) 1);
+by (blast_tac (!claset addSDs [Limit_has_0]) 1);
by (safe_tac (!claset));
by (etac Limit_VfromE 1);
by (assume_tac 1);
by (res_inst_tac [("x", "xa Un j")] exI 1);
by (best_tac (!claset addIs [subset_refl RS Vfrom_mono RS subsetD,
- Un_least_lt]) 1);
+ Un_least_lt]) 1);
val Fin_Vfrom_lemma = result();
goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
@@ -628,7 +628,7 @@
by (dtac Fin_Vfrom_lemma 1);
by (safe_tac (!claset));
by (resolve_tac [Vfrom RS ssubst] 1);
-by (fast_tac (!claset addSDs [ltD]) 1);
+by (blast_tac (!claset addSDs [ltD]) 1);
val Fin_VLimit = result();
bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
--- a/src/ZF/ZF.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/ZF.ML Wed Apr 09 12:37:44 1997 +0200
@@ -438,7 +438,6 @@
(fn _=> [ Blast_tac 1 ]);
Addsimps [empty_subsetI];
-AddSIs [empty_subsetI];
qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
(fn prems=> [ blast_tac (!claset addDs prems) 1 ]);
--- a/src/ZF/Zorn.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/Zorn.ML Wed Apr 09 12:37:44 1997 +0200
@@ -14,12 +14,12 @@
(*** Section 1. Mathematical Preamble ***)
goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_lemma0";
goal ZF.thy
"!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_lemma0";
@@ -73,7 +73,7 @@
\ |] ==> n<=m | next`m<=n";
by (cut_facts_tac prems 1);
by (rtac (major RS TFin_induct) 1);
-by (etac Union_lemma0 2); (*or just Fast_tac*)
+by (etac Union_lemma0 2); (*or just Blast_tac*)
by (fast_tac (subset_cs addIs [increasing_trans]) 1);
qed "TFin_linear_lemma1";
@@ -173,7 +173,7 @@
\ |] ==> ch ` super(S,X) : super(S,X)";
by (etac apply_type 1);
by (rewrite_goals_tac [super_def, maxchain_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "choice_super";
goal Zorn.thy
@@ -210,7 +210,7 @@
by (dtac choice_super 1);
by (REPEAT (assume_tac 1));
by (rewtac super_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Hausdorff_next_exists";
(*Lemma 4*)
@@ -227,13 +227,10 @@
choice_super RS (super_subset_chain RS subsetD)]
setloop split_tac [expand_if]) 1);
by (rewtac chain_def);
-by (rtac CollectI 1 THEN Fast_tac 1);
-(*Cannot use safe_tac: the disjunction must be left alone*)
-by (REPEAT (rtac ballI 1 ORELSE etac UnionE 1));
+by (rtac CollectI 1 THEN Blast_tac 1);
+by (safe_tac(!claset));
by (res_inst_tac [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
-(*fast_tac is just too slow here!*)
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, subsetD] 1
- ORELSE ball_tac 1 THEN etac (CollectD2 RS bspec RS bspec) 1));
+by (ALLGOALS Fast_tac);
qed "TFin_chain_lemma4";
goal Zorn.thy "EX c. c : maxchain(S)";
@@ -265,7 +262,7 @@
(*Used in the proof of Zorn's Lemma*)
goalw Zorn.thy [chain_def]
"!!c. [| c: chain(A); z: A; ALL x:c. x<=z |] ==> cons(z,c) : chain(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "chain_extend";
goal Zorn.thy
@@ -274,16 +271,16 @@
by (asm_full_simp_tac (!simpset addsimps [maxchain_def]) 1);
by (rename_tac "c" 1);
by (res_inst_tac [("x", "Union(c)")] bexI 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (safe_tac (!claset));
by (rename_tac "z" 1);
by (rtac classical 1);
by (subgoal_tac "cons(z,c): super(S,c)" 1);
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
by (rewtac super_def);
by (safe_tac (!claset));
by (fast_tac (!claset addEs [chain_extend]) 1);
-by (best_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
qed "Zorn";
@@ -295,13 +292,13 @@
\ |] ==> ALL m:Z. n<=m";
by (cut_facts_tac prems 1);
by (rtac (major RS TFin_induct) 1);
-by (Fast_tac 2); (*second induction step is easy*)
+by (Blast_tac 2); (*second induction step is easy*)
by (rtac ballI 1);
by (rtac (bspec RS TFin_subsetD RS disjE) 1);
by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
by (subgoal_tac "x = Inter(Z)" 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
qed "TFin_well_lemma5";
(*Well-ordering of TFin(S,next)*)
@@ -324,17 +321,17 @@
(*Prove the linearity goal first*)
by (REPEAT (rtac ballI 2));
by (excluded_middle_tac "x=y" 2);
-by (Fast_tac 3);
+by (Blast_tac 3);
(*The x~=y case remains*)
by (res_inst_tac [("n1","x"), ("m1","y")]
(TFin_subset_linear RS disjE) 2 THEN REPEAT (assume_tac 2));
-by (Fast_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
+by (Blast_tac 2);
(*Now prove the well_foundedness goal*)
by (rtac wf_onI 1);
by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "well_ord_TFin";
(** Defining the "next" operation for Zermelo's Theorem **)
--- a/src/ZF/equalities.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/equalities.ML Wed Apr 09 12:37:44 1997 +0200
@@ -532,8 +532,8 @@
(** RepFun **)
goal ZF.thy "{f(x).x:A}=0 <-> A=0";
- (*blast_tac takes too long to search depth 5*)
-by (Blast.depth_tac (!claset addSEs [equalityE]) 6 1);
+ (*blast_tac takes too long to find a good depth*)
+by (Blast.depth_tac (!claset addSEs [equalityE]) 10 1);
qed "RepFun_eq_0_iff";
(** Collect **)
--- a/src/ZF/func.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/func.ML Wed Apr 09 12:37:44 1997 +0200
@@ -306,7 +306,8 @@
"!!S. [| ALL x:S. function(x); \
\ ALL x:S. ALL y:S. x<=y | y<=x |] ==> \
\ function(Union(S))";
-by (blast_tac (!claset addSDs [bspec RS bspec]) 1);
+by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
+ (*by (Blast_tac 1); takes too long...*)
qed "function_Union";
goalw ZF.thy [Pi_def]
@@ -323,13 +324,12 @@
Un_upper1 RSN (2, subset_trans),
Un_upper2 RSN (2, subset_trans)];
-goal ZF.thy
- "!!f. [| f: A->B; g: C->D; A Int C = 0 |] ==> \
-\ (f Un g) : (A Un C) -> (B Un D)";
+goal ZF.thy "!!f. [| f: A->B; g: C->D; A Int C = 0 |] \
+\ ==> (f Un g) : (A Un C) -> (B Un D)";
(*Prove the product and domain subgoals using distributive laws*)
by (asm_full_simp_tac (!simpset addsimps [Pi_iff,extension]@Un_rls) 1);
by (rewtac function_def);
-by (Blast_tac 1);
+by (Blast.depth_tac (!claset) 11 1); (*11 secs*)
qed "fun_disjoint_Un";
goal ZF.thy
--- a/src/ZF/mono.ML Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/mono.ML Wed Apr 09 12:37:44 1997 +0200
@@ -13,53 +13,53 @@
(*Not easy to express monotonicity in P, since any "bigger" predicate
would have to be single-valued*)
goal thy "!!A B. A<=B ==> Replace(A,P) <= Replace(B,P)";
-by (fast_tac (!claset addSEs [ReplaceE]) 1);
+by (blast_tac (!claset addSEs [ReplaceE]) 1);
qed "Replace_mono";
goal thy "!!A B. A<=B ==> {f(x). x:A} <= {f(x). x:B}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "RepFun_mono";
goal thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Pow_mono";
goal thy "!!A B. A<=B ==> Union(A) <= Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_mono";
val prems = goal thy
"[| A<=C; !!x. x:A ==> B(x)<=D(x) \
\ |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))";
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
qed "UN_mono";
(*Intersection is ANTI-monotonic. There are TWO premises! *)
goal thy "!!A B. [| A<=B; a:A |] ==> Inter(B) <= Inter(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_anti_mono";
goal thy "!!C D. C<=D ==> cons(a,C) <= cons(a,D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "cons_mono";
goal thy "!!A B C D. [| A<=C; B<=D |] ==> A Un B <= C Un D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_mono";
goal thy "!!A B C D. [| A<=C; B<=D |] ==> A Int B <= C Int D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_mono";
goal thy "!!A B C D. [| A<=C; D<=B |] ==> A-B <= C-D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_mono";
(** Standard products, sums and function spaces **)
goal thy "!!A B C D. [| A<=C; ALL x:A. B(x) <= D(x) |] ==> \
\ Sigma(A,B) <= Sigma(C,D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Sigma_mono_lemma";
val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
@@ -69,7 +69,7 @@
(*Note that B->A and C->A are typically disjoint!*)
goal thy "!!A B C. B<=C ==> A->B <= A->C";
-by (fast_tac (!claset addIs [lam_type] addEs [Pi_lamE]) 1);
+by (blast_tac (!claset addIs [lam_type] addEs [Pi_lamE]) 1);
qed "Pi_mono";
goalw thy [lam_def] "!!A B. A<=B ==> Lambda(A,c) <= Lambda(B,c)";
@@ -84,7 +84,7 @@
goal QPair.thy "!!A B C D. [| A<=C; ALL x:A. B(x) <= D(x) |] ==> \
\ QSigma(A,B) <= QSigma(C,D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "QSigma_mono_lemma";
val QSigma_mono = ballI RSN (2,QSigma_mono_lemma);
@@ -97,35 +97,35 @@
qed "QInr_mono";
goal QPair.thy "!!A B C D. [| A<=C; B<=D |] ==> A <+> B <= C <+> D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "qsum_mono";
(** Converse, domain, range, field **)
goal thy "!!r s. r<=s ==> converse(r) <= converse(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "converse_mono";
goal thy "!!r s. r<=s ==> domain(r)<=domain(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "domain_mono";
bind_thm ("domain_rel_subset", [domain_mono, domain_subset] MRS subset_trans);
goal thy "!!r s. r<=s ==> range(r)<=range(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "range_mono";
bind_thm ("range_rel_subset", [range_mono, range_subset] MRS subset_trans);
goal thy "!!r s. r<=s ==> field(r)<=field(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "field_mono";
goal thy "!!r A. r <= A*A ==> field(r) <= A";
by (etac (field_mono RS subset_trans) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "field_rel_subset";
@@ -133,31 +133,31 @@
val [prem1,prem2] = goal thy
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B";
-by (fast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
qed "image_pair_mono";
val [prem1,prem2] = goal thy
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B";
-by (fast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem1, prem2 RS subsetD]) 1);
qed "vimage_pair_mono";
goal thy "!!r s. [| r<=s; A<=B |] ==> r``A <= s``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "image_mono";
goal thy "!!r s. [| r<=s; A<=B |] ==> r-``A <= s-``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "vimage_mono";
val [sub,PQimp] = goal thy
"[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)";
-by (fast_tac (!claset addIs [sub RS subsetD, PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [sub RS subsetD, PQimp RS mp]) 1);
qed "Collect_mono";
(** Monotonicity of implications -- some could go to FOL **)
goal thy "!!A B x. A<=B ==> x:A --> x:B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "in_mono";
goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";