Theory First_Order_Clause.Nonground_Order_With_Equality

theory Nonground_Order_With_Equality
  imports
    Nonground_Clause_With_Equality
    Nonground_Order_Generic
    Ground_Order_With_Equality
begin

section ‹Nonground Order›

locale nonground_order =
  nonground_clause +
  "term": nonground_term_order
begin

sublocale restricted_term_order_lifting where
  restriction = "range term.from_ground" and pos_to_mset = pos_to_mset and neg_to_mset = neg_to_mset
  by unfold_locales

sublocale literal: nonground_term_based_order_lifting where
  less = less⇩t and sub_subst = "(⋅t)" and sub_vars = term.vars and
  sub_to_ground = term.to_ground and sub_from_ground = term.from_ground and
  map = map_uprod_literal and to_set = uprod_literal_to_set and
  to_ground_map = map_uprod_literal and from_ground_map = map_uprod_literal and
  ground_map = map_uprod_literal and to_set_ground = uprod_literal_to_set and
  to_mset = literal_to_mset
rewrites
  "⋀l σ. functional_substitution_lifting.subst (⋅t) map_uprod_literal l σ = literal.subst l σ" and
  "⋀l. functional_substitution_lifting.vars term.vars uprod_literal_to_set l = literal.vars l" and
  "⋀l⇩G. grounding_lifting.from_ground term.from_ground map_uprod_literal l⇩G
    = literal.from_ground l⇩G" and
  "⋀l. grounding_lifting.to_ground term.to_ground map_uprod_literal l = literal.to_ground l"
proof unfold_locales
  fix l

  show "set_mset (literal_to_mset l) = uprod_literal_to_set l"
    by (cases l) auto
next
  fix f l

  show "literal_to_mset (map_uprod_literal f l) = image_mset f (literal_to_mset l)"
    by (cases l) (auto simp: mset_uprod_image_mset)
qed (auto simp: inj_literal_to_mset)

notation literal.order.less⇩G (infix "≺⇩l⇩G" 50)
notation literal.order.less_eq⇩G (infix "≼⇩l⇩G" 50)

sublocale nonground_order_generic where
  atom_subst = atom.subst and atom_vars = atom.vars and atom_from_ground = atom.from_ground and
  atom_to_ground = atom.to_ground and neg_to_mset = neg_to_mset and pos_to_mset = pos_to_mset and
  ground_neg_to_mset = neg_to_mset and ground_pos_to_mset = pos_to_mset
  by unfold_locales (simp_all add: atom.from_ground_def mset_uprod_image_mset)

lemma literal_order_less_if_all_lesseq_ex_less_set:
  assumes
    "∀t ∈ set_uprod (atm_of l). t ⋅t σ' ≼⇩t t ⋅t σ"
    "∃t ∈ set_uprod (atm_of l). t ⋅t σ' ≺⇩t t ⋅t σ"
  shows "l ⋅l σ' ≺⇩l l ⋅l σ"
  using assms literal.order.less_if_all_lesseq_ex_less 
  unfolding literal.order.to_mset_to_set[unfolded uprod_literal_to_set_atm_of]
  by presburger

end

locale context_compatible_nonground_order =
  nonground_order +
  "term": context_compatible_nonground_term_order
begin

sublocale literal.order: subst_update_stable_multiset_extension where
  less = less⇩t and sub_subst = "(⋅t)" and sub_vars = term.vars and
  sub_to_ground = term.to_ground and sub_from_ground = term.from_ground and
  map = map_uprod_literal and to_set = uprod_literal_to_set and
  to_ground_map = map_uprod_literal and from_ground_map = map_uprod_literal and
  ground_map = map_uprod_literal and to_set_ground = uprod_literal_to_set and
  to_mset = literal_to_mset and id_subst = Var and base_vars = term.vars and base_less = less⇩t and
  base_subst = "(⋅t)"
  rewrites
  "⋀l σ. functional_substitution_lifting.subst (⋅t) map_uprod_literal l σ = literal.subst l σ" and
  "⋀l. functional_substitution_lifting.vars term.vars uprod_literal_to_set l = literal.vars l" and
  "⋀l⇩G. grounding_lifting.from_ground term.from_ground map_uprod_literal l⇩G
    = literal.from_ground l⇩G" and
  "⋀l. grounding_lifting.to_ground term.to_ground map_uprod_literal l = literal.to_ground l"
  by unfold_locales simp_all

sublocale context_compatible_nonground_order_generic where
  atom_subst = atom.subst and atom_vars = atom.vars and atom_from_ground = atom.from_ground and
  atom_to_ground = atom.to_ground and neg_to_mset = neg_to_mset and pos_to_mset = pos_to_mset and
  ground_neg_to_mset = neg_to_mset and ground_pos_to_mset = pos_to_mset
  by unfold_locales

end

end