src/HOL/Cardinals/Cardinal_Order_Relation.thy

normalize imports

(*  Title:      HOL/Cardinals/Cardinal_Order_Relation.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Cardinal-order relations.
*)

section \<open>Cardinal-Order Relations\<close>

theory Cardinal_Order_Relation
imports Wellorder_Constructions
begin

declare
  card_order_on_well_order_on[simp]
  card_of_card_order_on[simp]
  card_of_well_order_on[simp]
  Field_card_of[simp]
  card_of_Card_order[simp]
  card_of_Well_order[simp]
  card_of_least[simp]
  card_of_unique[simp]
  card_of_mono1[simp]
  card_of_mono2[simp]
  card_of_cong[simp]
  card_of_Field_ordLess[simp]
  card_of_Field_ordIso[simp]
  card_of_underS[simp]
  ordLess_Field[simp]
  card_of_empty[simp]
  card_of_empty1[simp]
  card_of_image[simp]
  card_of_singl_ordLeq[simp]
  Card_order_singl_ordLeq[simp]
  card_of_Pow[simp]
  Card_order_Pow[simp]
  card_of_Plus1[simp]
  Card_order_Plus1[simp]
  card_of_Plus2[simp]
  Card_order_Plus2[simp]
  card_of_Plus_mono1[simp]
  card_of_Plus_mono2[simp]
  card_of_Plus_mono[simp]
  card_of_Plus_cong2[simp]
  card_of_Plus_cong[simp]
  card_of_Un_Plus_ordLeq[simp]
  card_of_Times1[simp]
  card_of_Times2[simp]
  card_of_Times3[simp]
  card_of_Times_mono1[simp]
  card_of_Times_mono2[simp]
  card_of_ordIso_finite[simp]
  card_of_Times_same_infinite[simp]
  card_of_Times_infinite_simps[simp]
  card_of_Plus_infinite1[simp]
  card_of_Plus_infinite2[simp]
  card_of_Plus_ordLess_infinite[simp]
  card_of_Plus_ordLess_infinite_Field[simp]
  infinite_cartesian_product[simp]
  cardSuc_Card_order[simp]
  cardSuc_greater[simp]
  cardSuc_ordLeq[simp]
  cardSuc_ordLeq_ordLess[simp]
  cardSuc_mono_ordLeq[simp]
  cardSuc_invar_ordIso[simp]
  card_of_cardSuc_finite[simp]
  cardSuc_finite[simp]
  card_of_Plus_ordLeq_infinite_Field[simp]
  curr_in[intro, simp]


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}|"
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
  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

lemma internalize_card_of_ordLess:
"( |A| <o r) = (\<exists>B < Field r. |A| =o |B| \<and> |B| <o r)"
proof
  assume "|A| <o r"
  then obtain p where 1: "Field p < Field r \<and> |A| =o p \<and> p <o r"
  using internalize_ordLess[of "|A|" r] by blast
  hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
  hence "|Field p| =o p" using card_of_Field_ordIso by blast
  hence "|A| =o |Field p| \<and> |Field p| <o r"
  using 1 ordIso_equivalence ordIso_ordLess_trans by blast
  thus "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r" using 1 by blast
next
  assume "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r"
  thus "|A| <o r" using ordIso_ordLess_trans by blast
qed

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

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

lemma Card_order_omax2:
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
  ultimately show ?thesis by(rule Card_order_omax)
qed


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

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_diff[simp]:
shows "|A - B| \<le>o |A|"
using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] 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

corollary subset_ordLeq_diff:
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

lemma card_of_empty5:
"|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

lemma card_of_UNIV[simp]:
"|A :: 'a set| \<le>o |UNIV :: 'a set|"
using card_of_mono1[of A] 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

lemma card_of_Pow_mono[simp]:
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
  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)
  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

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

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

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

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

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

lemma Un_Plus_bij_betw:
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)
  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

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

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

lemma card_of_Times_singl1: "|A| =o |A \<times> {b}|"
proof-
  have "bij_betw fst (A \<times> {b}) 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_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

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
  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

lemma card_of_Times_assoc: "|(A \<times> B) \<times> C| =o |A \<times> B \<times> C|"
proof -
  let ?f = "\<lambda>((a,b),c). (a,(b,c))"
  have "A \<times> B \<times> C \<subseteq> ?f ` ((A \<times> B) \<times> C)"
  proof
    fix x assume "x \<in> A \<times> B \<times> C"
    then obtain a b c where *: "a \<in> A" "b \<in> B" "c \<in> C" "x = (a, b, c)" by blast
    let ?x = "((a, b), c)"
    from * have "?x \<in> (A \<times> B) \<times> C" "x = ?f ?x" by auto
    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
  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)