Theory Transport_Galois_Relator_Properties

✐‹creator "Kevin Kappelmann"›
✐‹creator "Nils Harmsen"›
section ‹Properties of Galois Relator for White-Box Transport Side Conditions›
theory Transport_Galois_Relator_Properties
  imports
    Binary_Relations_Bi_Total
    Binary_Relations_Bi_Unique
    Galois_Connections
    Galois_Relator
begin

paragraph ‹Summary›
text ‹Properties of Galois relator arising as side conditions for white-box transport.›

context galois
begin

paragraph ‹Right-Uniqueness›

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

lemma right_unique_at_left_Galois_if_right_unique_at_rightI:
  assumes "right_unique_at Q (≤⇘R⇙)"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  shows "right_unique_at Q (⇘L⇙⪅)"
  using assms by (auto dest: right_unique_atD)

lemma right_unique_at_right_if_right_unique_at_left_GaloisI:
  assumes "right_unique_at Q (⇘L⇙⪅)"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "right_unique_at Q (≤⇘R⇙)"
  using assms by (blast dest: right_unique_atD)

corollary right_unique_at_left_Galois_iff_right_unique_at_rightI:
  assumes "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "right_unique_at Q (⇘L⇙⪅) ⟷ right_unique_at Q (≤⇘R⇙)"
  using assms right_unique_at_left_Galois_if_right_unique_at_rightI
    right_unique_at_right_if_right_unique_at_left_GaloisI
  by blast

corollary right_unique_on_left_Galois_if_right_unique_at_rightI:
  assumes "right_unique_at Q (≤⇘R⇙)"
  and "((⇘L⇙⪅) ⇛ (⟶)) P Q"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  shows "right_unique_on P (⇘L⇙⪅)"
  using assms by (intro right_unique_on_if_Fun_Rel_imp_if_right_unique_at)
  (blast intro: right_unique_at_left_Galois_if_right_unique_at_rightI)

corollary right_unique_at_right_if_right_unique_on_left_GaloisI:
  assumes "right_unique_on P (⇘L⇙⪅)"
  and "((⇘L⇙⪅) ⇛ (⟵)) P Q"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "right_unique_at Q (≤⇘R⇙)"
  using assms by (intro right_unique_at_right_if_right_unique_at_left_GaloisI
    right_unique_at_if_Fun_Rel_rev_imp_if_right_unique_on)

corollary right_unique_on_left_Galois_iff_right_unique_at_rightI:
  assumes "((⇘L⇙⪅) ⇛ (⟷)) P Q"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "right_unique_on P (⇘L⇙⪅) ⟷ right_unique_at Q (≤⇘R⇙)"
  using assms right_unique_on_left_Galois_if_right_unique_at_rightI
    right_unique_at_right_if_right_unique_on_left_GaloisI
  by blast

end

corollary right_unique_left_Galois_if_right_unique_rightI:
  assumes "right_unique (≤⇘R⇙)"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  shows "right_unique (⇘L⇙⪅)"
  using assms by (urule right_unique_at_left_Galois_if_right_unique_at_rightI)

corollary right_unique_right_if_right_unique_left_GaloisI:
  assumes "right_unique (⇘L⇙⪅)"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "right_unique (≤⇘R⇙)"
  using assms by (urule right_unique_at_right_if_right_unique_at_left_GaloisI)

corollary right_unique_left_Galois_iff_right_unique_rightI:
  assumes "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "right_unique (⇘L⇙⪅) ⟷ right_unique (≤⇘R⇙)"
  using assms right_unique_left_Galois_if_right_unique_rightI
    right_unique_right_if_right_unique_left_GaloisI
  by blast


paragraph ‹Injectivity›

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

lemma injective_on_left_Galois_if_rel_injective_on_left:
  assumes "rel_injective_on P (≤⇘L⇙)"
  shows "rel_injective_on P (⇘L⇙⪅)"
  using assms by (auto dest: rel_injective_onD)

lemma rel_injective_on_left_if_injective_on_left_GaloisI:
  assumes "rel_injective_on P (⇘L⇙⪅)"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "rel_injective_on P (≤⇘L⇙)"
  using assms by (intro rel_injective_onI) (blast dest!: rel_injective_onD)

corollary injective_on_left_Galois_iff_rel_injective_on_leftI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "rel_injective_on P (⇘L⇙⪅) ⟷ rel_injective_on P (≤⇘L⇙)"
  using assms injective_on_left_Galois_if_rel_injective_on_left
    rel_injective_on_left_if_injective_on_left_GaloisI
  by blast

corollary injective_at_left_Galois_if_rel_injective_on_leftI:
  assumes "rel_injective_on P (≤⇘L⇙)"
  and "((⇘L⇙⪅) ⇛ (⟵)) P Q"
  shows "rel_injective_at Q (⇘L⇙⪅)"
  using assms by (intro rel_injective_at_if_Fun_Rel_rev_imp_if_rel_injective_on)
  (blast intro: injective_on_left_Galois_if_rel_injective_on_left)

corollary rel_injective_on_left_if_injective_at_left_GaloisI:
  assumes "rel_injective_at Q (⇘L⇙⪅)"
  and "((⇘L⇙⪅) ⇛ (⟶)) P Q"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "rel_injective_on P (≤⇘L⇙)"
  using assms by (intro rel_injective_on_left_if_injective_on_left_GaloisI
    rel_injective_on_if_Fun_Rel_imp_if_rel_injective_at)

corollary injective_at_left_Galois_iff_rel_injective_on_leftI:
  assumes "((⇘L⇙⪅) ⇛ (⟷)) P Q"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "rel_injective_at Q (⇘L⇙⪅) ⟷ rel_injective_on P (≤⇘L⇙)"
  using assms injective_at_left_Galois_if_rel_injective_on_leftI
    rel_injective_on_left_if_injective_at_left_GaloisI
  by blast

end

corollary injective_left_Galois_if_rel_injective_left:
  assumes "rel_injective (≤⇘L⇙)"
  shows "rel_injective (⇘L⇙⪅)"
  using assms by (urule injective_on_left_Galois_if_rel_injective_on_left)

corollary rel_injective_left_if_injective_left_GaloisI:
  assumes "rel_injective (⇘L⇙⪅)"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows  "rel_injective (≤⇘L⇙)"
  using assms by (urule rel_injective_on_left_if_injective_on_left_GaloisI)

corollary rel_injective_left_Galois_iff_rel_injective_leftI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "rel_injective (⇘L⇙⪅) ⟷ rel_injective (≤⇘L⇙)"
  using assms injective_left_Galois_if_rel_injective_left
    rel_injective_left_if_injective_left_GaloisI
  by blast


paragraph ‹Bi-Uniqueness›

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

corollary bi_unique_on_left_Galois_if_right_unique_at_right_if_rel_injective_on_leftI:
  assumes "rel_injective_on P (≤⇘L⇙)"
  and "right_unique_at Q (≤⇘R⇙)"
  and "((⇘L⇙⪅) ⇛ (⟶)) P Q"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  shows "bi_unique_on P (⇘L⇙⪅)"
  using assms
  by (intro bi_unique_onI right_unique_on_left_Galois_if_right_unique_at_rightI
    injective_on_left_Galois_if_rel_injective_on_left)

corollary rel_injective_on_left_and_right_unique_at_right_if_bi_unique_on_left_GaloisI:
  assumes "bi_unique_on P (⇘L⇙⪅)"
  and "((⇘L⇙⪅) ⇛ (⟵)) P Q"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "rel_injective_on P (≤⇘L⇙) ∧ right_unique_at Q (≤⇘R⇙)"
  using assms by (intro conjI rel_injective_on_left_if_injective_on_left_GaloisI
    right_unique_at_right_if_right_unique_on_left_GaloisI)
  auto

corollary bi_unique_on_left_Galois_iff_rel_injective_on_left_and_right_unique_at_rightI:
  assumes "((⇘L⇙⪅) ⇛ (⟷)) P Q"
  and "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  shows "bi_unique_on P (⇘L⇙⪅) ⟷ rel_injective_on P (≤⇘L⇙) ∧ right_unique_at Q (≤⇘R⇙)"
  using assms bi_unique_on_left_Galois_if_right_unique_at_right_if_rel_injective_on_leftI
    rel_injective_on_left_and_right_unique_at_right_if_bi_unique_on_left_GaloisI
  by blast

end

corollary bi_unique_left_Galois_if_right_unique_right_if_rel_injective_leftI:
  assumes "rel_injective (≤⇘L⇙)"
  and "right_unique (≤⇘R⇙)"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  shows "bi_unique (⇘L⇙⪅)"
  by (urule (rr) bi_unique_on_left_Galois_if_right_unique_at_right_if_rel_injective_on_leftI assms)
  auto

corollary rel_injective_left_and_right_unique_right_if_bi_unique_left_GaloisI:
  assumes "bi_unique (⇘L⇙⪅)"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "rel_injective (≤⇘L⇙) ∧ right_unique (≤⇘R⇙)"
  by (urule (rr) rel_injective_on_left_and_right_unique_at_right_if_bi_unique_on_left_GaloisI assms)
  auto

corollary bi_unique_left_Galois_iff_rel_injective_left_and_right_unique_rightI:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  shows "bi_unique (⇘L⇙⪅) ⟷ rel_injective (≤⇘L⇙) ∧ right_unique (≤⇘R⇙)"
  using assms bi_unique_left_Galois_if_right_unique_right_if_rel_injective_leftI
    rel_injective_left_and_right_unique_right_if_bi_unique_left_GaloisI
  by blast


paragraph ‹Surjectivity›

context
  fixes Q :: "'b ⇒ bool"
begin

lemma surjective_at_left_Galois_if_rel_surjective_at_rightI:
  assumes "rel_surjective_at Q (≤⇘R⇙)"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "rel_surjective_at Q (⇘L⇙⪅)"
  using assms by (intro rel_surjective_atI) fast

lemma rel_surjective_at_right_if_surjective_at_left_Galois:
  assumes "rel_surjective_at Q (⇘L⇙⪅)"
  shows "rel_surjective_at Q (≤⇘R⇙)"
  using assms by (intro rel_surjective_atI) (auto)

corollary rel_surjective_at_right_iff_surjective_at_left_GaloisI:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "rel_surjective_at Q (⇘L⇙⪅) ⟷ rel_surjective_at Q (≤⇘R⇙)"
  using assms surjective_at_left_Galois_if_rel_surjective_at_rightI
    rel_surjective_at_right_if_surjective_at_left_Galois
  by blast

end

corollary surjective_left_Galois_if_rel_surjective_rightI:
  assumes "rel_surjective (≤⇘R⇙)"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "rel_surjective (⇘L⇙⪅)"
  using assms by (urule surjective_at_left_Galois_if_rel_surjective_at_rightI)

corollary rel_surjective_right_if_surjective_left_Galois:
  assumes "rel_surjective (⇘L⇙⪅)"
  shows "rel_surjective (≤⇘R⇙)"
  using assms by (urule rel_surjective_at_right_if_surjective_at_left_Galois)

corollary rel_surjective_right_iff_surjective_left_GaloisI:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  shows "rel_surjective (⇘L⇙⪅) ⟷ rel_surjective (≤⇘R⇙)"
  using assms surjective_left_Galois_if_rel_surjective_rightI
    rel_surjective_right_if_surjective_left_Galois
  by blast


paragraph ‹Left-Totality›

context
  fixes P :: "'a ⇒ bool"
begin

lemma left_total_on_left_Galois_if_left_total_on_leftI:
  assumes "left_total_on P (≤⇘L⇙)"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "left_total_on P (⇘L⇙⪅)"
  using assms by (intro left_total_onI) force

lemma left_total_on_left_if_left_total_on_left_GaloisI:
  assumes "left_total_on P (⇘L⇙⪅)"
  shows "left_total_on P (≤⇘L⇙)"
  using assms by (intro left_total_onI) auto

corollary left_total_on_left_Galois_iff_left_total_on_leftI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "left_total_on P (⇘L⇙⪅) ⟷ left_total_on P (≤⇘L⇙)"
  using assms left_total_on_left_Galois_if_left_total_on_leftI
    left_total_on_left_if_left_total_on_left_GaloisI
  by blast

end

corollary left_total_left_Galois_if_left_total_leftI:
  assumes "left_total (≤⇘L⇙)"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "left_total (⇘L⇙⪅)"
  using assms by (urule left_total_on_left_Galois_if_left_total_on_leftI)

corollary left_total_left_if_left_total_left_Galois:
  assumes "left_total (⇘L⇙⪅)"
  shows "left_total (≤⇘L⇙)"
  using assms by (urule left_total_on_left_if_left_total_on_left_GaloisI)

corollary left_total_left_Galois_iff_left_total_leftI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "left_total (⇘L⇙⪅) ⟷ left_total (≤⇘L⇙)"
  using assms left_total_left_Galois_if_left_total_leftI
    left_total_left_if_left_total_left_Galois
  by blast


paragraph ‹Bi-Totality›

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

lemma bi_total_on_left_GaloisI:
  assumes "left_total_on P (≤⇘L⇙)"
  and "rel_surjective_at Q (≤⇘R⇙)"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "bi_total_on P Q (⇘L⇙⪅)"
  using assms surjective_at_left_Galois_if_rel_surjective_at_rightI
    left_total_on_left_Galois_if_left_total_on_leftI
  by blast

lemma left_total_on_left_rel_surjective_at_right_if_bi_total_on_left_GaloisE:
  assumes "bi_total_on P Q (⇘L⇙⪅)"
  obtains "left_total_on P (≤⇘L⇙)" "rel_surjective_at Q (≤⇘R⇙)"
  using assms rel_surjective_at_right_if_surjective_at_left_Galois
    left_total_on_left_if_left_total_on_left_GaloisI
  by auto

corollary bi_total_on_left_Galois_iff_left_total_on_left_and_rel_surjective_on_rightI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "bi_total_on P Q (⇘L⇙⪅) ⟷ left_total_on P (≤⇘L⇙) ∧ rel_surjective_at Q (≤⇘R⇙)"
  using assms bi_total_on_left_GaloisI
    left_total_on_left_rel_surjective_at_right_if_bi_total_on_left_GaloisE
  by blast

end

corollary bi_total_left_GaloisI:
  assumes "left_total (≤⇘L⇙)"
  and "rel_surjective (≤⇘R⇙)"
  and "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "bi_total (⇘L⇙⪅)"
  using assms by (urule bi_total_on_left_GaloisI)

corollary left_total_left_rel_surjective_right_if_bi_total_left_GaloisE:
  assumes "bi_total (⇘L⇙⪅)"
  obtains "left_total (≤⇘L⇙)" "rel_surjective (≤⇘R⇙)"
  using assms by (urule (e) left_total_on_left_rel_surjective_at_right_if_bi_total_on_left_GaloisE)

corollary bi_total_left_Galois_iff_left_total_left_and_rel_surjective_rightI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "bi_total (⇘L⇙⪅) ⟷ left_total (≤⇘L⇙) ∧ rel_surjective (≤⇘R⇙)"
  using assms bi_total_left_GaloisI
    left_total_left_rel_surjective_right_if_bi_total_left_GaloisE
  by blast


paragraph ‹Function Relator›

lemma Fun_Rel_left_Galois_left_Galois_imp_left_rightI:
  assumes monol: "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and half_gal: "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and perR: "partial_equivalence_rel (≤⇘R⇙)"
  shows "((⇘L⇙⪅) ⇛ (⇘L⇙⪅) ⇛ (⟶)) (≤⇘L⇙) (≤⇘R⇙)"
proof (intro Fun_Rel_relI impI)
  fix x y x' y'
  assume "x ⇘L⇙⪅ y" "x' ⇘L⇙⪅ y'" "x ≤⇘L⇙ x'"
  with half_gal have "l x' ≤⇘R⇙ y'" by auto
  with ‹x ≤⇘L⇙ x'› monol perR have "l x ≤⇘R⇙ y'" by blast
  with ‹x ⇘L⇙⪅ y› half_gal perR have "y ≤⇘R⇙ l x" by (blast dest: symmetricD)
  with perR ‹l x ≤⇘R⇙ y'› show "y ≤⇘R⇙ y'" by blast
qed

lemma Fun_Rel_left_Galois_left_Galois_rev_imp_left_rightI:
  assumes monor: "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and perL: "partial_equivalence_rel (≤⇘L⇙)"
  shows "((⇘L⇙⪅) ⇛ (⇘L⇙⪅) ⇛ (⟵)) (≤⇘L⇙) (≤⇘R⇙)"
proof (intro Fun_Rel_relI rev_impI)
  fix x y x' y'
  assume "x ⇘L⇙⪅ y" and "x' ⇘L⇙⪅ y'" and "y ≤⇘R⇙ y'"
  with monor perL have "x ≤⇘L⇙ r y'" by fastforce
  with  ‹x' ⇘L⇙⪅ y'› have "x' ≤⇘L⇙ r y'" by auto
  with perL ‹x ≤⇘L⇙ r y'› show "x ≤⇘L⇙ x'" by (blast dest: symmetricD)
qed

corollary Fun_Rel_left_Galois_left_Galois_iff_left_rightI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "partial_equivalence_rel (≤⇘L⇙)"
  and "partial_equivalence_rel (≤⇘R⇙)"
  shows "((⇘L⇙⪅) ⇛ (⇘L⇙⪅) ⇛ (⟷)) (≤⇘L⇙) (≤⇘R⇙)"
  using assms Fun_Rel_left_Galois_left_Galois_imp_left_rightI
    Fun_Rel_left_Galois_left_Galois_rev_imp_left_rightI
  by (intro Fun_Rel_relI) blast

end


end