Theory Order_Isomorphisms

✐‹creator "Kevin Kappelmann"›
✐‹creator "Niklas Krofa"›
theory Order_Isomorphisms
  imports
    Transport_Bijections
begin

consts order_isomorphism_on :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ bool"

definition order_isomorphism_on_pred :: "('a ⇒ bool) ⇒ ('b ⇒ bool) ⇒
  ('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool" where
  "order_isomorphism_on_pred P Q L R l r ≡ bijection_on P Q l r ∧ (∀x y : P. L x y ⟷ R (l x) (l y))"
adhoc_overloading order_isomorphism_on ⇌ order_isomorphism_on_pred

context order_functors
begin

lemma order_isomorphism_onI [intro]:
  assumes bij: "bijection_on P Q l r"
  and monol: "((≤⇘L⇙)↑⇘P⇙ ⇒ (≤⇘R⇙)) l"
  and monor: "((≤⇘R⇙)↑⇘Q⇙ ⇒ (≤⇘L⇙)) r"
  shows "order_isomorphism_on P Q (≤⇘L⇙) (≤⇘R⇙) l r"
proof -
  have "x ≤⇘L⇙ x'" if "P x" "P x'" "l x ≤⇘R⇙ l x'" for x x'
  proof -
    have "η x ≤⇘L⇙ η x'" using that monor bij by fastforce
    then show ?thesis
      using ‹P x› ‹P x'› bij inverse_on_if_bijection_on_left_right by (force dest: inverse_onD)
  qed
  then have "x ≤⇘L⇙ x' ⟷ l x ≤⇘R⇙ l x'" if "P x" "P x'" for x x' using that monol by fast
  then show ?thesis unfolding order_isomorphism_on_pred_def using bij by auto
qed

lemma order_isomorphism_onE:
  assumes "order_isomorphism_on P Q (≤⇘L⇙) (≤⇘R⇙) l r"
  obtains "bijection_on P Q l r" "⋀x y. P x ⟹ P y ⟹ L x y ⟷ R (l x) (l y)"
  using assms unfolding order_isomorphism_on_pred_def by auto

context
  notes order_isomorphism_onE[elim!]
begin

lemma right_rel_right_if_right_rel_if_preds_if_order_isomorphism_on:
  assumes "order_isomorphism_on P Q (≤⇘L⇙) (≤⇘R⇙) l r"
  and "Q y" "Q y'"
  and "y ≤⇘R⇙ y'"
  shows "r y ≤⇘L⇙ r y'"
proof -
  from assms have "y = ε y" "y' = ε y'"
    using inverse_on_if_bijection_on_left_right inverse_on_if_bijection_on_right_left
    by (force dest!: inverse_onD)+
  with assms show ?thesis by force
qed

lemma order_isomorphism_on_right_left_if_order_isomorphism_on_left_right:
  assumes "order_isomorphism_on P Q (≤⇘L⇙) (≤⇘R⇙) l r"
  shows "order_isomorphism_on Q P (≤⇘R⇙) (≤⇘L⇙) r l"
  using assms bijection_on_right_left_if_bijection_on_left_right[of P Q l r]
    right_rel_right_if_right_rel_if_preds_if_order_isomorphism_on[OF assms]
  by (intro order_functors.order_isomorphism_onI mono_wrt_relI)
  (auto elim!: order_isomorphism_onE rel_restrict_leftE rel_restrict_rightE)

lemma mono_wrt_restrict_restrict_left_if_order_isomorphism_on:
  assumes "order_isomorphism_on P Q (≤⇘L⇙) (≤⇘R⇙) l r"
  shows "((≤⇘L⇙)↑⇘P⇙ ⇒ (≤⇘R⇙)↑⇘Q⇙) l"
  using assms unfolding order_isomorphism_on_pred_def by fastforce

end
end

context galois
begin

interpretation flip : galois R L r l .

lemma order_isomorphism_onE [elim]:
  assumes "order_isomorphism_on P Q (≤⇘L⇙) (≤⇘R⇙) l r"
  obtains "bijection_on P Q l r" "((≤⇘L⇙)↑⇘P⇙ ≡⇩G (≤⇘R⇙)↑⇘Q⇙) l r"
proof -
  note order_isomorphism_onE[elim]
  have "((≤⇘L⇙)↑⇘P⇙ ⇒ (≤⇘R⇙)↑⇘Q⇙) l"
    using assms by (intro mono_wrt_restrict_restrict_left_if_order_isomorphism_on)
  moreover have "((≤⇘R⇙)↑⇘Q⇙ ⇒ (≤⇘L⇙)↑⇘P⇙) r"
    using assms by (intro flip.mono_wrt_restrict_restrict_left_if_order_isomorphism_on
      order_isomorphism_on_right_left_if_order_isomorphism_on_left_right)
  moreover have "inverse_on (in_field (≤⇘L⇙)↑⇘P⇙) l r"
  proof -
    have "in_field (≤⇘L⇙)↑⇘P⇙ ≤ P" by auto
    with assms show ?thesis using antimono_inverse_on by blast
  qed
  moreover have "inverse_on (in_field (≤⇘R⇙)↑⇘Q⇙) r l"
  proof -
    have "in_field (≤⇘R⇙)↑⇘Q⇙ ≤ Q" by auto
    with assms show ?thesis using antimono_inverse_on by blast
  qed
  ultimately interpret transport_bijection "(≤⇘L⇙)↑⇘P⇙" "(≤⇘R⇙)↑⇘Q⇙" l r
    using assms unfolding order_isomorphism_on_pred_def by unfold_locales auto
  from assms galois_equivalence show ?thesis using that by blast
qed

lemma order_isomorphism_on_in_field_if_connected_on_if_asymmetric_if_galois_equivalence:
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "asymmetric (≤⇘L⇙)" "asymmetric (≤⇘R⇙)"
  and "connected_on (in_field (≤⇘L⇙)) (≤⇘L⇙)" "connected_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "order_isomorphism_on (in_field (≤⇘L⇙)) (in_field (≤⇘R⇙)) (≤⇘L⇙) (≤⇘R⇙) l r"
  using assms by (intro order_isomorphism_onI
    bijection_on_if_connected_on_if_asymmetric_if_galois_equivalence)
  blast+

end

context order_functors
begin

interpretation of : order_functors A B a b for A B a b .

lemma order_isomorphism_on_compI:
  assumes "order_isomorphism_on P Q L M l1 r1"
  and "order_isomorphism_on Q U M R l2 r2"
  shows "order_isomorphism_on P U L R (l2 ∘ l1) (r1 ∘ r2)"
proof (intro of.order_isomorphism_onI)
  from assms show "bijection_on P U (l2 ∘ l1) (r1 ∘ r2)"
    by (intro bijection_on_compI) (auto elim: of.order_isomorphism_onE)
  from assms show "((≤⇘L⇙)↑⇘P⇙ ⇒ (≤⇘R⇙)) (l2 ∘ l1)"
  proof -
    from assms have "((≤⇘L⇙)↑⇘P⇙ ⇒ M↑⇘Q⇙) l1" "(M↑⇘Q⇙ ⇒ (≤⇘R⇙)) l2"
      using of.mono_wrt_restrict_restrict_left_if_order_isomorphism_on by blast+
    then show ?thesis by (urule dep_mono_wrt_rel_compI')
  qed
  from assms show "((≤⇘R⇙)↑⇘U⇙ ⇒ (≤⇘L⇙)) (r1 ∘ r2)"
  proof -
    from assms have "order_isomorphism_on Q P M L r1 l1" "order_isomorphism_on U Q R M r2 l2"
      by (auto intro: of.order_isomorphism_on_right_left_if_order_isomorphism_on_left_right)
    then have "((≤⇘R⇙)↑⇘U⇙ ⇒ M↑⇘Q⇙) r2" "(M↑⇘Q⇙ ⇒ (≤⇘L⇙)) r1"
      using of.mono_wrt_restrict_restrict_left_if_order_isomorphism_on by blast+
    then show ?thesis by (urule dep_mono_wrt_rel_compI')
  qed
qed

lemma order_isomorphism_on_self_id: "order_isomorphism_on P P R R id id"
  by (intro of.order_isomorphism_onI bijection_on_self_id) fastforce+

end

consts order_isomorphic_on :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool"

definition order_isomorphic_on_pred ::
  "('a ⇒ bool) ⇒ ('b ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ bool" where
  "order_isomorphic_on_pred P Q L R ≡ ∃l r. order_isomorphism_on P Q L R l r"
adhoc_overloading order_isomorphic_on ⇌ order_isomorphic_on_pred

lemma order_isomorphic_onI [intro]:
  assumes "order_isomorphism_on P Q L R l r"
  shows "order_isomorphic_on P Q L R"
  using assms unfolding order_isomorphic_on_pred_def by blast

lemma order_isomorphic_onE [elim]:
  assumes "order_isomorphic_on P Q L R"
  obtains l r where "order_isomorphism_on P Q L R l r"
  using assms unfolding order_isomorphic_on_pred_def by blast

lemma order_isomorphic_on_if_order_isomorphic_on:
  assumes "order_isomorphic_on P Q L R"
  shows "order_isomorphic_on Q P R L"
  using assms order_functors.order_isomorphism_on_right_left_if_order_isomorphism_on_left_right
  by blast

lemma order_isomorphic_on_trans:
  assumes "order_isomorphic_on P Q L M"
  and "order_isomorphic_on Q U M R"
  shows "order_isomorphic_on P U L R"
  using assms by (elim order_isomorphic_onE) (blast intro: order_functors.order_isomorphism_on_compI)

lemma order_isomorphic_on_self: "order_isomorphic_on P P R R"
  using order_functors.order_isomorphism_on_self_id by blast

end