Theory Bijective_Embedding

theory Bijective_Embedding
  imports "HOL-Library.Countable_Set"
begin

text ‹Generalization of @{thm image_vimage_eq}›
lemma inj_on_vimage_image_eq: "f -` (f ` A) ∩ S = A" if "inj_on f S" "A ⊆ S"
  using that unfolding inj_on_def by blast

text ‹Generalization of @{thm card_vimage_inj}›
theorem card_vimage_inj_on:
  fixes f :: "'a ⇒ 'b"
    and A :: "'b set"
  assumes "inj_on f S"
    and "A ⊆ f ` S"
  shows "card (f -` A ∩ S) = card A"
  using assms
  by (auto 4 3 simp: subset_image_iff inj_on_vimage_image_eq
      intro: card_image[symmetric, OF subset_inj_on])

context
begin

private lemma finiteI: "finite {x. x ∈ A ∧ ordX x ≤ ordX a ∧ Q x}" (is "finite ?S")
    if "inj_on ordX A" for A a Q and ordX :: "_ ⇒ nat"
proof -
  have "?S ⊆ {x. x ∈ A ∧ ordX x ≤ ordX a}"
    by blast
  moreover have "finite …"
  proof -
    have "… = ordX -` {n. n ≤ ordX a} ∩ A"
      by auto
    moreover from ‹inj_on ordX A› have "finite …"
      by (intro finite_vimage_IntI) auto
    ultimately show ?thesis
      by simp
  qed
  ultimately show ?thesis
    by (rule finite_subset)
qed

qualified lemma enumeration_skip_finite_set_surj:
  "∃a. a ∈ A ∧ a ∉ S ∧ card {x ∈ A. ordX x ≤ ordX a ∧ x ∉ S} = n"
  if "n > 0" "inj_on ordX A" "ordX ` A = ℕ" "finite S" "S ⊆ A" for ordX :: "_ ⇒ nat"
  using ‹finite S› ‹n > 0› ‹S ⊆ A›
proof (induction arbitrary: n)
  case empty
  let ?a = "the_inv_into A ordX (n - 1)"
  have "card {x ∈ A. ordX x ≤ n - 1} = n"
  proof -
    have "{x ∈ A. ordX x ≤ n - 1} = ordX -` {x. x ≤ n - 1} ∩ A"
      by auto
    moreover have "card … = card {x. x ≤ n - 1}"
      using ‹inj_on ordX _› ‹ordX ` A = ℕ› by (intro card_vimage_inj_on) (auto simp: Nats_def)
    moreover have "… = n"
      using ‹n > 0› by auto
    ultimately show ?thesis
      by auto
  qed
  then have "∃ a ∈ A. card {x ∈ A. ordX x ≤ ordX a} = n"
    using ‹inj_on ordX A› ‹ordX ` A = ℕ›
    unfolding Nats_def
    by (intro bexI[where x = "the_inv_into A ordX (n - 1)"])
       (auto intro: the_inv_into_into simp: f_the_inv_into_f[where f = ordX])
  then show ?case
    by auto
next
  case (insert x F)
  then obtain a where a: "a ∈ A" "a ∉ F" "card {x ∈ A. ordX x ≤ ordX a ∧ x ∉ F} = n"
    by blast
  show ?case
  proof (cases "ordX x ≤ ordX a")
    case True
    then have *:
      "{xa ∈ A. ordX xa ≤ ordX a ∧ xa ∉ insert x F} = {x ∈ A. ordX x ≤ ordX a ∧ x ∉ F} - {x}"
      by auto
    let ?m = "Max (ordX ` F)"
    show ?thesis
    proof (cases "∃b ∈ A. b ∉ F ∧ ordX a < ordX b ∧ ordX b ≤ ?m")
      case False
      let ?a = "the_inv_into A ordX (max ?m (ordX a) + 1)"
      let ?S = "{xa ∈ A. ordX xa ≤ ordX ?a ∧ xa ∉ insert x F}"
      have "?a ∈ A"
        by (simp add: Nats_def ‹inj_on ordX A› ‹ordX ` A = ℕ› the_inv_into_into)
      have "ordX ?a = max ?m (ordX a) + 1"
        using ‹inj_on ordX A› ‹ordX ` A = ℕ› unfolding Nats_def
        by (subst f_the_inv_into_f[where f = ordX]) auto
      then have "?S = {xa ∈ A. ordX xa ≤ max ?m (ordX a) + 1 ∧ xa ∉ insert x F}"
        by simp
      also have "… = {xa ∈ A. ordX xa ≤ ordX a ∧ xa ∉ insert x F} ∪ {?a}"
      proof -
        have "{xa ∈ A. ordX xa = max ?m (ordX a) + 1 ∧ xa ∉ insert x F} = {?a}"
          unfolding ‹ordX ?a = _›
          apply (auto simp: ‹inj_on ordX A› the_inv_into_f_eq)
          using True ‹ordX ?a = _› ‹?a ∈ A›
          apply -
          apply (auto; fail)+
          by (metis Max.boundedE Suc_eq_plus1 Suc_n_not_le_n emptyE finite_imageI imageI
                insert.hyps(1) max.cobounded1)
        have *: "{xa ∈ A. ordX xa ≤ ordX a ∧ xa ∉ insert x F}
              = {xa ∈ A. ordX xa ≤ max ?m (ordX a) ∧ xa ∉ insert x F}"
          using False by auto
        show ?thesis
          unfolding ‹_ = {?a}›[symmetric] * by auto
      qed
      finally have "?S = ({x ∈ A. ordX x ≤ ordX a ∧ x ∉ F} - {x}) ∪ {?a}"
        by auto
      moreover have "?a ≠ x"
        using True ‹ordX ?a = max (MAX x ∈ F. ordX x) (ordX a) + 1› by auto
      moreover have "?a ∉ {x ∈ A. ordX x ≤ ordX a ∧ x ∉ F}"
        using ‹ordX ?a = max (MAX x ∈ F. ordX x) (ordX a) + 1› by auto
      moreover have "x ∈ {x ∈ A. ordX x ≤ ordX a ∧ x ∉ F}"
        using ‹ordX x ≤ _› ‹insert x _ ⊆ A› ‹x ∉ F› by auto
      ultimately have "card ?S = card {x ∈ A. ordX x ≤ ordX a ∧ x ∉ F}"
        apply simp
        apply (subst card_insert_disjoint)
        subgoal
          by (force intro: finiteI[OF ‹inj_on ordX A›, of a])
        apply simp
        apply (subst card.remove[symmetric])
        subgoal
          by (force intro: finiteI[OF ‹inj_on ordX A›, of a])
        by auto
      also have "… = n"
        using ‹_ = n› by auto
      finally show ?thesis
        using ‹inj_on ordX A› ‹ordX ` A = ℕ› unfolding Nats_def
        apply -
        apply (rule exI[where x = ?a], rule conjI)
         apply (auto intro: the_inv_into_into)
        using ‹ordX x ≤ _›
          apply (subgoal_tac "ordX x = Suc (ordX a)"; simp add: f_the_inv_into_f[where f = ordX])
         apply (subgoal_tac "ordX ?a ≤ ?m")
        subgoal
          using False
          apply (simp add: f_the_inv_into_f[where f = ordX])
          done
         apply (rule Max_ge)
        using ‹finite F› apply (rule finite_imageI)
         apply (rule imageI)
         apply (simp add: f_the_inv_into_f[where f = ordX])
        done
    next
      case True
      let ?M = "{b ∈ A. ordX a < ordX b ∧ ordX b ≤ ?m ∧ b ∉ F}"
      from True have "?M ≠ {}"
        by auto
      have "finite ?M"
      proof -
        have "?M ⊆ {b ∈ A. ordX b ≤ ?m}"
          by auto
        moreover have "finite …"
        proof -
          have *: "… = ordX -` {x. x ≤ ?m} ∩ A"
            by auto
          from ‹inj_on ordX A› show ?thesis
            unfolding * by (intro finite_vimage_IntI) auto
        qed
        ultimately show ?thesis
          by (rule finite_subset)
      qed
      let ?a = "arg_min_on ordX ?M"
      from arg_min_if_finite[OF ‹finite ?M› ‹?M ≠ {}›, of ordX] have a:
        "?a ∈ ?M" "¬ (∃ x ∈ ?M. ordX x < ordX ?a)"
        by fast+
      with ‹ordX x ≤ ordX a› have "?a ≠ x"
        by auto
      then have **: "{xa ∈ A. ordX xa ≤ ordX ?a ∧ xa ≠ x ∧ xa ∉ F} =
            {xa ∈ A. ordX xa ≤ ordX a ∧ xa ≠ x ∧ xa ∉ F} ∪ {?a}"
        using a
        by auto
           (smt ‹inj_on ordX A› inj_on_eq_iff le_eq_less_or_eq le_trans mem_Collect_eq not_le)
      have "?a ∉ {xa ∈ A. ordX xa ≤ ordX a ∧ xa ≠ x ∧ xa ∉ F}"
        using a(1) by auto
      then have "card {xa ∈ A. ordX xa ≤ ordX ?a ∧ xa ≠ x ∧ xa ∉ F} = n"
        unfolding *[simplified] **
        using ‹card _ = n›
        apply simp
        apply (subst card_insert_disjoint)
        subgoal
          by (auto intro: finiteI[OF ‹inj_on ordX A›])
        apply simp
        apply (subst card.remove[symmetric])
        subgoal
          by (auto intro: finiteI[OF ‹inj_on ordX A›])
        subgoal
          using ‹insert x F ⊆ A› ‹ordX x ≤ _› ‹x ∉ F› by simp
        apply assumption
        done
      then show ?thesis
        using a(1) ‹ordX x ≤ _› by (intro exI[where x = ?a]) auto
    qed
  next
    case False
    then have
      "{xa ∈ A. ordX xa ≤ ordX a ∧ xa ∉ insert x F} = {x ∈ A. ordX x ≤ ordX a ∧ x ∉ F}"
      by auto
    with a False show ?thesis
      by (intro exI[where x = a]) auto
  qed
qed

lemma bij_betw_relI:
  assumes "⋀x y z. x ∈ A ⟹ y ∈ B ⟹ z ∈ B ⟹ R x y ⟹ R x z ⟹ y = z"
      and "⋀x y z. x ∈ A ⟹ y ∈ A ⟹ z ∈ B ⟹ R x z ⟹ R y z ⟹ x = y"
      and "⋀x. x ∈ A ⟹ ∃y ∈ B. R x y" "⋀y. y ∈ B ⟹ ∃x ∈ A. R x y"
  shows "bij_betw (λa. SOME b. R a b ∧ b ∈ B) A B"
  by (rule bij_betwI'; smt assms someI)

lemma bijective_embedding:
  fixes f :: "'a ⇒ 'b"
    and A :: "'a set" and B :: "'b set"
    and S :: "'a set"
  assumes "inj_on f S" and "S ⊆ A" and "f ` S ⊆ B"
    and "finite S"
    and "countable A" and "countable B"
    and "infinite A" and "infinite B"
  shows "∃h. bij_betw h A B ∧ (∀x ∈ S. h x = f x)"
proof -
  obtain ordX :: "_ ⇒ nat" and ordY :: "_ ⇒ nat" where
    "inj_on ordX A" "ordX ` A = ℕ" and "inj_on ordY B" "ordY ` B = ℕ"
    using assms(5-) unfolding Nats_def
    by (metis bij_betw_def bij_betw_from_nat_into bij_betw_imp_inj_on bij_betw_the_inv_into
        of_nat_id surj_def)
  define P where "P a b ≡ a ∈ A ∧ b ∈ B ∧ a ∉ S ∧ b ∉ f ` S ∧
    card {x. x ∈ A ∧ ordX x ≤ ordX a ∧ x ∉ S} = card {x. x ∈ B ∧ ordY x ≤ ordY b ∧ x ∉ f ` S}"
    for a b
  let ?f = "λa. card {x. x ∈ A ∧ ordX x ≤ ordX a ∧ x ∉ S}"
  let ?g = "λa. card {x. x ∈ B ∧ ordY x ≤ ordY a ∧ x ∉ f ` S}"
  have P_right: "∃ b. P a b" if "a ∈ A" "a ∉ S" for a
  proof -
    have *: "∃b. b ∈ B ∧ b ∉ f ` S ∧ ?g b = n" if "n > 0" for n
      using ‹n > 0› ‹finite S› ‹f ` S ⊆ B› ‹inj_on ordY B› ‹ordY ` B = ℕ›
      by (intro enumeration_skip_finite_set_surj) auto
    from that have "?f a > 0"
      unfolding card_gt_0_iff by (auto intro: finiteI[OF ‹inj_on ordX A›])
    from *[OF this] show ?thesis
      unfolding P_def using that by auto
  qed
  have P_left: "∃a. P a b" if "b ∈ B" "b ∉ f ` S" for b
    using that ‹finite S› ‹S ⊆ A› ‹inj_on ordX A› ‹inj_on ordY B› ‹ordX ` A = ℕ› unfolding P_def
    by (auto 4 3 intro: enumeration_skip_finite_set_surj finiteI simp: card_gt_0_iff)
  have P_surj: "a = b" if "P a c" "P b c" for a b c
  proof -
    from that have "?f a = ?f b" (is "card ?A = card ?B")
      unfolding P_def by auto
    have fin: "finite ?A" "finite ?B"
      by (intro finiteI ‹inj_on ordX A›)+
    have *: "a ∈ A" "b ∈ A" "a ∉ S" "b ∉ S"
      using that unfolding P_def by auto
    consider (lt) "ordX a < ordX b" | (eq) "ordX a = ordX b" | (gt) "ordX a > ordX b"
      by force
    then show ?thesis
    proof cases
      case lt
      with * have "?f a < ?f b"
        using leD by (intro psubset_card_mono fin) auto
      with ‹?f a = ?f b› show ?thesis
        by auto
    next
      case eq
      then show ?thesis
        using ‹inj_on ordX A› ‹a ∈ A› ‹b ∈ A› by (auto dest: inj_onD)
    next
      case gt
      with * have "?f a > ?f b"
        using leD by (intro psubset_card_mono fin) auto
      with ‹?f a = ?f b› show ?thesis
        by auto
    qed
  qed
  have P_inj: "b = c" if "P a b" "P a c" for a b c
  proof -
    from that have "?g b = ?g c" (is "card ?A = card ?B")
      unfolding P_def by auto
    have fin: "finite ?A" "finite ?B"
      by (intro finiteI ‹inj_on ordY B›)+
    have *: "b ∈ B" "c ∈ B" "b ∉ f ` S" "c ∉ f ` S"
      using that unfolding P_def by auto
    consider (lt) "ordY b < ordY c" | (eq) "ordY b = ordY c" | (gt) "ordY b > ordY c"
      by force
    then show ?thesis
    proof cases
      case lt
      with * have "?g b < ?g c"
        using leD by (intro psubset_card_mono fin) (auto, blast)
      with ‹?g b = ?g c› show ?thesis
        by auto
    next
      case eq
      then show ?thesis
        using ‹inj_on ordY B› ‹b ∈ B› ‹c ∈ B› by (auto dest: inj_onD)
    next
      case gt
      with * have "?g b > ?g c"
        using leD by (intro psubset_card_mono fin) (auto, blast)
      with ‹?g b = ?g c› show ?thesis
        by auto
    qed
  qed

  define R where "R a b ≡ if a ∈ S then b = f a else P a b" for a b
  have R_A: "a ∈ A" and R_B: "b ∈ B" if "R a b" for a b
    using that ‹f ` S ⊆ B› ‹S ⊆ A› unfolding R_def by (auto split: if_split_asm simp: P_def)
  have R_inj: "b = c" if "R a b" "R a c" for a b c
    using that unfolding R_def by (auto split: if_split_asm dest: P_inj)
  moreover have R_surj: "a = b" if "R a c" "R b c" for a b c
    using that unfolding R_def
    by (auto split: if_split_asm dest: P_surj inj_onD[OF ‹inj_on f S›]) (auto simp: P_def)
  moreover have R_right: "∃b. R a b" if "a ∈ A" for a
    unfolding R_def by (auto dest: P_right[OF ‹a ∈ A›])
  moreover have R_left: "∃a. R a b" if "b ∈ B" for b
    unfolding R_def
    by (cases "b ∈ f ` S", (auto; fail), (frule P_left[OF ‹b ∈ B›], auto simp: P_def))
  ultimately show ?thesis
    apply (intro exI[of _ "λa. SOME b. R a b ∧ b ∈ B"] conjI)
     apply (rule bij_betw_relI)
        apply assumption+
      apply (smt R_A R_B)+
    using assms(3) by (subst R_def) (simp, blast)
qed

end

definition extend_bij :: "('a :: countable ⇒ 'b :: countable) ⇒ 'a set ⇒ _" where
  "extend_bij f S ≡ SOME h. bij h ∧ (∀x ∈ S. h x = f x)"

lemma
  fixes f :: "'a  :: countable ⇒ 'b :: countable" and S :: "'a set"
  assumes "infinite (UNIV :: 'a set)" and "infinite (UNIV :: 'b set)"
      and "inj_on f S" and "finite S"
    shows extend_bij_bij: "bij (extend_bij f S)"
      and extend_bij_extends: "∀x ∈ S. extend_bij f S x = f x"
proof -
  from bijective_embedding[OF assms(3) _ _ assms(4) _ _ assms(1,2)] obtain h where
    "bij h ∧ (∀x∈S. h x = f x)"
    by auto
  then show "bij (extend_bij f S)" "∀x ∈ S. extend_bij f S x = f x"
    unfolding atomize_conj extend_bij_def by (rule someI[where x = h])
qed

end