Theory Strict_Linear_Orders

✐‹creator "Kevin Kappelmann"›
✐‹creator "Niklas Krofta"›
subsection ‹Strict Linear Orders›
theory Strict_Linear_Orders
  imports
    Binary_Relations_Connected
    Strict_Partial_Orders
begin

definition "strict_linear_order_on ≡ strict_partial_order_on ⊓ connected_on"

lemma strict_linear_order_onI [intro]:
  assumes "strict_partial_order_on P R" "connected_on P R"
  shows "strict_linear_order_on P R"
  using assms unfolding strict_linear_order_on_def by auto

lemma strict_linear_order_onE [elim]:
  assumes "strict_linear_order_on P R"
  obtains "strict_partial_order_on P R" "connected_on P R"
  using assms unfolding strict_linear_order_on_def by auto

lemma antimono_strict_linear_order_on:
  "antimono (strict_linear_order_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  using antimono_strict_partial_order_on antimono_connected_on
  by (intro antimonoI le_predI; elim strict_linear_order_onE) auto

lemma strict_linear_order_on_rel_map_if_injective_on_if_mono_wrt_pred_if_strict_linear_order_on:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "strict_linear_order_on P R"
  and "(Q ⇒ P) f"
  and "injective_on Q f"
  shows "strict_linear_order_on Q (rel_map f R)"
  using assms by (intro strict_linear_order_onI
    strict_partial_order_on_rel_map_if_mono_wrt_pred_if_strict_partial_order_on
    connected_on_rel_map_if_injective_on_if_mono_wrt_pred_if_connected_on)
  auto

consts strict_linear_order :: "'a ⇒ bool"

overloading
  strict_linear_order ≡ "strict_linear_order :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(strict_linear_order :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ strict_linear_order_on (⊤ :: 'a ⇒ bool)"
end

lemma strict_linear_order_eq_strict_linear_order_on:
  "(strict_linear_order :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = strict_linear_order_on (⊤ :: 'a ⇒ bool)"
  unfolding strict_linear_order_def ..

lemma strict_linear_order_eq_strict_linear_order_on_uhint [uhint]:
  assumes "P ≡ ⊤ :: 'a ⇒ bool"
  shows "(strict_linear_order :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ strict_linear_order_on P"
  using assms by (simp add: strict_linear_order_eq_strict_linear_order_on)

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

lemma strict_linear_orderI [intro]:
  assumes "strict_partial_order R"
  and "connected R"
  shows "strict_linear_order R"
  using assms by (urule strict_linear_order_onI)

lemma strict_linear_orderE [elim]:
  assumes "strict_linear_order R"
  obtains "strict_partial_order R" "connected R"
  using assms by (urule (e) strict_linear_order_onE)

lemma strict_linear_order_on_if_strict_linear_order:
  fixes P :: "'a ⇒ bool"
  assumes "strict_linear_order R"
  shows "strict_linear_order_on P R"
  using assms by (elim strict_linear_orderE)
  (intro strict_linear_order_onI strict_partial_order_on_if_strict_partial_order
    connected_on_if_connected)

end

end