--- a/src/ZF/AC/AC15_WO6.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC15_WO6.thy Tue Sep 27 17:54:20 2022 +0100
@@ -32,7 +32,7 @@
(* ********************************************************************** *)
lemma lepoll_Sigma: "A\<noteq>0 \<Longrightarrow> B \<lesssim> A*B"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (erule not_emptyE)
apply (rule_tac x = "\<lambda>z \<in> B. \<langle>x,z\<rangle>" in exI)
apply (fast intro!: snd_conv lam_injective)
@@ -58,14 +58,14 @@
sets_of_size_between(f`B, 2, n) \<and> \<Union>(f`B)=B
\<Longrightarrow> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) \<and> u \<subseteq> cons(0, B*nat) \<and>
0 \<in> u \<and> 2 \<lesssim> u \<and> u \<lesssim> n"
-apply (unfold sets_of_size_between_def)
+ unfolding sets_of_size_between_def
apply (rule ballI)
apply (erule_tac x="cons(0, B*nat)" in ballE)
apply (blast dest: lemma1 intro!: lemma2, blast)
done
lemma lemma4: "\<lbrakk>A \<lesssim> i; Ord(i)\<rbrakk> \<Longrightarrow> {P(a). a \<in> A} \<lesssim> i"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (erule exE)
apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). \<mu> j. \<exists>a\<in>A. x=P(a) \<and> f`a=j"
in exI)
@@ -227,7 +227,7 @@
(* ********************************************************************** *)
lemma AC13_mono: "\<lbrakk>m\<le>n; AC13(m)\<rbrakk> \<Longrightarrow> AC13(n)"
-apply (unfold AC13_def)
+ unfolding AC13_def
apply (drule le_imp_lepoll)
apply (fast elim!: lepoll_trans)
done
--- a/src/ZF/AC/AC16_WO4.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Tue Sep 27 17:54:20 2022 +0100
@@ -18,7 +18,7 @@
"\<lbrakk>Finite(A); 0<m; m \<in> nat\<rbrakk>
\<Longrightarrow> \<exists>a f. Ord(a) \<and> domain(f) = a \<and>
(\<Union>b<a. f`b) = A \<and> (\<forall>b<a. f`b \<lesssim> m)"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (erule bexE)
apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
apply (erule exE)
@@ -345,7 +345,7 @@
"\<lbrakk>z \<in> xa \<inter> (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x\<rbrakk>
\<Longrightarrow> \<exists>! w. w \<in> t_n \<and> cons(z, cons(u, a)) \<subseteq> w"
apply (rule all_ex [THEN bspec])
-apply (unfold k_def)
+ unfolding k_def
apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym)
done
@@ -442,12 +442,12 @@
lemma the_in_MM_subset:
"v \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> v \<subseteq> x) \<subseteq> x \<union> y"
apply (drule unique_superset1)
-apply (unfold MM_def)
+ unfolding MM_def
apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
done
lemma GG_subset: "v \<in> LL \<Longrightarrow> GG ` v \<subseteq> x"
-apply (unfold GG_def)
+ unfolding GG_def
apply (frule the_in_MM_subset)
apply (frule in_LL_eq_Int)
apply (force elim: equalityE)
@@ -473,7 +473,7 @@
apply (rule ccontr)
apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v \<inter> y")
prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
-apply (unfold k_def)
+ unfolding k_def
apply (insert all_ex "includes" lnat)
apply (rule ex_subset_eqpoll_n [THEN exE], assumption)
apply (rule noLepoll [THEN notE])
@@ -489,7 +489,7 @@
apply (rule exists_in_MM [THEN bexE], assumption)
apply (rule bexI)
apply (erule_tac [2] Int_in_LL)
-apply (unfold GG_def)
+ unfolding GG_def
apply (simp add: Int_in_LL)
apply (subst unique_superset_in_MM [THEN the_equality2])
apply (fast elim!: Int_in_LL)+
@@ -516,7 +516,7 @@
(* ********************************************************************** *)
lemma in_MM_eqpoll_n: "w \<in> MM \<Longrightarrow> w \<approx> succ(k #+ m)"
-apply (unfold MM_def)
+ unfolding MM_def
apply (fast dest: "includes" [THEN subsetD])
done
@@ -529,7 +529,7 @@
lemma all_in_lepoll_m:
"well_ord(LL,S) \<Longrightarrow>
\<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) \<lesssim> m"
-apply (unfold GG_def)
+ unfolding GG_def
apply (rule oallI)
apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type])
apply (insert "includes")
--- a/src/ZF/AC/AC16_lemmas.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC16_lemmas.thy Tue Sep 27 17:54:20 2022 +0100
@@ -12,7 +12,7 @@
by fast
lemma nat_1_lepoll_iff: "1\<lesssim>X \<longleftrightarrow> (\<exists>x. x \<in> X)"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule iffI)
apply (fast intro: inj_is_fun [THEN apply_type])
apply (erule exE)
@@ -29,7 +29,7 @@
done
lemma cons_eqpoll_succ: "\<lbrakk>x\<approx>n; y\<notin>x\<rbrakk> \<Longrightarrow> cons(y,x)\<approx>succ(n)"
-apply (unfold succ_def)
+ unfolding succ_def
apply (fast elim!: cons_eqpoll_cong mem_irrefl)
done
@@ -71,7 +71,7 @@
lemma subsets_lepoll_lemma1:
"\<lbrakk>InfCard(x); n \<in> nat\<rbrakk>
\<Longrightarrow> {y \<in> Pow(x). y\<approx>succ(succ(n))} \<lesssim> x*{y \<in> Pow(x). y\<approx>succ(n)}"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule_tac x = "\<lambda>y \<in> {y \<in> Pow(x) . y\<approx>succ (succ (n))}.
<\<mu> i. i \<in> y, y-{\<mu> i. i \<in> y}>" in exI)
apply (rule_tac d = "\<lambda>z. cons (fst(z), snd(z))" in lam_injective)
@@ -144,7 +144,7 @@
lemma succ_lepoll_succ_succ:
"\<lbrakk>InfCard(x); n \<in> nat\<rbrakk>
\<Longrightarrow> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
-apply (unfold lepoll_def)
+ unfolding 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 = "\<lambda>z. z-{\<Union>(z) }" in lam_injective)
@@ -173,7 +173,7 @@
lemma image_vimage_eq:
"\<lbrakk>f \<in> surj(A,B); y \<subseteq> B\<rbrakk> \<Longrightarrow> f``(converse(f)``y) = y"
-apply (unfold surj_def)
+ unfolding surj_def
apply (fast dest: apply_equality2 elim: apply_iff [THEN iffD2])
done
@@ -182,7 +182,7 @@
lemma subsets_eqpoll:
"A\<approx>B \<Longrightarrow> {Y \<in> Pow(A). Y\<approx>n}\<approx>{Y \<in> Pow(B). Y\<approx>n}"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (erule exE)
apply (rule_tac x = "\<lambda>X \<in> {Y \<in> Pow (A) . \<exists>f. f \<in> bij (Y, n) }. f``X" in exI)
apply (rule_tac d = "\<lambda>Z. converse (f) ``Z" in lam_bijective)
@@ -197,7 +197,7 @@
done
lemma WO2_imp_ex_Card: "WO2 \<Longrightarrow> \<exists>a. Card(a) \<and> X\<approx>a"
-apply (unfold WO2_def)
+ unfolding WO2_def
apply (drule spec [of _ X])
apply (blast intro: Card_cardinal eqpoll_trans
well_ord_Memrel [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
@@ -207,7 +207,7 @@
by (blast intro: lepoll_Finite)
lemma infinite_Card_is_InfCard: "\<lbrakk>\<not>Finite(X); Card(X)\<rbrakk> \<Longrightarrow> InfCard(X)"
-apply (unfold InfCard_def)
+ unfolding InfCard_def
apply (fast elim!: Card_is_Ord [THEN nat_le_infinite_Ord])
done
--- a/src/ZF/AC/AC17_AC1.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC17_AC1.thy Tue Sep 27 17:54:20 2022 +0100
@@ -71,7 +71,7 @@
lemma not_AC1_imp_ex:
"\<not>AC1 \<Longrightarrow> \<exists>A. \<forall>f \<in> Pow(A)-{0} -> A. \<exists>u \<in> Pow(A)-{0}. f`u \<notin> u"
-apply (unfold AC1_def)
+ unfolding AC1_def
apply (erule swap)
apply (rule allI)
apply (erule swap)
@@ -112,7 +112,7 @@
by simp
lemma AC17_AC1: "AC17 \<Longrightarrow> AC1"
-apply (unfold AC17_def)
+ unfolding AC17_def
apply (rule classical)
apply (erule not_AC1_imp_ex [THEN exE])
apply (case_tac
--- a/src/ZF/AC/AC18_AC19.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC18_AC19.thy Tue Sep 27 17:54:20 2022 +0100
@@ -36,7 +36,7 @@
done
lemma AC1_AC18: "AC1 \<Longrightarrow> PROP AC18"
-apply (unfold AC1_def)
+ unfolding AC1_def
apply (rule AC18.intro)
apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)
done
@@ -46,7 +46,7 @@
(* ********************************************************************** *)
theorem (in AC18) AC19
-apply (unfold AC19_def)
+ unfolding AC19_def
apply (intro allI impI)
apply (rule AC18 [of _ "\<lambda>x. x", THEN mp], blast)
done
--- a/src/ZF/AC/AC7_AC9.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC7_AC9.thy Tue Sep 27 17:54:20 2022 +0100
@@ -22,7 +22,7 @@
"C \<in> A \<Longrightarrow> (\<lambda>g \<in> (nat->\<Union>(A))*C.
(\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1))))
\<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
-apply (unfold inj_def)
+ unfolding inj_def
apply (rule CollectI)
apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto)
apply (rule fun_extension, assumption+)
--- a/src/ZF/AC/AC_Equiv.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Tue Sep 27 17:54:20 2022 +0100
@@ -138,7 +138,7 @@
(* lemma for ordertype_Int *)
lemma rvimage_id: "rvimage(A,id(A),r) = r \<inter> A*A"
-apply (unfold rvimage_def)
+ unfolding rvimage_def
apply (rule equalityI, safe)
apply (drule_tac P = "\<lambda>a. <id (A) `xb,a>:r" in id_conv [THEN subst],
assumption)
@@ -194,7 +194,7 @@
(*Using AC we could trivially prove, for all u, domain(u) \<lesssim> u*)
lemma lepoll_m_imp_domain_lepoll_m:
"\<lbrakk>m \<in> nat; u \<lesssim> m\<rbrakk> \<Longrightarrow> domain(u) \<lesssim> m"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (erule exE)
apply (rule_tac x = "\<lambda>x \<in> domain(u). \<mu> i. \<exists>y. \<langle>x,y\<rangle> \<in> u \<and> f`\<langle>x,y\<rangle> = i"
in exI)
--- a/src/ZF/AC/Cardinal_aux.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/Cardinal_aux.thy Tue Sep 27 17:54:20 2022 +0100
@@ -99,7 +99,7 @@
by blast
lemma UN_sing_lepoll: "Ord(a) \<Longrightarrow> (\<Union>x \<in> a. {P(x)}) \<lesssim> a"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (\<mu> i. P (i) =z) " in exI)
apply (rule_tac d = "\<lambda>z. P (z) " in lam_injective)
apply (fast intro!: Least_in_Ord)
--- a/src/ZF/AC/DC.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/DC.thy Tue Sep 27 17:54:20 2022 +0100
@@ -9,7 +9,7 @@
begin
lemma RepFun_lepoll: "Ord(a) \<Longrightarrow> {P(b). b \<in> a} \<lesssim> a"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . \<mu> i. z=P (i) " in exI)
apply (rule_tac d="\<lambda>z. P (z)" in lam_injective)
apply (fast intro!: Least_in_Ord)
@@ -19,7 +19,7 @@
text\<open>Trivial in the presence of AC, but here we need a wellordering of X\<close>
lemma image_Ord_lepoll: "\<lbrakk>f \<in> X->Y; Ord(X)\<rbrakk> \<Longrightarrow> f``X \<lesssim> X"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule_tac x = "\<lambda>x \<in> f``X. \<mu> y. f`y = x" in exI)
apply (rule_tac d = "\<lambda>z. f`z" in lam_injective)
apply (fast intro!: Least_in_Ord apply_equality, clarify)
@@ -34,7 +34,7 @@
by blast
lemma cons_fun_type: "g \<in> n->X \<Longrightarrow> cons(\<langle>n,x\<rangle>, g) \<in> succ(n) -> cons(x, X)"
-apply (unfold succ_def)
+ unfolding succ_def
apply (fast intro!: fun_extend elim!: mem_irrefl)
done
@@ -352,7 +352,7 @@
lemma f_n_type:
"\<lbrakk>domain(f`n) = succ(k); f \<in> nat -> XX; n \<in> nat\<rbrakk>
\<Longrightarrow> f`n \<in> succ(k) -> domain(R)"
-apply (unfold XX_def)
+ unfolding XX_def
apply (drule apply_type, assumption)
apply (fast elim: domain_eq_imp_fun_type)
done
@@ -360,7 +360,7 @@
lemma f_n_pairs_in_R [rule_format]:
"\<lbrakk>h \<in> nat -> XX; domain(h`n) = succ(k); n \<in> nat\<rbrakk>
\<Longrightarrow> \<forall>i \<in> k. <h`n`i, h`n`succ(i)> \<in> R"
-apply (unfold XX_def)
+ unfolding XX_def
apply (drule apply_type, assumption)
apply (elim UN_E CollectE)
apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
@@ -369,7 +369,7 @@
lemma restrict_cons_eq_restrict:
"\<lbrakk>restrict(h, domain(u))=u; h \<in> n->X; domain(u) \<subseteq> n\<rbrakk>
\<Longrightarrow> restrict(cons(\<langle>n, y\<rangle>, h), domain(u)) = u"
-apply (unfold restrict_def)
+ unfolding restrict_def
apply (simp add: restrict_def Pi_iff)
apply (erule sym [THEN trans, symmetric])
apply (blast elim: mem_irrefl)
@@ -437,13 +437,13 @@
lemma lemma2:
"\<lbrakk>allRR; f \<in> nat->XX; range(R) \<subseteq> domain(R); x \<in> domain(R); n \<in> nat\<rbrakk>
\<Longrightarrow> f`n \<in> succ(n) -> domain(R) \<and> (\<forall>i \<in> n. <f`n`i, f`n`succ(i)>:R)"
-apply (unfold allRR_def)
+ unfolding allRR_def
apply (drule ospec)
apply (erule ltI [OF _ Ord_nat])
apply (erule CollectE, simp)
apply (rule conjI)
prefer 2 apply (fast elim!: f_n_pairs_in_R trans subst_context)
-apply (unfold XX_def)
+ unfolding XX_def
apply (fast elim!: trans [THEN domain_eq_imp_fun_type] subst_context)
done
@@ -451,7 +451,7 @@
"\<lbrakk>allRR; f \<in> nat->XX; n\<in>nat; range(R) \<subseteq> domain(R); x \<in> domain(R)\<rbrakk>
\<Longrightarrow> f`n`n = f`succ(n)`n"
apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
-apply (unfold allRR_def)
+ unfolding allRR_def
apply (drule ospec)
apply (drule ltI [OF nat_succI Ord_nat], assumption, simp)
apply (elim conjE ballE)
@@ -497,7 +497,7 @@
by (fast elim!: image_fun [THEN ssubst])
lemma lesspoll_lemma: "\<lbrakk>\<not> A \<prec> B; C \<prec> B\<rbrakk> \<Longrightarrow> A - C \<noteq> 0"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
intro!: eqpollI elim: notE
elim!: eqpollE lepoll_trans)
--- a/src/ZF/AC/HH.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/HH.thy Tue Sep 27 17:54:20 2022 +0100
@@ -196,7 +196,7 @@
f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x}\<rbrakk>
\<Longrightarrow> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))
\<in> bij(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})"
-apply (unfold bij_def)
+ unfolding bij_def
apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing)
done
--- a/src/ZF/AC/Hartog.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/Hartog.thy Tue Sep 27 17:54:20 2022 +0100
@@ -20,7 +20,7 @@
lemma Ord_lepoll_imp_ex_well_ord:
"\<lbrakk>Ord(a); a \<lesssim> X\<rbrakk>
\<Longrightarrow> \<exists>Y. Y \<subseteq> X \<and> (\<exists>R. well_ord(Y,R) \<and> ordertype(Y,R)=a)"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (erule exE)
apply (intro exI conjI)
apply (erule inj_is_fun [THEN fun_is_rel, THEN image_subset])
@@ -60,7 +60,7 @@
done
lemma not_Hartog_lepoll_self: "\<not> Hartog(A) \<lesssim> A"
-apply (unfold Hartog_def)
+ unfolding Hartog_def
apply (rule ex_Ord_not_lepoll [THEN exE])
apply (rule LeastI, auto)
done
--- a/src/ZF/AC/WO1_AC.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO1_AC.thy Tue Sep 27 17:54:20 2022 +0100
@@ -40,7 +40,7 @@
(* ********************************************************************** *)
lemma lemma1: "\<lbrakk>WO1; \<forall>B \<in> A. \<exists>C \<in> D(B). P(C,B)\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>B \<in> A. P(f`B,B)"
-apply (unfold WO1_def)
+ unfolding WO1_def
apply (erule_tac x = "\<Union>({{C \<in> D (B) . P (C,B) }. B \<in> A}) " in allE)
apply (erule exE, drule ex_choice_fun, fast)
apply (erule exE)
@@ -49,7 +49,7 @@
done
lemma lemma2_1: "\<lbrakk>\<not>Finite(B); WO1\<rbrakk> \<Longrightarrow> |B| + |B| \<approx> B"
-apply (unfold WO1_def)
+ unfolding WO1_def
apply (rule eqpoll_trans)
prefer 2 apply (fast elim!: well_ord_cardinal_eqpoll)
apply (rule eqpoll_sym [THEN eqpoll_trans])
@@ -67,7 +67,7 @@
lemma lemma2_3:
"f \<in> bij(D+D, B) \<Longrightarrow> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i \<in> D})"
-apply (unfold pairwise_disjoint_def)
+ unfolding pairwise_disjoint_def
apply (blast dest: bij_is_inj [THEN inj_apply_equality])
done
@@ -98,7 +98,7 @@
done
theorem WO1_AC10: "\<lbrakk>WO1; 1\<le>n\<rbrakk> \<Longrightarrow> AC10(n)"
-apply (unfold AC10_def)
+ unfolding AC10_def
apply (fast intro!: lemma1 elim!: lemma2)
done
--- a/src/ZF/AC/WO1_WO7.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO1_WO7.thy Tue Sep 27 17:54:20 2022 +0100
@@ -57,7 +57,7 @@
lemma converse_Memrel_not_well_ord:
"\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>well_ord(a,converse(Memrel(a)))"
-apply (unfold well_ord_def)
+ unfolding well_ord_def
apply (blast dest: converse_Memrel_not_wf_on)
done
--- a/src/ZF/AC/WO2_AC16.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Tue Sep 27 17:54:20 2022 +0100
@@ -76,7 +76,7 @@
lemma recfunAC16_mono:
"i\<le>j \<Longrightarrow> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)"
-apply (unfold recfunAC16_def)
+ unfolding recfunAC16_def
apply (rule transrec2_mono, auto)
done
@@ -167,10 +167,10 @@
lemma Finite_lesspoll_infinite_Ord:
"\<lbrakk>Finite(X); \<not>Finite(a); Ord(a)\<rbrakk> \<Longrightarrow> X\<prec>a"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (rule conjI)
apply (drule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption)
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (blast intro: leI [THEN le_imp_subset, THEN subset_imp_lepoll]
ltI eqpoll_imp_lepoll lepoll_trans)
apply (blast intro: eqpoll_sym [THEN eqpoll_trans])
@@ -256,7 +256,7 @@
\<Longrightarrow> (\<Union>x<a. F(x)) \<lesssim> a"
apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). \<mu> i. z \<in> F (i) " in exI)
-apply (unfold inj_def)
+ unfolding inj_def
apply (rule CollectI)
apply (rule lam_type)
apply (erule OUN_E)
@@ -547,7 +547,7 @@
(* ********************************************************************** *)
theorem WO2_AC16: "\<lbrakk>WO2; 0<m; k \<in> nat; m \<in> nat\<rbrakk> \<Longrightarrow> AC16(k #+ m,k)"
-apply (unfold AC16_def)
+ unfolding AC16_def
apply (rule allI)
apply (rule impI)
apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
--- a/src/ZF/AC/WO6_WO1.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Tue Sep 27 17:54:20 2022 +0100
@@ -86,7 +86,7 @@
by (fast intro!: lam_type apply_type)
lemma surj_imp_eq': "f \<in> surj(A,B) \<Longrightarrow> (\<Union>a \<in> A. {f`a}) = B"
-apply (unfold surj_def)
+ unfolding surj_def
apply (fast elim!: apply_type)
done
@@ -109,7 +109,7 @@
(* ********************************************************************** *)
lemma WO4_mono: "\<lbrakk>m\<le>n; WO4(m)\<rbrakk> \<Longrightarrow> WO4(n)"
-apply (unfold WO4_def)
+ unfolding WO4_def
apply (blast dest!: spec intro: lepoll_trans [OF _ le_imp_lepoll])
done
@@ -175,7 +175,7 @@
(\<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 \<and> u(f,b,g,d) \<prec> m))
| (\<exists>b<a. f`b \<noteq> 0 \<and> (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow>
u(f,b,g,d) \<approx> m))"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (blast del: equalityI)
done
@@ -330,7 +330,7 @@
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; Ord(a); m \<in> nat; s \<in> f`b; b<a\<rbrakk>
\<Longrightarrow> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y"
-apply (unfold gg2_def)
+ unfolding gg2_def
apply (drule sym)
apply (simp add: ltD UN_oadd oadd_le_self [THEN le_imp_not_lt]
lt_Ord odiff_oadd_inverse ww2_def
@@ -346,7 +346,7 @@
(* ********************************************************************** *)
lemma vv2_lepoll: "\<lbrakk>m \<in> nat; m\<noteq>0\<rbrakk> \<Longrightarrow> vv2(f,b,g,s) \<lesssim> m"
-apply (unfold vv2_def)
+ unfolding vv2_def
apply (simp add: empty_lepollI)
apply (fast dest!: le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_0_is_0]
intro!: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
@@ -357,7 +357,7 @@
lemma ww2_lepoll:
"\<lbrakk>\<forall>b<a. f`b \<lesssim> succ(m); g<a; m \<in> nat; vv2(f,b,g,d) \<subseteq> f`g\<rbrakk>
\<Longrightarrow> ww2(f,b,g,d) \<lesssim> m"
-apply (unfold ww2_def)
+ unfolding ww2_def
apply (case_tac "f`g = 0")
apply (simp add: empty_lepollI)
apply (drule ospec, assumption)
@@ -381,7 +381,7 @@
(* lemma ii *)
(* ********************************************************************** *)
lemma lemma_ii: "\<lbrakk>succ(m) \<in> NN(y); y*y \<subseteq> y; m \<in> nat; m\<noteq>0\<rbrakk> \<Longrightarrow> m \<in> NN(y)"
-apply (unfold NN_def)
+ unfolding NN_def
apply (elim CollectE exE conjE)
apply (rule quant_domain_uu_lepoll_m [THEN cases, THEN disjE], assumption)
(* case 1 *)
@@ -472,7 +472,7 @@
done
lemma NN_imp_ex_inj: "1 \<in> NN(y) \<Longrightarrow> \<exists>a f. Ord(a) \<and> f \<in> inj(y, a)"
-apply (unfold NN_def)
+ unfolding NN_def
apply (elim CollectE exE conjE)
apply (rule_tac x = a in exI)
apply (rule_tac x = "\<lambda>x \<in> y. \<mu> i. f`i = {x}" in exI)
@@ -517,12 +517,12 @@
(* another helpful lemma *)
lemma NN_y_0: "0 \<in> NN(y) \<Longrightarrow> y=0"
-apply (unfold NN_def)
+ unfolding NN_def
apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst)
done
lemma WO6_imp_WO1: "WO6 \<Longrightarrow> WO1"
-apply (unfold WO1_def)
+ unfolding WO1_def
apply (rule allI)
apply (case_tac "A=0")
apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
--- a/src/ZF/Arith.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Arith.thy Tue Sep 27 17:54:20 2022 +0100
@@ -191,7 +191,7 @@
by (simp add: diff_def raw_diff_type)
lemma diff_0_eq_0 [simp]: "0 #- n = 0"
-apply (unfold diff_def)
+ unfolding diff_def
apply (rule natify_in_nat [THEN nat_induct], auto)
done
@@ -245,7 +245,7 @@
done
lemma add_succ_right [simp]: "m #+ succ(n) = succ(m #+ n)"
-apply (unfold add_def)
+ unfolding add_def
apply (rule_tac n = "natify(m) " in nat_induct)
apply (auto simp add: natify_succ)
done
@@ -278,7 +278,7 @@
done
lemma add_left_cancel_natify: "k #+ m = k #+ n \<Longrightarrow> natify(m) = natify(n)"
-apply (unfold add_def)
+ unfolding add_def
apply (drule raw_add_left_cancel, auto)
done
@@ -468,7 +468,7 @@
(*right annihilation in product*)
lemma mult_0_right [simp]: "m #* 0 = 0"
-apply (unfold mult_def)
+ unfolding mult_def
apply (rule_tac n = "natify(m) " in nat_induct)
apply auto
done
--- a/src/ZF/ArithSimp.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ArithSimp.thy Tue Sep 27 17:54:20 2022 +0100
@@ -82,14 +82,14 @@
nat_into_Ord not_lt_iff_le [THEN iffD1]
lemma raw_mod_type: "\<lbrakk>m:nat; n:nat\<rbrakk> \<Longrightarrow> raw_mod (m, n) \<in> nat"
-apply (unfold raw_mod_def)
+ unfolding raw_mod_def
apply (rule Ord_transrec_type)
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
apply (blast intro: div_rls)
done
lemma mod_type [TC,iff]: "m mod n \<in> nat"
-apply (unfold mod_def)
+ unfolding mod_def
apply (simp (no_asm) add: mod_def raw_mod_type)
done
@@ -98,13 +98,13 @@
certain equations **)
lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0"
-apply (unfold div_def)
+ unfolding div_def
apply (rule raw_div_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp))
done (*NOT for adding to default simpset*)
lemma DIVISION_BY_ZERO_MOD: "a mod 0 = natify(a)"
-apply (unfold mod_def)
+ unfolding mod_def
apply (rule raw_mod_def [THEN def_transrec, THEN trans])
apply (simp (no_asm_simp))
done (*NOT for adding to default simpset*)
@@ -138,14 +138,14 @@
subsection\<open>Division\<close>
lemma raw_div_type: "\<lbrakk>m:nat; n:nat\<rbrakk> \<Longrightarrow> raw_div (m, n) \<in> nat"
-apply (unfold raw_div_def)
+ unfolding raw_div_def
apply (rule Ord_transrec_type)
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
apply (blast intro: div_rls)
done
lemma div_type [TC,iff]: "m div n \<in> nat"
-apply (unfold div_def)
+ unfolding div_def
apply (simp (no_asm) add: div_def raw_div_type)
done
--- a/src/ZF/Bin.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Bin.thy Tue Sep 27 17:54:20 2022 +0100
@@ -164,7 +164,7 @@
(*This proof is complicated by the mutual recursion*)
lemma bin_add_type [rule_format]:
"v \<in> bin \<Longrightarrow> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
-apply (unfold bin_add_def)
+ unfolding bin_add_def
apply (induct_tac "v")
apply (rule_tac [3] ballI)
apply (rename_tac [3] "w'")
@@ -215,7 +215,7 @@
by (unfold bin_add_def, simp)
lemma bin_add_Pls_right: "w \<in> bin \<Longrightarrow> bin_add(w,Pls) = w"
-apply (unfold bin_add_def)
+ unfolding bin_add_def
apply (erule bin.induct, auto)
done
@@ -223,7 +223,7 @@
by (unfold bin_add_def, simp)
lemma bin_add_Min_right: "w \<in> bin \<Longrightarrow> bin_add(w,Min) = bin_pred(w)"
-apply (unfold bin_add_def)
+ unfolding bin_add_def
apply (erule bin.induct, auto)
done
@@ -252,7 +252,7 @@
lemma diff_integ_of_eq:
"\<lbrakk>v \<in> bin; w \<in> bin\<rbrakk>
\<Longrightarrow> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
-apply (unfold zdiff_def)
+ unfolding zdiff_def
apply (simp add: integ_of_add integ_of_minus)
done
@@ -362,7 +362,7 @@
"\<lbrakk>v \<in> bin; w \<in> bin\<rbrakk>
\<Longrightarrow> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
iszero (integ_of (bin_add (v, bin_minus(w))))"
-apply (unfold iszero_def)
+ unfolding iszero_def
apply (simp add: zcompare_rls integ_of_add integ_of_minus)
done
@@ -371,7 +371,7 @@
lemma nonzero_integ_of_Min: "\<not> iszero (integ_of(Min))"
-apply (unfold iszero_def)
+ unfolding iszero_def
apply (simp add: zminus_equation)
done
@@ -497,7 +497,7 @@
lemma add_integ_of_diff1 [simp]:
"\<lbrakk>v \<in> bin; w \<in> bin\<rbrakk>
\<Longrightarrow> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)"
-apply (unfold zdiff_def)
+ unfolding zdiff_def
apply (rule add_integ_of_left, auto)
done
--- a/src/ZF/Cardinal.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Cardinal.thy Tue Sep 27 17:54:20 2022 +0100
@@ -79,7 +79,7 @@
(** Equipollence is an equivalence relation **)
lemma bij_imp_eqpoll: "f \<in> bij(A,B) \<Longrightarrow> A \<approx> B"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (erule exI)
done
@@ -87,20 +87,20 @@
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
lemma eqpoll_sym: "X \<approx> Y \<Longrightarrow> Y \<approx> X"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (blast intro: bij_converse_bij)
done
lemma eqpoll_trans [trans]:
"\<lbrakk>X \<approx> Y; Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<approx> Z"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (blast intro: comp_bij)
done
(** Le-pollence is a partial ordering **)
lemma subset_imp_lepoll: "X<=Y \<Longrightarrow> X \<lesssim> Y"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule exI)
apply (erule id_subset_inj)
done
@@ -113,7 +113,7 @@
by (unfold eqpoll_def bij_def lepoll_def, blast)
lemma lepoll_trans [trans]: "\<lbrakk>X \<lesssim> Y; Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<lesssim> Z"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (blast intro: comp_inj)
done
@@ -150,7 +150,7 @@
lemma Un_lepoll_Un:
"\<lbrakk>A \<lesssim> B; C \<lesssim> D; B \<inter> D = 0\<rbrakk> \<Longrightarrow> A \<union> C \<lesssim> B \<union> D"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (blast intro: inj_disjoint_Un)
done
@@ -163,7 +163,7 @@
lemma eqpoll_disjoint_Un:
"\<lbrakk>A \<approx> B; C \<approx> D; A \<inter> C = 0; B \<inter> D = 0\<rbrakk>
\<Longrightarrow> A \<union> C \<approx> B \<union> D"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (blast intro: bij_disjoint_Un)
done
@@ -180,12 +180,12 @@
by (unfold lesspoll_def, blast)
lemma lepoll_well_ord: "\<lbrakk>A \<lesssim> B; well_ord(B,r)\<rbrakk> \<Longrightarrow> \<exists>s. well_ord(A,s)"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (blast intro: well_ord_rvimage)
done
lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (blast intro!: eqpollI elim!: eqpollE)
done
@@ -208,19 +208,19 @@
lemma lesspoll_trans [trans]:
"\<lbrakk>X \<prec> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
lemma lesspoll_trans1 [trans]:
"\<lbrakk>X \<lesssim> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
lemma lesspoll_trans2 [trans]:
"\<lbrakk>X \<prec> Y; Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
@@ -237,7 +237,7 @@
lemma Least_equality:
"\<lbrakk>P(i); Ord(i); \<And>x. x<i \<Longrightarrow> \<not>P(x)\<rbrakk> \<Longrightarrow> (\<mu> x. P(x)) = i"
-apply (unfold Least_def)
+ unfolding Least_def
apply (rule the_equality, blast)
apply (elim conjE)
apply (erule Ord_linear_lt, assumption, blast+)
@@ -304,7 +304,7 @@
(*If there is no such P then \<mu> is vacuously 0*)
lemma Least_0:
"\<lbrakk>\<not> (\<exists>i. Ord(i) \<and> P(i))\<rbrakk> \<Longrightarrow> (\<mu> x. P(x)) = 0"
-apply (unfold Least_def)
+ unfolding Least_def
apply (rule the_0, blast)
done
@@ -369,12 +369,12 @@
(** Observations from Kunen, page 28 **)
lemma Ord_cardinal_le: "Ord(i) \<Longrightarrow> |i| \<le> i"
-apply (unfold cardinal_def)
+ unfolding cardinal_def
apply (erule eqpoll_refl [THEN Least_le])
done
lemma Card_cardinal_eq: "Card(K) \<Longrightarrow> |K| = K"
-apply (unfold Card_def)
+ unfolding Card_def
apply (erule sym)
done
@@ -396,7 +396,7 @@
done
lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
-apply (unfold cardinal_def)
+ unfolding cardinal_def
apply (rule Ord_Least)
done
@@ -417,7 +417,7 @@
qed
lemma lt_Card_imp_lesspoll: "\<lbrakk>Card(a); i<a\<rbrakk> \<Longrightarrow> i \<prec> a"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (drule Card_iff_initial [THEN iffD1])
apply (blast intro!: leI [THEN le_imp_lepoll])
done
@@ -536,7 +536,7 @@
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
lemma lesspoll_imp_eqpoll: "\<lbrakk>A \<prec> i; Ord(i)\<rbrakk> \<Longrightarrow> |A| \<approx> A"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (blast intro: lepoll_Ord_imp_eqpoll)
done
@@ -569,7 +569,7 @@
(*Lemma suggested by Mike Fourman*)
lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) \<Longrightarrow> m \<lesssim> n"
-apply (unfold succ_def)
+ unfolding succ_def
apply (erule cons_lepoll_consD)
apply (rule mem_not_refl)+
done
@@ -757,7 +757,7 @@
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
lemma singleton_eqpoll_1: "{a} \<approx> 1"
-apply (unfold succ_def)
+ unfolding succ_def
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
done
@@ -775,26 +775,26 @@
(*Congruence law for succ under equipollence*)
lemma succ_eqpoll_cong: "A \<approx> B \<Longrightarrow> succ(A) \<approx> succ(B)"
-apply (unfold succ_def)
+ unfolding succ_def
apply (simp add: cons_eqpoll_cong mem_not_refl)
done
(*Congruence law for + under equipollence*)
lemma sum_eqpoll_cong: "\<lbrakk>A \<approx> C; B \<approx> D\<rbrakk> \<Longrightarrow> A+B \<approx> C+D"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (blast intro!: sum_bij)
done
(*Congruence law for * under equipollence*)
lemma prod_eqpoll_cong:
"\<lbrakk>A \<approx> C; B \<approx> D\<rbrakk> \<Longrightarrow> A*B \<approx> C*D"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (blast intro!: prod_bij)
done
lemma inj_disjoint_eqpoll:
"\<lbrakk>f \<in> inj(A,B); A \<inter> B = 0\<rbrakk> \<Longrightarrow> A \<union> (B - range(f)) \<approx> B"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule_tac c = "\<lambda>x. if x \<in> A then f`x else x"
and d = "\<lambda>y. if y \<in> range (f) then converse (f) `y else y"
@@ -815,7 +815,7 @@
then \<^term>\<open>A-{a}\<close> has at most \<^term>\<open>n\<close>.\<close>
lemma Diff_sing_lepoll:
"\<lbrakk>a \<in> A; A \<lesssim> succ(n)\<rbrakk> \<Longrightarrow> A - {a} \<lesssim> n"
-apply (unfold succ_def)
+ unfolding succ_def
apply (rule cons_lepoll_consD)
apply (rule_tac [3] mem_not_refl)
apply (erule cons_Diff [THEN ssubst], safe)
@@ -846,7 +846,7 @@
done
lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x\<in>A then Inl (x) else Inr (x)" in exI)
apply (rule_tac d = "\<lambda>z. snd (z)" in lam_injective)
apply force
@@ -860,7 +860,7 @@
(*Krzysztof Grabczewski*)
lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 \<Longrightarrow> A \<union> B \<approx> A + B"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI)
apply (rule_tac d = "\<lambda>z. case (\<lambda>x. x, \<lambda>x. x, z)" in lam_bijective)
apply auto
@@ -870,17 +870,17 @@
subsection \<open>Finite and infinite sets\<close>
lemma eqpoll_imp_Finite_iff: "A \<approx> B \<Longrightarrow> Finite(A) \<longleftrightarrow> Finite(B)"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (blast intro: eqpoll_trans eqpoll_sym)
done
lemma Finite_0 [simp]: "Finite(0)"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (blast intro!: eqpoll_refl nat_0I)
done
lemma Finite_cons: "Finite(x) \<Longrightarrow> Finite(cons(y,x))"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (case_tac "y \<in> x")
apply (simp add: cons_absorb)
apply (erule bexE)
@@ -890,7 +890,7 @@
done
lemma Finite_succ: "Finite(x) \<Longrightarrow> Finite(succ(x))"
-apply (unfold succ_def)
+ unfolding succ_def
apply (erule Finite_cons)
done
@@ -912,7 +912,7 @@
lemma lesspoll_nat_is_Finite:
"A \<prec> nat \<Longrightarrow> Finite(A)"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (blast dest: ltD lesspoll_cardinal_lt
lesspoll_imp_eqpoll [THEN eqpoll_sym])
done
@@ -943,7 +943,7 @@
lemma nat_le_infinite_Ord:
"\<lbrakk>Ord(i); \<not> Finite(i)\<rbrakk> \<Longrightarrow> nat \<le> i"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (erule Ord_nat [THEN [2] Ord_linear2])
prefer 2 apply assumption
apply (blast intro!: eqpoll_refl elim!: ltE)
@@ -993,12 +993,12 @@
apply (rule Fin.consI, blast)
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
(*Now for the lemma assumed above*)
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
done
lemma Finite_into_Fin: "Finite(A) \<Longrightarrow> A \<in> Fin(A)"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (blast intro: Fin_lemma)
done
@@ -1036,7 +1036,7 @@
(*Sidi Ehmety. The contrapositive says \<not>Finite(A) \<Longrightarrow> \<not>Finite(A-{a}) *)
lemma Diff_sing_Finite: "Finite(A - {a}) \<Longrightarrow> Finite(A)"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (case_tac "a \<in> A")
apply (subgoal_tac [2] "A-{a}=A", auto)
apply (rule_tac x = "succ (n) " in bexI)
@@ -1154,7 +1154,7 @@
lemma Finite_well_ord_converse:
"\<lbrakk>Finite(A); well_ord(A,r)\<rbrakk> \<Longrightarrow> well_ord(A,converse(r))"
-apply (unfold Finite_def)
+ unfolding Finite_def
apply (rule well_ord_converse, assumption)
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
done
--- a/src/ZF/CardinalArith.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/CardinalArith.thy Tue Sep 27 17:54:20 2022 +0100
@@ -73,7 +73,7 @@
by (auto simp add: OUnion_def Card_0)
lemma in_Card_imp_lesspoll: "\<lbrakk>Card(K); b \<in> K\<rbrakk> \<Longrightarrow> b \<prec> K"
-apply (unfold lesspoll_def)
+ unfolding lesspoll_def
apply (simp add: Card_iff_initial)
apply (fast intro!: le_imp_lepoll ltI leI)
done
@@ -95,14 +95,14 @@
qed
lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
-apply (unfold cadd_def)
+ unfolding cadd_def
apply (rule sum_commute_eqpoll [THEN cardinal_cong])
done
subsubsection\<open>Cardinal addition is associative\<close>
lemma sum_assoc_eqpoll: "(A+B)+C \<approx> A+(B+C)"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule sum_assoc_bij)
done
@@ -125,13 +125,13 @@
subsubsection\<open>0 is the identity for addition\<close>
lemma sum_0_eqpoll: "0+A \<approx> A"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule bij_0_sum)
done
lemma cadd_0 [simp]: "Card(K) \<Longrightarrow> 0 \<oplus> K = K"
-apply (unfold cadd_def)
+ unfolding cadd_def
apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
done
@@ -161,7 +161,7 @@
lemma sum_lepoll_mono:
"\<lbrakk>A \<lesssim> C; B \<lesssim> D\<rbrakk> \<Longrightarrow> A + B \<lesssim> C + D"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (elim exE)
apply (rule_tac x = "\<lambda>z\<in>A+B. case (\<lambda>w. Inl(f`w), \<lambda>y. Inr(fa`y), z)" in exI)
apply (rule_tac d = "case (\<lambda>w. Inl(converse(f) `w), \<lambda>y. Inr(converse(fa) ` y))"
@@ -171,7 +171,7 @@
lemma cadd_le_mono:
"\<lbrakk>K' \<le> K; L' \<le> L\<rbrakk> \<Longrightarrow> (K' \<oplus> L') \<le> (K \<oplus> L)"
-apply (unfold cadd_def)
+ unfolding cadd_def
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule well_ord_lepoll_imp_cardinal_le)
apply (blast intro: well_ord_radd well_ord_Memrel)
@@ -181,7 +181,7 @@
subsubsection\<open>Addition of finite cardinals is "ordinary" addition\<close>
lemma sum_succ_eqpoll: "succ(A)+B \<approx> succ(A+B)"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule_tac c = "\<lambda>z. if z=Inl (A) then A+B else z"
and d = "\<lambda>z. if z=A+B then Inl (A) else z" in lam_bijective)
@@ -219,21 +219,21 @@
subsubsection\<open>Cardinal multiplication is commutative\<close>
lemma prod_commute_eqpoll: "A*B \<approx> B*A"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule_tac c = "\<lambda>\<langle>x,y\<rangle>.\<langle>y,x\<rangle>" and d = "\<lambda>\<langle>x,y\<rangle>.\<langle>y,x\<rangle>" in lam_bijective,
auto)
done
lemma cmult_commute: "i \<otimes> j = j \<otimes> i"
-apply (unfold cmult_def)
+ unfolding cmult_def
apply (rule prod_commute_eqpoll [THEN cardinal_cong])
done
subsubsection\<open>Cardinal multiplication is associative\<close>
lemma prod_assoc_eqpoll: "(A*B)*C \<approx> A*(B*C)"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule prod_assoc_bij)
done
@@ -255,7 +255,7 @@
subsubsection\<open>Cardinal multiplication distributes over addition\<close>
lemma sum_prod_distrib_eqpoll: "(A+B)*C \<approx> (A*C)+(B*C)"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule sum_prod_distrib_bij)
done
@@ -276,7 +276,7 @@
subsubsection\<open>Multiplication by 0 yields 0\<close>
lemma prod_0_eqpoll: "0*A \<approx> 0"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule lam_bijective, safe)
done
@@ -287,7 +287,7 @@
subsubsection\<open>1 is the identity for multiplication\<close>
lemma prod_singleton_eqpoll: "{x}*A \<approx> A"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule singleton_prod_bij [THEN bij_converse_bij])
done
@@ -306,7 +306,7 @@
(*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
lemma cmult_square_le: "Card(K) \<Longrightarrow> K \<le> K \<otimes> K"
-apply (unfold cmult_def)
+ unfolding cmult_def
apply (rule le_trans)
apply (rule_tac [2] well_ord_lepoll_imp_cardinal_le)
apply (rule_tac [3] prod_square_lepoll)
@@ -324,7 +324,7 @@
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
lemma cmult_le_self:
"\<lbrakk>Card(K); Ord(L); 0<L\<rbrakk> \<Longrightarrow> K \<le> (K \<otimes> L)"
-apply (unfold cmult_def)
+ unfolding cmult_def
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_cardinal_le])
apply assumption
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
@@ -335,7 +335,7 @@
lemma prod_lepoll_mono:
"\<lbrakk>A \<lesssim> C; B \<lesssim> D\<rbrakk> \<Longrightarrow> A * B \<lesssim> C * D"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (elim exE)
apply (rule_tac x = "lam \<langle>w,y\<rangle>:A*B. <f`w, fa`y>" in exI)
apply (rule_tac d = "\<lambda>\<langle>w,y\<rangle>. <converse (f) `w, converse (fa) `y>"
@@ -345,7 +345,7 @@
lemma cmult_le_mono:
"\<lbrakk>K' \<le> K; L' \<le> L\<rbrakk> \<Longrightarrow> (K' \<otimes> L') \<le> (K \<otimes> L)"
-apply (unfold cmult_def)
+ unfolding cmult_def
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule well_ord_lepoll_imp_cardinal_le)
apply (blast intro: well_ord_rmult well_ord_Memrel)
@@ -355,7 +355,7 @@
subsection\<open>Multiplication of finite cardinals is "ordinary" multiplication\<close>
lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (rule_tac c = "\<lambda>\<langle>x,y\<rangle>. if x=A then Inl (y) else Inr (\<langle>x,y\<rangle>)"
and d = "case (\<lambda>y. \<langle>A,y\<rangle>, \<lambda>z. z)" in lam_bijective)
@@ -402,7 +402,7 @@
and inverse \<lambda>y. if y \<in> nat then nat_case(u, \<lambda>z. z, y) else y. \
If f \<in> inj(nat,A) then range(f) behaves like the natural numbers.*)
lemma nat_cons_lepoll: "nat \<lesssim> A \<Longrightarrow> cons(u,A) \<lesssim> A"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (erule exE)
apply (rule_tac x =
"\<lambda>z\<in>cons (u,A).
@@ -426,35 +426,35 @@
(*Specialized version required below*)
lemma nat_succ_eqpoll: "nat \<subseteq> A \<Longrightarrow> succ(A) \<approx> A"
-apply (unfold succ_def)
+ unfolding succ_def
apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll])
done
lemma InfCard_nat: "InfCard(nat)"
-apply (unfold InfCard_def)
+ unfolding InfCard_def
apply (blast intro: Card_nat le_refl Card_is_Ord)
done
lemma InfCard_is_Card: "InfCard(K) \<Longrightarrow> Card(K)"
-apply (unfold InfCard_def)
+ unfolding InfCard_def
apply (erule conjunct1)
done
lemma InfCard_Un:
"\<lbrakk>InfCard(K); Card(L)\<rbrakk> \<Longrightarrow> InfCard(K \<union> L)"
-apply (unfold InfCard_def)
+ unfolding InfCard_def
apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans] Card_is_Ord)
done
(*Kunen's Lemma 10.11*)
lemma InfCard_is_Limit: "InfCard(K) \<Longrightarrow> Limit(K)"
-apply (unfold InfCard_def)
+ unfolding InfCard_def
apply (erule conjE)
apply (frule Card_is_Ord)
apply (rule ltI [THEN non_succ_LimitI])
apply (erule le_imp_subset [THEN subsetD])
apply (safe dest!: Limit_nat [THEN Limit_le_succD])
-apply (unfold Card_def)
+ unfolding Card_def
apply (drule trans)
apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong])
apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl])
@@ -468,7 +468,7 @@
(*A general fact about ordermap*)
lemma ordermap_eqpoll_pred:
"\<lbrakk>well_ord(A,r); x \<in> A\<rbrakk> \<Longrightarrow> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (rule exI)
apply (simp add: ordermap_eq_image well_ord_is_wf)
apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij,
@@ -492,7 +492,7 @@
lemma csquareD:
"\<lbrakk><\<langle>x,y\<rangle>, \<langle>z,z\<rangle>> \<in> csquare_rel(K); x<K; y<K; z<K\<rbrakk> \<Longrightarrow> x \<le> z \<and> y \<le> z"
-apply (unfold csquare_rel_def)
+ unfolding csquare_rel_def
apply (erule rev_mp)
apply (elim ltE)
apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
@@ -509,7 +509,7 @@
lemma csquare_ltI:
"\<lbrakk>x<z; y<z; z<K\<rbrakk> \<Longrightarrow> <\<langle>x,y\<rangle>, \<langle>z,z\<rangle>> \<in> csquare_rel(K)"
-apply (unfold csquare_rel_def)
+ unfolding csquare_rel_def
apply (subgoal_tac "x<K \<and> y<K")
prefer 2 apply (blast intro: lt_trans)
apply (elim ltE)
@@ -519,7 +519,7 @@
(*Part of the traditional proof. UNUSED since it's harder to prove \<and> apply *)
lemma csquare_or_eqI:
"\<lbrakk>x \<le> z; y \<le> z; z<K\<rbrakk> \<Longrightarrow> <\<langle>x,y\<rangle>, \<langle>z,z\<rangle>> \<in> csquare_rel(K) | x=z \<and> y=z"
-apply (unfold csquare_rel_def)
+ unfolding csquare_rel_def
apply (subgoal_tac "x<K \<and> y<K")
prefer 2 apply (blast intro: lt_trans1)
apply (elim ltE)
@@ -731,10 +731,10 @@
text\<open>This result is Kunen's Theorem 10.16, which would be trivial using AC\<close>
lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))"
-apply (unfold jump_cardinal_def)
+ unfolding jump_cardinal_def
apply (rule Ord_is_Transset [THEN [2] OrdI])
prefer 2 apply (blast intro!: Ord_ordertype)
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (safe del: subsetI)
apply (simp add: ordertype_pred_unfold, safe)
apply (rule UN_I)
@@ -746,7 +746,7 @@
lemma jump_cardinal_iff:
"i \<in> jump_cardinal(K) \<longleftrightarrow>
(\<exists>r X. r \<subseteq> K*K \<and> X \<subseteq> K \<and> well_ord(X,r) \<and> i = ordertype(X,r))"
-apply (unfold jump_cardinal_def)
+ unfolding jump_cardinal_def
apply (blast del: subsetI)
done
@@ -780,7 +780,7 @@
(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*)
lemma Card_jump_cardinal: "Card(jump_cardinal(K))"
apply (rule Ord_jump_cardinal [THEN CardI])
-apply (unfold eqpoll_def)
+ unfolding eqpoll_def
apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1])
apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl])
done
@@ -788,7 +788,7 @@
subsection\<open>Basic Properties of Successor Cardinals\<close>
lemma csucc_basic: "Ord(K) \<Longrightarrow> Card(csucc(K)) \<and> K < csucc(K)"
-apply (unfold csucc_def)
+ unfolding csucc_def
apply (rule LeastI)
apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+
done
@@ -801,7 +801,7 @@
by (blast intro: Ord_0_le lt_csucc lt_trans1)
lemma csucc_le: "\<lbrakk>Card(L); K<L\<rbrakk> \<Longrightarrow> csucc(K) \<le> L"
-apply (unfold csucc_def)
+ unfolding csucc_def
apply (rule Least_le)
apply (blast intro: Card_is_Ord)+
done
--- a/src/ZF/Coind/ECR.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/ECR.thy Tue Sep 27 17:54:20 2022 +0100
@@ -98,7 +98,7 @@
v_clos(x,e,ve_owr(ve,f,cl)) = cl;
hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel\<rbrakk> \<Longrightarrow>
\<langle>cl,t\<rangle> \<in> HasTyRel"
-apply (unfold hastyenv_def)
+ unfolding hastyenv_def
apply (erule elab_fixE, safe)
apply hypsubst_thin
apply (rule subst, assumption)
--- a/src/ZF/Coind/Map.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/Map.thy Tue Sep 27 17:54:20 2022 +0100
@@ -69,7 +69,7 @@
lemma MapQU_lemma:
"A \<subseteq> univ(X) \<Longrightarrow> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)"
-apply (unfold quniv_def)
+ unfolding quniv_def
apply (rule Pow_mono)
apply (rule subset_trans [OF Sigma_mono product_univ])
apply (erule subset_trans)
@@ -127,7 +127,7 @@
lemma pmap_appI:
"\<lbrakk>m \<in> PMap(A,B); a \<in> domain(m)\<rbrakk> \<Longrightarrow> map_app(m,a):B"
-apply (unfold PMap_def)
+ unfolding PMap_def
apply (frule tmap_app_notempty, assumption)
apply (drule tmap_appI, auto)
done
@@ -165,7 +165,7 @@
lemma map_domain_owr:
"b \<noteq> 0 \<Longrightarrow> domain(map_owr(f,a,b)) = {a} \<union> domain(f)"
-apply (unfold map_owr_def)
+ unfolding map_owr_def
apply (auto simp add: domain_Sigma)
done
--- a/src/ZF/Coind/Values.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/Values.thy Tue Sep 27 17:54:20 2022 +0100
@@ -101,7 +101,7 @@
done
lemma ve_empI: "ve_emp \<in> ValEnv"
-apply (unfold ve_emp_def)
+ unfolding ve_emp_def
apply (rule Val_ValEnv.intros)
apply (rule pmap_empI)
done
--- a/src/ZF/Constructible/AC_in_L.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Tue Sep 27 17:54:20 2022 +0100
@@ -216,7 +216,7 @@
text\<open>Not needed--but interesting?\<close>
theorem formula_lepoll_nat: "formula \<lesssim> nat"
apply (insert nat_times_nat_lepoll_nat)
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro)
done
@@ -447,7 +447,7 @@
lemma well_ord_L_r:
"Ord(i) \<Longrightarrow> \<exists>r. well_ord(Lset(i), r)"
apply (insert nat_times_nat_lepoll_nat)
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro)
done
--- a/src/ZF/Constructible/DPow_absolute.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Tue Sep 27 17:54:20 2022 +0100
@@ -177,7 +177,7 @@
theorem DPow_sats_reflection:
"REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
\<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold is_DPow_sats_def)
+ unfolding is_DPow_sats_def
apply (intro FOL_reflections function_reflections extra_reflections
satisfies_reflection)
done
@@ -264,7 +264,7 @@
mem_formula(##Lset(i),p) \<and> mem_list(##Lset(i),A,env) \<and>
pair(##Lset(i),env,p,u) \<and>
is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]"
-apply (unfold is_Collect_def)
+ unfolding is_Collect_def
apply (intro FOL_reflections function_reflections mem_formula_reflection
mem_list_reflection DPow_sats_reflection)
done
@@ -279,7 +279,7 @@
apply (rule_tac u="{A,B}"
in gen_separation_multi [OF DPow_replacement_Reflects],
auto)
-apply (unfold is_Collect_def)
+ unfolding is_Collect_def
apply (rule_tac env="[A,B]" in DPow_LsetI)
apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats
DPow_sats_iff_sats | simp)+
@@ -543,7 +543,7 @@
lemma strong_rep:
"\<lbrakk>L(x); L(g)\<rbrakk> \<Longrightarrow> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
-apply (unfold transrec_body_def)
+ unfolding transrec_body_def
apply (rule strong_replacementI)
apply (rule_tac u="{x,g,B}"
in gen_separation_multi [OF strong_rep_Reflects], auto)
@@ -582,7 +582,7 @@
\<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) \<and>
big_union(L, r, u), j)"
apply (rule L.transrec_replacementI, assumption)
-apply (unfold transrec_body_def)
+ unfolding transrec_body_def
apply (rule strong_replacementI)
apply (rule_tac u="{j,B,Memrel(eclose({j}))}"
in gen_separation_multi [OF transrec_rep_Reflects], auto)
--- a/src/ZF/Constructible/Formula.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Formula.thy Tue Sep 27 17:54:20 2022 +0100
@@ -799,7 +799,7 @@
lemma Pair_in_Lset:
"\<lbrakk>a \<in> Lset(i); b \<in> Lset(i); Ord(i)\<rbrakk> \<Longrightarrow> \<langle>a,b\<rangle> \<in> Lset(succ(succ(i)))"
-apply (unfold Pair_def)
+ unfolding Pair_def
apply (blast intro: doubleton_in_Lset)
done
@@ -862,7 +862,7 @@
lemma Lset_iff_lrank_lt: "Ord(i) \<Longrightarrow> x \<in> Lset(i) \<longleftrightarrow> L(x) \<and> lrank(x) < i"
apply (simp add: L_def, auto)
apply (blast intro: Lset_lrank_lt)
- apply (unfold lrank_def)
+ unfolding lrank_def
apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD])
apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption)
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
@@ -873,7 +873,7 @@
text\<open>Kunen's VI 1.9 (a)\<close>
lemma lrank_of_Ord: "Ord(i) \<Longrightarrow> lrank(i) = i"
-apply (unfold lrank_def)
+ unfolding lrank_def
apply (rule Least_equality)
apply (erule Ord_in_Lset)
apply assumption
@@ -894,7 +894,7 @@
done
lemma lrank_Lset: "Ord(i) \<Longrightarrow> lrank(Lset(i)) = i"
-apply (unfold lrank_def)
+ unfolding lrank_def
apply (rule Least_equality)
apply (rule Lset_in_Lset_succ)
apply assumption
--- a/src/ZF/Constructible/L_axioms.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Tue Sep 27 17:54:20 2022 +0100
@@ -155,7 +155,7 @@
theorem Not_reflection:
"REFLECTS[P,Q] \<Longrightarrow> REFLECTS[\<lambda>x. \<not>P(x), \<lambda>a x. \<not>Q(a,x)]"
-apply (unfold L_Reflects_def)
+ unfolding L_Reflects_def
apply (erule meta_exE)
apply (rule_tac x=Cl in meta_exI, simp)
done
@@ -163,7 +163,7 @@
theorem And_reflection:
"\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
\<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+ unfolding L_Reflects_def
apply (elim meta_exE)
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
@@ -172,7 +172,7 @@
theorem Or_reflection:
"\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
\<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+ unfolding L_Reflects_def
apply (elim meta_exE)
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
@@ -181,7 +181,7 @@
theorem Imp_reflection:
"\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
\<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<longrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longrightarrow> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+ unfolding L_Reflects_def
apply (elim meta_exE)
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
@@ -190,7 +190,7 @@
theorem Iff_reflection:
"\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
\<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<longleftrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longleftrightarrow> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+ unfolding L_Reflects_def
apply (elim meta_exE)
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
@@ -223,14 +223,14 @@
theorem Rex_reflection:
"REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
\<Longrightarrow> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold rex_def)
+ unfolding rex_def
apply (intro And_reflection Ex_reflection, assumption)
done
theorem Rall_reflection:
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
\<Longrightarrow> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold rall_def)
+ unfolding rall_def
apply (intro Imp_reflection All_reflection, assumption)
done
--- a/src/ZF/Constructible/Normal.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Normal.thy Tue Sep 27 17:54:20 2022 +0100
@@ -171,7 +171,7 @@
done
lemma Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
- apply (unfold Unbounded_def)
+ unfolding Unbounded_def
apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater)
done
@@ -367,7 +367,7 @@
lemma iterates_omega_increasing:
"\<lbrakk>Normal(F); Ord(a)\<rbrakk> \<Longrightarrow> a \<le> F^\<omega> (a)"
-apply (unfold iterates_omega_def)
+ unfolding iterates_omega_def
apply (rule UN_upper_le [of 0], simp_all)
done
--- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Sep 27 17:54:20 2022 +0100
@@ -595,7 +595,7 @@
theorem satisfies_is_a_reflection:
"REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
\<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_is_a_def)
+ unfolding satisfies_is_a_def
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
nth_reflection is_list_reflection)
done
@@ -644,7 +644,7 @@
theorem satisfies_is_b_reflection:
"REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
\<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_is_b_def)
+ unfolding satisfies_is_b_def
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
nth_reflection is_list_reflection)
done
@@ -695,7 +695,7 @@
theorem satisfies_is_c_reflection:
"REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
\<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
-apply (unfold satisfies_is_c_def)
+ unfolding satisfies_is_c_def
apply (intro FOL_reflections function_reflections is_lambda_reflection
extra_reflections nth_reflection depth_apply_reflection
is_list_reflection)
@@ -751,7 +751,7 @@
theorem satisfies_is_d_reflection:
"REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
\<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_is_d_def)
+ unfolding satisfies_is_d_def
apply (intro FOL_reflections function_reflections is_lambda_reflection
extra_reflections nth_reflection depth_apply_reflection
is_list_reflection)
@@ -810,7 +810,7 @@
theorem satisfies_MH_reflection:
"REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
\<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_MH_def)
+ unfolding satisfies_MH_def
apply (intro FOL_reflections satisfies_reflections)
done
@@ -925,7 +925,7 @@
is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow>
number1(##Lset(i),rpco),
bo) \<and> pair(##Lset(i),u,bo,x))]"
-apply (unfold is_bool_of_o_def)
+ unfolding is_bool_of_o_def
apply (intro FOL_reflections function_reflections Cons_reflection)
done
--- a/src/ZF/Constructible/Wellorderings.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Tue Sep 27 17:54:20 2022 +0100
@@ -214,7 +214,7 @@
lemma wellordered_subset:
"\<lbrakk>wellordered(M, A, r); B \<subseteq> A\<rbrakk> \<Longrightarrow> wellordered(M, B, r)"
-apply (unfold wellordered_def)
+ unfolding wellordered_def
apply (blast intro: linear_rel_subset transitive_rel_subset
wellfounded_on_subset)
done
--- a/src/ZF/Epsilon.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Epsilon.thy Tue Sep 27 17:54:20 2022 +0100
@@ -40,7 +40,7 @@
subsection\<open>Basic Closure Properties\<close>
lemma arg_subset_eclose: "A \<subseteq> eclose(A)"
-apply (unfold eclose_def)
+ unfolding eclose_def
apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
apply (rule nat_0I [THEN UN_upper])
done
@@ -86,7 +86,7 @@
lemma eclose_least_lemma:
"\<lbrakk>Transset(X); A<=X; n \<in> nat\<rbrakk> \<Longrightarrow> nat_rec(n, A, \<lambda>m r. \<Union>(r)) \<subseteq> X"
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (erule nat_induct)
apply (simp add: nat_rec_0)
apply (simp add: nat_rec_succ, blast)
@@ -94,7 +94,7 @@
lemma eclose_least:
"\<lbrakk>Transset(X); A<=X\<rbrakk> \<Longrightarrow> eclose(A) \<subseteq> X"
-apply (unfold eclose_def)
+ unfolding eclose_def
apply (rule eclose_least_lemma [THEN UN_least], assumption+)
done
@@ -106,7 +106,7 @@
\<rbrakk> \<Longrightarrow> P(a)"
apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
prefer 3 apply assumption
- apply (unfold Transset_def)
+ unfolding Transset_def
apply (blast intro: ecloseD)
apply (blast intro: arg_subset_eclose [THEN subsetD])
done
@@ -168,7 +168,7 @@
done
lemma transrec: "transrec(a,H) = H(a, \<lambda>x\<in>a. transrec(x,H))"
-apply (unfold transrec_def)
+ unfolding transrec_def
apply (rule wfrec_ssubst)
apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
done
@@ -291,13 +291,13 @@
done
lemma rank_pair1: "rank(a) < rank(\<langle>a,b\<rangle>)"
-apply (unfold Pair_def)
+ unfolding Pair_def
apply (rule consI1 [THEN rank_lt, THEN lt_trans])
apply (rule consI1 [THEN consI2, THEN rank_lt])
done
lemma rank_pair2: "rank(b) < rank(\<langle>a,b\<rangle>)"
-apply (unfold Pair_def)
+ unfolding Pair_def
apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans])
apply (rule consI1 [THEN consI2, THEN rank_lt])
done
@@ -380,12 +380,12 @@
(** rec: old version for compatibility **)
lemma rec_0 [simp]: "rec(0,a,b) = a"
-apply (unfold rec_def)
+ unfolding rec_def
apply (rule recursor_0)
done
lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))"
-apply (unfold rec_def)
+ unfolding rec_def
apply (rule recursor_succ)
done
--- a/src/ZF/EquivClass.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/EquivClass.thy Tue Sep 27 17:54:20 2022 +0100
@@ -45,7 +45,7 @@
lemma equiv_comp_eq:
"equiv(A,r) \<Longrightarrow> converse(r) O r = r"
-apply (unfold equiv_def)
+ unfolding equiv_def
apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)
done
@@ -66,7 +66,7 @@
lemma equiv_class_eq:
"\<lbrakk>equiv(A,r); \<langle>a,b\<rangle>: r\<rbrakk> \<Longrightarrow> r``{a} = r``{b}"
-apply (unfold equiv_def)
+ unfolding equiv_def
apply (safe del: subsetI intro!: equalityI equiv_class_subset)
apply (unfold sym_def, blast)
done
@@ -104,7 +104,7 @@
(** Introduction/elimination rules -- needed? **)
lemma quotientI [TC]: "x \<in> A \<Longrightarrow> r``{x}: A//r"
-apply (unfold quotient_def)
+ unfolding quotient_def
apply (erule RepFunI)
done
@@ -118,7 +118,7 @@
lemma quotient_disj:
"\<lbrakk>equiv(A,r); X \<in> A//r; Y \<in> A//r\<rbrakk> \<Longrightarrow> X=Y | (X \<inter> Y \<subseteq> 0)"
-apply (unfold quotient_def)
+ unfolding quotient_def
apply (safe intro!: equiv_class_eq, assumption)
apply (unfold equiv_def trans_def sym_def, blast)
done
--- a/src/ZF/Fixedpt.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Fixedpt.thy Tue Sep 27 17:54:20 2022 +0100
@@ -32,7 +32,7 @@
by (unfold bnd_mono_def, clarify, blast)
lemma bnd_monoD1: "bnd_mono(D,h) \<Longrightarrow> h(D) \<subseteq> D"
-apply (unfold bnd_mono_def)
+ unfolding bnd_mono_def
apply (erule conjunct1)
done
@@ -45,7 +45,7 @@
lemma bnd_mono_Un:
"\<lbrakk>bnd_mono(D,h); A \<subseteq> D; B \<subseteq> D\<rbrakk> \<Longrightarrow> h(A) \<union> h(B) \<subseteq> h(A \<union> B)"
-apply (unfold bnd_mono_def)
+ unfolding bnd_mono_def
apply (rule Un_least, blast+)
done
@@ -53,7 +53,7 @@
lemma bnd_mono_UN:
"\<lbrakk>bnd_mono(D,h); \<forall>i\<in>I. A(i) \<subseteq> D\<rbrakk>
\<Longrightarrow> (\<Union>i\<in>I. h(A(i))) \<subseteq> h((\<Union>i\<in>I. A(i)))"
-apply (unfold bnd_mono_def)
+ unfolding bnd_mono_def
apply (rule UN_least)
apply (elim conjE)
apply (drule_tac x="A(i)" in spec)
@@ -193,7 +193,7 @@
(*gfp contains each post-fixedpoint that is contained in D*)
lemma gfp_upperbound: "\<lbrakk>A \<subseteq> h(A); A<=D\<rbrakk> \<Longrightarrow> A \<subseteq> gfp(D,h)"
-apply (unfold gfp_def)
+ unfolding gfp_def
apply (rule PowI [THEN CollectI, THEN Union_upper])
apply (assumption+)
done
@@ -210,7 +210,7 @@
lemma gfp_least:
"\<lbrakk>bnd_mono(D,h); \<And>X. \<lbrakk>X \<subseteq> h(X); X<=D\<rbrakk> \<Longrightarrow> X<=A\<rbrakk> \<Longrightarrow>
gfp(D,h) \<subseteq> A"
-apply (unfold gfp_def)
+ unfolding gfp_def
apply (blast dest: bnd_monoD1)
done
--- a/src/ZF/IMP/Equiv.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/IMP/Equiv.thy Tue Sep 27 17:54:20 2022 +0100
@@ -66,7 +66,7 @@
apply safe
apply simp_all
apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
- apply (unfold Gamma_def)
+ unfolding Gamma_def
apply force
txt \<open>\<open>if\<close>\<close>
apply auto
--- a/src/ZF/Induct/Comb.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Comb.thy Tue Sep 27 17:54:20 2022 +0100
@@ -86,7 +86,7 @@
lemma diamond_strip_lemmaD [rule_format]:
"\<lbrakk>diamond(r); \<langle>x,y\<rangle>:r^+\<rbrakk> \<Longrightarrow>
\<forall>y'. <x,y'>:r \<longrightarrow> (\<exists>z. <y',z>: r^+ \<and> \<langle>y,z\<rangle>: r)"
- apply (unfold diamond_def)
+ unfolding diamond_def
apply (erule trancl_induct)
apply (blast intro: r_into_trancl)
apply clarify
@@ -186,7 +186,7 @@
by (blast intro: comb_I)
lemma not_diamond_contract: "\<not> diamond(contract)"
- apply (unfold diamond_def)
+ unfolding diamond_def
apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
elim!: I_contract_E)
done
@@ -228,7 +228,7 @@
lemma diamond_parcontract: "diamond(parcontract)"
\<comment> \<open>Church-Rosser property for parallel contraction\<close>
- apply (unfold diamond_def)
+ unfolding diamond_def
apply (rule impI [THEN allI, THEN allI])
apply (erule parcontract.induct)
apply (blast elim!: comb.free_elims intro: parcontract_combD2)+
--- a/src/ZF/Induct/FoldSet.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/FoldSet.thy Tue Sep 27 17:54:20 2022 +0100
@@ -144,7 +144,7 @@
lemma (in fold_typing) fold_equality:
"\<langle>C,y\<rangle> \<in> fold_set(A,B,f,e) \<Longrightarrow> fold[B](f,e,C) = y"
-apply (unfold fold_def)
+ unfolding fold_def
apply (frule fold_set.dom_subset [THEN subsetD], clarify)
apply (rule the_equality)
apply (rule_tac [2] A=C in fold_typing.fold_set_determ)
@@ -155,7 +155,7 @@
done
lemma fold_0 [simp]: "e \<in> B \<Longrightarrow> fold[B](f,e,0) = e"
-apply (unfold fold_def)
+ unfolding fold_def
apply (blast elim!: empty_fold_setE intro: fold_set.intros)
done
@@ -193,7 +193,7 @@
lemma (in fold_typing) fold_cons:
"\<lbrakk>C\<in>Fin(A); c\<in>A; c\<notin>C\<rbrakk>
\<Longrightarrow> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))"
-apply (unfold fold_def)
+ unfolding fold_def
apply (simp add: fold_cons_lemma)
apply (rule the_equality, auto)
apply (subgoal_tac [2] "\<langle>C, y\<rangle> \<in> fold_set(A, B, f, e)")
@@ -363,7 +363,7 @@
"\<lbrakk>setsum(f, A) = $# succ(n); n\<in>nat\<rbrakk>\<Longrightarrow> \<exists>a\<in>A. #0 $< f(a)"
apply (case_tac "Finite (A) ")
apply (blast intro: setsum_succD_lemma)
-apply (unfold setsum_def)
+ unfolding setsum_def
apply (auto simp del: int_of_0 int_of_succ simp add: int_succ_int_1 [symmetric] int_of_0 [symmetric])
done
--- a/src/ZF/Induct/Multiset.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Multiset.thy Tue Sep 27 17:54:20 2022 +0100
@@ -393,7 +393,7 @@
done
lemma msize_eq_succ_imp_elem: "\<lbrakk>msize(M)= $# succ(n); n \<in> nat\<rbrakk> \<Longrightarrow> \<exists>a. a \<in> mset_of(M)"
-apply (unfold msize_def)
+ unfolding msize_def
apply (blast dest: setsum_succD)
done
@@ -480,7 +480,7 @@
(\<forall>a \<in> mset_of(M). setsum(\<lambda>z. $# mcount(M(a:=M`a #- 1), z), A) =
(if a \<in> A then setsum(\<lambda>z. $# mcount(M, z), A) $- #1
else setsum(\<lambda>z. $# mcount(M, z), A))))"
-apply (unfold multiset_def)
+ unfolding multiset_def
apply (erule Finite_induct)
apply (auto simp add: multiset_fun_iff)
apply (unfold mset_of_def mcount_def)
--- a/src/ZF/Induct/Primrec.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Primrec.thy Tue Sep 27 17:54:20 2022 +0100
@@ -240,7 +240,7 @@
declare list_add_type [simp]
lemma SC_case: "l \<in> list(nat) \<Longrightarrow> SC ` l < ack(1, list_add(l))"
- apply (unfold SC_def)
+ unfolding SC_def
apply (erule list.cases)
apply (simp add: succ_iff)
apply (simp add: ack_1 add_le_self)
@@ -260,7 +260,7 @@
lemma PROJ_case [rule_format]:
"l \<in> list(nat) \<Longrightarrow> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"
- apply (unfold PROJ_def)
+ unfolding PROJ_def
apply simp
apply (erule list.induct)
apply (simp add: nat_0_le)
@@ -322,7 +322,7 @@
g \<in> prim_rec; kg\<in>nat;
l \<in> list(nat)\<rbrakk>
\<Longrightarrow> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"
- apply (unfold PREC_def)
+ unfolding PREC_def
apply (erule list.cases)
apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
apply simp
--- a/src/ZF/Induct/PropLog.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/PropLog.thy Tue Sep 27 17:54:20 2022 +0100
@@ -180,7 +180,7 @@
subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close>
theorem soundness: "H |- p \<Longrightarrow> H |= p"
- apply (unfold logcon_def)
+ unfolding logcon_def
apply (induct set: thms)
apply auto
done
--- a/src/ZF/Induct/Rmap.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Rmap.thy Tue Sep 27 17:54:20 2022 +0100
@@ -46,7 +46,7 @@
done
lemma rmap_functional: "function(r) \<Longrightarrow> function(rmap(r))"
- apply (unfold function_def)
+ unfolding function_def
apply (rule impI [THEN allI, THEN allI])
apply (erule rmap.induct)
apply blast+
--- a/src/ZF/Induct/Term.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Term.thy Tue Sep 27 17:54:20 2022 +0100
@@ -169,7 +169,7 @@
lemma term_map_type [TC]:
"\<lbrakk>t \<in> term(A); \<And>x. x \<in> A \<Longrightarrow> f(x): B\<rbrakk> \<Longrightarrow> term_map(f,t) \<in> term(B)"
- apply (unfold term_map_def)
+ unfolding term_map_def
apply (erule term_rec_simple_type)
apply fast
done
--- a/src/ZF/Induct/Tree_Forest.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Tue Sep 27 17:54:20 2022 +0100
@@ -109,7 +109,7 @@
\<rbrakk> \<Longrightarrow> (\<forall>t \<in> tree(A). tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
(\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
\<comment> \<open>Mutually recursive version.\<close>
- apply (unfold Ball_def)
+ unfolding Ball_def
apply (rule tree_forest.mutual_induct)
apply simp_all
done
--- a/src/ZF/IntDiv.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/IntDiv.thy Tue Sep 27 17:54:20 2022 +0100
@@ -688,12 +688,12 @@
done
lemma negateSnd_eq [simp]: "negateSnd (\<langle>q,r\<rangle>) = <q, $-r>"
-apply (unfold negateSnd_def)
+ unfolding negateSnd_def
apply auto
done
lemma negateSnd_type: "qr \<in> int * int \<Longrightarrow> negateSnd (qr) \<in> int * int"
-apply (unfold negateSnd_def)
+ unfolding negateSnd_def
apply auto
done
@@ -735,7 +735,7 @@
by (simp add: zdiv_def)
lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
-apply (unfold zdiv_def)
+ unfolding zdiv_def
apply (blast intro: fst_type divAlg_type)
done
@@ -746,7 +746,7 @@
by (simp add: zmod_def)
lemma zmod_type [iff,TC]: "z zmod w \<in> int"
-apply (unfold zmod_def)
+ unfolding zmod_def
apply (rule snd_type)
apply (blast intro: divAlg_type)
done
--- a/src/ZF/List.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/List.thy Tue Sep 27 17:54:20 2022 +0100
@@ -267,7 +267,7 @@
(** set_of_list **)
lemma set_of_list_type [TC]: "l \<in> list(A) \<Longrightarrow> set_of_list(l) \<in> Pow(A)"
-apply (unfold set_of_list_list_def)
+ unfolding set_of_list_list_def
apply (erule list_rec_type, auto)
done
@@ -463,7 +463,7 @@
(** min FIXME: replace by Int! **)
(* Min theorems are also true for i, j ordinals *)
lemma min_sym: "\<lbrakk>i \<in> nat; j \<in> nat\<rbrakk> \<Longrightarrow> min(i,j)=min(j,i)"
-apply (unfold min_def)
+ unfolding min_def
apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
done
@@ -471,17 +471,17 @@
by (unfold min_def, auto)
lemma min_0 [simp]: "i \<in> nat \<Longrightarrow> min(0,i) = 0"
-apply (unfold min_def)
+ unfolding min_def
apply (auto dest: not_lt_imp_le)
done
lemma min_02 [simp]: "i \<in> nat \<Longrightarrow> min(i, 0) = 0"
-apply (unfold min_def)
+ unfolding min_def
apply (auto dest: not_lt_imp_le)
done
lemma lt_min_iff: "\<lbrakk>i \<in> nat; j \<in> nat; k \<in> nat\<rbrakk> \<Longrightarrow> i<min(j,k) \<longleftrightarrow> i<j \<and> i<k"
-apply (unfold min_def)
+ unfolding min_def
apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
done
@@ -689,7 +689,7 @@
(** take **)
lemma take_0 [simp]: "xs:list(A) \<Longrightarrow> take(0, xs) = Nil"
-apply (unfold take_def)
+ unfolding take_def
apply (erule list.induct, auto)
done
@@ -917,7 +917,7 @@
lemma length_zip [rule_format]:
"xs:list(A) \<Longrightarrow> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
min(length(xs), length(ys))"
-apply (unfold min_def)
+ unfolding min_def
apply (induct_tac "xs", simp_all, clarify)
apply (erule_tac a = ys in list.cases, auto)
done
@@ -1200,7 +1200,7 @@
lemma sublist_type [simp,TC]:
"xs:list(B) \<Longrightarrow> sublist(xs, A):list(B)"
-apply (unfold sublist_def)
+ unfolding sublist_def
apply (induct_tac "xs")
apply (auto simp add: filter_append map_app_distrib)
done
@@ -1212,7 +1212,7 @@
lemma sublist_append:
"\<lbrakk>xs:list(B); ys:list(B)\<rbrakk> \<Longrightarrow>
sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j \<in> nat. j #+ length(xs): A})"
-apply (unfold sublist_def)
+ unfolding sublist_def
apply (erule_tac l = ys in list_append_induct, simp)
apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
--- a/src/ZF/Nat.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Nat.thy Tue Sep 27 17:54:20 2022 +0100
@@ -108,13 +108,13 @@
lemma Ord_nat [iff]: "Ord(nat)"
apply (rule OrdI)
apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (rule ballI)
apply (erule nat_induct, auto)
done
lemma Limit_nat [iff]: "Limit(nat)"
-apply (unfold Limit_def)
+ unfolding Limit_def
apply (safe intro!: ltI Ord_nat)
apply (erule ltD)
done
--- a/src/ZF/Order.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Order.thy Tue Sep 27 17:54:20 2022 +0100
@@ -142,13 +142,13 @@
lemma tot_ord_subset:
"\<lbrakk>tot_ord(A,r); B<=A\<rbrakk> \<Longrightarrow> tot_ord(B,r)"
-apply (unfold tot_ord_def)
+ unfolding tot_ord_def
apply (fast elim!: part_ord_subset linear_subset)
done
lemma well_ord_subset:
"\<lbrakk>well_ord(A,r); B<=A\<rbrakk> \<Longrightarrow> well_ord(B,r)"
-apply (unfold well_ord_def)
+ unfolding well_ord_def
apply (fast elim!: tot_ord_subset wf_on_subset_A)
done
@@ -162,7 +162,7 @@
by (unfold trans_on_def, blast)
lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) \<longleftrightarrow> part_ord(A,r)"
-apply (unfold part_ord_def)
+ unfolding part_ord_def
apply (simp add: irrefl_Int_iff trans_on_Int_iff)
done
@@ -170,7 +170,7 @@
by (unfold linear_def, blast)
lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) \<longleftrightarrow> tot_ord(A,r)"
-apply (unfold tot_ord_def)
+ unfolding tot_ord_def
apply (simp add: part_ord_Int_iff linear_Int_iff)
done
@@ -179,7 +179,7 @@
done
lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) \<longleftrightarrow> well_ord(A,r)"
-apply (unfold well_ord_def)
+ unfolding well_ord_def
apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
done
@@ -199,7 +199,7 @@
by (unfold trans_on_def, blast)
lemma part_ord_0: "part_ord(0,r)"
-apply (unfold part_ord_def)
+ unfolding part_ord_def
apply (simp add: irrefl_0 trans_on_0)
done
@@ -207,7 +207,7 @@
by (unfold linear_def, blast)
lemma tot_ord_0: "tot_ord(0,r)"
-apply (unfold tot_ord_def)
+ unfolding tot_ord_def
apply (simp add: part_ord_0 linear_0)
done
@@ -215,7 +215,7 @@
by (unfold wf_on_def wf_def, blast)
lemma well_ord_0: "well_ord(0,r)"
-apply (unfold well_ord_def)
+ unfolding well_ord_def
apply (simp add: tot_ord_0 wf_on_0)
done
@@ -228,7 +228,7 @@
by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
lemma well_ord_unit: "well_ord({a},0)"
-apply (unfold well_ord_def)
+ unfolding well_ord_def
apply (simp add: tot_ord_unit wf_on_any_0)
done
@@ -297,7 +297,7 @@
lemma mono_map_trans:
"\<lbrakk>g \<in> mono_map(A,r,B,s); f \<in> mono_map(B,s,C,t)\<rbrakk>
\<Longrightarrow> (f O g): mono_map(A,r,C,t)"
-apply (unfold mono_map_def)
+ unfolding mono_map_def
apply (auto simp add: comp_fun)
done
@@ -494,7 +494,7 @@
lemma converse_ord_iso_map:
"converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"
-apply (unfold ord_iso_map_def)
+ unfolding ord_iso_map_def
apply (blast intro: ord_iso_sym)
done
@@ -514,12 +514,12 @@
\<Longrightarrow> ord_iso_map(A,r,B,s)
\<in> mono_map(domain(ord_iso_map(A,r,B,s)), r,
range(ord_iso_map(A,r,B,s)), s)"
-apply (unfold mono_map_def)
+ unfolding mono_map_def
apply (simp (no_asm_simp) add: ord_iso_map_fun)
apply safe
apply (subgoal_tac "x \<in> A \<and> ya:A \<and> y \<in> B \<and> yb:B")
apply (simp add: apply_equality [OF _ ord_iso_map_fun])
- apply (unfold ord_iso_map_def)
+ unfolding ord_iso_map_def
apply (blast intro: well_ord_iso_preserving, blast)
done
@@ -542,7 +542,7 @@
"\<lbrakk>well_ord(A,r); well_ord(B,s);
a \<in> A; a \<notin> domain(ord_iso_map(A,r,B,s))\<rbrakk>
\<Longrightarrow> domain(ord_iso_map(A,r,B,s)) \<subseteq> pred(A, a, r)"
-apply (unfold ord_iso_map_def)
+ unfolding ord_iso_map_def
apply (safe intro!: predI)
(*Case analysis on xa vs a in r *)
apply (simp (no_asm_simp))
@@ -621,7 +621,7 @@
by (unfold trans_on_def, blast)
lemma part_ord_converse: "part_ord(A,r) \<Longrightarrow> part_ord(A,converse(r))"
-apply (unfold part_ord_def)
+ unfolding part_ord_def
apply (blast intro!: irrefl_converse trans_on_converse)
done
@@ -629,7 +629,7 @@
by (unfold linear_def, blast)
lemma tot_ord_converse: "tot_ord(A,r) \<Longrightarrow> tot_ord(A,converse(r))"
-apply (unfold tot_ord_def)
+ unfolding tot_ord_def
apply (blast intro!: part_ord_converse linear_converse)
done
--- a/src/ZF/OrderArith.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/OrderArith.thy Tue Sep 27 17:54:20 2022 +0100
@@ -69,7 +69,7 @@
subsubsection\<open>Type checking\<close>
lemma radd_type: "radd(A,r,B,s) \<subseteq> (A+B) * (A+B)"
-apply (unfold radd_def)
+ unfolding radd_def
apply (rule Collect_subset)
done
@@ -127,7 +127,7 @@
"\<lbrakk>f \<in> ord_iso(A,r,A',r'); g \<in> ord_iso(B,s,B',s')\<rbrakk> \<Longrightarrow>
(\<lambda>z\<in>A+B. case(\<lambda>x. Inl(f`x), \<lambda>y. Inr(g`y), z))
\<in> ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"
-apply (unfold ord_iso_def)
+ unfolding ord_iso_def
apply (safe intro!: sum_bij)
(*Do the beta-reductions now*)
apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type])
@@ -232,7 +232,7 @@
"\<lbrakk>f \<in> ord_iso(A,r,A',r'); g \<in> ord_iso(B,s,B',s')\<rbrakk>
\<Longrightarrow> (lam \<langle>x,y\<rangle>:A*B. \<langle>f`x, g`y\<rangle>)
\<in> ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"
-apply (unfold ord_iso_def)
+ unfolding ord_iso_def
apply (safe intro!: prod_bij)
apply (simp_all add: bij_is_fun [THEN apply_type])
apply (blast intro: bij_is_inj [THEN inj_apply_equality])
@@ -337,7 +337,7 @@
lemma part_ord_rvimage:
"\<lbrakk>f \<in> inj(A,B); part_ord(B,r)\<rbrakk> \<Longrightarrow> part_ord(A, rvimage(A,f,r))"
-apply (unfold part_ord_def)
+ unfolding part_ord_def
apply (blast intro!: irrefl_rvimage trans_on_rvimage)
done
@@ -351,7 +351,7 @@
lemma tot_ord_rvimage:
"\<lbrakk>f \<in> inj(A,B); tot_ord(B,r)\<rbrakk> \<Longrightarrow> tot_ord(A, rvimage(A,f,r))"
-apply (unfold tot_ord_def)
+ unfolding tot_ord_def
apply (blast intro!: part_ord_rvimage linear_rvimage)
done
@@ -391,7 +391,7 @@
lemma ord_iso_rvimage:
"f \<in> bij(A,B) \<Longrightarrow> f \<in> ord_iso(A, rvimage(A,f,s), B, s)"
-apply (unfold ord_iso_def)
+ unfolding ord_iso_def
apply (simp add: rvimage_iff)
done
--- a/src/ZF/OrderType.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/OrderType.thy Tue Sep 27 17:54:20 2022 +0100
@@ -80,7 +80,7 @@
apply (frule lt_pred_Memrel)
apply (erule ltE)
apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
-apply (unfold ord_iso_def)
+ unfolding ord_iso_def
(*Combining the two simplifications causes looping*)
apply (simp (no_asm_simp))
apply (blast intro: bij_is_fun [THEN apply_type] Ord_trans)
@@ -156,7 +156,7 @@
lemma Ord_ordertype:
"well_ord(A,r) \<Longrightarrow> Ord(ordertype(A,r))"
-apply (unfold ordertype_def)
+ unfolding ordertype_def
apply (subst image_fun [OF ordermap_type subset_refl])
apply (rule OrdI [OF _ Ord_is_Transset])
prefer 2 apply (blast intro: Ord_ordermap)
@@ -201,7 +201,7 @@
lemma ordertype_ord_iso:
"well_ord(A,r)
\<Longrightarrow> ordermap(A,r) \<in> ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
-apply (unfold ord_iso_def)
+ unfolding ord_iso_def
apply (safe elim!: well_ord_is_wf
intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
apply (blast dest!: converse_ordermap_mono)
@@ -272,7 +272,7 @@
lemma ordertype_unfold:
"ordertype(A,r) = {ordermap(A,r)`y . y \<in> A}"
-apply (unfold ordertype_def)
+ unfolding ordertype_def
apply (rule image_fun [OF ordermap_type subset_refl])
done
@@ -311,7 +311,7 @@
(*proof by Krzysztof Grabczewski*)
lemma Ord_is_Ord_alt: "Ord(i) \<Longrightarrow> Ord_alt(i)"
-apply (unfold Ord_alt_def)
+ unfolding Ord_alt_def
apply (rule conjI)
apply (erule well_ord_Memrel)
apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)
@@ -363,7 +363,7 @@
lemma pred_Inl_bij:
"a \<in> A \<Longrightarrow> (\<lambda>x\<in>pred(A,a,r). Inl(x))
\<in> bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
-apply (unfold pred_def)
+ unfolding pred_def
apply (rule_tac d = "case (\<lambda>x. x, \<lambda>y. y) " in lam_bijective)
apply auto
done
@@ -709,7 +709,7 @@
lemma Ord_odiff [simp,TC]:
"\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i--j)"
-apply (unfold odiff_def)
+ unfolding odiff_def
apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
done
@@ -750,7 +750,7 @@
lemma Ord_omult [simp,TC]:
"\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i**j)"
-apply (unfold omult_def)
+ unfolding omult_def
apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
done
@@ -797,7 +797,7 @@
lemma lt_omult:
"\<lbrakk>Ord(i); Ord(j); k<j**i\<rbrakk>
\<Longrightarrow> \<exists>j' i'. k = j**i' ++ j' \<and> j'<j \<and> i'<i"
-apply (unfold omult_def)
+ unfolding omult_def
apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
apply (safe elim!: ltE)
apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd
@@ -807,7 +807,7 @@
lemma omult_oadd_lt:
"\<lbrakk>j'<j; i'<i\<rbrakk> \<Longrightarrow> j**i' ++ j' < j**i"
-apply (unfold omult_def)
+ unfolding omult_def
apply (rule ltI)
prefer 2
apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
@@ -834,19 +834,19 @@
text\<open>Ordinal multiplication by zero\<close>
lemma omult_0 [simp]: "i**0 = 0"
-apply (unfold omult_def)
+ unfolding omult_def
apply (simp (no_asm_simp))
done
lemma omult_0_left [simp]: "0**i = 0"
-apply (unfold omult_def)
+ unfolding omult_def
apply (simp (no_asm_simp))
done
text\<open>Ordinal multiplication by 1\<close>
lemma omult_1 [simp]: "Ord(i) \<Longrightarrow> i**1 = i"
-apply (unfold omult_def)
+ unfolding omult_def
apply (rule_tac s1="Memrel(i)"
in ord_isoI [THEN ordertype_eq, THEN trans])
apply (rule_tac c = snd and d = "\<lambda>z.\<langle>0,z\<rangle>" in lam_bijective)
@@ -854,7 +854,7 @@
done
lemma omult_1_left [simp]: "Ord(i) \<Longrightarrow> 1**i = i"
-apply (unfold omult_def)
+ unfolding omult_def
apply (rule_tac s1="Memrel(i)"
in ord_isoI [THEN ordertype_eq, THEN trans])
apply (rule_tac c = fst and d = "\<lambda>z.\<langle>z,0\<rangle>" in lam_bijective)
@@ -886,7 +886,7 @@
lemma omult_assoc:
"\<lbrakk>Ord(i); Ord(j); Ord(k)\<rbrakk> \<Longrightarrow> (i**j)**k = i**(j**k)"
-apply (unfold omult_def)
+ unfolding omult_def
apply (rule ordertype_eq [THEN trans])
apply (rule prod_ord_iso_cong [OF ord_iso_refl
ordertype_ord_iso [THEN ord_iso_sym]])
--- a/src/ZF/Ordinal.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Ordinal.thy Tue Sep 27 17:54:20 2022 +0100
@@ -40,7 +40,7 @@
by (unfold Transset_def, blast)
lemma Transset_iff_Union_succ: "Transset(A) <-> \<Union>(succ(A)) = A"
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (blast elim!: equalityE)
done
@@ -157,12 +157,12 @@
by (blast intro: Ord_succ dest!: Ord_succD)
lemma Ord_Un [intro,simp,TC]: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i \<union> j)"
-apply (unfold Ord_def)
+ unfolding Ord_def
apply (blast intro!: Transset_Un)
done
lemma Ord_Int [TC]: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i \<inter> j)"
-apply (unfold Ord_def)
+ unfolding Ord_def
apply (blast intro!: Transset_Int)
done
@@ -188,7 +188,7 @@
lemma ltE:
"\<lbrakk>i<j; \<lbrakk>i\<in>j; Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-apply (unfold lt_def)
+ unfolding lt_def
apply (blast intro: Ord_in_Ord)
done
@@ -214,7 +214,7 @@
by (blast intro!: ltI elim!: ltE intro: Ord_trans)
lemma lt_not_sym: "i<j \<Longrightarrow> \<not> (j<i)"
-apply (unfold lt_def)
+ unfolding lt_def
apply (blast elim: mem_asym)
done
@@ -297,7 +297,7 @@
(*The membership relation (as a set) is well-founded.
Proof idea: show A<=B by applying the foundation axiom to A-B *)
lemma wf_Memrel: "wf(Memrel(A))"
-apply (unfold wf_def)
+ unfolding wf_def
apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast)
done
@@ -630,17 +630,17 @@
subsection\<open>Limit Ordinals -- General Properties\<close>
lemma Limit_Union_eq: "Limit(i) \<Longrightarrow> \<Union>(i) = i"
-apply (unfold Limit_def)
+ unfolding Limit_def
apply (fast intro!: ltI elim!: ltE elim: Ord_trans)
done
lemma Limit_is_Ord: "Limit(i) \<Longrightarrow> Ord(i)"
-apply (unfold Limit_def)
+ unfolding Limit_def
apply (erule conjunct1)
done
lemma Limit_has_0: "Limit(i) \<Longrightarrow> 0 < i"
-apply (unfold Limit_def)
+ unfolding Limit_def
apply (erule conjunct2 [THEN conjunct1])
done
--- a/src/ZF/Perm.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Perm.thy Tue Sep 27 17:54:20 2022 +0100
@@ -42,17 +42,17 @@
subsection\<open>Surjective Function Space\<close>
lemma surj_is_fun: "f \<in> surj(A,B) \<Longrightarrow> f \<in> A->B"
-apply (unfold surj_def)
+ unfolding surj_def
apply (erule CollectD1)
done
lemma fun_is_surj: "f \<in> Pi(A,B) \<Longrightarrow> f \<in> surj(A,range(f))"
-apply (unfold surj_def)
+ unfolding surj_def
apply (blast intro: apply_equality range_of_fun domain_type)
done
lemma surj_range: "f \<in> surj(A,B) \<Longrightarrow> range(f)=B"
-apply (unfold surj_def)
+ unfolding surj_def
apply (best intro: apply_Pair elim: range_type)
done
@@ -83,14 +83,14 @@
subsection\<open>Injective Function Space\<close>
lemma inj_is_fun: "f \<in> inj(A,B) \<Longrightarrow> f \<in> A->B"
-apply (unfold inj_def)
+ unfolding inj_def
apply (erule CollectD1)
done
text\<open>Good for dealing with sets of pairs, but a bit ugly in use [used in AC]\<close>
lemma inj_equality:
"\<lbrakk>\<langle>a,b\<rangle>:f; \<langle>c,b\<rangle>:f; f \<in> inj(A,B)\<rbrakk> \<Longrightarrow> a=c"
-apply (unfold inj_def)
+ unfolding inj_def
apply (blast dest: Pair_mem_PiD)
done
@@ -115,12 +115,12 @@
subsection\<open>Bijections\<close>
lemma bij_is_inj: "f \<in> bij(A,B) \<Longrightarrow> f \<in> inj(A,B)"
-apply (unfold bij_def)
+ unfolding bij_def
apply (erule IntD1)
done
lemma bij_is_surj: "f \<in> bij(A,B) \<Longrightarrow> f \<in> surj(A,B)"
-apply (unfold bij_def)
+ unfolding bij_def
apply (erule IntD2)
done
@@ -133,7 +133,7 @@
\<And>x. x \<in> A \<Longrightarrow> d(c(x)) = x;
\<And>y. y \<in> B \<Longrightarrow> c(d(y)) = y
\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
-apply (unfold bij_def)
+ unfolding bij_def
apply (blast intro!: lam_injective lam_surjective)
done
@@ -147,7 +147,7 @@
subsection\<open>Identity Function\<close>
lemma idI [intro!]: "a \<in> A \<Longrightarrow> \<langle>a,a\<rangle> \<in> id(A)"
-apply (unfold id_def)
+ unfolding id_def
apply (erule lamI)
done
@@ -155,17 +155,17 @@
by (simp add: id_def lam_def, blast)
lemma id_type: "id(A) \<in> A->A"
-apply (unfold id_def)
+ unfolding id_def
apply (rule lam_type, assumption)
done
lemma id_conv [simp]: "x \<in> A \<Longrightarrow> id(A)`x = x"
-apply (unfold id_def)
+ unfolding id_def
apply (simp (no_asm_simp))
done
lemma id_mono: "A<=B \<Longrightarrow> id(A) \<subseteq> id(B)"
-apply (unfold id_def)
+ unfolding id_def
apply (erule lam_mono)
done
@@ -182,12 +182,12 @@
done
lemma id_bij: "id(A): bij(A,A)"
-apply (unfold bij_def)
+ unfolding bij_def
apply (blast intro: id_inj id_surj)
done
lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B"
-apply (unfold id_def)
+ unfolding id_def
apply (force intro!: lam_type dest: apply_type)
done
@@ -199,7 +199,7 @@
subsection\<open>Converse of a Function\<close>
lemma inj_converse_fun: "f \<in> inj(A,B) \<Longrightarrow> converse(f) \<in> range(f)->A"
-apply (unfold inj_def)
+ unfolding inj_def
apply (simp (no_asm_simp) add: Pi_iff function_def)
apply (erule CollectE)
apply (simp (no_asm_simp) add: apply_iff)
@@ -251,7 +251,7 @@
text\<open>Adding this as an intro! rule seems to cause looping\<close>
lemma bij_converse_bij [TC]: "f \<in> bij(A,B) \<Longrightarrow> converse(f): bij(B,A)"
-apply (unfold bij_def)
+ unfolding bij_def
apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
done
@@ -372,13 +372,13 @@
lemma comp_surj:
"\<lbrakk>g \<in> surj(A,B); f \<in> surj(B,C)\<rbrakk> \<Longrightarrow> (f O g) \<in> surj(A,C)"
-apply (unfold surj_def)
+ unfolding surj_def
apply (blast intro!: comp_fun comp_fun_apply)
done
lemma comp_bij:
"\<lbrakk>g \<in> bij(A,B); f \<in> bij(B,C)\<rbrakk> \<Longrightarrow> (f O g) \<in> bij(A,C)"
-apply (unfold bij_def)
+ unfolding bij_def
apply (blast intro: comp_inj comp_surj)
done
@@ -405,7 +405,7 @@
lemma comp_mem_surjD1:
"\<lbrakk>(f O g): surj(A,C); g \<in> A->B; f \<in> B->C\<rbrakk> \<Longrightarrow> f \<in> surj(B,C)"
-apply (unfold surj_def)
+ unfolding surj_def
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
done
@@ -452,7 +452,7 @@
lemma fg_imp_bijective:
"\<lbrakk>f \<in> A->B; g \<in> B->A; f O g = id(B); g O f = id(A)\<rbrakk> \<Longrightarrow> f \<in> bij(A,B)"
-apply (unfold bij_def)
+ unfolding bij_def
apply (simp add: comp_eq_id_iff)
apply (blast intro: f_imp_injective f_imp_surjective apply_funtype)
done
@@ -513,7 +513,7 @@
lemma restrict_inj:
"\<lbrakk>f \<in> inj(A,B); C<=A\<rbrakk> \<Longrightarrow> restrict(f,C): inj(C,B)"
-apply (unfold inj_def)
+ unfolding inj_def
apply (safe elim!: restrict_type2, auto)
done
@@ -532,14 +532,14 @@
subsubsection\<open>Lemmas for Ramsey's Theorem\<close>
lemma inj_weaken_type: "\<lbrakk>f \<in> inj(A,B); B<=D\<rbrakk> \<Longrightarrow> f \<in> inj(A,D)"
-apply (unfold inj_def)
+ unfolding inj_def
apply (blast intro: fun_weaken_type)
done
lemma inj_succ_restrict:
"\<lbrakk>f \<in> inj(succ(m), A)\<rbrakk> \<Longrightarrow> restrict(f,m) \<in> inj(m, A-{f`m})"
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
-apply (unfold inj_def)
+ unfolding inj_def
apply (fast elim: range_type mem_irrefl dest: apply_equality)
done
@@ -547,7 +547,7 @@
lemma inj_extend:
"\<lbrakk>f \<in> inj(A,B); a\<notin>A; b\<notin>B\<rbrakk>
\<Longrightarrow> cons(\<langle>a,b\<rangle>,f) \<in> inj(cons(a,A), cons(b,B))"
-apply (unfold inj_def)
+ unfolding inj_def
apply (force intro: apply_type simp add: fun_extend)
done
--- a/src/ZF/QUniv.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/QUniv.thy Tue Sep 27 17:54:20 2022 +0100
@@ -47,7 +47,7 @@
by (simp add: quniv_def)
lemma quniv_mono: "A<=B \<Longrightarrow> quniv(A) \<subseteq> quniv(B)"
-apply (unfold quniv_def)
+ unfolding quniv_def
apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
done
@@ -67,7 +67,7 @@
lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD]
lemma Pow_univ_subset_quniv: "Pow(univ(A)) \<subseteq> quniv(A)"
-apply (unfold quniv_def)
+ unfolding quniv_def
apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
done
@@ -92,7 +92,7 @@
subsection\<open>Quine Disjoint Sum\<close>
lemma QInl_subset_univ: "a \<subseteq> univ(A) \<Longrightarrow> QInl(a) \<subseteq> univ(A)"
-apply (unfold QInl_def)
+ unfolding QInl_def
apply (erule empty_subsetI [THEN QPair_subset_univ])
done
@@ -103,7 +103,7 @@
subset_trans [OF naturals_subset_nat nat_subset_univ]
lemma QInr_subset_univ: "a \<subseteq> univ(A) \<Longrightarrow> QInr(a) \<subseteq> univ(A)"
-apply (unfold QInr_def)
+ unfolding QInr_def
apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
done
@@ -178,7 +178,7 @@
lemma QPair_Int_Vfrom_subset:
"Transset(X) \<Longrightarrow>
<a;b> \<inter> Vfrom(X,i) \<subseteq> <a \<inter> Vfrom(X,i); b \<inter> Vfrom(X,i)>"
-apply (unfold QPair_def)
+ unfolding QPair_def
apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
done
--- a/src/ZF/Resid/Confluence.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Resid/Confluence.thy Tue Sep 27 17:54:20 2022 +0100
@@ -110,7 +110,7 @@
apply (blast intro: red1D1 redD2)
apply (blast intro: red1D1 redD2)
apply (cut_tac confluence_beta_reduction)
-apply (unfold confluence_def)
+ unfolding confluence_def
apply (blast intro: Sred.trans)
done
--- a/src/ZF/Resid/Residuals.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Resid/Residuals.thy Tue Sep 27 17:54:20 2022 +0100
@@ -85,21 +85,21 @@
lemma res_Fun [simp]:
"\<lbrakk>s \<sim> t; regular(t)\<rbrakk>\<Longrightarrow> Fun(s) |> Fun(t) = Fun(s |> t)"
-apply (unfold res_func_def)
+ unfolding res_func_def
apply (blast intro: comp_resfuncD residuals_function)
done
lemma res_App [simp]:
"\<lbrakk>s \<sim> u; regular(u); t \<sim> v; regular(v); b \<in> bool\<rbrakk>
\<Longrightarrow> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
-apply (unfold res_func_def)
+ unfolding res_func_def
apply (blast dest!: comp_resfuncD intro: residuals_function)
done
lemma res_redex [simp]:
"\<lbrakk>s \<sim> u; regular(u); t \<sim> v; regular(v); b \<in> bool\<rbrakk>
\<Longrightarrow> App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"
-apply (unfold res_func_def)
+ unfolding res_func_def
apply (blast elim!: redexes.free_elims dest!: comp_resfuncD
intro: residuals_function)
done
--- a/src/ZF/Sum.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Sum.thy Tue Sep 27 17:54:20 2022 +0100
@@ -29,7 +29,7 @@
lemma Part_iff:
"a \<in> Part(A,h) \<longleftrightarrow> a \<in> A \<and> (\<exists>y. a=h(y))"
-apply (unfold Part_def)
+ unfolding Part_def
apply (rule separation)
done
@@ -46,7 +46,7 @@
done
lemma Part_subset: "Part(A,h) \<subseteq> A"
-apply (unfold Part_def)
+ unfolding Part_def
apply (rule Collect_subset)
done
--- a/src/ZF/Trancl.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Trancl.thy Tue Sep 27 17:54:20 2022 +0100
@@ -101,7 +101,7 @@
by (rule bnd_monoI, blast+)
lemma rtrancl_mono: "r<=s \<Longrightarrow> r^* \<subseteq> s^*"
-apply (unfold rtrancl_def)
+ unfolding rtrancl_def
apply (rule lfp_mono)
apply (rule rtrancl_bnd_mono)+
apply blast
@@ -172,7 +172,7 @@
(*transitivity of transitive closure\<And>-- by induction.*)
lemma trans_rtrancl: "trans(r^*)"
-apply (unfold trans_def)
+ unfolding trans_def
apply (intro allI impI)
apply (erule_tac b = z in rtrancl_induct, assumption)
apply (blast intro: rtrancl_into_rtrancl)
@@ -208,13 +208,13 @@
(** Conversions between trancl and rtrancl **)
lemma trancl_into_rtrancl: "\<langle>a,b\<rangle> \<in> r^+ \<Longrightarrow> \<langle>a,b\<rangle> \<in> r^*"
-apply (unfold trancl_def)
+ unfolding trancl_def
apply (blast intro: rtrancl_into_rtrancl)
done
(*r^+ contains all pairs in r *)
lemma r_into_trancl: "\<langle>a,b\<rangle> \<in> r \<Longrightarrow> \<langle>a,b\<rangle> \<in> r^+"
-apply (unfold trancl_def)
+ unfolding trancl_def
apply (blast intro!: rtrancl_refl)
done
@@ -266,7 +266,7 @@
done
lemma trancl_type: "r^+ \<subseteq> field(r)*field(r)"
-apply (unfold trancl_def)
+ unfolding trancl_def
apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
done
--- a/src/ZF/UNITY/AllocBase.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/AllocBase.thy Tue Sep 27 17:54:20 2022 +0100
@@ -118,7 +118,7 @@
done
lemma mono_tokens [iff]: "mono1(list(A), prefix(A), nat, Le,tokens)"
-apply (unfold mono1_def)
+ unfolding mono1_def
apply (auto intro: tokens_mono simp add: Le_def)
done
@@ -280,7 +280,7 @@
lemma all_distinct_Cons [simp]:
"all_distinct(Cons(a,l)) \<longleftrightarrow>
(a\<in>set_of_list(l) \<longrightarrow> False) \<and> (a \<notin> set_of_list(l) \<longrightarrow> all_distinct(l))"
-apply (unfold all_distinct_def)
+ unfolding all_distinct_def
apply (auto elim: list.cases)
done
@@ -336,14 +336,14 @@
lemma var_infinite_lemma:
"(\<lambda>x\<in>nat. nat_var_inj(x))\<in>inj(nat, var)"
-apply (unfold nat_var_inj_def)
+ unfolding nat_var_inj_def
apply (rule_tac d = var_inj in lam_injective)
apply (auto simp add: var.intros nat_list_inj_type)
apply (simp add: length_nat_list_inj)
done
lemma nat_lepoll_var: "nat \<lesssim> var"
-apply (unfold lepoll_def)
+ unfolding lepoll_def
apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
apply (rule var_infinite_lemma)
done
--- a/src/ZF/UNITY/AllocImpl.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy Tue Sep 27 17:54:20 2022 +0100
@@ -50,12 +50,12 @@
lemma available_tok_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`available_tok \<in> nat"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = available_tok in apply_type, auto)
done
lemma NbR_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`NbR \<in> nat"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = NbR in apply_type, auto)
done
@@ -270,7 +270,7 @@
{s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
\<longmapsto>w {x \<in> state. k \<le> length(x`rel)} \<inter>
(\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
-apply (unfold greater_than_def)
+ unfolding greater_than_def
apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
in LeadsTo_weaken_R)
apply safe
--- a/src/ZF/UNITY/ClientImpl.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Tue Sep 27 17:54:20 2022 +0100
@@ -56,29 +56,29 @@
(* This part should be automated *)
lemma ask_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`ask \<in> list(nat)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = ask in apply_type, auto)
done
lemma giv_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`giv \<in> list(nat)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = giv in apply_type, auto)
done
lemma rel_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`rel \<in> list(nat)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = rel in apply_type, auto)
done
lemma tok_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`tok \<in> nat"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = tok in apply_type, auto)
done
(** The Client Program **)
lemma client_type [simp,TC]: "client_prog \<in> program"
-apply (unfold client_prog_def)
+ unfolding client_prog_def
apply (simp (no_asm))
done
@@ -118,7 +118,7 @@
(*Safety property 1 \<in> ask, rel are increasing: (24) *)
lemma client_prog_Increasing_ask_rel:
"client_prog: program guarantees Incr(lift(ask)) \<inter> Incr(lift(rel))"
-apply (unfold guar_def)
+ unfolding guar_def
apply (auto intro!: increasing_imp_Increasing
simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
apply (safety, force, force)+
--- a/src/ZF/UNITY/Comp.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Comp.thy Tue Sep 27 17:54:20 2022 +0100
@@ -68,13 +68,13 @@
done
lemma component_SKIP [simp]: "F \<in> program \<Longrightarrow> SKIP component F"
-apply (unfold component_def)
+ unfolding component_def
apply (rule_tac x = F in exI)
apply (force intro: Join_SKIP_left)
done
lemma component_refl [simp]: "F \<in> program \<Longrightarrow> F component F"
-apply (unfold component_def)
+ unfolding component_def
apply (rule_tac x = F in exI)
apply (force intro: Join_SKIP_right)
done
@@ -88,7 +88,7 @@
by (unfold component_def, blast)
lemma component_Join2: "G component (F \<squnion> G)"
-apply (unfold component_def)
+ unfolding component_def
apply (simp (no_asm) add: Join_commute)
apply blast
done
@@ -111,12 +111,12 @@
done
lemma component_JOIN: "i \<in> I \<Longrightarrow> F(i) component (\<Squnion>i \<in> I. (F(i)))"
-apply (unfold component_def)
+ unfolding component_def
apply (blast intro: JOIN_absorb)
done
lemma component_trans: "\<lbrakk>F component G; G component H\<rbrakk> \<Longrightarrow> F component H"
-apply (unfold component_def)
+ unfolding component_def
apply (blast intro: Join_assoc [symmetric])
done
@@ -175,7 +175,7 @@
by (auto simp add: preserves_def INT_iff)
lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = <f(x), g(x)>"
-apply (unfold fun_pair_def)
+ unfolding fun_pair_def
apply (simp (no_asm))
done
@@ -252,7 +252,7 @@
(* component_of satisfies many of component's properties *)
lemma component_of_refl [simp]: "F \<in> program \<Longrightarrow> F component_of F"
-apply (unfold component_of_def)
+ unfolding component_of_def
apply (rule_tac x = SKIP in exI, auto)
done
@@ -263,7 +263,7 @@
lemma component_of_trans:
"\<lbrakk>F component_of G; G component_of H\<rbrakk> \<Longrightarrow> F component_of H"
-apply (unfold component_of_def)
+ unfolding component_of_def
apply (blast intro: Join_assoc [symmetric])
done
@@ -276,7 +276,7 @@
lemma localize_AllowedActs_eq [simp]:
"AllowedActs(localize(v,F)) = AllowedActs(F) \<inter> (\<Union>G \<in> preserves(v). Acts(G))"
-apply (unfold localize_def)
+ unfolding localize_def
apply (rule equalityI)
apply (auto dest: Acts_type [THEN subsetD])
done
--- a/src/ZF/UNITY/Constrains.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Constrains.thy Tue Sep 27 17:54:20 2022 +0100
@@ -66,7 +66,7 @@
done
lemma st_set_reachable: "st_set(reachable(F))"
-apply (unfold st_set_def)
+ unfolding st_set_def
apply (rule reachable_type)
done
declare st_set_reachable [iff]
@@ -129,7 +129,7 @@
(*Resembles the previous definition of Constrains*)
lemma Constrains_eq_constrains:
"A Co B = {F \<in> program. F:(reachable(F) \<inter> A) co (reachable(F) \<inter> B)}"
-apply (unfold Constrains_def)
+ unfolding Constrains_def
apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD]
intro: constrains_weaken)
done
@@ -137,7 +137,7 @@
lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection]
lemma constrains_imp_Constrains: "F \<in> A co A' \<Longrightarrow> F \<in> A Co A'"
-apply (unfold Constrains_def)
+ unfolding Constrains_def
apply (blast intro: constrains_weaken_L dest: constrainsD2)
done
@@ -160,26 +160,26 @@
declare Constrains_empty [iff]
lemma Constrains_state: "F \<in> A Co state \<longleftrightarrow> F \<in> program"
-apply (unfold Constrains_def)
+ unfolding Constrains_def
apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains)
done
declare Constrains_state [iff]
lemma Constrains_weaken_R:
"\<lbrakk>F \<in> A Co A'; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> A Co B'"
-apply (unfold Constrains_def2)
+ unfolding Constrains_def2
apply (blast intro: constrains_weaken_R)
done
lemma Constrains_weaken_L:
"\<lbrakk>F \<in> A Co A'; B<=A\<rbrakk> \<Longrightarrow> F \<in> B Co A'"
-apply (unfold Constrains_def2)
+ unfolding Constrains_def2
apply (blast intro: constrains_weaken_L st_set_subset)
done
lemma Constrains_weaken:
"\<lbrakk>F \<in> A Co A'; B<=A; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> B Co B'"
-apply (unfold Constrains_def2)
+ unfolding Constrains_def2
apply (blast intro: constrains_weaken st_set_subset)
done
@@ -202,7 +202,7 @@
lemma Constrains_Int:
"\<lbrakk>F \<in> A Co A'; F \<in> B Co B'\<rbrakk>\<Longrightarrow> F:(A \<inter> B) Co (A' \<inter> B')"
-apply (unfold Constrains_def)
+ unfolding Constrains_def
apply (subgoal_tac "reachable (F) \<inter> (A \<inter> B) = (reachable (F) \<inter> A) \<inter> (reachable (F) \<inter> B) ")
apply (auto intro: constrains_Int)
done
@@ -216,19 +216,19 @@
done
lemma Constrains_imp_subset: "F \<in> A Co A' \<Longrightarrow> reachable(F) \<inter> A \<subseteq> A'"
-apply (unfold Constrains_def)
+ unfolding Constrains_def
apply (blast dest: constrains_imp_subset)
done
lemma Constrains_trans:
"\<lbrakk>F \<in> A Co B; F \<in> B Co C\<rbrakk> \<Longrightarrow> F \<in> A Co C"
-apply (unfold Constrains_def2)
+ unfolding Constrains_def2
apply (blast intro: constrains_trans constrains_weaken)
done
lemma Constrains_cancel:
"\<lbrakk>F \<in> A Co (A' \<union> B); F \<in> B Co B'\<rbrakk> \<Longrightarrow> F \<in> A Co (A' \<union> B')"
-apply (unfold Constrains_def2)
+ unfolding Constrains_def2
apply (simp (no_asm_use) add: Int_Un_distrib)
apply (blast intro: constrains_cancel)
done
@@ -259,27 +259,27 @@
lemma Stable_Un:
"\<lbrakk>F \<in> Stable(A); F \<in> Stable(A')\<rbrakk> \<Longrightarrow> F \<in> Stable(A \<union> A')"
-apply (unfold Stable_def)
+ unfolding Stable_def
apply (blast intro: Constrains_Un)
done
lemma Stable_Int:
"\<lbrakk>F \<in> Stable(A); F \<in> Stable(A')\<rbrakk> \<Longrightarrow> F \<in> Stable (A \<inter> A')"
-apply (unfold Stable_def)
+ unfolding Stable_def
apply (blast intro: Constrains_Int)
done
lemma Stable_Constrains_Un:
"\<lbrakk>F \<in> Stable(C); F \<in> A Co (C \<union> A')\<rbrakk>
\<Longrightarrow> F \<in> (C \<union> A) Co (C \<union> A')"
-apply (unfold Stable_def)
+ unfolding Stable_def
apply (blast intro: Constrains_Un [THEN Constrains_weaken_R])
done
lemma Stable_Constrains_Int:
"\<lbrakk>F \<in> Stable(C); F \<in> (C \<inter> A) Co A'\<rbrakk>
\<Longrightarrow> F \<in> (C \<inter> A) Co (C \<inter> A')"
-apply (unfold Stable_def)
+ unfolding Stable_def
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
done
@@ -302,7 +302,7 @@
done
lemma Stable_type: "Stable(A) \<subseteq> program"
-apply (unfold Stable_def)
+ unfolding Stable_def
apply (rule Constrains_type)
done
@@ -329,7 +329,7 @@
(** Unless **)
lemma Unless_type: "A Unless B <=program"
-apply (unfold op_Unless_def)
+ unfolding op_Unless_def
apply (rule Constrains_type)
done
--- a/src/ZF/UNITY/Distributor.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Distributor.thy Tue Sep 27 17:54:20 2022 +0100
@@ -55,19 +55,19 @@
lemma (in distr) In_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`In \<in> list(A)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = In in apply_type, auto)
done
lemma (in distr) iIn_value_type [simp,TC]:
"s \<in> state \<Longrightarrow> s`iIn \<in> list(nat)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = iIn in apply_type, auto)
done
lemma (in distr) Out_value_type [simp,TC]:
"s \<in> state \<Longrightarrow> s`Out(n):list(A)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = "Out (n)" in apply_type)
apply auto
done
--- a/src/ZF/UNITY/FP.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/FP.thy Tue Sep 27 17:54:20 2022 +0100
@@ -24,7 +24,7 @@
by (unfold FP_Orig_def, blast)
lemma st_set_FP_Orig [iff]: "st_set(FP_Orig(F))"
-apply (unfold st_set_def)
+ unfolding st_set_def
apply (rule FP_Orig_type)
done
@@ -32,7 +32,7 @@
by (unfold FP_def, blast)
lemma st_set_FP [iff]: "st_set(FP(F))"
-apply (unfold st_set_def)
+ unfolding st_set_def
apply (rule FP_type)
done
--- a/src/ZF/UNITY/Follows.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Follows.thy Tue Sep 27 17:54:20 2022 +0100
@@ -165,7 +165,7 @@
(* Follows type *)
lemma Follows_type: "Follows(A, r, f, g)<=program"
-apply (unfold Follows_def)
+ unfolding Follows_def
apply (blast dest: Increasing_type [THEN subsetD])
done
@@ -175,7 +175,7 @@
lemma FollowsD:
"F \<in> Follows(A, r, f, g)\<Longrightarrow>
F \<in> program \<and> (\<exists>a. a \<in> A) \<and> (\<forall>x \<in> state. f(x):A \<and> g(x):A)"
-apply (unfold Follows_def)
+ unfolding Follows_def
apply (blast dest: IncreasingD)
done
@@ -406,7 +406,7 @@
lemma empty_le_MultLe [simp]:
"\<lbrakk>multiset(M); mset_of(M)<= A\<rbrakk> \<Longrightarrow> \<langle>0, M\<rangle> \<in> MultLe(A, r)"
-apply (unfold MultLe_def)
+ unfolding MultLe_def
apply (case_tac "M=0")
apply (auto simp add: FiniteFun.intros)
apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (A, r - id (A))")
@@ -420,7 +420,7 @@
lemma munion_mono:
"\<lbrakk>\<langle>M, N\<rangle> \<in> MultLe(A, r); \<langle>K, L\<rangle> \<in> MultLe(A, r)\<rbrakk> \<Longrightarrow>
<M +# K, N +# L> \<in> MultLe(A, r)"
-apply (unfold MultLe_def)
+ unfolding MultLe_def
apply (auto intro: munion_multirel_mono1 munion_multirel_mono2
munion_multirel_mono multiset_into_Mult simp add: Mult_iff_multiset)
done
--- a/src/ZF/UNITY/GenPrefix.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Tue Sep 27 17:54:20 2022 +0100
@@ -182,7 +182,7 @@
lemma prefix_gen_prefix_trans:
"\<lbrakk>\<langle>x,y\<rangle> \<in> prefix(A); \<langle>y, z\<rangle> \<in> gen_prefix(A, r); r<=A*A\<rbrakk>
\<Longrightarrow> \<langle>x, z\<rangle> \<in> gen_prefix(A, r)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (rule_tac P = "\<lambda>r. \<langle>x,z\<rangle> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst])
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
done
@@ -191,7 +191,7 @@
lemma gen_prefix_prefix_trans:
"\<lbrakk>\<langle>x,y\<rangle> \<in> gen_prefix(A,r); \<langle>y, z\<rangle> \<in> prefix(A); r<=A*A\<rbrakk>
\<Longrightarrow> \<langle>x, z\<rangle> \<in> gen_prefix(A, r)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (rule_tac P = "\<lambda>r. \<langle>x,z\<rangle> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst])
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
done
@@ -232,7 +232,7 @@
lemma same_gen_prefix_gen_prefix:
"\<lbrakk>refl(A, r); xs \<in> list(A)\<rbrakk> \<Longrightarrow>
<xs@ys, xs@zs>: gen_prefix(A, r) \<longleftrightarrow> \<langle>ys,zs\<rangle> \<in> gen_prefix(A, r)"
-apply (unfold refl_def)
+ unfolding refl_def
apply (induct_tac "xs")
apply (simp_all (no_asm_simp))
done
@@ -338,14 +338,14 @@
(** prefix is a partial order: **)
lemma refl_prefix: "refl(list(A), prefix(A))"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (rule refl_gen_prefix)
apply (auto simp add: refl_def)
done
declare refl_prefix [THEN reflD, simp]
lemma trans_prefix: "trans(prefix(A))"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (rule trans_gen_prefix)
apply (auto simp add: trans_def)
done
@@ -353,7 +353,7 @@
lemmas prefix_trans = trans_prefix [THEN transD]
lemma trans_on_prefix: "trans[list(A)](prefix(A))"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (rule trans_on_gen_prefix)
apply (auto simp add: trans_def)
done
@@ -365,7 +365,7 @@
lemma set_of_list_prefix_mono:
"\<langle>xs,ys\<rangle> \<in> prefix(A) \<Longrightarrow> set_of_list(xs) \<subseteq> set_of_list(ys)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (erule gen_prefix.induct)
apply (subgoal_tac [3] "xs \<in> list (A) \<and>ys \<in> list (A) ")
prefer 4 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
@@ -376,7 +376,7 @@
lemma Nil_prefix: "xs \<in> list(A) \<Longrightarrow> <[],xs> \<in> prefix(A)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (simp (no_asm_simp) add: Nil_gen_prefix)
done
declare Nil_prefix [simp]
@@ -399,7 +399,7 @@
lemma same_prefix_prefix:
"xs \<in> list(A)\<Longrightarrow> <xs@ys,xs@zs> \<in> prefix(A) \<longleftrightarrow> (\<langle>ys,zs\<rangle> \<in> prefix(A))"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (subgoal_tac "refl (A,id (A))")
apply (simp (no_asm_simp))
apply (auto simp add: refl_def)
@@ -414,7 +414,7 @@
lemma prefix_appendI:
"\<lbrakk>\<langle>xs,ys\<rangle> \<in> prefix(A); zs \<in> list(A)\<rbrakk> \<Longrightarrow> <xs,ys@zs> \<in> prefix(A)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (erule gen_prefix.append, assumption)
done
declare prefix_appendI [simp]
@@ -423,14 +423,14 @@
"\<lbrakk>xs \<in> list(A); ys \<in> list(A); y \<in> A\<rbrakk> \<Longrightarrow>
<xs,Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow>
(xs=[] | (\<exists>zs. xs=Cons(y,zs) \<and> \<langle>zs,ys\<rangle> \<in> prefix(A)))"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (auto simp add: gen_prefix_Cons)
done
lemma append_one_prefix:
"\<lbrakk>\<langle>xs,ys\<rangle> \<in> prefix(A); length(xs) < length(ys)\<rbrakk>
\<Longrightarrow> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (subgoal_tac "refl (A, id (A))")
apply (simp (no_asm_simp) add: append_one_gen_prefix)
apply (auto simp add: refl_def)
@@ -438,24 +438,24 @@
lemma prefix_length_le:
"\<langle>xs,ys\<rangle> \<in> prefix(A) \<Longrightarrow> length(xs) \<le> length(ys)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (blast dest: gen_prefix_length_le)
done
lemma prefix_type: "prefix(A)<=list(A)*list(A)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (blast intro!: gen_prefix.dom_subset)
done
lemma strict_prefix_type:
"strict_prefix(A) \<subseteq> list(A)*list(A)"
-apply (unfold strict_prefix_def)
+ unfolding strict_prefix_def
apply (blast intro!: prefix_type [THEN subsetD])
done
lemma strict_prefix_length_lt_aux:
"\<langle>xs,ys\<rangle> \<in> prefix(A) \<Longrightarrow> xs\<noteq>ys \<longrightarrow> length(xs) < length(ys)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (erule gen_prefix.induct, clarify)
apply (subgoal_tac [!] "ys \<in> list(A) \<and> xs \<in> list(A)")
apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
@@ -468,7 +468,7 @@
lemma strict_prefix_length_lt:
"\<langle>xs,ys\<rangle>:strict_prefix(A) \<Longrightarrow> length(xs) < length(ys)"
-apply (unfold strict_prefix_def)
+ unfolding strict_prefix_def
apply (rule strict_prefix_length_lt_aux [THEN mp])
apply (auto dest: prefix_type [THEN subsetD])
done
@@ -476,7 +476,7 @@
(*Equivalence to the definition used in Lex/Prefix.thy*)
lemma prefix_iff:
"\<langle>xs,zs\<rangle> \<in> prefix(A) \<longleftrightarrow> (\<exists>ys \<in> list(A). zs = xs@ys) \<and> xs \<in> list(A)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app)
apply (subgoal_tac "drop (length (xs), zs) \<in> list (A) ")
apply (rule_tac x = "drop (length (xs), zs) " in bexI)
@@ -544,7 +544,7 @@
declare refl_Le [simp]
lemma antisym_Le: "antisym(Le)"
-apply (unfold antisym_def)
+ unfolding antisym_def
apply (auto intro: le_anti_sym)
done
declare antisym_Le [simp]
@@ -579,7 +579,7 @@
lemma prefix_imp_pfixLe:
"\<langle>xs,ys\<rangle>:prefix(nat)\<Longrightarrow> xs pfixLe ys"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (rule gen_prefix_mono [THEN subsetD], auto)
done
@@ -619,7 +619,7 @@
lemma prefix_imp_take:
"\<langle>xs, ys\<rangle> \<in> prefix(A) \<Longrightarrow> xs = take(length(xs), ys)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (erule gen_prefix.induct)
apply (subgoal_tac [3] "length (xs) :nat")
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: length_type)
@@ -641,7 +641,7 @@
by (blast intro: prefix_length_equal le_anti_sym prefix_length_le)
lemma take_prefix [rule_format]: "xs \<in> list(A) \<Longrightarrow> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)"
-apply (unfold prefix_def)
+ unfolding prefix_def
apply (erule list.induct, simp, clarify)
apply (erule natE, auto)
done
--- a/src/ZF/UNITY/Guar.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Guar.thy Tue Sep 27 17:54:20 2022 +0100
@@ -95,7 +95,7 @@
lemma ex1 [rule_format]:
"GG \<in> Fin(program)
\<Longrightarrow> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (\<lambda>G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X"
-apply (unfold ex_prop_def)
+ unfolding ex_prop_def
apply (erule Fin_induct)
apply (simp_all add: OK_cons_iff)
apply (safe elim!: not_emptyE, auto)
@@ -132,14 +132,14 @@
(*** universal properties ***)
lemma uv_imp_subset_program: "uv_prop(X)\<Longrightarrow> X\<subseteq>program"
-apply (unfold uv_prop_def)
+ unfolding uv_prop_def
apply (simp (no_asm_simp))
done
lemma uv1 [rule_format]:
"GG \<in> Fin(program) \<Longrightarrow>
(uv_prop(X)\<longrightarrow> GG \<subseteq> X \<and> OK(GG, (\<lambda>G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
-apply (unfold uv_prop_def)
+ unfolding uv_prop_def
apply (erule Fin_induct)
apply (auto simp add: OK_cons_iff)
done
@@ -216,7 +216,7 @@
done
lemma guarantees_imp: "(Y = program guarantees Y) \<Longrightarrow> ex_prop(Y)"
-apply (unfold guar_def)
+ unfolding guar_def
apply (simp (no_asm_simp) add: ex_prop_equiv)
apply safe
apply (blast intro: elim: equalityE)
@@ -231,7 +231,7 @@
lemma guarantees_UN_left:
"i \<in> I \<Longrightarrow>(\<Union>i \<in> I. X(i)) guarantees Y = (\<Inter>i \<in> I. X(i) guarantees Y)"
-apply (unfold guar_def)
+ unfolding guar_def
apply (rule equalityI, safe)
prefer 2 apply force
apply blast+
@@ -239,13 +239,13 @@
lemma guarantees_Un_left:
"(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
-apply (unfold guar_def)
+ unfolding guar_def
apply (rule equalityI, safe, blast+)
done
lemma guarantees_INT_right:
"i \<in> I \<Longrightarrow> X guarantees (\<Inter>i \<in> I. Y(i)) = (\<Inter>i \<in> I. X guarantees Y(i))"
-apply (unfold guar_def)
+ unfolding guar_def
apply (rule equalityI, safe, blast+)
done
@@ -307,7 +307,7 @@
"\<lbrakk>F \<in> U guarantees V; G \<in> X guarantees Y; F ok G\<rbrakk>
\<Longrightarrow> F \<squnion> G: (U \<inter> X) guarantees (V \<inter> Y)"
-apply (unfold guar_def)
+ unfolding guar_def
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
@@ -319,7 +319,7 @@
lemma guarantees_Join_Un:
"\<lbrakk>F \<in> U guarantees V; G \<in> X guarantees Y; F ok G\<rbrakk>
\<Longrightarrow> F \<squnion> G: (U \<union> X) guarantees (V \<union> Y)"
-apply (unfold guar_def)
+ unfolding guar_def
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
@@ -480,7 +480,7 @@
lemma wx_equiv:
"wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<squnion> G) \<in> X}"
-apply (unfold wx_def)
+ unfolding wx_def
apply (rule equalityI, safe, blast)
apply (simp (no_asm_use) add: ex_prop_def)
apply blast
--- a/src/ZF/UNITY/Increasing.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Increasing.thy Tue Sep 27 17:54:20 2022 +0100
@@ -41,7 +41,7 @@
lemma increasingD:
"F \<in> increasing[A](r,f) \<Longrightarrow> F \<in> program \<and> (\<exists>a. a \<in> A) \<and> (\<forall>s \<in> state. f(s):A)"
-apply (unfold increasing_def)
+ unfolding increasing_def
apply (subgoal_tac "\<exists>x. x \<in> state")
apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
done
@@ -110,7 +110,7 @@
lemma IncreasingD:
"F \<in> Increasing[A](r, f) \<Longrightarrow> F \<in> program \<and> (\<exists>a. a \<in> A) \<and> (\<forall>s \<in> state. f(s):A)"
-apply (unfold Increasing_def)
+ unfolding Increasing_def
apply (subgoal_tac "\<exists>x. x \<in> state")
apply (auto intro: st0_in_state)
done
--- a/src/ZF/UNITY/Merge.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Merge.thy Tue Sep 27 17:54:20 2022 +0100
@@ -85,18 +85,18 @@
lemma (in merge) In_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`In(n) \<in> list(A)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = "In (n)" in apply_type)
apply auto
done
lemma (in merge) Out_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`Out \<in> list(A)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = Out in apply_type, auto)
done
lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`iOut \<in> list(nat)"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = iOut in apply_type, auto)
done
--- a/src/ZF/UNITY/Monotonicity.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy Tue Sep 27 17:54:20 2022 +0100
@@ -95,7 +95,7 @@
lemma mono_length [iff]:
"mono1(list(A), prefix(A), nat, Le, length)"
-apply (unfold mono1_def)
+ unfolding mono1_def
apply (auto dest: prefix_length_le simp add: Le_def)
done
--- a/src/ZF/UNITY/Mutex.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Mutex.thy Tue Sep 27 17:54:20 2022 +0100
@@ -94,27 +94,27 @@
declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp]
lemma u_value_type: "s \<in> state \<Longrightarrow>s`u \<in> bool"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = u in apply_type, auto)
done
lemma v_value_type: "s \<in> state \<Longrightarrow> s`v \<in> bool"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = v in apply_type, auto)
done
lemma p_value_type: "s \<in> state \<Longrightarrow> s`p \<in> bool"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = p in apply_type, auto)
done
lemma m_value_type: "s \<in> state \<Longrightarrow> s`m \<in> int"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = m in apply_type, auto)
done
lemma n_value_type: "s \<in> state \<Longrightarrow>s`n \<in> int"
-apply (unfold state_def)
+ unfolding state_def
apply (drule_tac a = n in apply_type, auto)
done
@@ -216,7 +216,7 @@
lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} \<longmapsto>w {s \<in> state. s`p=1}"
apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
- apply (unfold Mutex_def)
+ unfolding Mutex_def
apply (ensures U3)
apply (ensures U4)
done
@@ -267,7 +267,7 @@
lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} \<longmapsto>w {s \<in> state. s`p=0}"
apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
- apply (unfold Mutex_def)
+ unfolding Mutex_def
apply (ensures V3)
apply (ensures V4)
done
--- a/src/ZF/UNITY/SubstAx.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Tue Sep 27 17:54:20 2022 +0100
@@ -26,7 +26,7 @@
(* Equivalence with the HOL-like definition *)
lemma LeadsTo_eq:
"st_set(B)\<Longrightarrow> A \<longmapsto>w B = {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> B}"
-apply (unfold LeadsTo_def)
+ unfolding LeadsTo_def
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
done
@@ -40,7 +40,7 @@
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
lemma Always_LeadsTo_post: "F \<in> Always(I) \<Longrightarrow> (F \<in> A \<longmapsto>w (I \<inter> A')) \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
-apply (unfold LeadsTo_def)
+ unfolding LeadsTo_def
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
done
@@ -123,12 +123,12 @@
declare LeadsTo_state [iff]
lemma LeadsTo_weaken_R: "\<lbrakk>F \<in> A \<longmapsto>w A'; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w B'"
-apply (unfold LeadsTo_def)
+ unfolding LeadsTo_def
apply (auto intro: leadsTo_weaken_R)
done
lemma LeadsTo_weaken_L: "\<lbrakk>F \<in> A \<longmapsto>w A'; B \<subseteq> A\<rbrakk> \<Longrightarrow> F \<in> B \<longmapsto>w A'"
-apply (unfold LeadsTo_def)
+ unfolding LeadsTo_def
apply (auto intro: leadsTo_weaken_L)
done
@@ -256,7 +256,7 @@
lemma PSP_Unless:
"\<lbrakk>F \<in> A \<longmapsto>w A'; F \<in> B Unless B'\<rbrakk>\<Longrightarrow> F:(A \<inter> B) \<longmapsto>w ((A' \<inter> B) \<union> B')"
-apply (unfold op_Unless_def)
+ unfolding op_Unless_def
apply (drule PSP, assumption)
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
done
@@ -327,7 +327,7 @@
"\<lbrakk>F \<in> A \<longmapsto>w A'; F \<in> Stable(A');
F \<in> B \<longmapsto>w B'; F \<in> Stable(B')\<rbrakk>
\<Longrightarrow> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')"
-apply (unfold Stable_def)
+ unfolding Stable_def
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
prefer 5
apply blast
@@ -339,7 +339,7 @@
(\<And>i. i \<in> I \<Longrightarrow> F \<in> A(i) \<longmapsto>w A'(i));
(\<And>i. i \<in> I \<Longrightarrow>F \<in> Stable(A'(i))); F \<in> program\<rbrakk>
\<Longrightarrow> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))"
-apply (unfold Stable_def)
+ unfolding Stable_def
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
apply (rule_tac [3] subset_refl, auto)
done
--- a/src/ZF/UNITY/UNITY.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/UNITY.thy Tue Sep 27 17:54:20 2022 +0100
@@ -165,7 +165,7 @@
lemmas InitD = Init_type [THEN subsetD]
lemma st_set_Init [iff]: "st_set(Init(F))"
-apply (unfold st_set_def)
+ unfolding st_set_def
apply (rule Init_type)
done
@@ -469,7 +469,7 @@
by (force simp add: unless_def constrains_def)
lemma unlessI: "\<lbrakk>F \<in> (A-B) co (A \<union> B)\<rbrakk> \<Longrightarrow> F \<in> A unless B"
-apply (unfold unless_def)
+ unfolding unless_def
apply (blast dest: constrainsD2)
done
@@ -515,34 +515,34 @@
lemma stable_Un:
"\<lbrakk>F \<in> stable(A); F \<in> stable(A')\<rbrakk> \<Longrightarrow> F \<in> stable(A \<union> A')"
-apply (unfold stable_def)
+ unfolding stable_def
apply (blast intro: constrains_Un)
done
lemma stable_UN:
"\<lbrakk>\<And>i. i\<in>I \<Longrightarrow> F \<in> stable(A(i)); F \<in> program\<rbrakk>
\<Longrightarrow> F \<in> stable (\<Union>i \<in> I. A(i))"
-apply (unfold stable_def)
+ unfolding stable_def
apply (blast intro: constrains_UN)
done
lemma stable_Int:
"\<lbrakk>F \<in> stable(A); F \<in> stable(A')\<rbrakk> \<Longrightarrow> F \<in> stable (A \<inter> A')"
-apply (unfold stable_def)
+ unfolding stable_def
apply (blast intro: constrains_Int)
done
lemma stable_INT:
"\<lbrakk>\<And>i. i \<in> I \<Longrightarrow> F \<in> stable(A(i)); F \<in> program\<rbrakk>
\<Longrightarrow> F \<in> stable (\<Inter>i \<in> I. A(i))"
-apply (unfold stable_def)
+ unfolding stable_def
apply (blast intro: constrains_INT)
done
lemma stable_All:
"\<lbrakk>\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program\<rbrakk>
\<Longrightarrow> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})"
-apply (unfold stable_def)
+ unfolding stable_def
apply (rule constrains_All, auto)
done
@@ -562,7 +562,7 @@
subsection\<open>The Operator \<^term>\<open>invariant\<close>\<close>
lemma invariant_type: "invariant(A) \<subseteq> program"
-apply (unfold invariant_def)
+ unfolding invariant_def
apply (blast dest: stable_type [THEN subsetD])
done
@@ -575,7 +575,7 @@
by (unfold invariant_def initially_def, auto)
lemma invariantD2: "F \<in> invariant(A) \<Longrightarrow> F \<in> program \<and> st_set(A)"
-apply (unfold invariant_def)
+ unfolding invariant_def
apply (blast dest: stableD2)
done
--- a/src/ZF/UNITY/Union.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Union.thy Tue Sep 27 17:54:20 2022 +0100
@@ -159,7 +159,7 @@
lemma Acts_JOIN [simp]:
"Acts(JOIN(I,F)) = cons(id(state), \<Union>i \<in> I. Acts(F(i)))"
-apply (unfold JOIN_def)
+ unfolding JOIN_def
apply (auto simp del: INT_simps UN_simps)
apply (rule equalityI)
apply (auto dest: Acts_type [THEN subsetD])
@@ -325,7 +325,7 @@
"i \<in> I \<Longrightarrow>
(\<Squnion>i \<in> I. F(i)) \<in> transient(A) \<longleftrightarrow> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))"
apply (auto simp add: transient_def JOIN_def)
-apply (unfold st_set_def)
+ unfolding st_set_def
apply (drule_tac [2] x = act in bspec)
apply (auto dest: Acts_type [THEN subsetD])
done
@@ -357,7 +357,7 @@
(programify(F) \<in> (A-B) co (A \<union> B) \<and> programify(G) \<in> (A-B) co (A \<union> B) \<and>
(programify(F) \<in> transient (A-B) | programify(G) \<in> transient (A-B)))"
-apply (unfold ensures_def)
+ unfolding ensures_def
apply (auto simp add: Join_transient)
done
@@ -567,7 +567,7 @@
lemma def_UNION_ok_iff:
"\<lbrakk>F \<equiv> mk_program(init,acts, \<Union>G \<in> X. Acts(G)); safety_prop(X)\<rbrakk>
\<Longrightarrow> F ok G \<longleftrightarrow> (programify(G) \<in> X \<and> acts \<inter> Pow(state*state) \<subseteq> AllowedActs(G))"
-apply (unfold ok_def)
+ unfolding ok_def
apply (drule_tac G = G in safety_prop_Acts_iff)
apply (cut_tac F = G in AllowedActs_type)
apply (cut_tac F = G in Acts_type, auto)
--- a/src/ZF/UNITY/WFair.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/WFair.thy Tue Sep 27 17:54:20 2022 +0100
@@ -116,7 +116,7 @@
lemma ensuresI:
"\<lbrakk>F:(A-B) co (A \<union> B); F \<in> transient(A-B)\<rbrakk>\<Longrightarrow>F \<in> A ensures B"
-apply (unfold ensures_def)
+ unfolding ensures_def
apply (auto simp add: transient_type [THEN subsetD])
done
@@ -131,7 +131,7 @@
by (unfold ensures_def, auto)
lemma ensures_weaken_R: "\<lbrakk>F \<in> A ensures A'; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> A ensures B'"
-apply (unfold ensures_def)
+ unfolding ensures_def
apply (blast intro: transient_strengthen constrains_weaken)
done
@@ -139,7 +139,7 @@
lemma stable_ensures_Int:
"\<lbrakk>F \<in> stable(C); F \<in> A ensures B\<rbrakk> \<Longrightarrow> F:(C \<inter> A) ensures (C \<inter> B)"
-apply (unfold ensures_def)
+ unfolding ensures_def
apply (simp (no_asm) add: Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
apply (blast intro: transient_strengthen stable_constrains_Int constrains_weaken)
done
@@ -182,13 +182,13 @@
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
lemma leadsTo_Trans: "\<lbrakk>F \<in> A \<longmapsto> B; F \<in> B \<longmapsto> C\<rbrakk>\<Longrightarrow>F \<in> A \<longmapsto> C"
-apply (unfold leadsTo_def)
+ unfolding leadsTo_def
apply (auto intro: leads.Trans)
done
(* Better when used in association with leadsTo_weaken_R *)
lemma transient_imp_leadsTo: "F \<in> transient(A) \<Longrightarrow> F \<in> A \<longmapsto> (state-A)"
-apply (unfold transient_def)
+ unfolding transient_def
apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI)
done
@@ -424,7 +424,7 @@
lemma psp_stable:
"\<lbrakk>F \<in> A \<longmapsto> A'; F \<in> stable(B)\<rbrakk> \<Longrightarrow> F:(A \<inter> B) \<longmapsto> (A' \<inter> B)"
-apply (unfold stable_def)
+ unfolding stable_def
apply (frule leadsToD2)
apply (erule leadsTo_induct)
prefer 3 apply (blast intro: leadsTo_Union_Int)
@@ -470,7 +470,7 @@
lemma psp_unless:
"\<lbrakk>F \<in> A \<longmapsto> A'; F \<in> B unless B'; st_set(B); st_set(B')\<rbrakk>
\<Longrightarrow> F \<in> (A \<inter> B) \<longmapsto> ((A' \<inter> B) \<union> B')"
-apply (unfold unless_def)
+ unfolding unless_def
apply (subgoal_tac "st_set (A) \<and>st_set (A') ")
prefer 2 apply (blast dest: leadsToD2)
apply (drule psp, assumption, blast)
@@ -511,7 +511,7 @@
done
lemma nat_measure_field: "field(measure(nat, \<lambda>x. x)) = nat"
-apply (unfold field_def)
+ unfolding field_def
apply (simp add: measure_def)
apply (rule equalityI, force, clarify)
apply (erule_tac V = "x\<notin>range (y)" for y in thin_rl)
@@ -551,13 +551,13 @@
by (unfold wlt_def, auto)
lemma wlt_st_set: "st_set(wlt(F, B))"
-apply (unfold st_set_def)
+ unfolding st_set_def
apply (rule wlt_type)
done
declare wlt_st_set [iff]
lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) \<longmapsto> B \<longleftrightarrow> (F \<in> program \<and> st_set(B))"
-apply (unfold wlt_def)
+ unfolding wlt_def
apply (blast dest: leadsToD2 intro!: leadsTo_Union)
done
@@ -565,7 +565,7 @@
lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]
lemma leadsTo_subset: "F \<in> A \<longmapsto> B \<Longrightarrow> A \<subseteq> wlt(F, B)"
-apply (unfold wlt_def)
+ unfolding wlt_def
apply (frule leadsToD2)
apply (auto simp add: st_set_def)
done
@@ -687,7 +687,7 @@
"\<lbrakk>F \<in> A \<longmapsto> A'; F \<in> stable(A');
F \<in> B \<longmapsto> B'; F \<in> stable(B')\<rbrakk>
\<Longrightarrow> F \<in> (A \<inter> B) \<longmapsto> (A' \<inter> B')"
-apply (unfold stable_def)
+ unfolding stable_def
apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)
apply (blast dest: leadsToD2)
done
@@ -698,7 +698,7 @@
(\<And>i. i \<in> I \<Longrightarrow> F \<in> A(i) \<longmapsto> A'(i));
(\<And>i. i \<in> I \<Longrightarrow> F \<in> stable(A'(i))); F \<in> program\<rbrakk>
\<Longrightarrow> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> (\<Inter>i \<in> I. A'(i))"
-apply (unfold stable_def)
+ unfolding stable_def
apply (subgoal_tac "st_set (\<Inter>i \<in> I. A' (i))")
prefer 2 apply (blast dest: leadsToD2)
apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto)
--- a/src/ZF/Univ.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Univ.thy Tue Sep 27 17:54:20 2022 +0100
@@ -125,7 +125,7 @@
lemma Pair_in_Vfrom:
"\<lbrakk>a \<in> Vfrom(A,i); b \<in> Vfrom(A,i)\<rbrakk> \<Longrightarrow> \<langle>a,b\<rangle> \<in> Vfrom(A,succ(succ(i)))"
-apply (unfold Pair_def)
+ unfolding Pair_def
apply (blast intro: doubleton_in_Vfrom)
done
@@ -249,13 +249,13 @@
lemma Inl_in_VLimit:
"\<lbrakk>a \<in> Vfrom(A,i); Limit(i)\<rbrakk> \<Longrightarrow> Inl(a) \<in> Vfrom(A,i)"
-apply (unfold Inl_def)
+ unfolding Inl_def
apply (blast intro: zero_in_VLimit Pair_in_VLimit)
done
lemma Inr_in_VLimit:
"\<lbrakk>b \<in> Vfrom(A,i); Limit(i)\<rbrakk> \<Longrightarrow> Inr(b) \<in> Vfrom(A,i)"
-apply (unfold Inr_def)
+ unfolding Inr_def
apply (blast intro: one_in_VLimit Pair_in_VLimit)
done
@@ -336,7 +336,7 @@
\<Longrightarrow> a*b \<in> Vfrom(A, succ(succ(succ(j))))"
apply (drule Transset_Vfrom)
apply (rule subset_mem_Vfrom)
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (blast intro: Pair_in_Vfrom)
done
@@ -352,10 +352,10 @@
lemma sum_in_Vfrom:
"\<lbrakk>a \<in> Vfrom(A,j); b \<in> Vfrom(A,j); Transset(A); 1:j\<rbrakk>
\<Longrightarrow> a+b \<in> Vfrom(A, succ(succ(succ(j))))"
-apply (unfold sum_def)
+ unfolding sum_def
apply (drule Transset_Vfrom)
apply (rule subset_mem_Vfrom)
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD])
done
@@ -371,7 +371,7 @@
lemma fun_in_Vfrom:
"\<lbrakk>a \<in> Vfrom(A,j); b \<in> Vfrom(A,j); Transset(A)\<rbrakk> \<Longrightarrow>
a->b \<in> Vfrom(A, succ(succ(succ(succ(j)))))"
-apply (unfold Pi_def)
+ unfolding Pi_def
apply (drule Transset_Vfrom)
apply (rule subset_mem_Vfrom)
apply (rule Collect_subset [THEN subset_trans])
@@ -380,7 +380,7 @@
apply (rule_tac [3] Un_upper2)
apply (rule_tac [2] succI1 [THEN UN_upper])
apply (rule Pow_mono)
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (blast intro: Pair_in_Vfrom)
done
@@ -395,7 +395,7 @@
"\<lbrakk>a \<in> Vfrom(A,j); Transset(A)\<rbrakk> \<Longrightarrow> Pow(a) \<in> Vfrom(A, succ(succ(j)))"
apply (drule Transset_Vfrom)
apply (rule subset_mem_Vfrom)
-apply (unfold Transset_def)
+ unfolding Transset_def
apply (subst Vfrom, blast)
done
@@ -476,12 +476,12 @@
subsubsection\<open>Set Up an Environment for Simplification\<close>
lemma rank_Inl: "rank(a) < rank(Inl(a))"
-apply (unfold Inl_def)
+ unfolding Inl_def
apply (rule rank_pair2)
done
lemma rank_Inr: "rank(a) < rank(Inr(a))"
-apply (unfold Inr_def)
+ unfolding Inr_def
apply (rule rank_pair2)
done
@@ -491,7 +491,7 @@
text\<open>NOT SUITABLE FOR REWRITING: recursive!\<close>
lemma Vrec: "Vrec(a,H) = H(a, \<lambda>x\<in>Vset(rank(a)). Vrec(x,H))"
-apply (unfold Vrec_def)
+ unfolding Vrec_def
apply (subst transrec, simp)
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
done
@@ -507,7 +507,7 @@
text\<open>NOT SUITABLE FOR REWRITING: recursive!\<close>
lemma Vrecursor:
"Vrecursor(H,a) = H(\<lambda>x\<in>Vset(rank(a)). Vrecursor(H,x), a)"
-apply (unfold Vrecursor_def)
+ unfolding Vrecursor_def
apply (subst transrec, simp)
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
done
@@ -523,20 +523,20 @@
subsection\<open>The Datatype Universe: \<^term>\<open>univ(A)\<close>\<close>
lemma univ_mono: "A<=B \<Longrightarrow> univ(A) \<subseteq> univ(B)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (erule Vfrom_mono)
apply (rule subset_refl)
done
lemma Transset_univ: "Transset(A) \<Longrightarrow> Transset(univ(A))"
-apply (unfold univ_def)
+ unfolding univ_def
apply (erule Transset_Vfrom)
done
subsubsection\<open>The Set \<^term>\<open>univ(A)\<close> as a Limit\<close>
lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule Limit_nat [THEN Limit_Vfrom_eq])
done
@@ -567,7 +567,7 @@
subsection\<open>Closure Properties for \<^term>\<open>univ(A)\<close>\<close>
lemma zero_in_univ: "0 \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule nat_0I [THEN zero_in_Vfrom])
done
@@ -575,7 +575,7 @@
by (blast intro: zero_in_univ)
lemma A_subset_univ: "A \<subseteq> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule A_subset_Vfrom)
done
@@ -584,30 +584,30 @@
subsubsection\<open>Closure under Unordered and Ordered Pairs\<close>
lemma singleton_in_univ: "a: univ(A) \<Longrightarrow> {a} \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (blast intro: singleton_in_VLimit Limit_nat)
done
lemma doubleton_in_univ:
"\<lbrakk>a: univ(A); b: univ(A)\<rbrakk> \<Longrightarrow> {a,b} \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (blast intro: doubleton_in_VLimit Limit_nat)
done
lemma Pair_in_univ:
"\<lbrakk>a: univ(A); b: univ(A)\<rbrakk> \<Longrightarrow> \<langle>a,b\<rangle> \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (blast intro: Pair_in_VLimit Limit_nat)
done
lemma Union_in_univ:
"\<lbrakk>X: univ(A); Transset(A)\<rbrakk> \<Longrightarrow> \<Union>(X) \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (blast intro: Union_in_VLimit Limit_nat)
done
lemma product_univ: "univ(A)*univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule Limit_nat [THEN product_VLimit])
done
@@ -615,7 +615,7 @@
subsubsection\<open>The Natural Numbers\<close>
lemma nat_subset_univ: "nat \<subseteq> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule i_subset_Vfrom)
done
@@ -625,7 +625,7 @@
subsubsection\<open>Instances for 1 and 2\<close>
lemma one_in_univ: "1 \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule Limit_nat [THEN one_in_VLimit])
done
@@ -634,7 +634,7 @@
by (blast intro: nat_into_univ)
lemma bool_subset_univ: "bool \<subseteq> univ(A)"
-apply (unfold bool_def)
+ unfolding bool_def
apply (blast intro!: zero_in_univ one_in_univ)
done
@@ -644,17 +644,17 @@
subsubsection\<open>Closure under Disjoint Union\<close>
lemma Inl_in_univ: "a: univ(A) \<Longrightarrow> Inl(a) \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (erule Inl_in_VLimit [OF _ Limit_nat])
done
lemma Inr_in_univ: "b: univ(A) \<Longrightarrow> Inr(b) \<in> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (erule Inr_in_VLimit [OF _ Limit_nat])
done
lemma sum_univ: "univ(C)+univ(C) \<subseteq> univ(C)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule Limit_nat [THEN sum_VLimit])
done
@@ -694,7 +694,7 @@
lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit]
lemma Fin_univ: "Fin(univ(A)) \<subseteq> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule Limit_nat [THEN Fin_VLimit])
done
@@ -710,7 +710,7 @@
lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit]
lemma nat_fun_univ: "n: nat \<Longrightarrow> n -> univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (erule nat_fun_VLimit [OF _ Limit_nat])
done
@@ -726,7 +726,7 @@
done
lemma FiniteFun_univ1: "univ(A) -||> univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (rule Limit_nat [THEN FiniteFun_VLimit1])
done
@@ -740,7 +740,7 @@
lemma FiniteFun_univ:
"W \<subseteq> univ(A) \<Longrightarrow> W -||> univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+ unfolding univ_def
apply (erule FiniteFun_VLimit [OF _ Limit_nat])
done
@@ -777,7 +777,7 @@
lemma Pair_in_Vfrom_D:
"\<lbrakk>\<langle>a,b\<rangle> \<in> Vfrom(X,succ(i)); Transset(X)\<rbrakk>
\<Longrightarrow> a \<in> Vfrom(X,i) \<and> b \<in> Vfrom(X,i)"
-apply (unfold Pair_def)
+ unfolding Pair_def
apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D)
done
--- a/src/ZF/WF.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/WF.thy Tue Sep 27 17:54:20 2022 +0100
@@ -109,7 +109,7 @@
"\<lbrakk>wf(r);
\<And>x.\<lbrakk>\<forall>y. \<langle>y,x\<rangle>: r \<longrightarrow> P(y)\<rbrakk> \<Longrightarrow> P(x)\<rbrakk>
\<Longrightarrow> P(a)"
-apply (unfold wf_def)
+ unfolding wf_def
apply (erule_tac x = "{z \<in> domain(r). \<not> P(z)}" in allE)
apply blast
done
@@ -132,7 +132,7 @@
"\<lbrakk>wf[A](r); a \<in> A;
\<And>x.\<lbrakk>x \<in> A; \<forall>y\<in>A. \<langle>y,x\<rangle>: r \<longrightarrow> P(y)\<rbrakk> \<Longrightarrow> P(x)
\<rbrakk> \<Longrightarrow> P(a)"
-apply (unfold wf_on_def)
+ unfolding wf_on_def
apply (erule wf_induct2, assumption)
apply (rule field_Int_square, blast)
done
@@ -220,7 +220,7 @@
subsection\<open>The Predicate \<^term>\<open>is_recfun\<close>\<close>
lemma is_recfun_type: "is_recfun(r,a,H,f) \<Longrightarrow> f \<in> r-``{a} -> range(f)"
-apply (unfold is_recfun_def)
+ unfolding is_recfun_def
apply (erule ssubst)
apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
done
@@ -229,7 +229,7 @@
lemma apply_recfun:
"\<lbrakk>is_recfun(r,a,H,f); \<langle>x,a\<rangle>:r\<rbrakk> \<Longrightarrow> f`x = H(x, restrict(f,r-``{x}))"
-apply (unfold is_recfun_def)
+ unfolding is_recfun_def
txt\<open>replace f only on the left-hand side\<close>
apply (erule_tac P = "\<lambda>x. t(x) = u" for t u in ssubst)
apply (simp add: underI)
@@ -271,7 +271,7 @@
lemma the_recfun_eq:
"\<lbrakk>is_recfun(r,a,H,f); wf(r); trans(r)\<rbrakk> \<Longrightarrow> the_recfun(r,a,H) = f"
-apply (unfold the_recfun_def)
+ unfolding the_recfun_def
apply (blast intro: is_recfun_functional)
done
@@ -319,7 +319,7 @@
lemma wftrec:
"\<lbrakk>wf(r); trans(r)\<rbrakk> \<Longrightarrow>
wftrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wftrec(r,x,H))"
-apply (unfold wftrec_def)
+ unfolding wftrec_def
apply (subst unfold_the_recfun [unfolded is_recfun_def])
apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
done
@@ -330,7 +330,7 @@
(*NOT SUITABLE FOR REWRITING: it is recursive!*)
lemma wfrec:
"wf(r) \<Longrightarrow> wfrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wfrec(r,x,H))"
-apply (unfold wfrec_def)
+ unfolding wfrec_def
apply (erule wf_trancl [THEN wftrec, THEN ssubst])
apply (rule trans_trancl)
apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
--- a/src/ZF/ZF_Base.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ZF_Base.thy Tue Sep 27 17:54:20 2022 +0100
@@ -365,7 +365,7 @@
(*Rule in Modus Ponens style [was called subsetE] *)
lemma subsetD [elim]: "\<lbrakk>A \<subseteq> B; c\<in>A\<rbrakk> \<Longrightarrow> c\<in>B"
-apply (unfold subset_def)
+ unfolding subset_def
apply (erule bspec, assumption)
done
@@ -430,7 +430,7 @@
lemma Replace_iff:
"b \<in> {y. x\<in>A, P(x,y)} <-> (\<exists>x\<in>A. P(x,b) \<and> (\<forall>y. P(x,y) \<longrightarrow> y=b))"
-apply (unfold Replace_def)
+ unfolding Replace_def
apply (rule replacement [THEN iff_trans], blast+)
done
--- a/src/ZF/Zorn.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Zorn.thy Tue Sep 27 17:54:20 2022 +0100
@@ -70,7 +70,7 @@
subsection\<open>The Transfinite Construction\<close>
lemma increasingD1: "f \<in> increasing(A) \<Longrightarrow> f \<in> Pow(A)->Pow(A)"
-apply (unfold increasing_def)
+ unfolding increasing_def
apply (erule CollectD1)
done
@@ -182,17 +182,17 @@
text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close>
lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)"
-apply (unfold chain_def)
+ unfolding chain_def
apply (rule Collect_subset)
done
lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)"
-apply (unfold super_def)
+ unfolding super_def
apply (rule Collect_subset)
done
lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)"
-apply (unfold maxchain_def)
+ unfolding maxchain_def
apply (rule Collect_subset)
done
@@ -220,7 +220,7 @@
if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
in bexI)
apply force
-apply (unfold increasing_def)
+ unfolding increasing_def
apply (rule CollectI)
apply (rule lam_type)
apply (simp (no_asm_simp))
@@ -245,7 +245,7 @@
apply (erule TFin_induct)
apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
choice_super [THEN super_subset_chain [THEN subsetD]])
-apply (unfold chain_def)
+ unfolding chain_def
apply (rule CollectI, blast, safe)
apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
txt\<open>\<open>Blast_tac's\<close> slow\<close>
@@ -377,7 +377,7 @@
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
in bexI)
apply force
-apply (unfold increasing_def)
+ unfolding increasing_def
apply (rule CollectI)
apply (rule lam_type)
txt\<open>Type checking is surprisingly hard!\<close>
--- a/src/ZF/equalities.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/equalities.thy Tue Sep 27 17:54:20 2022 +0100
@@ -621,7 +621,7 @@
(** Range **)
lemma rangeI [intro]: "\<langle>a,b\<rangle>\<in> r \<Longrightarrow> b \<in> range(r)"
-apply (unfold range_def)
+ unfolding range_def
apply (erule converseI [THEN domainI])
done
@@ -629,7 +629,7 @@
by (unfold range_def, blast)
lemma range_subset: "range(A*B) \<subseteq> B"
-apply (unfold range_def)
+ unfolding range_def
apply (subst converse_prod)
apply (rule domain_subset)
done
@@ -682,12 +682,12 @@
by blast
lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
-apply (unfold field_def)
+ unfolding field_def
apply (rule Un_upper1)
done
lemma range_subset_field: "range(r) \<subseteq> field(r)"
-apply (unfold field_def)
+ unfolding field_def
apply (rule Un_upper2)
done
@@ -807,7 +807,7 @@
done
lemma vimage_subset: "r \<subseteq> A*B \<Longrightarrow> r-``C \<subseteq> A"
-apply (unfold vimage_def)
+ unfolding vimage_def
apply (erule converse_type [THEN image_subset])
done
--- a/src/ZF/ex/Commutation.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ex/Commutation.thy Tue Sep 27 17:54:20 2022 +0100
@@ -63,7 +63,7 @@
lemma commute_rtrancl:
"commute(r,s) \<Longrightarrow> field(r)=field(s) \<Longrightarrow> commute(r^*,s^*)"
-apply (unfold commute_def)
+ unfolding commute_def
apply (rule square_rtrancl)
apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
apply (simp_all add: rtrancl_field)
@@ -95,7 +95,7 @@
lemma confluent_Un:
"\<lbrakk>confluent(r); confluent(s); commute(r^*, s^*);
relation(r); relation(s)\<rbrakk> \<Longrightarrow> confluent(r \<union> s)"
-apply (unfold confluent_def)
+ unfolding confluent_def
apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
done
--- a/src/ZF/ex/Limit.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ex/Limit.thy Tue Sep 27 17:54:20 2022 +0100
@@ -470,7 +470,7 @@
lemma matrix_chain_left:
"\<lbrakk>matrix(D,M); n \<in> nat\<rbrakk> \<Longrightarrow> chain(D,M`n)"
-apply (unfold chain_def)
+ unfolding chain_def
apply (auto intro: matrix_fun [THEN apply_type] matrix_in matrix_rel_0_1)
done
--- a/src/ZF/ex/Ramsey.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ex/Ramsey.thy Tue Sep 27 17:54:20 2022 +0100
@@ -69,7 +69,7 @@
lemma Atleast_succD:
"Atleast(succ(m),A) \<Longrightarrow> \<exists>x \<in> A. Atleast(m, A-{x})"
-apply (unfold Atleast_def)
+ unfolding Atleast_def
apply (blast dest: inj_is_fun [THEN apply_type] inj_succ_restrict)
done
--- a/src/ZF/func.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/func.thy Tue Sep 27 17:54:20 2022 +0100
@@ -64,7 +64,7 @@
by (unfold apply_def function_def, blast)
lemma apply_equality: "\<lbrakk>\<langle>a,b\<rangle>: f; f \<in> Pi(A,B)\<rbrakk> \<Longrightarrow> f`a = b"
-apply (unfold Pi_def)
+ unfolding Pi_def
apply (blast intro: function_apply_equality)
done
@@ -132,7 +132,7 @@
subsection\<open>Lambda Abstraction\<close>
lemma lamI: "a \<in> A \<Longrightarrow> <a,b(a)> \<in> (\<lambda>x\<in>A. b(x))"
-apply (unfold lam_def)
+ unfolding lam_def
apply (erule RepFunI)
done
@@ -304,7 +304,7 @@
by (unfold restrict_def, blast)
lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) \<inter> C"
-apply (unfold restrict_def)
+ unfolding restrict_def
apply (auto simp add: domain_def)
done
@@ -352,7 +352,7 @@
"\<lbrakk>\<forall>f\<in>S. \<exists>C D. f \<in> C->D;
\<forall>f\<in>S. \<forall>y\<in>S. f<=y | y<=f\<rbrakk> \<Longrightarrow>
\<Union>(S) \<in> domain(\<Union>(S)) -> range(\<Union>(S))"
-apply (unfold Pi_def)
+ unfolding Pi_def
apply (blast intro!: rel_Union function_Union)
done
@@ -468,7 +468,7 @@
done
lemma update_idem: "\<lbrakk>f`x = y; f \<in> Pi(A,B); x \<in> A\<rbrakk> \<Longrightarrow> f(x:=y) = f"
-apply (unfold update_def)
+ unfolding update_def
apply (simp add: domain_of_fun cons_absorb)
apply (rule fun_extension)
apply (best intro: apply_type if_type lam_type, assumption, simp)
@@ -482,7 +482,7 @@
by (unfold update_def, simp)
lemma update_type: "\<lbrakk>f \<in> Pi(A,B); x \<in> A; y \<in> B(x)\<rbrakk> \<Longrightarrow> f(x:=y) \<in> Pi(A, B)"
-apply (unfold update_def)
+ unfolding update_def
apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
done
@@ -539,7 +539,7 @@
by (blast intro: lam_type elim: Pi_lamE)
lemma lam_mono: "A<=B \<Longrightarrow> Lambda(A,c) \<subseteq> Lambda(B,c)"
-apply (unfold lam_def)
+ unfolding lam_def
apply (erule RepFun_mono)
done
--- a/src/ZF/pair.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/pair.thy Tue Sep 27 17:54:20 2022 +0100
@@ -46,7 +46,7 @@
lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
lemma Pair_not_0: "\<langle>a,b\<rangle> \<noteq> 0"
-apply (unfold Pair_def)
+ unfolding Pair_def
apply (blast elim: equalityE)
done
--- a/src/ZF/upair.thy Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/upair.thy Tue Sep 27 17:54:20 2022 +0100
@@ -66,7 +66,7 @@
subsection\<open>Rules for Binary Intersection, Defined via \<^term>\<open>Upair\<close>\<close>
lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c \<in> A \<and> c \<in> B)"
-apply (unfold Int_def)
+ unfolding Int_def
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done
@@ -104,7 +104,7 @@
subsection\<open>Rules for \<^term>\<open>cons\<close>\<close>
lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a \<in> A)"
-apply (unfold cons_def)
+ unfolding cons_def
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done
@@ -152,7 +152,7 @@
lemma the_equality [intro]:
"\<lbrakk>P(a); \<And>x. P(x) \<Longrightarrow> x=a\<rbrakk> \<Longrightarrow> (THE x. P(x)) = a"
-apply (unfold the_def)
+ unfolding the_def
apply (fast dest: subst)
done
@@ -171,7 +171,7 @@
(*If it's "undefined", it's zero!*)
lemma the_0: "\<not> (\<exists>!x. P(x)) \<Longrightarrow> (THE x. P(x))=0"
-apply (unfold the_def)
+ unfolding the_def
apply (blast elim!: ReplaceE)
done