Theory Transport_Rel_If

✐‹creator "Kevin Kappelmann"›
section ‹Transport using Conditional Relation›
theory Transport_Rel_If
  imports
    Transport_Base
begin

paragraph ‹Summary›
text ‹Setup for Transport using conditional relations.›

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

lemma reflexive_on_rel_if_if_reflexive_onI [intro]:
  assumes "B ⟹ reflexive_on P R"
  shows "reflexive_on P (B ⟶⇩r R)"
  using assms by (intro reflexive_onI) blast

lemma transitive_on_rel_if_if_transitive_onI [intro]:
  assumes "B ⟹ transitive_on P R"
  shows "transitive_on P (B ⟶⇩r R)"
  using assms by (intro transitive_onI) (blast dest: transitive_onD)

lemma preorder_on_rel_if_if_preorder_onI [intro]:
  assumes "B ⟹ preorder_on P R"
  shows "preorder_on P (B ⟶⇩r R)"
  using assms by (intro preorder_onI) auto

lemma symmetric_on_rel_if_if_symmetric_onI [intro]:
  assumes "B ⟹ symmetric_on P R"
  shows "symmetric_on P (B ⟶⇩r R)"
  using assms by (intro symmetric_onI) (blast dest: symmetric_onD)

lemma partial_equivalence_rel_on_rel_if_if_partial_equivalence_rel_onI [intro]:
  assumes "B ⟹ partial_equivalence_rel_on P R"
  shows "partial_equivalence_rel_on P (B ⟶⇩r R)"
  using assms by (intro partial_equivalence_rel_onI)
  auto

lemma dep_mono_wrt_rel_if_rel_if_if_imp_if_dep_mono_wrt_rel:
  assumes "B ⟹ B' ⟹ ((x y ∷ R) ⇒ S x y) f"
  and "B' ⟹ B"
  shows "((x y ∷ B ⟶⇩r R) ⇒ (B' ⟶⇩r S x y)) f"
  using assms by fastforce

end


locale transport_rel_if =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"
  and l :: "'a ⇒ 'b"
  and r :: "'b ⇒ 'a"
  and B B' :: bool
begin

sublocale t : transport L R l r .
sublocale transport "B ⟶⇩r (≤⇘L⇙)" "B' ⟶⇩r (≤⇘R⇙)" l r .

lemma half_galois_prop_left_if_imp_if_half_galois_prop_left:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "B' ⟹ B"
  shows "((B ⟶⇩r (≤⇘L⇙)) ⇩h⊴ (B' ⟶⇩r (≤⇘R⇙))) l r"
  using assms by (intro half_galois_prop_leftI rel_if_if_impI) fast

lemma half_galois_prop_right_if_imp_if_half_galois_prop_right:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "B ⟹ B'"
  shows "((B ⟶⇩r (≤⇘L⇙)) ⊴⇩h (B' ⟶⇩r (≤⇘R⇙))) l r"
  using assms by (intro half_galois_prop_rightI) fast

lemma galois_prop_if_iff_if_galois_prop:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((B ⟶⇩r (≤⇘L⇙)) ⊴ (B' ⟶⇩r (≤⇘R⇙))) l r"
  using assms by (intro galois_propI
    half_galois_prop_left_if_imp_if_half_galois_prop_left
    half_galois_prop_right_if_imp_if_half_galois_prop_right)
  auto

lemma galois_connection_if_iff_if_galois_connection:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((B ⟶⇩r (≤⇘L⇙)) ⊣ (B' ⟶⇩r (≤⇘R⇙))) l r"
  by (urule (rr) galois_connectionI galois_prop_if_iff_if_galois_prop
    dep_mono_wrt_rel_if_rel_if_if_imp_if_dep_mono_wrt_rel)
  (use assms in auto)

lemma galois_equivalence_if_iff_if_galois_equivalence:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((B ⟶⇩r (≤⇘L⇙)) ≡⇩G (B' ⟶⇩r (≤⇘R⇙))) l r"
  using assms by (intro galois_equivalenceI
    galois_connection_if_iff_if_galois_connection
    transport_rel_if.galois_prop_if_iff_if_galois_prop)
  (auto elim: galois.galois_connectionE)

lemma preorder_equivalence_if_iff_if_preorder_equivalence:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((B ⟶⇩r (≤⇘L⇙)) ≡⇘pre⇙ (B' ⟶⇩r (≤⇘R⇙))) l r"
  using assms by (intro preorder_equivalence_if_galois_equivalenceI
    galois_equivalence_if_iff_if_galois_equivalence
    preorder_on_rel_if_if_preorder_onI)
  blast+

lemma partial_equivalence_rel_equivalence_if_iff_if_partial_equivalence_rel_equivalence:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((B ⟶⇩r (≤⇘L⇙)) ≡⇘PER⇙ (B' ⟶⇩r (≤⇘R⇙))) l r"
  using assms by (intro
    partial_equivalence_rel_equivalence_if_galois_equivalenceI
    galois_equivalence_if_iff_if_galois_equivalence)
  fastforce+

end

end