Theory Transport_Universal_Quantifier

✐‹creator "Kevin Kappelmann"›
✐‹creator "Nils Harmsen"›
section ‹White-Box Transport of (Bounded) Universal Quantifier›
theory Transport_Universal_Quantifier
  imports
    Bounded_Quantifiers
    Binary_Relations_Bi_Total
    Reverse_Implies
begin

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

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

lemma Fun_Rel_restricts_imp_ball_if_rel_surjective_atI:
  assumes "rel_surjective_at Q R↾⇘P⇙"
  shows "((R↾⇘P⇙↿⇘Q⇙ ⇛ (⟶)) ⇛ (⟶)) ∀⇘P⇙ ∀⇘Q⇙"
  using assms by (intro Fun_Rel_relI) blast

lemma Fun_Rel_restricts_rev_imp_ball_if_left_total_onI:
  assumes "left_total_on P R↿⇘Q⇙"
  shows "((R↾⇘P⇙↿⇘Q⇙ ⇛ (⟵)) ⇛ (⟵)) ∀⇘P⇙ ∀⇘Q⇙"
  using assms by (intro Fun_Rel_relI) blast

lemma Fun_Rel_restricts_iff_ball_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) blast

corollary Fun_Rel_restricts_iff_ball_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_ball_if_left_total_on_if_rel_surjective_at)
  force+

lemma rel_surjective_at_restrict_left_if_Fun_Rel_imp_ball:
  assumes "((R ⇛ (⟶)) ⇛ (⟶)) ∀⇘P⇙ ∀⇘Q⇙"
  shows "rel_surjective_at Q R↾⇘P⇙"
proof -
  let ?P2 = "in_codom R↾⇘P⇙"
  have "(R ⇛ (⟶)) P ?P2" by blast
  with assms have "(∀x : P. P x) ⟶ (∀y : Q. ?P2 y)" by blast
  then show "rel_surjective_at Q R↾⇘P⇙" by fast
qed

lemma Fun_Rel_Fun_Rel_if_le_left_if_Fun_Rel_Fun_Rel:
  assumes "(((O :: 'a ⇒ 'b ⇒ bool) ⇛ S) ⇛ T) U V"
  and "O ≤ O'"
  shows "((O' ⇛ S) ⇛ T) U V"
proof -
  from assms have "(O' ⇛ S) ≤ (O ⇛ S)" by blast
  with assms antimonoD[OF antimono_Dep_Fun_Rel_rel_left] show ?thesis
    unfolding Fun_Rel_rel_iff_Dep_Fun_Rel_rel by blast
qed

corollary Fun_Rel_imp_ball_iff_rel_surjective_at_restrict_left:
  "((R ⇛ (⟶)) ⇛ (⟶)) ∀⇘P⇙ ∀⇘Q⇙ ⟷ rel_surjective_at Q R↾⇘P⇙"
  by (blast intro: Fun_Rel_restricts_imp_ball_if_rel_surjective_atI
    Fun_Rel_Fun_Rel_if_le_left_if_Fun_Rel_Fun_Rel
    rel_surjective_at_restrict_left_if_Fun_Rel_imp_ball)

lemma left_total_on_restrict_right_if_Fun_Rel_rev_imp_ball:
  assumes "((R ⇛ (⟵)) ⇛ (⟵)) ∀⇘P⇙ ∀⇘Q⇙"
  shows "left_total_on P R↿⇘Q⇙"
proof -
  let ?P1 = "in_dom R↿⇘Q⇙"
  have "(R ⇛ (⟵)) ?P1 Q" by blast
  with assms have "(∀x : P. ?P1 x) ⟵ (∀y : Q. Q y)" by blast
  then show "left_total_on P R↿⇘Q⇙" by fast
qed

corollary Fun_Rel_rev_imp_ball_iff_left_total_on_restrict_right:
  "((R ⇛ (⟵)) ⇛ (⟵)) ∀⇘P⇙ ∀⇘Q⇙ ⟷ left_total_on P R↿⇘Q⇙"
  by (blast intro: Fun_Rel_restricts_rev_imp_ball_if_left_total_onI
    Fun_Rel_Fun_Rel_if_le_left_if_Fun_Rel_Fun_Rel
    left_total_on_restrict_right_if_Fun_Rel_rev_imp_ball)

lemma bi_total_on_if_Fun_Rel_iff_ball:
  assumes "((R ⇛ (⟷)) ⇛ (⟷)) ∀⇘P⇙ ∀⇘Q⇙"
  shows "bi_total_on P Q R"
proof (rule bi_total_onI)
  let ?P1 = "in_dom R" and ?P2 = "λ_. True"
  have "(R ⇛ (⟷)) ?P1 ?P2" by blast
  with assms have "(∀x : P. ?P1 x) ⟷ (∀y : Q. ?P2 y)" by blast
  then show "left_total_on P R" by fast
next
  let ?P1 = "λ_. True" and ?P2 = "in_codom R"
  have "(R ⇛ (⟷)) ?P1 ?P2" by blast
  with assms have "(∀x : P. ?P1 x) ⟷ (∀y : Q. ?P2 y)" by blast
  then show "rel_surjective_at Q R" by fast
qed

corollary Fun_Rel_iff_ball_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_ball_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_ball)

end

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

corollary Fun_Rel_imp_all_if_rel_surjective:
  assumes "rel_surjective R"
  shows "((R ⇛ (⟶)) ⇛ (⟶)) All All"
  using assms by (urule Fun_Rel_restricts_imp_ball_if_rel_surjective_atI)

corollary Fun_Rel_rev_imp_all_if_left_total:
  assumes "left_total R"
  shows "((R ⇛ (⟵)) ⇛ (⟵)) All All"
  using assms by (urule Fun_Rel_restricts_rev_imp_ball_if_left_total_onI)

corollary Fun_Rel_iff_all_if_bi_total:
  assumes "bi_total R"
  shows "((R ⇛ (⟷)) ⇛ (⟷)) All All"
  using assms by (urule Fun_Rel_restricts_iff_ball_if_bi_total_on)

corollary rel_surjective_if_Fun_Rel_imp_all:
  assumes "((R ⇛ (⟶)) ⇛ (⟶)) All All"
  shows "rel_surjective R"
  using assms by (urule rel_surjective_at_restrict_left_if_Fun_Rel_imp_ball)

corollary Fun_Rel_imp_all_iff_rel_surjective:
  "((R ⇛ (⟶)) ⇛ (⟶)) All All ⟷ rel_surjective R"
  using rel_surjective_if_Fun_Rel_imp_all Fun_Rel_imp_all_if_rel_surjective by blast

corollary left_total_if_Fun_Rel_rev_imp_all:
  assumes "((R ⇛ (⟵)) ⇛ (⟵)) All All"
  shows "left_total R"
  using assms by (urule left_total_on_restrict_right_if_Fun_Rel_rev_imp_ball)

corollary Fun_Rel_rev_imp_all_iff_left_total:
  "((R ⇛ (⟵)) ⇛ (⟵)) All All ⟷ left_total R"
  using left_total_if_Fun_Rel_rev_imp_all Fun_Rel_rev_imp_all_if_left_total by blast

corollary bi_total_if_Fun_Rel_iff_all:
  assumes "((R ⇛ (⟷)) ⇛ (⟷)) All All"
  shows "bi_total R"
  using assms by (urule bi_total_on_if_Fun_Rel_iff_ball)

corollary Fun_Rel_iff_all_iff_bi_total:
  "((R ⇛ (⟷)) ⇛ (⟷)) All All ⟷ bi_total R"
  using bi_total_if_Fun_Rel_iff_all Fun_Rel_iff_all_if_bi_total by blast

end


end