Theory Transport_Functions_Mono_Conditions

✐‹creator "Kevin Kappelmann"›
subsection ‹Monotonicity Conditions›
theory Transport_Functions_Mono_Conditions
  imports
    Transport_Functions_Base
begin

paragraph ‹Summary›
text ‹In the dependent function relator case, we need to stipulate monotonicity conditions,
which we formalize here.›

context transport_Dep_Fun_Rel
begin

definition "mono_cond_left_rel ≡ ((x1 x2 ∷ (≥⇘L1⇙)) ⇒ ⦇x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3⦈ ⇛ (≤)) L2"

lemma mono_cond_left_relI [intro]:
  assumes "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ ⦇x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3⦈ ⇛ (≤)) L2"
  shows mono_cond_left_rel
  using assms unfolding mono_cond_left_rel_def by auto

lemma mono_cond_left_relD [dest]:
  assumes mono_cond_left_rel
  shows "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ ⦇x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3⦈ ⇛ (≤)) L2"
  using assms unfolding mono_cond_left_rel_def by auto

end

context transport_Dep_Fun_Rel
begin

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

definition "mono_cond_right_rel ≡ flip.mono_cond_left_rel"

lemma mono_cond_right_relI [intro]:
  assumes "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ ⦇x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3'⦈ ⇛ (≤)) R2"
  shows mono_cond_right_rel
  using assms unfolding mono_cond_right_rel_def by (rule flip.mono_cond_left_relI)

lemma mono_cond_right_relD [dest]:
  assumes mono_cond_right_rel
  shows "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ ⦇x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3'⦈ ⇛ (≤)) R2"
  using assms unfolding mono_cond_right_rel_def by (rule flip.mono_cond_left_relD)

definition "mono_conds_rel ≡ mono_cond_left_rel ∧ mono_cond_right_rel"

lemma mono_conds_relI [intro]:
  assumes mono_cond_left_rel
  and mono_cond_right_rel
  shows mono_conds_rel
  using assms unfolding mono_conds_rel_def by auto

lemma mono_conds_relE [elim]:
  assumes mono_conds_rel
  obtains mono_cond_left_rel mono_cond_right_rel
  using assms unfolding mono_conds_rel_def by auto

definition "mono_cond_left_fun ≡ ((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
  in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"

lemma mono_cond_left_funI [intro]:
  assumes "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  shows mono_cond_left_fun
  using assms unfolding mono_cond_left_fun_def by auto

lemma mono_cond_left_funD [dest]:
  assumes mono_cond_left_fun
  shows "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  using assms unfolding mono_cond_left_fun_def by auto

definition "mono_cond_right_fun ≡ ((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
  in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"

lemma mono_cond_right_funI [intro]:
  assumes "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows mono_cond_right_fun
  using assms unfolding mono_cond_right_fun_def by simp

lemma mono_cond_right_funD [dest]:
  assumes mono_cond_right_fun
  shows "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  using assms unfolding mono_cond_right_fun_def by simp

definition "mono_conds_fun ≡ mono_cond_left_fun ∧ mono_cond_right_fun"

lemma mono_conds_funI [intro]:
  assumes mono_cond_left_fun
  and mono_cond_right_fun
  shows "mono_conds_fun"
  using assms unfolding mono_conds_fun_def by auto

lemma mono_conds_funE [elim]:
  assumes "mono_conds_fun"
  obtains mono_cond_left_fun mono_cond_right_fun
  using assms unfolding mono_conds_fun_def by auto

definition "mono_conds ≡ mono_conds_rel ∧ mono_conds_fun"

lemma mono_condsI [intro]:
  assumes mono_conds_rel
  and mono_conds_fun
  shows mono_conds
  using assms unfolding mono_conds_def by auto

lemma mono_condsE [elim]:
  assumes mono_conds
  obtains mono_conds_rel mono_conds_fun
  using assms unfolding mono_conds_def by auto

lemmas mono_cond_intros =
  mono_cond_left_relI mono_cond_right_relI mono_conds_relI
  mono_cond_left_funI mono_cond_right_funI mono_conds_funI
  mono_condsI

end
end