--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Jan 12 17:12:36 2023 +0000
@@ -8,15 +8,15 @@
section \<open>Cardinal Arithmetic\<close>
theory Cardinal_Arithmetic
-imports Cardinal_Order_Relation
+ imports Cardinal_Order_Relation
begin
subsection \<open>Binary sum\<close>
lemma csum_Cnotzero2:
"Cnotzero r2 \<Longrightarrow> Cnotzero (r1 +c r2)"
-unfolding csum_def
-by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE)
+ unfolding csum_def
+ by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE)
lemma single_cone:
"|{x}| =o cone"
@@ -27,10 +27,10 @@
qed
lemma cone_Cnotzero: "Cnotzero cone"
-by (simp add: cone_not_czero Card_order_cone)
+ by (simp add: cone_not_czero Card_order_cone)
lemma cone_ordLeq_ctwo: "cone \<le>o ctwo"
-unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto
+ unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto
lemma csum_czero1: "Card_order r \<Longrightarrow> r +c czero =o r"
unfolding czero_def csum_def Field_card_of
@@ -44,7 +44,7 @@
subsection \<open>Product\<close>
lemma Times_cprod: "|A \<times> B| =o |A| *c |B|"
-by (simp only: cprod_def Field_card_of card_of_refl)
+ by (simp only: cprod_def Field_card_of card_of_refl)
lemma card_of_Times_singleton:
fixes A :: "'a set"
@@ -64,21 +64,20 @@
lemma cprod_cone: "Card_order r \<Longrightarrow> r *c cone =o r"
unfolding cprod_def cone_def Field_card_of
- by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])
-
+ by (metis (no_types) card_of_Field_ordIso card_of_Times_singleton ordIso_transitive)
lemma ordLeq_cprod1: "\<lbrakk>Card_order p1; Cnotzero p2\<rbrakk> \<Longrightarrow> p1 \<le>o p1 *c p2"
-unfolding cprod_def by (metis Card_order_Times1 czeroI)
+ unfolding cprod_def by (metis Card_order_Times1 czeroI)
subsection \<open>Exponentiation\<close>
lemma cexp_czero: "r ^c czero =o cone"
-unfolding cexp_def czero_def Field_card_of Func_empty by (rule single_cone)
+ unfolding cexp_def czero_def Field_card_of Func_empty by (rule single_cone)
lemma Pow_cexp_ctwo:
"|Pow A| =o ctwo ^c |A|"
-unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
+ by (simp add: card_of_Pow_Func cexp_def ctwo_def)
lemma Cnotzero_cexp:
assumes "Cnotzero q"
@@ -92,29 +91,24 @@
lemma Cinfinite_ctwo_cexp:
"Cinfinite r \<Longrightarrow> Cinfinite (ctwo ^c r)"
-unfolding ctwo_def cexp_def cinfinite_def Field_card_of
-by (rule conjI, rule infinite_Func, auto)
+ unfolding ctwo_def cexp_def cinfinite_def Field_card_of
+ by (rule conjI, rule infinite_Func, auto)
lemma cone_ordLeq_iff_Field:
assumes "cone \<le>o r"
shows "Field r \<noteq> {}"
-proof (rule ccontr)
- assume "\<not> Field r \<noteq> {}"
- hence "Field r = {}" by simp
- thus False using card_of_empty3
- card_of_mono2[OF assms] Cnotzero_imp_not_empty[OF cone_Cnotzero] by auto
-qed
+ by (metis assms card_of_empty3 card_of_mono2 cone_Cnotzero czeroI)
lemma cone_ordLeq_cexp: "cone \<le>o r1 \<Longrightarrow> cone \<le>o r1 ^c r2"
-by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field)
+ by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field)
lemma Card_order_czero: "Card_order czero"
-by (simp only: card_of_Card_order czero_def)
+ by (simp only: card_of_Card_order czero_def)
lemma cexp_mono2'':
assumes 2: "p2 \<le>o r2"
- and n1: "Cnotzero q"
- and n2: "Card_order p2"
+ and n1: "Cnotzero q"
+ and n2: "Card_order p2"
shows "q ^c p2 \<le>o q ^c r2"
proof (cases "p2 =o (czero :: 'a rel)")
case True
@@ -129,28 +123,20 @@
lemma csum_cexp: "\<lbrakk>Cinfinite r1; Cinfinite r2; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow>
q ^c r1 +c q ^c r2 \<le>o q ^c (r1 +c r2)"
apply (rule csum_cinfinite_bound)
- apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum1)
- apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum2)
+ apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum1)
+ apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum2)
by (simp_all add: Card_order_cexp Cinfinite_csum1 Cinfinite_cexp cinfinite_cexp)
lemma csum_cexp': "\<lbrakk>Cinfinite r; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow> q +c r \<le>o q ^c r"
-apply (rule csum_cinfinite_bound)
- apply (metis Cinfinite_Cnotzero ordLeq_cexp1)
- apply (metis ordLeq_cexp2)
- apply blast+
-by (metis Cinfinite_cexp)
+ apply (rule csum_cinfinite_bound)
+ apply (metis Cinfinite_Cnotzero ordLeq_cexp1)
+ apply (metis ordLeq_cexp2)
+ apply blast+
+ by (metis Cinfinite_cexp)
lemma card_of_Sigma_ordLeq_Cinfinite:
"\<lbrakk>Cinfinite r; |I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r\<rbrakk> \<Longrightarrow> |SIGMA i : I. A i| \<le>o r"
-unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)
-
-lemma card_order_cexp:
- assumes "card_order r1" "card_order r2"
- shows "card_order (r1 ^c r2)"
-proof -
- have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto
- thus ?thesis unfolding cexp_def Func_def by simp
-qed
+ unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)
lemma Cinfinite_ordLess_cexp:
assumes r: "Cinfinite r"
@@ -165,19 +151,19 @@
lemma infinite_ordLeq_cexp:
assumes "Cinfinite r"
shows "r \<le>o r ^c r"
-by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])
+ by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])
lemma czero_cexp: "Cnotzero r \<Longrightarrow> czero ^c r =o czero"
- by (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso)
+ by (metis Cnotzero_imp_not_empty cexp_def czero_def card_of_empty_ordIso Field_card_of Func_is_emp)
lemma Func_singleton:
-fixes x :: 'b and A :: "'a set"
-shows "|Func A {x}| =o |{x}|"
+ fixes x :: 'b and A :: "'a set"
+ shows "|Func A {x}| =o |{x}|"
proof (rule ordIso_symmetric)
define f where [abs_def]: "f y a = (if y = x \<and> a \<in> A then x else undefined)" for y a
have "Func A {x} \<subseteq> f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff)
- hence "bij_betw f {x} (Func A {x})" unfolding bij_betw_def inj_on_def f_def Func_def
- by (auto split: if_split_asm)
+ hence "bij_betw f {x} (Func A {x})"
+ unfolding bij_betw_def inj_on_def f_def Func_def by (auto split: if_split_asm)
thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast
qed
@@ -225,32 +211,32 @@
definition cpow where "cpow r = |Pow (Field r)|"
lemma card_order_cpow: "card_order r \<Longrightarrow> card_order (cpow r)"
-by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on)
+ by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on)
lemma cpow_greater_eq: "Card_order r \<Longrightarrow> r \<le>o cpow r"
-by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow)
+ by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow)
lemma Cinfinite_cpow: "Cinfinite r \<Longrightarrow> Cinfinite (cpow r)"
-unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow)
+ unfolding cpow_def cinfinite_def by simp
lemma Card_order_cpow: "Card_order (cpow r)"
-unfolding cpow_def by (rule card_of_Card_order)
+ unfolding cpow_def by (rule card_of_Card_order)
lemma cardSuc_ordLeq_cpow: "Card_order r \<Longrightarrow> cardSuc r \<le>o cpow r"
-unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order)
+ unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order)
lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
-unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
+ unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
subsection \<open>Inverse image\<close>
lemma vimage_ordLeq:
-assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k"
-shows "|vimage f A| \<le>o k"
+ assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k"
+ shows "|vimage f A| \<le>o k"
proof-
have "vimage f A = (\<Union>a \<in> A. vimage f {a})" by auto
also have "|\<Union>a \<in> A. vimage f {a}| \<le>o k"
- using UNION_Cinfinite_bound[OF assms] .
+ using UNION_Cinfinite_bound[OF assms] .
finally show ?thesis .
qed
@@ -268,7 +254,8 @@
lemma cmax1:
assumes "Card_order r" "Card_order s" "s \<le>o r"
shows "cmax r s =o r"
-unfolding cmax_def proof (split if_splits, intro conjI impI)
+ unfolding cmax_def
+proof (split if_splits, intro conjI impI)
assume "cinfinite r \<or> cinfinite s"
hence Cinf: "Cinfinite r" using assms(1,3) by (metis cinfinite_mono)
have "czero +c r +c s =o r +c s" by (rule csum_czero2[OF Card_order_csum])
@@ -299,33 +286,14 @@
shows "cmax r s =o s"
by (metis assms cmax1 cmax_com ordIso_transitive)
-lemma csum_absorb2: "Cinfinite r2 \<Longrightarrow> r1 \<le>o r2 \<Longrightarrow> r1 +c r2 =o r2"
- by (metis csum_absorb2')
-
-lemma cprod_infinite2': "\<lbrakk>Cnotzero r1; Cinfinite r2; r1 \<le>o r2\<rbrakk> \<Longrightarrow> r1 *c r2 =o r2"
- unfolding ordIso_iff_ordLeq
- by (intro conjI cprod_cinfinite_bound ordLeq_cprod2 ordLeq_refl)
- (auto dest!: ordIso_imp_ordLeq not_ordLeq_ordLess simp: czero_def Card_order_empty)
-
context
fixes r s
assumes r: "Cinfinite r"
- and s: "Cinfinite s"
+ and s: "Cinfinite s"
begin
lemma cmax_csum: "cmax r s =o r +c s"
-proof (cases "r \<le>o s")
- case True
- hence "cmax r s =o s" by (metis cmax2 r s)
- also have "s =o r +c s" by (metis True csum_absorb2 ordIso_symmetric s)
- finally show ?thesis .
-next
- case False
- hence "s \<le>o r" by (metis ordLeq_total r s card_order_on_def)
- hence "cmax r s =o r" by (metis cmax1 r s)
- also have "r =o r +c s" by (metis \<open>s \<le>o r\<close> csum_absorb1 ordIso_symmetric r)
- finally show ?thesis .
-qed
+ by (simp add: Card_order_csum cmax_def csum_czero2 r)
lemma cmax_cprod: "cmax r s =o r *c s"
proof (cases "r \<le>o s")
@@ -344,39 +312,21 @@
end
lemma Card_order_cmax:
-assumes r: "Card_order r" and s: "Card_order s"
-shows "Card_order (cmax r s)"
-unfolding cmax_def by (auto simp: Card_order_csum)
+ assumes r: "Card_order r" and s: "Card_order s"
+ shows "Card_order (cmax r s)"
+ unfolding cmax_def by (auto simp: Card_order_csum)
lemma ordLeq_cmax:
-assumes r: "Card_order r" and s: "Card_order s"
-shows "r \<le>o cmax r s \<and> s \<le>o cmax r s"
-proof-
- {assume "r \<le>o s"
- hence ?thesis by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
- }
- moreover
- {assume "s \<le>o r"
- hence ?thesis using cmax_com by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
- }
- ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
-qed
+ assumes r: "Card_order r" and s: "Card_order s"
+ shows "r \<le>o cmax r s \<and> s \<le>o cmax r s"
+ by (meson card_order_on_def cmax1 cmax2 ordIso_iff_ordLeq ordLeq_total ordLeq_transitive r s)
lemmas ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and
- ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2]
+ ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2]
lemma finite_cmax:
-assumes r: "Card_order r" and s: "Card_order s"
-shows "finite (Field (cmax r s)) \<longleftrightarrow> finite (Field r) \<and> finite (Field s)"
-proof-
- {assume "r \<le>o s"
- hence ?thesis by (metis cmax2 ordIso_finite_Field ordLeq_finite_Field r s)
- }
- moreover
- {assume "s \<le>o r"
- hence ?thesis by (metis cmax1 ordIso_finite_Field ordLeq_finite_Field r s)
- }
- ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
-qed
+ assumes r: "Card_order r" and s: "Card_order s"
+ shows "finite (Field (cmax r s)) \<longleftrightarrow> finite (Field r) \<and> finite (Field s)"
+ by (meson card_order_on_def cmax1 cmax2 ordIso_finite_Field ordLeq_finite_Field ordLeq_total r s)
end
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 12 17:12:36 2023 +0000
@@ -8,7 +8,7 @@
section \<open>Cardinal-Order Relations\<close>
theory Cardinal_Order_Relation
-imports Wellorder_Constructions
+ imports Wellorder_Constructions
begin
declare
@@ -72,46 +72,36 @@
subsection \<open>Cardinal of a set\<close>
lemma card_of_inj_rel: assumes INJ: "\<And>x y y'. \<lbrakk>(x,y) \<in> R; (x,y') \<in> R\<rbrakk> \<Longrightarrow> y = y'"
-shows "|{y. \<exists>x. (x,y) \<in> R}| <=o |{x. \<exists>y. (x,y) \<in> R}|"
+ shows "|{y. \<exists>x. (x,y) \<in> R}| <=o |{x. \<exists>y. (x,y) \<in> R}|"
proof-
let ?Y = "{y. \<exists>x. (x,y) \<in> R}" let ?X = "{x. \<exists>y. (x,y) \<in> R}"
let ?f = "\<lambda>y. SOME x. (x,y) \<in> R"
have "?f ` ?Y <= ?X" by (auto dest: someI)
moreover have "inj_on ?f ?Y"
- unfolding inj_on_def proof(auto)
- fix y1 x1 y2 x2
- assume *: "(x1, y1) \<in> R" "(x2, y2) \<in> R" and **: "?f y1 = ?f y2"
- hence "(?f y1,y1) \<in> R" using someI[of "\<lambda>x. (x,y1) \<in> R"] by auto
- moreover have "(?f y2,y2) \<in> R" using * someI[of "\<lambda>x. (x,y2) \<in> R"] by auto
- ultimately show "y1 = y2" using ** INJ by auto
- qed
+ by (metis (mono_tags, lifting) assms inj_onI mem_Collect_eq)
ultimately show "|?Y| <=o |?X|" using card_of_ordLeq by blast
qed
lemma card_of_unique2: "\<lbrakk>card_order_on B r; bij_betw f A B\<rbrakk> \<Longrightarrow> r =o |A|"
-using card_of_ordIso card_of_unique ordIso_equivalence by blast
+ using card_of_ordIso card_of_unique ordIso_equivalence by blast
lemma internalize_card_of_ordLess2:
-"( |A| <o |C| ) = (\<exists>B < C. |A| =o |B| \<and> |B| <o |C| )"
-using internalize_card_of_ordLess[of "A" "|C|"] Field_card_of[of C] by auto
+ "( |A| <o |C| ) = (\<exists>B < C. |A| =o |B| \<and> |B| <o |C| )"
+ using internalize_card_of_ordLess[of "A" "|C|"] Field_card_of[of C] by auto
lemma Card_order_omax:
-assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Card_order r"
-shows "Card_order (omax R)"
-proof-
- have "\<forall>r\<in>R. Well_order r"
- using assms unfolding card_order_on_def by simp
- thus ?thesis using assms apply - apply(drule omax_in) by auto
-qed
+ assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Card_order r"
+ shows "Card_order (omax R)"
+ by (simp add: assms omax_in)
lemma Card_order_omax2:
-assumes "finite I" and "I \<noteq> {}"
-shows "Card_order (omax {|A i| | i. i \<in> I})"
+ assumes "finite I" and "I \<noteq> {}"
+ shows "Card_order (omax {|A i| | i. i \<in> I})"
proof-
let ?R = "{|A i| | i. i \<in> I}"
have "finite ?R" and "?R \<noteq> {}" using assms by auto
moreover have "\<forall>r\<in>?R. Card_order r"
- using card_of_Card_order by auto
+ using card_of_Card_order by auto
ultimately show ?thesis by(rule Card_order_omax)
qed
@@ -119,138 +109,104 @@
subsection \<open>Cardinals versus set operations on arbitrary sets\<close>
lemma card_of_set_type[simp]: "|UNIV::'a set| <o |UNIV::'a set set|"
-using card_of_Pow[of "UNIV::'a set"] by simp
+ using card_of_Pow[of "UNIV::'a set"] by simp
-lemma card_of_Un1[simp]:
-shows "|A| \<le>o |A \<union> B| "
-using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
+lemma card_of_Un1[simp]: "|A| \<le>o |A \<union> B| "
+ by fastforce
-lemma card_of_diff[simp]:
-shows "|A - B| \<le>o |A|"
-using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce
+lemma card_of_diff[simp]: "|A - B| \<le>o |A|"
+ by fastforce
lemma subset_ordLeq_strict:
-assumes "A \<le> B" and "|A| <o |B|"
-shows "A < B"
-proof-
- {assume "\<not>(A < B)"
- hence "A = B" using assms(1) by blast
- hence False using assms(2) not_ordLess_ordIso card_of_refl by blast
- }
- thus ?thesis by blast
-qed
+ assumes "A \<le> B" and "|A| <o |B|"
+ shows "A < B"
+ using assms ordLess_irreflexive by blast
corollary subset_ordLeq_diff:
-assumes "A \<le> B" and "|A| <o |B|"
-shows "B - A \<noteq> {}"
-using assms subset_ordLeq_strict by blast
+ assumes "A \<le> B" and "|A| <o |B|"
+ shows "B - A \<noteq> {}"
+ using assms subset_ordLeq_strict by blast
lemma card_of_empty4:
-"|{}::'b set| <o |A::'a set| = (A \<noteq> {})"
-proof(intro iffI notI)
- assume *: "|{}::'b set| <o |A|" and "A = {}"
- hence "|A| =o |{}::'b set|"
- using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
- hence "|{}::'b set| =o |A|" using ordIso_symmetric by blast
- with * show False using not_ordLess_ordIso[of "|{}::'b set|" "|A|"] by blast
-next
- assume "A \<noteq> {}"
- hence "(\<not> (\<exists>f. inj_on f A \<and> f ` A \<subseteq> {}))"
- unfolding inj_on_def by blast
- thus "| {} | <o | A |"
- using card_of_ordLess by blast
-qed
+ "|{}::'b set| <o |A::'a set| = (A \<noteq> {})"
+ by (metis card_of_empty card_of_ordLess2 image_is_empty not_ordLess_ordLeq)
lemma card_of_empty5:
-"|A| <o |B| \<Longrightarrow> B \<noteq> {}"
-using card_of_empty not_ordLess_ordLeq by blast
+ "|A| <o |B| \<Longrightarrow> B \<noteq> {}"
+ using card_of_empty not_ordLess_ordLeq by blast
lemma Well_order_card_of_empty:
-"Well_order r \<Longrightarrow> |{}| \<le>o r" by simp
+ "Well_order r \<Longrightarrow> |{}| \<le>o r"
+ by simp
lemma card_of_UNIV[simp]:
-"|A :: 'a set| \<le>o |UNIV :: 'a set|"
-using card_of_mono1[of A] by simp
+ "|A :: 'a set| \<le>o |UNIV :: 'a set|"
+ by simp
lemma card_of_UNIV2[simp]:
-"Card_order r \<Longrightarrow> (r :: 'a rel) \<le>o |UNIV :: 'a set|"
-using card_of_UNIV[of "Field r"] card_of_Field_ordIso
- ordIso_symmetric ordIso_ordLeq_trans by blast
+ "Card_order r \<Longrightarrow> (r :: 'a rel) \<le>o |UNIV :: 'a set|"
+ using card_of_UNIV[of "Field r"] card_of_Field_ordIso
+ ordIso_symmetric ordIso_ordLeq_trans by blast
lemma card_of_Pow_mono[simp]:
-assumes "|A| \<le>o |B|"
-shows "|Pow A| \<le>o |Pow B|"
+ assumes "|A| \<le>o |B|"
+ shows "|Pow A| \<le>o |Pow B|"
proof-
obtain f where "inj_on f A \<and> f ` A \<le> B"
- using assms card_of_ordLeq[of A B] by auto
+ using assms card_of_ordLeq[of A B] by auto
hence "inj_on (image f) (Pow A) \<and> (image f) ` (Pow A) \<le> (Pow B)"
- by (auto simp add: inj_on_image_Pow image_Pow_mono)
+ by (auto simp: inj_on_image_Pow image_Pow_mono)
thus ?thesis using card_of_ordLeq[of "Pow A"] by metis
qed
lemma ordIso_Pow_mono[simp]:
-assumes "r \<le>o r'"
-shows "|Pow(Field r)| \<le>o |Pow(Field r')|"
-using assms card_of_mono2 card_of_Pow_mono by blast
+ assumes "r \<le>o r'"
+ shows "|Pow(Field r)| \<le>o |Pow(Field r')|"
+ using assms card_of_mono2 card_of_Pow_mono by blast
lemma card_of_Pow_cong[simp]:
-assumes "|A| =o |B|"
-shows "|Pow A| =o |Pow B|"
-proof-
- obtain f where "bij_betw f A B"
- using assms card_of_ordIso[of A B] by auto
- hence "bij_betw (image f) (Pow A) (Pow B)"
- by (auto simp add: bij_betw_image_Pow)
- thus ?thesis using card_of_ordIso[of "Pow A"] by auto
-qed
+ assumes "|A| =o |B|"
+ shows "|Pow A| =o |Pow B|"
+ by (meson assms card_of_Pow_mono ordIso_iff_ordLeq)
lemma ordIso_Pow_cong[simp]:
-assumes "r =o r'"
-shows "|Pow(Field r)| =o |Pow(Field r')|"
-using assms card_of_cong card_of_Pow_cong by blast
+ assumes "r =o r'"
+ shows "|Pow(Field r)| =o |Pow(Field r')|"
+ using assms card_of_cong card_of_Pow_cong by blast
corollary Card_order_Plus_empty1:
-"Card_order r \<Longrightarrow> r =o |(Field r) <+> {}|"
-using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast
+ "Card_order r \<Longrightarrow> r =o |(Field r) <+> {}|"
+ using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast
corollary Card_order_Plus_empty2:
-"Card_order r \<Longrightarrow> r =o |{} <+> (Field r)|"
-using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast
-
-lemma Card_order_Un1:
-shows "Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<union> B| "
-using card_of_Un1 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
+ "Card_order r \<Longrightarrow> r =o |{} <+> (Field r)|"
+ using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast
lemma card_of_Un2[simp]:
-shows "|A| \<le>o |B \<union> A|"
-using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
-
-lemma Card_order_Un2:
-shows "Card_order r \<Longrightarrow> |Field r| \<le>o |A \<union> (Field r)| "
-using card_of_Un2 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
+ shows "|A| \<le>o |B \<union> A|"
+ by fastforce
lemma Un_Plus_bij_betw:
-assumes "A Int B = {}"
-shows "\<exists>f. bij_betw f (A \<union> B) (A <+> B)"
+ assumes "A Int B = {}"
+ shows "\<exists>f. bij_betw f (A \<union> B) (A <+> B)"
proof-
- let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
- have "bij_betw ?f (A \<union> B) (A <+> B)"
- using assms by(unfold bij_betw_def inj_on_def, auto)
+ have "bij_betw (\<lambda> c. if c \<in> A then Inl c else Inr c) (A \<union> B) (A <+> B)"
+ using assms unfolding bij_betw_def inj_on_def by auto
thus ?thesis by blast
qed
lemma card_of_Un_Plus_ordIso:
-assumes "A Int B = {}"
-shows "|A \<union> B| =o |A <+> B|"
-using assms card_of_ordIso[of "A \<union> B"] Un_Plus_bij_betw[of A B] by auto
+ assumes "A Int B = {}"
+ shows "|A \<union> B| =o |A <+> B|"
+ by (meson Un_Plus_bij_betw assms card_of_ordIso)
lemma card_of_Un_Plus_ordIso1:
-"|A \<union> B| =o |A <+> (B - A)|"
-using card_of_Un_Plus_ordIso[of A "B - A"] by auto
+ "|A \<union> B| =o |A <+> (B - A)|"
+ using card_of_Un_Plus_ordIso[of A "B - A"] by auto
lemma card_of_Un_Plus_ordIso2:
-"|A \<union> B| =o |(A - B) <+> B|"
-using card_of_Un_Plus_ordIso[of "A - B" B] by auto
+ "|A \<union> B| =o |(A - B) <+> B|"
+ using card_of_Un_Plus_ordIso[of "A - B" B] by auto
lemma card_of_Times_singl1: "|A| =o |A \<times> {b}|"
proof-
@@ -259,18 +215,19 @@
qed
corollary Card_order_Times_singl1:
-"Card_order r \<Longrightarrow> r =o |(Field r) \<times> {b}|"
-using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast
+ "Card_order r \<Longrightarrow> r =o |(Field r) \<times> {b}|"
+ using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast
lemma card_of_Times_singl2: "|A| =o |{b} \<times> A|"
proof-
- have "bij_betw snd ({b} \<times> A) A" unfolding bij_betw_def inj_on_def by force
+ have "bij_betw snd ({b} \<times> A) A"
+ unfolding bij_betw_def inj_on_def by force
thus ?thesis using card_of_ordIso ordIso_symmetric by blast
qed
corollary Card_order_Times_singl2:
-"Card_order r \<Longrightarrow> r =o |{a} \<times> (Field r)|"
-using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast
+ "Card_order r \<Longrightarrow> r =o |{a} \<times> (Field r)|"
+ using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast
lemma card_of_Times_assoc: "|(A \<times> B) \<times> C| =o |A \<times> B \<times> C|"
proof -
@@ -284,118 +241,111 @@
thus "x \<in> ?f ` ((A \<times> B) \<times> C)" by blast
qed
hence "bij_betw ?f ((A \<times> B) \<times> C) (A \<times> B \<times> C)"
- unfolding bij_betw_def inj_on_def by auto
+ unfolding bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by blast
qed
-corollary Card_order_Times3:
-"Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<times> (Field r)|"
- by (rule card_of_Times3)
-
lemma card_of_Times_cong1[simp]:
-assumes "|A| =o |B|"
-shows "|A \<times> C| =o |B \<times> C|"
-using assms by (simp add: ordIso_iff_ordLeq)
+ assumes "|A| =o |B|"
+ shows "|A \<times> C| =o |B \<times> C|"
+ using assms by (simp add: ordIso_iff_ordLeq)
lemma card_of_Times_cong2[simp]:
-assumes "|A| =o |B|"
-shows "|C \<times> A| =o |C \<times> B|"
-using assms by (simp add: ordIso_iff_ordLeq)
+ assumes "|A| =o |B|"
+ shows "|C \<times> A| =o |C \<times> B|"
+ using assms by (simp add: ordIso_iff_ordLeq)
lemma card_of_Times_mono[simp]:
-assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
-shows "|A \<times> C| \<le>o |B \<times> D|"
-using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B]
- ordLeq_transitive[of "|A \<times> C|"] by blast
+ assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
+ shows "|A \<times> C| \<le>o |B \<times> D|"
+ using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B]
+ ordLeq_transitive[of "|A \<times> C|"] by blast
corollary ordLeq_Times_mono:
-assumes "r \<le>o r'" and "p \<le>o p'"
-shows "|(Field r) \<times> (Field p)| \<le>o |(Field r') \<times> (Field p')|"
-using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Times_mono by blast
+ assumes "r \<le>o r'" and "p \<le>o p'"
+ shows "|(Field r) \<times> (Field p)| \<le>o |(Field r') \<times> (Field p')|"
+ using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Times_mono by blast
corollary ordIso_Times_cong1[simp]:
-assumes "r =o r'"
-shows "|(Field r) \<times> C| =o |(Field r') \<times> C|"
-using assms card_of_cong card_of_Times_cong1 by blast
+ assumes "r =o r'"
+ shows "|(Field r) \<times> C| =o |(Field r') \<times> C|"
+ using assms card_of_cong card_of_Times_cong1 by blast
corollary ordIso_Times_cong2:
-assumes "r =o r'"
-shows "|A \<times> (Field r)| =o |A \<times> (Field r')|"
-using assms card_of_cong card_of_Times_cong2 by blast
+ assumes "r =o r'"
+ shows "|A \<times> (Field r)| =o |A \<times> (Field r')|"
+ using assms card_of_cong card_of_Times_cong2 by blast
lemma card_of_Times_cong[simp]:
-assumes "|A| =o |B|" and "|C| =o |D|"
-shows "|A \<times> C| =o |B \<times> D|"
-using assms
-by (auto simp add: ordIso_iff_ordLeq)
+ assumes "|A| =o |B|" and "|C| =o |D|"
+ shows "|A \<times> C| =o |B \<times> D|"
+ using assms
+ by (auto simp: ordIso_iff_ordLeq)
corollary ordIso_Times_cong:
-assumes "r =o r'" and "p =o p'"
-shows "|(Field r) \<times> (Field p)| =o |(Field r') \<times> (Field p')|"
-using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Times_cong by blast
+ assumes "r =o r'" and "p =o p'"
+ shows "|(Field r) \<times> (Field p)| =o |(Field r') \<times> (Field p')|"
+ using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Times_cong by blast
lemma card_of_Sigma_mono2:
-assumes "inj_on f (I::'i set)" and "f ` I \<le> (J::'j set)"
-shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| \<le>o |SIGMA j : J. A j|"
+ assumes "inj_on f (I::'i set)" and "f ` I \<le> (J::'j set)"
+ shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| \<le>o |SIGMA j : J. A j|"
proof-
let ?LEFT = "SIGMA i : I. A (f i)"
let ?RIGHT = "SIGMA j : J. A j"
obtain u where u_def: "u = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
have "inj_on u ?LEFT \<and> u `?LEFT \<le> ?RIGHT"
- using assms unfolding u_def inj_on_def by auto
+ using assms unfolding u_def inj_on_def by auto
thus ?thesis using card_of_ordLeq by blast
qed
lemma card_of_Sigma_mono:
-assumes INJ: "inj_on f I" and IM: "f ` I \<le> J" and
- LEQ: "\<forall>j \<in> J. |A j| \<le>o |B j|"
-shows "|SIGMA i : I. A (f i)| \<le>o |SIGMA j : J. B j|"
+ assumes INJ: "inj_on f I" and IM: "f ` I \<le> J" and
+ LEQ: "\<forall>j \<in> J. |A j| \<le>o |B j|"
+ shows "|SIGMA i : I. A (f i)| \<le>o |SIGMA j : J. B j|"
proof-
have "\<forall>i \<in> I. |A(f i)| \<le>o |B(f i)|"
- using IM LEQ by blast
+ using IM LEQ by blast
hence "|SIGMA i : I. A (f i)| \<le>o |SIGMA i : I. B (f i)|"
- using card_of_Sigma_mono1[of I] by metis
+ using card_of_Sigma_mono1[of I] by metis
moreover have "|SIGMA i : I. B (f i)| \<le>o |SIGMA j : J. B j|"
- using INJ IM card_of_Sigma_mono2 by blast
+ using INJ IM card_of_Sigma_mono2 by blast
ultimately show ?thesis using ordLeq_transitive by blast
qed
lemma ordLeq_Sigma_mono1:
-assumes "\<forall>i \<in> I. p i \<le>o r i"
-shows "|SIGMA i : I. Field(p i)| \<le>o |SIGMA i : I. Field(r i)|"
-using assms by (auto simp add: card_of_Sigma_mono1)
+ assumes "\<forall>i \<in> I. p i \<le>o r i"
+ shows "|SIGMA i : I. Field(p i)| \<le>o |SIGMA i : I. Field(r i)|"
+ using assms by (auto simp: card_of_Sigma_mono1)
lemma ordLeq_Sigma_mono:
-assumes "inj_on f I" and "f ` I \<le> J" and
- "\<forall>j \<in> J. p j \<le>o r j"
-shows "|SIGMA i : I. Field(p(f i))| \<le>o |SIGMA j : J. Field(r j)|"
-using assms card_of_mono2 card_of_Sigma_mono
- [of f I J "\<lambda> i. Field(p i)" "\<lambda> j. Field(r j)"] by metis
+ assumes "inj_on f I" and "f ` I \<le> J" and
+ "\<forall>j \<in> J. p j \<le>o r j"
+ shows "|SIGMA i : I. Field(p(f i))| \<le>o |SIGMA j : J. Field(r j)|"
+ using assms card_of_mono2 card_of_Sigma_mono [of f I J "\<lambda> i. Field(p i)"] by metis
lemma ordIso_Sigma_cong1:
-assumes "\<forall>i \<in> I. p i =o r i"
-shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|"
-using assms by (auto simp add: card_of_Sigma_cong1)
+ assumes "\<forall>i \<in> I. p i =o r i"
+ shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|"
+ using assms by (auto simp: card_of_Sigma_cong1)
lemma ordLeq_Sigma_cong:
-assumes "bij_betw f I J" and
- "\<forall>j \<in> J. p j =o r j"
-shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|"
-using assms card_of_cong card_of_Sigma_cong
- [of f I J "\<lambda> j. Field(p j)" "\<lambda> j. Field(r j)"] by blast
+ assumes "bij_betw f I J" and
+ "\<forall>j \<in> J. p j =o r j"
+ shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|"
+ using assms card_of_cong card_of_Sigma_cong
+ [of f I J "\<lambda> j. Field(p j)" "\<lambda> j. Field(r j)"] by blast
lemma card_of_UNION_Sigma2:
-assumes
-"!! i j. \<lbrakk>{i,j} <= I; i ~= j\<rbrakk> \<Longrightarrow> A i Int A j = {}"
-shows
-"|\<Union>i\<in>I. A i| =o |Sigma I A|"
+ assumes "\<And>i j. \<lbrakk>{i,j} <= I; i \<noteq> j\<rbrakk> \<Longrightarrow> A i Int A j = {}"
+ shows "|\<Union>i\<in>I. A i| =o |Sigma I A|"
proof-
let ?L = "\<Union>i\<in>I. A i" let ?R = "Sigma I A"
have "|?L| <=o |?R|" using card_of_UNION_Sigma .
moreover have "|?R| <=o |?L|"
proof-
have "inj_on snd ?R"
- unfolding inj_on_def using assms by auto
+ unfolding inj_on_def using assms by auto
moreover have "snd ` ?R <= ?L" by auto
ultimately show ?thesis using card_of_ordLeq by blast
qed
@@ -403,102 +353,91 @@
qed
corollary Plus_into_Times:
-assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
- B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
-shows "\<exists>f. inj_on f (A <+> B) \<and> f ` (A <+> B) \<le> A \<times> B"
-using assms by (auto simp add: card_of_Plus_Times card_of_ordLeq)
+ assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
+ shows "\<exists>f. inj_on f (A <+> B) \<and> f ` (A <+> B) \<le> A \<times> B"
+ using assms by (auto simp: card_of_Plus_Times card_of_ordLeq)
corollary Plus_into_Times_types:
-assumes A2: "(a1::'a) \<noteq> a2" and B2: "(b1::'b) \<noteq> b2"
-shows "\<exists>(f::'a + 'b \<Rightarrow> 'a * 'b). inj f"
-using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV]
-by auto
+ assumes A2: "(a1::'a) \<noteq> a2" and B2: "(b1::'b) \<noteq> b2"
+ shows "\<exists>(f::'a + 'b \<Rightarrow> 'a * 'b). inj f"
+ using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV]
+ by auto
corollary Times_same_infinite_bij_betw:
-assumes "\<not>finite A"
-shows "\<exists>f. bij_betw f (A \<times> A) A"
-using assms by (auto simp add: card_of_ordIso)
+ assumes "\<not>finite A"
+ shows "\<exists>f. bij_betw f (A \<times> A) A"
+ using assms by (auto simp: card_of_ordIso)
corollary Times_same_infinite_bij_betw_types:
-assumes INF: "\<not>finite(UNIV::'a set)"
-shows "\<exists>(f::('a * 'a) => 'a). bij f"
-using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
-by auto
+ assumes INF: "\<not>finite(UNIV::'a set)"
+ shows "\<exists>(f::('a * 'a) => 'a). bij f"
+ using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
+ by auto
corollary Times_infinite_bij_betw:
-assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
-shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
+ assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
+ shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
proof-
have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
thus ?thesis using INF NE
- by (auto simp add: card_of_ordIso card_of_Times_infinite)
+ by (auto simp: card_of_ordIso card_of_Times_infinite)
qed
corollary Times_infinite_bij_betw_types:
-assumes INF: "\<not>finite(UNIV::'a set)" and
- BIJ: "inj(g::'b \<Rightarrow> 'a)"
-shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
-using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
-by auto
+ assumes "\<not>finite(UNIV::'a set)" and "inj(g::'b \<Rightarrow> 'a)"
+ shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
+ using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
+ by auto
lemma card_of_Times_ordLeq_infinite:
-"\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
- \<Longrightarrow> |A \<times> B| \<le>o |C|"
-by(simp add: card_of_Sigma_ordLeq_infinite)
+ "\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk> \<Longrightarrow> |A \<times> B| \<le>o |C|"
+ by(simp add: card_of_Sigma_ordLeq_infinite)
corollary Plus_infinite_bij_betw:
-assumes INF: "\<not>finite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
-shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
+ assumes INF: "\<not>finite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
+ shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
proof-
have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
thus ?thesis using INF
- by (auto simp add: card_of_ordIso)
+ by (auto simp: card_of_ordIso)
qed
corollary Plus_infinite_bij_betw_types:
-assumes INF: "\<not>finite(UNIV::'a set)" and
- BIJ: "inj(g::'b \<Rightarrow> 'a)"
-shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
-using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
-by auto
+ assumes "\<not>finite(UNIV::'a set)" and "inj(g::'b \<Rightarrow> 'a)"
+ shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
+ using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
+ by auto
lemma card_of_Un_infinite:
-assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
-shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
-proof-
- have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
- moreover have "|A <+> B| =o |A|"
- using assms by (metis card_of_Plus_infinite)
- ultimately have "|A \<union> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
- hence "|A \<union> B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast
- thus ?thesis using Un_commute[of B A] by auto
-qed
+ assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
+ shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
+ by (simp add: INF LEQ card_of_Un_ordLeq_infinite_Field ordIso_iff_ordLeq)
lemma card_of_Un_infinite_simps[simp]:
-"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
-"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
-using card_of_Un_infinite by auto
+ "\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
+ "\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
+ using card_of_Un_infinite by auto
lemma card_of_Un_diff_infinite:
-assumes INF: "\<not>finite A" and LESS: "|B| <o |A|"
-shows "|A - B| =o |A|"
+ assumes INF: "\<not>finite A" and LESS: "|B| <o |A|"
+ shows "|A - B| =o |A|"
proof-
obtain C where C_def: "C = A - B" by blast
have "|A \<union> B| =o |A|"
- using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast
+ using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast
moreover have "C \<union> B = A \<union> B" unfolding C_def by auto
ultimately have 1: "|C \<union> B| =o |A|" by auto
- (* *)
+ (* *)
{assume *: "|C| \<le>o |B|"
- moreover
- {assume **: "finite B"
- hence "finite C"
- using card_of_ordLeq_finite * by blast
- hence False using ** INF card_of_ordIso_finite 1 by blast
- }
- hence "\<not>finite B" by auto
- ultimately have False
- using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
+ moreover
+ {assume **: "finite B"
+ hence "finite C"
+ using card_of_ordLeq_finite * by blast
+ hence False using ** INF card_of_ordIso_finite 1 by blast
+ }
+ hence "\<not>finite B" by auto
+ ultimately have False
+ using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
}
hence 2: "|B| \<le>o |C|" using card_of_Well_order ordLeq_total by blast
{assume *: "finite C"
@@ -507,155 +446,121 @@
}
hence "\<not>finite C" by auto
hence "|C| =o |A|"
- using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
+ using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
thus ?thesis unfolding C_def .
qed
corollary Card_order_Un_infinite:
-assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
- LEQ: "p \<le>o r"
-shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
+ assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
+ LEQ: "p \<le>o r"
+ shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
proof-
have "| Field r \<union> Field p | =o | Field r | \<and>
| Field p \<union> Field r | =o | Field r |"
- using assms by (auto simp add: card_of_Un_infinite)
+ using assms by (auto simp: card_of_Un_infinite)
thus ?thesis
- using assms card_of_Field_ordIso[of r]
- ordIso_transitive[of "|Field r \<union> Field p|"]
- ordIso_transitive[of _ "|Field r|"] by blast
+ using assms card_of_Field_ordIso[of r]
+ ordIso_transitive[of "|Field r \<union> Field p|"]
+ ordIso_transitive[of _ "|Field r|"] by blast
qed
corollary subset_ordLeq_diff_infinite:
-assumes INF: "\<not>finite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
-shows "\<not>finite (B - A)"
-using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
+ assumes INF: "\<not>finite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
+ shows "\<not>finite (B - A)"
+ using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
lemma card_of_Times_ordLess_infinite[simp]:
-assumes INF: "\<not>finite C" and
- LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
-shows "|A \<times> B| <o |C|"
+ assumes INF: "\<not>finite C" and
+ LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
+ shows "|A \<times> B| <o |C|"
proof(cases "A = {} \<or> B = {}")
assume Case1: "A = {} \<or> B = {}"
hence "A \<times> B = {}" by blast
moreover have "C \<noteq> {}" using
- LESS1 card_of_empty5 by blast
- ultimately show ?thesis by(auto simp add: card_of_empty4)
+ LESS1 card_of_empty5 by blast
+ ultimately show ?thesis by(auto simp: card_of_empty4)
next
assume Case2: "\<not>(A = {} \<or> B = {})"
{assume *: "|C| \<le>o |A \<times> B|"
- hence "\<not>finite (A \<times> B)" using INF card_of_ordLeq_finite by blast
- hence 1: "\<not>finite A \<or> \<not>finite B" using finite_cartesian_product by blast
- {assume Case21: "|A| \<le>o |B|"
- hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
- hence "|A \<times> B| =o |B|" using Case2 Case21
- by (auto simp add: card_of_Times_infinite)
- hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
- }
- moreover
- {assume Case22: "|B| \<le>o |A|"
- hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
- hence "|A \<times> B| =o |A|" using Case2 Case22
- by (auto simp add: card_of_Times_infinite)
- hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
- }
- ultimately have False using ordLeq_total card_of_Well_order[of A]
- card_of_Well_order[of B] by blast
+ hence "\<not>finite (A \<times> B)" using INF card_of_ordLeq_finite by blast
+ hence 1: "\<not>finite A \<or> \<not>finite B" using finite_cartesian_product by blast
+ {assume Case21: "|A| \<le>o |B|"
+ hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
+ hence "|A \<times> B| =o |B|" using Case2 Case21
+ by (auto simp: card_of_Times_infinite)
+ hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
+ }
+ moreover
+ {assume Case22: "|B| \<le>o |A|"
+ hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
+ hence "|A \<times> B| =o |A|" using Case2 Case22
+ by (auto simp: card_of_Times_infinite)
+ hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
+ }
+ ultimately have False using ordLeq_total card_of_Well_order[of A]
+ card_of_Well_order[of B] by blast
}
thus ?thesis using ordLess_or_ordLeq[of "|A \<times> B|" "|C|"]
- card_of_Well_order[of "A \<times> B"] card_of_Well_order[of "C"] by auto
+ card_of_Well_order[of "A \<times> B"] card_of_Well_order[of "C"] by auto
qed
lemma card_of_Times_ordLess_infinite_Field[simp]:
-assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
- LESS1: "|A| <o r" and LESS2: "|B| <o r"
-shows "|A \<times> B| <o r"
+ assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
+ LESS1: "|A| <o r" and LESS2: "|B| <o r"
+ shows "|A \<times> B| <o r"
proof-
let ?C = "Field r"
have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
- ordIso_symmetric by blast
+ ordIso_symmetric by blast
hence "|A| <o |?C|" "|B| <o |?C|"
- using LESS1 LESS2 ordLess_ordIso_trans by blast+
+ using LESS1 LESS2 ordLess_ordIso_trans by blast+
hence "|A \<times> B| <o |?C|" using INF
- card_of_Times_ordLess_infinite by blast
- thus ?thesis using 1 ordLess_ordIso_trans by blast
-qed
-
-lemma card_of_Un_ordLess_infinite[simp]:
-assumes INF: "\<not>finite C" and
- LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
-shows "|A \<union> B| <o |C|"
-using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
- ordLeq_ordLess_trans by blast
-
-lemma card_of_Un_ordLess_infinite_Field[simp]:
-assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
- LESS1: "|A| <o r" and LESS2: "|B| <o r"
-shows "|A Un B| <o r"
-proof-
- let ?C = "Field r"
- have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
- ordIso_symmetric by blast
- hence "|A| <o |?C|" "|B| <o |?C|"
- using LESS1 LESS2 ordLess_ordIso_trans by blast+
- hence "|A Un B| <o |?C|" using INF
- card_of_Un_ordLess_infinite by blast
+ card_of_Times_ordLess_infinite by blast
thus ?thesis using 1 ordLess_ordIso_trans by blast
qed
lemma ordLeq_finite_Field:
-assumes "r \<le>o s" and "finite (Field s)"
-shows "finite (Field r)"
-by (metis assms card_of_mono2 card_of_ordLeq_infinite)
+ assumes "r \<le>o s" and "finite (Field s)"
+ shows "finite (Field r)"
+ by (metis assms card_of_mono2 card_of_ordLeq_infinite)
lemma ordIso_finite_Field:
-assumes "r =o s"
-shows "finite (Field r) \<longleftrightarrow> finite (Field s)"
-by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field)
+ assumes "r =o s"
+ shows "finite (Field r) \<longleftrightarrow> finite (Field s)"
+ by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field)
subsection \<open>Cardinals versus set operations involving infinite sets\<close>
lemma finite_iff_cardOf_nat:
-"finite A = ( |A| <o |UNIV :: nat set| )"
-using infinite_iff_card_of_nat[of A]
-not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
-by fastforce
+ "finite A = ( |A| <o |UNIV :: nat set| )"
+ by (meson card_of_Well_order infinite_iff_card_of_nat not_ordLeq_iff_ordLess)
lemma finite_ordLess_infinite2[simp]:
-assumes "finite A" and "\<not>finite B"
-shows "|A| <o |B|"
-using assms
-finite_ordLess_infinite[of "|A|" "|B|"]
-card_of_Well_order[of A] card_of_Well_order[of B]
-Field_card_of[of A] Field_card_of[of B] by auto
+ assumes "finite A" and "\<not>finite B"
+ shows "|A| <o |B|"
+ by (meson assms card_of_Well_order card_of_ordLeq_finite not_ordLeq_iff_ordLess)
lemma infinite_card_of_insert:
-assumes "\<not>finite A"
-shows "|insert a A| =o |A|"
+ assumes "\<not>finite A"
+ shows "|insert a A| =o |A|"
proof-
have iA: "insert a A = A \<union> {a}" by simp
show ?thesis
- using infinite_imp_bij_betw2[OF assms] unfolding iA
- by (metis bij_betw_inv card_of_ordIso)
+ using infinite_imp_bij_betw2[OF assms] unfolding iA
+ by (metis bij_betw_inv card_of_ordIso)
qed
lemma card_of_Un_singl_ordLess_infinite1:
-assumes "\<not>finite B" and "|A| <o |B|"
-shows "|{a} Un A| <o |B|"
-proof-
- have "|{a}| <o |B|" using assms by auto
- thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by blast
-qed
+ assumes "\<not>finite B" and "|A| <o |B|"
+ shows "|{a} Un A| <o |B|"
+ by (metis assms card_of_Un_ordLess_infinite finite.emptyI finite_insert finite_ordLess_infinite2)
lemma card_of_Un_singl_ordLess_infinite:
-assumes "\<not>finite B"
-shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
-using assms card_of_Un_singl_ordLess_infinite1[of B A]
-proof(auto)
- assume "|insert a A| <o |B|"
- moreover have "|A| <=o |insert a A|" using card_of_mono1[of A "insert a A"] by blast
- ultimately show "|A| <o |B|" using ordLeq_ordLess_trans by blast
-qed
+ assumes "\<not>finite B"
+ shows "|A| <o |B| \<longleftrightarrow> |{a} Un A| <o |B|"
+ using assms card_of_Un_singl_ordLess_infinite1[of B A]
+ using card_of_Un2 ordLeq_ordLess_trans by blast
subsection \<open>Cardinals versus lists\<close>
@@ -664,48 +569,39 @@
proofs of facts concerning the cardinality of \<open>List\<close> :\<close>
definition nlists :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set"
-where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}"
-
-lemma lists_def2: "lists A = {l. set l \<le> A}"
-using in_listsI by blast
+ where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}"
lemma lists_UNION_nlists: "lists A = (\<Union>n. nlists A n)"
-unfolding lists_def2 nlists_def by blast
+ unfolding lists_eq_set nlists_def by blast
lemma card_of_lists: "|A| \<le>o |lists A|"
proof-
let ?h = "\<lambda> a. [a]"
have "inj_on ?h A \<and> ?h ` A \<le> lists A"
- unfolding inj_on_def lists_def2 by auto
+ unfolding inj_on_def lists_eq_set by auto
thus ?thesis by (metis card_of_ordLeq)
qed
lemma nlists_0: "nlists A 0 = {[]}"
-unfolding nlists_def by auto
+ unfolding nlists_def by auto
lemma nlists_not_empty:
-assumes "A \<noteq> {}"
-shows "nlists A n \<noteq> {}"
-proof(induct n, simp add: nlists_0)
- fix n assume "nlists A n \<noteq> {}"
+ assumes "A \<noteq> {}"
+ shows "nlists A n \<noteq> {}"
+proof (induction n)
+ case (Suc n)
then obtain a and l where "a \<in> A \<and> l \<in> nlists A n" using assms by auto
hence "a # l \<in> nlists A (Suc n)" unfolding nlists_def by auto
- thus "nlists A (Suc n) \<noteq> {}" by auto
-qed
-
-lemma Nil_in_lists: "[] \<in> lists A"
-unfolding lists_def2 by auto
-
-lemma lists_not_empty: "lists A \<noteq> {}"
-using Nil_in_lists by blast
+ then show ?case by auto
+qed (simp add: nlists_0)
lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
proof-
let ?B = "A \<times> (nlists A n)" let ?h = "\<lambda>(a,l). a # l"
have "inj_on ?h ?B \<and> ?h ` ?B \<le> nlists A (Suc n)"
- unfolding inj_on_def nlists_def by auto
+ unfolding inj_on_def nlists_def by auto
moreover have "nlists A (Suc n) \<le> ?h ` ?B"
- proof(auto)
+ proof clarify
fix l assume "l \<in> nlists A (Suc n)"
hence 1: "length l = Suc n \<and> set l \<le> A" unfolding nlists_def by auto
then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv)
@@ -713,131 +609,113 @@
thus "l \<in> ?h ` ?B" using 2 unfolding nlists_def by auto
qed
ultimately have "bij_betw ?h ?B (nlists A (Suc n))"
- unfolding bij_betw_def by auto
+ unfolding bij_betw_def by auto
thus ?thesis using card_of_ordIso ordIso_symmetric by blast
qed
lemma card_of_nlists_infinite:
-assumes "\<not>finite A"
-shows "|nlists A n| \<le>o |A|"
-proof(induct n)
+ assumes "\<not>finite A"
+ shows "|nlists A n| \<le>o |A|"
+proof(induction n)
+ case 0
have "A \<noteq> {}" using assms by auto
- thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0)
+ then show ?case
+ by (simp add: nlists_0)
next
- fix n assume IH: "|nlists A n| \<le>o |A|"
+ case (Suc n)
have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
- using card_of_nlists_Succ by blast
+ using card_of_nlists_Succ by blast
moreover
- {have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast
- hence "|A \<times> (nlists A n)| =o |A|"
- using assms IH by (auto simp add: card_of_Times_infinite)
- }
- ultimately show "|nlists A (Suc n)| \<le>o |A|"
- using ordIso_transitive ordIso_iff_ordLeq by blast
+ have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast
+ hence "|A \<times> (nlists A n)| =o |A|"
+ using Suc assms by auto
+ ultimately show ?case
+ using ordIso_transitive ordIso_iff_ordLeq by blast
qed
+
lemma Card_order_lists: "Card_order r \<Longrightarrow> r \<le>o |lists(Field r) |"
-using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
+ using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
lemma Union_set_lists: "\<Union>(set ` (lists A)) = A"
- unfolding lists_def2
-proof(auto)
- fix a assume "a \<in> A"
+proof -
+ { fix a assume "a \<in> A"
hence "set [a] \<le> A \<and> a \<in> set [a]" by auto
- thus "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast
+ hence "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast }
+ then show ?thesis by force
qed
lemma inj_on_map_lists:
-assumes "inj_on f A"
-shows "inj_on (map f) (lists A)"
-using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto
+ assumes "inj_on f A"
+ shows "inj_on (map f) (lists A)"
+ using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto
lemma map_lists_mono:
-assumes "f ` A \<le> B"
-shows "(map f) ` (lists A) \<le> lists B"
-using assms unfolding lists_def2 by (auto, blast) (* lethal combination of methods :) *)
+ assumes "f ` A \<le> B"
+ shows "(map f) ` (lists A) \<le> lists B"
+ using assms by force
lemma map_lists_surjective:
-assumes "f ` A = B"
-shows "(map f) ` (lists A) = lists B"
-using assms unfolding lists_def2
-proof (auto, blast)
- fix l' assume *: "set l' \<le> f ` A"
- have "set l' \<le> f ` A \<longrightarrow> l' \<in> map f ` {l. set l \<le> A}"
- proof(induct l', auto)
- fix l a
- assume "a \<in> A" and "set l \<le> A" and
- IH: "f ` (set l) \<le> f ` A"
- hence "set (a # l) \<le> A" by auto
- hence "map f (a # l) \<in> map f ` {l. set l \<le> A}" by blast
- thus "f a # map f l \<in> map f ` {l. set l \<le> A}" by auto
- qed
- thus "l' \<in> map f ` {l. set l \<le> A}" using * by auto
-qed
+ assumes "f ` A = B"
+ shows "(map f) ` (lists A) = lists B"
+ by (metis assms lists_image)
lemma bij_betw_map_lists:
-assumes "bij_betw f A B"
-shows "bij_betw (map f) (lists A) (lists B)"
-using assms unfolding bij_betw_def
-by(auto simp add: inj_on_map_lists map_lists_surjective)
+ assumes "bij_betw f A B"
+ shows "bij_betw (map f) (lists A) (lists B)"
+ using assms unfolding bij_betw_def
+ by(auto simp: inj_on_map_lists map_lists_surjective)
lemma card_of_lists_mono[simp]:
-assumes "|A| \<le>o |B|"
-shows "|lists A| \<le>o |lists B|"
+ assumes "|A| \<le>o |B|"
+ shows "|lists A| \<le>o |lists B|"
proof-
obtain f where "inj_on f A \<and> f ` A \<le> B"
- using assms card_of_ordLeq[of A B] by auto
+ using assms card_of_ordLeq[of A B] by auto
hence "inj_on (map f) (lists A) \<and> (map f) ` (lists A) \<le> (lists B)"
- by (auto simp add: inj_on_map_lists map_lists_mono)
+ by (auto simp: inj_on_map_lists map_lists_mono)
thus ?thesis using card_of_ordLeq[of "lists A"] by metis
qed
lemma ordIso_lists_mono:
-assumes "r \<le>o r'"
-shows "|lists(Field r)| \<le>o |lists(Field r')|"
-using assms card_of_mono2 card_of_lists_mono by blast
+ assumes "r \<le>o r'"
+ shows "|lists(Field r)| \<le>o |lists(Field r')|"
+ using assms card_of_mono2 card_of_lists_mono by blast
lemma card_of_lists_cong[simp]:
-assumes "|A| =o |B|"
-shows "|lists A| =o |lists B|"
-proof-
- obtain f where "bij_betw f A B"
- using assms card_of_ordIso[of A B] by auto
- hence "bij_betw (map f) (lists A) (lists B)"
- by (auto simp add: bij_betw_map_lists)
- thus ?thesis using card_of_ordIso[of "lists A"] by auto
-qed
+ assumes "|A| =o |B|"
+ shows "|lists A| =o |lists B|"
+ by (meson assms card_of_lists_mono ordIso_iff_ordLeq)
lemma card_of_lists_infinite[simp]:
-assumes "\<not>finite A"
-shows "|lists A| =o |A|"
+ assumes "\<not>finite A"
+ shows "|lists A| =o |A|"
proof-
have "|lists A| \<le>o |A|" unfolding lists_UNION_nlists
- by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
- (metis infinite_iff_card_of_nat assms)
+ by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
+ (metis infinite_iff_card_of_nat assms)
thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
qed
lemma Card_order_lists_infinite:
-assumes "Card_order r" and "\<not>finite(Field r)"
-shows "|lists(Field r)| =o r"
-using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
+ assumes "Card_order r" and "\<not>finite(Field r)"
+ shows "|lists(Field r)| =o r"
+ using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
lemma ordIso_lists_cong:
-assumes "r =o r'"
-shows "|lists(Field r)| =o |lists(Field r')|"
-using assms card_of_cong card_of_lists_cong by blast
+ assumes "r =o r'"
+ shows "|lists(Field r)| =o |lists(Field r')|"
+ using assms card_of_cong card_of_lists_cong by blast
corollary lists_infinite_bij_betw:
-assumes "\<not>finite A"
-shows "\<exists>f. bij_betw f (lists A) A"
-using assms card_of_lists_infinite card_of_ordIso by blast
+ assumes "\<not>finite A"
+ shows "\<exists>f. bij_betw f (lists A) A"
+ using assms card_of_lists_infinite card_of_ordIso by blast
corollary lists_infinite_bij_betw_types:
-assumes "\<not>finite(UNIV :: 'a set)"
-shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
-using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
-using lists_UNIV by auto
+ assumes "\<not>finite(UNIV :: 'a set)"
+ shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
+ using assms lists_infinite_bij_betw by fastforce
subsection \<open>Cardinals versus the finite powerset operator\<close>
@@ -846,82 +724,72 @@
proof-
let ?h = "\<lambda> a. {a}"
have "inj_on ?h A \<and> ?h ` A \<le> Fpow A"
- unfolding inj_on_def Fpow_def by auto
+ unfolding inj_on_def Fpow_def by auto
thus ?thesis using card_of_ordLeq by metis
qed
lemma Card_order_Fpow: "Card_order r \<Longrightarrow> r \<le>o |Fpow(Field r) |"
-using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
+ using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
lemma image_Fpow_surjective:
-assumes "f ` A = B"
-shows "(image f) ` (Fpow A) = Fpow B"
-using assms proof(unfold Fpow_def, auto)
- fix Y assume *: "Y \<le> f ` A" and **: "finite Y"
- hence "\<forall>b \<in> Y. \<exists>a. a \<in> A \<and> f a = b" by auto
- with bchoice[of Y "\<lambda>b a. a \<in> A \<and> f a = b"]
- obtain g where 1: "\<forall>b \<in> Y. g b \<in> A \<and> f(g b) = b" by blast
- obtain X where X_def: "X = g ` Y" by blast
- have "f ` X = Y \<and> X \<le> A \<and> finite X"
- by(unfold X_def, force simp add: ** 1)
- thus "Y \<in> (image f) ` {X. X \<le> A \<and> finite X}" by auto
+ assumes "f ` A = B"
+ shows "(image f) ` (Fpow A) = Fpow B"
+proof -
+ have "\<And>C. \<lbrakk>C \<subseteq> f ` A; finite C\<rbrakk> \<Longrightarrow> C \<in> (`) f ` {X. X \<subseteq> A \<and> finite X}"
+ by (simp add: finite_subset_image image_iff)
+ then show ?thesis
+ using assms by (force simp add: Fpow_def)
qed
lemma bij_betw_image_Fpow:
-assumes "bij_betw f A B"
-shows "bij_betw (image f) (Fpow A) (Fpow B)"
-using assms unfolding bij_betw_def
-by (auto simp add: inj_on_image_Fpow image_Fpow_surjective)
+ assumes "bij_betw f A B"
+ shows "bij_betw (image f) (Fpow A) (Fpow B)"
+ using assms unfolding bij_betw_def
+ by (auto simp: inj_on_image_Fpow image_Fpow_surjective)
lemma card_of_Fpow_mono[simp]:
-assumes "|A| \<le>o |B|"
-shows "|Fpow A| \<le>o |Fpow B|"
+ assumes "|A| \<le>o |B|"
+ shows "|Fpow A| \<le>o |Fpow B|"
proof-
obtain f where "inj_on f A \<and> f ` A \<le> B"
- using assms card_of_ordLeq[of A B] by auto
+ using assms card_of_ordLeq[of A B] by auto
hence "inj_on (image f) (Fpow A) \<and> (image f) ` (Fpow A) \<le> (Fpow B)"
- by (auto simp add: inj_on_image_Fpow image_Fpow_mono)
+ by (auto simp: inj_on_image_Fpow image_Fpow_mono)
thus ?thesis using card_of_ordLeq[of "Fpow A"] by auto
qed
lemma ordIso_Fpow_mono:
-assumes "r \<le>o r'"
-shows "|Fpow(Field r)| \<le>o |Fpow(Field r')|"
-using assms card_of_mono2 card_of_Fpow_mono by blast
+ assumes "r \<le>o r'"
+ shows "|Fpow(Field r)| \<le>o |Fpow(Field r')|"
+ using assms card_of_mono2 card_of_Fpow_mono by blast
lemma card_of_Fpow_cong[simp]:
-assumes "|A| =o |B|"
-shows "|Fpow A| =o |Fpow B|"
-proof-
- obtain f where "bij_betw f A B"
- using assms card_of_ordIso[of A B] by auto
- hence "bij_betw (image f) (Fpow A) (Fpow B)"
- by (auto simp add: bij_betw_image_Fpow)
- thus ?thesis using card_of_ordIso[of "Fpow A"] by auto
-qed
+ assumes "|A| =o |B|"
+ shows "|Fpow A| =o |Fpow B|"
+ by (meson assms card_of_Fpow_mono ordIso_iff_ordLeq)
lemma ordIso_Fpow_cong:
-assumes "r =o r'"
-shows "|Fpow(Field r)| =o |Fpow(Field r')|"
-using assms card_of_cong card_of_Fpow_cong by blast
+ assumes "r =o r'"
+ shows "|Fpow(Field r)| =o |Fpow(Field r')|"
+ using assms card_of_cong card_of_Fpow_cong by blast
lemma card_of_Fpow_lists: "|Fpow A| \<le>o |lists A|"
proof-
have "set ` (lists A) = Fpow A"
- unfolding lists_def2 Fpow_def using finite_list finite_set by blast
+ unfolding lists_eq_set Fpow_def using finite_list finite_set by blast
thus ?thesis using card_of_ordLeq2[of "Fpow A"] Fpow_not_empty[of A] by blast
qed
lemma card_of_Fpow_infinite[simp]:
-assumes "\<not>finite A"
-shows "|Fpow A| =o |A|"
-using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
- ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
+ assumes "\<not>finite A"
+ shows "|Fpow A| =o |A|"
+ using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
+ ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
corollary Fpow_infinite_bij_betw:
-assumes "\<not>finite A"
-shows "\<exists>f. bij_betw f (Fpow A) A"
-using assms card_of_Fpow_infinite card_of_ordIso by blast
+ assumes "\<not>finite A"
+ shows "\<exists>f. bij_betw f (Fpow A) A"
+ using assms card_of_Fpow_infinite card_of_ordIso by blast
subsection \<open>The cardinal $\omega$ and the finite cardinals\<close>
@@ -929,108 +797,120 @@
subsubsection \<open>First as well-orders\<close>
lemma Field_natLess: "Field natLess = (UNIV::nat set)"
-by(unfold Field_def natLess_def, auto)
+ by (auto simp: Field_def natLess_def)
lemma natLeq_well_order_on: "well_order_on UNIV natLeq"
-using natLeq_Well_order Field_natLeq by auto
+ using natLeq_Well_order Field_natLeq by auto
lemma natLeq_wo_rel: "wo_rel natLeq"
-unfolding wo_rel_def using natLeq_Well_order .
+ unfolding wo_rel_def using natLeq_Well_order .
lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
-by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
- simp add: Field_natLeq, unfold under_def natLeq_def, auto)
+proof -
+ have "\<forall>t<n. t \<in> Field natLeq"
+ by (simp add: Field_natLeq)
+ moreover have "\<forall>x<n. \<forall>t. (t, x) \<in> natLeq \<longrightarrow> t < n"
+ by (simp add: natLeq_def)
+ ultimately show ?thesis
+ by (auto simp: natLeq_wo_rel wo_rel.ofilter_def under_def)
+qed
lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
-by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
- simp add: Field_natLeq, unfold under_def natLeq_def, auto)
+ by (metis (no_types) atLeastLessThanSuc_atLeastAtMost natLeq_ofilter_less)
lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
-using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
+ using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
lemma closed_nat_set_iff:
-assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
-shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
+ assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
+ shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
proof-
{assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
- moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
- ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
- using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
- have "A = {0 ..< n}"
- proof(auto simp add: 1)
- fix m assume *: "m \<in> A"
- {assume "n \<le> m" with assms * have "n \<in> A" by blast
- hence False using 1 by auto
- }
- thus "m < n" by fastforce
- qed
- hence "\<exists>n. A = {0 ..< n}" by blast
+ moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
+ ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
+ using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
+ then have "A = {0 ..< n}"
+ proof(auto simp: 1)
+ fix m assume *: "m \<in> A"
+ {assume "n \<le> m" with assms * have "n \<in> A" by blast
+ hence False using 1 by auto
+ }
+ thus "m < n" by fastforce
+ qed
+ hence "\<exists>n. A = {0 ..< n}" by blast
}
thus ?thesis by blast
qed
lemma natLeq_ofilter_iff:
-"ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
+ "ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
proof(rule iffI)
assume "ofilter natLeq A"
hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A" using natLeq_wo_rel
- by(auto simp add: natLeq_def wo_rel.ofilter_def under_def)
+ by(auto simp: natLeq_def wo_rel.ofilter_def under_def)
thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
next
assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
thus "ofilter natLeq A"
- by(auto simp add: natLeq_ofilter_less natLeq_UNIV_ofilter)
+ by(auto simp: natLeq_ofilter_less natLeq_UNIV_ofilter)
qed
lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
-unfolding under_def natLeq_def by auto
+ unfolding under_def natLeq_def by auto
lemma natLeq_on_ofilter_less_eq:
-"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
-apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
-apply (simp add: Field_natLeq_on)
-by (auto simp add: under_def)
+ "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
+ by (auto simp: natLeq_on_wo_rel wo_rel.ofilter_def Field_natLeq_on under_def)
lemma natLeq_on_ofilter_iff:
-"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
+ "wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
proof(rule iffI)
assume *: "wo_rel.ofilter (natLeq_on m) A"
hence 1: "A \<le> {0..<m}"
- by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on)
+ by (auto simp: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on)
hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
- using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def)
+ using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def)
hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
next
assume "(\<exists>n\<le>m. A = {0 ..< n})"
- thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
+ thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp: natLeq_on_ofilter_less_eq)
qed
corollary natLeq_on_ofilter:
-"ofilter(natLeq_on n) {0 ..< n}"
-by (auto simp add: natLeq_on_ofilter_less_eq)
+ "ofilter(natLeq_on n) {0 ..< n}"
+ by (auto simp: natLeq_on_ofilter_less_eq)
lemma natLeq_on_ofilter_less:
-"n < m \<Longrightarrow> ofilter (natLeq_on m) {0 .. n}"
-by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
- simp add: Field_natLeq_on, unfold under_def, auto)
+ assumes "n < m" shows "ofilter (natLeq_on m) {0 .. n}"
+proof -
+ have "Suc n \<le> m"
+ using assms by simp
+ then show ?thesis
+ using natLeq_on_ofilter_iff by auto
+qed
lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
-using Field_natLeq Field_natLeq_on[of n]
- finite_ordLess_infinite[of "natLeq_on n" natLeq]
- natLeq_Well_order natLeq_on_Well_order[of n] by auto
+proof -
+ have "well_order natLeq"
+ using Field_natLeq natLeq_Well_order by auto
+ moreover have "\<And>n. well_order_on {na. na < n} (natLeq_on n)"
+ using Field_natLeq_on natLeq_on_Well_order by presburger
+ ultimately show ?thesis
+ by (simp add: Field_natLeq Field_natLeq_on finite_ordLess_infinite)
+qed
lemma natLeq_on_injective:
-"natLeq_on m = natLeq_on n \<Longrightarrow> m = n"
-using Field_natLeq_on[of m] Field_natLeq_on[of n]
- atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast
+ "natLeq_on m = natLeq_on n \<Longrightarrow> m = n"
+ using Field_natLeq_on[of m] Field_natLeq_on[of n]
+ atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast
lemma natLeq_on_injective_ordIso:
-"(natLeq_on m =o natLeq_on n) = (m = n)"
-proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
+ "(natLeq_on m =o natLeq_on n) = (m = n)"
+proof(auto simp: natLeq_on_Well_order ordIso_reflexive)
assume "natLeq_on m =o natLeq_on n"
then obtain f where "bij_betw f {x. x<m} {x. x<n}"
- using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto
+ using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto
thus "m = n" using atLeastLessThan_injective2[of f m n]
unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
qed
@@ -1039,46 +919,48 @@
subsubsection \<open>Then as cardinals\<close>
lemma ordIso_natLeq_infinite1:
-"|A| =o natLeq \<Longrightarrow> \<not>finite A"
-using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
+ "|A| =o natLeq \<Longrightarrow> \<not>finite A"
+ by (meson finite_iff_ordLess_natLeq not_ordLess_ordIso)
lemma ordIso_natLeq_infinite2:
-"natLeq =o |A| \<Longrightarrow> \<not>finite A"
-using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
+ "natLeq =o |A| \<Longrightarrow> \<not>finite A"
+ using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
lemma ordIso_natLeq_on_imp_finite:
-"|A| =o natLeq_on n \<Longrightarrow> finite A"
-unfolding ordIso_def iso_def[abs_def]
-by (auto simp: Field_natLeq_on bij_betw_finite)
+ "|A| =o natLeq_on n \<Longrightarrow> finite A"
+ unfolding ordIso_def iso_def[abs_def]
+ by (auto simp: Field_natLeq_on bij_betw_finite)
lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
-proof(unfold card_order_on_def,
- auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
- fix r assume "well_order_on {x. x < n} r"
- thus "natLeq_on n \<le>o r"
- using finite_atLeastLessThan natLeq_on_well_order_on
+proof -
+ { fix r assume "well_order_on {x. x < n} r"
+ hence "natLeq_on n \<le>o r"
+ using finite_atLeastLessThan natLeq_on_well_order_on
finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
+ }
+ then show ?thesis
+ unfolding card_order_on_def using Field_natLeq_on natLeq_on_Well_order by presburger
qed
corollary card_of_Field_natLeq_on:
-"|Field (natLeq_on n)| =o natLeq_on n"
-using Field_natLeq_on natLeq_on_Card_order
- Card_order_iff_ordIso_card_of[of "natLeq_on n"]
- ordIso_symmetric[of "natLeq_on n"] by blast
+ "|Field (natLeq_on n)| =o natLeq_on n"
+ using Field_natLeq_on natLeq_on_Card_order
+ Card_order_iff_ordIso_card_of[of "natLeq_on n"]
+ ordIso_symmetric[of "natLeq_on n"] by blast
corollary card_of_less:
-"|{0 ..< n}| =o natLeq_on n"
-using Field_natLeq_on card_of_Field_natLeq_on
-unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto
+ "|{0 ..< n}| =o natLeq_on n"
+ using Field_natLeq_on card_of_Field_natLeq_on
+ unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto
lemma natLeq_on_ordLeq_less_eq:
-"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
+ "((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
proof
assume "natLeq_on m \<le>o natLeq_on n"
then obtain f where "inj_on f {x. x < m} \<and> f ` {x. x < m} \<le> {x. x < n}"
- unfolding ordLeq_def using
- embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
- embed_Field Field_natLeq_on by blast
+ unfolding ordLeq_def using
+ embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
+ embed_Field Field_natLeq_on by blast
thus "m \<le> n" using atLeastLessThan_less_eq2
unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
next
@@ -1086,141 +968,126 @@
hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
thus "natLeq_on m \<le>o natLeq_on n"
- using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
+ using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
qed
lemma natLeq_on_ordLeq_less:
-"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
-using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
- natLeq_on_ordLeq_less_eq[of n m] by linarith
+ "((natLeq_on m) <o (natLeq_on n)) = (m < n)"
+ using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
+ natLeq_on_ordLeq_less_eq[of n m] by linarith
lemma ordLeq_natLeq_on_imp_finite:
-assumes "|A| \<le>o natLeq_on n"
-shows "finite A"
+ assumes "|A| \<le>o natLeq_on n"
+ shows "finite A"
proof-
have "|A| \<le>o |{0 ..< n}|"
- using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast
- thus ?thesis by (auto simp add: card_of_ordLeq_finite)
+ using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast
+ thus ?thesis by (auto simp: card_of_ordLeq_finite)
qed
subsubsection \<open>"Backward compatibility" with the numeric cardinal operator for finite sets\<close>
lemma finite_card_of_iff_card2:
-assumes FIN: "finite A" and FIN': "finite B"
-shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
-using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
+ assumes FIN: "finite A" and FIN': "finite B"
+ shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
+ using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
lemma finite_imp_card_of_natLeq_on:
-assumes "finite A"
-shows "|A| =o natLeq_on (card A)"
+ assumes "finite A"
+ shows "|A| =o natLeq_on (card A)"
proof-
obtain h where "bij_betw h A {0 ..< card A}"
- using assms ex_bij_betw_finite_nat by blast
+ using assms ex_bij_betw_finite_nat by blast
thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
qed
lemma finite_iff_card_of_natLeq_on:
-"finite A = (\<exists>n. |A| =o natLeq_on n)"
-using finite_imp_card_of_natLeq_on[of A]
-by(auto simp add: ordIso_natLeq_on_imp_finite)
+ "finite A = (\<exists>n. |A| =o natLeq_on n)"
+ using finite_imp_card_of_natLeq_on[of A]
+ by(auto simp: ordIso_natLeq_on_imp_finite)
lemma finite_card_of_iff_card:
-assumes FIN: "finite A" and FIN': "finite B"
-shows "( |A| =o |B| ) = (card A = card B)"
-using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast
+ assumes FIN: "finite A" and FIN': "finite B"
+ shows "( |A| =o |B| ) = (card A = card B)"
+ using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast
lemma finite_card_of_iff_card3:
-assumes FIN: "finite A" and FIN': "finite B"
-shows "( |A| <o |B| ) = (card A < card B)"
+ assumes FIN: "finite A" and FIN': "finite B"
+ shows "( |A| <o |B| ) = (card A < card B)"
proof-
have "( |A| <o |B| ) = (~ ( |B| \<le>o |A| ))" by simp
- also have "... = (~ (card B \<le> card A))"
- using assms by(simp add: finite_card_of_iff_card2)
- also have "... = (card A < card B)" by auto
+ also have "\<dots> = (~ (card B \<le> card A))"
+ using assms by(simp add: finite_card_of_iff_card2)
+ also have "\<dots> = (card A < card B)" by auto
finally show ?thesis .
qed
lemma card_Field_natLeq_on:
-"card(Field(natLeq_on n)) = n"
-using Field_natLeq_on card_atLeastLessThan by auto
+ "card(Field(natLeq_on n)) = n"
+ using Field_natLeq_on card_atLeastLessThan by auto
subsection \<open>The successor of a cardinal\<close>
lemma embed_implies_ordIso_Restr:
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f"
-shows "r' =o Restr r (f ` (Field r'))"
-using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast
-
-lemma cardSuc_Well_order[simp]:
-"Card_order r \<Longrightarrow> Well_order(cardSuc r)"
-using cardSuc_Card_order unfolding card_order_on_def by blast
-
-lemma Field_cardSuc_not_empty:
-assumes "Card_order r"
-shows "Field (cardSuc r) \<noteq> {}"
-proof
- assume "Field(cardSuc r) = {}"
- hence "|Field(cardSuc r)| \<le>o r" using assms Card_order_empty[of r] by auto
- hence "cardSuc r \<le>o r" using assms card_of_Field_ordIso
- cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast
- thus False using cardSuc_greater not_ordLess_ordLeq assms by blast
-qed
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f"
+ shows "r' =o Restr r (f ` (Field r'))"
+ using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast
lemma cardSuc_mono_ordLess[simp]:
-assumes CARD: "Card_order r" and CARD': "Card_order r'"
-shows "(cardSuc r <o cardSuc r') = (r <o r')"
+ assumes CARD: "Card_order r" and CARD': "Card_order r'"
+ shows "(cardSuc r <o cardSuc r') = (r <o r')"
proof-
have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
- using assms by auto
+ using assms by auto
thus ?thesis
- using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r']
- using cardSuc_mono_ordLeq[of r' r] assms by blast
+ using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r']
+ using cardSuc_mono_ordLeq[of r' r] assms by blast
qed
lemma cardSuc_natLeq_on_Suc:
-"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
+ "cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
proof-
obtain r r' p where r_def: "r = natLeq_on n" and
- r'_def: "r' = cardSuc(natLeq_on n)" and
- p_def: "p = natLeq_on(Suc n)" by blast
- (* Preliminary facts: *)
+ r'_def: "r' = cardSuc(natLeq_on n)" and
+ p_def: "p = natLeq_on(Suc n)" by blast
+ (* Preliminary facts: *)
have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
- using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
+ using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
hence WELL: "Well_order r \<and> Well_order r' \<and> Well_order p"
- unfolding card_order_on_def by force
+ unfolding card_order_on_def by force
have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
- unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp
+ unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp
hence FIN: "finite (Field r)" by force
have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
hence LESS: "|Field r| <o |Field r'|"
- using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
- (* Main proof: *)
+ using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
+ (* Main proof: *)
have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
- using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
+ using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
moreover have "p \<le>o r'"
proof-
{assume "r' <o p"
- then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
- let ?q = "Restr p (f ` Field r')"
- have 1: "embed r' p f" using 0 unfolding embedS_def by force
- hence 2: "f ` Field r' < {0..<(Suc n)}"
- using WELL FIELD 0 by (auto simp add: embedS_iff)
- have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
- then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
- unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
- hence 4: "m \<le> n" using 2 by force
- (* *)
- have "bij_betw f (Field r') (f ` (Field r'))"
- using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast
- moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
- ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
- using bij_betw_same_card bij_betw_finite by metis
- hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
- hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
- hence False using LESS not_ordLess_ordLeq by auto
+ then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
+ let ?q = "Restr p (f ` Field r')"
+ have 1: "embed r' p f" using 0 unfolding embedS_def by force
+ hence 2: "f ` Field r' < {0..<(Suc n)}"
+ using WELL FIELD 0 by (auto simp: embedS_iff)
+ have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
+ then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
+ unfolding p_def by (auto simp: natLeq_on_ofilter_iff)
+ hence 4: "m \<le> n" using 2 by force
+ (* *)
+ have "bij_betw f (Field r') (f ` (Field r'))"
+ using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast
+ moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
+ ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
+ using bij_betw_same_card bij_betw_finite by metis
+ hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
+ hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
+ hence False using LESS not_ordLess_ordLeq by auto
}
thus ?thesis using WELL CARD by fastforce
qed
@@ -1228,129 +1095,104 @@
qed
lemma card_of_Plus_ordLeq_infinite[simp]:
-assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
-shows "|A <+> B| \<le>o |C|"
-proof-
- let ?r = "cardSuc |C|"
- have "Card_order ?r \<and> \<not>finite (Field ?r)" using assms by simp
- moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
- ultimately have "|A <+> B| <o ?r"
- using card_of_Plus_ordLess_infinite_Field by blast
- thus ?thesis using C by simp
-qed
+ assumes "\<not>finite C" and "|A| \<le>o |C|" and "|B| \<le>o |C|"
+ shows "|A <+> B| \<le>o |C|"
+ by (simp add: assms)
lemma card_of_Un_ordLeq_infinite[simp]:
-assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
-shows "|A Un B| \<le>o |C|"
-using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
-ordLeq_transitive by metis
+ assumes "\<not>finite C" and "|A| \<le>o |C|" and "|B| \<le>o |C|"
+ shows "|A Un B| \<le>o |C|"
+ using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq ordLeq_transitive by metis
subsection \<open>Others\<close>
lemma under_mono[simp]:
-assumes "Well_order r" and "(i,j) \<in> r"
-shows "under r i \<subseteq> under r j"
-using assms unfolding under_def order_on_defs
-trans_def by blast
+ assumes "Well_order r" and "(i,j) \<in> r"
+ shows "under r i \<subseteq> under r j"
+ using assms unfolding under_def order_on_defs trans_def by blast
lemma underS_under:
-assumes "i \<in> Field r"
-shows "underS r i = under r i - {i}"
-using assms unfolding underS_def under_def by auto
+ assumes "i \<in> Field r"
+ shows "underS r i = under r i - {i}"
+ using assms unfolding underS_def under_def by auto
lemma relChain_under:
-assumes "Well_order r"
-shows "relChain r (\<lambda> i. under r i)"
-using assms unfolding relChain_def by auto
+ assumes "Well_order r"
+ shows "relChain r (\<lambda> i. under r i)"
+ using assms unfolding relChain_def by auto
lemma card_of_infinite_diff_finite:
-assumes "\<not>finite A" and "finite B"
-shows "|A - B| =o |A|"
-by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
+ assumes "\<not>finite A" and "finite B"
+ shows "|A - B| =o |A|"
+ by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
lemma infinite_card_of_diff_singl:
-assumes "\<not>finite A"
-shows "|A - {a}| =o |A|"
-by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
+ assumes "\<not>finite A"
+ shows "|A - {a}| =o |A|"
+ by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
lemma card_of_vimage:
-assumes "B \<subseteq> range f"
-shows "|B| \<le>o |f -` B|"
-apply(rule surj_imp_ordLeq[of _ f])
-using assms by (metis Int_absorb2 image_vimage_eq order_refl)
+ assumes "B \<subseteq> range f"
+ shows "|B| \<le>o |f -` B|"
+ by (metis Int_absorb2 assms image_vimage_eq order_refl surj_imp_ordLeq)
lemma surj_card_of_vimage:
-assumes "surj f"
-shows "|B| \<le>o |f -` B|"
-by (metis assms card_of_vimage subset_UNIV)
-
-lemma infinite_Pow:
-assumes "\<not> finite A"
-shows "\<not> finite (Pow A)"
-proof-
- have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
- thus ?thesis by (metis assms finite_Pow_iff)
-qed
+ assumes "surj f"
+ shows "|B| \<le>o |f -` B|"
+ by (metis assms card_of_vimage subset_UNIV)
(* bounded powerset *)
definition Bpow where
-"Bpow r A \<equiv> {X . X \<subseteq> A \<and> |X| \<le>o r}"
+ "Bpow r A \<equiv> {X . X \<subseteq> A \<and> |X| \<le>o r}"
lemma Bpow_empty[simp]:
-assumes "Card_order r"
-shows "Bpow r {} = {{}}"
-using assms unfolding Bpow_def by auto
+ assumes "Card_order r"
+ shows "Bpow r {} = {{}}"
+ using assms unfolding Bpow_def by auto
lemma singl_in_Bpow:
-assumes rc: "Card_order r"
-and r: "Field r \<noteq> {}" and a: "a \<in> A"
-shows "{a} \<in> Bpow r A"
+ assumes rc: "Card_order r"
+ and r: "Field r \<noteq> {}" and a: "a \<in> A"
+ shows "{a} \<in> Bpow r A"
proof-
have "|{a}| \<le>o r" using r rc by auto
thus ?thesis unfolding Bpow_def using a by auto
qed
lemma ordLeq_card_Bpow:
-assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
-shows "|A| \<le>o |Bpow r A|"
+ assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
+ shows "|A| \<le>o |Bpow r A|"
proof-
have "inj_on (\<lambda> a. {a}) A" unfolding inj_on_def by auto
moreover have "(\<lambda> a. {a}) ` A \<subseteq> Bpow r A"
- using singl_in_Bpow[OF assms] by auto
+ using singl_in_Bpow[OF assms] by auto
ultimately show ?thesis unfolding card_of_ordLeq[symmetric] by blast
qed
lemma infinite_Bpow:
-assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
-and A: "\<not>finite A"
-shows "\<not>finite (Bpow r A)"
-using ordLeq_card_Bpow[OF rc r]
-by (metis A card_of_ordLeq_infinite)
+ assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
+ and A: "\<not>finite A"
+ shows "\<not>finite (Bpow r A)"
+ using ordLeq_card_Bpow[OF rc r]
+ by (metis A card_of_ordLeq_infinite)
definition Func_option where
- "Func_option A B \<equiv>
+ "Func_option A B \<equiv>
{f. (\<forall> a. f a \<noteq> None \<longleftrightarrow> a \<in> A) \<and> (\<forall> a \<in> A. case f a of Some b \<Rightarrow> b \<in> B |None \<Rightarrow> True)}"
lemma card_of_Func_option_Func:
-"|Func_option A B| =o |Func A B|"
+ "|Func_option A B| =o |Func A B|"
proof (rule ordIso_symmetric, unfold card_of_ordIso[symmetric], intro exI)
let ?F = "\<lambda> f a. if a \<in> A then Some (f a) else None"
show "bij_betw ?F (Func A B) (Func_option A B)"
- unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI)
+ unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI)
fix f g assume f: "f \<in> Func A B" and g: "g \<in> Func A B" and eq: "?F f = ?F g"
show "f = g"
proof(rule ext)
fix a
show "f a = g a"
- proof(cases "a \<in> A")
- case True
- have "Some (f a) = ?F f a" using True by auto
- also have "... = ?F g a" using eq unfolding fun_eq_iff by(rule allE)
- also have "... = Some (g a)" using True by auto
- finally have "Some (f a) = Some (g a)" .
- thus ?thesis by simp
- qed(insert f g, unfold Func_def, auto)
+ by (smt (verit) Func_def eq f g mem_Collect_eq option.inject)
qed
next
show "?F ` Func A B = Func_option A B"
@@ -1358,11 +1200,11 @@
fix f assume f: "f \<in> Func_option A B"
define g where [abs_def]: "g a = (case f a of Some b \<Rightarrow> b | None \<Rightarrow> undefined)" for a
have "g \<in> Func A B"
- using f unfolding g_def Func_def Func_option_def by force+
+ using f unfolding g_def Func_def Func_option_def by force+
moreover have "f = ?F g"
proof(rule ext)
fix a show "f a = ?F g a"
- using f unfolding Func_option_def g_def by (cases "a \<in> A") force+
+ using f unfolding Func_option_def g_def by (cases "a \<in> A") force+
qed
ultimately show "f \<in> ?F ` (Func A B)" by blast
qed(unfold Func_def Func_option_def, auto)
@@ -1371,16 +1213,16 @@
(* partial-function space: *)
definition Pfunc where
-"Pfunc A B \<equiv>
+ "Pfunc A B \<equiv>
{f. (\<forall>a. f a \<noteq> None \<longrightarrow> a \<in> A) \<and>
(\<forall>a. case f a of None \<Rightarrow> True | Some b \<Rightarrow> b \<in> B)}"
lemma Func_Pfunc:
-"Func_option A B \<subseteq> Pfunc A B"
-unfolding Func_option_def Pfunc_def by auto
+ "Func_option A B \<subseteq> Pfunc A B"
+ unfolding Func_option_def Pfunc_def by auto
lemma Pfunc_Func_option:
-"Pfunc A B = (\<Union>A' \<in> Pow A. Func_option A' B)"
+ "Pfunc A B = (\<Union>A' \<in> Pow A. Func_option A' B)"
proof safe
fix f assume f: "f \<in> Pfunc A B"
show "f \<in> (\<Union>A'\<in>Pow A. Func_option A' B)"
@@ -1395,180 +1237,161 @@
qed
lemma card_of_Func_mono:
-fixes A1 A2 :: "'a set" and B :: "'b set"
-assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
-shows "|Func A1 B| \<le>o |Func A2 B|"
+ fixes A1 A2 :: "'a set" and B :: "'b set"
+ assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
+ shows "|Func A1 B| \<le>o |Func A2 B|"
proof-
obtain bb where bb: "bb \<in> B" using B by auto
define F where [abs_def]: "F f1 a =
(if a \<in> A2 then (if a \<in> A1 then f1 a else bb) else undefined)" for f1 :: "'a \<Rightarrow> 'b" and a
- show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI)
- show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe
+ show ?thesis unfolding card_of_ordLeq[symmetric]
+ proof(intro exI[of _ F] conjI)
+ show "inj_on F (Func A1 B)" unfolding inj_on_def
+ proof safe
fix f g assume f: "f \<in> Func A1 B" and g: "g \<in> Func A1 B" and eq: "F f = F g"
show "f = g"
proof(rule ext)
fix a show "f a = g a"
- proof(cases "a \<in> A1")
- case True
- thus ?thesis using eq A12 unfolding F_def fun_eq_iff
- by (elim allE[of _ a]) auto
- qed(insert f g, unfold Func_def, fastforce)
+ by (smt (verit) A12 F_def Func_def eq f g mem_Collect_eq subsetD)
qed
qed
qed(insert bb, unfold Func_def F_def, force)
qed
lemma card_of_Func_option_mono:
-fixes A1 A2 :: "'a set" and B :: "'b set"
-assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
-shows "|Func_option A1 B| \<le>o |Func_option A2 B|"
-by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func
- ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric)
+ fixes A1 A2 :: "'a set" and B :: "'b set"
+ assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
+ shows "|Func_option A1 B| \<le>o |Func_option A2 B|"
+ by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func
+ ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric)
lemma card_of_Pfunc_Pow_Func_option:
-assumes "B \<noteq> {}"
-shows "|Pfunc A B| \<le>o |Pow A \<times> Func_option A B|"
+ assumes "B \<noteq> {}"
+ shows "|Pfunc A B| \<le>o |Pow A \<times> Func_option A B|"
proof-
have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
unfolding Pfunc_Func_option by(rule card_of_refl)
also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A \<times> Func_option A B|"
- apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto
+ by (simp add: assms card_of_Func_option_mono card_of_Sigma_mono1)
finally show ?thesis .
qed
lemma Bpow_ordLeq_Func_Field:
-assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "\<not>finite A"
-shows "|Bpow r A| \<le>o |Func (Field r) A|"
+ assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "\<not>finite A"
+ shows "|Bpow r A| \<le>o |Func (Field r) A|"
proof-
let ?F = "\<lambda> f. {x | x a. f a = x \<and> a \<in> Field r}"
{fix X assume "X \<in> Bpow r A - {{}}"
- hence XA: "X \<subseteq> A" and "|X| \<le>o r"
- and X: "X \<noteq> {}" unfolding Bpow_def by auto
- hence "|X| \<le>o |Field r|" by (metis Field_card_of card_of_mono2)
- then obtain F where 1: "X = F ` (Field r)"
- using card_of_ordLeq2[OF X] by metis
- define f where [abs_def]: "f i = (if i \<in> Field r then F i else undefined)" for i
- have "\<exists> f \<in> Func (Field r) A. X = ?F f"
- apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto
+ hence XA: "X \<subseteq> A" and "|X| \<le>o r"
+ and X: "X \<noteq> {}" unfolding Bpow_def by auto
+ hence "|X| \<le>o |Field r|" by (metis Field_card_of card_of_mono2)
+ then obtain F where 1: "X = F ` (Field r)"
+ using card_of_ordLeq2[OF X] by metis
+ define f where [abs_def]: "f i = (if i \<in> Field r then F i else undefined)" for i
+ have "\<exists> f \<in> Func (Field r) A. X = ?F f"
+ apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto
}
hence "Bpow r A - {{}} \<subseteq> ?F ` (Func (Field r) A)" by auto
hence "|Bpow r A - {{}}| \<le>o |Func (Field r) A|"
- by (rule surj_imp_ordLeq)
+ by (rule surj_imp_ordLeq)
moreover
{have 2: "\<not>finite (Bpow r A)" using infinite_Bpow[OF rc r A] .
- have "|Bpow r A| =o |Bpow r A - {{}}|"
- by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
+ have "|Bpow r A| =o |Bpow r A - {{}}|"
+ by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
}
ultimately show ?thesis by (metis ordIso_ordLeq_trans)
qed
lemma empty_in_Func[simp]:
-"B \<noteq> {} \<Longrightarrow> (\<lambda>x. undefined) \<in> Func {} B"
-unfolding Func_def by auto
+ "B \<noteq> {} \<Longrightarrow> (\<lambda>x. undefined) \<in> Func {} B"
+ by simp
lemma Func_mono[simp]:
-assumes "B1 \<subseteq> B2"
-shows "Func A B1 \<subseteq> Func A B2"
-using assms unfolding Func_def by force
+ assumes "B1 \<subseteq> B2"
+ shows "Func A B1 \<subseteq> Func A B2"
+ using assms unfolding Func_def by force
lemma Pfunc_mono[simp]:
-assumes "A1 \<subseteq> A2" and "B1 \<subseteq> B2"
-shows "Pfunc A B1 \<subseteq> Pfunc A B2"
-using assms unfolding Pfunc_def
-apply safe
-apply (case_tac "x a", auto)
-apply (metis in_mono option.simps(5))
-done
+ assumes "A1 \<subseteq> A2" and "B1 \<subseteq> B2"
+ shows "Pfunc A B1 \<subseteq> Pfunc A B2"
+ using assms unfolding Pfunc_def
+ by (force split: option.split_asm option.split)
lemma card_of_Func_UNIV_UNIV:
-"|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \<Rightarrow> 'b) set|"
-using card_of_Func_UNIV[of "UNIV::'b set"] by auto
+ "|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \<Rightarrow> 'b) set|"
+ using card_of_Func_UNIV[of "UNIV::'b set"] by auto
lemma ordLeq_Func:
-assumes "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
-shows "|A| \<le>o |Func A B|"
-unfolding card_of_ordLeq[symmetric] proof(intro exI conjI)
- let ?F = "\<lambda> aa a. if a \<in> A then (if a = aa then b1 else b2) else undefined"
+ assumes "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
+ shows "|A| \<le>o |Func A B|"
+ unfolding card_of_ordLeq[symmetric] proof(intro exI conjI)
+ let ?F = "\<lambda>x a. if a \<in> A then (if a = x then b1 else b2) else undefined"
show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto
show "?F ` A \<subseteq> Func A B" using assms unfolding Func_def by auto
qed
lemma infinite_Func:
-assumes A: "\<not>finite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
-shows "\<not>finite (Func A B)"
-using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
+ assumes A: "\<not>finite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
+ shows "\<not>finite (Func A B)"
+ using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
subsection \<open>Infinite cardinals are limit ordinals\<close>
lemma card_order_infinite_isLimOrd:
-assumes c: "Card_order r" and i: "\<not>finite (Field r)"
-shows "isLimOrd r"
+ assumes c: "Card_order r" and i: "\<not>finite (Field r)"
+ shows "isLimOrd r"
proof-
have 0: "wo_rel r" and 00: "Well_order r"
- using c unfolding card_order_on_def wo_rel_def by auto
+ using c unfolding card_order_on_def wo_rel_def by auto
hence rr: "Refl r" by (metis wo_rel.REFL)
- show ?thesis unfolding wo_rel.isLimOrd_def[OF 0] wo_rel.isSuccOrd_def[OF 0] proof safe
- fix j assume j: "j \<in> Field r" and jm: "\<forall>i\<in>Field r. (i, j) \<in> r"
- define p where "p = Restr r (Field r - {j})"
- have fp: "Field p = Field r - {j}"
- unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto
- have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe
- fix a x assume a: "a \<in> Field p" and "x \<in> under r a"
- hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding under_def Field_def by auto
- moreover have a: "a \<noteq> j" "a \<in> Field r" "(a,j) \<in> r" using a jm unfolding fp by auto
- ultimately have "x \<noteq> j" using j jm by (metis 0 wo_rel.max2_def wo_rel.max2_equals1)
- thus "x \<in> Field p" using x unfolding fp by auto
- qed(unfold p_def Field_def, auto)
- have "p <o r" using j ofilter_ordLess[OF 00 of] unfolding fp p_def[symmetric] by auto
- hence 2: "|Field p| <o r" using c by (metis BNF_Cardinal_Order_Relation.ordLess_Field)
- have "|Field p| =o |Field r|" unfolding fp using i by (metis infinite_card_of_diff_singl)
- also have "|Field r| =o r"
- using c by (metis card_of_unique ordIso_symmetric)
- finally have "|Field p| =o r" .
- with 2 show False by (metis not_ordLess_ordIso)
+ show ?thesis unfolding wo_rel.isLimOrd_def[OF 0] wo_rel.isSuccOrd_def[OF 0]
+ proof safe
+ fix j assume "j \<in> Field r" and "\<forall>i\<in>Field r. (i, j) \<in> r"
+ then show False
+ by (metis Card_order_trans c i infinite_Card_order_limit)
qed
qed
lemma insert_Chain:
-assumes "Refl r" "C \<in> Chains r" and "i \<in> Field r" and "\<And>j. j \<in> C \<Longrightarrow> (j,i) \<in> r \<or> (i,j) \<in> r"
-shows "insert i C \<in> Chains r"
-using assms unfolding Chains_def by (auto dest: refl_onD)
+ assumes "Refl r" "C \<in> Chains r" and "i \<in> Field r" and "\<And>j. j \<in> C \<Longrightarrow> (j,i) \<in> r \<or> (i,j) \<in> r"
+ shows "insert i C \<in> Chains r"
+ using assms unfolding Chains_def by (auto dest: refl_onD)
lemma Collect_insert: "{R j |j. j \<in> insert j1 J} = insert (R j1) {R j |j. j \<in> J}"
-by auto
+ by auto
lemma Field_init_seg_of[simp]:
-"Field init_seg_of = UNIV"
-unfolding Field_def init_seg_of_def by auto
+ "Field init_seg_of = UNIV"
+ unfolding Field_def init_seg_of_def by auto
lemma refl_init_seg_of[intro, simp]: "refl init_seg_of"
-unfolding refl_on_def Field_def by auto
+ unfolding refl_on_def Field_def by auto
lemma regularCard_all_ex:
-assumes r: "Card_order r" "regularCard r"
-and As: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
-and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
-and cardB: "|B| <o r"
-shows "\<exists> i \<in> Field r. \<forall> b \<in> B. P i b"
+ assumes r: "Card_order r" "regularCard r"
+ and As: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
+ and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
+ and cardB: "|B| <o r"
+ shows "\<exists> i \<in> Field r. \<forall> b \<in> B. P i b"
proof-
let ?As = "\<lambda>i. {b \<in> B. P i b}"
have "\<exists>i \<in> Field r. B \<le> ?As i"
- apply(rule regularCard_UNION) using assms unfolding relChain_def by auto
+ apply(rule regularCard_UNION) using assms unfolding relChain_def by auto
thus ?thesis by auto
qed
lemma relChain_stabilize:
-assumes rc: "relChain r As" and AsB: "(\<Union>i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
-and ir: "\<not>finite (Field r)" and cr: "Card_order r"
-shows "\<exists> i \<in> Field r. As (succ r i) = As i"
+ assumes rc: "relChain r As" and AsB: "(\<Union>i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
+ and ir: "\<not>finite (Field r)" and cr: "Card_order r"
+ shows "\<exists> i \<in> Field r. As (succ r i) = As i"
proof(rule ccontr, auto)
have 0: "wo_rel r" and 00: "Well_order r"
- unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
+ unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
- using AsB L apply safe by (metis "0" UN_I subsetD wo_rel.isLimOrd_succ)
+ using AsB L by (simp add: "0" Sup_le_iff wo_rel.isLimOrd_succ)
assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
proof safe
@@ -1576,18 +1399,19 @@
hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)
hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
moreover
- {have "(i,succ r i) \<in> r" apply(rule wo_rel.succ_in[OF 0])
- using 1 unfolding aboveS_def by auto
- hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
+ { have "(i,succ r i) \<in> r"
+ by (meson "0" "1"(1) FieldI1 L wo_rel.isLimOrd_aboveS wo_rel.succ_in)
+ hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
}
ultimately show False unfolding Asij by auto
qed (insert rc, unfold relChain_def, auto)
hence "\<forall> i \<in> Field r. \<exists> a. a \<in> As (succ r i) - As i"
- using wo_rel.succ_in[OF 0] AsB
- by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem
- wo_rel.isLimOrd_aboveS wo_rel.succ_diff)
+ using wo_rel.succ_in[OF 0] AsB
+ by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem
+ wo_rel.isLimOrd_aboveS wo_rel.succ_diff)
then obtain f where f: "\<forall> i \<in> Field r. f i \<in> As (succ r i) - As i" by metis
- have "inj_on f (Field r)" unfolding inj_on_def proof safe
+ have "inj_on f (Field r)" unfolding inj_on_def
+ proof safe
fix i j assume ij: "i \<in> Field r" "j \<in> Field r" and fij: "f i = f j"
show "i = j"
proof(cases rule: wo_rel.cases_Total3[OF 0], safe)
@@ -1610,118 +1434,62 @@
subsection \<open>Regular vs. stable cardinals\<close>
-lemma stable_regularCard:
-assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
-shows "regularCard r"
-unfolding regularCard_def proof safe
- fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
- have "|K| \<le>o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans)
- moreover
- {assume Kr: "|K| <o r"
- then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
- using cof unfolding cofinal_def by metis
- hence "Field r \<subseteq> (\<Union>a \<in> K. underS r a)" unfolding underS_def by auto
- hence "r \<le>o |\<Union>a \<in> K. underS r a|" using cr
- by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
- also have "|\<Union>a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
- also
- {have "\<forall> a \<in> K. |underS r a| <o r" using K by (metis card_of_underS cr subsetD)
- hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
- }
- finally have "r <o r" .
- hence False by (metis ordLess_irreflexive)
- }
- ultimately show "|K| =o r" by (metis ordLeq_iff_ordLess_or_ordIso)
-qed
-
-lemma stable_natLeq: "stable natLeq"
-proof(unfold stable_def, safe)
- fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set"
- assume "|A| <o natLeq" and "\<forall>a\<in>A. |F a| <o natLeq"
- hence "finite A \<and> (\<forall>a \<in> A. finite(F a))"
- by (auto simp add: finite_iff_ordLess_natLeq)
- hence "finite(Sigma A F)" by (simp only: finite_SigmaI[of A F])
- thus "|Sigma A F | <o natLeq"
- by (auto simp add: finite_iff_ordLess_natLeq)
-qed
-
-corollary regularCard_natLeq: "regularCard natLeq"
-using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
-
lemma stable_cardSuc:
-assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
-shows "stable(cardSuc r)"
-using infinite_cardSuc_regularCard regularCard_stable
-by (metis CARD INF cardSuc_Card_order cardSuc_finite)
-
-lemma stable_ordIso1:
-assumes ST: "stable r" and ISO: "r' =o r"
-shows "stable r'"
-proof(unfold stable_def, auto)
- fix A::"'b set" and F::"'b \<Rightarrow> 'b set"
- assume "|A| <o r'" and "\<forall>a \<in> A. |F a| <o r'"
- hence "( |A| <o r) \<and> (\<forall>a \<in> A. |F a| <o r)"
- using ISO ordLess_ordIso_trans by blast
- hence "|SIGMA a : A. F a| <o r" using assms stable_elim by blast
- thus "|SIGMA a : A. F a| <o r'"
- using ISO ordIso_symmetric ordLess_ordIso_trans by blast
-qed
-
-lemma stable_ordIso2:
-assumes ST: "stable r" and ISO: "r =o r'"
-shows "stable r'"
-using assms stable_ordIso1 ordIso_symmetric by blast
+ assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
+ shows "stable(cardSuc r)"
+ using infinite_cardSuc_regularCard regularCard_stable
+ by (metis CARD INF cardSuc_Card_order cardSuc_finite)
lemma stable_ordIso:
-assumes "r =o r'"
-shows "stable r = stable r'"
-using assms stable_ordIso1 stable_ordIso2 by blast
+ assumes "r =o r'"
+ shows "stable r = stable r'"
+ by (metis assms ordIso_symmetric stable_ordIso1)
lemma stable_nat: "stable |UNIV::nat set|"
-using stable_natLeq card_of_nat stable_ordIso by auto
+ using stable_natLeq card_of_nat stable_ordIso by auto
text\<open>Below, the type of "A" is not important -- we just had to choose an appropriate
type to make "A" possible. What is important is that arbitrarily large
infinite sets of stable cardinality exist.\<close>
lemma infinite_stable_exists:
-assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
-shows "\<exists>(A :: (nat + 'a set)set).
+ assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
+ shows "\<exists>(A :: (nat + 'a set)set).
\<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"
proof-
have "\<exists>(A :: (nat + 'a set)set).
\<not>finite A \<and> stable |A| \<and> |UNIV::'a set| <o |A|"
proof(cases "finite (UNIV::'a set)")
- assume Case1: "finite (UNIV::'a set)"
+ case True
let ?B = "UNIV::nat set"
have "\<not>finite(?B <+> {})" using finite_Plus_iff by blast
moreover
have "stable |?B|" using stable_natLeq card_of_nat stable_ordIso1 by blast
hence "stable |?B <+> {}|" using stable_ordIso card_of_Plus_empty1 by blast
moreover
- have "\<not>finite(Field |?B| ) \<and> finite(Field |UNIV::'a set| )" using Case1 by simp
+ have "\<not>finite(Field |?B| ) \<and> finite(Field |UNIV::'a set| )" using True by simp
hence "|UNIV::'a set| <o |?B|" by (simp add: finite_ordLess_infinite)
hence "|UNIV::'a set| <o |?B <+> {}|" using card_of_Plus_empty1 ordLess_ordIso_trans by blast
ultimately show ?thesis by blast
next
- assume Case1: "\<not>finite (UNIV::'a set)"
+ case False
hence *: "\<not>finite(Field |UNIV::'a set| )" by simp
let ?B = "Field(cardSuc |UNIV::'a set| )"
have 0: "|?B| =o |{} <+> ?B|" using card_of_Plus_empty2 by blast
- have 1: "\<not>finite ?B" using Case1 card_of_cardSuc_finite by blast
+ have 1: "\<not>finite ?B" using False card_of_cardSuc_finite by blast
hence 2: "\<not>finite({} <+> ?B)" using 0 card_of_ordIso_finite by blast
have "|?B| =o cardSuc |UNIV::'a set|"
- using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
+ using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
moreover have "stable(cardSuc |UNIV::'a set| )"
- using stable_cardSuc * card_of_Card_order by blast
+ using stable_cardSuc * card_of_Card_order by blast
ultimately have "stable |?B|" using stable_ordIso by blast
hence 3: "stable |{} <+> ?B|" using stable_ordIso 0 by blast
have "|UNIV::'a set| <o cardSuc |UNIV::'a set|"
- using card_of_Card_order cardSuc_greater by blast
+ using card_of_Card_order cardSuc_greater by blast
moreover have "|?B| =o cardSuc |UNIV::'a set|"
- using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
+ using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
ultimately have "|UNIV::'a set| <o |?B|"
- using ordIso_symmetric ordLess_ordIso_trans by blast
+ using ordIso_symmetric ordLess_ordIso_trans by blast
hence "|UNIV::'a set| <o |{} <+> ?B|" using 0 ordLess_ordIso_trans by blast
thus ?thesis using 2 3 by blast
qed
@@ -1729,9 +1497,9 @@
qed
corollary infinite_regularCard_exists:
-assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
-shows "\<exists>(A :: (nat + 'a set)set).
+ assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
+ shows "\<exists>(A :: (nat + 'a set)set).
\<not>finite A \<and> regularCard |A| \<and> (\<forall>r \<in> R. r <o |A| )"
-using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)
+ using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)
end
--- a/src/HOL/Cardinals/Fun_More.thy Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Cardinals/Fun_More.thy Thu Jan 12 17:12:36 2023 +0000
@@ -8,44 +8,20 @@
section \<open>More on Injections, Bijections and Inverses\<close>
theory Fun_More
-imports Main
+ imports Main
begin
subsection \<open>Purely functional properties\<close>
(* unused *)
-(*1*)lemma notIn_Un_bij_betw2:
-assumes NIN: "b \<notin> A" and NIN': "b' \<notin> A'" and
- BIJ: "bij_betw f A A'"
-shows "bij_betw f (A \<union> {b}) (A' \<union> {b'}) = (f b = b')"
-proof
- assume "f b = b'"
- thus "bij_betw f (A \<union> {b}) (A' \<union> {b'})"
- using assms notIn_Un_bij_betw[of b A f A'] by auto
-next
- assume *: "bij_betw f (A \<union> {b}) (A' \<union> {b'})"
- hence "f b \<in> A' \<union> {b'}"
- unfolding bij_betw_def by auto
- moreover
- {assume "f b \<in> A'"
- then obtain b1 where 1: "b1 \<in> A" and 2: "f b1 = f b" using BIJ
- by (auto simp add: bij_betw_def)
- hence "b = b1" using *
- by (auto simp add: bij_betw_def inj_on_def)
- with 1 NIN have False by auto
- }
- ultimately show "f b = b'" by blast
-qed
-
-(* unused *)
(*1*)lemma bij_betw_diff_singl:
-assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
-shows "bij_betw f (A - {a}) (A' - {f a})"
+ assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
+ shows "bij_betw f (A - {a}) (A' - {f a})"
proof-
let ?B = "A - {a}" let ?B' = "A' - {f a}"
have "f a \<in> A'" using IN BIJ unfolding bij_betw_def by blast
hence "a \<notin> ?B \<and> f a \<notin> ?B' \<and> A = ?B \<union> {a} \<and> A' = ?B' \<union> {f a}"
- using IN by blast
+ using IN by blast
thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp
qed
@@ -54,120 +30,62 @@
(* unused *)
(*1*)lemma bij_betw_inv_into_RIGHT:
-assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'"
-shows "f `((inv_into A f)`B') = B'"
-using assms
-proof(auto simp add: bij_betw_inv_into_right)
- let ?f' = "(inv_into A f)"
- fix a' assume *: "a' \<in> B'"
- hence "a' \<in> A'" using SUB by auto
- hence "a' = f (?f' a')"
- using BIJ by (auto simp add: bij_betw_inv_into_right)
- thus "a' \<in> f ` (?f' ` B')" using * by blast
-qed
+ assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'"
+ shows "f `((inv_into A f)`B') = B'"
+ by (metis BIJ SUB bij_betw_imp_surj_on image_inv_into_cancel)
+
(* unused *)
(*1*)lemma bij_betw_inv_into_RIGHT_LEFT:
-assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'" and
- IM: "(inv_into A f) ` B' = B"
-shows "f ` B = B'"
-proof-
- have "f`((inv_into A f)` B') = B'"
- using assms bij_betw_inv_into_RIGHT[of f A A' B'] by auto
- thus ?thesis using IM by auto
-qed
+ assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'" and
+ IM: "(inv_into A f) ` B' = B"
+ shows "f ` B = B'"
+ by (metis BIJ IM SUB bij_betw_inv_into_RIGHT)
(* unused *)
(*2*)lemma bij_betw_inv_into_twice:
-assumes "bij_betw f A A'"
-shows "\<forall>a \<in> A. inv_into A' (inv_into A f) a = f a"
-proof
- let ?f' = "inv_into A f" let ?f'' = "inv_into A' ?f'"
- have 1: "bij_betw ?f' A' A" using assms
- by (auto simp add: bij_betw_inv_into)
- fix a assume *: "a \<in> A"
- then obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
- using 1 unfolding bij_betw_def by force
- hence "?f'' a = a'"
- using * 1 3 by (auto simp add: bij_betw_inv_into_left)
- moreover have "f a = a'" using assms 2 3
- by (auto simp add: bij_betw_inv_into_right)
- ultimately show "?f'' a = f a" by simp
-qed
+ assumes "bij_betw f A A'"
+ shows "\<forall>a \<in> A. inv_into A' (inv_into A f) a = f a"
+ by (simp add: assms inv_into_inv_into_eq)
subsection \<open>Properties involving Hilbert choice\<close>
(*1*)lemma bij_betw_inv_into_LEFT:
-assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A"
-shows "(inv_into A f)`(f ` B) = B"
-using assms unfolding bij_betw_def using inv_into_image_cancel by force
+ assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A"
+ shows "(inv_into A f)`(f ` B) = B"
+ using assms unfolding bij_betw_def using inv_into_image_cancel by force
(*1*)lemma bij_betw_inv_into_LEFT_RIGHT:
-assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" and
- IM: "f ` B = B'"
-shows "(inv_into A f) ` B' = B"
-using assms bij_betw_inv_into_LEFT[of f A A' B] by fast
+ assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" and
+ IM: "f ` B = B'"
+ shows "(inv_into A f) ` B' = B"
+ using assms bij_betw_inv_into_LEFT[of f A A' B] by fast
subsection \<open>Other facts\<close>
(*3*)lemma atLeastLessThan_injective:
-assumes "{0 ..< m::nat} = {0 ..< n}"
-shows "m = n"
-proof-
- {assume "m < n"
- hence "m \<in> {0 ..< n}" by auto
- hence "{0 ..< m} < {0 ..< n}" by auto
- hence False using assms by blast
- }
- moreover
- {assume "n < m"
- hence "n \<in> {0 ..< m}" by auto
- hence "{0 ..< n} < {0 ..< m}" by auto
- hence False using assms by blast
- }
- ultimately show ?thesis by force
-qed
+ assumes "{0 ..< m::nat} = {0 ..< n}"
+ shows "m = n"
+ using assms atLeast0LessThan by force
(*2*)lemma atLeastLessThan_injective2:
-"bij_betw f {0 ..< m::nat} {0 ..< n} \<Longrightarrow> m = n"
-using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
- card_atLeastLessThan[of m] card_atLeastLessThan[of n]
- bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto
+ "bij_betw f {0 ..< m::nat} {0 ..< n} \<Longrightarrow> m = n"
+ using bij_betw_same_card by fastforce
(*2*)lemma atLeastLessThan_less_eq:
-"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
-unfolding ivl_subset by arith
+ "({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
+ by auto
(*2*)lemma atLeastLessThan_less_eq2:
-assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}"
-shows "m \<le> n"
-using assms
-using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
- card_atLeastLessThan[of m] card_atLeastLessThan[of n]
- card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
-
-(* unused *)
-(*2*)lemma atLeastLessThan_less_eq3:
-"(\<exists>f. inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}) = (m \<le> n)"
-using atLeastLessThan_less_eq2
-proof(auto)
- assume "m \<le> n"
- hence "inj_on id {0..<m} \<and> id ` {0..<m} \<subseteq> {0..<n}" unfolding inj_on_def by force
- thus "\<exists>f. inj_on f {0..<m} \<and> f ` {0..<m} \<subseteq> {0..<n}" by blast
-qed
+ assumes "inj_on f {0..<(m::nat)}" "f ` {0..<m} \<le> {0..<n}"
+ shows "m \<le> n"
+ by (metis assms card_inj_on_le card_lessThan finite_lessThan lessThan_atLeast0)
(* unused *)
(*3*)lemma atLeastLessThan_less:
-"({0..<m} < {0..<n}) = ((m::nat) < n)"
-proof-
- have "({0..<m} < {0..<n}) = ({0..<m} \<le> {0..<n} \<and> {0..<m} ~= {0..<n})"
- using subset_iff_psubset_eq by blast
- also have "\<dots> = (m \<le> n \<and> m ~= n)"
- using atLeastLessThan_less_eq atLeastLessThan_injective by blast
- also have "\<dots> = (m < n)" by auto
- finally show ?thesis .
-qed
+ "({0..<m} < {0..<n}) = ((m::nat) < n)"
+ by auto
end
--- a/src/HOL/Cardinals/Order_Relation_More.thy Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Cardinals/Order_Relation_More.thy Thu Jan 12 17:12:36 2023 +0000
@@ -8,57 +8,57 @@
section \<open>Basics on Order-Like Relations\<close>
theory Order_Relation_More
-imports Main
+ imports Main
begin
subsection \<open>The upper and lower bounds operators\<close>
lemma aboveS_subset_above: "aboveS r a \<le> above r a"
-by(auto simp add: aboveS_def above_def)
+ by(auto simp add: aboveS_def above_def)
lemma AboveS_subset_Above: "AboveS r A \<le> Above r A"
-by(auto simp add: AboveS_def Above_def)
+ by(auto simp add: AboveS_def Above_def)
lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
-by(auto simp add: UnderS_def)
+ by(auto simp add: UnderS_def)
lemma aboveS_notIn: "a \<notin> aboveS r a"
-by(auto simp add: aboveS_def)
+ by(auto simp add: aboveS_def)
lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above r a"
-by(auto simp add: refl_on_def above_def)
+ by(auto simp add: refl_on_def above_def)
lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above r (under r a)"
-by(auto simp add: Above_def under_def)
+ by(auto simp add: Above_def under_def)
lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under r (above r a)"
-by(auto simp add: Under_def above_def)
+ by(auto simp add: Under_def above_def)
lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS r (aboveS r a)"
-by(auto simp add: UnderS_def aboveS_def)
+ by(auto simp add: UnderS_def aboveS_def)
lemma UnderS_subset_Under: "UnderS r A \<le> Under r A"
-by(auto simp add: UnderS_def Under_def)
+ by(auto simp add: UnderS_def Under_def)
lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above r (Under r B)"
-by(auto simp add: Above_def Under_def)
+ by(auto simp add: Above_def Under_def)
lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under r (Above r B)"
-by(auto simp add: Under_def Above_def)
+ by(auto simp add: Under_def Above_def)
lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS r (UnderS r B)"
-by(auto simp add: AboveS_def UnderS_def)
+ by(auto simp add: AboveS_def UnderS_def)
lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS r (AboveS r B)"
-by(auto simp add: UnderS_def AboveS_def)
+ by(auto simp add: UnderS_def AboveS_def)
lemma Under_Above_Galois:
-"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above r C) = (C \<le> Under r B)"
-by(unfold Above_def Under_def, blast)
+ "\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above r C) = (C \<le> Under r B)"
+ by(unfold Above_def Under_def, blast)
lemma UnderS_AboveS_Galois:
-"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS r C) = (C \<le> UnderS r B)"
-by(unfold AboveS_def UnderS_def, blast)
+ "\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS r C) = (C \<le> UnderS r B)"
+ by(unfold AboveS_def UnderS_def, blast)
lemma Refl_above_aboveS:
assumes REFL: "Refl r" and IN: "a \<in> Field r"
@@ -79,20 +79,20 @@
with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
have "(a,b) \<in> r \<or> a = b" by blast
thus "(a,b) \<in> r"
- using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
+ using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
next
fix b assume "(b, a) \<in> r"
thus "b \<in> Field r"
- using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
+ using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
next
fix b assume "b \<noteq> a" "(a, b) \<in> r"
thus "b \<in> Field r"
- using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
+ using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
qed
lemma Linear_order_underS_above_Field:
-assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
-shows "Field r = underS r a \<union> above r a"
+ assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
+ shows "Field r = underS r a \<union> above r a"
proof(unfold underS_def above_def, auto)
assume "a \<in> Field r" "(a, a) \<notin> r"
with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
@@ -102,174 +102,174 @@
with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
have "(b,a) \<in> r \<or> b = a" by blast
thus "(b,a) \<in> r"
- using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
+ using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
next
fix b assume "b \<noteq> a" "(b, a) \<in> r"
thus "b \<in> Field r"
- using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
+ using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
next
fix b assume "(a, b) \<in> r"
thus "b \<in> Field r"
- using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
+ using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
qed
lemma under_empty: "a \<notin> Field r \<Longrightarrow> under r a = {}"
-unfolding Field_def under_def by auto
+ unfolding Field_def under_def by auto
lemma Under_Field: "Under r A \<le> Field r"
-by(unfold Under_def Field_def, auto)
+ by(unfold Under_def Field_def, auto)
lemma UnderS_Field: "UnderS r A \<le> Field r"
-by(unfold UnderS_def Field_def, auto)
+ by(unfold UnderS_def Field_def, auto)
lemma above_Field: "above r a \<le> Field r"
-by(unfold above_def Field_def, auto)
+ by(unfold above_def Field_def, auto)
lemma aboveS_Field: "aboveS r a \<le> Field r"
-by(unfold aboveS_def Field_def, auto)
+ by(unfold aboveS_def Field_def, auto)
lemma Above_Field: "Above r A \<le> Field r"
-by(unfold Above_def Field_def, auto)
+ by(unfold Above_def Field_def, auto)
lemma Refl_under_Under:
-assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Under r A = (\<Inter>a \<in> A. under r a)"
+ assumes REFL: "Refl r" and NE: "A \<noteq> {}"
+ shows "Under r A = (\<Inter>a \<in> A. under r a)"
proof
show "Under r A \<subseteq> (\<Inter>a \<in> A. under r a)"
- by(unfold Under_def under_def, auto)
+ by(unfold Under_def under_def, auto)
next
show "(\<Inter>a \<in> A. under r a) \<subseteq> Under r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> under r xa"
hence "\<forall>xa \<in> A. (x,xa) \<in> r"
- by (simp add: under_def)
+ by (simp add: under_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> under r a" by simp
- hence "x \<in> Field r"
- using under_Field[of r a] by auto
+ with * have "x \<in> under r a" by simp
+ hence "x \<in> Field r"
+ using under_Field[of r a] by auto
}
ultimately show "x \<in> Under r A"
- unfolding Under_def by auto
+ unfolding Under_def by auto
qed
qed
lemma Refl_underS_UnderS:
-assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "UnderS r A = (\<Inter>a \<in> A. underS r a)"
+ assumes REFL: "Refl r" and NE: "A \<noteq> {}"
+ shows "UnderS r A = (\<Inter>a \<in> A. underS r a)"
proof
show "UnderS r A \<subseteq> (\<Inter>a \<in> A. underS r a)"
- by(unfold UnderS_def underS_def, auto)
+ by(unfold UnderS_def underS_def, auto)
next
show "(\<Inter>a \<in> A. underS r a) \<subseteq> UnderS r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
hence "\<forall>xa \<in> A. x \<noteq> xa \<and> (x,xa) \<in> r"
- by (auto simp add: underS_def)
+ by (auto simp add: underS_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> underS r a" by simp
- hence "x \<in> Field r"
- using underS_Field[of _ r a] by auto
+ with * have "x \<in> underS r a" by simp
+ hence "x \<in> Field r"
+ using underS_Field[of _ r a] by auto
}
ultimately show "x \<in> UnderS r A"
- unfolding UnderS_def by auto
+ unfolding UnderS_def by auto
qed
qed
lemma Refl_above_Above:
-assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Above r A = (\<Inter>a \<in> A. above r a)"
+ assumes REFL: "Refl r" and NE: "A \<noteq> {}"
+ shows "Above r A = (\<Inter>a \<in> A. above r a)"
proof
show "Above r A \<subseteq> (\<Inter>a \<in> A. above r a)"
- by(unfold Above_def above_def, auto)
+ by(unfold Above_def above_def, auto)
next
show "(\<Inter>a \<in> A. above r a) \<subseteq> Above r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> above r xa"
hence "\<forall>xa \<in> A. (xa,x) \<in> r"
- by (simp add: above_def)
+ by (simp add: above_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> above r a" by simp
- hence "x \<in> Field r"
- using above_Field[of r a] by auto
+ with * have "x \<in> above r a" by simp
+ hence "x \<in> Field r"
+ using above_Field[of r a] by auto
}
ultimately show "x \<in> Above r A"
- unfolding Above_def by auto
+ unfolding Above_def by auto
qed
qed
lemma Refl_aboveS_AboveS:
-assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "AboveS r A = (\<Inter>a \<in> A. aboveS r a)"
+ assumes REFL: "Refl r" and NE: "A \<noteq> {}"
+ shows "AboveS r A = (\<Inter>a \<in> A. aboveS r a)"
proof
show "AboveS r A \<subseteq> (\<Inter>a \<in> A. aboveS r a)"
- by(unfold AboveS_def aboveS_def, auto)
+ by(unfold AboveS_def aboveS_def, auto)
next
show "(\<Inter>a \<in> A. aboveS r a) \<subseteq> AboveS r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
hence "\<forall>xa \<in> A. xa \<noteq> x \<and> (xa,x) \<in> r"
- by (auto simp add: aboveS_def)
+ by (auto simp add: aboveS_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> aboveS r a" by simp
- hence "x \<in> Field r"
- using aboveS_Field[of r a] by auto
+ with * have "x \<in> aboveS r a" by simp
+ hence "x \<in> Field r"
+ using aboveS_Field[of r a] by auto
}
ultimately show "x \<in> AboveS r A"
- unfolding AboveS_def by auto
+ unfolding AboveS_def by auto
qed
qed
lemma under_Under_singl: "under r a = Under r {a}"
-by(unfold Under_def under_def, auto simp add: Field_def)
+ by(unfold Under_def under_def, auto simp add: Field_def)
lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
-by(unfold UnderS_def underS_def, auto simp add: Field_def)
+ by(unfold UnderS_def underS_def, auto simp add: Field_def)
lemma above_Above_singl: "above r a = Above r {a}"
-by(unfold Above_def above_def, auto simp add: Field_def)
+ by(unfold Above_def above_def, auto simp add: Field_def)
lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
-by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
+ by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
lemma Under_decr: "A \<le> B \<Longrightarrow> Under r B \<le> Under r A"
-by(unfold Under_def, auto)
+ by(unfold Under_def, auto)
lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS r B \<le> UnderS r A"
-by(unfold UnderS_def, auto)
+ by(unfold UnderS_def, auto)
lemma Above_decr: "A \<le> B \<Longrightarrow> Above r B \<le> Above r A"
-by(unfold Above_def, auto)
+ by(unfold Above_def, auto)
lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS r B \<le> AboveS r A"
-by(unfold AboveS_def, auto)
+ by(unfold AboveS_def, auto)
lemma under_incl_iff:
-assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \<in> Field r"
-shows "(under r a \<le> under r b) = ((a,b) \<in> r)"
+ assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \<in> Field r"
+ shows "(under r a \<le> under r b) = ((a,b) \<in> r)"
proof
assume "(a,b) \<in> r"
thus "under r a \<le> under r b" using TRANS
- by (auto simp add: under_incr)
+ by (auto simp add: under_incr)
next
assume "under r a \<le> under r b"
moreover
have "a \<in> under r a" using REFL IN
- by (auto simp add: Refl_under_in)
+ by (auto simp add: Refl_under_in)
ultimately show "(a,b) \<in> r"
- by (auto simp add: under_def)
+ by (auto simp add: under_def)
qed
lemma above_decr:
-assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
-shows "above r b \<le> above r a"
+ assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
+ shows "above r b \<le> above r a"
proof(unfold above_def, auto)
fix x assume "(b,x) \<in> r"
with REL TRANS trans_def[of r]
@@ -277,9 +277,9 @@
qed
lemma aboveS_decr:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- REL: "(a,b) \<in> r"
-shows "aboveS r b \<le> aboveS r a"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ REL: "(a,b) \<in> r"
+ shows "aboveS r b \<le> aboveS r a"
proof(unfold aboveS_def, auto)
assume *: "a \<noteq> b" and **: "(b,a) \<in> r"
with ANTISYM antisym_def[of r] REL
@@ -291,26 +291,26 @@
qed
lemma under_trans:
-assumes TRANS: "trans r" and
- IN1: "a \<in> under r b" and IN2: "b \<in> under r c"
-shows "a \<in> under r c"
+ assumes TRANS: "trans r" and
+ IN1: "a \<in> under r b" and IN2: "b \<in> under r c"
+ shows "a \<in> under r c"
proof-
have "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 under_def by fastforce
+ using IN1 IN2 under_def by fastforce
hence "(a,c) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
thus ?thesis unfolding under_def by simp
qed
lemma under_underS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> under r b" and IN2: "b \<in> underS r c"
-shows "a \<in> underS r c"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> under r b" and IN2: "b \<in> underS r c"
+ shows "a \<in> underS r c"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 under_def underS_def by fastforce
+ using IN1 IN2 under_def underS_def by fastforce
hence 1: "(a,c) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
have 2: "b \<noteq> c" using IN2 underS_def by force
have 3: "a \<noteq> c"
proof
@@ -321,14 +321,14 @@
qed
lemma underS_under_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS r b" and IN2: "b \<in> under r c"
-shows "a \<in> underS r c"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> underS r b" and IN2: "b \<in> under r c"
+ shows "a \<in> underS r c"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 under_def underS_def by fast
+ using IN1 IN2 under_def underS_def by fast
hence 1: "(a,c) \<in> r"
- using TRANS trans_def[of r] by fast
+ using TRANS trans_def[of r] by fast
have 2: "a \<noteq> b" using IN1 underS_def by force
have 3: "a \<noteq> c"
proof
@@ -339,36 +339,36 @@
qed
lemma underS_underS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS r b" and IN2: "b \<in> underS r c"
-shows "a \<in> underS r c"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> underS r b" and IN2: "b \<in> underS r c"
+ shows "a \<in> underS r c"
proof-
have "a \<in> under r b"
- using IN1 underS_subset_under by fast
+ using IN1 underS_subset_under by fast
with assms under_underS_trans show ?thesis by fast
qed
lemma above_trans:
-assumes TRANS: "trans r" and
- IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
-shows "c \<in> above r a"
+ assumes TRANS: "trans r" and
+ IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
+ shows "c \<in> above r a"
proof-
have "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 above_def by fast
+ using IN1 IN2 above_def by fast
hence "(a,c) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
thus ?thesis unfolding above_def by simp
qed
lemma above_aboveS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
-shows "c \<in> aboveS r a"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
+ shows "c \<in> aboveS r a"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 above_def aboveS_def by fast
+ using IN1 IN2 above_def aboveS_def by fast
hence 1: "(a,c) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
have 2: "b \<noteq> c" using IN2 aboveS_def by force
have 3: "a \<noteq> c"
proof
@@ -379,14 +379,14 @@
qed
lemma aboveS_above_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
-shows "c \<in> aboveS r a"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
+ shows "c \<in> aboveS r a"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 above_def aboveS_def by fast
+ using IN1 IN2 above_def aboveS_def by fast
hence 1: "(a,c) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
have 2: "a \<noteq> b" using IN1 aboveS_def by force
have 3: "a \<noteq> c"
proof
@@ -397,26 +397,26 @@
qed
lemma aboveS_aboveS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
-shows "c \<in> aboveS r a"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
+ shows "c \<in> aboveS r a"
proof-
have "b \<in> above r a"
- using IN1 aboveS_subset_above by fast
+ using IN1 aboveS_subset_above by fast
with assms above_aboveS_trans show ?thesis by fast
qed
lemma under_Under_trans:
-assumes TRANS: "trans r" and
- IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
-shows "a \<in> Under r C"
+ assumes TRANS: "trans r" and
+ IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
+ shows "a \<in> Under r C"
proof-
have "b \<in> {u \<in> Field r. \<forall>x. x \<in> C \<longrightarrow> (u, x) \<in> r}"
using IN2 Under_def by force
hence "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
using IN1 under_def by fast
hence "\<forall>c \<in> C. (a,c) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
moreover
have "a \<in> Field r" using IN1 unfolding Field_def under_def by blast
ultimately
@@ -424,53 +424,53 @@
qed
lemma underS_Under_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
-shows "a \<in> UnderS r C"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
+ shows "a \<in> UnderS r C"
proof-
from IN1 have "a \<in> under r b"
- using underS_subset_under[of r b] by fast
+ using underS_subset_under[of r b] by fast
with assms under_Under_trans
have "a \<in> Under r C" by fast
- (* *)
+ (* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "b \<noteq> a \<and> (a,b) \<in> r"
- using IN1 underS_def[of r b] by auto
+ using IN1 underS_def[of r b] by auto
have "\<forall>c \<in> C. (b,c) \<in> r"
- using IN2 Under_def[of r C] by auto
+ using IN2 Under_def[of r C] by auto
with * have "(b,a) \<in> r" by simp
with 1 ANTISYM antisym_def[of r]
show False by blast
qed
- (* *)
+ (* *)
ultimately
show ?thesis unfolding UnderS_def
- using Under_def by force
+ using Under_def by force
qed
lemma underS_UnderS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
-shows "a \<in> UnderS r C"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
+ shows "a \<in> UnderS r C"
proof-
from IN2 have "b \<in> Under r C"
- using UnderS_subset_Under[of r C] by blast
+ using UnderS_subset_Under[of r C] by blast
with underS_Under_trans assms
show ?thesis by force
qed
lemma above_Above_trans:
-assumes TRANS: "trans r" and
- IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
-shows "a \<in> Above r C"
+ assumes TRANS: "trans r" and
+ IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
+ shows "a \<in> Above r C"
proof-
have "(b,a) \<in> r \<and> (\<forall>c \<in> C. (c,b) \<in> r)"
using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
hence "\<forall>c \<in> C. (c,a) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
moreover
have "a \<in> Field r" using IN1[unfolded above_def] Field_def by fast
ultimately
@@ -478,95 +478,95 @@
qed
lemma aboveS_Above_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
-shows "a \<in> AboveS r C"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
+ shows "a \<in> AboveS r C"
proof-
from IN1 have "a \<in> above r b"
- using aboveS_subset_above[of r b] by blast
+ using aboveS_subset_above[of r b] by blast
with assms above_Above_trans
have "a \<in> Above r C" by fast
- (* *)
+ (* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "b \<noteq> a \<and> (b,a) \<in> r"
- using IN1 aboveS_def[of r b] by auto
+ using IN1 aboveS_def[of r b] by auto
have "\<forall>c \<in> C. (c,b) \<in> r"
- using IN2 Above_def[of r C] by auto
+ using IN2 Above_def[of r C] by auto
with * have "(a,b) \<in> r" by simp
with 1 ANTISYM antisym_def[of r]
show False by blast
qed
- (* *)
+ (* *)
ultimately
show ?thesis unfolding AboveS_def
- using Above_def by force
+ using Above_def by force
qed
lemma above_AboveS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
-shows "a \<in> AboveS r C"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
+ shows "a \<in> AboveS r C"
proof-
from IN2 have "b \<in> Above r C"
- using AboveS_subset_Above[of r C] by blast
+ using AboveS_subset_Above[of r C] by blast
with assms above_Above_trans
have "a \<in> Above r C" by force
- (* *)
+ (* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "(b,a) \<in> r"
- using IN1 above_def[of r b] by auto
+ using IN1 above_def[of r b] by auto
have "\<forall>c \<in> C. b \<noteq> c \<and> (c,b) \<in> r"
- using IN2 AboveS_def[of r C] by auto
+ using IN2 AboveS_def[of r C] by auto
with * have "b \<noteq> a \<and> (a,b) \<in> r" by simp
with 1 ANTISYM antisym_def[of r]
show False by blast
qed
- (* *)
+ (* *)
ultimately
show ?thesis unfolding AboveS_def
- using Above_def by force
+ using Above_def by force
qed
lemma aboveS_AboveS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
-shows "a \<in> AboveS r C"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
+ shows "a \<in> AboveS r C"
proof-
from IN2 have "b \<in> Above r C"
- using AboveS_subset_Above[of r C] by blast
+ using AboveS_subset_Above[of r C] by blast
with aboveS_Above_trans assms
show ?thesis by force
qed
lemma under_UnderS_trans:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
-shows "a \<in> UnderS r C"
+ assumes TRANS: "trans r" and ANTISYM: "antisym r" and
+ IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
+ shows "a \<in> UnderS r C"
proof-
from IN2 have "b \<in> Under r C"
- using UnderS_subset_Under[of r C] by blast
+ using UnderS_subset_Under[of r C] by blast
with assms under_Under_trans
have "a \<in> Under r C" by force
- (* *)
+ (* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "(a,b) \<in> r"
- using IN1 under_def[of r b] by auto
+ using IN1 under_def[of r b] by auto
have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
- using IN2 UnderS_def[of r C] by blast
+ using IN2 UnderS_def[of r C] by blast
with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
with 1 ANTISYM antisym_def[of r]
show False by blast
qed
- (* *)
+ (* *)
ultimately
show ?thesis unfolding UnderS_def Under_def by fast
qed
@@ -575,12 +575,12 @@
subsection \<open>Properties depending on more than one relation\<close>
lemma under_incr2:
-"r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
-unfolding under_def by blast
+ "r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
+ unfolding under_def by blast
lemma underS_incr2:
-"r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
-unfolding underS_def by blast
+ "r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
+ unfolding underS_def by blast
(* FIXME: r \<leadsto> r'
lemma Under_incr:
@@ -601,12 +601,12 @@
*)
lemma above_incr2:
-"r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
-unfolding above_def by blast
+ "r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
+ unfolding above_def by blast
lemma aboveS_incr2:
-"r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
-unfolding aboveS_def by blast
+ "r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
+ unfolding aboveS_def by blast
(* FIXME
lemma Above_incr:
--- a/src/HOL/Cardinals/Order_Union.thy Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Cardinals/Order_Union.thy Thu Jan 12 17:12:36 2023 +0000
@@ -7,7 +7,7 @@
section \<open>Order Union\<close>
theory Order_Union
-imports Main
+ imports Main
begin
definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60) where
@@ -19,10 +19,10 @@
unfolding Osum_def Field_def by blast
lemma Osum_wf:
-assumes FLD: "Field r Int Field r' = {}" and
- WF: "wf r" and WF': "wf r'"
-shows "wf (r Osum r')"
-unfolding wf_eq_minimal2 unfolding Field_Osum
+ assumes FLD: "Field r Int Field r' = {}" and
+ WF: "wf r" and WF': "wf r'"
+ shows "wf (r Osum r')"
+ unfolding wf_eq_minimal2 unfolding Field_Osum
proof(intro allI impI, elim conjE)
fix A assume *: "A \<subseteq> Field r \<union> Field r'" and **: "A \<noteq> {}"
obtain B where B_def: "B = A Int Field r" by blast
@@ -31,26 +31,26 @@
assume Case1: "B \<noteq> {}"
hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto
then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r"
- using WF unfolding wf_eq_minimal2 by blast
+ using WF unfolding wf_eq_minimal2 by blast
hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto
- (* *)
+ (* *)
have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'"
proof(intro ballI)
fix a1 assume **: "a1 \<in> A"
{assume Case11: "a1 \<in> Field r"
- hence "(a1,a) \<notin> r" using B_def ** 2 by auto
- moreover
- have "(a1,a) \<notin> r'" using 3 by (auto simp add: Field_def)
- ultimately have "(a1,a) \<notin> r Osum r'"
- using 3 unfolding Osum_def by auto
+ hence "(a1,a) \<notin> r" using B_def ** 2 by auto
+ moreover
+ have "(a1,a) \<notin> r'" using 3 by (auto simp add: Field_def)
+ ultimately have "(a1,a) \<notin> r Osum r'"
+ using 3 unfolding Osum_def by auto
}
moreover
{assume Case12: "a1 \<notin> Field r"
- hence "(a1,a) \<notin> r" unfolding Field_def by auto
- moreover
- have "(a1,a) \<notin> r'" using 3 unfolding Field_def by auto
- ultimately have "(a1,a) \<notin> r Osum r'"
- using 3 unfolding Osum_def by auto
+ hence "(a1,a) \<notin> r" unfolding Field_def by auto
+ moreover
+ have "(a1,a) \<notin> r'" using 3 unfolding Field_def by auto
+ ultimately have "(a1,a) \<notin> r Osum r'"
+ using 3 unfolding Osum_def by auto
}
ultimately show "(a1,a) \<notin> r Osum r'" by blast
qed
@@ -59,9 +59,9 @@
assume Case2: "B = {}"
hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto
then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'"
- using WF' unfolding wf_eq_minimal2 by blast
+ using WF' unfolding wf_eq_minimal2 by blast
hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast
- (* *)
+ (* *)
have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'"
proof(unfold Osum_def, auto simp add: 3)
fix a1' assume "(a1', a') \<in> r"
@@ -75,296 +75,231 @@
qed
lemma Osum_Refl:
-assumes FLD: "Field r Int Field r' = {}" and
- REFL: "Refl r" and REFL': "Refl r'"
-shows "Refl (r Osum r')"
-using assms
-unfolding refl_on_def Field_Osum unfolding Osum_def by blast
+ assumes FLD: "Field r Int Field r' = {}" and
+ REFL: "Refl r" and REFL': "Refl r'"
+ shows "Refl (r Osum r')"
+ using assms
+ unfolding refl_on_def Field_Osum unfolding Osum_def by blast
lemma Osum_trans:
-assumes FLD: "Field r Int Field r' = {}" and
- TRANS: "trans r" and TRANS': "trans r'"
-shows "trans (r Osum r')"
-proof(unfold trans_def, auto)
- fix x y z assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, z) \<in> r \<union>o r'"
- show "(x, z) \<in> r \<union>o r'"
- proof-
- {assume Case1: "(x,y) \<in> r"
- hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto
- have ?thesis
- proof-
- {assume Case11: "(y,z) \<in> r"
- hence "(x,z) \<in> r" using Case1 TRANS trans_def[of r] by blast
- hence ?thesis unfolding Osum_def by auto
- }
- moreover
- {assume Case12: "(y,z) \<in> r'"
- hence "y \<in> Field r'" unfolding Field_def by auto
- hence False using FLD 1 by auto
- }
- moreover
- {assume Case13: "z \<in> Field r'"
- hence ?thesis using 1 unfolding Osum_def by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case2: "(x,y) \<in> r'"
- hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto
- have ?thesis
- proof-
- {assume Case21: "(y,z) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD 2 by auto
- }
- moreover
- {assume Case22: "(y,z) \<in> r'"
- hence "(x,z) \<in> r'" using Case2 TRANS' trans_def[of r'] by blast
- hence ?thesis unfolding Osum_def by auto
- }
- moreover
- {assume Case23: "y \<in> Field r"
- hence False using FLD 2 by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case3: "x \<in> Field r \<and> y \<in> Field r'"
- have ?thesis
- proof-
- {assume Case31: "(y,z) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD Case3 by auto
- }
- moreover
- {assume Case32: "(y,z) \<in> r'"
- hence "z \<in> Field r'" unfolding Field_def by blast
- hence ?thesis unfolding Osum_def using Case3 by auto
- }
- moreover
- {assume Case33: "y \<in> Field r"
- hence False using FLD Case3 by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- ultimately show ?thesis using * unfolding Osum_def by blast
- qed
-qed
+ assumes FLD: "Field r Int Field r' = {}" and
+ TRANS: "trans r" and TRANS': "trans r'"
+ shows "trans (r Osum r')"
+ using assms
+ apply (clarsimp simp: trans_def disjoint_iff)
+ by (smt (verit) Domain.DomainI Field_def Osum_def Pair_inject Range.intros Un_iff case_prodE case_prodI mem_Collect_eq)
lemma Osum_Preorder:
-"\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')"
-unfolding preorder_on_def using Osum_Refl Osum_trans by blast
+ "\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')"
+ unfolding preorder_on_def using Osum_Refl Osum_trans by blast
lemma Osum_antisym:
-assumes FLD: "Field r Int Field r' = {}" and
- AN: "antisym r" and AN': "antisym r'"
-shows "antisym (r Osum r')"
+ assumes FLD: "Field r Int Field r' = {}" and
+ AN: "antisym r" and AN': "antisym r'"
+ shows "antisym (r Osum r')"
proof(unfold antisym_def, auto)
fix x y assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, x) \<in> r \<union>o r'"
show "x = y"
proof-
{assume Case1: "(x,y) \<in> r"
- hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto
- have ?thesis
- proof-
- have "(y,x) \<in> r \<Longrightarrow> ?thesis"
- using Case1 AN antisym_def[of r] by blast
- moreover
- {assume "(y,x) \<in> r'"
- hence "y \<in> Field r'" unfolding Field_def by auto
- hence False using FLD 1 by auto
- }
- moreover
- have "x \<in> Field r' \<Longrightarrow> False" using FLD 1 by auto
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
+ hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto
+ have ?thesis
+ proof-
+ have "(y,x) \<in> r \<Longrightarrow> ?thesis"
+ using Case1 AN antisym_def[of r] by blast
+ moreover
+ {assume "(y,x) \<in> r'"
+ hence "y \<in> Field r'" unfolding Field_def by auto
+ hence False using FLD 1 by auto
+ }
+ moreover
+ have "x \<in> Field r' \<Longrightarrow> False" using FLD 1 by auto
+ ultimately show ?thesis using ** unfolding Osum_def by blast
+ qed
}
moreover
{assume Case2: "(x,y) \<in> r'"
- hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto
- have ?thesis
- proof-
- {assume "(y,x) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD 2 by auto
- }
- moreover
- have "(y,x) \<in> r' \<Longrightarrow> ?thesis"
- using Case2 AN' antisym_def[of r'] by blast
- moreover
- {assume "y \<in> Field r"
- hence False using FLD 2 by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
+ hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto
+ have ?thesis
+ proof-
+ {assume "(y,x) \<in> r"
+ hence "y \<in> Field r" unfolding Field_def by auto
+ hence False using FLD 2 by auto
+ }
+ moreover
+ have "(y,x) \<in> r' \<Longrightarrow> ?thesis"
+ using Case2 AN' antisym_def[of r'] by blast
+ moreover
+ {assume "y \<in> Field r"
+ hence False using FLD 2 by auto
+ }
+ ultimately show ?thesis using ** unfolding Osum_def by blast
+ qed
}
moreover
{assume Case3: "x \<in> Field r \<and> y \<in> Field r'"
- have ?thesis
- proof-
- {assume "(y,x) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD Case3 by auto
- }
- moreover
- {assume Case32: "(y,x) \<in> r'"
- hence "x \<in> Field r'" unfolding Field_def by blast
- hence False using FLD Case3 by auto
- }
- moreover
- have "\<not> y \<in> Field r" using FLD Case3 by auto
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
+ have ?thesis
+ proof-
+ {assume "(y,x) \<in> r"
+ hence "y \<in> Field r" unfolding Field_def by auto
+ hence False using FLD Case3 by auto
+ }
+ moreover
+ {assume Case32: "(y,x) \<in> r'"
+ hence "x \<in> Field r'" unfolding Field_def by blast
+ hence False using FLD Case3 by auto
+ }
+ moreover
+ have "\<not> y \<in> Field r" using FLD Case3 by auto
+ ultimately show ?thesis using ** unfolding Osum_def by blast
+ qed
}
ultimately show ?thesis using * unfolding Osum_def by blast
qed
qed
lemma Osum_Partial_order:
-"\<lbrakk>Field r Int Field r' = {}; Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow>
+ "\<lbrakk>Field r Int Field r' = {}; Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow>
Partial_order (r Osum r')"
-unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast
+ unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast
lemma Osum_Total:
-assumes FLD: "Field r Int Field r' = {}" and
- TOT: "Total r" and TOT': "Total r'"
-shows "Total (r Osum r')"
-using assms
-unfolding total_on_def Field_Osum unfolding Osum_def by blast
+ assumes FLD: "Field r Int Field r' = {}" and
+ TOT: "Total r" and TOT': "Total r'"
+ shows "Total (r Osum r')"
+ using assms
+ unfolding total_on_def Field_Osum unfolding Osum_def by blast
lemma Osum_Linear_order:
-"\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow>
+ "\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow>
Linear_order (r Osum r')"
-unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast
+ unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast
lemma Osum_minus_Id1:
-assumes "r \<le> Id"
-shows "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
+ assumes "r \<le> Id"
+ shows "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
proof-
let ?Left = "(r Osum r') - Id"
let ?Right = "(r' - Id) \<union> (Field r \<times> Field r')"
{fix a::'a and b assume *: "(a,b) \<notin> Id"
- {assume "(a,b) \<in> r"
- with * have False using assms by auto
- }
- moreover
- {assume "(a,b) \<in> r'"
- with * have "(a,b) \<in> r' - Id" by auto
- }
- ultimately
- have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
- unfolding Osum_def by auto
+ {assume "(a,b) \<in> r"
+ with * have False using assms by auto
+ }
+ moreover
+ {assume "(a,b) \<in> r'"
+ with * have "(a,b) \<in> r' - Id" by auto
+ }
+ ultimately
+ have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
+ unfolding Osum_def by auto
}
thus ?thesis by auto
qed
lemma Osum_minus_Id2:
-assumes "r' \<le> Id"
-shows "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
+ assumes "r' \<le> Id"
+ shows "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
proof-
let ?Left = "(r Osum r') - Id"
let ?Right = "(r - Id) \<union> (Field r \<times> Field r')"
{fix a::'a and b assume *: "(a,b) \<notin> Id"
- {assume "(a,b) \<in> r'"
- with * have False using assms by auto
- }
- moreover
- {assume "(a,b) \<in> r"
- with * have "(a,b) \<in> r - Id" by auto
- }
- ultimately
- have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
- unfolding Osum_def by auto
+ {assume "(a,b) \<in> r'"
+ with * have False using assms by auto
+ }
+ moreover
+ {assume "(a,b) \<in> r"
+ with * have "(a,b) \<in> r - Id" by auto
+ }
+ ultimately
+ have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
+ unfolding Osum_def by auto
}
thus ?thesis by auto
qed
lemma Osum_minus_Id:
-assumes TOT: "Total r" and TOT': "Total r'" and
- NID: "\<not> (r \<le> Id)" and NID': "\<not> (r' \<le> Id)"
-shows "(r Osum r') - Id \<le> (r - Id) Osum (r' - Id)"
+ assumes TOT: "Total r" and TOT': "Total r'" and
+ NID: "\<not> (r \<le> Id)" and NID': "\<not> (r' \<le> Id)"
+ shows "(r Osum r') - Id \<le> (r - Id) Osum (r' - Id)"
proof-
{fix a a' assume *: "(a,a') \<in> (r Osum r')" and **: "a \<noteq> a'"
- have "(a,a') \<in> (r - Id) Osum (r' - Id)"
- proof-
- {assume "(a,a') \<in> r \<or> (a,a') \<in> r'"
- with ** have ?thesis unfolding Osum_def by auto
- }
- moreover
- {assume "a \<in> Field r \<and> a' \<in> Field r'"
- hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)"
- using assms Total_Id_Field by blast
- hence ?thesis unfolding Osum_def by auto
- }
- ultimately show ?thesis using * unfolding Osum_def by fast
- qed
+ have "(a,a') \<in> (r - Id) Osum (r' - Id)"
+ proof-
+ {assume "(a,a') \<in> r \<or> (a,a') \<in> r'"
+ with ** have ?thesis unfolding Osum_def by auto
+ }
+ moreover
+ {assume "a \<in> Field r \<and> a' \<in> Field r'"
+ hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)"
+ using assms Total_Id_Field by blast
+ hence ?thesis unfolding Osum_def by auto
+ }
+ ultimately show ?thesis using * unfolding Osum_def by fast
+ qed
}
thus ?thesis by(auto simp add: Osum_def)
qed
lemma wf_Int_Times:
-assumes "A Int B = {}"
-shows "wf(A \<times> B)"
-unfolding wf_def using assms by blast
+ assumes "A Int B = {}"
+ shows "wf(A \<times> B)"
+ unfolding wf_def using assms by blast
lemma Osum_wf_Id:
-assumes TOT: "Total r" and TOT': "Total r'" and
- FLD: "Field r Int Field r' = {}" and
- WF: "wf(r - Id)" and WF': "wf(r' - Id)"
-shows "wf ((r Osum r') - Id)"
+ assumes TOT: "Total r" and TOT': "Total r'" and
+ FLD: "Field r Int Field r' = {}" and
+ WF: "wf(r - Id)" and WF': "wf(r' - Id)"
+ shows "wf ((r Osum r') - Id)"
proof(cases "r \<le> Id \<or> r' \<le> Id")
assume Case1: "\<not>(r \<le> Id \<or> r' \<le> Id)"
have "Field(r - Id) Int Field(r' - Id) = {}"
- using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r']
- Diff_subset[of r Id] Diff_subset[of r' Id] by blast
+ using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r']
+ Diff_subset[of r Id] Diff_subset[of r' Id] by blast
thus ?thesis
- using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"]
- wf_subset[of "(r - Id) \<union>o (r' - Id)" "(r Osum r') - Id"] by auto
+ using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"]
+ wf_subset[of "(r - Id) \<union>o (r' - Id)" "(r Osum r') - Id"] by auto
next
have 1: "wf(Field r \<times> Field r')"
- using FLD by (auto simp add: wf_Int_Times)
+ using FLD by (auto simp add: wf_Int_Times)
assume Case2: "r \<le> Id \<or> r' \<le> Id"
moreover
{assume Case21: "r \<le> Id"
- hence "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
- using Osum_minus_Id1[of r r'] by simp
- moreover
- {have "Domain(Field r \<times> Field r') Int Range(r' - Id) = {}"
- using FLD unfolding Field_def by blast
- hence "wf((r' - Id) \<union> (Field r \<times> Field r'))"
- using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"]
- by (auto simp add: Un_commute)
- }
- ultimately have ?thesis using wf_subset by blast
+ hence "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
+ using Osum_minus_Id1[of r r'] by simp
+ moreover
+ {have "Domain(Field r \<times> Field r') Int Range(r' - Id) = {}"
+ using FLD unfolding Field_def by blast
+ hence "wf((r' - Id) \<union> (Field r \<times> Field r'))"
+ using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"]
+ by (auto simp add: Un_commute)
+ }
+ ultimately have ?thesis using wf_subset by blast
}
moreover
{assume Case22: "r' \<le> Id"
- hence "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
- using Osum_minus_Id2[of r' r] by simp
- moreover
- {have "Range(Field r \<times> Field r') Int Domain(r - Id) = {}"
- using FLD unfolding Field_def by blast
- hence "wf((r - Id) \<union> (Field r \<times> Field r'))"
- using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"]
- by (auto simp add: Un_commute)
- }
- ultimately have ?thesis using wf_subset by blast
+ hence "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
+ using Osum_minus_Id2[of r' r] by simp
+ moreover
+ {have "Range(Field r \<times> Field r') Int Domain(r - Id) = {}"
+ using FLD unfolding Field_def by blast
+ hence "wf((r - Id) \<union> (Field r \<times> Field r'))"
+ using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"]
+ by (auto simp add: Un_commute)
+ }
+ ultimately have ?thesis using wf_subset by blast
}
ultimately show ?thesis by blast
qed
lemma Osum_Well_order:
-assumes FLD: "Field r Int Field r' = {}" and
- WELL: "Well_order r" and WELL': "Well_order r'"
-shows "Well_order (r Osum r')"
+ assumes FLD: "Field r Int Field r' = {}" and
+ WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "Well_order (r Osum r')"
proof-
have "Total r \<and> Total r'" using WELL WELL'
- by (auto simp add: order_on_defs)
+ by (auto simp add: order_on_defs)
thus ?thesis using assms unfolding well_order_on_def
- using Osum_Linear_order Osum_wf_Id by blast
+ using Osum_Linear_order Osum_wf_Id by blast
qed
end
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Thu Jan 12 17:12:36 2023 +0000
@@ -8,8 +8,8 @@
section \<open>Constructions on Wellorders\<close>
theory Wellorder_Constructions
-imports
- Wellorder_Embedding Order_Union
+ imports
+ Wellorder_Embedding Order_Union
begin
unbundle cardinal_syntax
@@ -21,254 +21,189 @@
Func_empty[simp]
Func_is_emp[simp]
-lemma Func_emp2[simp]: "A \<noteq> {} \<Longrightarrow> Func A {} = {}" by auto
-
-
-subsection \<open>Restriction to a set\<close>
-
-lemma Restr_incr2:
-"r <= r' \<Longrightarrow> Restr r A <= Restr r' A"
-by blast
-
-lemma Restr_incr:
-"\<lbrakk>r \<le> r'; A \<le> A'\<rbrakk> \<Longrightarrow> Restr r A \<le> Restr r' A'"
-by blast
-
-lemma Restr_Int:
-"Restr (Restr r A) B = Restr r (A Int B)"
-by blast
-
-lemma Restr_iff: "(a,b) \<in> Restr r A = (a \<in> A \<and> b \<in> A \<and> (a,b) \<in> r)"
-by (auto simp add: Field_def)
-
-lemma Restr_subset1: "Restr r A \<le> r"
-by auto
-
-lemma Restr_subset2: "Restr r A \<le> A \<times> A"
-by auto
-
-lemma wf_Restr:
-"wf r \<Longrightarrow> wf(Restr r A)"
-using Restr_subset by (elim wf_subset) simp
-
-lemma Restr_incr1:
-"A \<le> B \<Longrightarrow> Restr r A \<le> Restr r B"
-by blast
subsection \<open>Order filters versus restrictions and embeddings\<close>
-lemma ofilter_Restr:
-assumes WELL: "Well_order r" and
- OFA: "ofilter r A" and OFB: "ofilter r B" and SUB: "A \<le> B"
-shows "ofilter (Restr r B) A"
-proof-
- let ?rB = "Restr r B"
- have Well: "wo_rel r" unfolding wo_rel_def using WELL .
- hence Refl: "Refl r" by (auto simp add: wo_rel.REFL)
- hence Field: "Field ?rB = Field r Int B"
- using Refl_Field_Restr by blast
- have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
- by (auto simp add: Well_order_Restr wo_rel_def)
- (* Main proof *)
- show ?thesis
- proof(auto simp add: WellB wo_rel.ofilter_def)
- fix a assume "a \<in> A"
- hence "a \<in> Field r \<and> a \<in> B" using assms Well
- by (auto simp add: wo_rel.ofilter_def)
- with Field show "a \<in> Field(Restr r B)" by auto
- next
- fix a b assume *: "a \<in> A" and "b \<in> under (Restr r B) a"
- hence "b \<in> under r a"
- using WELL OFB SUB ofilter_Restr_under[of r B a] by auto
- thus "b \<in> A" using * Well OFA by(auto simp add: wo_rel.ofilter_def)
- qed
-qed
-
lemma ofilter_subset_iso:
-assumes WELL: "Well_order r" and
- OFA: "ofilter r A" and OFB: "ofilter r B"
-shows "(A = B) = iso (Restr r A) (Restr r B) id"
-using assms
-by (auto simp add: ofilter_subset_embedS_iso)
+ assumes WELL: "Well_order r" and
+ OFA: "ofilter r A" and OFB: "ofilter r B"
+ shows "(A = B) = iso (Restr r A) (Restr r B) id"
+ using assms by (auto simp add: ofilter_subset_embedS_iso)
subsection \<open>Ordering the well-orders by existence of embeddings\<close>
corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq"
-using ordLeq_reflexive unfolding ordLeq_def refl_on_def
-by blast
+ using ordLeq_reflexive unfolding ordLeq_def refl_on_def
+ by blast
corollary ordLeq_trans: "trans ordLeq"
-using trans_def[of ordLeq] ordLeq_transitive by blast
+ using trans_def[of ordLeq] ordLeq_transitive by blast
corollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq"
-by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans)
+ by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans)
corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso"
-using ordIso_reflexive unfolding refl_on_def ordIso_def
-by blast
+ using ordIso_reflexive unfolding refl_on_def ordIso_def
+ by blast
corollary ordIso_trans: "trans ordIso"
-using trans_def[of ordIso] ordIso_transitive by blast
+ using trans_def[of ordIso] ordIso_transitive by blast
corollary ordIso_sym: "sym ordIso"
-by (auto simp add: sym_def ordIso_symmetric)
+ by (auto simp add: sym_def ordIso_symmetric)
corollary ordIso_equiv: "equiv {r. Well_order r} ordIso"
-by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans)
+ by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans)
lemma ordLess_Well_order_simp[simp]:
-assumes "r <o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordLess_def by simp
+ assumes "r <o r'"
+ shows "Well_order r \<and> Well_order r'"
+ using assms unfolding ordLess_def by simp
lemma ordIso_Well_order_simp[simp]:
-assumes "r =o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordIso_def by simp
+ assumes "r =o r'"
+ shows "Well_order r \<and> Well_order r'"
+ using assms unfolding ordIso_def by simp
lemma ordLess_irrefl: "irrefl ordLess"
-by(unfold irrefl_def, auto simp add: ordLess_irreflexive)
+ by(unfold irrefl_def, auto simp add: ordLess_irreflexive)
lemma ordLess_or_ordIso:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "r <o r' \<or> r' <o r \<or> r =o r'"
-unfolding ordLess_def ordIso_def
-using assms embedS_or_iso[of r r'] by auto
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "r <o r' \<or> r' <o r \<or> r =o r'"
+ unfolding ordLess_def ordIso_def
+ using assms embedS_or_iso[of r r'] by auto
corollary ordLeq_ordLess_Un_ordIso:
-"ordLeq = ordLess \<union> ordIso"
-by (auto simp add: ordLeq_iff_ordLess_or_ordIso)
-
-lemma not_ordLeq_ordLess:
-"r \<le>o r' \<Longrightarrow> \<not> r' <o r"
-using not_ordLess_ordLeq by blast
+ "ordLeq = ordLess \<union> ordIso"
+ by (auto simp add: ordLeq_iff_ordLess_or_ordIso)
lemma ordIso_or_ordLess:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "r =o r' \<or> r <o r' \<or> r' <o r"
-using assms ordLess_or_ordLeq ordLeq_iff_ordLess_or_ordIso by blast
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "r =o r' \<or> r <o r' \<or> r' <o r"
+ using assms ordLess_or_ordLeq ordLeq_iff_ordLess_or_ordIso by blast
lemmas ord_trans = ordIso_transitive ordLeq_transitive ordLess_transitive
- ordIso_ordLeq_trans ordLeq_ordIso_trans
- ordIso_ordLess_trans ordLess_ordIso_trans
- ordLess_ordLeq_trans ordLeq_ordLess_trans
+ ordIso_ordLeq_trans ordLeq_ordIso_trans
+ ordIso_ordLess_trans ordLess_ordIso_trans
+ ordLess_ordLeq_trans ordLeq_ordLess_trans
lemma ofilter_ordLeq:
-assumes "Well_order r" and "ofilter r A"
-shows "Restr r A \<le>o r"
+ assumes "Well_order r" and "ofilter r A"
+ shows "Restr r A \<le>o r"
proof-
have "A \<le> Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
thus ?thesis using assms
- by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter
- wo_rel_def Restr_Field)
+ by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter
+ wo_rel_def Restr_Field)
qed
corollary under_Restr_ordLeq:
-"Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r"
-by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def)
+ "Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r"
+ by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def)
subsection \<open>Copy via direct images\<close>
lemma Id_dir_image: "dir_image Id f \<le> Id"
-unfolding dir_image_def by auto
+ unfolding dir_image_def by auto
lemma Un_dir_image:
-"dir_image (r1 \<union> r2) f = (dir_image r1 f) \<union> (dir_image r2 f)"
-unfolding dir_image_def by auto
+ "dir_image (r1 \<union> r2) f = (dir_image r1 f) \<union> (dir_image r2 f)"
+ unfolding dir_image_def by auto
lemma Int_dir_image:
-assumes "inj_on f (Field r1 \<union> Field r2)"
-shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)"
+ assumes "inj_on f (Field r1 \<union> Field r2)"
+ shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)"
proof
show "dir_image (r1 Int r2) f \<le> (dir_image r1 f) Int (dir_image r2 f)"
- using assms unfolding dir_image_def inj_on_def by auto
+ using assms unfolding dir_image_def inj_on_def by auto
next
show "(dir_image r1 f) Int (dir_image r2 f) \<le> dir_image (r1 Int r2) f"
proof(clarify)
fix a' b'
assume "(a',b') \<in> dir_image r1 f" "(a',b') \<in> dir_image r2 f"
then obtain a1 b1 a2 b2
- where 1: "a' = f a1 \<and> b' = f b1 \<and> a' = f a2 \<and> b' = f b2" and
- 2: "(a1,b1) \<in> r1 \<and> (a2,b2) \<in> r2" and
- 3: "{a1,b1} \<le> Field r1 \<and> {a2,b2} \<le> Field r2"
- unfolding dir_image_def Field_def by blast
+ where 1: "a' = f a1 \<and> b' = f b1 \<and> a' = f a2 \<and> b' = f b2" and
+ 2: "(a1,b1) \<in> r1 \<and> (a2,b2) \<in> r2" and
+ 3: "{a1,b1} \<le> Field r1 \<and> {a2,b2} \<le> Field r2"
+ unfolding dir_image_def Field_def by blast
hence "a1 = a2 \<and> b1 = b2" using assms unfolding inj_on_def by auto
hence "a' = f a1 \<and> b' = f b1 \<and> (a1,b1) \<in> r1 Int r2 \<and> (a2,b2) \<in> r1 Int r2"
- using 1 2 by auto
+ using 1 2 by auto
thus "(a',b') \<in> dir_image (r1 \<inter> r2) f"
- unfolding dir_image_def by blast
+ unfolding dir_image_def by blast
qed
qed
(* More facts on ordinal sum: *)
lemma Osum_embed:
-assumes FLD: "Field r Int Field r' = {}" and
- WELL: "Well_order r" and WELL': "Well_order r'"
-shows "embed r (r Osum r') id"
+ assumes FLD: "Field r Int Field r' = {}" and
+ WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "embed r (r Osum r') id"
proof-
have 1: "Well_order (r Osum r')"
- using assms by (auto simp add: Osum_Well_order)
+ using assms by (auto simp add: Osum_Well_order)
moreover
have "compat r (r Osum r') id"
- unfolding compat_def Osum_def by auto
+ unfolding compat_def Osum_def by auto
moreover
have "inj_on id (Field r)" by simp
moreover
have "ofilter (r Osum r') (Field r)"
- using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
- Field_Osum under_def)
+ using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
+ Field_Osum under_def)
fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'"
moreover
{assume "(b,a) \<in> r'"
- hence "a \<in> Field r'" using Field_def[of r'] by blast
- hence False using 2 FLD by blast
+ hence "a \<in> Field r'" using Field_def[of r'] by blast
+ hence False using 2 FLD by blast
}
moreover
{assume "a \<in> Field r'"
- hence False using 2 FLD by blast
+ hence False using 2 FLD by blast
}
ultimately
show "b \<in> Field r" by (auto simp add: Osum_def Field_def)
qed
ultimately show ?thesis
- using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
+ using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed
corollary Osum_ordLeq:
-assumes FLD: "Field r Int Field r' = {}" and
- WELL: "Well_order r" and WELL': "Well_order r'"
-shows "r \<le>o r Osum r'"
-using assms Osum_embed Osum_Well_order
-unfolding ordLeq_def by blast
+ assumes FLD: "Field r Int Field r' = {}" and
+ WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "r \<le>o r Osum r'"
+ using assms Osum_embed Osum_Well_order
+ unfolding ordLeq_def by blast
lemma Well_order_embed_copy:
-assumes WELL: "well_order_on A r" and
- INJ: "inj_on f A" and SUB: "f ` A \<le> B"
-shows "\<exists>r'. well_order_on B r' \<and> r \<le>o r'"
+ assumes WELL: "well_order_on A r" and
+ INJ: "inj_on f A" and SUB: "f ` A \<le> B"
+ shows "\<exists>r'. well_order_on B r' \<and> r \<le>o r'"
proof-
have "bij_betw f A (f ` A)"
- using INJ inj_on_imp_bij_betw by blast
+ using INJ inj_on_imp_bij_betw by blast
then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''"
- using WELL Well_order_iso_copy by blast
+ using WELL Well_order_iso_copy by blast
hence 2: "Well_order r'' \<and> Field r'' = (f ` A)"
- using well_order_on_Well_order by blast
- (* *)
+ using well_order_on_Well_order by blast
+ (* *)
let ?C = "B - (f ` A)"
obtain r''' where "well_order_on ?C r'''"
- using well_order_on by blast
+ using well_order_on by blast
hence 3: "Well_order r''' \<and> Field r''' = ?C"
- using well_order_on_Well_order by blast
- (* *)
+ using well_order_on_Well_order by blast
+ (* *)
let ?r' = "r'' Osum r'''"
have "Field r'' Int Field r''' = {}"
- using 2 3 by auto
+ using 2 3 by auto
hence "r'' \<le>o ?r'" using Osum_ordLeq[of r'' r'''] 2 3 by blast
hence 4: "r \<le>o ?r'" using 1 ordIso_ordLeq_trans by blast
- (* *)
+ (* *)
hence "Well_order ?r'" unfolding ordLeq_def by auto
moreover
have "Field ?r' = B" using 2 3 SUB by (auto simp add: Field_Osum)
@@ -278,56 +213,56 @@
subsection \<open>The maxim among a finite set of ordinals\<close>
-text \<open>The correct phrasing would be ``a maxim of ...", as \<open>\<le>o\<close> is only a preorder.\<close>
+text \<open>The correct phrasing would be ``a maxim of \<dots>", as \<open>\<le>o\<close> is only a preorder.\<close>
definition isOmax :: "'a rel set \<Rightarrow> 'a rel \<Rightarrow> bool"
-where
-"isOmax R r \<equiv> r \<in> R \<and> (\<forall>r' \<in> R. r' \<le>o r)"
+ where
+ "isOmax R r \<equiv> r \<in> R \<and> (\<forall>r' \<in> R. r' \<le>o r)"
definition omax :: "'a rel set \<Rightarrow> 'a rel"
-where
-"omax R == SOME r. isOmax R r"
+ where
+ "omax R == SOME r. isOmax R r"
lemma exists_isOmax:
-assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
-shows "\<exists> r. isOmax R r"
+ assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
+ shows "\<exists> r. isOmax R r"
proof-
have "finite R \<Longrightarrow> R \<noteq> {} \<longrightarrow> (\<forall> r \<in> R. Well_order r) \<longrightarrow> (\<exists> r. isOmax R r)"
- apply(erule finite_induct) apply(simp add: isOmax_def)
+ apply(erule finite_induct) apply(simp add: isOmax_def)
proof(clarsimp)
fix r :: "('a \<times> 'a) set" and R assume *: "finite R" and **: "r \<notin> R"
- and ***: "Well_order r" and ****: "\<forall>r\<in>R. Well_order r"
- and IH: "R \<noteq> {} \<longrightarrow> (\<exists>p. isOmax R p)"
+ and ***: "Well_order r" and ****: "\<forall>r\<in>R. Well_order r"
+ and IH: "R \<noteq> {} \<longrightarrow> (\<exists>p. isOmax R p)"
let ?R' = "insert r R"
show "\<exists>p'. (isOmax ?R' p')"
proof(cases "R = {}")
- assume Case1: "R = {}"
+ case True
thus ?thesis unfolding isOmax_def using ***
- by (simp add: ordLeq_reflexive)
+ by (simp add: ordLeq_reflexive)
next
- assume Case2: "R \<noteq> {}"
+ case False
then obtain p where p: "isOmax R p" using IH by auto
hence 1: "Well_order p" using **** unfolding isOmax_def by simp
{assume Case21: "r \<le>o p"
- hence "isOmax ?R' p" using p unfolding isOmax_def by simp
- hence ?thesis by auto
+ hence "isOmax ?R' p" using p unfolding isOmax_def by simp
+ hence ?thesis by auto
}
moreover
{assume Case22: "p \<le>o r"
- {fix r' assume "r' \<in> ?R'"
- moreover
- {assume "r' \<in> R"
- hence "r' \<le>o p" using p unfolding isOmax_def by simp
- hence "r' \<le>o r" using Case22 by(rule ordLeq_transitive)
+ {fix r' assume "r' \<in> ?R'"
+ moreover
+ {assume "r' \<in> R"
+ hence "r' \<le>o p" using p unfolding isOmax_def by simp
+ hence "r' \<le>o r" using Case22 by(rule ordLeq_transitive)
+ }
+ moreover have "r \<le>o r" using *** by(rule ordLeq_reflexive)
+ ultimately have "r' \<le>o r" by auto
}
- moreover have "r \<le>o r" using *** by(rule ordLeq_reflexive)
- ultimately have "r' \<le>o r" by auto
- }
- hence "isOmax ?R' r" unfolding isOmax_def by simp
- hence ?thesis by auto
+ hence "isOmax ?R' r" unfolding isOmax_def by simp
+ hence ?thesis by auto
}
moreover have "r \<le>o p \<or> p \<le>o r"
- using 1 *** ordLeq_total by auto
+ using 1 *** ordLeq_total by auto
ultimately show ?thesis by blast
qed
qed
@@ -335,120 +270,86 @@
qed
lemma omax_isOmax:
-assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
-shows "isOmax R (omax R)"
-unfolding omax_def using assms
-by(simp add: exists_isOmax someI_ex)
+ assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
+ shows "isOmax R (omax R)"
+ unfolding omax_def using assms
+ by(simp add: exists_isOmax someI_ex)
lemma omax_in:
-assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
-shows "omax R \<in> R"
-using assms omax_isOmax unfolding isOmax_def by blast
+ assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
+ shows "omax R \<in> R"
+ using assms omax_isOmax unfolding isOmax_def by blast
lemma Well_order_omax:
-assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Well_order r"
-shows "Well_order (omax R)"
-using assms apply - apply(drule omax_in) by auto
+ assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Well_order r"
+ shows "Well_order (omax R)"
+ using assms omax_in by blast
lemma omax_maxim:
-assumes "finite R" and "\<forall> r \<in> R. Well_order r" and "r \<in> R"
-shows "r \<le>o omax R"
-using assms omax_isOmax unfolding isOmax_def by blast
+ assumes "finite R" and "\<forall> r \<in> R. Well_order r" and "r \<in> R"
+ shows "r \<le>o omax R"
+ using assms omax_isOmax unfolding isOmax_def by blast
lemma omax_ordLeq:
-assumes "finite R" and "R \<noteq> {}" and *: "\<forall> r \<in> R. r \<le>o p"
-shows "omax R \<le>o p"
-proof-
- have "\<forall> r \<in> R. Well_order r" using * unfolding ordLeq_def by simp
- thus ?thesis using assms omax_in by auto
-qed
+ assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. r \<le>o p"
+ shows "omax R \<le>o p"
+ by (meson assms omax_in ordLeq_Well_order_simp)
lemma omax_ordLess:
-assumes "finite R" and "R \<noteq> {}" and *: "\<forall> r \<in> R. r <o p"
-shows "omax R <o p"
-proof-
- have "\<forall> r \<in> R. Well_order r" using * unfolding ordLess_def by simp
- thus ?thesis using assms omax_in by auto
-qed
+ assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. r <o p"
+ shows "omax R <o p"
+ by (meson assms omax_in ordLess_Well_order_simp)
lemma omax_ordLeq_elim:
-assumes "finite R" and "\<forall> r \<in> R. Well_order r"
-and "omax R \<le>o p" and "r \<in> R"
-shows "r \<le>o p"
-using assms omax_maxim[of R r] apply simp
-using ordLeq_transitive by blast
+ assumes "finite R" and "\<forall> r \<in> R. Well_order r"
+ and "omax R \<le>o p" and "r \<in> R"
+ shows "r \<le>o p"
+ by (meson assms omax_maxim ordLeq_transitive)
lemma omax_ordLess_elim:
-assumes "finite R" and "\<forall> r \<in> R. Well_order r"
-and "omax R <o p" and "r \<in> R"
-shows "r <o p"
-using assms omax_maxim[of R r] apply simp
-using ordLeq_ordLess_trans by blast
+ assumes "finite R" and "\<forall> r \<in> R. Well_order r"
+ and "omax R <o p" and "r \<in> R"
+ shows "r <o p"
+ by (meson assms omax_maxim ordLeq_ordLess_trans)
lemma ordLeq_omax:
-assumes "finite R" and "\<forall> r \<in> R. Well_order r"
-and "r \<in> R" and "p \<le>o r"
-shows "p \<le>o omax R"
-using assms omax_maxim[of R r] apply simp
-using ordLeq_transitive by blast
+ assumes "finite R" and "\<forall> r \<in> R. Well_order r"
+ and "r \<in> R" and "p \<le>o r"
+ shows "p \<le>o omax R"
+ by (meson assms omax_maxim ordLeq_transitive)
lemma ordLess_omax:
-assumes "finite R" and "\<forall> r \<in> R. Well_order r"
-and "r \<in> R" and "p <o r"
-shows "p <o omax R"
-using assms omax_maxim[of R r] apply simp
-using ordLess_ordLeq_trans by blast
+ assumes "finite R" and "\<forall> r \<in> R. Well_order r"
+ and "r \<in> R" and "p <o r"
+ shows "p <o omax R"
+ by (meson assms omax_maxim ordLess_ordLeq_trans)
lemma omax_ordLeq_mono:
-assumes P: "finite P" and R: "finite R"
-and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r"
-and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p \<le>o r"
-shows "omax P \<le>o omax R"
-proof-
- let ?mp = "omax P" let ?mr = "omax R"
- {fix p assume "p \<in> P"
- then obtain r where r: "r \<in> R" and "p \<le>o r"
- using LEQ by blast
- moreover have "r <=o ?mr"
- using r R Well_R omax_maxim by blast
- ultimately have "p <=o ?mr"
- using ordLeq_transitive by blast
- }
- thus "?mp <=o ?mr"
- using NE_P P using omax_ordLeq by blast
-qed
+ assumes P: "finite P" and R: "finite R"
+ and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r"
+ and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p \<le>o r"
+ shows "omax P \<le>o omax R"
+ by (meson LEQ NE_P P R Well_R omax_ordLeq ordLeq_omax)
lemma omax_ordLess_mono:
-assumes P: "finite P" and R: "finite R"
-and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r"
-and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p <o r"
-shows "omax P <o omax R"
-proof-
- let ?mp = "omax P" let ?mr = "omax R"
- {fix p assume "p \<in> P"
- then obtain r where r: "r \<in> R" and "p <o r"
- using LEQ by blast
- moreover have "r <=o ?mr"
- using r R Well_R omax_maxim by blast
- ultimately have "p <o ?mr"
- using ordLess_ordLeq_trans by blast
- }
- thus "?mp <o ?mr"
- using NE_P P omax_ordLess by blast
-qed
+ assumes P: "finite P" and R: "finite R"
+ and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r"
+ and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p <o r"
+ shows "omax P <o omax R"
+ by (meson LEQ NE_P P R Well_R omax_ordLess ordLess_omax)
subsection \<open>Limit and succesor ordinals\<close>
lemma embed_underS2:
-assumes r: "Well_order r" and g: "embed r s g" and a: "a \<in> Field r"
-shows "g ` underS r a = underS s (g a)"
+ assumes r: "Well_order r" and g: "embed r s g" and a: "a \<in> Field r"
+ shows "g ` underS r a = underS s (g a)"
by (meson a bij_betw_def embed_underS g r)
lemma bij_betw_insert:
-assumes "b \<notin> A" and "f b \<notin> A'" and "bij_betw f A A'"
-shows "bij_betw f (insert b A) (insert (f b) A')"
-using notIn_Un_bij_betw[OF assms] by auto
+ assumes "b \<notin> A" and "f b \<notin> A'" and "bij_betw f A A'"
+ shows "bij_betw f (insert b A) (insert (f b) A')"
+ using notIn_Un_bij_betw[OF assms] by auto
context wo_rel
begin
@@ -459,90 +360,80 @@
by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
lemma suc_underS:
-assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
-shows "b \<in> underS (suc B)"
-using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto
+ assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
+ shows "b \<in> underS (suc B)"
+ using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto
lemma underS_supr:
-assumes bA: "b \<in> underS (supr A)" and A: "A \<subseteq> Field r"
-shows "\<exists> a \<in> A. b \<in> underS a"
-proof(rule ccontr, auto)
+ assumes bA: "b \<in> underS (supr A)" and A: "A \<subseteq> Field r"
+ shows "\<exists> a \<in> A. b \<in> underS a"
+proof(rule ccontr, simp)
have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
assume "\<forall>a\<in>A. b \<notin> underS a"
hence 0: "\<forall>a \<in> A. (a,b) \<in> r" using A bA unfolding underS_def
- by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
- have "(supr A, b) \<in> r" apply(rule supr_least[OF A bb]) using 0 by auto
+ by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
+ have "(supr A, b) \<in> r"
+ by (simp add: "0" A bb supr_least)
thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
qed
lemma underS_suc:
-assumes bA: "b \<in> underS (suc A)" and A: "A \<subseteq> Field r"
-shows "\<exists> a \<in> A. b \<in> under a"
-proof(rule ccontr, auto)
+ assumes bA: "b \<in> underS (suc A)" and A: "A \<subseteq> Field r"
+ shows "\<exists> a \<in> A. b \<in> under a"
+proof(rule ccontr, simp)
have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
assume "\<forall>a\<in>A. b \<notin> under a"
- hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
- by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def rev_subsetD)
- have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
+ hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA
+ by (metis bb in_mono max2_def max2_greater mem_Collect_eq underS_I under_def)
+ have "(suc A, b) \<in> r"
+ by (metis "0" A bb suc_least underS_E)
thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
qed
lemma (in wo_rel) in_underS_supr:
-assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
-shows "j \<in> underS (supr A)"
+ assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
+ shows "j \<in> underS (supr A)"
proof-
have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
thus ?thesis using j unfolding underS_def
- by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
+ by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
qed
lemma inj_on_Field:
-assumes A: "A \<subseteq> Field r" and f: "\<And> a b. \<lbrakk>a \<in> A; b \<in> A; a \<in> underS b\<rbrakk> \<Longrightarrow> f a \<noteq> f b"
-shows "inj_on f A"
-unfolding inj_on_def proof safe
- fix a b assume a: "a \<in> A" and b: "b \<in> A" and fab: "f a = f b"
- {assume "a \<in> underS b"
- hence False using f[OF a b] fab by auto
- }
- moreover
- {assume "b \<in> underS a"
- hence False using f[OF b a] fab by auto
- }
- ultimately show "a = b" using TOTALS A a b unfolding underS_def by auto
-qed
+ assumes A: "A \<subseteq> Field r" and f: "\<And> a b. \<lbrakk>a \<in> A; b \<in> A; a \<in> underS b\<rbrakk> \<Longrightarrow> f a \<noteq> f b"
+ shows "inj_on f A"
+ by (smt (verit) A f in_notinI inj_on_def subsetD underS_I)
lemma ofilter_init_seg_of:
-assumes "ofilter F"
-shows "Restr r F initial_segment_of r"
-using assms unfolding ofilter_def init_seg_of_def under_def by auto
+ assumes "ofilter F"
+ shows "Restr r F initial_segment_of r"
+ using assms unfolding ofilter_def init_seg_of_def under_def by auto
lemma underS_init_seg_of_Collect:
-assumes "\<And>j1 j2. \<lbrakk>j2 \<in> underS i; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
-shows "{R j |j. j \<in> underS i} \<in> Chains init_seg_of"
-unfolding Chains_def proof safe
+ assumes "\<And>j1 j2. \<lbrakk>j2 \<in> underS i; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
+ shows "{R j |j. j \<in> underS i} \<in> Chains init_seg_of"
+ unfolding Chains_def proof safe
fix j ja assume jS: "j \<in> underS i" and jaS: "ja \<in> underS i"
- and init: "(R ja, R j) \<notin> init_seg_of"
+ and init: "(R ja, R j) \<notin> init_seg_of"
hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
- and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
- and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
+ and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
+ and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
show "R j initial_segment_of R ja"
- using jja init jjai i
- by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: underS_def)
+ using jja init TOTALS assms jS jaS by auto
qed
lemma (in wo_rel) Field_init_seg_of_Collect:
-assumes "\<And>j1 j2. \<lbrakk>j2 \<in> Field r; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
-shows "{R j |j. j \<in> Field r} \<in> Chains init_seg_of"
-unfolding Chains_def proof safe
+ assumes "\<And>j1 j2. \<lbrakk>j2 \<in> Field r; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
+ shows "{R j |j. j \<in> Field r} \<in> Chains init_seg_of"
+ unfolding Chains_def proof safe
fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
- and init: "(R ja, R j) \<notin> init_seg_of"
+ and init: "(R ja, R j) \<notin> init_seg_of"
hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
- unfolding Field_def underS_def by auto
+ unfolding Field_def underS_def by auto
have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
show "R j initial_segment_of R ja"
- using jja init
- by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: Field_def)
+ using TOTALS assms init jS jaS by blast
qed
subsubsection \<open>Successor and limit elements of an ordinal\<close>
@@ -556,77 +447,65 @@
definition "isLim i \<equiv> \<not> isSucc i"
lemma zero_smallest[simp]:
-assumes "j \<in> Field r" shows "(zero, j) \<in> r"
-unfolding zero_def
-by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS)
+ assumes "j \<in> Field r" shows "(zero, j) \<in> r"
+ unfolding zero_def
+ by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS)
lemma zero_in_Field: assumes "Field r \<noteq> {}" shows "zero \<in> Field r"
-using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def)
+ using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def)
lemma leq_zero_imp[simp]:
-"(x, zero) \<in> r \<Longrightarrow> x = zero"
-by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest)
+ "(x, zero) \<in> r \<Longrightarrow> x = zero"
+ by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest)
lemma leq_zero[simp]:
-assumes "Field r \<noteq> {}" shows "(x, zero) \<in> r \<longleftrightarrow> x = zero"
-using zero_in_Field[OF assms] in_notinI[of x zero] by auto
+ assumes "Field r \<noteq> {}" shows "(x, zero) \<in> r \<longleftrightarrow> x = zero"
+ using zero_in_Field[OF assms] in_notinI[of x zero] by auto
lemma under_zero[simp]:
-assumes "Field r \<noteq> {}" shows "under zero = {zero}"
-using assms unfolding under_def by auto
+ assumes "Field r \<noteq> {}" shows "under zero = {zero}"
+ using assms unfolding under_def by auto
lemma underS_zero[simp,intro]: "underS zero = {}"
-unfolding underS_def by auto
+ unfolding underS_def by auto
lemma isSucc_succ: "aboveS i \<noteq> {} \<Longrightarrow> isSucc (succ i)"
-unfolding isSucc_def succ_def by auto
+ unfolding isSucc_def succ_def by auto
lemma succ_in_diff:
-assumes "aboveS i \<noteq> {}" shows "(i,succ i) \<in> r \<and> succ i \<noteq> i"
-using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto
+ assumes "aboveS i \<noteq> {}" shows "(i,succ i) \<in> r \<and> succ i \<noteq> i"
+ using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto
lemmas succ_in[simp] = succ_in_diff[THEN conjunct1]
lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2]
lemma succ_in_Field[simp]:
-assumes "aboveS i \<noteq> {}" shows "succ i \<in> Field r"
-using succ_in[OF assms] unfolding Field_def by auto
+ assumes "aboveS i \<noteq> {}" shows "succ i \<in> Field r"
+ using succ_in[OF assms] unfolding Field_def by auto
lemma succ_not_in:
-assumes "aboveS i \<noteq> {}" shows "(succ i, i) \<notin> r"
-proof
- assume 1: "(succ i, i) \<in> r"
- hence "succ i \<in> Field r \<and> i \<in> Field r" unfolding Field_def by auto
- hence "(i, succ i) \<in> r \<and> succ i \<noteq> i" using assms by auto
- thus False using 1 by (metis ANTISYM antisymD)
-qed
+ assumes "aboveS i \<noteq> {}" shows "(succ i, i) \<notin> r"
+ by (metis FieldI2 assms max2_equals1 max2_equals2 succ_diff succ_in)
lemma not_isSucc_zero: "\<not> isSucc zero"
-proof
- assume *: "isSucc zero"
- then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i"
- unfolding isSucc_def zero_def by auto
- hence "succ i \<in> Field r" by auto
- with * show False
- by (metis REFL isSucc_def minim_least refl_on_domain
- subset_refl succ_in succ_not_in zero_def)
-qed
+ by (metis isSucc_def leq_zero_imp succ_in_diff)
lemma isLim_zero[simp]: "isLim zero"
by (metis isLim_def not_isSucc_zero)
lemma succ_smallest:
-assumes "(i,j) \<in> r" and "i \<noteq> j"
-shows "(succ i, j) \<in> r"
-unfolding succ_def apply(rule suc_least)
-using assms unfolding Field_def by auto
+ assumes "(i,j) \<in> r" and "i \<noteq> j"
+ shows "(succ i, j) \<in> r"
+ unfolding succ_def apply(rule suc_least)
+ using assms unfolding Field_def by auto
lemma isLim_supr:
-assumes f: "i \<in> Field r" and l: "isLim i"
-shows "i = supr (underS i)"
+ assumes f: "i \<in> Field r" and l: "isLim i"
+ shows "i = supr (underS i)"
proof(rule equals_supr)
fix j assume j: "j \<in> Field r" and 1: "\<And> j'. j' \<in> underS i \<Longrightarrow> (j',j) \<in> r"
- show "(i,j) \<in> r" proof(intro in_notinI[OF _ f j], safe)
+ show "(i,j) \<in> r"
+ proof(intro in_notinI[OF _ f j], safe)
assume ji: "(j,i) \<in> r" "j \<noteq> i"
hence a: "aboveS j \<noteq> {}" unfolding aboveS_def by auto
hence "i \<noteq> succ j" using l unfolding isLim_def isSucc_def by auto
@@ -635,17 +514,19 @@
hence "(succ j, j) \<in> r" using 1 by auto
thus False using succ_not_in[OF a] by simp
qed
-qed(insert f, unfold underS_def Field_def, auto)
+qed(use f underS_def Field_def in fastforce)+
definition "pred i \<equiv> SOME j. j \<in> Field r \<and> aboveS j \<noteq> {} \<and> succ j = i"
lemma pred_Field_succ:
-assumes "isSucc i" shows "pred i \<in> Field r \<and> aboveS (pred i) \<noteq> {} \<and> succ (pred i) = i"
+ assumes "isSucc i" shows "pred i \<in> Field r \<and> aboveS (pred i) \<noteq> {} \<and> succ (pred i) = i"
proof-
- obtain j where a: "aboveS j \<noteq> {}" and i: "i = succ j" using assms unfolding isSucc_def by auto
- have 1: "j \<in> Field r" "j \<noteq> i" unfolding Field_def i
- using succ_diff[OF a] a unfolding aboveS_def by auto
- show ?thesis unfolding pred_def apply(rule someI_ex) using 1 i a by auto
+ obtain j where j: "aboveS j \<noteq> {}" "i = succ j"
+ using assms unfolding isSucc_def by auto
+ then obtain "j \<in> Field r" "j \<noteq> i"
+ by (metis FieldI1 succ_diff succ_in)
+ then show ?thesis unfolding pred_def
+ by (metis (mono_tags, lifting) j someI_ex)
qed
lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1]
@@ -653,165 +534,100 @@
lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2]
lemma isSucc_pred_in:
-assumes "isSucc i" shows "(pred i, i) \<in> r"
-proof-
- define j where "j = pred i"
- have i: "i = succ j" using assms unfolding j_def by simp
- have a: "aboveS j \<noteq> {}" unfolding j_def using assms by auto
- show ?thesis unfolding j_def[symmetric] unfolding i using succ_in[OF a] .
-qed
+ assumes "isSucc i" shows "(pred i, i) \<in> r"
+ by (metis assms pred_Field_succ succ_in)
lemma isSucc_pred_diff:
-assumes "isSucc i" shows "pred i \<noteq> i"
-by (metis aboveS_pred assms succ_diff succ_pred)
+ assumes "isSucc i" shows "pred i \<noteq> i"
+ by (metis aboveS_pred assms succ_diff succ_pred)
(* todo: pred maximal, pred injective? *)
lemma succ_inj[simp]:
-assumes "aboveS i \<noteq> {}" and "aboveS j \<noteq> {}"
-shows "succ i = succ j \<longleftrightarrow> i = j"
-proof safe
- assume s: "succ i = succ j"
- {assume "i \<noteq> j" and "(i,j) \<in> r"
- hence "(succ i, j) \<in> r" using assms by (metis succ_smallest)
- hence False using s assms by (metis succ_not_in)
- }
- moreover
- {assume "i \<noteq> j" and "(j,i) \<in> r"
- hence "(succ j, i) \<in> r" using assms by (metis succ_smallest)
- hence False using s assms by (metis succ_not_in)
- }
- ultimately show "i = j" by (metis TOTALS WELL assms(1) assms(2) succ_in_diff well_order_on_domain)
-qed
+ assumes "aboveS i \<noteq> {}" and "aboveS j \<noteq> {}"
+ shows "succ i = succ j \<longleftrightarrow> i = j"
+ by (metis FieldI1 assms succ_def succ_in supr_under under_underS_suc)
lemma pred_succ[simp]:
-assumes "aboveS j \<noteq> {}" shows "pred (succ j) = j"
-unfolding pred_def apply(rule some_equality)
-using assms apply(force simp: Field_def aboveS_def)
-by (metis assms succ_inj)
+ assumes "aboveS j \<noteq> {}" shows "pred (succ j) = j"
+ using assms isSucc_def pred_Field_succ succ_inj by blast
lemma less_succ[simp]:
-assumes "aboveS i \<noteq> {}"
-shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
-apply safe
- apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff)
- apply (metis (opaque_lifting, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD)
- apply (metis assms in_notinI succ_in_Field)
-done
+ assumes "aboveS i \<noteq> {}"
+ shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
+ by (metis FieldI1 assms in_notinI max2_equals1 max2_equals2 max2_iff succ_in succ_smallest)
lemma underS_succ[simp]:
-assumes "aboveS i \<noteq> {}"
-shows "underS (succ i) = under i"
-unfolding underS_def under_def by (auto simp: assms succ_not_in)
+ assumes "aboveS i \<noteq> {}"
+ shows "underS (succ i) = under i"
+ unfolding underS_def under_def by (auto simp: assms succ_not_in)
lemma succ_mono:
-assumes "aboveS j \<noteq> {}" and "(i,j) \<in> r"
-shows "(succ i, succ j) \<in> r"
-by (metis (full_types) assms less_succ succ_smallest)
+ assumes "aboveS j \<noteq> {}" and "(i,j) \<in> r"
+ shows "(succ i, succ j) \<in> r"
+ by (metis (full_types) assms less_succ succ_smallest)
lemma under_succ[simp]:
-assumes "aboveS i \<noteq> {}"
-shows "under (succ i) = insert (succ i) (under i)"
-using less_succ[OF assms] unfolding under_def by auto
+ assumes "aboveS i \<noteq> {}"
+ shows "under (succ i) = insert (succ i) (under i)"
+ using less_succ[OF assms] unfolding under_def by auto
definition mergeSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
-"mergeSL S L f i \<equiv>
- if isSucc i then S (pred i) (f (pred i))
- else L f i"
+ where
+ "mergeSL S L f i \<equiv> if isSucc i then S (pred i) (f (pred i)) else L f i"
subsubsection \<open>Well-order recursion with (zero), succesor, and limit\<close>
definition worecSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where "worecSL S L \<equiv> worec (mergeSL S L)"
+ where "worecSL S L \<equiv> worec (mergeSL S L)"
definition "adm_woL L \<equiv> \<forall>f g i. isLim i \<and> (\<forall>j\<in>underS i. f j = g j) \<longrightarrow> L f i = L g i"
-lemma mergeSL:
-assumes "adm_woL L" shows "adm_wo (mergeSL S L)"
-unfolding adm_wo_def proof safe
- fix f g :: "'a => 'b" and i :: 'a
- assume 1: "\<forall>j\<in>underS i. f j = g j"
- show "mergeSL S L f i = mergeSL S L g i"
- proof(cases "isSucc i")
- case True
- hence "pred i \<in> underS i" unfolding underS_def using isSucc_pred_in isSucc_pred_diff by auto
- thus ?thesis using True 1 unfolding mergeSL_def by auto
- next
- case False hence "isLim i" unfolding isLim_def by auto
- thus ?thesis using assms False 1 unfolding mergeSL_def adm_woL_def by auto
- qed
-qed
+lemma mergeSL: "adm_woL L \<Longrightarrow>adm_wo (mergeSL S L)"
+ unfolding adm_wo_def adm_woL_def isLim_def
+ by (smt (verit, ccfv_threshold) isSucc_pred_diff isSucc_pred_in mergeSL_def underS_I)
lemma worec_fixpoint1: "adm_wo H \<Longrightarrow> worec H i = H (worec H) i"
-by (metis worec_fixpoint)
+ by (metis worec_fixpoint)
lemma worecSL_isSucc:
-assumes a: "adm_woL L" and i: "isSucc i"
-shows "worecSL S L i = S (pred i) (worecSL S L (pred i))"
-proof-
- let ?H = "mergeSL S L"
- have "worecSL S L i = ?H (worec ?H) i"
- unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] .
- also have "... = S (pred i) (worecSL S L (pred i))"
- unfolding worecSL_def mergeSL_def using i by simp
- finally show ?thesis .
-qed
+ assumes a: "adm_woL L" and i: "isSucc i"
+ shows "worecSL S L i = S (pred i) (worecSL S L (pred i))"
+ by (metis a i mergeSL mergeSL_def worecSL_def worec_fixpoint)
lemma worecSL_succ:
-assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
-shows "worecSL S L (succ j) = S j (worecSL S L j)"
-proof-
- define i where "i = succ j"
- have i: "isSucc i" by (metis i i_def isSucc_succ)
- have ij: "j = pred i" unfolding i_def using assms by simp
- have 0: "succ (pred i) = i" using i by simp
- show ?thesis unfolding ij using worecSL_isSucc[OF a i] unfolding 0 .
-qed
+ assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
+ shows "worecSL S L (succ j) = S j (worecSL S L j)"
+ by (simp add: a i isSucc_succ worecSL_isSucc)
lemma worecSL_isLim:
-assumes a: "adm_woL L" and i: "isLim i"
-shows "worecSL S L i = L (worecSL S L) i"
-proof-
- let ?H = "mergeSL S L"
- have "worecSL S L i = ?H (worec ?H) i"
- unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] .
- also have "... = L (worecSL S L) i"
- using i unfolding worecSL_def mergeSL_def isLim_def by simp
- finally show ?thesis .
-qed
+ assumes a: "adm_woL L" and i: "isLim i"
+ shows "worecSL S L i = L (worecSL S L) i"
+ by (metis a i isLim_def mergeSL mergeSL_def worecSL_def worec_fixpoint)
definition worecZSL :: "'b \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where "worecZSL Z S L \<equiv> worecSL S (\<lambda> f a. if a = zero then Z else L f a)"
+ where "worecZSL Z S L \<equiv> worecSL S (\<lambda> f a. if a = zero then Z else L f a)"
lemma worecZSL_zero:
-assumes a: "adm_woL L"
-shows "worecZSL Z S L zero = Z"
-proof-
- let ?L = "\<lambda> f a. if a = zero then Z else L f a"
- have "worecZSL Z S L zero = ?L (worecZSL Z S L) zero"
- unfolding worecZSL_def apply(rule worecSL_isLim)
- using assms unfolding adm_woL_def by auto
- also have "... = Z" by simp
- finally show ?thesis .
-qed
+ assumes a: "adm_woL L"
+ shows "worecZSL Z S L zero = Z"
+ by (smt (verit, best) adm_woL_def assms isLim_zero worecSL_isLim worecZSL_def)
lemma worecZSL_succ:
-assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
-shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)"
-unfolding worecZSL_def apply(rule worecSL_succ)
-using assms unfolding adm_woL_def by auto
+ assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
+ shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)"
+ unfolding worecZSL_def
+ by (smt (verit, best) a adm_woL_def i worecSL_succ)
lemma worecZSL_isLim:
-assumes a: "adm_woL L" and "isLim i" and "i \<noteq> zero"
-shows "worecZSL Z S L i = L (worecZSL Z S L) i"
+ assumes a: "adm_woL L" and "isLim i" and "i \<noteq> zero"
+ shows "worecZSL Z S L i = L (worecZSL Z S L) i"
proof-
let ?L = "\<lambda> f a. if a = zero then Z else L f a"
have "worecZSL Z S L i = ?L (worecZSL Z S L) i"
- unfolding worecZSL_def apply(rule worecSL_isLim)
- using assms unfolding adm_woL_def by auto
- also have "... = L (worecZSL Z S L) i" using assms by simp
+ unfolding worecZSL_def by (smt (verit, best) adm_woL_def assms worecSL_isLim)
+ also have "\<dots> = L (worecZSL Z S L) i" using assms by simp
finally show ?thesis .
qed
@@ -819,70 +635,54 @@
subsubsection \<open>Well-order succ-lim induction\<close>
lemma ord_cases:
-obtains j where "i = succ j" and "aboveS j \<noteq> {}" | "isLim i"
-by (metis isLim_def isSucc_def)
+ obtains j where "i = succ j" and "aboveS j \<noteq> {}" | "isLim i"
+ by (metis isLim_def isSucc_def)
lemma well_order_inductSL[case_names Suc Lim]:
-assumes SUCC: "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and
-LIM: "\<And>i. \<lbrakk>isLim i; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
-shows "P i"
+ assumes "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" "\<And>i. \<lbrakk>isLim i; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
+ shows "P i"
proof(induction rule: well_order_induct)
- fix i assume 0: "\<forall>j. j \<noteq> i \<and> (j, i) \<in> r \<longrightarrow> P j"
- show "P i" proof(cases i rule: ord_cases)
- fix j assume i: "i = succ j" and j: "aboveS j \<noteq> {}"
- hence "j \<noteq> i \<and> (j, i) \<in> r" by (metis succ_diff succ_in)
- hence 1: "P j" using 0 by simp
- show "P i" unfolding i apply(rule SUCC) using 1 j by auto
- qed(insert 0 LIM, unfold underS_def, auto)
+ case (1 x)
+ then show ?case
+ by (metis assms ord_cases succ_diff succ_in underS_E)
qed
lemma well_order_inductZSL[case_names Zero Suc Lim]:
-assumes ZERO: "P zero"
-and SUCC: "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and
-LIM: "\<And>i. \<lbrakk>isLim i; i \<noteq> zero; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
-shows "P i"
-apply(induction rule: well_order_inductSL) using assms by auto
+ assumes "P zero"
+ and "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and
+ "\<And>i. \<lbrakk>isLim i; i \<noteq> zero; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
+ shows "P i"
+ by (metis assms well_order_inductSL)
(* Succesor and limit ordinals *)
definition "isSuccOrd \<equiv> \<exists> j \<in> Field r. \<forall> i \<in> Field r. (i,j) \<in> r"
definition "isLimOrd \<equiv> \<not> isSuccOrd"
lemma isLimOrd_succ:
-assumes isLimOrd and "i \<in> Field r"
-shows "succ i \<in> Field r"
-using assms unfolding isLimOrd_def isSuccOrd_def
-by (metis REFL in_notinI refl_on_domain succ_smallest)
+ assumes isLimOrd and "i \<in> Field r"
+ shows "succ i \<in> Field r"
+ using assms unfolding isLimOrd_def isSuccOrd_def
+ by (metis REFL in_notinI refl_on_domain succ_smallest)
lemma isLimOrd_aboveS:
-assumes l: isLimOrd and i: "i \<in> Field r"
-shows "aboveS i \<noteq> {}"
+ assumes l: isLimOrd and i: "i \<in> Field r"
+ shows "aboveS i \<noteq> {}"
proof-
obtain j where "j \<in> Field r" and "(j,i) \<notin> r"
- using assms unfolding isLimOrd_def isSuccOrd_def by auto
+ using assms unfolding isLimOrd_def isSuccOrd_def by auto
hence "(i,j) \<in> r \<and> j \<noteq> i" by (metis i max2_def max2_greater)
thus ?thesis unfolding aboveS_def by auto
qed
lemma succ_aboveS_isLimOrd:
-assumes "\<forall> i \<in> Field r. aboveS i \<noteq> {} \<and> succ i \<in> Field r"
-shows isLimOrd
-unfolding isLimOrd_def isSuccOrd_def proof safe
- fix j assume j: "j \<in> Field r" "\<forall>i\<in>Field r. (i, j) \<in> r"
- hence "(succ j, j) \<in> r" using assms by auto
- moreover have "aboveS j \<noteq> {}" using assms j unfolding aboveS_def by auto
- ultimately show False by (metis succ_not_in)
-qed
+ assumes "\<forall> i \<in> Field r. aboveS i \<noteq> {} \<and> succ i \<in> Field r"
+ shows isLimOrd
+ using assms isLimOrd_def isSuccOrd_def succ_not_in by blast
lemma isLim_iff:
-assumes l: "isLim i" and j: "j \<in> underS i"
-shows "\<exists> k. k \<in> underS i \<and> j \<in> underS k"
-proof-
- have a: "aboveS j \<noteq> {}" using j unfolding underS_def aboveS_def by auto
- show ?thesis apply(rule exI[of _ "succ j"]) apply safe
- using assms a unfolding underS_def isLim_def
- apply (metis (lifting, full_types) isSucc_def mem_Collect_eq succ_smallest)
- by (metis (lifting, full_types) a mem_Collect_eq succ_diff succ_in)
-qed
+ assumes l: "isLim i" and j: "j \<in> underS i"
+ shows "\<exists> k. k \<in> underS i \<and> j \<in> underS k"
+ by (metis Order_Relation.underS_Field empty_iff isLim_supr j l underS_empty underS_supr)
end (* context wo_rel *)
@@ -903,124 +703,98 @@
definition "oproj r s f \<equiv> Field s \<subseteq> f ` (Field r) \<and> compat r s f"
lemma oproj_in:
-assumes "oproj r s f" and "(a,a') \<in> r"
-shows "(f a, f a') \<in> s"
-using assms unfolding oproj_def compat_def by auto
+ assumes "oproj r s f" and "(a,a') \<in> r"
+ shows "(f a, f a') \<in> s"
+ using assms unfolding oproj_def compat_def by auto
lemma oproj_Field:
-assumes f: "oproj r s f" and a: "a \<in> Field r"
-shows "f a \<in> Field s"
-using oproj_in[OF f] a unfolding Field_def by auto
+ assumes f: "oproj r s f" and a: "a \<in> Field r"
+ shows "f a \<in> Field s"
+ using oproj_in[OF f] a unfolding Field_def by auto
lemma oproj_Field2:
-assumes f: "oproj r s f" and a: "b \<in> Field s"
-shows "\<exists> a \<in> Field r. f a = b"
-using assms unfolding oproj_def by auto
+ assumes f: "oproj r s f" and a: "b \<in> Field s"
+ shows "\<exists> a \<in> Field r. f a = b"
+ using assms unfolding oproj_def by auto
lemma oproj_under:
-assumes f: "oproj r s f" and a: "a \<in> under r a'"
-shows "f a \<in> under s (f a')"
-using oproj_in[OF f] a unfolding under_def by auto
+ assumes f: "oproj r s f" and a: "a \<in> under r a'"
+ shows "f a \<in> under s (f a')"
+ using oproj_in[OF f] a unfolding under_def by auto
(* An ordinal is embedded in another whenever it is embedded as an order
(not necessarily as initial segment):*)
theorem embedI:
-assumes r: "Well_order r" and s: "Well_order s"
-and f: "\<And> a. a \<in> Field r \<Longrightarrow> f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
-shows "\<exists> g. embed r s g"
+ assumes r: "Well_order r" and s: "Well_order s"
+ and f: "\<And> a. a \<in> Field r \<Longrightarrow> f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
+ shows "\<exists> g. embed r s g"
proof-
interpret r: wo_rel r by unfold_locales (rule r)
interpret s: wo_rel s by unfold_locales (rule s)
let ?G = "\<lambda> g a. suc s (g ` underS r a)"
define g where "g = worec r ?G"
have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto
- (* *)
+ (* *)
{fix a assume "a \<in> Field r"
- hence "bij_betw g (under r a) (under s (g a)) \<and>
+ hence "bij_betw g (under r a) (under s (g a)) \<and>
g a \<in> under s (f a)"
- proof(induction a rule: r.underS_induct)
- case (1 a)
- hence a: "a \<in> Field r"
- and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)"
- and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
- and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
- unfolding underS_def Field_def bij_betw_def by auto
- have fa: "f a \<in> Field s" using f[OF a] by auto
- have g: "g a = suc s (g ` underS r a)"
- using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast
- have A0: "g ` underS r a \<subseteq> Field s"
- using IH1b by (metis IH2 image_subsetI in_mono under_Field)
- {fix a1 assume a1: "a1 \<in> underS r a"
- from IH2[OF this] have "g a1 \<in> under s (f a1)" .
- moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
- ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
- }
- hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def
- using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
- hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
- have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
- unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
- {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
- hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
- unfolding underS_def under_def refl_on_def Field_def by auto
- hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
- hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12
- unfolding underS_def under_def by auto
- } note C = this
- have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
- have aa: "a \<in> under r a"
- using a r.REFL unfolding under_def underS_def refl_on_def by auto
- show ?case proof safe
- show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
- show "inj_on g (under r a)" proof(rule r.inj_on_Field)
- fix a1 a2 assume "a1 \<in> under r a" and a2: "a2 \<in> under r a" and a1: "a1 \<in> underS r a2"
- hence a22: "a2 \<in> under r a2" and a12: "a1 \<in> under r a2" "a1 \<noteq> a2"
- using a r.REFL unfolding under_def underS_def refl_on_def by auto
- show "g a1 \<noteq> g a2"
- proof(cases "a2 = a")
- case False hence "a2 \<in> underS r a"
- using a2 unfolding underS_def under_def by auto
- from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto
- qed(insert B a1, unfold underS_def, auto)
- qed(unfold under_def Field_def, auto)
- next
- fix a1 assume a1: "a1 \<in> under r a"
- show "g a1 \<in> under s (g a)"
- proof(cases "a1 = a")
- case True thus ?thesis
- using ga s.REFL unfolding refl_on_def under_def by auto
- next
- case False
- hence a1: "a1 \<in> underS r a" using a1 unfolding underS_def under_def by auto
- thus ?thesis using B unfolding underS_def under_def by auto
- qed
- next
- fix b1 assume b1: "b1 \<in> under s (g a)"
- show "b1 \<in> g ` under r a"
- proof(cases "b1 = g a")
- case True thus ?thesis using aa by auto
- next
- case False
- hence "b1 \<in> underS s (g a)" using b1 unfolding underS_def under_def by auto
- from s.underS_suc[OF this[unfolded g] A0]
- obtain a1 where a1: "a1 \<in> underS r a" and b1: "b1 \<in> under s (g a1)" by auto
- obtain a2 where "a2 \<in> under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto
- hence "a2 \<in> under r a" using a1
- by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans)
- thus ?thesis using b1 by auto
- qed
- qed
- next
- have "(g a, f a) \<in> s" unfolding g proof(rule s.suc_least[OF A0])
- fix b1 assume "b1 \<in> g ` underS r a"
- then obtain a1 where a1: "b1 = g a1" and a1: "a1 \<in> underS r a" by auto
- hence "b1 \<in> underS s (f a)"
- using a by (metis \<open>\<And>a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (f a)\<close>)
- thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding underS_def by auto
- qed(insert fa, auto)
- thus "g a \<in> under s (f a)" unfolding under_def by auto
- qed
- qed
+ proof(induction a rule: r.underS_induct)
+ case (1 a)
+ hence a: "a \<in> Field r"
+ and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)"
+ and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
+ and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
+ unfolding underS_def Field_def bij_betw_def by auto
+ have fa: "f a \<in> Field s" using f[OF a] by auto
+ have g: "g a = suc s (g ` underS r a)"
+ using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast
+ have A0: "g ` underS r a \<subseteq> Field s"
+ using IH1b by (metis IH2 image_subsetI in_mono under_Field)
+ {fix a1 assume a1: "a1 \<in> underS r a"
+ from IH2[OF this] have "g a1 \<in> under s (f a1)" .
+ moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
+ ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
+ }
+ hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def
+ using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
+ hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
+ have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
+ unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
+ {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
+ hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
+ unfolding underS_def under_def refl_on_def Field_def by auto
+ hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
+ hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12
+ unfolding underS_def under_def by auto
+ } note C = this
+ have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
+ have aa: "a \<in> under r a"
+ using a r.REFL unfolding under_def underS_def refl_on_def by auto
+ show ?case proof safe
+ show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
+ show "inj_on g (under r a)"
+ by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
+ next
+ fix a1 assume a1: "a1 \<in> under r a"
+ show "g a1 \<in> under s (g a)"
+ by (metis (mono_tags, lifting) B a1 ga mem_Collect_eq s.in_notinI underS_def under_def)
+ next
+ fix b1 assume b1: "b1 \<in> under s (g a)"
+ show "b1 \<in> g ` under r a"
+ proof(cases "b1 = g a")
+ case True thus ?thesis using aa by auto
+ next
+ case False
+ show ?thesis
+ by (metis b1 A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
+ qed
+ qed
+ next
+ have "(g a, f a) \<in> s" unfolding g
+ using \<open>f a \<in> s.AboveS (g ` r.underS a)\<close> s.suc_least_AboveS by blast
+ thus "g a \<in> under s (f a)" unfolding under_def by auto
+ qed
+ qed
}
thus ?thesis unfolding embed_def by auto
qed
@@ -1028,39 +802,39 @@
corollary ordLeq_def2:
"r \<le>o s \<longleftrightarrow> Well_order r \<and> Well_order s \<and>
(\<exists> f. \<forall> a \<in> Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a))"
-using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s]
-unfolding ordLeq_def by fast
+ using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s]
+ unfolding ordLeq_def by fast
lemma iso_oproj:
assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
shows "oproj r s f"
-using assms unfolding oproj_def
-by (subst (asm) iso_iff3) (auto simp: bij_betw_def)
+ using assms unfolding oproj_def
+ by (metis iso_Field iso_iff3 order_refl)
theorem oproj_embed:
-assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
-shows "\<exists> g. embed s r g"
+ assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
+ shows "\<exists> g. embed s r g"
proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe)
fix b assume "b \<in> Field s"
- thus "inv_into (Field r) f b \<in> Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into)
+ thus "inv_into (Field r) f b \<in> Field r"
+ using oproj_Field2[OF f] by (metis imageI inv_into_into)
next
fix a b assume "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s"
"inv_into (Field r) f a = inv_into (Field r) f b"
- with f show False by (auto dest!: inv_into_injective simp: Field_def oproj_def)
+ with f show False
+ by (meson FieldI1 in_mono inv_into_injective oproj_def)
next
fix a b assume *: "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s"
- { assume "(inv_into (Field r) f a, inv_into (Field r) f b) \<notin> r"
+ { assume notin: "(inv_into (Field r) f a, inv_into (Field r) f b) \<notin> r"
moreover
from *(3) have "a \<in> Field s" unfolding Field_def by auto
- with *(1,2) have
- "inv_into (Field r) f a \<in> Field r" "inv_into (Field r) f b \<in> Field r"
- "inv_into (Field r) f a \<noteq> inv_into (Field r) f b"
- by (auto dest!: oproj_Field2[OF f] inv_into_injective intro!: inv_into_into)
+ then have "(inv_into (Field r) f b, inv_into (Field r) f a) \<in> r"
+ by (meson "*"(1) notin f in_mono inv_into_into oproj_def r wo_rel.in_notinI wo_rel.intro)
ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) \<in> r"
using r by (auto simp: well_order_on_def linear_order_on_def total_on_def)
with f[unfolded oproj_def compat_def] *(1) \<open>a \<in> Field s\<close>
f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"]
- have "(b, a) \<in> s" by (metis in_mono)
+ have "(b, a) \<in> s" by (metis in_mono)
with *(2,3) s have False
by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def)
} thus "(inv_into (Field r) f a, inv_into (Field r) f b) \<in> r" by blast