Theory Ground_Ordering

theory Ground_Ordering
  imports
    Ground_Clause
    Transitive_Closure_Extra
    Clausal_Calculus_Extra
    Min_Max_Least_Greatest.Min_Max_Least_Greatest_Multiset
    Term_Ordering_Lifting
begin

locale ground_ordering = term_ordering_lifting less_trm
  for
    less_trm :: "'f gterm ⇒ 'f gterm ⇒ bool" (infix "≺⇩t" 50) +
  assumes
    wfP_less_trm[intro]: "wfP (≺⇩t)" and
    totalp_less_trm[intro]: "totalp (≺⇩t)" and
    less_trm_compatible_with_gctxt[simp]: "⋀ctxt t t'. t ≺⇩t t' ⟹ ctxt⟨t⟩⇩G ≺⇩t ctxt⟨t'⟩⇩G" and
    less_trm_if_subterm[simp]: "⋀t ctxt. ctxt ≠ □⇩G ⟹ t ≺⇩t ctxt⟨t⟩⇩G"
begin

abbreviation lesseq_trm (infix "≼⇩t" 50) where
  "lesseq_trm ≡ (≺⇩t)⇧=⇧="

lemma lesseq_trm_if_subtermeq: "t ≼⇩t ctxt⟨t⟩⇩G"
  using less_trm_if_subterm
  by (metis gctxt_ident_iff_eq_GHole reflclp_iff)

abbreviation lesseq_lit (infix "≼⇩l" 50) where
  "lesseq_lit ≡ (≺⇩l)⇧=⇧="

abbreviation lesseq_cls (infix "≼⇩c" 50) where
  "lesseq_cls ≡ (≺⇩c)⇧=⇧="

lemma wfP_less_lit[simp]: "wfp (≺⇩l)"
  unfolding less_lit_def
  using wfP_less_trm wfp_multp wfp_if_convertible_to_wfp by meson

lemma wfP_less_cls[simp]: "wfp (≺⇩c)"
  using wfP_less_lit wfp_multp less_cls_def by metis


sublocale term_order: linorder lesseq_trm less_trm
proof unfold_locales
  show "⋀x y. x ≼⇩t y ∨ y ≼⇩t x"
    by (metis reflclp_iff totalpD totalp_less_trm)
qed

sublocale literal_order: linorder lesseq_lit less_lit
proof unfold_locales
  have "totalp_on A (≺⇩l)" for A
  proof (rule totalp_onI)
    fix L1 L2 :: "'f gatom literal"
    assume "L1 ≠ L2"

    show "L1 ≺⇩l L2 ∨ L2 ≺⇩l L1"
      unfolding less_lit_def
    proof (rule totalp_multp[THEN totalpD])
      show "totalp (≺⇩t)"
        using totalp_less_trm .
    next
      show "transp (≺⇩t)"
        using transp_less_trm .
    next
      obtain x1 y1 x2 y2 :: "'f gterm" where
        "atm_of L1 = Upair x1 y1" and "atm_of L2 = Upair x2 y2"
        using uprod_exhaust by metis
      thus "mset_lit L1 ≠ mset_lit L2"
        using ‹L1 ≠ L2›
        by (cases L1; cases L2) (auto simp add: add_eq_conv_ex)
    qed
  qed
  thus "⋀x y. x ≼⇩l y ∨ y ≼⇩l x"
    by (metis reflclp_iff totalpD)
qed

sublocale clause_order: linorder lesseq_cls less_cls
proof unfold_locales
  show "⋀x y. x ≼⇩c y ∨ y ≼⇩c x"
    unfolding less_cls_def
    using totalp_multp[OF literal_order.totalp_on_less literal_order.transp_on_less]
    by (metis reflclp_iff totalpD)
qed

abbreviation is_maximal_lit :: "'f gatom literal ⇒ 'f gatom clause ⇒ bool" where
  "is_maximal_lit L M ≡ is_maximal_in_mset_wrt (≺⇩l) M L"

abbreviation is_strictly_maximal_lit :: "'f gatom literal ⇒ 'f gatom clause ⇒ bool" where
  "is_strictly_maximal_lit L M ≡ is_greatest_in_mset_wrt (≺⇩l) M L"

lemma less_trm_compatible_with_gctxt':
  assumes "ctxt⟨t⟩⇩G ≺⇩t ctxt⟨t'⟩⇩G"
  shows "t ≺⇩t t'"
proof(rule ccontr)
  assume "¬ t ≺⇩t t'"
  hence "t' ≼⇩t t"
    by order

  show False
  proof(cases "t' = t")
    case True
    then have "ctxt⟨t⟩⇩G = ctxt⟨t'⟩⇩G"
      by blast
    then show False
      using assms by order
  next
    case False
    then have "t' ≺⇩t t"
      using ‹t' ≼⇩t t› by order

    then have "ctxt⟨t'⟩⇩G ≺⇩t ctxt⟨t⟩⇩G"
      using less_trm_compatible_with_gctxt by metis
      
    then show ?thesis
      using assms by order
  qed
qed

lemma less_trm_compatible_with_gctxt_iff: "ctxt⟨t⟩⇩G ≺⇩t ctxt⟨t'⟩⇩G ⟷ t ≺⇩t t'"
  using less_trm_compatible_with_gctxt less_trm_compatible_with_gctxt' 
  by blast

lemma context_less_term_lesseq:
  assumes 
    "⋀t. ctxt⟨t⟩⇩G ≺⇩t ctxt'⟨t⟩⇩G"
    "t ≼⇩t t'"
  shows "ctxt⟨t⟩⇩G ≺⇩t ctxt'⟨t'⟩⇩G"
  using assms less_trm_compatible_with_gctxt
  by (metis reflclp_iff term_order.dual_order.strict_trans)

lemma context_lesseq_term_less:
  assumes 
    "⋀t. ctxt⟨t⟩⇩G ≼⇩t ctxt'⟨t⟩⇩G"
    "t ≺⇩t t'"
  shows "ctxt⟨t⟩⇩G ≺⇩t ctxt'⟨t'⟩⇩G"
  using assms less_trm_compatible_with_gctxt term_order.dual_order.strict_trans1 
  by blast

end

end