Theory Transport_Compositions_Agree_Base

✐‹creator "Kevin Kappelmann"›
section ‹Compositions With Agreeing Relations›
subsection ‹Basic Setup›
theory Transport_Compositions_Agree_Base
  imports
    Transport_Base
begin

locale transport_comp_agree =
  g1 : galois L1 R1 l1 r1 + g2 : galois L2 R2 l2 r2
  for L1 :: "'a ⇒ 'a ⇒ bool"
  and R1 :: "'b ⇒ 'b ⇒ bool"
  and l1 :: "'a ⇒ 'b"
  and r1 :: "'b ⇒ 'a"
  and L2 :: "'b ⇒ 'b ⇒ bool"
  and R2 :: "'c ⇒ 'c ⇒ bool"
  and l2 :: "'b ⇒ 'c"
  and r2 :: "'c ⇒ 'b"
begin

text ‹This locale collects results about the composition of transportable
components under the assumption that the relations @{term "R1"} and
@{term "L2"} agree (in one sense or another) whenever required. Such an
agreement may not necessarily hold in practice, and the resulting theorems are
not particularly pretty. However, in the special case where @{term "R1 = L2"},
most side-conditions disappear and the results are very simple.›

notation L1 (infix "≤⇘L1⇙" 50)
notation R1 (infix "≤⇘R1⇙" 50)
notation L2 (infix "≤⇘L2⇙" 50)
notation R2 (infix "≤⇘R2⇙" 50)

notation g1.ge_left (infix "≥⇘L1⇙" 50)
notation g1.ge_right (infix "≥⇘R1⇙" 50)
notation g2.ge_left (infix "≥⇘L2⇙" 50)
notation g2.ge_right (infix "≥⇘R2⇙" 50)

notation g1.left_Galois (infix "⇘L1⇙⪅" 50)
notation g1.right_Galois (infix "⇘R1⇙⪅" 50)
notation g2.left_Galois (infix "⇘L2⇙⪅" 50)
notation g2.right_Galois (infix "⇘R2⇙⪅" 50)

notation g1.ge_Galois_left (infix "⪆⇘L1⇙" 50)
notation g1.ge_Galois_right (infix "⪆⇘R1⇙" 50)
notation g2.ge_Galois_left (infix "⪆⇘L2⇙" 50)
notation g2.ge_Galois_right (infix "⪆⇘R2⇙" 50)

notation g1.right_ge_Galois (infix "⇘R1⇙⪆" 50)
notation g1.Galois_right (infix "⪅⇘R1⇙" 50)
notation g2.right_ge_Galois (infix "⇘R2⇙⪆" 50)
notation g2.Galois_right (infix "⪅⇘R2⇙" 50)

notation g1.left_ge_Galois (infix "⇘L1⇙⪆" 50)
notation g1.Galois_left (infix "⪅⇘L1⇙" 50)
notation g2.left_ge_Galois (infix "⇘L2⇙⪆" 50)
notation g2.Galois_left (infix "⪅⇘L2⇙" 50)

notation g1.unit ("η⇩1")
notation g1.counit ("ε⇩1")
notation g2.unit ("η⇩2")
notation g2.counit ("ε⇩2")

abbreviation (input) "L ≡ L1"

definition "l ≡ l2 ∘ l1"

lemma left_eq_comp: "l = l2 ∘ l1"
  unfolding l_def ..

lemma left_eq [simp]: "l x = l2 (l1 x)"
  unfolding left_eq_comp by simp

context
begin

interpretation flip : transport_comp_agree R2 L2 r2 l2 R1 L1 r1 l1 .

abbreviation (input) "R ≡ flip.L"
abbreviation "r ≡ flip.l"

lemma right_eq_comp: "r = r1 ∘ r2"
  unfolding flip.l_def ..

lemma right_eq [simp]: "r z = r1 (r2 z)"
  unfolding right_eq_comp by simp

lemmas transport_defs = left_eq_comp right_eq_comp

end

sublocale transport L R l r .

(*FIXME: somehow the notation for the fixed parameters L and R, defined in
Order_Functions_Base.thy, is lost. We hence re-declare it here.*)
notation L (infix "≤⇘L⇙" 50)
notation R (infix "≤⇘R⇙" 50)

end

locale transport_comp_same =
  transport_comp_agree L1 R1 l1 r1 R1 R2 l2 r2
  for L1 :: "'a ⇒ 'a ⇒ bool"
  and R1 :: "'b ⇒ 'b ⇒ bool"
  and l1 :: "'a ⇒ 'b"
  and r1 :: "'b ⇒ 'a"
  and R2 :: "'c ⇒ 'c ⇒ bool"
  and l2 :: "'b ⇒ 'c"
  and r2 :: "'c ⇒ 'b"
begin

text ‹This locale is a special case of @{locale "transport_comp_agree"} where
the left and right components both use @{term "(≤⇘R1⇙)"} as their right and left
relation, respectively. This is the special case that is most prominent in the
literature. The resulting theorems are quite simple, but often not applicable
in practice.›

end


end