Theory Type_Simple_Orders

(* Title: Examples/TTS_Foundations/Orders/Type_Simple_Orders.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Abstract orders on types›
theory Type_Simple_Orders
  imports
    "../Foundations/FNDS_Definite_Description"
    FNDS_Auxiliary
begin



subsection‹Background›


text‹
The results presented in this section were ported 
(with amendments and additions) from the theories \<^text>‹Orderings› 
and \<^text>‹Set_Interval› in the main library of Isabelle/HOL.
›



subsection‹Order operations›


text‹Abstract order operations.›

locale ord = 
  fixes le ls :: "['a, 'a] ⇒ bool"

locale ord_syntax = ord le ls for le ls :: "['a, 'a] ⇒ bool"
begin

notation
  le ("'(≤⇩_a')") and
  le (infix "≤⇩_a" 50) and
  ls ("'(<⇩_a')") and
  ls (infix "<⇩_a" 50)

abbreviation (input) ge (infix "≥⇩_a" 50)
  where "x ≥⇩_a y ≡ y ≤⇩_a x"
abbreviation (input) gt (infix ">⇩_a" 50)
  where "x >⇩_a y ≡ y <⇩_a x"

notation
  ge ("'(≥⇩_a')") and
  ge (infix "≥⇩_a" 50) and
  gt ("'(>⇩_a')") and
  gt (infix ">⇩_a" 50)

end

locale ord_dual = ord le ls for le ls :: "['a, 'a] ⇒ bool"
begin

interpretation ord_syntax .
sublocale dual: ord ge gt .

end


text‹Pairs.›

locale ord_pair = ord⇩_a: ord le⇩_a ls⇩_a + ord⇩_b: ord le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"
begin

sublocale rev: ord_pair le⇩_b ls⇩_b le⇩_a ls⇩_a .

end

locale ord_pair_syntax = ord_pair le⇩_a ls⇩_a le⇩_b ls⇩_b 
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"
begin

sublocale ord⇩_a: ord_syntax le⇩_a ls⇩_a + ord⇩_b: ord_syntax le⇩_b ls⇩_b .

notation le⇩_a (‹'(≤⇩_a')›)
  and le⇩_a (infix ‹≤⇩_a› 50) 
  and ls⇩_a (‹'(<⇩_a')›) 
  and ls⇩_a (infix ‹<⇩_a› 50)
  and le⇩_b (‹'(≤⇩_b')›)
  and le⇩_b (infix ‹≤⇩_b› 50) 
  and ls⇩_b (‹'(<⇩_b')›) 
  and ls⇩_b (infix ‹<⇩_b› 50)

notation ord⇩_a.ge (‹'(≥⇩_a')›) 
  and ord⇩_a.ge (infix ‹≥⇩_a› 50) 
  and ord⇩_a.gt (‹'(>⇩_a')›) 
  and ord⇩_a.gt (infix ‹>⇩_a› 50)
  and ord⇩_b.ge (‹'(≥⇩_b')›) 
  and ord⇩_b.ge (infix ‹≥⇩_b› 50) 
  and ord⇩_b.gt (‹'(>⇩_b')›) 
  and ord⇩_b.gt (infix ‹>⇩_b› 50)

end

locale ord_pair_dual = ord_pair le⇩_a ls⇩_a le⇩_b ls⇩_b 
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale ord_dual: ord_pair ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› .
sublocale dual_ord: ord_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› .
sublocale dual_dual: ord_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› .

end



subsection‹Preorders›


subsubsection‹Definitions›


text‹Abstract preorders.›

locale preorder = ord le ls for le ls :: "['a, 'a] ⇒ bool" +
  assumes less_le_not_le: "ls x y ⟷ le x y ∧ ¬ (le y x)"
    and order_refl[iff]: "le x x"
    and order_trans: "le x y ⟹ le y z ⟹ le x z"

locale preorder_dual = preorder le ls for le ls :: "['a, 'a] ⇒ bool"
begin

interpretation ord_syntax .

sublocale ord_dual .

sublocale dual: preorder ge gt 
  by standard (auto simp: less_le_not_le intro: order_trans)

end


text‹Pairs.›

locale ord_preorder = ord_pair le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_b: preorder le⇩_b ls⇩_b 
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"

locale ord_preorder_dual = ord_preorder le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale ord_pair_dual .
sublocale ord_dual: ord_preorder ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)›
  by unfold_locales (auto simp: ord⇩_b.less_le_not_le intro: ord⇩_b.order_trans)
sublocale dual_ord: ord_preorder ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› 
  by (rule ord_preorder_axioms)
sublocale dual_dual: ord_preorder ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)›
  by (rule ord_dual.ord_preorder_axioms)

end

locale preorder_pair = ord_preorder le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_a: preorder le⇩_a ls⇩_a
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"
begin

sublocale rev: preorder_pair le⇩_b ls⇩_b le⇩_a ls⇩_a ..

end

locale preorder_pair_dual = preorder_pair le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale ord_preorder_dual ..
sublocale ord_dual: preorder_pair ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..
sublocale dual_ord: preorder_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› 
  by unfold_locales (auto intro: ord⇩_a.order_trans simp: ord⇩_a.less_le_not_le)
sublocale dual_dual: preorder_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..

end


subsubsection‹Results›

context preorder
begin

interpretation ord_syntax .


text‹Reflexivity.›

lemma eq_refl: 
  assumes "x = y"
  shows "x ≤⇩_a y" 
  using assms by (rule ssubst) (rule order_refl)  
  
lemma less_irrefl[iff]: "¬ x <⇩_a x" by (simp add: less_le_not_le)

lemma less_imp_le: 
  assumes "x <⇩_a y"
  shows "x ≤⇩_a y" 
  using assms by (simp add: less_le_not_le)

lemma strict_implies_not_eq: 
  assumes "a <⇩_a b"
  shows "a ≠ b" 
  using assms by blast


text‹Asymmetry.›

lemma less_not_sym: 
  assumes "x <⇩_a y"
  shows "¬ (y <⇩_a x)"
  using assms by (simp add: less_le_not_le)

lemma asym: 
  assumes "a <⇩_a b" and "b <⇩_a a" 
  shows False
  using assms by (simp add: less_not_sym)

lemma less_asym: 
  assumes "x <⇩_a y" and "(¬ P ⟹ y <⇩_a x)" 
  shows P
  using assms by (auto dest: asym)
 

text‹Transitivity.›

lemma less_trans: 
  assumes "x <⇩_a y" and "y <⇩_a z" 
  shows "x <⇩_a z"
  using assms by (auto simp: less_le_not_le intro: order_trans)

lemma le_less_trans: 
  assumes "x ≤⇩_a y" and "y <⇩_a z" 
  shows "x <⇩_a z"  
  using assms by (auto simp: less_le_not_le intro: order_trans)

lemma less_le_trans: 
  assumes "x <⇩_a y" and "y ≤⇩_a z" 
  shows "x <⇩_a z"
  using assms by (auto simp: less_le_not_le intro: order_trans)

lemma less_imp_not_less: 
  assumes "x <⇩_a y"
  shows "(¬ y <⇩_a x) ⟷ True"
  using assms by (elim less_asym) simp

lemma less_imp_triv: 
  assumes "x <⇩_a y"
  shows "(y <⇩_a x ⟶ P) ⟷ True"
  using assms by (elim less_asym) simp

lemma less_asym': 
  assumes "a <⇩_a b" and "b <⇩_a a" 
  shows P 
  using assms by (rule less_asym)

end



subsection‹Partial orders›


subsubsection‹Definitions›


text‹Abstract partial orders.›

locale order = preorder le ls for le ls :: "['a, 'a] ⇒ bool" +
  assumes antisym: "le x y ⟹ le y x ⟹ x = y"

locale order_dual = order le ls for le ls :: "['a, 'a] ⇒ bool"
begin

interpretation ord_syntax .

sublocale preorder_dual ..

sublocale dual: order ge gt 
  unfolding order_def order_axioms_def
  apply unfold_locales
  apply(rule conjI)
  subgoal by (rule dual.preorder_axioms)
  subgoal by (simp add: antisym)
  done

end


text‹Pairs.›

locale ord_order = ord_preorder le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_b: order le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"

locale ord_order_dual = ord_order le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale ord_preorder_dual ..
sublocale ord_dual: ord_order ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)›
  by unfold_locales (simp add: ord⇩_b.antisym)
sublocale dual_ord: ord_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› 
  by (rule ord_order_axioms)
sublocale dual_dual: ord_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)›
  by (rule ord_dual.ord_order_axioms)

end

locale preorder_order = ord_order le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_a: preorder le⇩_a ls⇩_a
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool"
begin

sublocale preorder_pair ..

end

locale preorder_order_dual = preorder_order le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool" 
begin

interpretation ord_pair_syntax .

sublocale ord_order_dual ..
sublocale preorder_pair_dual ..
sublocale ord_dual: preorder_order ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› .. 
sublocale dual_ord: preorder_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› .. 
sublocale dual_dual: preorder_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..

end

locale order_pair = preorder_order le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_a: order le⇩_a ls⇩_a
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool" 
begin

sublocale rev: order_pair le⇩_b ls⇩_b le⇩_a ls⇩_a ..

end

locale order_pair_dual = order_pair le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "['a, 'a] ⇒ bool" and le⇩_b ls⇩_b :: "['b, 'b] ⇒ bool" 
begin

interpretation ord_pair_syntax .

sublocale preorder_order_dual ..
sublocale ord_dual: order_pair ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..
sublocale dual_ord: order_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› 
  by unfold_locales (simp add: ord⇩_a.antisym)
sublocale dual_dual: order_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..

end


subsubsection‹Results›

context order
begin

interpretation ord_syntax .


text‹Reflexivity.›

lemma less_le: "x <⇩_a y ⟷ x ≤⇩_a y ∧ x ≠ y"
  by (auto simp: less_le_not_le intro: antisym)

lemma le_less: "x ≤⇩_a y ⟷ x <⇩_a y ∨ x = y" by (auto simp: less_le)

lemma le_imp_less_or_eq: 
  assumes "x ≤⇩_a y"
  shows "x <⇩_a y ∨ x = y" 
  using assms by (simp add: le_less)

lemma less_imp_not_eq: 
  assumes "x <⇩_a y"
  shows "(x = y) ⟷ False" 
  using assms by auto

lemma less_imp_not_eq2: 
  assumes "x <⇩_a y"
  shows "(y = x) ⟷ False"
  using assms by auto


text‹Transitivity.›

lemma neq_le_trans: 
  assumes "a ≠ b" and "a ≤⇩_a b" 
  shows "a <⇩_a b" 
  using assms by (simp add: less_le)

lemma le_neq_trans: 
  assumes "a ≤⇩_a b" and "a ≠ b" 
  shows "a <⇩_a b" 
  using assms by (simp add: less_le)

text‹Asymmetry.›

lemma eq_iff: "x = y ⟷ x ≤⇩_a y ∧ y ≤⇩_a x" by (blast intro: antisym)

lemma antisym_conv: 
  assumes "y ≤⇩_a x"
  shows "x ≤⇩_a y ⟷ x = y" 
  using assms by (blast intro: antisym)


text‹Other results.›

lemma antisym_conv1: 
  assumes "¬ x <⇩_a y"
  shows "x ≤⇩_a y ⟷ x = y"
  using assms by (simp add: le_less)

lemma antisym_conv2: 
  assumes "x ≤⇩_a y"
  shows "¬ x <⇩_a y ⟷ x = y"
  using assms le_less by auto

lemma leD: 
  assumes "y ≤⇩_a x"
  shows "¬ x <⇩_a y"
  using assms by (simp add: less_le_not_le)

end



subsection‹Dense orders›


text‹Abstract dense orders.›

locale dense_order = order le ls for le ls :: "['a, 'a] ⇒ bool" +
  assumes dense: "ls x y ⟹ (∃z. ls x z ∧ ls z y)"

locale dense_order_dual = dense_order le ls for le ls :: "['a, 'a] ⇒ bool"
begin

interpretation ord_syntax .

sublocale order_dual ..

sublocale dual: dense_order ge gt 
  using dense by unfold_locales auto

end


text‹Pairs.›

locale ord_dense_order = ord_order le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_b: dense_order le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"

locale ord_dense_order_dual = ord_dense_order le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale ord_order_dual ..
sublocale ord_dual: ord_dense_order ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)›
  using ord⇩_b.dense by unfold_locales blast
sublocale dual_ord: ord_dense_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› 
  by (rule ord_dense_order_axioms)
sublocale dual_dual: ord_dense_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)›
  by (rule ord_dual.ord_dense_order_axioms)

end

locale preorder_dense_order = 
  ord_dense_order le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_a: preorder le⇩_a ls⇩_a
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"
begin

sublocale preorder_order ..

end

locale preorder_dense_order_dual = preorder_dense_order le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale ord_dense_order_dual ..
sublocale preorder_order_dual ..
sublocale ord_dual: preorder_dense_order ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..
sublocale dual_ord: preorder_dense_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› ..    
sublocale dual_dual: preorder_dense_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..

end

locale order_dense_order = 
  preorder_dense_order le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_a: order le⇩_a ls⇩_a
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"
begin

sublocale order_pair ..

end

locale order_dense_order_dual = order_dense_order le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale preorder_dense_order_dual ..
sublocale order_pair_dual ..
sublocale ord_dual: order_dense_order ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..
sublocale dual_ord: order_dense_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› ..    
sublocale dual_dual: order_dense_order ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..

end

locale dense_order_pair = 
  order_dense_order le⇩_a ls⇩_a le⇩_b ls⇩_b + ord⇩_a: dense_order le⇩_a ls⇩_a
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"

locale dense_order_pair_dual = dense_order_pair le⇩_a ls⇩_a le⇩_b ls⇩_b
  for le⇩_a ls⇩_a :: "'a ⇒ 'a ⇒ bool" and le⇩_b ls⇩_b :: "'b ⇒ 'b ⇒ bool"
begin

interpretation ord_pair_syntax .

sublocale order_dense_order_dual ..
sublocale ord_dual: dense_order_pair ‹(≤⇩_a)› ‹(<⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..
sublocale dual_ord: dense_order_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≤⇩_b)› ‹(<⇩_b)› 
  using ord⇩_a.dense by unfold_locales auto
sublocale dual_dual: dense_order_pair ‹(≥⇩_a)› ‹(>⇩_a)› ‹(≥⇩_b)› ‹(>⇩_b)› ..

end



subsection‹(Unique) top and bottom elements›


text‹Abstract extremum.›

locale extremum =
  fixes extremum :: 'a 

locale ord_extremum = ord le ls + extremum extremum 
  for le ls :: "'a ⇒ 'a ⇒ bool" and extremum :: 'a


text‹Concrete syntax.›

locale bot = extremum bot for bot :: 'a
begin

notation bot ("⊥")

end

locale top = extremum top for top :: 'a
begin

notation top ("⊤")

end



subsection‹(Unique) top and bottom elements for partial orders›


subsubsection‹Definitions›


text‹Abstract partial order with extremum.›

locale order_extremum = ord_extremum le ls extremum + order le ls
  for le ls :: "'a ⇒ 'a ⇒ bool"
  and extremum :: 'a  +
  assumes extremum[simp]: "le a extremum"


text‹Concrete syntax.›

locale order_bot = 
  order_dual le ls + 
  dual: order_extremum ‹λx y. le y x› ‹λx y. ls y x› bot + 
  bot bot 
  for le ls :: "'a ⇒ 'a ⇒ bool" and bot :: 'a 

locale order_top = order_dual le ls + order_extremum le ls top + top top
  for le ls :: "'a ⇒ 'a ⇒ bool" and top :: 'a 


subsubsection‹Results›

context order_extremum
begin

interpretation ord_syntax .

lemma extremum_uniqueI: 
  assumes "extremum ≤⇩_a a"
  shows "a = extremum"
  using assms by (simp add: antisym)

lemma extremum_unique: "extremum ≤⇩_a a ⟷ a = extremum"
  by (auto intro: antisym)

lemma extremum_strict[simp]: "¬ (extremum <⇩_a a)"
  by (fastforce simp: less_le_not_le)

lemma not_eq_extremum: "a ≠ extremum ⟷ a <⇩_a extremum"
  using le_imp_less_or_eq by (auto intro: extremum)

end



subsection‹Partial orders without top or bottom elements›


text‹Abstract partial orders without top or bottom elements.›

locale no_extremum = order le ls for le ls :: "'a ⇒ 'a ⇒ bool" +
  assumes gt_ex: "∃y. ls x y"


text‹Concrete syntax.›

locale no_top = order_dual le ls + no_extremum le ls 
  for le ls :: "'a ⇒ 'a ⇒ bool"

locale no_bot = 
  order_dual le ls + 
  dual: no_extremum ‹λx y. le y x› ‹λx y. ls y x› 
  for le ls :: "'a ⇒ 'a ⇒ bool"



subsection‹Least and greatest operators›

definition Least :: "['a set, ['a, 'a] ⇒ bool, 'a ⇒ bool] ⇒ 'a option" 
  (‹(on _ with _ : «Least» _)› [1000, 1000, 1000] 10) 
  where 
    "on U with op : «Least» P ≡ (THE x on U. P x ∧ (∀y∈U. P y ⟶ op x y))"

ctr relativization
  synthesis ctr_simps
  assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (λx. x ∈ U)"
    and [transfer_rule]: "bi_unique A" "right_total A" 
  trp (?'a A)
  in Least_def

context ord_syntax
begin

abbreviation Least where "Least ≡ Type_Simple_Orders.Least UNIV (≤⇩_a)"
abbreviation Greatest where "Greatest ≡ Type_Simple_Orders.Least UNIV (≥⇩_a)"

lemmas Least_def = Least_def[of UNIV ‹(≤⇩_a)›]

end

context order
begin

interpretation ord_syntax .
                  
lemma Least_equality:
  assumes "P x" and "⋀y. P y ⟹ x ≤⇩_a y"
  shows "Least P = Some x"
  unfolding Least_def by (rule The_on_Some_equality) (auto simp: assms antisym)

lemma LeastI2_order:
  assumes "P x" 
    and "⋀y. P y ⟹ x ≤⇩_a y"
    and "⋀x. P x ⟹ ∀y. P y ⟶ x ≤⇩_a y ⟹ Q x"
  obtains z where "Least P = Some z" and "Q z"
  unfolding Least_def using assms by (clarsimp simp: that Least_equality)

lemma Least_ex1:
  assumes "∃!x. P x ∧ (∀y. P y ⟶ x ≤⇩_a y)"
  obtains x where "Least P = Some x" and "P x" and "P z ⟹ x ≤⇩_a z"
  using assms unfolding Least_def by (clarsimp simp: that Least_equality)

end



subsection‹min and max›

definition min :: "[['a, 'a] ⇒ bool, 'a, 'a] ⇒ 'a" where
  "min le a b = (if le a b then a else b)"

ctr parametricity
  in min_def  

context ord_syntax
begin

abbreviation min where "min ≡ Type_Simple_Orders.min (≤⇩_a)"
abbreviation max where "max ≡ Type_Simple_Orders.min (≥⇩_a)"

end

context ord
begin

interpretation ord_syntax .

lemma min_absorb1: "x ≤⇩_a y ⟹ min x y = x"
  unfolding min_def by simp

end


context order
begin

interpretation ord_syntax .

lemma min_absorb2: 
  assumes "y ≤⇩_a x"
  shows "min x y = y"
  using assms unfolding min_def by (simp add: eq_iff)

end

context order_extremum
begin

interpretation ord_syntax .

lemma max_top[simp]: "max extremum x = extremum"
  by (simp add: ord.min_absorb1)

lemma max_top2[simp]: "max x extremum = extremum"
  unfolding min_def by (simp add: extremum_uniqueI)

lemma min_top[simp]: "min extremum x = x" by (simp add: min_absorb2)

lemma min_top2[simp]: "min x extremum = x"  by (simp add: min_def top_unique)

end



subsection‹Monotonicity›

definition mono :: 
  "['a set, ['a, 'a] ⇒ bool, ['b, 'b] ⇒ bool, 'a ⇒ 'b] ⇒ bool" 
  (‹(on _ with _ _ : «mono» _)› [1000, 1000, 999, 1000] 10) 
  where
    "on U⇩_a with op⇩₁ op⇩₂ : «mono» f ≡ ∀x∈U⇩_a. ∀y∈U⇩_a. op⇩₁ x y ⟶ op⇩₂ (f x) (f y)"

ctr parametricity
  in mono_def

context ord_pair_syntax
begin

abbreviation mono⇩_a⇩_b 
  where "mono⇩_a⇩_b ≡ Type_Simple_Orders.mono UNIV (≤⇩_a) (≤⇩_b)"
abbreviation mono⇩_b⇩_a 
  where "mono⇩_b⇩_a ≡ Type_Simple_Orders.mono UNIV (≤⇩_b) (≤⇩_a)"
abbreviation antimono⇩_a⇩_b 
  where "antimono⇩_a⇩_b ≡ Type_Simple_Orders.mono UNIV (≤⇩_a) (≥⇩_b)"
abbreviation antimono⇩_b⇩_a 
  where "antimono⇩_b⇩_a ≡ Type_Simple_Orders.mono UNIV (≤⇩_b) (≥⇩_a)"
abbreviation strict_mono⇩_a⇩_b 
  where "strict_mono⇩_a⇩_b ≡ Type_Simple_Orders.mono UNIV (<⇩_a) (<⇩_b)"
abbreviation strict_mono⇩_b⇩_a 
  where "strict_mono⇩_b⇩_a ≡ Type_Simple_Orders.mono UNIV (<⇩_b) (<⇩_a)"
abbreviation strict_antimono⇩_a⇩_b 
  where "strict_antimono⇩_a⇩_b ≡ Type_Simple_Orders.mono UNIV (<⇩_a) (>⇩_b)"
abbreviation strict_antimono⇩_b⇩_a 
  where "strict_antimono⇩_b⇩_a ≡ Type_Simple_Orders.mono UNIV (<⇩_b) (>⇩_a)"

end

context ord_pair
begin

interpretation ord_pair_syntax .

lemma monoI[intro?]: 
  assumes "⋀x y. x ≤⇩_a y ⟹ f x ≤⇩_b f y" 
  shows "mono⇩_a⇩_b f"
  unfolding mono_def using assms by simp

lemma monoD[dest?]:
  assumes "mono⇩_a⇩_b f" and "x ≤⇩_a y" 
  shows "f x ≤⇩_b f y"
  using assms unfolding mono_def by simp

lemma monoE:
  assumes "mono⇩_a⇩_b f" and "x ≤⇩_a y"
  obtains "f x ≤⇩_b f y"
  using assms unfolding mono_def by simp

lemma strict_monoI[intro?]: 
  assumes "⋀x y. x <⇩_a y ⟹ f x <⇩_b f y" 
  shows "strict_mono⇩_a⇩_b f"
  unfolding mono_def using assms by simp

lemma strict_monoD[dest?]:
  assumes "strict_mono⇩_a⇩_b f" and "x <⇩_a y" 
  shows "f x <⇩_b f y"
  using assms unfolding mono_def by simp

lemma strict_monoE:
  assumes "strict_mono⇩_a⇩_b f" and "x <⇩_a y"
  obtains "f x <⇩_b f y"
  using assms unfolding mono_def by simp

end

context order_pair
begin

interpretation ord_pair_syntax .

lemma strict_mono_mono[dest?]: 
  assumes "strict_mono⇩_a⇩_b f"
  shows "mono⇩_a⇩_b f"
proof(rule monoI)
  fix x y
  assume "x ≤⇩_a y"
  show "f x ≤⇩_b f y"
  proof (cases "x = y")
    case True then show ?thesis by simp
  next
    case False with ‹x ≤⇩_a y› have "x <⇩_a y" by (simp add: ord⇩_a.neq_le_trans)
    with assms strict_monoD have "f x <⇩_b f y" by simp
    then show ?thesis by (simp add: ord⇩_b.le_less)
  qed
qed

end



subsection‹Set intervals›

definition ray :: "['a set, ['a, 'a] ⇒ bool, 'a] ⇒ 'a set" 
  (‹(on _ with _ : {..⊏_})› [1000, 1000, 1000] 10) 
  where "on U with op : {..⊏u} ≡ {x ∈ U. op x u}" 
definition interval :: 
  "['a set, ['a, 'a] ⇒ bool, ['a, 'a] ⇒ bool, 'a, 'a] ⇒ 'a set"
  (‹(on _ with _ _ : {_⊏..⊏_})› [1000, 1000, 999, 1000, 1000] 10) 
  where "on U with op⇩₁ op⇩₂ : {l⊏..⊏u} ≡ 
    (on U with (λx y. op⇩₁ y x) : {..⊏l}) ∩ (on U with op⇩₂ : {..⊏u})"

lemma ray_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows "(rel_set A ===> (A ===> A ===> (=)) ===> A ===> rel_set A) ray ray"
  unfolding ray_def
proof(intro rel_funI)
  fix S :: "'a set" and S' :: "'b set" 
    and le :: "['a, 'a] ⇒ bool" and le' :: "['b, 'b] ⇒ bool" 
    and u u'
  assume [transfer_rule]: "rel_set A S S'"
    and [transfer_rule]: "(A ===> A ===> (=)) le le'"
    and [transfer_rule]: "A u u'"
  show "rel_set A {xc ∈ S. le xc u} {x ∈ S'. le' x u'}"
  proof(intro rel_setI)
    show "x ∈ {xc ∈ S. le xc u} ⟹ ∃x'∈{x ∈ S'. le' x u'}. A x x'" for x
    proof-
      assume x: "x ∈ {xc ∈ S. le xc u}"
      then obtain x' where [transfer_rule]: "A x x'"  
        using ‹rel_set A S S'› rel_setD1 by fastforce
      from x have "x' ∈ {x ∈ S'. le' x u'}" 
        apply transfer using ‹A x x'› by auto
      then show ?thesis by (auto simp: ‹A x x'›)
    qed
    show "x' ∈ {x ∈ S'. le' x u'} ⟹ ∃x∈{xc ∈ S. le xc u}. A x x'" for x'
    proof-
      assume x': "x' ∈ {x ∈ S'. le' x u'}"
      then obtain x where [transfer_rule]: "A x x'"   
        using assms(2) by (auto elim: right_totalE)
      from x' have "x ∈ {xc ∈ S. le xc u}" by transfer auto
      then show ?thesis by (auto simp: ‹A x x'›)
    qed  
  qed
qed

ctr relativization
  assumes [transfer_rule]: "right_total A" "bi_unique A"
  trp (?'a A)
  in interval_def

lemma interval_ge_le:
  "(on UNIV with (λx y. le⇩_a y x) (λx y. le⇩_b y x) : {l⊏..⊏h}) = 
    (on UNIV with le⇩_b le⇩_a : {h⊏..⊏l})"
  unfolding interval_def by auto

context ord_syntax  
begin

abbreviation lessThan (‹{..<⇩_a_}›) 
  where "{..<⇩_au} ≡ on UNIV with (<⇩_a) : {..⊏u}"
abbreviation atMost (‹{..≤⇩_a_}›) 
  where "{..≤⇩_au} ≡ on UNIV with (≤⇩_a) : {..⊏u}"
abbreviation greaterThan (‹{_<⇩_a..}›) 
  where "{l<⇩_a..} ≡ on UNIV with (>⇩_a) : {..⊏l}"
abbreviation atLeast (‹{_≤⇩_a..}›) 
  where "{l≤⇩_a..} ≡ on UNIV with (≥⇩_a) : {..⊏l}"
abbreviation greaterThanLessThan (‹{_<⇩_a..<⇩_a_}›) 
  where "{l<⇩_a..<⇩_au} ≡ on UNIV with (<⇩_a) (<⇩_a) : {l⊏..⊏u}"
abbreviation atLeastLessThan (‹{_≤⇩_a..<⇩_a_}›) 
  where "{l≤⇩_a..<⇩_au} ≡ on UNIV with (≤⇩_a) (<⇩_a) : {l⊏..⊏u}"
abbreviation greaterThanAtMost (‹{_<⇩_a..≤⇩_a_}›) 
  where "{l<⇩_a..≤⇩_au} ≡ on UNIV with (<⇩_a) (≤⇩_a) : {l⊏..⊏u}"
abbreviation atLeastAtMost (‹{_≤⇩_a..≤⇩_a_}›) 
  where "{l≤⇩_a..≤⇩_au} ≡ on UNIV with (≤⇩_a) (≤⇩_a) : {l⊏..⊏u}"
abbreviation lessThanGreaterThan (‹{_>⇩_a..>⇩_a_}›) 
  where "{l>⇩_a..>⇩_au} ≡ on UNIV with (>⇩_a) (>⇩_a) : {l⊏..⊏u}"
abbreviation lessThanAtLeast (‹{_≥⇩_a..>⇩_a_}›) 
  where "{l≥⇩_a..>⇩_au} ≡ on UNIV with (≥⇩_a) (>⇩_a) : {l⊏..⊏u}"
abbreviation atMostGreaterThan (‹{_>⇩_a..≥⇩_a_}›) 
  where "{l>⇩_a..≥⇩_au} ≡ on UNIV with (>⇩_a) (≥⇩_a) : {l⊏..⊏u}"
abbreviation atMostAtLeast (‹{_≥⇩_a..≥⇩_a_}›) 
  where "{l≥⇩_a..≥⇩_au} ≡ on UNIV with (≥⇩_a) (≥⇩_a) : {l⊏..⊏u}"

end

context ord
begin

interpretation ord_syntax .

lemma lessThan_iff[iff]: "(i ∈ {..<⇩_ak}) = (i <⇩_a k)"
  unfolding ray_def by simp

lemma atLeast_iff[iff]: "(i ∈ {k≤⇩_a..}) = (k ≤⇩_a i)"
  unfolding ray_def by simp

lemma greaterThanLessThan_iff[simp]: "(i ∈ {l<⇩_a..<⇩_au}) = (l <⇩_a i ∧ i <⇩_a u)"
  unfolding interval_def ray_def by simp

lemma atLeastLessThan_iff[simp]: "(i ∈ {l≤⇩_a..<⇩_au}) = (l ≤⇩_a i ∧ i <⇩_a u)"
  unfolding interval_def ray_def by simp

lemma greaterThanAtMost_iff[simp]: "(i ∈ {l<⇩_a..≤⇩_au}) = (l <⇩_a i ∧ i ≤⇩_a u)"
  unfolding interval_def ray_def by simp

lemma atLeastAtMost_iff[simp]: "(i ∈ {l≤⇩_a..≤⇩_au}) = (l ≤⇩_a i ∧ i ≤⇩_a u)"
  unfolding interval_def ray_def by simp

lemma greaterThanLessThan_eq: "{a<⇩_a..<⇩_ab} = {a<⇩_a..} ∩ {..<⇩_ab}"
  unfolding interval_def ray_def by simp

end

context ord_pair_syntax
begin

notation ord⇩_a.lessThan (‹{..<⇩_a_}›) 
  and ord⇩_a.atMost (‹{..≤⇩_a_}›) 
  and ord⇩_a.greaterThan (‹{_<⇩_a..}›) 
  and ord⇩_a.atLeast (‹{_≤⇩_a..}›) 
  and ord⇩_a.greaterThanLessThan (‹{_<⇩_a..<⇩_a_}›) 
  and ord⇩_a.atLeastLessThan (‹{_≤⇩_a..<⇩_a_}›) 
  and ord⇩_a.greaterThanAtMost (‹{_<⇩_a..≤⇩_a_}›) 
  and ord⇩_a.atLeastAtMost (‹{_≤⇩_a..≤⇩_a_}›) 
  and ord⇩_a.lessThanGreaterThan (‹{_>⇩_a..>⇩_a_}›)
  and ord⇩_a.lessThanAtLeast (‹{_≥⇩_a..>⇩_a_}›) 
  and ord⇩_a.atMostGreaterThan (‹{_>⇩_a..≥⇩_a_}›) 
  and ord⇩_a.atMostAtLeast (‹{_≥⇩_a..≥⇩_a_}›) 
  and ord⇩_b.lessThan (‹{..<⇩_b_}›) 
  and ord⇩_b.atMost (‹{..≤⇩_b_}›) 
  and ord⇩_b.greaterThan (‹{_<⇩_b..}›) 
  and ord⇩_b.atLeast (‹{_≤⇩_b..}›) 
  and ord⇩_b.greaterThanLessThan (‹{_<⇩_b..<⇩_b_}›) 
  and ord⇩_b.atLeastLessThan (‹{_≤⇩_b..<⇩_b_}›) 
  and ord⇩_b.greaterThanAtMost (‹{_<⇩_b..≤⇩_b_}›) 
  and ord⇩_b.atLeastAtMost (‹{_≤⇩_b..≤⇩_b_}›)
  and ord⇩_b.lessThanGreaterThan (‹{_>⇩_b..>⇩_b_}›)
  and ord⇩_b.lessThanAtLeast (‹{_≥⇩_b..>⇩_b_}›) 
  and ord⇩_b.atMostGreaterThan (‹{_>⇩_b..≥⇩_b_}›) 
  and ord⇩_b.atMostAtLeast (‹{_≥⇩_b..≥⇩_b_}›)

end

context preorder
begin

interpretation ord_syntax .

lemma Ioi_le_Ico: "{a<⇩_a..} ⊆ {a≤⇩_a..}"
  unfolding ray_def by (fastforce simp: less_le_not_le)

end

context preorder
begin

interpretation ord_syntax .

interpretation preorder_dual le ls
  by (rule preorder_dual.intro[OF preorder_axioms])

lemma single_Diff_lessThan[simp]: "{k} - {..<⇩_ak} = {k}" by auto

lemma atLeast_subset_iff[iff]: "({x≤⇩_a..} ⊆ {y≤⇩_a..}) = (y ≤⇩_a x)"
  by (auto intro: order_trans)

lemma atLeastatMost_empty[simp]: 
  assumes "b <⇩_a a"
  shows "{a≤⇩_a..≤⇩_ab} = {}"
  unfolding interval_def 
  using less_le_not_le assms
  by (metis Int_emptyI ord.lessThan_iff atLeast_iff order_trans)

lemma atLeastatMost_empty_iff[simp]: "{a≤⇩_a..≤⇩_ab} = {} ⟷ (¬ a ≤⇩_a b)"
  by auto (blast intro: order_trans)

lemma atLeastatMost_empty_iff2[simp]: "{} = {a≤⇩_a..≤⇩_ab} ⟷ (¬ a ≤⇩_a b)"
  by auto (blast intro: order_trans)

lemma atLeastLessThan_empty[simp]: 
  assumes "b ≤⇩_a a" 
  shows "{a≤⇩_a..<⇩_ab} = {}"
  unfolding interval_def 
  using assms less_le_not_le 
  by (blast intro: order_trans)

lemma atLeastLessThan_empty_iff[simp]: "{a≤⇩_a..<⇩_ab} = {} ⟷ (¬ a <⇩_a b)"
  unfolding interval_def by (auto simp: le_less_trans ord.lessThan_iff)

lemma atLeastLessThan_empty_iff2[simp]: "{} = {a≤⇩_a..<⇩_ab} ⟷ (¬ a <⇩_a b)"
  unfolding interval_def by (auto simp: le_less_trans ord.lessThan_iff)

lemma greaterThanAtMost_empty[simp]: 
  assumes "l ≤⇩_a k" 
  shows "{k<⇩_a..≤⇩_al} = {}" 
  using assms atLeastLessThan_empty[OF assms]
  unfolding 
    greaterThanAtMost_eq_atLeastAtMost_diff 
    atLeastLessThan_eq_atLeastAtMost_diff
  using le_less_trans by auto blast

lemma greaterThanAtMost_empty_iff[simp]: "{k<⇩_a..≤⇩_al} = {} ⟷ ¬ k <⇩_a l"
  by (auto simp: dual.le_less_trans)

lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<⇩_a..≤⇩_al} ⟷ ¬ k <⇩_a l"
  unfolding interval_def ray_def by (blast intro: less_le_trans)

lemma greaterThanLessThan_empty[simp]: 
  assumes "l ≤⇩_a k" 
  shows "{k<⇩_a..<⇩_al} = {}"
  using assms by auto (blast intro: le_less_trans asym equals0I)

lemma atLeastatMost_subset_iff[simp]:
  "{a≤⇩_a..≤⇩_ab} ≤ {c≤⇩_a..≤⇩_ad} ⟷ (¬ a ≤⇩_a b) ∨ c ≤⇩_a a ∧ b ≤⇩_a d"
  by auto (blast intro: order_trans)+

lemma atLeastatMost_psubset_iff:
  "{a≤⇩_a..≤⇩_ab} < {c≤⇩_a..≤⇩_ad} ⟷
    ((¬ a ≤⇩_a b) ∨ c ≤⇩_a a ∧ b ≤⇩_a d ∧ (c <⇩_a a ∨ b <⇩_a d)) ∧ c ≤⇩_a d"
  by (simp add: psubset_eq set_eq_iff less_le_not_le) 
    (blast intro: order_trans)

lemma Icc_subset_Ici_iff[simp]: 
  "{l≤⇩_a..≤⇩_ah} ⊆ {l'≤⇩_a..} = (¬ l ≤⇩_a h ∨ l ≥⇩_a l')"
  by (auto simp: subset_eq intro: order_trans)

lemma Icc_subset_Iic_iff[simp]: 
  "{l≤⇩_a..≤⇩_ah} ⊆ {..≤⇩_ah'} = (¬ l ≤⇩_a h ∨ h ≤⇩_a h')"
  unfolding interval_def ray_def by (blast intro: order_trans)+

lemma not_Ici_eq_empty[simp]: "{l≤⇩_a..} ≠ {}" by (auto simp: set_eq_iff)

lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]

lemma Iio_Int_singleton: "{..<⇩_ak} ∩ {x} = (if x <⇩_a k then {x} else {})" by simp

lemma ivl_disj_int_one:
  "{..≤⇩_al} ∩ {l<⇩_a..<⇩_au} = {}"
  "{..<⇩_al} ∩ {l≤⇩_a..<⇩_au} = {}"
  "{..≤⇩_al} ∩ {l<⇩_a..≤⇩_au} = {}"
  "{..<⇩_al} ∩ {l≤⇩_a..≤⇩_au} = {}"
  "{l<⇩_a..≤⇩_au} ∩ {u<⇩_a..} = {}"
  "{l<⇩_a..<⇩_au} ∩ {u≤⇩_a..} = {}"
  "{l≤⇩_a..≤⇩_au} ∩ {u<⇩_a..} = {}"
  "{l≤⇩_a..<⇩_au} ∩ {u≤⇩_a..} = {}"
  using lessThan_iff dual.lessThan_iff by (auto simp: less_le_not_le)

lemma ivl_disj_int_two:
  "{l<⇩_a..<⇩_am} ∩ {m≤⇩_a..<⇩_au} = {}"
  "{l<⇩_a..≤⇩_am} ∩ {m<⇩_a..<⇩_au} = {}"
  "{l≤⇩_a..<⇩_am} ∩ {m≤⇩_a..<⇩_au} = {}"
  "{l≤⇩_a..≤⇩_am} ∩ {m<⇩_a..<⇩_au} = {}"
  "{l<⇩_a..<⇩_am} ∩ {m≤⇩_a..≤⇩_au} = {}"
  "{l<⇩_a..≤⇩_am} ∩ {m<⇩_a..≤⇩_au} = {}"
  "{l≤⇩_a..<⇩_am} ∩ {m≤⇩_a..≤⇩_au} = {}"
  "{l≤⇩_a..≤⇩_am} ∩ {m<⇩_a..≤⇩_au} = {}"
  using lessThan_iff by (auto simp: less_le_not_le)

end

context order
begin     

interpretation ord_syntax .

interpretation order_dual le ls
  by (rule order_dual.intro[OF order_axioms])

lemma atMost_Int_atLeast: "{..≤⇩_an} ∩ {n≤⇩_a..} = {n}"
  unfolding ray_def by (auto simp: eq_iff)

lemma atLeast_eq_iff[iff]: "({x≤⇩_a..} = {y≤⇩_a..}) = (x = y)" 
  unfolding ray_def using antisym by auto

lemma atLeastLessThan_eq_atLeastAtMost_diff: "{a≤⇩_a..<⇩_ab} = {a≤⇩_a..≤⇩_ab} - {b}"
  unfolding interval_def ray_def by (auto simp: less_imp_le le_less)

lemma greaterThanAtMost_eq_atLeastAtMost_diff: "{a<⇩_a..≤⇩_ab} = {a≤⇩_a..≤⇩_ab} - {a}"
  unfolding interval_def ray_def by (auto simp: less_imp_le le_less)

lemma atLeastAtMost_singleton[simp]: "{a≤⇩_a..≤⇩_aa} = {a}"
  using atMost_Int_atLeast by (fastforce simp: ray_def) 

lemma atLeastAtMost_singleton': 
  assumes "a = b"
  shows "{a≤⇩_a..≤⇩_ab} = {a}" 
  using assms by simp

lemma Icc_eq_Icc[simp]:
  "{l≤⇩_a..≤⇩_ah} = {l'≤⇩_a..≤⇩_ah'} = (l = l' ∧ h = h' ∨ ¬ l ≤⇩_a h ∧ ¬ l' ≤⇩_a h')"
  apply(rule iffI)
  subgoal by (metis antisym atLeastatMost_subset_iff eq_refl)
  subgoal using atLeastatMost_empty_iff by blast
  done

lemma atLeastAtMost_singleton_iff[simp]: "{a≤⇩_a..≤⇩_ab} = {c} ⟷ a = b ∧ b = c"
proof
  assume "{a≤⇩_a..≤⇩_ab} = {c}"
  hence *: "¬ (¬ a ≤⇩_a b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
  with ‹{a≤⇩_a..≤⇩_ab} = {c}› have "c ≤⇩_a a ∧ b ≤⇩_a c" by auto
  with * show "a = b ∧ b = c" by (auto intro: antisym order_trans) 
qed simp

end

context order_extremum
begin

interpretation ord_syntax .

lemma atMost_eq_UNIV_iff: "{..≤⇩_ax} = UNIV ⟷ x = extremum"
  by (metis ord.lessThan_iff eq_iff UNIV_I UNIV_eq_I extremum)

end

context no_extremum
begin

interpretation ord_syntax .

interpretation order_dual le ls
  by (rule order_dual.intro[OF order_axioms])

lemma not_UNIV_le_Icc[simp]: "¬ UNIV ⊆ {l≤⇩_a..≤⇩_ah}"
  using gt_ex[of h] by (auto simp: subset_eq less_le_not_le)

lemma not_UNIV_le_Iic[simp]: "¬ UNIV ⊆ {..≤⇩_ah}"
  using gt_ex[of h] by (auto simp: less_le_not_le)

lemma not_Ici_le_Icc[simp]: "¬ {l≤⇩_a..} ⊆ {l'≤⇩_a..≤⇩_ah'}"
  using gt_ex[of h']
  by (auto simp: subset_eq less_le) 
    (blast dest: antisym_conv intro: order_trans)

lemma not_Ici_le_Iic[simp]: "¬ {l≤⇩_a..} ⊆ {..≤⇩_ah'}"
proof
  assume "{l≤⇩_a..} ⊆ {..≤⇩_ah'}"
  then have x: "l ≤⇩_a x ⟹ x ≤⇩_a h'" for x by auto
  from gt_ex obtain x where "h' <⇩_a x" by auto
  show False
  proof(cases ‹l ≤⇩_a x›)
    case True show ?thesis 
      using x[OF True] less_le_not_le by (force simp: ‹h' <⇩_a x›)
  next
    case False
    obtain y where "x ≤⇩_a y" and "y <⇩_a l"
      using ‹h' <⇩_a x› dual.less_le_trans by (blast intro: x less_imp_le)
    then have "x <⇩_a l" by (rule le_less_trans)
    then show ?thesis 
      using ‹h' <⇩_a x› less_le_not_le by (blast intro: x dual.less_trans)
  qed
qed

lemma not_UNIV_eq_Icc[simp]: "UNIV ≠ {l'≤⇩_a..≤⇩_ah'}"
  using gt_ex by (auto simp: set_eq_iff less_le_not_le)
  
lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]

lemma not_UNIV_eq_Iic[simp]: "UNIV ≠ {..≤⇩_ah'}"
  using gt_ex[of h'] not_UNIV_le_Iic by blast

lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]

lemma not_Icc_eq_Ici[simp]: "{l≤⇩_a..≤⇩_ah} ≠ {l'≤⇩_a..}"
  using not_Ici_le_Icc by blast

lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]

lemma not_Iic_eq_Ici[simp]: "{..≤⇩_ah} ≠ {l'≤⇩_a..}"
  using not_Ici_le_Iic[of l' h] by blast

lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]

lemma greaterThan_non_empty[simp]: "{x<⇩_a..} ≠ {}"
  using gt_ex[of x] unfolding ray_def by simp

end

context order
begin

interpretation ord_syntax .
interpretation order_pair le ls le ls ..
interpretation ord_pair_syntax le ls le ls .

lemma mono_image_least:
  assumes f_mono: "mono⇩_a⇩_b f" 
    and f_img: "f ` {m≤⇩_a..<⇩_an} = {m'≤⇩_a..<⇩_an'}" 
    and "m <⇩_a n"
  shows "f m = m'"
proof -
  from f_img have "{m'≤⇩_a..<⇩_an'} ≠ {}" by (force simp: assms(3))
  with f_img have "m' ∈ f ` {m≤⇩_a..<⇩_an}" by auto
  then obtain k where "f k = m'" "m ≤⇩_a k" by auto
  moreover have "m' ≤⇩_a f m" 
    unfolding interval_def using f_img by (auto simp: assms(3))
  ultimately show "f m = m'"
    using f_mono by (auto dest: monoD intro: antisym)
qed

end



subsection‹Bounded sets›

definition bdd :: "['a set, ['a, 'a] ⇒ bool, 'a set] ⇒ bool"
  (‹(on _ with _ : «bdd» _)› [1000, 1000, 1000] 10) 
  where "bdd U op A ⟷ (∃M∈U. ∀x ∈ A. op x M)"

ctr parametricity
  in bdd_def

context ord_syntax  
begin

abbreviation bdd_above where "bdd_above ≡ bdd UNIV (≤⇩_a)"
abbreviation bdd_below where "bdd_below ≡ bdd UNIV (≥⇩_a)"

end

context preorder
begin

interpretation ord_syntax .

interpretation preorder_dual ..

lemma bdd_aboveI[intro]: 
  assumes "⋀x. x ∈ A ⟹ x ≤⇩_a M"
  shows "bdd_above A"
  using assms unfolding bdd_def by auto

lemma bdd_belowI[intro]: 
  assumes "⋀x. x ∈ A ⟹ m ≤⇩_a x"
  shows "bdd_below A"
  using assms unfolding bdd_def by auto

lemma bdd_aboveI2: 
  assumes "⋀x. x ∈ A ⟹ f x ≤⇩_a M"
  shows "bdd_above (f ` A)" 
  using assms by force

lemma bdd_belowI2: 
  assumes "⋀x. x ∈ A ⟹ m ≤⇩_a f x"
  shows "bdd_below (f ` A)" 
  using assms by force

lemma bdd_above_empty[simp, intro]: "bdd_above {}"
  unfolding bdd_above_def by auto

lemma bdd_below_empty[simp, intro]: "bdd_below {}"
  unfolding bdd_below_def by auto

lemma bdd_above_mono: 
  assumes "bdd_above B" and "A ⊆ B" 
  shows "bdd_above A"
  using assms unfolding bdd_def by auto

lemma bdd_below_mono: 
  assumes "bdd_below B" and "A ⊆ B"
  shows "bdd_below A"
  using assms unfolding bdd_def by auto

lemma bdd_above_Int1[simp]: 
  assumes "bdd_above A"
  shows "bdd_above (A ∩ B)"
  using assms by (auto simp: bdd_above_mono)

lemma bdd_above_Int2[simp]: 
  assumes "bdd_above B"
  shows "bdd_above (A ∩ B)"
  using assms by (auto simp: bdd_above_mono)

lemma bdd_below_Int1[simp]: 
  assumes "bdd_below A"
  shows "bdd_below (A ∩ B)"
  using assms by (auto simp: bdd_below_mono)

lemma bdd_below_Int2[simp]: 
  assumes "bdd_below B"
  shows "bdd_below (A ∩ B)"
  using assms by (auto simp: bdd_below_mono)

lemma bdd_above_Ioo[simp, intro]: "bdd_above {a<⇩_a..<⇩_ab}" 
  by (auto intro!: less_imp_le)

lemma bdd_above_Ico[simp, intro]: "bdd_above {a≤⇩_a..<⇩_ab}" 
  by (auto intro!: less_imp_le)

lemma bdd_above_Iio[simp, intro]: "bdd_above {..<⇩_ab}"
  by (auto intro: less_imp_le)

lemma bdd_above_Ioc[simp, intro]: "bdd_above {a<⇩_a..≤⇩_ab}" by auto

lemma bdd_above_Icc[simp, intro]: "bdd_above {a≤⇩_a..≤⇩_ab}"
  by (auto intro: less_imp_le)

lemma bdd_above_Iic[simp, intro]: "bdd_above {..≤⇩_ab}"
  by (auto intro: less_imp_le)

lemma bdd_below_Ioo[simp, intro]: "bdd_below {a<⇩_a..<⇩_ab}"
  by (auto intro!: less_imp_le)

lemma bdd_below_Ioc[simp, intro]: "bdd_below {a<⇩_a..≤⇩_ab}"
  by (auto intro!: less_imp_le)

lemma bdd_below_Ioi[simp, intro]: "bdd_below {a<⇩_a..}"
  by (auto intro: less_imp_le)

lemma bdd_below_Ico[simp, intro]: "bdd_below {a≤⇩_a..<⇩_ab}" by auto

lemma bdd_below_Icc[simp, intro]: "bdd_below {a≤⇩_a..≤⇩_ab}" by auto

lemma bdd_below_Ici[simp, intro]: "bdd_below {a≤⇩_a..}"
  by (auto intro: less_imp_le)

end

context order_pair
begin

interpretation ord_pair_syntax .

lemma bdd_above_image_mono: 
  assumes "mono⇩_a⇩_b f" and "ord⇩_a.bdd_above A"
  shows "ord⇩_b.bdd_above (f ` A)"
  using assms by (auto simp: bdd_def mono_def)

lemma bdd_below_image_mono: 
  assumes "mono⇩_a⇩_b f" and "ord⇩_a.bdd_below A" 
  shows "ord⇩_b.bdd_below (f ` A)"
  using assms by (auto simp: bdd_def mono_def)

lemma bdd_above_image_antimono:
  assumes "antimono⇩_a⇩_b f" and "ord⇩_a.bdd_below A" 
  shows "ord⇩_b.bdd_above (f ` A)"
  using assms by (auto simp: bdd_def mono_def)

lemma bdd_below_image_antimono: 
  assumes "antimono⇩_a⇩_b f" and "ord⇩_a.bdd_above A"   
  shows "ord⇩_b.bdd_below (f ` A)"
  using assms by (auto simp: bdd_def mono_def)

end

context order_extremum
begin

interpretation ord_syntax .
interpretation order_dual ..

lemma bdd_above_top[simp, intro!]: "bdd_above A"
  by (rule bdd_aboveI[of _ extremum]) simp

end

text‹\newpage›

end