--- a/src/ZF/Constructible/AC_in_L.thy Fri Oct 18 11:32:10 2024 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy Fri Oct 18 11:44:05 2024 +0200
@@ -46,28 +46,24 @@
lemma linear_rlist:
assumes r: "linear(A,r)" shows "linear(list(A),rlist(A,r))"
proof -
- { fix xs ys
- have "xs \<in> list(A) \<Longrightarrow> ys \<in> list(A) \<Longrightarrow> \<langle>xs,ys\<rangle> \<in> rlist(A,r) \<or> xs = ys \<or> \<langle>ys,xs\<rangle> \<in> rlist(A, r) "
- proof (induct xs arbitrary: ys rule: list.induct)
- case Nil
- thus ?case by (induct ys rule: list.induct) (auto simp add: shorterI)
- next
- case (Cons x xs)
- { fix y ys
- assume "y \<in> A" and "ys \<in> list(A)"
- with Cons
- have "\<langle>Cons(x,xs),Cons(y,ys)\<rangle> \<in> rlist(A,r) \<or> x=y \<and> xs = ys \<or> \<langle>Cons(y,ys), Cons(x,xs)\<rangle> \<in> rlist(A,r)"
- apply (rule_tac i = "length(xs)" and j = "length(ys)" in Ord_linear_lt)
- apply (simp_all add: shorterI)
- apply (rule linearE [OF r, of x y])
- apply (auto simp add: diffI intro: sameI)
- done
- }
- note yConsCase = this
- show ?case using \<open>ys \<in> list(A)\<close>
- by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase)
- qed
- }
+ have "xs \<in> list(A) \<Longrightarrow> ys \<in> list(A) \<Longrightarrow> \<langle>xs,ys\<rangle> \<in> rlist(A,r) \<or> xs = ys \<or> \<langle>ys,xs\<rangle> \<in> rlist(A, r)"
+ for xs ys
+ proof (induct xs arbitrary: ys rule: list.induct)
+ case Nil
+ thus ?case by (induct ys rule: list.induct) (auto simp add: shorterI)
+ next
+ case (Cons x xs)
+ then have yConsCase: "\<langle>Cons(x,xs),Cons(y,ys)\<rangle> \<in> rlist(A,r) \<or> x=y \<and> xs = ys \<or> \<langle>Cons(y,ys), Cons(x,xs)\<rangle> \<in> rlist(A,r)"
+ if "y \<in> A" and "ys \<in> list(A)" for y ys
+ using that
+ apply (rule_tac i = "length(xs)" and j = "length(ys)" in Ord_linear_lt)
+ apply (simp_all add: shorterI)
+ apply (rule linearE [OF r, of x y])
+ apply (auto simp add: diffI intro: sameI)
+ done
+ from \<open>ys \<in> list(A)\<close> show ?case
+ by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase)
+ qed
thus ?thesis by (simp add: linear_def)
qed
--- a/src/ZF/Constructible/Normal.thy Fri Oct 18 11:32:10 2024 +0200
+++ b/src/ZF/Constructible/Normal.thy Fri Oct 18 11:44:05 2024 +0200
@@ -409,27 +409,26 @@
assumes ab: "a < b" and F: "\<And>x. Ord(x) \<Longrightarrow> Ord(F(x))"
shows "normalize(F,a) < normalize(F,b)"
proof -
- { fix x
- have "Ord(b)" using ab by (blast intro: lt_Ord2)
- hence "x < b \<Longrightarrow> normalize(F,x) < normalize(F,b)"
- proof (induct b arbitrary: x rule: trans_induct3)
- case 0 thus ?case by simp
- next
- case (succ b)
- thus ?case
- by (auto simp add: le_iff def_transrec2 [OF normalize_def] intro: Un_upper2_lt F)
- next
- case (limit l)
- hence sc: "succ(x) < l"
- by (blast intro: Limit_has_succ)
- hence "normalize(F,x) < normalize(F,succ(x))"
- by (blast intro: limit elim: ltE)
- hence "normalize(F,x) < (\<Union>j<l. normalize(F,j))"
- by (blast intro: OUN_upper_lt lt_Ord F sc)
- thus ?case using limit
- by (simp add: def_transrec2 [OF normalize_def])
- qed
- } thus ?thesis using ab .
+ have "Ord(b)" using ab by (blast intro: lt_Ord2)
+ hence "x < b \<Longrightarrow> normalize(F,x) < normalize(F,b)" for x
+ proof (induct b arbitrary: x rule: trans_induct3)
+ case 0 thus ?case by simp
+ next
+ case (succ b)
+ thus ?case
+ by (auto simp add: le_iff def_transrec2 [OF normalize_def] intro: Un_upper2_lt F)
+ next
+ case (limit l)
+ hence sc: "succ(x) < l"
+ by (blast intro: Limit_has_succ)
+ hence "normalize(F,x) < normalize(F,succ(x))"
+ by (blast intro: limit elim: ltE)
+ hence "normalize(F,x) < (\<Union>j<l. normalize(F,j))"
+ by (blast intro: OUN_upper_lt lt_Ord F sc)
+ thus ?case using limit
+ by (simp add: def_transrec2 [OF normalize_def])
+ qed
+ thus ?thesis using ab .
qed
theorem Normal_normalize:
@@ -464,7 +463,7 @@
definition
Aleph :: "i \<Rightarrow> i" (\<open>(\<open>open_block notation=\<open>prefix \<aleph>\<close>\<close>\<aleph>_)\<close> [90] 90) where
- "Aleph(a) \<equiv> transrec2(a, nat, \<lambda>x r. csucc(r))"
+ "\<aleph>a \<equiv> transrec2(a, nat, \<lambda>x r. csucc(r))"
lemma Card_Aleph [simp, intro]:
"Ord(a) \<Longrightarrow> Card(Aleph(a))"
@@ -476,33 +475,32 @@
lemma Aleph_increasing:
assumes ab: "a < b" shows "Aleph(a) < Aleph(b)"
proof -
- { fix x
- have "Ord(b)" using ab by (blast intro: lt_Ord2)
- hence "x < b \<Longrightarrow> Aleph(x) < Aleph(b)"
- proof (induct b arbitrary: x rule: trans_induct3)
- case 0 thus ?case by simp
- next
- case (succ b)
- thus ?case
- by (force simp add: le_iff def_transrec2 [OF Aleph_def]
- intro: lt_trans lt_csucc Card_is_Ord)
- next
- case (limit l)
- hence sc: "succ(x) < l"
- by (blast intro: Limit_has_succ)
- hence "\<aleph> x < (\<Union>j<l. \<aleph>j)" using limit
- by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord)
- thus ?case using limit
- by (simp add: def_transrec2 [OF Aleph_def])
- qed
- } thus ?thesis using ab .
+ have "Ord(b)" using ab by (blast intro: lt_Ord2)
+ hence "x < b \<Longrightarrow> Aleph(x) < Aleph(b)" for x
+ proof (induct b arbitrary: x rule: trans_induct3)
+ case 0 thus ?case by simp
+ next
+ case (succ b)
+ thus ?case
+ by (force simp add: le_iff def_transrec2 [OF Aleph_def]
+ intro: lt_trans lt_csucc Card_is_Ord)
+ next
+ case (limit l)
+ hence sc: "succ(x) < l"
+ by (blast intro: Limit_has_succ)
+ hence "\<aleph>x < (\<Union>j<l. \<aleph>j)" using limit
+ by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord)
+ thus ?case using limit
+ by (simp add: def_transrec2 [OF Aleph_def])
+ qed
+ thus ?thesis using ab .
qed
theorem Normal_Aleph: "Normal(Aleph)"
proof (rule NormalI)
- show "\<And>i j. i < j \<Longrightarrow> \<aleph>i < \<aleph>j"
+ show "i < j \<Longrightarrow> \<aleph>i < \<aleph>j" for i j
by (blast intro!: Aleph_increasing)
- show "\<And>l. Limit(l) \<Longrightarrow> \<aleph>l = (\<Union>i<l. \<aleph>i)"
+ show "Limit(l) \<Longrightarrow> \<aleph>l = (\<Union>i<l. \<aleph>i)" for l
by (simp add: def_transrec2 [OF Aleph_def])
qed