Theory First_Order_Clause.Restricted_Order

theory Restricted_Order
  imports 
    Main
    (*TODO: Complete_Non_Orders.Binary_Relations *)
begin
(* TODO: Report 
definition aless where
  "aless _ _ = True"

definition alesseq where
  "alesseq _ _ = True"

interpretation t: order aless alesseq
  sorry*)

section ‹Restricted Orders›

locale relation_restriction =
  fixes R :: "'a ⇒ 'a ⇒ bool" and lift :: "'b ⇒ 'a"
  assumes inj_lift [intro]: "inj lift"
begin

definition R⇩r :: "'b ⇒ 'b ⇒ bool" where
  "R⇩r b b' ≡ R (lift b) (lift b')"

end

subsection ‹Strict Orders›

locale strict_order =
  fixes
    less :: "'a ⇒ 'a ⇒ bool" (infix "≺" 50)
  assumes
    transp [intro]: "transp (≺)" and
    asymp [intro]: "asymp (≺)"
begin

abbreviation less_eq where "less_eq ≡ (≺)⇧=⇧="

notation less_eq (infix "≼" 50)

sublocale order "(≼)" "(≺)"
  by (rule order_reflclp_if_transp_and_asymp[OF transp asymp])

end

locale strict_order_restriction =
  strict_order +
  relation_restriction where R = "(≺)"
begin

abbreviation "less⇩r ≡ R⇩r"

lemmas less⇩r_def = R⇩r_def

notation less⇩r (infix "≺⇩r" 50)

sublocale restriction: strict_order "(≺⇩r)"
  by unfold_locales (auto simp: R⇩r_def transp_def)

abbreviation "less_eq⇩r ≡ restriction.less_eq"
notation less_eq⇩r (infix "≼⇩r" 50)

end

subsection ‹Wellfounded Strict Orders›

locale restricted_wellfounded_strict_order = strict_order +
  fixes restriction
  assumes wfp [intro]: "wfp_on restriction (≺)"

locale wellfounded_strict_order =
  restricted_wellfounded_strict_order where restriction = UNIV

locale wellfounded_strict_order_restriction =
  strict_order_restriction +
  restricted_wellfounded_strict_order where restriction = "range lift" and less = "(≺)"
begin

sublocale restriction: wellfounded_strict_order "(≺⇩r)"
proof unfold_locales
  show "wfp (≺⇩r)"
    using wfp_on_if_convertible_to_wfp_on[OF wfp]
    unfolding R⇩r_def
    by simp
qed

end

subsection ‹Total Strict Orders›

locale restricted_total_strict_order = strict_order +
  fixes restriction
  assumes totalp [intro]: "totalp_on restriction (≺)"
begin

lemma restricted_not_le:
  assumes "a ∈ restriction" "b ∈ restriction" "¬ b ≺ a"
  shows "a ≼ b"
  using assms
  by (metis less_le local.order_refl totalp totalp_on_def)

end

locale total_strict_order =
  restricted_total_strict_order where restriction = UNIV
begin

sublocale linorder "(≼)" "(≺)"
  using totalpD
  by unfold_locales fastforce

end

locale total_strict_order_restriction =
  strict_order_restriction +
  restricted_total_strict_order where restriction = "range lift" and less = "(≺)"
begin

sublocale restriction: total_strict_order "(≺⇩r)"
proof unfold_locales
  show "totalp (≺⇩r)"
    using totalp inj_lift
    unfolding R⇩r_def totalp_on_def inj_def
    by blast
qed

end

locale restricted_wellfounded_total_strict_order =
  restricted_wellfounded_strict_order + restricted_total_strict_order

end