Theory Transport_Rel_If

✐‹creator "Kevin Kappelmann"›
section ‹Transport for Dependent Function Relator with Non-Dependent Functions›
theory Transport_Rel_If
  imports
    Transport_Black_Box
begin

paragraph ‹Summary›
text ‹We introduce a special case of @{locale transport_Dep_Fun_Rel}.
The derived theorem is easier to apply and supported by the current prototype.›

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 (rel_if B 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 (rel_if B 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 (rel_if B 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 (rel_if B 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 (rel_if B R)"
  using assms by (intro partial_equivalence_rel_onI)
  auto

lemma rel_if_dep_mono_wrt_rel_if_iff_if_dep_mono_wrt_relI:
  assumes "B ⟹ B' ⟹ ((x y ∷ R) ⇒ S x y) f"
  and "B ⟷ B'"
  shows "((x y ∷ rel_if B R) ⇒ (rel_if B' (S x y))) f"
  using assms by (intro dep_mono_wrt_relI) auto

corollary reflexive_rel_if_if_reflexiveI [intro]:
  assumes "B ⟹ reflexive R"
  shows "reflexive (rel_if B R)"
  using assms unfolding reflexive_eq_reflexive_on by blast

corollary transitive_rel_if_if_transitiveI [intro]:
  assumes "B ⟹ transitive R"
  shows "transitive (rel_if B R)"
  using assms unfolding transitive_eq_transitive_on
  by (intro transitive_onI) (force dest: transitive_onD)

end

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

corollary preorder_rel_if_if_preorderI [intro]:
  assumes "B ⟹ preorder R"
  shows "preorder (rel_if B R)"
  using assms unfolding preorder_eq_preorder_on by blast

corollary symmetric_rel_if_if_symmetricI [intro]:
  assumes "B ⟹ symmetric R"
  shows "symmetric (rel_if B R)"
  using assms unfolding symmetric_eq_symmetric_on by blast

corollary partial_equivalence_rel_rel_if_if_partial_equivalence_relI [intro]:
  assumes "B ⟹ partial_equivalence_rel R"
  shows "partial_equivalence_rel (rel_if B R)"
  using assms unfolding partial_equivalence_rel_eq_partial_equivalence_rel_on
  by blast

end

context galois_prop
begin

interpretation rel_if : galois_prop "rel_if B (≤⇘L⇙)" "rel_if B' (≤⇘R⇙)" l r .
interpretation flip_inv : galois_prop "(≥⇘R⇙)" "(≥⇘L⇙)" r l .

lemma rel_if_half_galois_prop_left_if_iff_if_half_galois_prop_leftI:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((rel_if B (≤⇘L⇙)) ⇩h⊴ (rel_if B' (≤⇘R⇙))) l r"
  using assms by (intro rel_if.half_galois_prop_leftI) auto

lemma rel_if_half_galois_prop_right_if_iff_if_half_galois_prop_rightI:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((rel_if B (≤⇘L⇙)) ⊴⇩h (rel_if B' (≤⇘R⇙))) l r"
  using assms by (intro rel_if.half_galois_prop_rightI) fastforce

lemma rel_if_galois_prop_if_iff_if_galois_propI:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((rel_if B (≤⇘L⇙)) ⊴ (rel_if B' (≤⇘R⇙))) l r"
  using assms by (intro rel_if.galois_propI
    rel_if_half_galois_prop_left_if_iff_if_half_galois_prop_leftI
    rel_if_half_galois_prop_right_if_iff_if_half_galois_prop_rightI)
  auto

end

context galois
begin

interpretation rel_if : galois "rel_if B (≤⇘L⇙)" "rel_if B' (≤⇘R⇙)" l r .

lemma rel_if_galois_connection_if_iff_if_galois_connectionI:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((rel_if B (≤⇘L⇙)) ⊣ (rel_if B' (≤⇘R⇙))) l r"
  using assms by (intro rel_if.galois_connectionI
    rel_if_dep_mono_wrt_rel_if_iff_if_dep_mono_wrt_relI
    rel_if_galois_prop_if_iff_if_galois_propI)
  auto

lemma rel_if_galois_equivalence_if_iff_if_galois_equivalenceI:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((rel_if B (≤⇘L⇙)) ≡⇩G (rel_if B' (≤⇘R⇙))) l r"
  using assms by (intro rel_if.galois_equivalenceI
    rel_if_galois_connection_if_iff_if_galois_connectionI
    galois_prop.rel_if_galois_prop_if_iff_if_galois_propI)
  (auto elim: galois.galois_connectionE)

end

context transport
begin

interpretation rel_if : transport "rel_if B (≤⇘L⇙)" "rel_if B' (≤⇘R⇙)" l r .

lemma rel_if_preorder_equivalence_if_iff_if_preorder_equivalenceI:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((rel_if B (≤⇘L⇙)) ≡⇘pre⇙ (rel_if B' (≤⇘R⇙))) l r"
  using assms by (intro rel_if.preorder_equivalence_if_galois_equivalenceI
    rel_if_galois_equivalence_if_iff_if_galois_equivalenceI
    preorder_on_rel_if_if_preorder_onI)
  blast+

lemma rel_if_partial_equivalence_rel_equivalence_if_iff_if_partial_equivalence_rel_equivalenceI:
  assumes "B ⟹ B' ⟹ ((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  and "B ⟷ B'"
  shows "((rel_if B (≤⇘L⇙)) ≡⇘PER⇙ (rel_if B' (≤⇘R⇙))) l r"
  using assms by (intro
    rel_if.partial_equivalence_rel_equivalence_if_galois_equivalenceI
    rel_if_galois_equivalence_if_iff_if_galois_equivalenceI)
  blast+

end

locale transport_Dep_Fun_Rel_no_dep_fun =
  transport_Dep_Fun_Rel_syntax L1 R1 l1 r1 L2 R2 "λ_ _. l2" "λ_ _. r2" +
  tdfr : transport_Dep_Fun_Rel L1 R1 l1 r1 L2 R2 "λ_ _. l2" "λ_ _. r2"
  for L1 :: "'a1 ⇒ 'a1 ⇒ bool"
  and R1 :: "'a2 ⇒ 'a2 ⇒ bool"
  and l1 :: "'a1 ⇒ 'a2"
  and r1 :: "'a2 ⇒ 'a1"
  and L2 :: "'a1 ⇒ 'a1 ⇒ 'b1 ⇒ 'b1 ⇒ bool"
  and R2 :: "'a2 ⇒ 'a2 ⇒ 'b2 ⇒ 'b2 ⇒ bool"
  and l2 :: "'b1 ⇒ 'b2"
  and r2 :: "'b2 ⇒ 'b1"
begin

notation t2.unit (‹η⇩2›)
notation t2.counit (‹ε⇩2›)

abbreviation "L ≡ tdfr.L"
abbreviation "R ≡ tdfr.R"

abbreviation "l ≡ tdfr.l"
abbreviation "r ≡ tdfr.r"

notation tdfr.L (infix ‹≤⇘L⇙› 50)
notation tdfr.R (infix ‹≤⇘R⇙› 50)

notation tdfr.ge_left (infix ‹≥⇘L⇙› 50)
notation tdfr.ge_right (infix ‹≥⇘R⇙› 50)

notation tdfr.unit (‹η›)
notation tdfr.counit (‹ε›)

theorem partial_equivalence_rel_equivalenceI:
  assumes per_equiv1: "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and per_equiv2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) l2 r2"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
proof -
  have per2I: "((≤⇘L2 x1 (r1 x2')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x1) x2'⇙)) l2 r2"
    if hyps: "x1 ≤⇘L1⇙ x2" "x2 ⇘L1⇙⪅ x1'" "x1' ≤⇘R1⇙ x2'" for x1 x2 x1' x2'
  proof -
    from hyps have "x1 ⇘L1⇙⪅ x2'"
      using per_equiv1 t1.left_Galois_if_left_Galois_if_left_relI
        t1.left_Galois_if_right_rel_if_left_GaloisI
      by fast
    with per_equiv2 show ?thesis by blast
  qed
  have "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) (λ_ _. l2)"
    by (intro dep_mono_wrt_relI Dep_Fun_Rel_relI Dep_Fun_Rel_predI rel_if_if_impI)
    (auto 10 0 dest!: per2I)
  moreover have
    "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) (λ_ _. r2)"
    by (intro dep_mono_wrt_relI Dep_Fun_Rel_relI Dep_Fun_Rel_predI rel_if_if_impI)
    (auto 10 0 dest!: per2I)
  ultimately show ?thesis
    using assms by (intro tdfr.partial_equivalence_rel_equivalenceI) auto
qed

end


end