Theory Transport_Equality

✐‹creator "Kevin Kappelmann"›
✐‹creator "Nils Harmsen"›
section ‹White-Box Transport of (Restricted) Equality›
theory Transport_Equality
  imports
    Restricted_Equality
    Binary_Relations_Bi_Unique
begin

paragraph ‹Summary›
text ‹Theorems for white-box transports of (restricted) equalities.›

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

lemma Fun_Rel_imp_eq_restrict_if_right_unique_onI:
  assumes runique: "right_unique_on P R"
  and rel: "(R ⇛ (⟶)) P Q"
  shows "(R ⇛ R ⇛ (⟶)) (=⇘P⇙) (=⇘Q⇙)"
proof (intro Fun_Rel_relI impI)
  fix x x' y y'
  assume "R x y" "R x' y'" "x =⇘P⇙ x'"
  moreover with rel have "R x y'" "Q y'" by auto
  ultimately show "y =⇘Q⇙ y'" using runique by (auto dest: right_unique_onD)
qed

lemma Fun_Rel_rev_imp_eq_restrict_if_rel_injective_atI:
  assumes rinjective: "rel_injective_at Q R"
  and rel: "(R ⇛ (⟵)) P Q"
  shows "(R ⇛ R ⇛ (⟵)) (=⇘P⇙) (=⇘Q⇙)"
proof (intro Fun_Rel_relI rev_impI)
  fix x x' y y'
  assume "R x y" "R x' y'" "y =⇘Q⇙ y'"
  moreover with rel have "R x y'" "P x" by auto
  ultimately show "x =⇘P⇙ x'" using rinjective by (auto dest: rel_injective_atD)
qed

corollary Fun_Rel_iff_eq_restrict_if_bi_unique_onI:
  assumes bi_unique: "bi_unique_on P R"
  and "(R ⇛ (⟷)) P Q"
  shows "(R ⇛ R ⇛ (⟷)) (=⇘P⇙) (=⇘Q⇙)"
proof -
  from assms have "(R ⇛ (⟶)) P Q" "(R ⇛ (⟵)) P Q" "bi_unique_on Q R¯"
    using bi_unique_on_rel_inv_if_Fun_Rel_iff_if_bi_unique_on by auto
  with bi_unique Fun_Rel_imp_eq_restrict_if_right_unique_onI
    Fun_Rel_rev_imp_eq_restrict_if_rel_injective_atI
    have "(R ⇛ R ⇛ (⟶)) (=⇘P⇙) (=⇘Q⇙)" "(R ⇛ R ⇛ (⟵)) (=⇘P⇙) (=⇘Q⇙)" by auto
  then show ?thesis by blast
qed

lemma right_unique_on_if_Fun_Rel_imp_eq_restrict:
  assumes "(R ⇛ R ⇛ (⟶)) (=⇘P⇙) (=)"
  shows "right_unique_on P R"
  using assms by (intro right_unique_onI) auto

lemma Fun_Rel_imp_if_Fun_Rel_imp_eq_restrict:
  assumes "(R ⇛ R ⇛ (⟶)) (=⇘P⇙) ((S :: 'b ⇒ 'b ⇒ bool)↾⇘Q⇙)"
  shows "(R ⇛ (⟶)) P Q"
  using assms by (intro Fun_Rel_relI) blast

corollary Fun_Rel_imp_eq_restrict_iff_right_unique_on_and_Fun_Rel_imp:
  "(R ⇛ R ⇛ (⟶)) (=⇘P⇙) (=⇘Q⇙) ⟷ (right_unique_on P R ∧ (R ⇛ (⟶)) P Q)"
  using Fun_Rel_imp_eq_restrict_if_right_unique_onI
    right_unique_on_if_Fun_Rel_imp_eq_restrict Fun_Rel_imp_if_Fun_Rel_imp_eq_restrict
  by blast

lemma rel_injective_at_if_Fun_Rel_rev_imp_eq_restrict:
  assumes "(R ⇛ R ⇛ (⟵)) (=) (=⇘Q⇙)"
  shows "rel_injective_at Q R"
  using assms by (intro rel_injective_atI) auto

lemma Fun_Rel_rev_imp_if_Fun_Rel_rev_imp_eq_restrict:
  assumes "(R ⇛ R ⇛ (⟵)) ((S :: 'a ⇒ 'a ⇒ bool)↾⇘P⇙) (=⇘Q⇙)"
  shows "(R ⇛ (⟵)) P Q"
  using assms by (intro Fun_Rel_relI rev_impI) auto

corollary Fun_Rel_rev_imp_eq_restrict_iff_rel_injective_at_and_Fun_Rel_rev_imp:
  "(R ⇛ R ⇛ (⟵)) (=⇘P⇙) (=⇘Q⇙) ⟷ (rel_injective_at Q R ∧ (R ⇛ (⟵)) P Q)"
  using Fun_Rel_rev_imp_eq_restrict_if_rel_injective_atI
    rel_injective_at_if_Fun_Rel_rev_imp_eq_restrict Fun_Rel_rev_imp_if_Fun_Rel_rev_imp_eq_restrict
  by blast

lemma bi_unique_on_if_Fun_Rel_iff_eq_restrict:
  assumes "(R ⇛ R ⇛ (⟷)) (=⇘P⇙) (=⇘Q⇙)"
  shows "bi_unique_on P R"
  using assms by (intro bi_unique_onI) blast+

lemma Fun_Rel_iff_if_Fun_Rel_iff_eq_restrict:
  assumes "(R ⇛ R ⇛ (⟷)) (=⇘P⇙) (=⇘Q⇙)"
  shows "(R ⇛ (⟷)) P Q"
  using assms by (intro Fun_Rel_relI) blast

corollary Fun_Rel_iff_eq_restrict_iff_bi_unique_on_and_Fun_Rel_iff:
  "(R ⇛ R ⇛ (⟷)) (=⇘P⇙) (=⇘Q⇙) ⟷ (bi_unique_on P R ∧ (R ⇛ (⟷)) P Q)"
  using Fun_Rel_iff_eq_restrict_if_bi_unique_onI
    bi_unique_on_if_Fun_Rel_iff_eq_restrict Fun_Rel_iff_if_Fun_Rel_iff_eq_restrict
  by blast

end

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

corollary Fun_Rel_imp_eq_if_right_unique:
  assumes "right_unique R"
  shows "(R ⇛ R ⇛ (⟶)) (=) (=)"
  using assms by (urule Fun_Rel_imp_eq_restrict_if_right_unique_onI) auto

corollary Fun_Rel_rev_imp_eq_if_rel_injective:
  assumes "rel_injective R"
  shows "(R ⇛ R ⇛ (⟵)) (=) (=)"
  using assms by (urule Fun_Rel_rev_imp_eq_restrict_if_rel_injective_atI) auto

corollary Fun_Rel_iff_eq_if_bi_unique:
  assumes "bi_unique R"
  shows "(R ⇛ R ⇛ (⟷)) (=) (=)"
  using assms by (urule Fun_Rel_iff_eq_restrict_if_bi_unique_onI) auto

corollary right_unique_if_Fun_Rel_imp_eq:
  assumes "(R ⇛ R ⇛ (⟶)) (=) (=)"
  shows "right_unique R"
  using assms by (urule right_unique_on_if_Fun_Rel_imp_eq_restrict)

corollary Fun_Rel_imp_eq_iff_right_unique: "(R ⇛ R ⇛ (⟶)) (=) (=) ⟷ right_unique R"
  using right_unique_if_Fun_Rel_imp_eq Fun_Rel_imp_eq_if_right_unique by blast

corollary rel_injective_if_Fun_Rel_rev_imp_eq:
  assumes "(R ⇛ R ⇛ (⟵)) (=) (=)"
  shows "rel_injective R"
  using assms by (urule rel_injective_at_if_Fun_Rel_rev_imp_eq_restrict)

corollary Fun_Rel_rev_imp_eq_iff_rel_injective: "(R ⇛ R ⇛ (⟵)) (=) (=) ⟷ rel_injective R"
  using rel_injective_if_Fun_Rel_rev_imp_eq Fun_Rel_rev_imp_eq_if_rel_injective by blast

corollary bi_unique_if_Fun_Rel_iff_eq:
  assumes "(R ⇛ R ⇛ (⟷)) (=) (=)"
  shows "bi_unique R"
  using assms by (urule bi_unique_on_if_Fun_Rel_iff_eq_restrict)

corollary Fun_Rel_iff_eq_iff_bi_unique: "(R ⇛ R ⇛ (⟷)) (=) (=) ⟷ bi_unique R"
  using bi_unique_if_Fun_Rel_iff_eq Fun_Rel_iff_eq_if_bi_unique by blast

end

end