--- a/src/ZF/AC/AC15_WO6.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC15_WO6.thy Tue Sep 27 18:02:34 2022 +0100
@@ -134,7 +134,7 @@
(* ********************************************************************** *)
theorem AC12_AC15: "AC12 \<Longrightarrow> AC15"
-apply (unfold AC12_def AC15_def)
+ unfolding AC12_def AC15_def
apply (blast del: ballI
intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
done
@@ -168,7 +168,7 @@
done
theorem AC15_WO6: "AC15 \<Longrightarrow> WO6"
-apply (unfold AC15_def WO6_def)
+ unfolding AC15_def WO6_def
apply (rule allI)
apply (erule_tac x = "Pow (A) -{0}" in allE)
apply (erule impE, fast)
@@ -212,7 +212,7 @@
(* ********************************************************************** *)
lemma AC1_AC13: "AC1 \<Longrightarrow> AC13(1)"
-apply (unfold AC1_def AC13_def)
+ unfolding AC1_def AC13_def
apply (rule allI)
apply (erule allE)
apply (rule impI)
@@ -272,7 +272,7 @@
done
theorem AC13_AC1: "AC13(1) \<Longrightarrow> AC1"
-apply (unfold AC13_def AC1_def)
+ unfolding AC13_def AC1_def
apply (fast elim!: AC13_AC1_lemma)
done
@@ -281,7 +281,7 @@
(* ********************************************************************** *)
theorem AC11_AC14: "AC11 \<Longrightarrow> AC14"
-apply (unfold AC11_def AC14_def)
+ unfolding AC11_def AC14_def
apply (fast intro!: AC10_AC13)
done
--- a/src/ZF/AC/AC16_WO4.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Tue Sep 27 18:02:34 2022 +0100
@@ -87,7 +87,7 @@
done
lemma succ_not_lepoll_imp_eqpoll: "\<lbrakk>\<not>A \<approx> B; A \<lesssim> B\<rbrakk> \<Longrightarrow> succ(A) \<lesssim> B"
-apply (unfold lepoll_def eqpoll_def bij_def surj_def)
+ unfolding lepoll_def eqpoll_def bij_def surj_def
apply (fast elim!: succ_not_lepoll_lemma inj_is_fun)
done
@@ -254,7 +254,7 @@
lemma sI:
"\<lbrakk>w \<in> t_n; cons(b,cons(u,a)) \<subseteq> w; a \<subseteq> y; b \<in> y-a; l \<approx> a\<rbrakk>
\<Longrightarrow> w \<in> s(u)"
-apply (unfold s_def succ_def k_def)
+ unfolding s_def succ_def k_def
apply (blast intro!: eqpoll_imp_lepoll [THEN cons_lepoll_cong]
intro: subset_imp_lepoll lepoll_trans)
done
@@ -394,7 +394,7 @@
lemma LL_subset: "LL \<subseteq> {z \<in> Pow(y). z \<lesssim> succ(k #+ m)}"
-apply (unfold LL_def MM_def)
+ unfolding LL_def MM_def
apply (insert "includes")
apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
done
@@ -563,7 +563,7 @@
theorem AC16_WO4:
"\<lbrakk>AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat\<rbrakk> \<Longrightarrow> WO4(m)"
-apply (unfold AC_Equiv.AC16_def WO4_def)
+ unfolding AC_Equiv.AC16_def WO4_def
apply (rule allI)
apply (case_tac "Finite (A)")
apply (rule lemma1, assumption+)
--- a/src/ZF/AC/AC16_lemmas.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC16_lemmas.thy Tue Sep 27 18:02:34 2022 +0100
@@ -46,7 +46,7 @@
done
lemma eqpoll_RepFun_sing: "X\<approx>{{x}. x \<in> X}"
-apply (unfold eqpoll_def bij_def)
+ unfolding eqpoll_def bij_def
apply (rule_tac x = "\<lambda>x \<in> X. {x}" in exI)
apply (rule IntI)
apply (unfold inj_def surj_def, simp)
--- a/src/ZF/AC/AC17_AC1.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC17_AC1.thy Tue Sep 27 18:02:34 2022 +0100
@@ -19,7 +19,7 @@
by (fast intro!: lam_type apply_type)
lemma AC0_AC1: "AC0 \<Longrightarrow> AC1"
-apply (unfold AC0_def AC1_def)
+ unfolding AC0_def AC1_def
apply (blast intro: AC0_AC1_lemma)
done
@@ -35,7 +35,7 @@
done
lemma AC1_AC17: "AC1 \<Longrightarrow> AC17"
-apply (unfold AC1_def AC17_def)
+ unfolding AC1_def AC17_def
apply (rule allI)
apply (rule ballI)
apply (erule_tac x = "Pow (A) -{0}" in allE)
@@ -152,7 +152,7 @@
by (unfold pairwise_disjoint_def, fast)
lemma AC1_AC2: "AC1 \<Longrightarrow> AC2"
-apply (unfold AC1_def AC2_def)
+ unfolding AC1_def AC2_def
apply (rule allI)
apply (rule impI)
apply (elim asm_rl conjE allE exE impE, assumption)
@@ -185,7 +185,7 @@
done
lemma AC2_AC1: "AC2 \<Longrightarrow> AC1"
-apply (unfold AC1_def AC2_def pairwise_disjoint_def)
+ unfolding AC1_def AC2_def pairwise_disjoint_def
apply (intro allI impI)
apply (elim allE impE)
prefer 2 apply (fast elim!: AC2_AC1_aux3)
@@ -201,7 +201,7 @@
by blast
lemma AC1_AC4: "AC1 \<Longrightarrow> AC4"
-apply (unfold AC1_def AC4_def)
+ unfolding AC1_def AC4_def
apply (intro allI impI)
apply (drule spec, drule mp [OF _ empty_notin_images])
apply (best intro!: lam_type elim!: apply_type)
@@ -222,7 +222,7 @@
by fast
lemma AC4_AC3: "AC4 \<Longrightarrow> AC3"
-apply (unfold AC3_def AC4_def)
+ unfolding AC3_def AC4_def
apply (intro allI ballI)
apply (elim allE impE)
apply (erule AC4_AC3_aux1)
@@ -240,7 +240,7 @@
done
lemma AC3_AC1: "AC3 \<Longrightarrow> AC1"
-apply (unfold AC1_def AC3_def)
+ unfolding AC1_def AC3_def
apply (fast intro!: id_type elim: AC3_AC1_lemma [THEN subst])
done
@@ -249,7 +249,7 @@
(* ********************************************************************** *)
lemma AC4_AC5: "AC4 \<Longrightarrow> AC5"
-apply (unfold range_def AC4_def AC5_def)
+ unfolding range_def AC4_def AC5_def
apply (intro allI ballI)
apply (elim allE impE)
apply (erule fun_is_rel [THEN converse_type])
--- a/src/ZF/AC/AC7_AC9.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC7_AC9.thy Tue Sep 27 18:02:34 2022 +0100
@@ -69,7 +69,7 @@
by (blast dest: Sigma_fun_space_not0)
lemma AC7_AC6: "AC7 \<Longrightarrow> AC6"
-apply (unfold AC6_def AC7_def)
+ unfolding AC6_def AC7_def
apply (rule allI)
apply (rule impI)
apply (case_tac "A=0", simp)
@@ -97,7 +97,7 @@
done
lemma AC1_AC8: "AC1 \<Longrightarrow> AC8"
-apply (unfold AC1_def AC8_def)
+ unfolding AC1_def AC8_def
apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2)
done
@@ -114,7 +114,7 @@
by fast
lemma AC8_AC9: "AC8 \<Longrightarrow> AC9"
-apply (unfold AC8_def AC9_def)
+ unfolding AC8_def AC9_def
apply (intro allI impI)
apply (erule allE)
apply (erule impE, erule AC8_AC9_lemma, force)
@@ -159,7 +159,7 @@
done
lemma AC9_AC1: "AC9 \<Longrightarrow> AC1"
-apply (unfold AC1_def AC9_def)
+ unfolding AC1_def AC9_def
apply (intro allI impI)
apply (erule allE)
apply (case_tac "A\<noteq>0")
--- a/src/ZF/AC/DC.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/DC.thy Tue Sep 27 18:02:34 2022 +0100
@@ -136,7 +136,7 @@
by (unfold RR_def, fast)
lemma lemma1_2: "RR \<noteq> 0"
-apply (unfold RR_def XX_def)
+ unfolding RR_def XX_def
apply (rule all_ex [THEN ballE])
apply (erule_tac [2] notE [OF _ empty_subsetI [THEN PowI]])
apply (erule_tac impE [OF _ nat_0I [THEN n_lesspoll_nat]])
@@ -153,7 +153,7 @@
done
lemma lemma1_3: "range(RR) \<subseteq> domain(RR)"
-apply (unfold RR_def XX_def)
+ unfolding RR_def XX_def
apply (rule range_subset_domain, blast, clarify)
apply (frule fun_is_rel [THEN image_subset, THEN PowI,
THEN all_ex [THEN bspec]])
@@ -326,7 +326,7 @@
succ(\<Union>f \<in> Y. domain(f)) \<and> (\<forall>f\<in>Y. restrict(g, domain(f)) = f)")
apply (simp add: RR_def, blast)
apply (safe del: domainE)
-apply (unfold XX_def RR_def)
+ unfolding XX_def RR_def
apply (rule rev_bexI, erule singleton_in_funs)
apply (simp add: nat_0I [THEN rev_bexI] cons_fun_type2)
done
@@ -393,7 +393,7 @@
"\<lbrakk>\<forall>b<nat. <f``b, f`b> \<in> RR;
f \<in> nat -> XX; range(R) \<subseteq> domain(R); x \<in> domain(R)\<rbrakk>
\<Longrightarrow> allRR"
-apply (unfold RR_def allRR_def)
+ unfolding RR_def allRR_def
apply (rule oallI, drule ltD)
apply (erule nat_induct)
apply (drule_tac x=0 in ospec, blast intro: Limit_has_0)
@@ -463,7 +463,7 @@
theorem DC_nat_imp_DC0: "DC(nat) \<Longrightarrow> DC0"
-apply (unfold DC_def DC0_def)
+ unfolding DC_def DC0_def
apply (intro allI impI)
apply (erule asm_rl conjE ex_in_domain [THEN exE] allE)+
apply (erule impE [OF _ imp_DC0.lemma4], assumption+)
@@ -504,7 +504,7 @@
done
theorem DC_WO3: "(\<forall>K. Card(K) \<longrightarrow> DC(K)) \<Longrightarrow> WO3"
-apply (unfold DC_def WO3_def)
+ unfolding DC_def WO3_def
apply (rule allI)
apply (case_tac "A \<prec> Hartog (A)")
apply (fast dest!: lesspoll_imp_ex_lt_eqpoll
@@ -572,7 +572,7 @@
done
theorem WO1_DC_Card: "WO1 \<Longrightarrow> \<forall>K. Card(K) \<longrightarrow> DC(K)"
-apply (unfold DC_def WO1_def)
+ unfolding DC_def WO1_def
apply (rule allI impI)+
apply (erule allE exE conjE)+
apply (rule_tac x = "\<lambda>b \<in> K. ff (b, X, Ra, R) " in bexI)
--- a/src/ZF/AC/HH.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/HH.thy Tue Sep 27 18:02:34 2022 +0100
@@ -99,7 +99,7 @@
lemma HH_subset_x_imp_lepoll:
"\<lbrakk>HH(f, x, i) \<in> Pow(x)-{0}; Ord(i)\<rbrakk> \<Longrightarrow> i \<lesssim> Pow(x)-{0}"
-apply (unfold lepoll_def inj_def)
+ unfolding lepoll_def inj_def
apply (rule_tac x = "\<lambda>j \<in> i. HH (f, x, j) " in exI)
apply (simp (no_asm_simp))
apply (fast del: DiffE
@@ -235,7 +235,7 @@
done
lemma AC1_WO2: "AC1 \<Longrightarrow> WO2"
-apply (unfold AC1_def WO2_def eqpoll_def)
+ unfolding AC1_def WO2_def eqpoll_def
apply (intro allI)
apply (drule_tac x = "Pow(A) - {0}" in spec)
apply (blast dest: bijection)
--- a/src/ZF/AC/WO1_AC.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO1_AC.thy Tue Sep 27 18:02:34 2022 +0100
@@ -83,7 +83,7 @@
lemma lemma2_5:
"f \<in> bij(D+D, B) \<Longrightarrow> \<Union>({{f`Inl(i), f`Inr(i)}. i \<in> D})=B"
-apply (unfold bij_def surj_def)
+ unfolding bij_def surj_def
apply (fast elim!: inj_is_fun [THEN apply_type])
done
--- a/src/ZF/AC/WO1_WO7.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO1_WO7.thy Tue Sep 27 18:02:34 2022 +0100
@@ -21,7 +21,7 @@
(* ********************************************************************** *)
lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA"
-apply (unfold WO7_def LEMMA_def)
+ unfolding WO7_def LEMMA_def
apply (blast intro: Finite_well_ord_converse)
done
@@ -30,7 +30,7 @@
(* ********************************************************************** *)
lemma LEMMA_imp_WO1: "LEMMA \<Longrightarrow> WO1"
-apply (unfold WO1_def LEMMA_def Finite_def eqpoll_def)
+ unfolding WO1_def LEMMA_def Finite_def eqpoll_def
apply (blast intro!: well_ord_rvimage [OF bij_is_inj nat_implies_well_ord])
done
@@ -49,7 +49,7 @@
lemma converse_Memrel_not_wf_on:
"\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>wf[a](converse(Memrel(a)))"
-apply (unfold wf_on_def wf_def)
+ unfolding wf_on_def wf_def
apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
apply (rule notI)
apply (erule_tac x = nat in allE, blast)
@@ -102,7 +102,7 @@
(* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin \<and> Rubin's proof*)
lemma WO8_WO1: "WO8 \<Longrightarrow> WO1"
-apply (unfold WO1_def WO8_def)
+ unfolding WO1_def WO8_def
apply (rule allI)
apply (erule_tac x = "{{x}. x \<in> A}" in allE)
apply (erule impE)
--- a/src/ZF/AC/WO2_AC16.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Tue Sep 27 18:02:34 2022 +0100
@@ -394,7 +394,7 @@
\<Longrightarrow> b=y"
apply (drule subset_imp_eq)
apply (erule_tac [3] nat_succI)
-apply (unfold bij_def inj_def)
+ unfolding bij_def inj_def
apply (blast intro: eqpoll_sym eqpoll_imp_lepoll
dest: ltD apply_type)+
done
--- a/src/ZF/AC/WO6_WO1.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Tue Sep 27 18:02:34 2022 +0100
@@ -66,7 +66,7 @@
(* ********************************************************************** *)
lemma WO3_WO1: "WO3 \<Longrightarrow> WO1"
-apply (unfold eqpoll_def WO1_def WO3_def)
+ unfolding eqpoll_def WO1_def WO3_def
apply (intro allI)
apply (drule_tac x=A in spec)
apply (blast intro: bij_is_inj well_ord_rvimage
@@ -76,7 +76,7 @@
(* ********************************************************************** *)
lemma WO1_WO2: "WO1 \<Longrightarrow> WO2"
-apply (unfold eqpoll_def WO1_def WO2_def)
+ unfolding eqpoll_def WO1_def WO2_def
apply (blast intro!: Ord_ordertype ordermap_bij)
done
@@ -94,7 +94,7 @@
by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)
lemma WO1_WO4: "WO1 \<Longrightarrow> WO4(1)"
-apply (unfold WO1_def WO4_def)
+ unfolding WO1_def WO4_def
apply (rule allI)
apply (erule_tac x = A in allE)
apply (erule exE)
--- a/src/ZF/Bin.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Bin.thy Tue Sep 27 18:02:34 2022 +0100
@@ -402,7 +402,7 @@
"\<lbrakk>v \<in> bin; w \<in> bin\<rbrakk>
\<Longrightarrow> integ_of(v) $< integ_of(w)
\<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
-apply (unfold zless_def zdiff_def)
+ unfolding zless_def zdiff_def
apply (simp add: integ_of_minus integ_of_add)
done
--- a/src/ZF/Cardinal.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Cardinal.thy Tue Sep 27 18:02:34 2022 +0100
@@ -125,7 +125,7 @@
(*Asymmetry law*)
lemma eqpollI: "\<lbrakk>X \<lesssim> Y; Y \<lesssim> X\<rbrakk> \<Longrightarrow> X \<approx> Y"
-apply (unfold lepoll_def eqpoll_def)
+ unfolding lepoll_def eqpoll_def
apply (elim exE)
apply (rule schroeder_bernstein, assumption+)
done
@@ -138,7 +138,7 @@
by (blast intro: eqpollI elim!: eqpollE)
lemma lepoll_0_is_0: "A \<lesssim> 0 \<Longrightarrow> A = 0"
-apply (unfold lepoll_def inj_def)
+ unfolding lepoll_def inj_def
apply (blast dest: apply_type)
done
@@ -332,7 +332,7 @@
(*Need AC to get @{term"X \<lesssim> Y \<Longrightarrow> |X| \<le> |Y|"}; see well_ord_lepoll_imp_cardinal_le
Converse also requires AC, but see well_ord_cardinal_eqE*)
lemma cardinal_cong: "X \<approx> Y \<Longrightarrow> |X| = |Y|"
-apply (unfold eqpoll_def cardinal_def)
+ unfolding eqpoll_def cardinal_def
apply (rule Least_cong)
apply (blast intro: comp_bij bij_converse_bij)
done
@@ -380,13 +380,13 @@
(* Could replace the @{term"\<not>(j \<approx> i)"} by @{term"\<not>(i \<preceq> j)"}. *)
lemma CardI: "\<lbrakk>Ord(i); \<And>j. j<i \<Longrightarrow> \<not>(j \<approx> i)\<rbrakk> \<Longrightarrow> Card(i)"
-apply (unfold Card_def cardinal_def)
+ unfolding Card_def cardinal_def
apply (subst Least_equality)
apply (blast intro: eqpoll_refl)+
done
lemma Card_is_Ord: "Card(i) \<Longrightarrow> Ord(i)"
-apply (unfold Card_def cardinal_def)
+ unfolding Card_def cardinal_def
apply (erule ssubst)
apply (rule Ord_Least)
done
@@ -621,7 +621,7 @@
lemma nat_lepoll_imp_ex_eqpoll_n:
"\<lbrakk>n \<in> nat; nat \<lesssim> X\<rbrakk> \<Longrightarrow> \<exists>Y. Y \<subseteq> X \<and> n \<approx> Y"
-apply (unfold lepoll_def eqpoll_def)
+ unfolding lepoll_def eqpoll_def
apply (fast del: subsetI subsetCE
intro!: subset_SIs
dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
@@ -650,7 +650,7 @@
lemma lesspoll_succ_imp_lepoll:
"\<lbrakk>A \<prec> succ(m); m \<in> nat\<rbrakk> \<Longrightarrow> A \<lesssim> m"
-apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def)
+ unfolding lesspoll_def lepoll_def eqpoll_def bij_def
apply (auto dest: inj_not_surj_succ)
done
@@ -951,7 +951,7 @@
lemma Finite_imp_well_ord:
"Finite(A) \<Longrightarrow> \<exists>r. well_ord(A,r)"
-apply (unfold Finite_def eqpoll_def)
+ unfolding Finite_def eqpoll_def
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
done
--- a/src/ZF/CardinalArith.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/CardinalArith.thy Tue Sep 27 18:02:34 2022 +0100
@@ -293,14 +293,14 @@
done
lemma cmult_1 [simp]: "Card(K) \<Longrightarrow> 1 \<otimes> K = K"
-apply (unfold cmult_def succ_def)
+ unfolding cmult_def succ_def
apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
done
subsection\<open>Some inequalities for multiplication\<close>
lemma prod_square_lepoll: "A \<lesssim> A*A"
-apply (unfold lepoll_def inj_def)
+ unfolding lepoll_def inj_def
apply (rule_tac x = "\<lambda>x\<in>A. \<langle>x,x\<rangle>" in exI, simp)
done
@@ -317,7 +317,7 @@
subsubsection\<open>Multiplication by a non-zero cardinal\<close>
lemma prod_lepoll_self: "b \<in> B \<Longrightarrow> A \<lesssim> A*B"
-apply (unfold lepoll_def inj_def)
+ unfolding lepoll_def inj_def
apply (rule_tac x = "\<lambda>x\<in>A. \<langle>x,b\<rangle>" in exI, simp)
done
@@ -366,7 +366,7 @@
(*Unconditional version requires AC*)
lemma cmult_succ_lemma:
"\<lbrakk>Ord(m); Ord(n)\<rbrakk> \<Longrightarrow> succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)"
-apply (unfold cmult_def cadd_def)
+ unfolding cmult_def cadd_def
apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])
apply (rule cardinal_cong [symmetric])
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
@@ -502,7 +502,7 @@
lemma pred_csquare_subset:
"z<K \<Longrightarrow> Order.pred(K*K, \<langle>z,z\<rangle>, csquare_rel(K)) \<subseteq> succ(z)*succ(z)"
-apply (unfold Order.pred_def)
+ unfolding Order.pred_def
apply (safe del: SigmaI dest!: csquareD)
apply (unfold lt_def, auto)
done
--- a/src/ZF/Coind/ECR.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/ECR.thy Tue Sep 27 18:02:34 2022 +0100
@@ -61,7 +61,7 @@
lemma basic_consistency_lem:
"\<lbrakk>ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te)\<rbrakk> \<Longrightarrow> hastyenv(ve,te)"
-apply (unfold isofenv_def hastyenv_def)
+ unfolding isofenv_def hastyenv_def
apply (force intro: te_appI ve_domI)
done
--- a/src/ZF/Coind/Map.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/Map.thy Tue Sep 27 18:02:34 2022 +0100
@@ -81,7 +81,7 @@
lemma mapQU:
"\<lbrakk>m \<in> PMap(A,quniv(B)); \<And>x. x \<in> A \<Longrightarrow> x \<in> univ(B)\<rbrakk> \<Longrightarrow> m \<in> quniv(B)"
-apply (unfold PMap_def TMap_def)
+ unfolding PMap_def TMap_def
apply (blast intro!: MapQU_lemma [THEN subsetD])
done
--- a/src/ZF/Coind/Values.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/Values.thy Tue Sep 27 18:02:34 2022 +0100
@@ -67,7 +67,7 @@
lemma v_constNE [simp]: "c \<in> Const \<Longrightarrow> v_const(c) \<noteq> 0"
-apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
+ unfolding QPair_def QInl_def QInr_def Val_ValEnv.con_defs
apply (drule constNEE, auto)
done
--- a/src/ZF/Constructible/L_axioms.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Tue Sep 27 18:02:34 2022 +0100
@@ -205,7 +205,7 @@
theorem Ex_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(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
+ unfolding L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def
apply (elim meta_exE)
apply (rule meta_exI)
apply (erule reflection.Ex_reflection [OF reflection_Lset])
@@ -214,7 +214,7 @@
theorem All_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(z) \<longrightarrow> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
+ unfolding L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def
apply (elim meta_exE)
apply (rule meta_exI)
apply (erule reflection.All_reflection [OF reflection_Lset])
@@ -239,7 +239,7 @@
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[##Lset(a)]. Q(a,x,z)]"
-apply (unfold setclass_def rex_def)
+ unfolding setclass_def rex_def
apply (erule Rex_reflection [unfolded rex_def Bex_def])
done
@@ -247,7 +247,7 @@
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[##Lset(a)]. Q(a,x,z)]"
-apply (unfold setclass_def rall_def)
+ unfolding setclass_def rall_def
apply (erule Rall_reflection [unfolded rall_def Ball_def])
done
@@ -259,7 +259,7 @@
lemma ReflectsD:
"\<lbrakk>REFLECTS[P,Q]; Ord(i)\<rbrakk>
\<Longrightarrow> \<exists>j. i<j \<and> (\<forall>x \<in> Lset(j). P(x) \<longleftrightarrow> Q(j,x))"
-apply (unfold L_Reflects_def Closed_Unbounded_def)
+ unfolding L_Reflects_def Closed_Unbounded_def
apply (elim meta_exE, clarify)
apply (blast dest!: UnboundedD)
done
--- a/src/ZF/Constructible/Rank.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Rank.thy Tue Sep 27 18:02:34 2022 +0100
@@ -39,7 +39,7 @@
lemma (in M_ordertype) wellordered_iso_subset_lemma:
"\<lbrakk>wellordered(M,A,r); f \<in> ord_iso(A,r, A',r); A'<= A; y \<in> A;
M(A); M(f); M(r)\<rbrakk> \<Longrightarrow> \<not> <f`y, y> \<in> r"
-apply (unfold wellordered_def ord_iso_def)
+ unfolding wellordered_def ord_iso_def
apply (elim conjE CollectE)
apply (erule wellfounded_on_induct, assumption+)
apply (insert well_ord_iso_separation [of A f r])
--- a/src/ZF/Constructible/Reflection.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Reflection.thy Tue Sep 27 18:02:34 2022 +0100
@@ -187,7 +187,7 @@
"\<lbrakk>y\<in>Mset(a); Cl(a); ClEx(P,a);
\<And>a. \<lbrakk>Cl(a); Ord(a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)\<rbrakk>
\<Longrightarrow> (\<exists>z. M(z) \<and> P(\<langle>y,z\<rangle>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,\<langle>y,z\<rangle>))"
-apply (unfold ClEx_def FF_def F0_def M_def)
+ unfolding ClEx_def FF_def F0_def M_def
apply (rule ex_reflection.ZF_ClEx_iff
[OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro,
of Mset Cl])
@@ -204,7 +204,7 @@
lemma Closed_Unbounded_ClEx:
"(\<And>a. \<lbrakk>Cl(a); Ord(a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x))
\<Longrightarrow> Closed_Unbounded(ClEx(P))"
-apply (unfold ClEx_eq FF_def F0_def M_def)
+ unfolding ClEx_eq FF_def F0_def M_def
apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl])
apply (rule ex_reflection.intro, rule reflection_axioms)
apply (blast intro: ex_reflection_axioms.intro)
--- a/src/ZF/Constructible/Relative.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Relative.thy Tue Sep 27 18:02:34 2022 +0100
@@ -945,7 +945,7 @@
lemma (in M_trivial) limit_ordinal_abs [simp]:
"M(a) \<Longrightarrow> limit_ordinal(M,a) \<longleftrightarrow> Limit(a)"
-apply (unfold Limit_def limit_ordinal_def)
+ unfolding Limit_def limit_ordinal_def
apply (simp add: Ord_0_lt_iff)
apply (simp add: lt_def, blast)
done
--- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Sep 27 18:02:34 2022 +0100
@@ -890,7 +890,7 @@
fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
-apply (unfold is_and_def is_not_def)
+ unfolding is_and_def is_not_def
apply (intro FOL_reflections function_reflections)
done
--- a/src/ZF/Epsilon.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Epsilon.thy Tue Sep 27 18:02:34 2022 +0100
@@ -48,7 +48,7 @@
lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
lemma Transset_eclose: "Transset(eclose(A))"
-apply (unfold eclose_def Transset_def)
+ unfolding eclose_def Transset_def
apply (rule subsetI [THEN ballI])
apply (erule UN_E)
apply (rule nat_succI [THEN UN_I], assumption)
--- a/src/ZF/EquivClass.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/EquivClass.thy Tue Sep 27 18:02:34 2022 +0100
@@ -52,7 +52,7 @@
(*second half*)
lemma comp_equivI:
"\<lbrakk>converse(r) O r = r; domain(r) = A\<rbrakk> \<Longrightarrow> equiv(A,r)"
-apply (unfold equiv_def refl_def sym_def trans_def)
+ unfolding equiv_def refl_def sym_def trans_def
apply (erule equalityE)
apply (subgoal_tac "\<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> \<langle>y,x\<rangle> \<in> r", blast+)
done
--- a/src/ZF/Finite.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Finite.thy Tue Sep 27 18:02:34 2022 +0100
@@ -41,7 +41,7 @@
subsection \<open>Finite Powerset Operator\<close>
lemma Fin_mono: "A<=B \<Longrightarrow> Fin(A) \<subseteq> Fin(B)"
-apply (unfold Fin.defs)
+ unfolding Fin.defs
apply (rule lfp_mono)
apply (rule Fin.bnd_mono)+
apply blast
@@ -130,7 +130,7 @@
lemma FiniteFun_mono:
"\<lbrakk>A<=C; B<=D\<rbrakk> \<Longrightarrow> A -||> B \<subseteq> C -||> D"
-apply (unfold FiniteFun.defs)
+ unfolding FiniteFun.defs
apply (rule lfp_mono)
apply (rule FiniteFun.bnd_mono)+
apply (intro Fin_mono Sigma_mono basic_monos, assumption+)
--- a/src/ZF/Induct/Binary_Trees.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy Tue Sep 27 18:02:34 2022 +0100
@@ -33,14 +33,14 @@
\<close>
lemma bt_mono: "A \<subseteq> B \<Longrightarrow> bt(A) \<subseteq> bt(B)"
- apply (unfold bt.defs)
+ unfolding bt.defs
apply (rule lfp_mono)
apply (rule bt.bnd_mono)+
apply (rule univ_mono basic_monos | assumption)+
done
lemma bt_univ: "bt(univ(A)) \<subseteq> univ(A)"
- apply (unfold bt.defs bt.con_defs)
+ unfolding bt.defs bt.con_defs
apply (rule lfp_lowerbound)
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
--- a/src/ZF/Induct/Datatypes.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Datatypes.thy Tue Sep 27 18:02:34 2022 +0100
@@ -32,14 +32,14 @@
\<close>
lemma data_mono: "\<lbrakk>A \<subseteq> C; B \<subseteq> D\<rbrakk> \<Longrightarrow> data(A, B) \<subseteq> data(C, D)"
- apply (unfold data.defs)
+ unfolding data.defs
apply (rule lfp_mono)
apply (rule data.bnd_mono)+
apply (rule univ_mono Un_mono basic_monos | assumption)+
done
lemma data_univ: "data(univ(A), univ(A)) \<subseteq> univ(A)"
- apply (unfold data.defs data.con_defs)
+ unfolding data.defs data.con_defs
apply (rule lfp_lowerbound)
apply (rule_tac [2] subset_trans [OF A_subset_univ Un_upper1, THEN univ_mono])
apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
--- a/src/ZF/Induct/ListN.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/ListN.thy Tue Sep 27 18:02:34 2022 +0100
@@ -37,7 +37,7 @@
done
lemma listn_mono: "A \<subseteq> B \<Longrightarrow> listn(A) \<subseteq> listn(B)"
- apply (unfold listn.defs)
+ unfolding listn.defs
apply (rule lfp_mono)
apply (rule listn.bnd_mono)+
apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
--- a/src/ZF/Induct/Multiset.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Multiset.thy Tue Sep 27 18:02:34 2022 +0100
@@ -268,12 +268,12 @@
by (auto intro!: lam_cong simp add: munion_def)
lemma munion_assoc: "(M +# N) +# K = M +# (N +# K)"
-apply (unfold munion_def mset_of_def)
+ unfolding munion_def mset_of_def
apply (rule lam_cong, auto)
done
lemma munion_lcommute: "M +# (N +# K) = N +# (M +# K)"
-apply (unfold munion_def mset_of_def)
+ unfolding munion_def mset_of_def
apply (rule lam_cong, auto)
done
@@ -291,7 +291,7 @@
by (auto simp add: multiset_def mdiff_def normalize_def multiset_fun_iff mset_of_def funrestrict_def)
lemma mdiff_union_inverse2 [simp]: "multiset(M) \<Longrightarrow> M +# {#a#} -# {#a#} = M"
-apply (unfold multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def)
+ unfolding multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def
apply (auto cong add: if_cong simp add: ltD multiset_fun_iff funrestrict_def subset_Un_iff2 [THEN iffD1])
prefer 2 apply (force intro!: lam_type)
apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
@@ -483,7 +483,7 @@
unfolding multiset_def
apply (erule Finite_induct)
apply (auto simp add: multiset_fun_iff)
-apply (unfold mset_of_def mcount_def)
+ unfolding mset_of_def mcount_def
apply (case_tac "x \<in> A", auto)
apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1")
apply (erule ssubst)
--- a/src/ZF/Induct/Ntree.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Ntree.thy Tue Sep 27 18:02:34 2022 +0100
@@ -85,7 +85,7 @@
\<close>
lemma ntree_mono: "A \<subseteq> B \<Longrightarrow> ntree(A) \<subseteq> ntree(B)"
- apply (unfold ntree.defs)
+ unfolding ntree.defs
apply (rule lfp_mono)
apply (rule ntree.bnd_mono)+
apply (assumption | rule univ_mono basic_monos)+
@@ -93,7 +93,7 @@
lemma ntree_univ: "ntree(univ(A)) \<subseteq> univ(A)"
\<comment> \<open>Easily provable by induction also\<close>
- apply (unfold ntree.defs ntree.con_defs)
+ unfolding ntree.defs ntree.con_defs
apply (rule lfp_lowerbound)
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
apply (blast intro: Pair_in_univ nat_fun_univ [THEN subsetD])
--- a/src/ZF/Induct/PropLog.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/PropLog.thy Tue Sep 27 18:02:34 2022 +0100
@@ -107,7 +107,7 @@
subsection \<open>Proof theory of propositional logic\<close>
lemma thms_mono: "G \<subseteq> H \<Longrightarrow> thms(G) \<subseteq> thms(H)"
- apply (unfold thms.defs)
+ unfolding thms.defs
apply (rule lfp_mono)
apply (rule thms.bnd_mono)+
apply (assumption | rule univ_mono basic_monos)+
--- a/src/ZF/Induct/Rmap.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Rmap.thy Tue Sep 27 18:02:34 2022 +0100
@@ -21,7 +21,7 @@
type_intros domainI rangeI list.intros
lemma rmap_mono: "r \<subseteq> s \<Longrightarrow> rmap(r) \<subseteq> rmap(s)"
- apply (unfold rmap.defs)
+ unfolding rmap.defs
apply (rule lfp_mono)
apply (rule rmap.bnd_mono)+
apply (assumption | rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
--- a/src/ZF/Induct/Term.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Term.thy Tue Sep 27 18:02:34 2022 +0100
@@ -77,7 +77,7 @@
\<close>
lemma term_mono: "A \<subseteq> B \<Longrightarrow> term(A) \<subseteq> term(B)"
- apply (unfold term.defs)
+ unfolding term.defs
apply (rule lfp_mono)
apply (rule term.bnd_mono)+
apply (rule univ_mono basic_monos| assumption)+
@@ -85,7 +85,7 @@
lemma term_univ: "term(univ(A)) \<subseteq> univ(A)"
\<comment> \<open>Easily provable by induction also\<close>
- apply (unfold term.defs term.con_defs)
+ unfolding term.defs term.con_defs
apply (rule lfp_lowerbound)
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
apply safe
@@ -120,7 +120,7 @@
term_rec(Apply(a,ts), d) = d(a, ts, map (\<lambda>z. term_rec(z,d), ts))"
\<comment> \<open>Typing premise is necessary to invoke \<open>map_lemma\<close>.\<close>
apply (rule term_rec_def [THEN def_Vrec, THEN trans])
- apply (unfold term.con_defs)
+ unfolding term.con_defs
apply (simp add: rank_pair2 map_lemma)
done
--- a/src/ZF/Induct/Tree_Forest.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Tue Sep 27 18:02:34 2022 +0100
@@ -39,7 +39,7 @@
\<close>
lemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)"
- apply (unfold tree_forest.defs)
+ unfolding tree_forest.defs
apply (rule Part_subset)
done
@@ -47,7 +47,7 @@
by (rule tree_subset_TF [THEN subsetD])
lemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)"
- apply (unfold tree_forest.defs)
+ unfolding tree_forest.defs
apply (rule Part_subset)
done
@@ -63,7 +63,7 @@
"tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
\<comment> \<open>NOT useful, but interesting \dots\<close>
supply rews = tree_forest.con_defs tree_def forest_def
- apply (unfold tree_def forest_def)
+ unfolding tree_def forest_def
apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
elim: tree_forest.cases [unfolded rews])
done
@@ -75,13 +75,13 @@
by (rule tree_forest_unfold [unfolded tree_def forest_def])
lemma tree_unfold: "tree(A) = {Inl(x). x \<in> A \<times> forest(A)}"
- apply (unfold tree_def forest_def)
+ unfolding tree_def forest_def
apply (rule Part_Inl [THEN subst])
apply (rule tree_forest_unfold' [THEN subst_context])
done
lemma forest_unfold: "forest(A) = {Inr(x). x \<in> {0} + tree(A)*forest(A)}"
- apply (unfold tree_def forest_def)
+ unfolding tree_def forest_def
apply (rule Part_Inr [THEN subst])
apply (rule tree_forest_unfold' [THEN subst_context])
done
--- a/src/ZF/List.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/List.thy Tue Sep 27 18:02:34 2022 +0100
@@ -154,7 +154,7 @@
(** Lemmas to justify using "list" in other recursive type definitions **)
lemma list_mono: "A<=B \<Longrightarrow> list(A) \<subseteq> list(B)"
-apply (unfold list.defs )
+ unfolding list.defs
apply (rule lfp_mono)
apply (simp_all add: list.bnd_mono)
apply (assumption | rule univ_mono basic_monos)+
@@ -162,7 +162,7 @@
(*There is a similar proof by list induction.*)
lemma list_univ: "list(univ(A)) \<subseteq> univ(A)"
-apply (unfold list.defs list.con_defs)
+ unfolding list.defs list.con_defs
apply (rule lfp_lowerbound)
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
--- a/src/ZF/Order.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Order.thy Tue Sep 27 18:02:34 2022 +0100
@@ -362,7 +362,7 @@
lemma well_ord_ord_iso:
"\<lbrakk>well_ord(B,s); f \<in> ord_iso(A,r,B,s)\<rbrakk> \<Longrightarrow> well_ord(A,r)"
-apply (unfold well_ord_def tot_ord_def)
+ unfolding well_ord_def tot_ord_def
apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
done
@@ -409,7 +409,7 @@
(*Does not assume r is a wellordering!*)
lemma ord_iso_image_pred:
"\<lbrakk>f \<in> ord_iso(A,r,B,s); a \<in> A\<rbrakk> \<Longrightarrow> f `` pred(A,a,r) = pred(B, f`a, s)"
-apply (unfold ord_iso_def pred_def)
+ unfolding ord_iso_def pred_def
apply (erule CollectE)
apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
apply (rule equalityI)
@@ -500,7 +500,7 @@
lemma function_ord_iso_map:
"well_ord(B,s) \<Longrightarrow> function(ord_iso_map(A,r,B,s))"
-apply (unfold ord_iso_map_def function_def)
+ unfolding ord_iso_map_def function_def
apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans)
done
@@ -567,7 +567,7 @@
\<Longrightarrow> domain(ord_iso_map(A,r,B,s)) = A |
(\<exists>x\<in>A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"
apply (frule well_ord_is_wf)
-apply (unfold wf_on_def wf_def)
+ unfolding wf_on_def wf_def
apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec)
apply safe
(*The first case: the domain equals A*)
@@ -642,7 +642,7 @@
lemma well_ord_imp_ex1_first:
"\<lbrakk>well_ord(A,r); B<=A; B\<noteq>0\<rbrakk> \<Longrightarrow> (\<exists>!b. first(b,B,r))"
-apply (unfold well_ord_def wf_on_def wf_def first_def)
+ unfolding well_ord_def wf_on_def wf_def first_def
apply (elim conjE allE disjE, blast)
apply (erule bexE)
apply (rule_tac a = x in ex1I, auto)
--- a/src/ZF/OrderArith.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/OrderArith.thy Tue Sep 27 18:02:34 2022 +0100
@@ -325,13 +325,13 @@
lemma irrefl_rvimage:
"\<lbrakk>f \<in> inj(A,B); irrefl(B,r)\<rbrakk> \<Longrightarrow> irrefl(A, rvimage(A,f,r))"
-apply (unfold irrefl_def rvimage_def)
+ unfolding irrefl_def rvimage_def
apply (blast intro: inj_is_fun [THEN apply_type])
done
lemma trans_on_rvimage:
"\<lbrakk>f \<in> inj(A,B); trans[B](r)\<rbrakk> \<Longrightarrow> trans[A](rvimage(A,f,r))"
-apply (unfold trans_on_def rvimage_def)
+ unfolding trans_on_def rvimage_def
apply (blast intro: inj_is_fun [THEN apply_type])
done
@@ -384,7 +384,7 @@
lemma well_ord_rvimage:
"\<lbrakk>f \<in> inj(A,B); well_ord(B,r)\<rbrakk> \<Longrightarrow> well_ord(A, rvimage(A,f,r))"
apply (rule well_ordI)
-apply (unfold well_ord_def tot_ord_def)
+ unfolding well_ord_def tot_ord_def
apply (blast intro!: wf_on_rvimage inj_is_fun)
apply (blast intro!: linear_rvimage)
done
--- a/src/ZF/OrderType.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/OrderType.thy Tue Sep 27 18:02:34 2022 +0100
@@ -99,7 +99,7 @@
lemma ordermap_type:
"ordermap(A,r) \<in> A -> ordertype(A,r)"
-apply (unfold ordermap_def ordertype_def)
+ unfolding ordermap_def ordertype_def
apply (rule lam_type)
apply (rule lamI [THEN imageI], assumption+)
done
@@ -110,7 +110,7 @@
lemma ordermap_eq_image:
"\<lbrakk>wf[A](r); x \<in> A\<rbrakk>
\<Longrightarrow> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
-apply (unfold ordermap_def pred_def)
+ unfolding ordermap_def pred_def
apply (simp (no_asm_simp))
apply (erule wfrec_on [THEN trans], assumption)
apply (simp (no_asm_simp) add: subset_iff image_lam vimage_singleton_iff)
@@ -149,7 +149,7 @@
apply (rule_tac a=x in wf_on_induct, assumption+)
apply (simp (no_asm_simp) add: ordermap_pred_unfold)
apply (rule OrdI [OF _ Ord_is_Transset])
-apply (unfold pred_def Transset_def)
+ unfolding pred_def Transset_def
apply (blast intro: trans_onD
dest!: ordermap_unfold [THEN equalityD1])+
done
@@ -160,7 +160,7 @@
apply (subst image_fun [OF ordermap_type subset_refl])
apply (rule OrdI [OF _ Ord_is_Transset])
prefer 2 apply (blast intro: Ord_ordermap)
-apply (unfold Transset_def well_ord_def)
+ unfolding Transset_def well_ord_def
apply (blast intro: trans_onD
dest!: ordermap_unfold [THEN equalityD1])
done
@@ -190,7 +190,7 @@
lemma ordermap_bij:
"well_ord(A,r) \<Longrightarrow> ordermap(A,r) \<in> bij(A, ordertype(A,r))"
-apply (unfold well_ord_def tot_ord_def bij_def inj_def)
+ unfolding well_ord_def tot_ord_def bij_def inj_def
apply (force intro!: ordermap_type ordermap_surj
elim: linearE dest: ordermap_mono
simp add: mem_not_refl)
@@ -381,7 +381,7 @@
"b \<in> B \<Longrightarrow>
id(A+pred(B,b,s))
\<in> bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
-apply (unfold pred_def id_def)
+ unfolding pred_def id_def
apply (rule_tac d = "\<lambda>z. z" in lam_bijective, auto)
done
@@ -780,7 +780,7 @@
\<Longrightarrow> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
rmult(i,Memrel(i),j,Memrel(j))) =
raw_oadd (j**i', j')"
-apply (unfold raw_oadd_def omult_def)
+ unfolding raw_oadd_def omult_def
apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2
well_ord_Memrel)
apply (rule trans)
--- a/src/ZF/Perm.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Perm.thy Tue Sep 27 18:02:34 2022 +0100
@@ -177,7 +177,7 @@
lemmas id_inj = subset_refl [THEN id_subset_inj]
lemma id_surj: "id(A): surj(A,A)"
-apply (unfold id_def surj_def)
+ unfolding id_def surj_def
apply (simp (no_asm_simp))
done
--- a/src/ZF/QUniv.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/QUniv.thy Tue Sep 27 18:02:34 2022 +0100
@@ -122,7 +122,7 @@
(*The opposite inclusion*)
lemma quniv_QPair_D:
"<a;b> \<in> quniv(A) \<Longrightarrow> a: quniv(A) \<and> b: quniv(A)"
-apply (unfold quniv_def QPair_def)
+ unfolding quniv_def QPair_def
apply (rule Transset_includes_summands [THEN conjE])
apply (rule Transset_eclose [THEN Transset_univ])
apply (erule PowD, blast)
--- a/src/ZF/Resid/Confluence.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Resid/Confluence.thy Tue Sep 27 18:02:34 2022 +0100
@@ -22,7 +22,7 @@
lemma strip_lemma_r:
"\<lbrakk>confluence(Spar_red1)\<rbrakk>\<Longrightarrow> strip"
-apply (unfold confluence_def strip_def)
+ unfolding confluence_def strip_def
apply (rule impI [THEN allI, THEN allI])
apply (erule Spar_red.induct, fast)
apply (fast intro: Spar_red.trans)
@@ -31,7 +31,7 @@
lemma strip_lemma_l:
"strip\<Longrightarrow> confluence(Spar_red)"
-apply (unfold confluence_def strip_def)
+ unfolding confluence_def strip_def
apply (rule impI [THEN allI, THEN allI])
apply (erule Spar_red.induct, blast)
apply clarify
--- a/src/ZF/Trancl.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Trancl.thy Tue Sep 27 18:02:34 2022 +0100
@@ -196,7 +196,7 @@
(*Transitivity of r^+ is proved by transitivity of r^* *)
lemma trans_trancl: "trans(r^+)"
-apply (unfold trans_def trancl_def)
+ unfolding trans_def trancl_def
apply (blast intro: rtrancl_into_rtrancl
trans_rtrancl [THEN transD, THEN compI])
done
--- a/src/ZF/UNITY/AllocBase.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/AllocBase.thy Tue Sep 27 18:02:34 2022 +0100
@@ -268,7 +268,7 @@
lemma part_ord_Lt [simp]: "part_ord(nat, Lt)"
-apply (unfold part_ord_def Lt_def irrefl_def trans_on_def)
+ unfolding part_ord_def Lt_def irrefl_def trans_on_def
apply (auto intro: lt_trans)
done
--- a/src/ZF/UNITY/ClientImpl.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Tue Sep 27 18:02:34 2022 +0100
@@ -210,7 +210,7 @@
lemma strict_prefix_is_prefix:
"\<langle>xs, ys\<rangle> \<in> strict_prefix(A) \<longleftrightarrow> \<langle>xs, ys\<rangle> \<in> prefix(A) \<and> xs\<noteq>ys"
-apply (unfold strict_prefix_def id_def lam_def)
+ unfolding strict_prefix_def id_def lam_def
apply (auto dest: prefix_type [THEN subsetD])
done
--- a/src/ZF/UNITY/Comp.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Comp.thy Tue Sep 27 18:02:34 2022 +0100
@@ -144,7 +144,7 @@
(*** preserves ***)
lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))"
-apply (unfold preserves_def safety_prop_def)
+ unfolding preserves_def safety_prop_def
apply (auto dest: ActsD simp add: stable_def constrains_def)
apply (drule_tac c = act in subsetD, auto)
done
@@ -157,7 +157,7 @@
lemma preserves_imp_eq:
"\<lbrakk>F \<in> preserves(f); act \<in> Acts(F); \<langle>s,t\<rangle> \<in> act\<rbrakk> \<Longrightarrow> f(s) = f(t)"
-apply (unfold preserves_def stable_def constrains_def)
+ unfolding preserves_def stable_def constrains_def
apply (subgoal_tac "s \<in> state \<and> t \<in> state")
prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force)
done
@@ -224,7 +224,7 @@
lemma preserves_imp_increasing:
"\<lbrakk>F \<in> preserves(f); \<forall>x \<in> state. f(x):A\<rbrakk> \<Longrightarrow> F \<in> Increasing.increasing(A, r, f)"
-apply (unfold Increasing.increasing_def)
+ unfolding Increasing.increasing_def
apply (auto intro: preserves_into_program)
apply (rule_tac P = "\<lambda>x. \<langle>k, x\<rangle>:r" in preserves_imp_stable, auto)
done
@@ -324,7 +324,7 @@
\<forall>k \<in> A. F \<squnion> G \<in> Stable({s \<in> state. P(k, g(s))});
G \<in> preserves(f); \<forall>s \<in> state. f(s):A\<rbrakk>
\<Longrightarrow> F \<squnion> G \<in> Stable({s \<in> state. P(f(s), g(s))})"
-apply (unfold stable_def Stable_def preserves_def)
+ unfolding stable_def Stable_def preserves_def
apply (rule_tac A = "(\<Union>k \<in> A. {s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))})" in Constrains_weaken_L)
prefer 2 apply blast
apply (rule Constrains_UN_left, auto)
--- a/src/ZF/UNITY/Constrains.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Constrains.thy Tue Sep 27 18:02:34 2022 +0100
@@ -103,7 +103,7 @@
(*The set of all reachable states is an invariant...*)
lemma invariant_reachable:
"F \<in> program \<Longrightarrow> F \<in> invariant(reachable(F))"
-apply (unfold invariant_def initially_def)
+ unfolding invariant_def initially_def
apply (blast intro: reachable_type [THEN subsetD] reachable.intros)
done
@@ -239,7 +239,7 @@
lemma stable_imp_Stable:
"F \<in> stable(A) \<Longrightarrow> F \<in> Stable(A)"
-apply (unfold stable_def Stable_def)
+ unfolding stable_def Stable_def
apply (erule constrains_imp_Constrains)
done
@@ -340,7 +340,7 @@
lemma AlwaysI:
"\<lbrakk>Init(F)<=A; F \<in> Stable(A)\<rbrakk> \<Longrightarrow> F \<in> Always(A)"
-apply (unfold Always_def initially_def)
+ unfolding Always_def initially_def
apply (frule Stable_type [THEN subsetD], auto)
done
@@ -360,7 +360,7 @@
lemma invariant_imp_Always:
"F \<in> invariant(A) \<Longrightarrow> F \<in> Always(A)"
-apply (unfold Always_def invariant_def Stable_def stable_def)
+ unfolding Always_def invariant_def Stable_def stable_def
apply (blast intro: constrains_imp_Constrains)
done
--- a/src/ZF/UNITY/FP.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/FP.thy Tue Sep 27 18:02:34 2022 +0100
@@ -51,7 +51,7 @@
apply (subgoal_tac "FP (F) \<inter> B = (\<Union>x\<in>B. FP (F) \<inter> {x}) ")
prefer 2 apply blast
apply (simp (no_asm_simp) add: Int_cons_right)
-apply (unfold FP_def stable_def)
+ unfolding FP_def stable_def
apply (rule constrains_UN)
apply (auto simp add: cons_absorb)
done
--- a/src/ZF/UNITY/Follows.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Follows.thy Tue Sep 27 18:02:34 2022 +0100
@@ -53,7 +53,7 @@
lemma subset_Always_comp:
"\<lbrakk>mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A \<and> g(x):A\<rbrakk> \<Longrightarrow>
Always({x \<in> state. <f(x), g(x)> \<in> r})<=Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
-apply (unfold mono1_def metacomp_def)
+ unfolding mono1_def metacomp_def
apply (auto simp add: Always_eq_includes_reachable)
done
@@ -110,7 +110,7 @@
mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t);
\<forall>x \<in> state. f1(x):A \<and> f(x):A \<and> g(x):B; k \<in> C\<rbrakk> \<Longrightarrow>
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f1(x), g(x))> \<in> t}"
-apply (unfold mono2_def Increasing_def)
+ unfolding mono2_def Increasing_def
apply (rule single_LeadsTo_I, auto)
apply (drule_tac x = "g (sa) " and A = B in bspec)
apply auto
@@ -133,7 +133,7 @@
mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
\<forall>x \<in> state. f(x):A \<and> g1(x):B \<and> g(x):B; k \<in> C\<rbrakk> \<Longrightarrow>
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
-apply (unfold mono2_def Increasing_def)
+ unfolding mono2_def Increasing_def
apply (rule single_LeadsTo_I, auto)
apply (drule_tac x = "f (sa) " and P = "\<lambda>k. F \<in> Stable (X (k))" for X in bspec)
apply auto
@@ -275,7 +275,7 @@
lemma Always_Follows1:
"\<lbrakk>F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);
\<forall>x \<in> state. g(x):A\<rbrakk> \<Longrightarrow> F \<in> Follows(A, r, g, h)"
-apply (unfold Follows_def Increasing_def Stable_def)
+ unfolding Follows_def Increasing_def Stable_def
apply (simp add: INT_iff, auto)
apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}"
and A = "{s \<in> state. <k, h (s)> \<in> r}"
@@ -293,7 +293,7 @@
lemma Always_Follows2:
"\<lbrakk>F \<in> Always({s \<in> state. g(s) = h(s)});
F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A\<rbrakk> \<Longrightarrow> F \<in> Follows(A, r, f, h)"
-apply (unfold Follows_def Increasing_def Stable_def)
+ unfolding Follows_def Increasing_def Stable_def
apply (simp add: INT_iff, auto)
apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }"
and A = "{s \<in> state. <k, g (s) > \<in> r}"
@@ -352,7 +352,7 @@
lemma MultLe_refl1 [simp]:
"\<lbrakk>multiset(M); mset_of(M)<=A\<rbrakk> \<Longrightarrow> \<langle>M, M\<rangle> \<in> MultLe(A, r)"
-apply (unfold MultLe_def id_def lam_def)
+ unfolding MultLe_def id_def lam_def
apply (auto simp add: Mult_iff_multiset)
done
@@ -361,7 +361,7 @@
lemma trans_on_MultLe [simp]: "trans[Mult(A)](MultLe(A,r))"
-apply (unfold MultLe_def trans_on_def)
+ unfolding MultLe_def trans_on_def
apply (auto intro: trancl_trans simp add: multirel_def)
done
@@ -379,7 +379,7 @@
lemma part_order_imp_part_ord:
"part_order(A, r) \<Longrightarrow> part_ord(A, r-id(A))"
-apply (unfold part_order_def part_ord_def)
+ unfolding part_order_def part_ord_def
apply (simp add: refl_def id_def lam_def irrefl_def, auto)
apply (simp (no_asm) add: trans_on_def)
apply auto
@@ -390,7 +390,7 @@
lemma antisym_MultLe [simp]:
"part_order(A, r) \<Longrightarrow> antisym(MultLe(A,r))"
-apply (unfold MultLe_def antisym_def)
+ unfolding MultLe_def antisym_def
apply (drule part_order_imp_part_ord, auto)
apply (drule irrefl_on_multirel)
apply (frule multirel_type [THEN subsetD])
--- a/src/ZF/UNITY/GenPrefix.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Tue Sep 27 18:02:34 2022 +0100
@@ -588,13 +588,13 @@
declare refl_Ge [iff]
lemma antisym_Ge: "antisym(Ge)"
-apply (unfold antisym_def Ge_def)
+ unfolding antisym_def Ge_def
apply (auto intro: le_anti_sym)
done
declare antisym_Ge [iff]
lemma trans_Ge: "trans(Ge)"
-apply (unfold trans_def Ge_def)
+ unfolding trans_def Ge_def
apply (auto intro: le_trans)
done
declare trans_Ge [iff]
@@ -611,7 +611,7 @@
lemma prefix_imp_pfixGe:
"\<langle>xs,ys\<rangle>:prefix(nat) \<Longrightarrow> xs pfixGe ys"
-apply (unfold prefix_def Ge_def)
+ unfolding prefix_def Ge_def
apply (rule gen_prefix_mono [THEN subsetD], auto)
done
(* Added by Sidi \<in> prefix and take *)
--- a/src/ZF/UNITY/Increasing.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Increasing.thy Tue Sep 27 18:02:34 2022 +0100
@@ -48,7 +48,7 @@
lemma increasing_constant [simp]:
"F \<in> increasing[A](r, \<lambda>s. c) \<longleftrightarrow> F \<in> program \<and> c \<in> A"
-apply (unfold increasing_def stable_def)
+ unfolding increasing_def stable_def
apply (subgoal_tac "\<exists>x. x \<in> state")
apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
done
@@ -94,7 +94,7 @@
lemma increasing_imp_Increasing:
"F \<in> increasing[A](r, f) \<Longrightarrow> F \<in> Increasing[A](r, f)"
-apply (unfold increasing_def Increasing_def)
+ unfolding increasing_def Increasing_def
apply (auto intro: stable_imp_Stable)
done
--- a/src/ZF/UNITY/Monotonicity.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy Tue Sep 27 18:02:34 2022 +0100
@@ -109,7 +109,7 @@
lemma mono_munion [iff]:
"mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
-apply (unfold mono2_def MultLe_def)
+ unfolding mono2_def MultLe_def
apply (auto simp add: Mult_iff_multiset)
apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
done
--- a/src/ZF/UNITY/UNITY.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/UNITY.thy Tue Sep 27 18:02:34 2022 +0100
@@ -567,7 +567,7 @@
done
lemma invariantI: "\<lbrakk>Init(F)\<subseteq>A; F \<in> stable(A)\<rbrakk> \<Longrightarrow> F \<in> invariant(A)"
-apply (unfold invariant_def initially_def)
+ unfolding invariant_def initially_def
apply (frule stable_type [THEN subsetD], auto)
done
@@ -583,7 +583,7 @@
\<^term>\<open>invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)\<close>\<close>
lemma invariant_Int:
"\<lbrakk>F \<in> invariant(A); F \<in> invariant(B)\<rbrakk> \<Longrightarrow> F \<in> invariant(A \<inter> B)"
-apply (unfold invariant_def initially_def)
+ unfolding invariant_def initially_def
apply (simp add: stable_Int, blast)
done
--- a/src/ZF/UNITY/Union.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Union.thy Tue Sep 27 18:02:34 2022 +0100
@@ -121,7 +121,7 @@
by auto
lemma Join_SKIP_left [simp]: "SKIP \<squnion> F = programify(F)"
-apply (unfold Join_def SKIP_def)
+ unfolding Join_def SKIP_def
apply (auto simp add: Int_absorb cons_eq)
done
@@ -364,7 +364,7 @@
lemma stable_Join_constrains:
"\<lbrakk>F \<in> stable(A); G \<in> A co A'\<rbrakk>
\<Longrightarrow> F \<squnion> G \<in> A co A'"
-apply (unfold stable_def constrains_def Join_def st_set_def)
+ unfolding stable_def constrains_def Join_def st_set_def
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = G in Acts_type, force)
done
--- a/src/ZF/UNITY/WFair.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/WFair.thy Tue Sep 27 18:02:34 2022 +0100
@@ -165,13 +165,13 @@
lemma leadsToD2:
"F \<in> A \<longmapsto> B \<Longrightarrow> F \<in> program \<and> st_set(A) \<and> st_set(B)"
-apply (unfold leadsTo_def st_set_def)
+ unfolding leadsTo_def st_set_def
apply (blast dest: leads_left leads_right)
done
lemma leadsTo_Basis:
"\<lbrakk>F \<in> A ensures B; st_set(A); st_set(B)\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto> B"
-apply (unfold leadsTo_def st_set_def)
+ unfolding leadsTo_def st_set_def
apply (cut_tac ensures_type)
apply (auto intro: leads.Basis)
done
@@ -204,14 +204,14 @@
lemma leadsTo_Union:
"\<lbrakk>\<And>A. A \<in> S \<Longrightarrow> F \<in> A \<longmapsto> B; F \<in> program; st_set(B)\<rbrakk>
\<Longrightarrow> F \<in> \<Union>(S) \<longmapsto> B"
-apply (unfold leadsTo_def st_set_def)
+ unfolding leadsTo_def st_set_def
apply (blast intro: leads.Union dest: leads_left)
done
lemma leadsTo_Union_Int:
"\<lbrakk>\<And>A. A \<in> S \<Longrightarrow>F \<in> (A \<inter> C) \<longmapsto> B; F \<in> program; st_set(B)\<rbrakk>
\<Longrightarrow> F \<in> (\<Union>(S)Int C)\<longmapsto> B"
-apply (unfold leadsTo_def st_set_def)
+ unfolding leadsTo_def st_set_def
apply (simp only: Int_Union_Union)
apply (blast dest: leads_left intro: leads.Union)
done
@@ -441,7 +441,7 @@
lemma psp_ensures:
"\<lbrakk>F \<in> A ensures A'; F \<in> B co B'\<rbrakk>\<Longrightarrow> F: (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))"
-apply (unfold ensures_def constrains_def st_set_def)
+ unfolding ensures_def constrains_def st_set_def
(*speeds up the proof*)
apply clarify
apply (blast intro: transient_strengthen)
--- a/src/ZF/WF.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/WF.thy Tue Sep 27 18:02:34 2022 +0100
@@ -82,7 +82,7 @@
lemma wf_onI:
assumes prem: "\<And>Z u. \<lbrakk>Z<=A; u \<in> Z; \<forall>x\<in>Z. \<exists>y\<in>Z. \<langle>y,x\<rangle>:r\<rbrakk> \<Longrightarrow> False"
shows "wf[A](r)"
-apply (unfold wf_on_def wf_def)
+ unfolding wf_on_def wf_def
apply (rule equals0I [THEN disjCI, THEN allI])
apply (rule_tac Z = Z in prem, blast+)
done
@@ -287,7 +287,7 @@
apply (rename_tac a1)
apply (rule_tac f = "\<lambda>y\<in>r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
apply typecheck
-apply (unfold is_recfun_def wftrec_def)
+ unfolding is_recfun_def wftrec_def
\<comment> \<open>Applying the substitution: must keep the quantified assumption!\<close>
apply (rule lam_cong [OF refl])
apply (drule underD)
@@ -359,7 +359,7 @@
lemma wfrec_on:
"\<lbrakk>wf[A](r); a \<in> A\<rbrakk> \<Longrightarrow>
wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r-``{a}) \<inter> A. wfrec[A](r,x,H))"
-apply (unfold wf_on_def wfrec_on_def)
+ unfolding wf_on_def wfrec_on_def
apply (erule wfrec [THEN trans])
apply (simp add: vimage_Int_square cons_subset_iff)
done
--- a/src/ZF/ZF_Base.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ZF_Base.thy Tue Sep 27 18:02:34 2022 +0100
@@ -393,7 +393,7 @@
(*Useful for proving A<=B by rewriting in some cases*)
lemma subset_iff:
"A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
-apply (unfold subset_def Ball_def)
+ unfolding subset_def Ball_def
apply (rule iff_refl)
done
--- a/src/ZF/Zorn.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Zorn.thy Tue Sep 27 18:02:34 2022 +0100
@@ -312,7 +312,7 @@
apply (rule ccontr)
apply (frule_tac z=z in chain_extend)
apply (assumption, blast)
-apply (unfold maxchain_def super_def)
+ unfolding maxchain_def super_def
apply (blast elim!: equalityCE)
done
@@ -346,7 +346,7 @@
"next \<in> increasing(S)
\<Longrightarrow> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
apply (rule well_ordI)
-apply (unfold Subset_rel_def linear_def)
+ unfolding Subset_rel_def linear_def
txt\<open>Prove the well-foundedness goal\<close>
apply (rule wf_onI)
apply (frule well_ord_TFin_lemma, assumption)
--- a/src/ZF/ex/CoUnit.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/CoUnit.thy Tue Sep 27 18:02:34 2022 +0100
@@ -37,7 +37,7 @@
apply (rule subsetI)
apply (erule counit.coinduct)
apply (rule subset_refl)
- apply (unfold counit.con_defs)
+ unfolding counit.con_defs
apply fast
done
@@ -60,7 +60,7 @@
by (fast elim!: counit2.free_elims)
lemma Con2_bnd_mono: "bnd_mono(univ(0), \<lambda>x. Con2(x, x))"
- apply (unfold counit2.con_defs)
+ unfolding counit2.con_defs
apply (rule bnd_monoI)
apply (assumption | rule subset_refl QPair_subset_univ QPair_mono)+
done
@@ -79,7 +79,7 @@
apply (tactic "safe_tac (put_claset subset_cs \<^context>)")
apply (erule counit2.cases)
apply (erule counit2.cases)
- apply (unfold counit2.con_defs)
+ unfolding counit2.con_defs
apply (tactic \<open>fast_tac (put_claset subset_cs \<^context>
addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}]
addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1\<close>)
--- a/src/ZF/ex/Commutation.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/Commutation.thy Tue Sep 27 18:02:34 2022 +0100
@@ -52,7 +52,7 @@
(* A special case of square_rtrancl_on *)
lemma diamond_strip:
"diamond(r) \<Longrightarrow> strip(r)"
-apply (unfold diamond_def commute_def strip_def)
+ unfolding diamond_def commute_def strip_def
apply (rule square_rtrancl, simp_all)
done
@@ -74,7 +74,7 @@
by (simp add: confluent_def)
lemma strip_confluent: "strip(r) \<Longrightarrow> confluent(r)"
-apply (unfold strip_def confluent_def diamond_def)
+ unfolding strip_def confluent_def diamond_def
apply (drule commute_rtrancl)
apply (simp_all add: rtrancl_field)
done
@@ -88,7 +88,7 @@
lemma diamond_confluent:
"diamond(r) \<Longrightarrow> confluent(r)"
-apply (unfold diamond_def confluent_def)
+ unfolding diamond_def confluent_def
apply (erule commute_rtrancl, simp)
done
--- a/src/ZF/ex/Group.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/Group.thy Tue Sep 27 18:02:34 2022 +0100
@@ -154,7 +154,7 @@
lemma (in group) inv [simp]:
"x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) \<and> inv x \<cdot> x = \<one> \<and> x \<cdot> inv x = \<one>"
apply (frule inv_ex)
- apply (unfold Bex_def m_inv_def)
+ unfolding Bex_def m_inv_def
apply (erule exE)
apply (rule theI)
apply (rule ex1I, assumption)
--- a/src/ZF/ex/LList.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/LList.thy Tue Sep 27 18:02:34 2022 +0100
@@ -91,7 +91,7 @@
(*** Lemmas to justify using "llist" in other recursive type definitions ***)
lemma llist_mono: "A \<subseteq> B \<Longrightarrow> llist(A) \<subseteq> llist(B)"
-apply (unfold llist.defs )
+ unfolding llist.defs
apply (rule gfp_mono)
apply (rule llist.bnd_mono)
apply (assumption | rule quniv_mono basic_monos)+
@@ -184,7 +184,7 @@
(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
lemma lconst_fun_bnd_mono: "bnd_mono(univ(a), \<lambda>l. LCons(a,l))"
-apply (unfold llist.con_defs )
+ unfolding llist.con_defs
apply (rule bnd_monoI)
apply (blast intro: A_subset_univ QInr_subset_univ)
apply (blast intro: subset_refl QInr_mono QPair_mono)
--- a/src/ZF/ex/Ramsey.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/Ramsey.thy Tue Sep 27 18:02:34 2022 +0100
@@ -79,7 +79,7 @@
lemma Atleast_succI:
"\<lbrakk>Atleast(m,B); b\<notin> B\<rbrakk> \<Longrightarrow> Atleast(succ(m), cons(b,B))"
-apply (unfold Atleast_def succ_def)
+ unfolding Atleast_def succ_def
apply (blast intro: inj_extend elim: mem_irrefl)
done
@@ -148,7 +148,7 @@
"\<lbrakk>Indept(I, {z \<in> V-{a}. \<langle>a,z\<rangle> \<notin> E}, E); Symmetric(E); a \<in> V;
Atleast(j,I)\<rbrakk> \<Longrightarrow>
Indept(cons(a,I), V, E) \<and> Atleast(succ(j), cons(a,I))"
-apply (unfold Symmetric_def Indept_def)
+ unfolding Symmetric_def Indept_def
apply (blast intro!: Atleast_succI)
done
@@ -157,7 +157,7 @@
"\<lbrakk>Clique(C, {z \<in> V-{a}. \<langle>a,z\<rangle>:E}, E); Symmetric(E); a \<in> V;
Atleast(j,C)\<rbrakk> \<Longrightarrow>
Clique(cons(a,C), V, E) \<and> Atleast(succ(j), cons(a,C))"
-apply (unfold Symmetric_def Clique_def)
+ unfolding Symmetric_def Clique_def
apply (blast intro!: Atleast_succI)
done
--- a/src/ZF/func.thy Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/func.thy Tue Sep 27 18:02:34 2022 +0100
@@ -318,7 +318,7 @@
by (simp add: restrict_def relation_def, blast)
lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A \<inter> C"
-apply (unfold restrict_def lam_def)
+ unfolding restrict_def lam_def
apply (rule equalityI)
apply (auto simp add: domain_iff)
done