Theory Transport_Functions_Base

✐‹creator "Kevin Kappelmann"›
section ‹Transport For Functions›
subsection ‹Basic Setup›
theory Transport_Functions_Base
  imports
    HOL_Syntax_Bundles_Base
    Monotone_Function_Relator
    Transport_Base
begin

unbundle no HOL_ascii_syntax

paragraph ‹Summary›
text ‹Basic setup for closure proofs. We introduce locales for the syntax,
the dependent relator, the non-dependent relator, the monotone dependent relator,
and the monotone non-dependent relator.›


definition "flip2 f x1 x2 x3 x4 ≡ f x2 x1 x4 x3"

lemma flip2_eq: "flip2 f x1 x2 x3 x4 = f x2 x1 x4 x3"
  unfolding flip2_def by simp

lemma flip2_eq_rel_inv [simp]: "flip2 R x y = (R y x)¯"
  by (intro ext) (simp only: flip2_eq rel_inv_iff_rel)

lemma flip2_flip2_eq_self [simp]: "flip2 (flip2 f) = f"
  by (intro ext) (simp add: flip2_eq)

lemma flip2_eq_flip2_iff_eq [iff]: "flip2 f = flip2 g ⟷ f = g"
  unfolding flip2_def by (intro iffI ext) (auto dest: fun_cong)


paragraph ‹Dependent Function Relator›

locale transport_Dep_Fun_Rel_syntax =
  t1 : transport L1 R1 l1 r1 +
  dfro1 : hom_Dep_Fun_Rel_orders L1 L2 +
  dfro2 : hom_Dep_Fun_Rel_orders R1 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 :: "'a2 ⇒ 'a1 ⇒ 'b1 ⇒ 'b2"
  and r2 :: "'a1 ⇒ 'a2 ⇒ 'b2 ⇒ 'b1"
begin

notation L1 (infix ‹≤⇘L1⇙› 50)
notation R1 (infix ‹≤⇘R1⇙› 50)

notation t1.ge_left (infix ‹≥⇘L1⇙› 50)
notation t1.ge_right (infix ‹≥⇘R1⇙› 50)

notation t1.left_Galois (infix ‹⇘L1⇙⪅› 50)
notation t1.ge_Galois_left (infix ‹⪆⇘L1⇙› 50)
notation t1.right_Galois (infix ‹⇘R1⇙⪅› 50)
notation t1.ge_Galois_right (infix ‹⪆⇘R1⇙› 50)
notation t1.right_ge_Galois (infix ‹⇘R1⇙⪆› 50)
notation t1.Galois_right (infix ‹⪅⇘R1⇙› 50)
notation t1.left_ge_Galois (infix ‹⇘L1⇙⪆› 50)
notation t1.Galois_left (infix ‹⪅⇘L1⇙› 50)

notation t1.unit (‹η⇩1›)
notation t1.counit (‹ε⇩1›)

notation (input) L2 (‹('(≤(⇘L2 _ _⇙)'))›)
notation (output) L2 (‹('(≤(⇘L2 ('(_')) ('(_'))⇙)'))›)
term "L2 x y"
term "((x x' ∷ N) ⇛ ((M x x')↾⇘P⇙))"

notation (input) R2 (‹('(≤(⇘R2 (_) (_)⇙)'))›)
notation (output) R2 (‹('(≤(⇘R2 ('(_')) ('(_'))⇙)'))›)

notation (input) dfro1.right_infix (‹(_ ≤(⇘L2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) dfro1.right_infix (‹(_ ≤(⇘L2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)
notation (input) dfro2.right_infix (‹(_ ≤(⇘R2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) dfro2.right_infix (‹(_ ≤(⇘R2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)

notation (input) dfro1.o.ge_right (‹('(≥(⇘L2 (_) (_)⇙)'))›)
notation (output) dfro1.o.ge_right (‹('(≥(⇘L2 ('(_')) ('(_'))⇙)'))›)
notation (input) dfro2.o.ge_right (‹('(≥(⇘R2 (_) (_)⇙)'))›)
notation (output) dfro2.o.ge_right (‹('(≥(⇘R2 ('(_')) ('(_'))⇙)'))›)

notation (input) dfro1.ge_right_infix (‹(_ ≥(⇘L2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) dfro1.ge_right_infix (‹(_ ≥(⇘L2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)
notation (input) dfro2.ge_right_infix (‹(_ ≥(⇘R2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) dfro2.ge_right_infix (‹(_ ≥(⇘R2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)

notation (input) l2 (‹l2⇘(_) (_)⇙›)
notation (output) l2 (‹l2⇘('(_')) ('(_'))⇙›)
notation (input) r2 (‹r2⇘(_) (_)⇙›)
notation (output) r2 (‹r2⇘('(_')) ('(_'))⇙›)

sublocale t2 : transport "(≤⇘L2 x (r1 x')⇙)" "(≤⇘R2 (l1 x) x'⇙)" "l2⇘x' x⇙" "r2⇘x x'⇙" for x x' .

notation (input) t2.left_Galois (‹('((⇘L2 (_) (_)⇙)⪅'))›)
notation (output) t2.left_Galois (‹('((⇘L2 ('(_')) ('(_'))⇙)⪅'))›)
notation (input) t2.right_Galois (‹('((⇘R2 (_) (_)⇙)⪅'))›)
notation (output) t2.right_Galois (‹('((⇘R2 ('(_')) ('(_'))⇙)⪅'))›)

abbreviation "left2_Galois_infix y x x' y' ≡ (⇘L2 x x'⇙⪅) y y'"
notation (input) left2_Galois_infix (‹(_ (⇘L2 (_) (_)⇙)⪅ _)› [51,0,0,51] 50)
notation (output) left2_Galois_infix (‹(_ (⇘L2 ('(_')) ('(_'))⇙)⪅ _)› [51,0,0,51] 50)
abbreviation "right2_Galois_infix y' x x' y ≡ (⇘R2 x x'⇙⪅) y' y"
notation (input) right2_Galois_infix (‹(_ (⇘R2 (_) (_)⇙)⪅ _)› [51,0,0,51] 50)
notation (output) right2_Galois_infix (‹(_ (⇘R2 ('(_')) ('(_'))⇙)⪅ _)› [51,0,0,51] 50)

notation (input) t2.ge_Galois_left (‹('(⪆(⇘L2 (_) (_)⇙)'))›)
notation (output) t2.ge_Galois_left (‹('(⪆(⇘L2 ('(_')) ('(_'))⇙)'))›)
notation (input) t2.ge_Galois_right (‹('(⪆(⇘R2 (_) (_)⇙)'))›)
notation (output) t2.ge_Galois_right (‹('(⪆(⇘R2 ('(_')) ('(_'))⇙)'))›)

abbreviation (input) "ge_Galois_left_left2_infix y' x x' y ≡ (⪆⇘L2 x x'⇙) y' y"
notation (input) ge_Galois_left_left2_infix (‹(_ ⪆(⇘L2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) ge_Galois_left_left2_infix (‹(_ ⪆(⇘L2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)
abbreviation (input) "ge_Galois_left_right2_infix y x x' y' ≡ (⪆⇘R2 x x'⇙) y y'"
notation (input) ge_Galois_left_right2_infix (‹(_ ⪆(⇘R2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) ge_Galois_left_right2_infix (‹(_ ⪆(⇘R2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)

notation (input) t2.right_ge_Galois (‹('((⇘R2 (_) (_)⇙)⪆'))›)
notation (output) t2.right_ge_Galois (‹('((⇘R2 ('(_')) ('(_'))⇙)⪆'))›)
notation (input) t2.left_ge_Galois (‹('((⇘L2 (_) (_)⇙)⪆'))›)
notation (output) t2.left_ge_Galois (‹('((⇘L2 ('(_')) ('(_'))⇙)⪆'))›)

abbreviation "left2_ge_Galois_left_infix y x x' y' ≡ (⇘L2 x x'⇙⪆) y y'"
notation (input) left2_ge_Galois_left_infix (‹(_ (⇘L2 (_) (_)⇙)⪆ _)› [51,0,0,51] 50)
notation (output) left2_ge_Galois_left_infix (‹(_ (⇘L2 ('(_')) ('(_'))⇙)⪆ _)› [51,0,0,51] 50)
abbreviation "right2_ge_Galois_left_infix y' x x' y ≡ (⇘R2 x x'⇙⪆) y' y"
notation (input) right2_ge_Galois_left_infix (‹(_ (⇘R2 (_) (_)⇙)⪆ _)› [51,0,0,51] 50)
notation (output) right2_ge_Galois_left_infix (‹(_ (⇘R2 ('(_')) ('(_'))⇙)⪆ _)› [51,0,0,51] 50)

notation (input) t2.Galois_right (‹('(⪅(⇘R2 (_) (_)⇙)'))›)
notation (output) t2.Galois_right (‹('(⪅(⇘R2 ('(_')) ('(_'))⇙)'))›)
notation (input) t2.Galois_left (‹('(⪅(⇘L2 (_) (_)⇙)'))›)
notation (output) t2.Galois_left (‹('(⪅(⇘L2 ('(_')) ('(_'))⇙)'))›)

abbreviation (input) "Galois_left2_infix y' x x' y ≡ (⪅⇘L2 x x'⇙) y' y"
notation (input) Galois_left2_infix (‹(_ ⪅(⇘L2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) Galois_left2_infix (‹(_ ⪅(⇘L2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)
abbreviation (input) "Galois_right2_infix y x x' y' ≡ (⪅⇘R2 x x'⇙) y y'"
notation (input) Galois_right2_infix (‹(_ ⪅(⇘R2 (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) Galois_right2_infix (‹(_ ⪅(⇘R2 ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)

abbreviation "t2_unit x x' ≡ t2.unit x' x"
notation (input) t2_unit (‹η⇘2 (_) (_)⇙›)
notation (output) t2_unit (‹η⇘2 ('(_')) ('(_'))⇙›)
abbreviation "t2_counit x x' ≡ t2.counit x' x"
notation (input) t2_counit (‹ε⇘2 (_) (_)⇙›)
notation (output) t2_counit (‹ε⇘2 ('(_')) ('(_'))⇙›)

end

locale transport_Dep_Fun_Rel =
  transport_Dep_Fun_Rel_syntax 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 :: "'a2 ⇒ 'a1 ⇒ 'b1 ⇒ 'b2"
  and r2 :: "'a1 ⇒ 'a2 ⇒ 'b2 ⇒ 'b1"
begin

definition "L ≡ (x1 x2 ∷ (≤⇘L1⇙)) ⇛ (≤⇘L2 x1 x2⇙)"

lemma left_rel_eq_Dep_Fun_Rel: "L = ((x1 x2 ∷ (≤⇘L1⇙)) ⇛ (≤⇘L2 x1 x2⇙))"
  unfolding L_def ..

definition "l ≡ ((x' : r1) ↝ l2 x')"

lemma left_eq_dep_fun_map: "l = ((x' : r1) ↝ l2 x')"
  unfolding l_def ..

lemma left_eq [simp]: "l f x' = l2⇘x' (r1 x')⇙ (f (r1 x'))"
  unfolding left_eq_dep_fun_map by simp

context
begin

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

abbreviation "R ≡ flip.L"
abbreviation "r ≡ flip.l"

lemma right_rel_eq_Dep_Fun_Rel: "R = ((x1' x2' ∷ (≤⇘R1⇙)) ⇛ (≤⇘R2 x1' x2'⇙))"
  unfolding flip.L_def ..

lemma right_eq_dep_fun_map: "r = ((x : l1) ↝ r2 x)"
  unfolding flip.l_def ..

end

lemma right_eq [simp]: "r g x = r2⇘x (l1 x)⇙ (g (l1 x))"
  unfolding right_eq_dep_fun_map by simp

lemmas transport_defs = left_rel_eq_Dep_Fun_Rel left_eq_dep_fun_map
  right_rel_eq_Dep_Fun_Rel right_eq_dep_fun_map

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)

lemma left_relI [intro]:
  assumes "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ f x1 ≤⇘L2 x1 x2⇙ f' x2"
  shows "f ≤⇘L⇙ f'"
  unfolding left_rel_eq_Dep_Fun_Rel using assms by blast

lemma left_relE [elim]:
  assumes "f ≤⇘L⇙ f'"
  and "x1 ≤⇘L1⇙ x2"
  obtains "f x1 ≤⇘L2 x1 x2⇙ f' x2"
  using assms unfolding left_rel_eq_Dep_Fun_Rel by blast

interpretation flip_inv :
  transport_Dep_Fun_Rel "(≥⇘R1⇙)" "(≥⇘L1⇙)" r1 l1 "flip2 R2" "flip2 L2" r2 l2 .

lemma flip_inv_right_eq_ge_left: "flip_inv.R = (≥⇘L⇙)"
  unfolding left_rel_eq_Dep_Fun_Rel flip_inv.right_rel_eq_Dep_Fun_Rel
  by (simp only: flip: Dep_Fun_Rel_rel_inv_rel_inv_eq flip2_eq_rel_inv[of "L2"])

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

lemma flip_inv_left_eq_ge_right: "flip_inv.L ≡ (≥⇘R⇙)"
  unfolding flip.flip_inv_right_eq_ge_left .


subparagraph ‹Useful Rewritings for Dependent Relation›

lemma left_rel2_unit_eqs_left_rel2I:
  assumes "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 (η⇩1 x) x⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "x ≤⇘L1⇙ x"
  and "x ≡⇘L1⇙ η⇩1 x"
  shows "(≤⇘L2 (η⇩1 x) x⇙) = (≤⇘L2 x x⇙)"
  and "(≤⇘L2 x (η⇩1 x)⇙) = (≤⇘L2 x x⇙)"
  using assms by (auto intro!: antisym)

lemma left2_eq_if_bi_related_if_monoI:
  assumes mono_L2: "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ ⦇x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3⦈ ⇛ (≤)) L2"
  and "x1 ≤⇘L1⇙ x2"
  and "x1 ≡⇘L1⇙ x3"
  and "x2 ≡⇘L1⇙ x4"
  and trans_L1: "transitive (≤⇘L1⇙)"
  shows "(≤⇘L2 x1 x2⇙) = (≤⇘L2 x3 x4⇙)"
proof (intro antisym)
  from ‹x1 ≡⇘L1⇙ x3› ‹x2 ≡⇘L1⇙ x4› have "x3 ≤⇘L1⇙ x1" "x2 ≤⇘L1⇙ x4" by auto
  with ‹x1 ≤⇘L1⇙ x2› mono_L2 show "(≤⇘L2 x1 x2⇙) ≤ (≤⇘L2 x3 x4⇙)" by blast
  from ‹x1 ≡⇘L1⇙ x3› ‹x2 ≡⇘L1⇙ x4› have "x1 ≤⇘L1⇙ x3" "x4 ≤⇘L1⇙ x2" by auto
  moreover from ‹x3 ≤⇘L1⇙ x1› ‹x1 ≤⇘L1⇙ x2› ‹x2 ≤⇘L1⇙ x4› have "x3 ≤⇘L1⇙ x4"
    using trans_L1 by blast
  ultimately show "(≤⇘L2 x3 x4⇙) ≤ (≤⇘L2 x1 x2⇙)" using mono_L2 by blast
qed

end

paragraph ‹Function Relator›

locale transport_Fun_Rel_syntax =
  tdfrs : transport_Dep_Fun_Rel_syntax 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 :: "'b1 ⇒ 'b1 ⇒ bool"
  and R2 :: "'b2 ⇒ 'b2 ⇒ bool"
  and l2 :: "'b1 ⇒ 'b2"
  and r2 :: "'b2 ⇒ 'b1"
begin

notation L1 (infix ‹≤⇘L1⇙› 50)
notation R1 (infix ‹≤⇘R1⇙› 50)

notation tdfrs.t1.ge_left (infix ‹≥⇘L1⇙› 50)
notation tdfrs.t1.ge_right (infix ‹≥⇘R1⇙› 50)

notation tdfrs.t1.left_Galois (infix ‹⇘L1⇙⪅› 50)
notation tdfrs.t1.ge_Galois_left (infix ‹⪆⇘L1⇙› 50)
notation tdfrs.t1.right_Galois (infix ‹⇘R1⇙⪅› 50)
notation tdfrs.t1.ge_Galois_right (infix ‹⪆⇘R1⇙› 50)
notation tdfrs.t1.right_ge_Galois (infix ‹⇘R1⇙⪆› 50)
notation tdfrs.t1.Galois_right (infix ‹⪅⇘R1⇙› 50)
notation tdfrs.t1.left_ge_Galois (infix ‹⇘L1⇙⪆› 50)
notation tdfrs.t1.Galois_left (infix ‹⪅⇘L1⇙› 50)

notation tdfrs.t1.unit (‹η⇩1›)
notation tdfrs.t1.counit (‹ε⇩1›)

notation L2 (infix ‹≤⇘L2⇙› 50)
notation R2 (infix ‹≤⇘R2⇙› 50)

notation tdfrs.t2.ge_left (infix ‹≥⇘L2⇙› 50)
notation tdfrs.t2.ge_right (infix ‹≥⇘R2⇙› 50)

notation tdfrs.t2.left_Galois (infix ‹⇘L2⇙⪅› 50)
notation tdfrs.t2.ge_Galois_left (infix ‹⪆⇘L2⇙› 50)
notation tdfrs.t2.right_Galois (infix ‹⇘R2⇙⪅› 50)
notation tdfrs.t2.ge_Galois_right (infix ‹⪆⇘R2⇙› 50)
notation tdfrs.t2.right_ge_Galois (infix ‹⇘R2⇙⪆› 50)
notation tdfrs.t2.Galois_right (infix ‹⪅⇘R2⇙› 50)
notation tdfrs.t2.left_ge_Galois (infix ‹⇘L2⇙⪆› 50)
notation tdfrs.t2.Galois_left (infix ‹⪅⇘L2⇙› 50)

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

end

locale transport_Fun_Rel =
  transport_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 :: "'b1 ⇒ 'b1 ⇒ bool"
  and R2 :: "'b2 ⇒ 'b2 ⇒ bool"
  and l2 :: "'b1 ⇒ 'b2"
  and r2 :: "'b2 ⇒ 'b1"
begin

(*FIXME: we have to repeat the Galois syntax here since tdfr already contains
a Galois instance, blocking a galois sublocale interpretation here*)
notation tdfr.L (‹L›)
notation tdfr.R (‹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.left_Galois (infix ‹⇘L⇙⪅› 50)
notation tdfr.ge_Galois_left (infix ‹⪆⇘L⇙› 50)
notation tdfr.right_Galois (infix ‹⇘R⇙⪅› 50)
notation tdfr.ge_Galois_right (infix ‹⪆⇘R⇙› 50)
notation tdfr.right_ge_Galois (infix ‹⇘R⇙⪆› 50)
notation tdfr.Galois_right (infix ‹⪅⇘R⇙› 50)
notation tdfr.left_ge_Galois (infix ‹⇘L⇙⪆› 50)
notation tdfr.Galois_left (infix ‹⪅⇘L⇙› 50)

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

lemma left_rel_eq_Fun_Rel: "(≤⇘L⇙) = ((≤⇘L1⇙) ⇛ (≤⇘L2⇙))"
  by (urule tdfr.left_rel_eq_Dep_Fun_Rel)

lemma left_eq_fun_map: "l = (r1 ↝ l2)"
  by (intro ext) simp

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

lemma right_rel_eq_Fun_Rel: "(≤⇘R⇙) = ((≤⇘R1⇙) ⇛ (≤⇘R2⇙))"
  unfolding flip.left_rel_eq_Fun_Rel ..

lemma right_eq_fun_map: "r = (l1 ↝ r2)"
  unfolding flip.left_eq_fun_map ..

lemmas transport_defs = left_rel_eq_Fun_Rel right_rel_eq_Fun_Rel
  left_eq_fun_map right_eq_fun_map

end


paragraph ‹Monotone Dependent Function Relator›

locale transport_Mono_Dep_Fun_Rel =
  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 :: "'a2 ⇒ 'a1 ⇒ 'b1 ⇒ 'b2"
  and r2 :: "'a1 ⇒ 'a2 ⇒ 'b2 ⇒ 'b1"
begin

definition "L ≡ tdfr.L⇧⊕"

lemma left_rel_eq_tdfr_left_Refl_Rel: "L = tdfr.L⇧⊕"
  unfolding L_def ..

lemma left_rel_eq_Mono_Dep_Fun_Rel: "L = ((x1 x2 ∷ (≤⇘L1⇙)) ⇛⊕ (≤⇘L2 x1 x2⇙))"
  unfolding left_rel_eq_tdfr_left_Refl_Rel tdfr.left_rel_eq_Dep_Fun_Rel by simp

lemma left_rel_eq_tdfr_left_rel_if_reflexive_on:
  assumes "reflexive_on (in_field tdfr.L) tdfr.L"
  shows "L = tdfr.L"
  unfolding left_rel_eq_tdfr_left_Refl_Rel using assms
  by (rule Refl_Rel_eq_self_if_reflexive_on)

abbreviation "l ≡ tdfr.l"

lemma left_eq_tdfr_left: "l = tdfr.l" ..

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

abbreviation "R ≡ flip.L"

lemma right_rel_eq_tdfr_right_Refl_Rel: "R = tdfr.R⇧⊕"
  unfolding flip.left_rel_eq_tdfr_left_Refl_Rel ..

lemma right_rel_eq_Mono_Dep_Fun_Rel: "R = ((y1 y2 ∷ (≤⇘R1⇙)) ⇛⊕ (≤⇘R2 y1 y2⇙))"
  unfolding flip.left_rel_eq_Mono_Dep_Fun_Rel ..

lemma right_rel_eq_tdfr_right_rel_if_reflexive_on:
  assumes "reflexive_on (in_field tdfr.R) tdfr.R"
  shows "R = tdfr.R"
  using assms by (rule flip.left_rel_eq_tdfr_left_rel_if_reflexive_on)

abbreviation "r ≡ tdfr.r"

lemma right_eq_tdfr_right: "r = tdfr.r" ..

lemmas transport_defs = left_rel_eq_tdfr_left_Refl_Rel
  right_rel_eq_tdfr_right_Refl_Rel

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


paragraph ‹Monotone Function Relator›

locale transport_Mono_Fun_Rel =
  transport_Fun_Rel_syntax L1 R1 l1 r1 L2 R2 l2 r2 +
  tfr : transport_Fun_Rel L1 R1 l1 r1 L2 R2 l2 r2 +
  tmdfr : transport_Mono_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 :: "'b1 ⇒ 'b1 ⇒ bool"
  and R2 :: "'b2 ⇒ 'b2 ⇒ bool"
  and l2 :: "'b1 ⇒ 'b2"
  and r2 :: "'b2 ⇒ 'b1"
begin

(*FIXME: we have to repeat the Galois syntax here since tdfr already contains
a Galois instance, blocking a galois sublocale interpretation here*)
notation tmdfr.L (‹L›)
notation tmdfr.R (‹R›)

abbreviation "l ≡ tmdfr.l"
abbreviation "r ≡ tmdfr.r"

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

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

notation tmdfr.left_Galois (infix ‹⇘L⇙⪅› 50)
notation tmdfr.ge_Galois_left (infix ‹⪆⇘L⇙› 50)
notation tmdfr.right_Galois (infix ‹⇘R⇙⪅› 50)
notation tmdfr.ge_Galois_right (infix ‹⪆⇘R⇙› 50)
notation tmdfr.right_ge_Galois (infix ‹⇘R⇙⪆› 50)
notation tmdfr.Galois_right (infix ‹⪅⇘R⇙› 50)
notation tmdfr.left_ge_Galois (infix ‹⇘L⇙⪆› 50)
notation tmdfr.Galois_left (infix ‹⪅⇘L⇙› 50)

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

lemma left_rel_eq_Mono_Fun_Rel: "(≤⇘L⇙) = ((≤⇘L1⇙) ⇛⊕ (≤⇘L2⇙))"
  unfolding tmdfr.left_rel_eq_Mono_Dep_Fun_Rel by simp

lemma left_eq_fun_map: "l = (r1 ↝ l2)"
  unfolding tfr.left_eq_fun_map ..

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

lemma right_rel_eq_Mono_Fun_Rel: "(≤⇘R⇙) = ((≤⇘R1⇙) ⇛⊕ (≤⇘R2⇙))"
  unfolding flip.left_rel_eq_Mono_Fun_Rel ..

lemma right_eq_fun_map: "r = (l1 ↝ r2)"
  unfolding flip.left_eq_fun_map ..

lemmas transport_defs = tmdfr.transport_defs

end


end