Theory Linear_Orders

✐‹creator "Kevin Kappelmann"›
subsection ‹Linear Orders›
theory Linear_Orders
  imports
    Binary_Relations_Connected
    Partial_Orders
begin

definition "linear_order_on ≡ partial_order_on ⊓ connected_on"

lemma linear_order_onI [intro]:
  assumes "partial_order_on P R"
  and "connected_on P R"
  shows "linear_order_on P R"
  using assms unfolding linear_order_on_def by auto

lemma linear_order_onE [elim]:
  assumes "linear_order_on P R"
  obtains "partial_order_on P R" "connected_on P R"
  using assms unfolding linear_order_on_def by auto

definition "(linear_order :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ linear_order_on (⊤ :: 'a ⇒ bool)"

lemma linear_order_eq_linear_order_on:
  "(linear_order :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = linear_order_on (⊤ :: 'a ⇒ bool)"
  unfolding linear_order_def ..

lemma linear_order_eq_linear_order_on_uhint [uhint]:
  assumes "P ≡ ⊤ :: 'a ⇒ bool"
  shows "(linear_order :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ linear_order_on P"
  using assms by (simp add: linear_order_eq_linear_order_on)

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

lemma linear_orderI [intro]:
  assumes "partial_order R"
  and "connected R"
  shows "linear_order R"
  using assms by (urule linear_order_onI)

lemma linear_orderE [elim]:
  assumes "linear_order R"
  obtains "partial_order R" "connected R"
  using assms by (urule (e) linear_order_onE)

lemma linear_order_on_if_linear_order:
  fixes P :: "'a ⇒ bool"
  assumes "linear_order R"
  shows "linear_order_on P R"
  using assms by (elim linear_orderE)
  (intro linear_order_onI partial_order_on_if_partial_order connected_on_if_connected)

end

end