Theory First_Order_Ordering

theory First_Order_Ordering
  imports 
    First_Order_Clause
    Ground_Ordering
    Relation_Extra
begin

context ground_ordering
begin

lemmas less⇩l⇩G_transitive_on = literal_order.transp_on_less
lemmas less⇩l⇩G_asymmetric_on = literal_order.asymp_on_less
lemmas less⇩l⇩G_total_on = literal_order.totalp_on_less

lemmas less⇩c⇩G_transitive_on = clause_order.transp_on_less
lemmas less⇩c⇩G_asymmetric_on = clause_order.asymp_on_less
lemmas less⇩c⇩G_total_on = clause_order.totalp_on_less

lemmas is_maximal_lit_def = is_maximal_in_mset_wrt_iff[OF less⇩l⇩G_transitive_on less⇩l⇩G_asymmetric_on]
lemmas is_strictly_maximal_lit_def = 
  is_strictly_maximal_in_mset_wrt_iff[OF less⇩l⇩G_transitive_on less⇩l⇩G_asymmetric_on]

end

section ‹First order ordering›

locale first_order_ordering = term_ordering_lifting less⇩t
  for
    less⇩t :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "≺⇩t" 50) +
  assumes
    less⇩t_total_on [intro]: "totalp_on {term. term.is_ground term} (≺⇩t)" and
    less⇩t_wellfounded_on: "wfp_on {term. term.is_ground term} (≺⇩t)" and    
    less⇩t_ground_context_compatible:
      "⋀context term⇩1 term⇩2. 
        term⇩1 ≺⇩t term⇩2 ⟹
        term.is_ground term⇩1 ⟹ 
        term.is_ground term⇩2 ⟹ 
        context.is_ground context ⟹
        context⟨term⇩1⟩ ≺⇩t context⟨term⇩2⟩" and
    less⇩t_ground_subst_stability: 
      "⋀term⇩1 term⇩2 (γ :: 'v ⇒ ('f, 'v) term). 
        term.is_ground (term⇩1 ⋅t γ) ⟹
        term.is_ground (term⇩2 ⋅t γ) ⟹
        term⇩1 ≺⇩t term⇩2 ⟹
        term⇩1 ⋅t γ ≺⇩t term⇩2 ⋅t γ" and
    less⇩t_ground_subterm_property: 
      "⋀term⇩G context⇩G.
         term.is_ground term⇩G ⟹
         context.is_ground context⇩G ⟹ 
         context⇩G ≠ □ ⟹ 
         term⇩G ≺⇩t context⇩G⟨term⇩G⟩"
begin

lemmas less⇩t_transitive = transp_less_trm 
lemmas less⇩t_asymmetric = asymp_less_trm


subsection ‹Definitions›

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

definition less⇩t⇩G :: "'f ground_term ⇒ 'f ground_term ⇒ bool" (infix "≺⇩t⇩G" 50) where
  "term⇩G⇩1 ≺⇩t⇩G term⇩G⇩2 ≡ term.from_ground term⇩G⇩1 ≺⇩t term.from_ground term⇩G⇩2"

notation less_lit (infix "≺⇩l" 50)
notation less_cls (infix "≺⇩c" 50)

lemma
  assumes
    L_in: "L ∈# C" and
    subst_stability: "⋀L K. L ≺⇩l K ⟹ (L ⋅l σ) ≺⇩l (K ⋅l σ)" and
    Lσ_max_in_Cσ: "literal_order.is_maximal_in_mset (C ⋅ σ) (L ⋅l σ)"
  shows "literal_order.is_maximal_in_mset C L"
proof -
  have Lσ_in: "L ⋅l σ ∈# C ⋅ σ" and Lσ_max: "∀y∈#C ⋅ σ. y ≠ L ⋅l σ ⟶ ¬ L ⋅l σ ≺⇩l y"
    using Lσ_max_in_Cσ
    unfolding atomize_conj literal_order.is_maximal_in_mset_iff
    by argo

  show "literal_order.is_maximal_in_mset C L"
    unfolding literal_order.is_maximal_in_mset_iff
  proof (intro conjI ballI impI)
    show "L ∈# C"
      using L_in .
  next
    show "⋀y. y ∈# C ⟹ y ≠ L ⟹ ¬ L ≺⇩l y"
      using subst_stability
      by (metis Lσ_max clause.subst_in_to_set_subst literal_order.order.strict_iff_order)
  qed
qed

lemmas less⇩l_def = less_lit_def
lemmas less⇩c_def = less_cls_def

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

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

abbreviation is_maximal⇩l :: 
  "('f, 'v) atom literal ⇒ ('f, 'v) atom clause ⇒ bool" where
  "is_maximal⇩l literal clause ≡ is_maximal_in_mset_wrt (≺⇩l) clause literal"

abbreviation is_strictly_maximal⇩l :: 
  "('f, 'v) atom literal ⇒ ('f, 'v) atom clause ⇒ bool" where
  "is_strictly_maximal⇩l literal clause ≡ is_strictly_maximal_in_mset_wrt (≺⇩l) clause literal"


subsection ‹Term ordering›

lemmas less⇩t_asymmetric_on = term_order.asymp_on_less
lemmas less⇩t_irreflexive_on = term_order.irreflp_on_less
lemmas less⇩t_transitive_on = term_order.transp_on_less

lemma less⇩t_wellfounded_on': "Wellfounded.wfp_on (term.from_ground ` terms⇩G) (≺⇩t)"
proof (rule Wellfounded.wfp_on_subset)
  show "Wellfounded.wfp_on {term. term.is_ground term} (≺⇩t)"
    using less⇩t_wellfounded_on .
next
  show "term.from_ground ` terms⇩G ⊆ {term. term.is_ground term}"
    by force
qed

lemma less⇩t_total_on': "totalp_on (term.from_ground ` terms⇩G) (≺⇩t)"
  using less⇩t_total_on
  by (simp add: totalp_on_def)

lemma less⇩t⇩G_wellfounded: "wfp (≺⇩t⇩G)"
proof -
  have "Wellfounded.wfp_on (range term.from_ground) (≺⇩t)"
    using less⇩t_wellfounded_on' by metis
  hence "wfp (λterm⇩G⇩1 term⇩G⇩2. term.from_ground term⇩G⇩1 ≺⇩t term.from_ground term⇩G⇩2)"
    unfolding Wellfounded.wfp_on_image[symmetric] .
  thus "wfp (≺⇩t⇩G)"
    unfolding less⇩t⇩G_def .
qed

subsection ‹Ground term ordering›

lemma less⇩t⇩G_asymmetric [intro]: "asymp (≺⇩t⇩G)"
  by (simp add: wfp_imp_asymp less⇩t⇩G_wellfounded)

lemmas less⇩t⇩G_asymmetric_on = less⇩t⇩G_asymmetric[THEN asymp_on_subset, OF subset_UNIV]

lemma less⇩t⇩G_transitive [intro]: "transp (≺⇩t⇩G)"
  using less⇩t⇩G_def less⇩t_transitive transpE transpI
  by (metis (full_types))

lemmas less⇩t⇩G_transitive_on = less⇩t⇩G_transitive[THEN transp_on_subset, OF subset_UNIV]

lemma less⇩t⇩G_total [intro]: "totalp (≺⇩t⇩G)"
  unfolding less⇩t⇩G_def
  using totalp_on_image[OF inj_term_of_gterm] less⇩t_total_on'
  by blast

lemmas less⇩t⇩G_total_on = less⇩t⇩G_total[THEN totalp_on_subset, OF subset_UNIV]

lemma less⇩t⇩G_context_compatible [simp]: 
  assumes "term⇩1 ≺⇩t⇩G term⇩2"  
  shows "context⟨term⇩1⟩⇩G ≺⇩t⇩G context⟨term⇩2⟩⇩G"
  using assms less⇩t_ground_context_compatible
  unfolding less⇩t⇩G_def
  by (metis context.ground_is_ground term.ground_is_ground ground_term_with_context(3)) 

lemma less⇩t⇩G_subterm_property [simp]: 
  assumes "context ≠ □⇩G" 
  shows "term ≺⇩t⇩G context⟨term⟩⇩G"
  using 
    assms
    less⇩t_ground_subterm_property[OF term.ground_is_ground context.ground_is_ground] 
    context_from_ground_hole
  unfolding less⇩t⇩G_def ground_term_with_context(3)  
  by blast

lemma less⇩t_less⇩t⇩G [clause_simp]: 
  assumes "term.is_ground term⇩1" and "term.is_ground term⇩2"
  shows "term⇩1 ≺⇩t term⇩2 ⟷ term.to_ground term⇩1 ≺⇩t⇩G term.to_ground term⇩2"
  by (simp add: assms less⇩t⇩G_def)

lemma less_eq⇩t_ground_subst_stability:
  assumes "term.is_ground (term⇩1 ⋅t γ)" "term.is_ground (term⇩2 ⋅t γ)"  "term⇩1 ≼⇩t term⇩2"
  shows "term⇩1 ⋅t γ ≼⇩t term⇩2 ⋅t γ"
  using less⇩t_ground_subst_stability[OF assms(1, 2)] assms(3)
  by auto

subsection ‹Literal ordering›

lemmas less⇩l_asymmetric [intro] = literal_order.asymp_on_less[of UNIV]
lemmas less⇩l_asymmetric_on [intro] = literal_order.asymp_on_less

lemmas less⇩l_transitive [intro] = literal_order.transp_on_less[of UNIV]
lemmas less⇩l_transitive_on = literal_order.transp_on_less
                                                            
lemmas is_maximal⇩l_def = is_maximal_in_mset_wrt_iff[OF less⇩l_transitive_on less⇩l_asymmetric_on]

lemmas is_strictly_maximal⇩l_def =
  is_strictly_maximal_in_mset_wrt_iff[OF less⇩l_transitive_on less⇩l_asymmetric_on]

lemmas is_maximal⇩l_if_is_strictly_maximal⇩l =
  is_maximal_in_mset_wrt_if_is_strictly_maximal_in_mset_wrt[OF 
    less⇩l_transitive_on less⇩l_asymmetric_on
  ]

lemma less⇩l_ground_subst_stability: 
  assumes 
    "literal.is_ground (literal ⋅l γ)" 
    "literal.is_ground (literal' ⋅l γ)" 
  shows "literal ≺⇩l literal' ⟹ literal ⋅l γ ≺⇩l literal' ⋅l γ"
  unfolding less⇩l_def mset_mset_lit_subst[symmetric]
proof (elim multp_map_strong[rotated -1])
  show "monotone_on (set_mset (mset_lit literal + mset_lit literal')) (≺⇩t) (≺⇩t) (λterm. term ⋅t γ)"
    by (rule monotone_onI)
      (metis assms(1,2) less⇩t_ground_subst_stability ground_term_in_ground_literal_subst union_iff)
qed (use less⇩t_asymmetric less⇩t_transitive in simp_all)

lemma maximal⇩l_in_clause:
  assumes "is_maximal⇩l literal clause"
  shows "literal ∈# clause"
  using assms 
  unfolding is_maximal⇩l_def
  by(rule conjunct1)

lemma strictly_maximal⇩l_in_clause:
  assumes "is_strictly_maximal⇩l literal clause"
  shows "literal ∈# clause"
  using assms 
  unfolding is_strictly_maximal⇩l_def
  by(rule conjunct1)

subsection ‹Clause ordering›

lemmas less⇩c_asymmetric [intro] = clause_order.asymp_on_less[of UNIV]
lemmas less⇩c_asymmetric_on [intro] = clause_order.asymp_on_less
lemmas less⇩c_transitive [intro] = clause_order.transp_on_less[of UNIV]
lemmas less⇩c_transitive_on [intro] = clause_order.transp_on_less

lemma less⇩c_ground_subst_stability: 
  assumes 
    "clause.is_ground (clause ⋅ γ)" 
    "clause.is_ground (clause' ⋅ γ)" 
  shows "clause ≺⇩c clause' ⟹ clause ⋅ γ ≺⇩c clause' ⋅ γ"
  unfolding clause.subst_def less⇩c_def
proof (elim multp_map_strong[rotated -1])
  show "monotone_on (set_mset (clause + clause')) (≺⇩l) (≺⇩l) (λliteral. literal ⋅l γ)"
    by (rule monotone_onI)
      (metis assms(1,2) clause.to_set_is_ground_subst less⇩l_ground_subst_stability union_iff)
qed (use less⇩l_asymmetric less⇩l_transitive in simp_all)

subsection ‹Grounding›

sublocale ground: ground_ordering "(≺⇩t⇩G)" 
  apply unfold_locales
  by(simp_all add: less⇩t⇩G_transitive less⇩t⇩G_asymmetric less⇩t⇩G_wellfounded less⇩t⇩G_total)

notation ground.less_lit (infix "≺⇩l⇩G" 50)
notation ground.less_cls (infix "≺⇩c⇩G" 50)

notation ground.lesseq_trm (infix "≼⇩t⇩G" 50)
notation ground.lesseq_lit (infix "≼⇩l⇩G" 50)
notation ground.lesseq_cls (infix "≼⇩c⇩G" 50)

lemma not_less_eq⇩t⇩G: "¬ term⇩G⇩2 ≼⇩t⇩G term⇩G⇩1 ⟷ term⇩G⇩1 ≺⇩t⇩G term⇩G⇩2"
  using ground.term_order.not_le .

lemma less_eq⇩t_less_eq⇩t⇩G:
  assumes "term.is_ground term⇩1" and "term.is_ground term⇩2" 
  shows "term⇩1 ≼⇩t term⇩2 ⟷ term.to_ground term⇩1 ≼⇩t⇩G term.to_ground term⇩2"
  unfolding reflclp_iff less⇩t_less⇩t⇩G[OF assms]
  using assms[THEN term.to_ground_inverse]
  by auto

lemma less_eq⇩t⇩G_less_eq⇩t:
   "term⇩G⇩1 ≼⇩t⇩G term⇩G⇩2 ⟷ term.from_ground term⇩G⇩1 ≼⇩t term.from_ground term⇩G⇩2"
  unfolding 
    less_eq⇩t_less_eq⇩t⇩G[OF term.ground_is_ground term.ground_is_ground] 
    term.from_ground_inverse
  ..

lemma not_less_eq⇩t: 
  assumes "term.is_ground term⇩1" and "term.is_ground term⇩2"
  shows "¬ term⇩2 ≼⇩t term⇩1 ⟷ term⇩1 ≺⇩t term⇩2"
  unfolding less⇩t_less⇩t⇩G[OF assms] less_eq⇩t_less_eq⇩t⇩G[OF assms(2, 1)] not_less_eq⇩t⇩G
  ..

lemma less⇩l⇩G_less⇩l: 
  "literal⇩G⇩1 ≺⇩l⇩G literal⇩G⇩2 ⟷ literal.from_ground literal⇩G⇩1 ≺⇩l literal.from_ground literal⇩G⇩2"
  unfolding less⇩l_def ground.less_lit_def less⇩t⇩G_def mset_literal_from_ground
  using
     multp_image_mset_image_msetI[OF _ less⇩t_transitive]
     multp_image_mset_image_msetD[OF _ less⇩t_transitive_on term.inj_from_ground]
   by blast

lemma less⇩l_less⇩l⇩G: 
  assumes "literal.is_ground literal⇩1" "literal.is_ground literal⇩2" 
  shows "literal⇩1 ≺⇩l literal⇩2 ⟷ literal.to_ground literal⇩1 ≺⇩l⇩G literal.to_ground literal⇩2"
  using assms
  by (simp add: less⇩l⇩G_less⇩l)

lemma less_eq⇩l_less_eq⇩l⇩G:
  assumes "literal.is_ground literal⇩1" and "literal.is_ground literal⇩2" 
  shows "literal⇩1 ≼⇩l literal⇩2 ⟷ literal.to_ground literal⇩1 ≼⇩l⇩G literal.to_ground literal⇩2"
  unfolding reflclp_iff less⇩l_less⇩l⇩G[OF assms]
  using assms[THEN literal.to_ground_inverse]
  by auto

lemma less_eq⇩l⇩G_less_eq⇩l:
   "literal⇩G⇩1 ≼⇩l⇩G literal⇩G⇩2 ⟷ literal.from_ground literal⇩G⇩1 ≼⇩l literal.from_ground literal⇩G⇩2"
  unfolding 
    less_eq⇩l_less_eq⇩l⇩G[OF literal.ground_is_ground literal.ground_is_ground] 
    literal.from_ground_inverse
  ..

lemma maximal_lit_in_clause:
  assumes "ground.is_maximal_lit literal⇩G clause⇩G"
  shows "literal⇩G ∈# clause⇩G"
  using assms 
  unfolding ground.is_maximal_lit_def
  by(rule conjunct1)

lemma is_maximal⇩l_empty [simp]: 
  assumes "is_maximal⇩l literal {#}"  
  shows False
  using assms maximal⇩l_in_clause
  by fastforce

lemma is_strictly_maximal⇩l_empty [simp]: 
  assumes "is_strictly_maximal⇩l literal {#}"  
  shows False
  using assms strictly_maximal⇩l_in_clause
  by fastforce

lemma is_maximal_lit_iff_is_maximal⇩l: 
  "ground.is_maximal_lit literal⇩G clause⇩G ⟷ 
    is_maximal⇩l (literal.from_ground literal⇩G) (clause.from_ground clause⇩G)"
   unfolding 
    is_maximal⇩l_def
    ground.is_maximal_lit_def
    clause.ground_sub_in_ground[symmetric]
   using 
     less⇩l_less⇩l⇩G[OF literal.ground_is_ground clause.sub_in_ground_is_ground] 
     clause.sub_in_ground_is_ground
     clause.ground_sub_in_ground
   by (metis literal.to_ground_inverse literal.from_ground_inverse)

lemma is_strictly_maximal⇩G⇩l_iff_is_strictly_maximal⇩l:
  "ground.is_strictly_maximal_lit literal⇩G clause⇩G 
    ⟷ is_strictly_maximal⇩l (literal.from_ground literal⇩G) (clause.from_ground clause⇩G)"
  unfolding 
    is_strictly_maximal_in_mset_wrt_iff_is_greatest_in_mset_wrt[OF 
      ground.less⇩l⇩G_transitive_on ground.less⇩l⇩G_asymmetric_on ground.less⇩l⇩G_total_on, symmetric
    ]
    ground.is_strictly_maximal_lit_def
    is_strictly_maximal⇩l_def
    clause.ground_sub_in_ground[symmetric]
    remove1_mset_literal_from_ground
    clause.ground_sub
    less_eq⇩l⇩G_less_eq⇩l
  ..
 
lemma not_less_eq⇩l⇩G: "¬ literal⇩G⇩2 ≼⇩l⇩G literal⇩G⇩1 ⟷ literal⇩G⇩1 ≺⇩l⇩G literal⇩G⇩2"
  using asympD[OF ground.less⇩l⇩G_asymmetric_on] totalpD[OF ground.less⇩l⇩G_total_on]
  by blast

lemma not_less_eq⇩l: 
  assumes "literal.is_ground literal⇩1" and "literal.is_ground literal⇩2"
  shows "¬ literal⇩2 ≼⇩l literal⇩1 ⟷ literal⇩1 ≺⇩l literal⇩2"
  unfolding less⇩l_less⇩l⇩G[OF assms] less_eq⇩l_less_eq⇩l⇩G[OF assms(2, 1)] not_less_eq⇩l⇩G
  ..

lemma less⇩c⇩G_less⇩c: 
  "clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2 ⟷ clause.from_ground clause⇩G⇩1 ≺⇩c clause.from_ground clause⇩G⇩2"
proof (rule iffI)
  show "clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2 ⟹ clause.from_ground clause⇩G⇩1 ≺⇩c clause.from_ground clause⇩G⇩2"
    unfolding less⇩c_def
    by (auto simp: clause.from_ground_def ground.less_cls_def less⇩l⇩G_less⇩l
        intro!: multp_image_mset_image_msetI elim: multp_mono_strong)
next
  have "transp (λx y. literal.from_ground x ≺⇩l literal.from_ground y)"
    by (metis (no_types, lifting) literal_order.less_trans transpI)
  thus "clause.from_ground clause⇩G⇩1 ≺⇩c clause.from_ground clause⇩G⇩2 ⟹ clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2"
    unfolding ground.less_cls_def clause.from_ground_def less⇩c_def
    by (auto simp: less⇩l⇩G_less⇩l
        dest!: multp_image_mset_image_msetD[OF _ less⇩l_transitive literal.inj_from_ground]
        elim!: multp_mono_strong)
qed

lemma less⇩c_less⇩c⇩G: 
  assumes "clause.is_ground clause⇩1" "clause.is_ground clause⇩2"
  shows "clause⇩1 ≺⇩c clause⇩2 ⟷ clause.to_ground clause⇩1 ≺⇩c⇩G  clause.to_ground clause⇩2"
  using assms
  by (simp add: less⇩c⇩G_less⇩c)

lemma less_eq⇩c_less_eq⇩c⇩G:
  assumes "clause.is_ground clause⇩1" and "clause.is_ground clause⇩2" 
  shows "clause⇩1 ≼⇩c clause⇩2 ⟷ clause.to_ground clause⇩1 ≼⇩c⇩G clause.to_ground clause⇩2"
  unfolding reflclp_iff less⇩c_less⇩c⇩G[OF assms]
  using assms[THEN clause.to_ground_inverse]
  by fastforce

lemma less_eq⇩c⇩G_less_eq⇩c:
   "clause⇩G⇩1 ≼⇩c⇩G clause⇩G⇩2 ⟷ clause.from_ground clause⇩G⇩1 ≼⇩c clause.from_ground clause⇩G⇩2"
  unfolding 
    less_eq⇩c_less_eq⇩c⇩G[OF clause.ground_is_ground clause.ground_is_ground] 
    clause.from_ground_inverse
  ..

lemma not_less_eq⇩c⇩G: "¬ clause⇩G⇩2 ≼⇩c⇩G clause⇩G⇩1 ⟷ clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2"
  using asympD[OF ground.less⇩c⇩G_asymmetric_on] totalpD[OF ground.less⇩c⇩G_total_on]
  by blast

lemma not_less_eq⇩c: 
  assumes "clause.is_ground clause⇩1" and "clause.is_ground clause⇩2"
  shows "¬ clause⇩2 ≼⇩c clause⇩1 ⟷ clause⇩1 ≺⇩c clause⇩2"
  unfolding less⇩c_less⇩c⇩G[OF assms] less_eq⇩c_less_eq⇩c⇩G[OF assms(2, 1)] not_less_eq⇩c⇩G
  ..

lemma less⇩t_ground_context_compatible':
  assumes 
    "context.is_ground context" 
    "term.is_ground term" 
    "term.is_ground term'" 
    "context⟨term⟩ ≺⇩t context⟨term'⟩"
  shows "term ≺⇩t term'"
  using assms 
  by (metis less⇩t_ground_context_compatible not_less_eq⇩t term_order.dual_order.asym 
        term_order.order.not_eq_order_implies_strict)
  

lemma less⇩t_ground_context_compatible_iff:
   assumes 
    "context.is_ground context" 
    "term.is_ground term" 
    "term.is_ground term'" 
  shows "context⟨term⟩ ≺⇩t context⟨term'⟩ ⟷ term ≺⇩t term'"
  using assms less⇩t_ground_context_compatible less⇩t_ground_context_compatible'
  by blast

subsection ‹Stability under ground substitution›

lemma less⇩t_less_eq⇩t_ground_subst_stability:
  assumes 
    "term.is_ground (term⇩1 ⋅t γ)"
    "term.is_ground (term⇩2 ⋅t γ)"
    "term⇩1 ⋅t γ ≺⇩t term⇩2 ⋅t γ"
  shows
    "¬ term⇩2 ≼⇩t term⇩1"
proof
  assume assumption: "term⇩2 ≼⇩t term⇩1"

  have "term⇩2 ⋅t γ ≼⇩t term⇩1 ⋅t γ"
    using less_eq⇩t_ground_subst_stability[OF 
            assms(2, 1)
            assumption
           ].

  then show False 
    using assms(3) by order
qed

lemma less_eq⇩l_ground_subst_stability:
  assumes   
    "literal.is_ground (literal⇩1 ⋅l γ)" 
    "literal.is_ground (literal⇩2 ⋅l γ)"  
    "literal⇩1 ≼⇩l literal⇩2"
  shows "literal⇩1 ⋅l γ ≼⇩l literal⇩2 ⋅l γ"
  using less⇩l_ground_subst_stability[OF assms(1, 2)] assms(3)
  by auto

lemma less⇩l_less_eq⇩l_ground_subst_stability: assumes 
  "literal.is_ground (literal⇩1 ⋅l γ)"
  "literal.is_ground (literal⇩2 ⋅l γ)"
  "literal⇩1 ⋅l γ ≺⇩l literal⇩2 ⋅l γ"
shows
  "¬ literal⇩2 ≼⇩l literal⇩1"
  by (meson assms less_eq⇩l_ground_subst_stability not_less_eq⇩l)

lemma less_eq⇩c_ground_subst_stability:
  assumes   
    "clause.is_ground (clause⇩1 ⋅ γ)" 
    "clause.is_ground (clause⇩2 ⋅ γ)"  
    "clause⇩1 ≼⇩c clause⇩2"
  shows "clause⇩1 ⋅ γ ≼⇩c clause⇩2 ⋅ γ"
  using less⇩c_ground_subst_stability[OF assms(1, 2)] assms(3)
  by auto

lemma less⇩c_less_eq⇩c_ground_subst_stability: assumes 
  "clause.is_ground (clause⇩1 ⋅ γ)"
  "clause.is_ground (clause⇩2 ⋅ γ)"
  "clause⇩1 ⋅ γ ≺⇩c clause⇩2 ⋅ γ"
shows
  "¬ clause⇩2 ≼⇩c clause⇩1"
  by (meson assms less_eq⇩c_ground_subst_stability not_less_eq⇩c)
  
lemma is_maximal⇩l_ground_subst_stability:
  assumes 
    clause_not_empty: "clause ≠ {#}" and
    clause_grounding: "clause.is_ground (clause ⋅ γ)" 
  obtains literal
  where "is_maximal⇩l literal clause" "is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
proof-
  assume assumption: 
    "⋀literal. is_maximal⇩l literal clause ⟹ is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ) ⟹ thesis"

  from clause_not_empty 
  have clause_grounding_not_empty: "clause ⋅ γ ≠ {#}"
    unfolding clause.subst_def
    by simp

  obtain literal where 
    literal: "literal ∈# clause" and
    literal_grounding_is_maximal: "is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)" 
    using
      ex_maximal_in_mset_wrt[OF less⇩l_transitive_on less⇩l_asymmetric_on clause_grounding_not_empty]  
      maximal⇩l_in_clause
    unfolding clause.subst_def
    by force

  from literal_grounding_is_maximal
  have no_bigger_than_literal: 
    "∀literal' ∈# clause ⋅ γ. literal' ≠ literal ⋅l γ ⟶ ¬ literal ⋅l γ ≺⇩l literal'"
    unfolding is_maximal⇩l_def
    by simp

  show ?thesis
  proof(cases "is_maximal⇩l literal clause")
    case True
    with literal_grounding_is_maximal assumption show ?thesis
      by blast
  next
    case False
    then obtain literal' where 
      literal': "literal' ∈# clause" "literal ≺⇩l literal'" 
      unfolding is_maximal⇩l_def
      using literal
      by blast 

    note literals_in_clause = literal(1) literal'(1)
    note literals_grounding = literals_in_clause[THEN 
         clause.to_set_is_ground_subst[OF _ clause_grounding]
      ]

    have "literal ⋅l γ ≺⇩l literal' ⋅l γ"
      using less⇩l_ground_subst_stability[OF literals_grounding literal'(2)].
   
    then have False
     using 
       no_bigger_than_literal
       clause.subst_in_to_set_subst[OF literal'(1)] 
     by (metis asymp_onD less⇩l_asymmetric_on)
       
    then show ?thesis..
  qed
qed

lemma is_maximal⇩l_ground_subst_stability':
  assumes 
   "literal ∈# clause"
   "clause.is_ground (clause ⋅ γ)"
   "is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
 shows 
   "is_maximal⇩l literal clause"
proof(rule ccontr)
  assume "¬ is_maximal⇩l literal clause"
  
  then obtain literal' where literal':
      "literal ≺⇩l literal'" 
      "literal' ∈# clause "
  using assms(1)
  unfolding is_maximal⇩l_def
  by blast

  then have literal'_grounding: "literal.is_ground (literal' ⋅l γ)"
    using assms(2) clause.to_set_is_ground_subst by blast

  have literal_grounding: "literal.is_ground (literal ⋅l γ)"
    using assms(1) assms(2) clause.to_set_is_ground_subst by blast

  have literal_γ_in_premise: "literal' ⋅l γ ∈# clause ⋅ γ"
    using clause.subst_in_to_set_subst[OF literal'(2)]
    by simp
     
  have "literal ⋅l γ ≺⇩l literal' ⋅l γ"
    using less⇩l_ground_subst_stability[OF literal_grounding literal'_grounding literal'(1)].
  
  then have "¬ is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
    using literal_γ_in_premise 
    unfolding is_maximal⇩l_def literal.subst_comp_subst
    by (metis asympD less⇩l_asymmetric)
  
  then show False
    using assms(3)
    by blast
qed

lemma less⇩l_total_on [intro]: "totalp_on (literal.from_ground ` literals⇩G) (≺⇩l)"
  by (smt (verit, best) image_iff less⇩l⇩G_less⇩l totalpD ground.less⇩l⇩G_total_on totalp_on_def)

lemmas less⇩l_total_on_set_mset =
  less⇩l_total_on[THEN totalp_on_subset, OF clause.to_set_from_ground[THEN equalityD1]]

lemma less⇩c_total_on: "totalp_on (clause.from_ground ` clauses) (≺⇩c)"
  by (smt ground.clause_order.totalp_on_less image_iff less⇩c⇩G_less⇩c totalpD totalp_onI)

lemma unique_maximal_in_ground_clause:
  assumes
    "clause.is_ground clause" 
    "is_maximal⇩l literal clause"
    "is_maximal⇩l literal' clause"
  shows
    "literal = literal'"
  using assms(2, 3)
  unfolding is_maximal⇩l_def
  by (metis assms(1) less⇩l_total_on_set_mset clause.to_ground_inverse totalp_onD)

lemma unique_strictly_maximal_in_ground_clause:
  assumes
    "clause.is_ground clause" 
    "is_strictly_maximal⇩l literal clause"
    "is_strictly_maximal⇩l literal' clause"
  shows
    "literal = literal'"
proof-
  note are_maximal⇩l = assms(2, 3)[THEN is_maximal⇩l_if_is_strictly_maximal⇩l]
   
  show ?thesis
    using unique_maximal_in_ground_clause[OF assms(1) are_maximal⇩l].
qed

lemma is_strictly_maximal⇩l_ground_subst_stability:
  assumes 
   clause_grounding: "clause.is_ground (clause ⋅ γ)" and
   ground_strictly_maximal: "is_strictly_maximal⇩l literal⇩G (clause ⋅ γ)"
 obtains literal where 
   "is_strictly_maximal⇩l literal clause" "literal ⋅l γ = literal⇩G"
proof-
  assume assumption: "⋀literal. 
    is_strictly_maximal⇩l literal clause ⟹ literal ⋅l γ = literal⇩G ⟹ thesis"

  have clause_grounding_not_empty: "clause ⋅ γ ≠ {#}"
    using ground_strictly_maximal
    unfolding is_strictly_maximal⇩l_def
    by fastforce

  have literal⇩G_in_clause_grounding: "literal⇩G ∈# clause ⋅ γ"
    using ground_strictly_maximal is_strictly_maximal⇩l_def by blast

  obtain literal where literal: "literal ∈# clause" "literal ⋅l γ = literal⇩G"
    by (smt (verit, best) clause.subst_def imageE literal⇩G_in_clause_grounding multiset.set_map)

  show ?thesis
  proof(cases "is_strictly_maximal⇩l literal clause")
    case True
    then show ?thesis
      using assumption
      using literal(2) by blast
  next
    case False

    then obtain literal' where literal': 
      "literal' ∈# clause - {# literal #}"  
      "literal ≼⇩l literal'" 
      unfolding is_strictly_maximal⇩l_def
      using literal(1)
      by blast 

    note literal_grounding = 
       clause.to_set_is_ground_subst[OF literal(1) clause_grounding]

    have literal'_grounding: "literal.is_ground (literal' ⋅l γ)"
      using literal'(1) clause_grounding
      by (meson clause.to_set_is_ground_subst in_diffD)

    have "literal ⋅l γ ≼⇩l literal' ⋅l γ"
      using less_eq⇩l_ground_subst_stability[OF literal_grounding literal'_grounding literal'(2)].

    then have False
      using  clause.subst_in_to_set_subst[OF literal'(1)]  ground_strictly_maximal 
      unfolding 
        is_strictly_maximal⇩l_def 
        literal(2)[symmetric]
        subst_clause_remove1_mset[OF literal(1)]
      by blast
   
    then show ?thesis..
  qed
qed

lemma is_strictly_maximal⇩l_ground_subst_stability':
  assumes 
   "literal ∈# clause"
   "clause.is_ground (clause ⋅ γ)"
   "is_strictly_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
 shows 
   "is_strictly_maximal⇩l literal clause"
  using 
    is_maximal⇩l_ground_subst_stability'[OF 
      assms(1,2) 
      is_maximal⇩l_if_is_strictly_maximal⇩l[OF assms(3)]
    ]
    assms(3)
  unfolding 
    is_strictly_maximal⇩l_def is_maximal⇩l_def
    subst_clause_remove1_mset[OF assms(1), symmetric]
  by (metis in_diffD clause.subst_in_to_set_subst reflclp_iff)

lemma less⇩t_less⇩l: 
  assumes "term⇩1 ≺⇩t term⇩2"
  shows 
    "term⇩1 ≈ term⇩3 ≺⇩l term⇩2 ≈ term⇩3"
    "term⇩1 !≈ term⇩3 ≺⇩l term⇩2 !≈ term⇩3"
  using assms
  unfolding less⇩l_def multp_eq_multp⇩H⇩O[OF less⇩t_asymmetric less⇩t_transitive] multp⇩H⇩O_def 
  by (auto simp: add_mset_eq_add_mset)

lemma less⇩t_less⇩l':
  assumes 
    "∀term ∈ set_uprod (atm_of literal). term ⋅t σ' ≼⇩t term ⋅t σ"
    "∃term ∈ set_uprod (atm_of literal). term ⋅t σ' ≺⇩t term ⋅t σ"
  shows "literal ⋅l σ' ≺⇩l literal ⋅l σ"
proof(cases literal)
  case (Pos atom)
  show ?thesis
  proof(cases atom)
    case (Upair term⇩1 term⇩2)
    have "term⇩2 ⋅t σ' ≺⇩t term⇩2 ⋅t σ ⟹ 
          multp (≺⇩t) {#term⇩1 ⋅t σ, term⇩2 ⋅t σ'#} {#term⇩1 ⋅t σ, term⇩2 ⋅t σ#}"
      using multp_add_mset'[of "(≺⇩t)" "term⇩2 ⋅t σ'"  "term⇩2 ⋅t σ" "{#term⇩1 ⋅t σ#}"] add_mset_commute
      by metis

    then show ?thesis 
      using assms
      unfolding less⇩l_def Pos subst_literal(1) Upair subst_atom
      by (auto simp: multp_add_mset multp_add_mset')
  qed
next
  case (Neg atom)
  show ?thesis
   proof(cases atom)
     case (Upair term⇩1 term⇩2)
     have "term⇩2 ⋅t σ' ≺⇩t term⇩2 ⋅t σ ⟹ 
            multp (≺⇩t) 
              {#term⇩1 ⋅t σ, term⇩1 ⋅t σ, term⇩2 ⋅t σ', term⇩2 ⋅t σ'#} 
              {#term⇩1 ⋅t σ, term⇩1 ⋅t σ, term⇩2 ⋅t σ, term⇩2 ⋅t σ#}"
       using multp_add_mset' multp_add_same[OF less⇩t_asymmetric less⇩t_transitive]
       by simp

     then show ?thesis 
      using assms
      unfolding less⇩l_def Neg subst_literal(2) Upair subst_atom
      by (auto simp: multp_add_mset multp_add_mset' add_mset_commute)
  qed
qed

lemmas less⇩c_add_mset = multp_add_mset_reflclp[OF less⇩l_asymmetric less⇩l_transitive, folded less⇩c_def] 

lemmas less⇩c_add_same = multp_add_same[OF less⇩l_asymmetric less⇩l_transitive, folded less⇩c_def]

lemma less_eq⇩l_less_eq⇩c:
  assumes "∀literal ∈# clause. literal ⋅l σ' ≼⇩l literal ⋅l σ"
  shows "clause ⋅ σ' ≼⇩c clause ⋅ σ"
  using assms 
  by(induction clause)(clause_auto simp: less⇩c_add_same less⇩c_add_mset)
   
lemma less⇩l_less⇩c:
  assumes 
    "∀literal ∈# clause. literal ⋅l σ' ≼⇩l literal ⋅l σ"
    "∃literal ∈# clause. literal ⋅l σ' ≺⇩l literal ⋅l σ"
  shows "clause ⋅ σ' ≺⇩c clause ⋅ σ"
  using assms
proof(induction clause)
  case empty
  then show ?case by auto
next
  case (add literal clause)
  then have less_eq: "∀literal ∈# clause. literal ⋅l σ' ≼⇩l literal ⋅l σ"
    by (metis add_mset_remove_trivial in_diffD)

  show ?case 
  proof(cases "literal ⋅l σ' ≺⇩l literal ⋅l σ")
    case True
    moreover have "clause ⋅ σ' ≼⇩c clause ⋅ σ"
      using less_eq⇩l_less_eq⇩c[OF less_eq].

    ultimately show ?thesis
      using less⇩c_add_mset
      unfolding subst_clause_add_mset less⇩c_def
      by blast
  next
    case False
    then have less: "∃literal ∈# clause. literal ⋅l σ' ≺⇩l literal ⋅l σ"
      using add.prems(2) by auto

   from False have eq: "literal ⋅l σ' = literal ⋅l σ"
      using add.prems(1) by force

   show ?thesis
     using add(1)[OF less_eq less] less⇩c_add_same
     unfolding subst_clause_add_mset eq less⇩c_def
     by blast
  qed
qed

subsection ‹Substitution update›

lemma less⇩t_subst_upd:
  fixes γ :: "('f, 'v) subst"
  assumes 
    update_is_ground: "term.is_ground update" and
    update_less: "update ≺⇩t γ var" and
    term_grounding: "term.is_ground (term ⋅t γ)" and
    var: "var ∈ term.vars term"
  shows "term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
  using assms(3, 4)
proof(induction "term")
  case Var
  then show ?case 
    using update_is_ground update_less
    by simp
next
  case (Fun f terms)

  then have "∀term ∈ set terms. term ⋅t γ(var := update) ≼⇩t term ⋅t γ"
    by (metis eval_with_fresh_var is_ground_iff reflclp_iff term.set_intros(4))

  moreover then have "∃term ∈ set terms. term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
    using Fun assms(2)
    by (metis (full_types) fun_upd_same  term.distinct(1) term.sel(4) term.set_cases(2) 
          term_order.dual_order.strict_iff_order term_subst_eq_rev)

  ultimately show ?case
    using Fun(2, 3)
  proof(induction "filter (λterm. term ⋅t γ(var := update) ≺⇩t term ⋅t γ) terms" 
          arbitrary: terms)
    case Nil
    then show ?case
      unfolding empty_filter_conv
      by blast
  next
    case first: (Cons t ts)

    have update_grounding [simp]: "term.is_ground (t ⋅t γ(var := update))"
      using first.prems(3) update_is_ground first.hyps(2)
      by (metis (no_types, lifting) filter_eq_ConsD fun_upd_other fun_upd_same in_set_conv_decomp 
            is_ground_iff term.set_intros(4))

    then have t_grounding [simp]: "term.is_ground (t ⋅t γ)"
      using update_grounding Fun.prems(1,2)
      by (metis fun_upd_other is_ground_iff)
    
    show ?case
    proof(cases ts)
      case Nil
      then obtain ss1 ss2 where terms: "terms = ss1 @ t # ss2"
        using filter_eq_ConsD[OF first.hyps(2)[symmetric]]
        by blast

      have ss1: "∀term ∈ set ss1. term ⋅t γ(var := update) = term ⋅t γ"
        using first.hyps(2) first.prems(1) 
        unfolding Nil terms
        by (smt (verit, del_insts) Un_iff append_Cons_eq_iff filter_empty_conv filter_eq_ConsD 
              set_append term_order.antisym_conv2)

      have ss2: "∀term ∈ set ss2. term ⋅t γ(var := update) = term ⋅t γ"
        using first.hyps(2) first.prems(1) 
        unfolding Nil terms
        by (smt (verit, ccfv_SIG) Un_iff append_Cons_eq_iff filter_empty_conv filter_eq_ConsD 
              list.set_intros(2) set_append term_order.antisym_conv2)

      let ?context = "More f (map (λterm. (term ⋅t γ)) ss1) □ (map (λterm. (term ⋅t γ)) ss2)"

      have 1: "term.is_ground (t ⋅t γ)"
        using terms first(5)
        by auto

      moreover then have "term.is_ground (t ⋅t γ(var := update))"
        by (metis assms(1) fun_upd_other fun_upd_same is_ground_iff)

      moreover have "context.is_ground ?context"
        using terms first(5)
        by auto

      moreover have "t ⋅t γ(var := update) ≺⇩t t ⋅t γ" 
        using first.hyps(2)
        by (meson Cons_eq_filterD)

      ultimately have "?context⟨t ⋅t γ(var := update)⟩ ≺⇩t ?context⟨t ⋅t γ⟩"
        using less⇩t_ground_context_compatible
        by blast

      moreover have "Fun f terms ⋅t γ(var := update) = ?context⟨t ⋅t γ(var := update)⟩"
        unfolding terms
        using ss1 ss2
        by simp

      moreover have "Fun f terms ⋅t γ = ?context⟨t ⋅t γ⟩"
        unfolding terms
        by auto

      ultimately show ?thesis
        by argo
    next
      case (Cons t' ts')

      from first(2) 
      obtain ss1 ss2 where
        terms: "terms = ss1 @ t # ss2" and
        ss1: "∀s∈set ss1. ¬ s ⋅t γ(var := update) ≺⇩t s ⋅t γ" and
        less: "t ⋅t γ(var := update) ≺⇩t t ⋅t γ" and 
        ts: "ts = filter (λterm. term ⋅t γ(var := update)≺⇩t term ⋅t γ) ss2"
        using Cons_eq_filter_iff[of t ts "(λterm. term ⋅t γ(var := update) ≺⇩t term ⋅t γ)"]
        by blast

      let ?terms' = "ss1 @ (t ⋅t γ(var := update))  # ss2"

      have [simp]: "t ⋅t γ(var := update) ⋅t γ = t ⋅t γ(var := update)"
        using first.prems(3) update_is_ground
        unfolding terms
        by (simp add: is_ground_iff)

      have [simp]: "t ⋅t γ(var := update) ⋅t γ(var := update) = t ⋅t γ(var := update)"
        using first.prems(3) update_is_ground
        unfolding terms
        by (simp add: is_ground_iff)

      have "ts = filter (λterm. term ⋅t γ(var := update) ≺⇩t term ⋅t γ) ?terms'" 
        using ss1 ts
        by auto
    
      moreover have "∀term ∈ set ?terms'. term ⋅t γ(var := update) ≼⇩t term ⋅t γ"
        using first.prems(1)
        unfolding terms
        by simp
    
      moreover have "∃term ∈ set ?terms'. term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
        using calculation(1) Cons neq_Nil_conv by force

      moreover have terms'_grounding: "term.is_ground (Fun f ?terms' ⋅t γ)"
        using first.prems(3)
        unfolding terms
        by simp
       
      moreover have "var ∈ term.vars (Fun f ?terms')"
        by (metis calculation(3) eval_with_fresh_var term.set_intros(4) term_order.less_irrefl)

      ultimately have less_terms': "Fun f ?terms' ⋅t γ(var := update) ≺⇩t Fun f ?terms' ⋅t γ"
        using first.hyps(1) first.prems(3) by blast

      have context_grounding: "context.is_ground (More f ss1 □ ss2 ⋅t⇩c γ)"
        using terms'_grounding
        by auto

      have "Fun f (ss1 @ t ⋅t γ(var := update) # ss2) ⋅t γ ≺⇩t Fun f terms ⋅t γ"
        unfolding terms
        using less⇩t_ground_context_compatible[OF less _ _ context_grounding]
        by simp

      with less_terms' show ?thesis 
        unfolding terms 
        by auto
    qed
  qed
qed

lemma less⇩l_subst_upd:
  fixes γ :: "('f, 'v) subst"
  assumes 
    update_is_ground: "term.is_ground update" and
    update_less: "update ≺⇩t γ var" and
    literal_grounding: "literal.is_ground (literal ⋅l γ)" and
    var: "var ∈ literal.vars literal"
  shows "literal ⋅l γ(var := update) ≺⇩l literal ⋅l γ"
proof-
  note less⇩t_subst_upd = less⇩t_subst_upd[of _ γ, OF update_is_ground update_less] 

  have all_ground_terms: "∀term ∈ set_uprod (atm_of literal). term.is_ground (term ⋅t γ)"
    using assms(3)
    apply(cases literal)
    by (simp add: ground_term_in_ground_literal_subst)+
     
  then have 
    "∀term ∈ set_uprod (atm_of literal). 
       var ∈ term.vars term ⟶ term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
    using less⇩t_subst_upd
    by blast

  moreover have
    "∀term ∈ set_uprod (atm_of literal). 
       var ∉ term.vars term ⟶ term ⋅t γ(var := update) = term ⋅t γ"
    by (meson eval_with_fresh_var)  

  ultimately have "∀term ∈ set_uprod (atm_of literal). term ⋅t γ(var := update) ≼⇩t term ⋅t γ" 
    by blast

  moreover have "∃term ∈ set_uprod (atm_of literal). term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
    using update_less var less⇩t_subst_upd all_ground_terms
    unfolding literal.vars_def atom.vars_def set_literal_atm_of
    by blast

  ultimately show ?thesis
    using less⇩t_less⇩l'
    by blast
qed

lemma less⇩c_subst_upd:
  assumes 
    update_is_ground: "term.is_ground update" and
    update_less: "update ≺⇩t γ var" and
    literal_grounding: "clause.is_ground (clause ⋅ γ)" and
    var: "var ∈ clause.vars clause"
  shows "clause ⋅ γ(var := update) ≺⇩c clause ⋅ γ"
proof-
  note less⇩l_subst_upd = less⇩l_subst_upd[of _ γ, OF update_is_ground update_less] 

  have all_ground_literals: "∀literal ∈# clause. literal.is_ground (literal ⋅l γ)"
    using clause.to_set_is_ground_subst[OF _ literal_grounding] by blast

  then have 
    "∀literal ∈# clause. 
      var ∈ literal.vars literal ⟶ literal ⋅l γ(var := update) ≺⇩l literal ⋅l γ"
    using less⇩l_subst_upd
    by blast

  then have "∀literal ∈# clause. literal ⋅l γ(var := update) ≼⇩l literal ⋅l γ"
    by fastforce

  moreover have "∃literal ∈# clause. literal ⋅l γ(var := update) ≺⇩l literal ⋅l γ"
    using update_less var less⇩l_subst_upd all_ground_literals
    unfolding clause.vars_def
    by blast

  ultimately show ?thesis
    using less⇩l_less⇩c
    by blast
qed

end

end