Theory HOL-Cardinals.Wellorder_Embedding

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

Well-order embeddings.
*)

section ‹Well-Order Embeddings›

theory Wellorder_Embedding
  imports Fun_More Wellorder_Relation
begin

subsection ‹Auxiliaries›

lemma UNION_bij_betw_ofilter:
  assumes WELL: "Well_order r" and
    OF: "⋀ i. i ∈ I ⟹ ofilter r (A i)" and
    BIJ: "⋀ i. i ∈ I ⟹ bij_betw f (A i) (A' i)"
  shows "bij_betw f (⋃i ∈ I. A i) (⋃i ∈ I. A' i)"
proof-
  have "wo_rel r" using WELL by (simp add: wo_rel_def)
  hence "⋀ i j. ⟦i ∈ I; j ∈ I⟧ ⟹ A i ≤ A j ∨ A j ≤ A i"
    using wo_rel.ofilter_linord[of r] OF by blast
  with WELL BIJ show ?thesis
    by (auto simp add: bij_betw_UNION_chain)
qed


subsection ‹(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
functions›

lemma embed_halfcong:
  assumes "⋀ a. a ∈ Field r ⟹ f a = g a" and "embed r r' f"
  shows "embed r r' g"
  by (smt (verit, del_insts) assms bij_betw_cong embed_def in_mono under_Field)

lemma embed_cong[fundef_cong]:
  assumes "⋀ a. a ∈ Field r ⟹ f a = g a"
  shows "embed r r' f = embed r r' g"
  by (metis assms embed_halfcong)

lemma embedS_cong[fundef_cong]:
  assumes "⋀ a. a ∈ Field r ⟹ f a = g a"
  shows "embedS r r' f = embedS r r' g"
  unfolding embedS_def using assms
    embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast

lemma iso_cong[fundef_cong]:
  assumes "⋀ a. a ∈ Field r ⟹ f a = g a"
  shows "iso r r' f = iso r r' g"
  unfolding iso_def using assms
    embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast

lemma id_compat: "compat r r id"
  by(auto simp add: id_def compat_def)

lemma comp_compat:
  "⟦compat r r' f; compat r' r'' f'⟧ ⟹ compat r r'' (f' o f)"
  by(auto simp add: comp_def compat_def)

corollary one_set_greater:
  "(∃f::'a ⇒ 'a'. f ` A ≤ A' ∧ inj_on f A) ∨ (∃g::'a' ⇒ 'a. g ` A' ≤ A ∧ inj_on g A')"
proof-
  obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)
  hence 1: "A = Field r ∧ Well_order r"
    using well_order_on_Well_order by auto
  obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)
  hence 2: "A' = Field r' ∧ Well_order r'"
    using well_order_on_Well_order by auto
  hence "(∃f. embed r r' f) ∨ (∃g. embed r' r g)"
    using 1 2 by (auto simp add: wellorders_totally_ordered)
  moreover
  {fix f assume "embed r r' f"
    hence "f`A ≤ A' ∧ inj_on f A"
      using 1 2 by (auto simp add: embed_Field embed_inj_on)
  }
  moreover
  {fix g assume "embed r' r g"
    hence "g`A' ≤ A ∧ inj_on g A'"
      using 1 2 by (auto simp add: embed_Field embed_inj_on)
  }
  ultimately show ?thesis by blast
qed

corollary one_type_greater:
  "(∃f::'a ⇒ 'a'. inj f) ∨ (∃g::'a' ⇒ 'a. inj g)"
  using one_set_greater[of UNIV UNIV] by auto


subsection ‹Uniqueness of embeddings›

lemma comp_embedS:
  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
    and  EMB: "embedS r r' f" and EMB': "embedS r' r'' f'"
  shows "embedS r r'' (f' o f)"
  using EMB EMB' WELL WELL' embedS_comp_embed embedS_def by blast

lemma iso_iff4:
  assumes WELL: "Well_order r"  and WELL': "Well_order r'"
  shows "iso r r' f = (embed r r' f ∧ embed r' r (inv_into (Field r) f))"
  using assms embed_bothWays_iso
  by(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw)

lemma embed_embedS_iso:
  "embed r r' f = (embedS r r' f ∨ iso r r' f)"
  unfolding embedS_def iso_def by blast

lemma not_embedS_iso:
  "¬ (embedS r r' f ∧ iso r r' f)"
  unfolding embedS_def iso_def by blast

lemma embed_embedS_iff_not_iso:
  assumes "embed r r' f"
  shows "embedS r r' f = (¬ iso r r' f)"
  using assms unfolding embedS_def iso_def by blast

lemma iso_inv_into:
  assumes WELL: "Well_order r" and ISO: "iso r r' f"
  shows "iso r' r (inv_into (Field r) f)"
  by (meson ISO WELL bij_betw_inv_into inv_into_Field_embed_bij_betw iso_def iso_iff iso_iff2)

lemma embedS_or_iso:
  assumes WELL: "Well_order r" and WELL': "Well_order r'"
  shows "(∃g. embedS r r' g) ∨ (∃h. embedS r' r h) ∨ (∃f. iso r r' f)"
  by (metis WELL WELL' embed_embedS_iso embed_embedS_iso iso_iff4 wellorders_totally_ordered)

end