Theory Term_Ordering_Lifting

theory Term_Ordering_Lifting
  imports Clausal_Calculus_Extra
begin

lemma antisymp_on_reflclp_if_asymp_on:
  assumes "asymp_on A R"
  shows "antisymp_on A R⇧=⇧="
  unfolding antisym_on_reflcl[to_pred]
  using antisymp_on_if_asymp_on[OF ‹asymp_on A R›] .

lemma order_reflclp_if_transp_and_asymp:
  assumes "transp R" and "asymp R"
  shows "class.order R⇧=⇧= R"
proof unfold_locales
  show "⋀x y. R x y = (R⇧=⇧= x y ∧ ¬ R⇧=⇧= y x)"
    using ‹asymp R› asympD by fastforce
next
  show "⋀x. R⇧=⇧= x x"
    by simp
next
  show "⋀x y z. R⇧=⇧= x y ⟹ R⇧=⇧= y z ⟹ R⇧=⇧= x z"
    using transp_on_reflclp[OF ‹transp R›, THEN transpD] .
next
  show "⋀x y. R⇧=⇧= x y ⟹ R⇧=⇧= y x ⟹ x = y"
    using antisymp_on_reflclp_if_asymp_on[OF ‹asymp R›, THEN antisympD] .
qed

locale term_ordering_lifting =
  fixes
    less_trm :: "'t ⇒ 't ⇒ bool" (infix "≺⇩t" 50)
  assumes
    transp_less_trm[intro]: "transp (≺⇩t)" and
    asymp_less_trm[intro]: "asymp (≺⇩t)"
begin

definition less_lit :: "'t uprod literal ⇒ 't uprod literal ⇒ bool" (infix "≺⇩l" 50) where
  "less_lit L1 L2 ≡ multp (≺⇩t) (mset_lit L1) (mset_lit L2)"

definition less_cls :: "'t uprod clause ⇒ 't uprod clause ⇒ bool" (infix "≺⇩c" 50) where
  "less_cls ≡ multp (≺⇩l)"

sublocale term_order: order "(≺⇩t)⇧=⇧=" "(≺⇩t)"
  using order_reflclp_if_transp_and_asymp transp_less_trm asymp_less_trm by metis

sublocale literal_order: order "(≺⇩l)⇧=⇧=" "(≺⇩l)"
proof (rule order_reflclp_if_transp_and_asymp)
  show "transp (≺⇩l)"
    using transp_less_trm
    by (metis (opaque_lifting) less_lit_def transp_def transp_multp)
next
  show "asymp (≺⇩l)"
  by (metis asympD asymp_less_trm asymp_multp⇩H⇩O asympI less_lit_def multp_eq_multp⇩H⇩O
      transp_less_trm)
qed

sublocale clause_order: order "(≺⇩c)⇧=⇧=" "(≺⇩c)"
proof (rule order_reflclp_if_transp_and_asymp)
  show "transp (≺⇩c)"
    by (simp add: less_cls_def transp_multp)
next
  show "asymp (≺⇩c)"
    by (simp add: less_cls_def asymp_multp⇩H⇩O multp_eq_multp⇩H⇩O)
qed

end

end