--- a/src/ZF/AC/HH.thy Wed Sep 28 11:00:13 2022 +0200
+++ b/src/ZF/AC/HH.thy Wed Sep 28 11:23:49 2022 +0100
@@ -126,7 +126,7 @@
apply (erule_tac [2] ltI [OF _ Ord_Least], assumption)
done
-subsection\<open>Lemmas used in the proofs of AC1 \<Longrightarrow> WO2 and AC17 \<Longrightarrow> AC1\<close>
+subsection\<open>Lemmas used in the proofs of @{term "AC1 \<Longrightarrow> WO2"} and @{term "AC17 \<Longrightarrow> AC1"}\<close>
lemma lam_Least_HH_inj_Pow:
"(\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))
@@ -213,7 +213,7 @@
lam_sing_bij [THEN bij_converse_bij]]
-subsection\<open>The proof of AC1 \<Longrightarrow> WO2\<close>
+subsection\<open>The proof of @{term "AC1 \<Longrightarrow> WO2"}\<close>
(*Establishing the existence of a bijection, namely
converse
@@ -236,10 +236,9 @@
lemma AC1_WO2: "AC1 \<Longrightarrow> WO2"
unfolding AC1_def WO2_def eqpoll_def
-apply (intro allI)
-apply (drule_tac x = "Pow(A) - {0}" in spec)
-apply (blast dest: bijection)
-done
+ apply (intro allI)
+ apply (drule_tac x = "Pow(A) - {0}" in spec)
+ apply (blast dest: bijection)
+ done
end
-
--- a/src/ZF/Constructible/AC_in_L.thy Wed Sep 28 11:00:13 2022 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy Wed Sep 28 11:23:49 2022 +0100
@@ -453,7 +453,7 @@
text\<open>Every constructible set is well-ordered! Therefore the Wellordering Theorem and
- the Axiom of Choice hold in \<^term>\<open>L\<close>\<And>\<close>
+ the Axiom of Choice hold in \<^term>\<open>L\<close>!\<close>
theorem L_implies_AC: assumes x: "L(x)" shows "\<exists>r. well_ord(x,r)"
using Transset_Lset x
apply (simp add: Transset_def L_def)
--- a/src/ZF/Constructible/DPow_absolute.thy Wed Sep 28 11:00:13 2022 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy Wed Sep 28 11:23:49 2022 +0100
@@ -13,7 +13,7 @@
subsubsection\<open>The Operator \<^term>\<open>is_formula_rec\<close>\<close>
text\<open>The three arguments of \<^term>\<open>p\<close> are always 2, 1, 0. It is buried
- within 11 quantifiers\<And>\<close>
+ within 11 quantifiers!\<close>
(* is_formula_rec :: "[i\<Rightarrow>o, [i,i,i]\<Rightarrow>o, i, i] \<Rightarrow> o"
"is_formula_rec(M,MH,p,z) \<equiv>
@@ -595,15 +595,10 @@
subsubsection\<open>Actually Instantiating \<open>M_Lset\<close>\<close>
lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
- apply (rule M_Lset_axioms.intro)
- apply (assumption | rule strong_rep transrec_rep)+
- done
+ by (blast intro: M_Lset_axioms.intro strong_rep transrec_rep)
theorem M_Lset_L: "M_Lset(L)"
- apply (rule M_Lset.intro)
- apply (rule M_DPow_L)
- apply (rule M_Lset_axioms_L)
- done
+ by (blast intro: M_Lset.intro M_DPow_L M_Lset_axioms_L)
text\<open>Finally: the point of the whole theory!\<close>
lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
@@ -619,9 +614,12 @@
theorem V_equals_L_in_L:
"L(x) \<longleftrightarrow> constructible(L,x)"
-apply (simp add: constructible_def Lset_abs Lset_closed)
-apply (simp add: L_def)
-apply (blast intro: Ord_in_L)
-done
+proof -
+ have "L(x) \<longleftrightarrow> (\<exists>i[L]. Ord(i) \<and> x \<in> Lset(i))"
+ by (auto simp add: L_def intro: Ord_in_L)
+ moreover have "\<dots> \<longleftrightarrow> constructible(L,x)"
+ by (simp add: constructible_def Lset_abs Lset_closed)
+ ultimately show ?thesis by blast
+qed
end