Theory Transport_Existential_Quantifier

✐‹creator "Kevin Kappelmann"›
✐‹creator "Nils Harmsen"›
section ‹White-Box Transport of (Bounded) Existential Quantifier›
theory Transport_Existential_Quantifier
  imports
    Transport_Universal_Quantifier
begin

paragraph ‹Summary›
text ‹Theorems for white-box transports of (bounded) existential quantifiers.›

context
  fixes R :: "'a ⇒ 'b ⇒ bool" and P :: "'a ⇒ bool" and Q :: "'b ⇒ bool"
begin

lemma Fun_Rel_restricts_imp_bex_if_left_total_onI:
  assumes "left_total_on P R↿⇘Q⇙"
  shows "((R↾⇘P⇙↿⇘Q⇙ ⇛ (⟶)) ⇛ (⟶)) ∃⇘P⇙ ∃⇘Q⇙"
  using assms by (intro Fun_Rel_relI) fast

lemma Fun_Rel_restricts_rev_imp_bex_if_rel_surjective_at:
  assumes "rel_surjective_at Q R↾⇘P⇙"
  shows "((R↾⇘P⇙↿⇘Q⇙ ⇛ (⟵)) ⇛ (⟵)) ∃⇘P⇙ ∃⇘Q⇙"
  using assms by (intro Fun_Rel_relI) fast

lemma Fun_Rel_restricts_iff_bex_if_left_total_on_if_rel_surjective_at:
  assumes "rel_surjective_at Q R↾⇘P⇙"
  and "left_total_on P R↿⇘Q⇙"
  shows "((R↾⇘P⇙↿⇘Q⇙ ⇛ (⟷)) ⇛ (⟷)) ∃⇘P⇙ ∃⇘Q⇙"
  using assms by (intro Fun_Rel_relI) fast

corollary Fun_Rel_restricts_iff_bex_if_bi_total_on:
  assumes "bi_total_on P Q R↾⇘P⇙↿⇘Q⇙"
  shows "((R↾⇘P⇙↿⇘Q⇙ ⇛ (⟷)) ⇛ (⟷)) ∃⇘P⇙ ∃⇘Q⇙"
  using assms by (intro Fun_Rel_restricts_iff_bex_if_left_total_on_if_rel_surjective_at)
  fast+

lemma left_total_on_restrict_right_if_Fun_Rel_imp_bex:
  assumes "((R ⇛ (⟶)) ⇛ (⟶)) ∃⇘P⇙ ∃⇘Q⇙"
  shows "left_total_on P R↿⇘Q⇙"
proof
  fix x assume "P x"
  let ?P1 = "(=) x" and ?P2 = "R x"
  have "(R ⇛ (⟶)) ?P1 ?P2" by auto
  with assms have "∃⇘P⇙ ?P1 ⟶ ∃⇘Q⇙ ?P2" by blast
  with ‹P x› show "in_dom R↿⇘Q⇙ x" by blast
qed

corollary Fun_Rel_imp_all_on_iff_left_total_on_restrict_right:
  "((R ⇛ (⟶)) ⇛ (⟶)) ∃⇘P⇙ ∃⇘Q⇙ ⟷ left_total_on P R↿⇘Q⇙"
  by (blast intro: Fun_Rel_restricts_imp_bex_if_left_total_onI
    Fun_Rel_Fun_Rel_if_le_left_if_Fun_Rel_Fun_Rel
    left_total_on_restrict_right_if_Fun_Rel_imp_bex)

lemma rel_surjective_at_restrict_left_if_Fun_Rel_rev_imp_bex:
  assumes "((R ⇛ (⟵)) ⇛ (⟵)) ∃⇘P⇙ ∃⇘Q⇙"
  shows "rel_surjective_at Q R↾⇘P⇙"
proof
  fix y assume "Q y"
  let ?P1 = "R¯ y" and ?P2 = "(=) y"
  have "(R ⇛ (⟵)) ?P1 ?P2" by auto
  with assms have "∃⇘P⇙ ?P1 ⟵ ∃⇘Q⇙ ?P2" by blast
  with ‹Q y› show "in_codom R↾⇘P⇙ y" by blast
qed

corollary Fun_Rel_rev_imp_bex_iff_rel_surjective_at_restrict_left:
  "((R ⇛ (⟵)) ⇛ (⟵)) ∃⇘P⇙ ∃⇘Q⇙ ⟷ rel_surjective_at Q R↾⇘P⇙"
  by (blast intro: Fun_Rel_restricts_rev_imp_bex_if_rel_surjective_at
    Fun_Rel_Fun_Rel_if_le_left_if_Fun_Rel_Fun_Rel
    rel_surjective_at_restrict_left_if_Fun_Rel_rev_imp_bex)

lemma bi_total_on_if_Fun_Rel_iff_bex:
  assumes "((R ⇛ (⟷)) ⇛ (⟷)) ∃⇘P⇙ ∃⇘Q⇙"
  shows "bi_total_on P Q R"
proof (intro bi_total_onI left_total_onI rel_surjective_atI; rule ccontr)
  fix x assume "P x" and not_dom: "¬(in_dom R x)"
  let ?P1 = "(=) x" and ?P2 = "R x"
  from not_dom have "(R ⇛ (⟷)) ?P1 ?P2" by blast
  with assms have "(∃x : P. ?P1 x) ⟷ (∃y : Q. ?P2 y)" by blast
  with ‹P x› not_dom show "False" by blast
next
  fix y assume "Q y" and not_codom: "¬(in_codom R y)"
  let ?P1 = "λx. R x y" and ?P2 = "(=) y"
  from not_codom have "(R ⇛ (⟷)) ?P1 ?P2" by blast
  with assms have "(∃x : P. ?P1 x) ⟷ (∃y : Q. ?P2 y)" by blast
  with ‹Q y› not_codom show "False" by blast
qed

corollary Fun_Rel_iff_bex_iff_bi_total_on_if_Fun_Rel_iff:
  assumes "(R ⇛ (⟷)) P Q"
  shows "((R ⇛ (⟷)) ⇛ (⟷)) ∃⇘P⇙ ∃⇘Q⇙ ⟷ bi_total_on P Q R"
  using assms by (blast intro: Fun_Rel_restricts_iff_bex_if_bi_total_on
    Fun_Rel_Fun_Rel_if_le_left_if_Fun_Rel_Fun_Rel
    bi_total_on_restricts_if_Fun_Rel_iff_if_bi_total_on
    bi_total_on_if_Fun_Rel_iff_bex)

end

context
  fixes R :: "'a ⇒ 'b ⇒ bool"
begin

corollary Fun_Rel_imp_ex_if_left_total:
  assumes "left_total R"
  shows "((R ⇛ (⟶)) ⇛ (⟶)) Ex Ex"
  using assms by (urule Fun_Rel_restricts_imp_bex_if_left_total_onI)

corollary Fun_Rel_rev_imp_ex_if_rel_surjective:
  assumes "rel_surjective R"
  shows "((R ⇛ (⟵)) ⇛ (⟵)) Ex Ex"
  using assms by (urule Fun_Rel_restricts_rev_imp_bex_if_rel_surjective_at)

corollary Fun_Rel_iff_ex_if_bi_total:
  assumes "bi_total R"
  shows "((R ⇛ (⟷)) ⇛ (⟷)) Ex Ex"
  using assms by (urule Fun_Rel_restricts_iff_bex_if_bi_total_on)

corollary left_total_if_Fun_Rel_imp_ex:
  assumes "((R ⇛ (⟶)) ⇛ (⟶)) Ex Ex"
  shows "left_total R"
  using assms by (urule left_total_on_restrict_right_if_Fun_Rel_imp_bex)

corollary Fun_Rel_imp_ex_iff_left_total:
  "((R ⇛ (⟶)) ⇛ (⟶)) Ex Ex ⟷ left_total R"
  using left_total_if_Fun_Rel_imp_ex Fun_Rel_imp_ex_if_left_total by blast

corollary rel_surjective_if_Fun_Rel_rev_imp_ex:
  assumes "((R ⇛ (⟵)) ⇛ (⟵)) Ex Ex"
  shows "rel_surjective R"
  using assms by (urule rel_surjective_at_restrict_left_if_Fun_Rel_rev_imp_bex)

corollary Fun_Rel_rev_imp_ex_iff_rel_surjective:
  "((R ⇛ (⟵)) ⇛ (⟵)) Ex Ex ⟷ rel_surjective R"
  using rel_surjective_if_Fun_Rel_rev_imp_ex Fun_Rel_rev_imp_ex_if_rel_surjective by blast

corollary bi_total_if_Fun_Rel_iff_ex:
  assumes "((R ⇛ (⟷)) ⇛ (⟷)) Ex Ex"
  shows "bi_total R"
  using assms by (urule bi_total_on_if_Fun_Rel_iff_bex)

corollary Fun_Rel_iff_ex_iff_bi_total:
  "((R ⇛ (⟷)) ⇛ (⟷)) Ex Ex ⟷ bi_total R"
  using bi_total_if_Fun_Rel_iff_ex Fun_Rel_iff_ex_if_bi_total by blast

end

end