--- a/src/ZF/AC/AC15_WO6.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC15_WO6.thy Mon Jan 21 11:25:45 2002 +0100
@@ -43,7 +43,7 @@
apply (drule subset_consI [THEN subset_imp_lepoll, THEN lepoll_Finite])
apply (rule nat_not_Finite [THEN notE] )
apply (subgoal_tac "x ~= 0")
-apply (blast intro: lepoll_Sigma [THEN lepoll_Finite] , blast)
+apply (blast intro: lepoll_Sigma [THEN lepoll_Finite], blast)
done
lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
@@ -61,8 +61,7 @@
apply (unfold sets_of_size_between_def)
apply (rule ballI)
apply (erule_tac x="cons(0, B*nat)" in ballE)
- apply (blast dest: lemma1 intro!: lemma2)
-apply blast
+ apply (blast dest: lemma1 intro!: lemma2, blast)
done
lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
@@ -180,7 +179,7 @@
apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
apply simp
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
- elim!: less_Least_subset_x lemma1 lemma2, assumption);
+ elim!: less_Least_subset_x lemma1 lemma2, assumption)
done
@@ -199,7 +198,7 @@
theorem AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)"
apply (unfold AC10_def AC13_def, safe)
apply (erule allE)
-apply (erule impE [OF _ cons_times_nat_not_Finite], assumption);
+apply (erule impE [OF _ cons_times_nat_not_Finite], assumption)
apply (fast elim!: impE [OF _ cons_times_nat_not_Finite]
dest!: ex_fun_AC13_AC15)
done
--- a/src/ZF/AC/AC16_WO4.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Mon Jan 21 11:25:45 2002 +0100
@@ -144,7 +144,7 @@
apply (erule impE)
apply (simp add: add_succ)
apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing)
-apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp);
+apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
apply blast
done
@@ -171,7 +171,7 @@
apply (erule_tac x = "B - {xa}" in allE)
apply (erule impE)
apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll)
-apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp);
+apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
apply blast
done
@@ -361,7 +361,7 @@
(** LEVEL 8 **)
apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE])
apply (blast, assumption+)
-apply (drule equalityD1 [THEN subsetD], (assumption))
+apply (drule equalityD1 [THEN subsetD], assumption)
apply (frule cons_cons_in, assumption+)
apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+
done
@@ -385,7 +385,7 @@
apply (erule exE)
apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption)
apply (simp add: subsets_lepoll_succ)
-apply (drule well_ord_radd, (assumption))
+apply (drule well_ord_radd, assumption)
apply (erule Int_empty [THEN disj_Un_eqpoll_sum,
THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
apply (fast elim!: bij_is_inj [THEN well_ord_rvimage])
@@ -410,9 +410,8 @@
lemma (in AC16) unique_superset_in_MM:
"v \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> w"
-apply (unfold MM_def LL_def, safe)
-apply fast
-apply (rule lepoll_imp_eqpoll_subset [THEN exE], (assumption))
+apply (unfold MM_def LL_def, safe, fast)
+apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
apply (rule_tac x = "x" in all_ex [THEN ballE])
apply (blast intro: eqpoll_sym)+
done
--- a/src/ZF/AC/AC16_lemmas.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC16_lemmas.thy Mon Jan 21 11:25:45 2002 +0100
@@ -40,8 +40,7 @@
apply (fast intro!: RepFunI)
apply (rule subsetI)
apply (erule RepFunE)
-apply (rule CollectI)
-apply fast
+apply (rule CollectI, fast)
apply (fast intro!: singleton_eqpoll_1)
done
@@ -49,10 +48,8 @@
apply (unfold eqpoll_def bij_def)
apply (rule_tac x = "\<lambda>x \<in> X. {x}" in exI)
apply (rule IntI)
-apply (unfold inj_def surj_def)
-apply simp
-apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1])
-apply simp
+apply (unfold inj_def surj_def, simp)
+apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1], simp)
apply (fast intro!: lam_type)
done
@@ -76,15 +73,15 @@
apply (unfold lepoll_def)
apply (rule_tac x = "\<lambda>y \<in> {y \<in> Pow(x) . y\<approx>succ (succ (n))}.
<LEAST i. i \<in> y, y-{LEAST i. i \<in> y}>" in exI)
-apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective);
- apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in);
-apply (simp, blast intro: InfCard_Least_in);
+apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective)
+ apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in)
+apply (simp, blast intro: InfCard_Least_in)
done
lemma set_of_Ord_succ_Union: "(\<forall>y \<in> z. Ord(y)) ==> z \<subseteq> succ(Union(z))"
apply (rule subsetI)
-apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast );
-apply (simp, erule bexE);
+apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast )
+apply (simp, erule bexE)
apply (rule_tac i=xa and j=x in Ord_linear_le)
apply (blast dest: le_imp_subset elim: leE ltE)+
done
@@ -94,8 +91,7 @@
lemma succ_Union_not_mem:
"(!!y. y \<in> z ==> Ord(y)) ==> succ(Union(z)) \<notin> z"
-apply (rule set_of_Ord_succ_Union [THEN subset_not_mem]);
-apply blast
+apply (rule set_of_Ord_succ_Union [THEN subset_not_mem], blast)
done
lemma Union_cons_eq_succ_Union:
@@ -115,35 +111,31 @@
apply (intro allI impI)
apply (erule natE)
apply (fast dest!: eqpoll_1_iff_singleton [THEN iffD1]
- intro!: Union_singleton)
-apply (clarify );
+ intro!: Union_singleton, clarify)
apply (elim not_emptyE)
apply (erule_tac x = "z-{xb}" in allE)
apply (erule impE)
apply (fast elim!: Diff_sing_eqpoll
Diff_sing_eqpoll [THEN eqpoll_succ_imp_not_empty])
-apply (subgoal_tac "xb \<union> \<Union>(z - {xb}) \<in> z");
-apply (simp add: Union_eq_Un [symmetric]);
+apply (subgoal_tac "xb \<union> \<Union>(z - {xb}) \<in> z")
+apply (simp add: Union_eq_Un [symmetric])
apply (frule bspec, assumption)
-apply (drule bspec);
-apply (erule Diff_subset [THEN subsetD]);
-apply (drule Un_Ord_disj, assumption)
-apply (auto );
+apply (drule bspec)
+apply (erule Diff_subset [THEN subsetD])
+apply (drule Un_Ord_disj, assumption, auto)
done
lemma Union_in: "[| \<forall>x \<in> z. Ord(x); z\<approx>n; z\<noteq>0; n \<in> nat |] ==> Union(z) \<in> z"
-apply (blast intro: Union_in_lemma);
-done
+by (blast intro: Union_in_lemma)
lemma succ_Union_in_x:
"[| InfCard(x); z \<in> Pow(x); z\<approx>n; n \<in> nat |] ==> succ(Union(z)) \<in> x"
-apply (rule Limit_has_succ [THEN ltE]);
+apply (rule Limit_has_succ [THEN ltE])
prefer 3 apply assumption
apply (erule InfCard_is_Limit)
-apply (case_tac "z=0");
-apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0]);
-apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]]);
-apply assumption;
+apply (case_tac "z=0")
+apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0])
+apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]], assumption)
apply (blast intro: Union_in
InfCard_is_Card [THEN Card_is_Ord, THEN Ord_in_Ord])+
done
@@ -151,18 +143,18 @@
lemma succ_lepoll_succ_succ:
"[| InfCard(x); n \<in> nat |]
==> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
-apply (unfold lepoll_def);
+apply (unfold lepoll_def)
apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(Union(z)), z)"
in exI)
apply (rule_tac d = "%z. z-{Union (z) }" in lam_injective)
apply (blast intro!: succ_Union_in_x succ_Union_not_mem
intro: cons_eqpoll_succ Ord_in_Ord
dest!: InfCard_is_Card [THEN Card_is_Ord])
-apply (simp only: Union_cons_eq_succ_Union);
-apply (rule cons_Diff_eq);
+apply (simp only: Union_cons_eq_succ_Union)
+apply (rule cons_Diff_eq)
apply (fast dest!: InfCard_is_Card [THEN Card_is_Ord]
elim: Ord_in_Ord
- intro!: succ_Union_not_mem);
+ intro!: succ_Union_not_mem)
done
lemma subsets_eqpoll_X:
@@ -170,9 +162,9 @@
apply (induct_tac "n")
apply (rule subsets_eqpoll_1_eqpoll)
apply (rule eqpollI)
-apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+);
-apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll]);
- apply (erule eqpoll_refl [THEN prod_eqpoll_cong]);
+apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+)
+apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll])
+ apply (erule eqpoll_refl [THEN prod_eqpoll_cong])
apply (erule InfCard_square_eqpoll)
apply (fast elim: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
intro!: succ_lepoll_succ_succ)
@@ -185,8 +177,7 @@
done
lemma vimage_image_eq: "[| f \<in> inj(A,B); y \<subseteq> A |] ==> converse(f)``(f``y) = y"
-apply (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)
-done
+by (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)
lemma subsets_eqpoll:
"A\<approx>B ==> {Y \<in> Pow(A). Y\<approx>n}\<approx>{Y \<in> Pow(B). Y\<approx>n}"
@@ -222,10 +213,10 @@
lemma WO2_infinite_subsets_eqpoll_X: "[| WO2; n \<in> nat; ~Finite(X) |]
==> {Y \<in> Pow(X). Y\<approx>succ(n)}\<approx>X"
apply (drule WO2_imp_ex_Card)
-apply (elim allE exE conjE);
+apply (elim allE exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (drule infinite_Card_is_InfCard, assumption)
-apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans);
+apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans)
done
lemma well_ord_imp_ex_Card: "well_ord(X,R) ==> \<exists>a. Card(a) & X\<approx>a"
@@ -238,7 +229,7 @@
apply (elim allE exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (drule infinite_Card_is_InfCard, assumption)
-apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans);
+apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans)
done
end
--- a/src/ZF/AC/AC18_AC19.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC18_AC19.thy Mon Jan 21 11:25:45 2002 +0100
@@ -66,7 +66,7 @@
lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a"
apply clarify
-apply (rule subst_elem , (assumption))
+apply (rule subst_elem, assumption)
apply (fast elim: notE subst_elem)
done
@@ -98,10 +98,9 @@
apply (case_tac "A=0", force)
apply (erule_tac x = "{uu (a) . a \<in> A}" in allE)
apply (erule impE)
-apply (erule RepRep_conj , (assumption))
+apply (erule RepRep_conj, assumption)
apply (rule lemma1)
-apply (drule lemma2 , (assumption))
-apply auto
+apply (drule lemma2, assumption, auto)
done
end
--- a/src/ZF/AC/AC_Equiv.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Mon Jan 21 11:25:45 2002 +0100
@@ -139,7 +139,7 @@
apply (unfold rvimage_def)
apply (rule equalityI, safe)
apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst],
- (assumption))
+ assumption)
apply (drule_tac P = "%a. <a,ya>:r" in id_conv [THEN subst], (assumption+))
apply (fast intro: id_conv [THEN ssubst])
done
@@ -179,7 +179,7 @@
lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
apply (unfold surj_def)
apply (erule CollectE)
-apply (rule image_fun [THEN ssubst], (assumption), rule subset_refl)
+apply (rule image_fun [THEN ssubst], assumption, rule subset_refl)
apply (blast dest: apply_type)
done
@@ -217,7 +217,7 @@
apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord]
inj_is_fun [THEN apply_type])
apply (erule domainE)
-apply (frule inj_is_fun [THEN apply_type], (assumption))
+apply (frule inj_is_fun [THEN apply_type], assumption)
apply (rule LeastI2)
apply (auto elim!: nat_into_Ord [THEN Ord_in_Ord])
done
--- a/src/ZF/AC/Cardinal_aux.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/Cardinal_aux.thy Mon Jan 21 11:25:45 2002 +0100
@@ -8,7 +8,7 @@
theory Cardinal_aux = AC_Equiv:
lemma Diff_lepoll: "[| A \<lesssim> succ(m); B \<subseteq> A; B\<noteq>0 |] ==> A-B \<lesssim> m"
-apply (rule not_emptyE, (assumption))
+apply (rule not_emptyE, assumption)
apply (blast intro: lepoll_trans [OF subset_imp_lepoll Diff_sing_lepoll])
done
@@ -151,7 +151,7 @@
~Finite(a); Ord(a); n \<in> nat |]
==> (\<Union>b \<in> a. F(b)) \<lesssim> a"
apply (rule rev_mp)
-apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll);
+apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll)
apply auto
done
@@ -187,7 +187,7 @@
apply (drule Un_least_lt, assumption)
apply (drule eqpoll_imp_lepoll [THEN lepoll_trans],
rule le_imp_lepoll, assumption)+
-apply (case_tac "Finite(x Un xa)");
+apply (case_tac "Finite(x Un xa)")
txt{*finite case*}
apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+)
apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite])
--- a/src/ZF/AC/DC.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/DC.thy Mon Jan 21 11:25:45 2002 +0100
@@ -363,8 +363,7 @@
apply (unfold XX_def)
apply (drule apply_type, assumption)
apply (elim UN_E CollectE)
-apply (drule domain_of_fun [symmetric, THEN trans], assumption)
-apply simp
+apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
done
lemma (in imp_DC0) restrict_cons_eq_restrict:
@@ -404,7 +403,7 @@
(*induction step*) (** LEVEL 5 **)
(*prevent simplification of ~\<exists> to \<forall>~ *)
apply (simp only: separation split)
-apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI);
+apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI)
apply (elim conjE disjE)
apply (force elim!: trans subst_context
intro!: UN_image_succ_eq_succ)
@@ -455,8 +454,7 @@
apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
apply (unfold allRR_def)
apply (drule ospec)
-apply (drule ltI [OF nat_succI Ord_nat], assumption)
-apply simp
+apply (drule ltI [OF nat_succI Ord_nat], assumption, simp)
apply (elim conjE ballE)
apply (erule restrict_eq_imp_val_eq [symmetric], force)
apply (simp add: image_fun OrdmemD)
@@ -500,7 +498,7 @@
theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
apply (unfold DC_def WO3_def)
apply (rule allI)
-apply (case_tac "A \<prec> Hartog (A)");
+apply (case_tac "A \<prec> Hartog (A)")
apply (fast dest!: lesspoll_imp_ex_lt_eqpoll
intro!: Ord_Hartog leI [THEN le_imp_subset])
apply (erule allE impE)+
--- a/src/ZF/AC/HH.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/HH.thy Mon Jan 21 11:25:45 2002 +0100
@@ -239,8 +239,7 @@
apply (rule bij_Least_HH_x [THEN bij_converse_bij])
apply (rule f_subsets_imp_UN_HH_eq_x)
apply (intro ballI apply_type)
-apply (fast intro: lam_type apply_type del: DiffE)
-apply assumption;
+apply (fast intro: lam_type apply_type del: DiffE, assumption)
apply (fast intro: Pi_weaken_type)
done
--- a/src/ZF/AC/Hartog.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/Hartog.thy Mon Jan 21 11:25:45 2002 +0100
@@ -25,7 +25,7 @@
apply (erule inj_is_fun [THEN fun_is_rel, THEN image_subset])
apply (rule well_ord_rvimage [OF bij_is_inj well_ord_Memrel])
apply (erule restrict_bij [THEN bij_converse_bij])
-apply (rule subset_refl, assumption);
+apply (rule subset_refl, assumption)
apply (rule trans)
apply (rule bij_ordertype_vimage)
apply (erule restrict_bij [THEN bij_converse_bij])
@@ -36,8 +36,7 @@
lemma Ord_lepoll_imp_eq_ordertype:
"[| Ord(a); a \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & (\<exists>R. R \<subseteq> X*X & ordertype(Y,R)=a)"
-apply (drule Ord_lepoll_imp_ex_well_ord, (assumption))
-apply clarify
+apply (drule Ord_lepoll_imp_ex_well_ord, assumption, clarify)
apply (intro exI conjI)
apply (erule_tac [3] ordertype_Int, auto)
done
--- a/src/ZF/AC/WO1_WO7.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/WO1_WO7.thy Mon Jan 21 11:25:45 2002 +0100
@@ -50,7 +50,7 @@
lemma converse_Memrel_not_wf_on:
"[| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"
apply (unfold wf_on_def wf_def)
-apply (drule nat_le_infinite_Ord [THEN le_imp_subset], (assumption))
+apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
apply (rule notI)
apply (erule_tac x = "nat" in allE, blast)
done
--- a/src/ZF/AC/WO2_AC16.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Mon Jan 21 11:25:45 2002 +0100
@@ -31,8 +31,7 @@
(* ********************************************************************** *)
lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0"
-apply (simp add: recfunAC16_def);
-done
+by (simp add: recfunAC16_def)
lemma recfunAC16_succ:
"recfunAC16(f,h,succ(i),a) =
@@ -41,7 +40,7 @@
{f ` (LEAST j. h ` i \<subseteq> f ` j &
(\<forall>b<a. (h`b \<subseteq> f`j
--> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
-apply (simp add: recfunAC16_def);
+apply (simp add: recfunAC16_def)
done
lemma recfunAC16_Limit: "Limit(i)
@@ -55,12 +54,11 @@
lemma transrec2_mono_lemma [rule_format]:
"[| !!g r. r \<subseteq> B(g,r); Ord(i) |]
==> j<i --> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
-apply (erule trans_induct);
-apply (rule Ord_cases , assumption+);
-apply fast
+apply (erule trans_induct)
+apply (rule Ord_cases, assumption+, fast)
apply (simp (no_asm_simp))
-apply (blast elim!: leE);
-apply (simp add: transrec2_Limit);
+apply (blast elim!: leE)
+apply (simp add: transrec2_Limit)
apply (blast intro: OUN_I ltI Ord_in_Ord [THEN le_refl]
elim!: Limit_has_succ [THEN ltE])
done
@@ -68,9 +66,9 @@
lemma transrec2_mono:
"[| !!g r. r \<subseteq> B(g,r); j\<le>i |]
==> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
-apply (erule leE);
+apply (erule leE)
apply (rule transrec2_mono_lemma)
-apply (auto intro: lt_Ord2 );
+apply (auto intro: lt_Ord2 )
done
(* ********************************************************************** *)
@@ -80,8 +78,7 @@
lemma recfunAC16_mono:
"i\<le>j ==> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)"
apply (unfold recfunAC16_def)
-apply (rule transrec2_mono)
-apply (auto );
+apply (rule transrec2_mono, auto)
done
(* ********************************************************************** *)
@@ -95,8 +92,7 @@
V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]
==> V = W"
apply (erule asm_rl allE impE)+
-apply (drule subsetD, assumption)
-apply blast
+apply (drule subsetD, assumption, blast)
done
@@ -118,8 +114,7 @@
==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) -->
(\<exists>! Y. Y \<in> F(y) & h(z) \<subseteq> Y)"
apply (intro oallI impI)
-apply (drule ospec, assumption)
-apply clarify
+apply (drule ospec, assumption, clarify)
apply (blast elim!: oallE )
done
@@ -134,8 +129,7 @@
apply (rule conjI)
apply (rule subsetI)
apply (erule OUN_E)
-apply (drule ospec, assumption)
-apply fast
+apply (drule ospec, assumption, fast)
apply (drule lemma4, assumption)
apply (rule oallI)
apply (rule impI)
@@ -314,7 +308,7 @@
apply (simp add: Union_recfunAC16_lesspoll)
apply (rule Finite_lesspoll_infinite_Ord)
apply (rule Finite_def [THEN def_imp_iff, THEN iffD2])
-apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption);
+apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)
apply (blast intro: Card_is_Ord)
done;
@@ -528,7 +522,7 @@
apply (erule imageE)
apply (drule ltI, erule Limit_is_Ord)
apply (drule Limit_has_succ, assumption)
-apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption);
+apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption)
apply (erule conjE)
apply (drule ospec)
(** LEVEL 10 **)
@@ -559,8 +553,7 @@
apply (rule allI)
apply (rule impI)
apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
-apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp)
-apply simp
+apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp, simp)
apply (frule WO2_imp_ex_Card)
apply (elim exE conjE)
apply (drule eqpoll_trans [THEN eqpoll_sym,
--- a/src/ZF/AC/WO6_WO1.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Mon Jan 21 11:25:45 2002 +0100
@@ -446,9 +446,7 @@
(* ********************************************************************** *)
lemma WO6_imp_NN_not_empty: "WO6 ==> NN(y) \<noteq> 0"
-apply (unfold WO6_def NN_def, clarify)
-apply blast
-done
+by (unfold WO6_def NN_def, clarify, blast)
(* ********************************************************************** *)
(* 1 \<in> NN(y) ==> y can be well-ordered *)
--- a/src/ZF/CardinalArith.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/CardinalArith.thy Mon Jan 21 11:25:45 2002 +0100
@@ -45,8 +45,7 @@
lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
apply (erule trans_induct3 [of j])
apply (simp_all add: oadd_Limit)
-apply (simp add: Union_empty_iff Limit_def lt_def)
-apply blast
+apply (simp add: Union_empty_iff Limit_def lt_def, blast)
done
lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
@@ -66,8 +65,7 @@
apply (rule Ord_0_lt)
apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
apply (force simp add: Union_empty_iff oadd_eq_0_iff
- Limit_is_Ord [of j, THEN Ord_in_Ord])
-apply auto
+ Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
apply (rule_tac x="succ(x)" in bexI)
apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
apply (simp add: Limit_def lt_def)
@@ -110,7 +108,7 @@
apply (erule eqpollE)
apply (rule succ_lepoll_natE)
apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll]
- lepoll_trans, assumption);
+ lepoll_trans, assumption)
done
lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
@@ -133,12 +131,12 @@
apply (rule allI)
apply (rule impI)
apply (erule conjE)
-apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], (assumption))
-apply (frule Diff_sing_eqpoll, (assumption))
+apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
+apply (frule Diff_sing_eqpoll, assumption)
apply (erule allE)
apply (erule impE, fast)
-apply (drule subsetD, (assumption))
-apply (drule Fin.consI, (assumption))
+apply (drule subsetD, assumption)
+apply (drule Fin.consI, assumption)
apply (simp add: cons_Diff)
done
--- a/src/ZF/Main.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/Main.thy Mon Jan 21 11:25:45 2002 +0100
@@ -60,9 +60,9 @@
(* belongs to theory CardinalArith *)
lemma InfCard_square_eqpoll: "InfCard(K) \<Longrightarrow> K \<times> K \<approx> K"
-apply (rule well_ord_InfCard_square_eq);
- apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]);
-apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]);
+apply (rule well_ord_InfCard_square_eq)
+ apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel])
+apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq])
done
lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
--- a/src/ZF/OrdQuant.thy Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/OrdQuant.thy Mon Jan 21 11:25:45 2002 +0100
@@ -45,8 +45,7 @@
lemma Union_upper_le:
"\<lbrakk>j: J; i\<le>j; Ord(\<Union>(J))\<rbrakk> \<Longrightarrow> i \<le> \<Union>J"
apply (subst Union_eq_UN)
-apply (rule UN_upper_le)
-apply auto
+apply (rule UN_upper_le, auto)
done
lemma zero_not_Limit [iff]: "~ Limit(0)"
@@ -61,8 +60,7 @@
done
lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
-apply (simp add: Limit_def lt_Ord2)
-apply clarify
+apply (simp add: Limit_def lt_Ord2, clarify)
apply (drule_tac i=y in ltD)
apply (blast intro: lt_trans1 succ_leI ltI lt_Ord2)
done
@@ -115,8 +113,7 @@
lemma OUN_upper_le:
"\<lbrakk>a<A; i\<le>b(a); Ord(\<Union>x<A. b(x))\<rbrakk> \<Longrightarrow> i \<le> (\<Union>x<A. b(x))"
-apply (unfold OUnion_def)
-apply auto
+apply (unfold OUnion_def, auto)
apply (rule UN_upper_le )
apply (auto simp add: lt_def)
done