--- a/src/HOL/Library/Cardinality.thy Sun Oct 27 20:11:08 2024 +0100
+++ b/src/HOL/Library/Cardinality.thy Sun Oct 27 22:35:02 2024 +0100
@@ -74,8 +74,9 @@
lemma card_fun: "CARD('a \<Rightarrow> 'b) = (if CARD('a) \<noteq> 0 \<and> CARD('b) \<noteq> 0 \<or> CARD('b) = 1 then CARD('b) ^ CARD('a) else 0)"
proof -
- { assume "0 < CARD('a)" and "0 < CARD('b)"
- hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
+ have "CARD('a \<Rightarrow> 'b) = CARD('b) ^ CARD('a)" if "0 < CARD('a)" and "0 < CARD('b)"
+ proof -
+ from that have fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
by(simp_all only: card_ge_0_finite)
from finite_distinct_list[OF finb] obtain bs
where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
@@ -113,19 +114,23 @@
qed
hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
- ultimately have "CARD('a \<Rightarrow> 'b) = CARD('b) ^ CARD('a)" using cb ca by simp }
- moreover {
- assume cb: "CARD('b) = 1"
- then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
+ ultimately show ?thesis using cb ca by simp
+ qed
+ moreover have "CARD('a \<Rightarrow> 'b) = 1" if "CARD('b) = 1"
+ proof -
+ from that obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
proof(rule UNIV_eq_I)
fix x :: "'a \<Rightarrow> 'b"
- { fix y
+ have "x y = b" for y
+ proof -
have "x y \<in> UNIV" ..
- hence "x y = b" unfolding b by simp }
+ thus ?thesis unfolding b by simp
+ qed
thus "x \<in> {\<lambda>x. b}" by(auto)
qed
- have "CARD('a \<Rightarrow> 'b) = 1" unfolding eq by simp }
+ show ?thesis unfolding eq by simp
+ qed
ultimately show ?thesis
by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
qed
--- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Oct 27 20:11:08 2024 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Sun Oct 27 22:35:02 2024 +0100
@@ -4,8 +4,8 @@
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
-theory Complete_Partial_Order2 imports
- Main
+theory Complete_Partial_Order2
+ imports Main
begin
unbundle lattice_syntax
@@ -604,7 +604,7 @@
and mcont: "\<And>f. mcont lub (\<sqsubseteq>) Sup (\<le>) f \<Longrightarrow> mcont lub (\<sqsubseteq>) Sup (\<le>) (F f)"
shows "mcont lub (\<sqsubseteq>) Sup (\<le>) (ccpo.fixp (fun_lub Sup) (fun_ord (\<le>)) F)"
(is "mcont _ _ _ _ ?fixp")
-unfolding mcont_def
+ unfolding mcont_def
proof(intro conjI monotoneI contI)
have mono: "monotone (fun_ord (\<le>)) (fun_ord (\<le>)) F"
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
@@ -612,36 +612,33 @@
have chain: "\<And>x. Complete_Partial_Order.chain (\<le>) ((\<lambda>f. f x) ` ?iter)"
by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
- {
- fix x y
- assume "x \<sqsubseteq> y"
- show "?fixp x \<le> ?fixp y"
- apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
- using chain
- proof(rule ccpo_Sup_least)
- fix x'
- assume "x' \<in> (\<lambda>f. f x) ` ?iter"
- then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
- also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
- by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
- also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
- by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
- finally show "x' \<le> \<dots>" .
- qed
- next
- fix Y
- assume chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
- and Y: "Y \<noteq> {}"
- { fix f
- assume "f \<in> ?iter"
- hence "f (\<Or>Y) = \<Squnion>(f ` Y)"
- using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) }
+ show "?fixp x \<le> ?fixp y" if "x \<sqsubseteq> y" for x y
+ apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
+ using chain
+ proof(rule ccpo_Sup_least)
+ fix x'
+ assume "x' \<in> (\<lambda>f. f x) ` ?iter"
+ then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
+ also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
+ by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
+ also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
+ finally show "x' \<le> \<dots>" .
+ qed
+
+ show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)"
+ if chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y" and Y: "Y \<noteq> {}" for Y
+ proof -
+ have "f (\<Or>Y) = \<Squnion>(f ` Y)" if "f \<in> ?iter" for f
+ using that mcont chain Y
+ by (rule mcont_contD[OF iterates_mcont])
moreover have "\<Squnion>((\<lambda>f. \<Squnion>(f ` Y)) ` ?iter) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` ?iter)) ` Y)"
using chain ccpo.chain_iterates[OF ccpo_fun mono]
- by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
- ultimately show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun]
- by(simp add: fun_lub_apply cong: image_cong)
- }
+ by (rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
+ ultimately show ?thesis
+ unfolding ccpo.fixp_def[OF ccpo_fun]
+ by (simp add: fun_lub_apply cong: image_cong)
+ qed
qed
end
@@ -1753,12 +1750,14 @@
from A obtain z where "z \<in> A" by blast
with * have z: "\<not> flat_ord x y z" ..
hence y: "x \<noteq> y" "y \<noteq> z" by(auto simp add: flat_ord_def)
- { assume "\<not> A \<subseteq> {x}"
- then obtain z' where "z' \<in> A" "z' \<noteq> x" by auto
+ have "y \<noteq> (THE z. z \<in> A - {x})" if "\<not> A \<subseteq> {x}"
+ proof -
+ from that obtain z' where "z' \<in> A" "z' \<noteq> x" by auto
then have "(THE z. z \<in> A - {x}) = z'"
by(intro the_equality)(auto dest: chainD[OF chain] simp add: flat_ord_def)
moreover have "z' \<noteq> y" using \<open>z' \<in> A\<close> * by(auto simp add: flat_ord_def)
- ultimately have "y \<noteq> (THE z. z \<in> A - {x})" by simp }
+ ultimately show ?thesis by simp
+ qed
with z show "\<not> flat_ord x y (flat_lub x A)" by(simp add: flat_ord_def flat_lub_def)
qed