Theory Nonground_Order

theory Nonground_Order
  imports
    Nonground_Clause
    Nonground_Term_Order
    Term_Order_Lifting
begin

section ‹Nonground Order›

locale nonground_order_lifting =
  grounding_lifting +
  order: total_grounded_multiset_extension +
  order: ground_subst_stable_total_multiset_extension +
  order: subst_update_stable_multiset_extension
begin

sublocale order: grounded_restricted_total_strict_order where
  less = order.multiset_extension and subst = subst and vars = vars and to_ground = to_ground and
  from_ground = "from_ground"
  by unfold_locales

end

locale nonground_term_based_order_lifting =
  "term": nonground_term +
  nonground_order_lifting where
  id_subst = Var and comp_subst = "(⊙)" and base_vars = term.vars and base_less = less⇩t and
  base_subst = "(⋅t)"
for less⇩t

(* TODO: Abstract out non-equality literal order + better name *)
locale nonground_equality_order =
  nonground_clause +
  "term": nonground_term_order
begin

sublocale restricted_term_order_lifting where
  restriction = "range term.from_ground" and literal_to_mset = mset_lit
  by unfold_locales (rule inj_mset_lit)

(* TODO: Find way to not have this twice *)
notation term.order.less⇩G (infix "≺⇩t⇩G" 50)
notation term.order.less_eq⇩G (infix "≼⇩t⇩G" 50)

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 = mset_lit
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 (auto simp: inj_mset_lit mset_lit_image_mset)

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

sublocale clause: nonground_term_based_order_lifting where
  less = "(≺⇩l)" and sub_subst = literal.subst and sub_vars = literal.vars and
  sub_to_ground = literal.to_ground and sub_from_ground = literal.from_ground and
  map = image_mset and to_set = set_mset and to_ground_map = image_mset and
  from_ground_map = image_mset and ground_map = image_mset and to_set_ground = set_mset and
  to_mset = "λx. x"
  by unfold_locales simp_all

notation clause.order.less⇩G (infix "≺⇩c⇩G" 50)
notation clause.order.less_eq⇩G (infix "≼⇩c⇩G" 50)

lemma obtain_maximal_literal:
  assumes
    not_empty: "C ≠ {#}" and
    grounding: "clause.is_ground (C ⋅ γ)"
  obtains l
  where "is_maximal l C" "is_maximal (l ⋅l γ) (C ⋅ γ)"
proof-

  have grounding_not_empty: "C ⋅ γ ≠ {#}"
    using not_empty
    by simp

  obtain l where
    l_in_C: "l ∈# C" and
    l_grounding_is_maximal: "is_maximal (l ⋅l γ) (C ⋅ γ)"
    using
      ex_maximal_in_mset_wrt[OF
        literal.order.transp_on_less literal.order.asymp_on_less grounding_not_empty]
      maximal_in_clause
    unfolding clause.subst_def
    by (metis (mono_tags, lifting) image_iff multiset.set_map)

  show ?thesis
  proof(cases "is_maximal l C")
    case True

    with l_grounding_is_maximal that
    show ?thesis
      by blast
  next
    case False
    then obtain l' where
      l'_in_C: "l' ∈# C" and
      l_less_l': "l ≺⇩l l'"
      unfolding is_maximal_def
      using l_in_C
      by blast

    note literals_in_C = l_in_C l'_in_C
    note literals_grounding = literals_in_C[THEN clause.to_set_is_ground_subst[OF _ grounding]]

    have "l ⋅l γ ≺⇩l l' ⋅l γ"
      using literal.order.ground_subst_stability[OF literals_grounding l_less_l'].

    then have False
     using
       l_grounding_is_maximal
       clause.subst_in_to_set_subst[OF l'_in_C]
     unfolding is_maximal_def
     by force

    then show ?thesis..
  qed
qed

lemma obtain_strictly_maximal_literal:
  assumes
   grounding: "clause.is_ground (C ⋅ γ)" and
   ground_strictly_maximal: "is_strictly_maximal l⇩G (C ⋅ γ)"
 obtains l where
   "is_strictly_maximal l C" "l⇩G = l ⋅l γ"
proof-

  have grounding_not_empty: "C ⋅ γ ≠ {#}"
    using is_strictly_maximal_not_empty[OF ground_strictly_maximal].

  have l⇩G_in_grounding: "l⇩G ∈# C ⋅ γ"
    using strictly_maximal_in_clause[OF ground_strictly_maximal].

  obtain l where
    l_in_C: "l ∈# C" and
    l⇩G [simp]: "l⇩G = l ⋅l γ"
    using l⇩G_in_grounding
    unfolding clause.subst_def
    by blast

  show ?thesis
  proof(cases "is_strictly_maximal l C")
    case True
    show ?thesis
      using that[OF True l⇩G].
  next
    case False

    then obtain l' where
      l'_in_C: "l' ∈# C - {# l #}" and
      l_less_eq_l': "l ≼⇩l l'"
      unfolding is_strictly_maximal_def
      using l_in_C
      by blast

    note l_grounding =
       clause.to_set_is_ground_subst[OF l_in_C grounding]

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

    have "l ⋅l γ ≼⇩l l' ⋅l γ"
      using literal.order.less_eq.ground_subst_stability[OF l_grounding l'_grounding l_less_eq_l'].

    then have False
      using clause.subst_in_to_set_subst[OF l'_in_C] ground_strictly_maximal
      unfolding is_strictly_maximal_def subst_clause_remove1_mset[OF l_in_C]
      by simp

    then show ?thesis..
  qed
qed

lemma is_maximal_if_grounding_is_maximal:
  assumes
   l_in_C: "l ∈# C" and
   C_grounding: "clause.is_ground (C ⋅ γ)" and
   l_grounding_is_maximal: "is_maximal (l ⋅l γ) (C ⋅ γ)"
 shows
   "is_maximal l C"
proof(rule ccontr)
  assume "¬ is_maximal l C"

  then obtain l' where l_less_l': "l ≺⇩l l'" and l'_in_C: "l' ∈# C"
    using l_in_C
    unfolding is_maximal_def
    by blast

  have l'_grounding: "literal.is_ground (l' ⋅l γ)"
    using clause.to_set_is_ground_subst[OF l'_in_C C_grounding].

  have l_grounding: "literal.is_ground (l ⋅l γ)"
    using clause.to_set_is_ground_subst[OF l_in_C C_grounding].

  have l'_γ_in_C_γ: "l' ⋅l γ ∈# C ⋅ γ"
    using clause.subst_in_to_set_subst[OF l'_in_C].

  have "l ⋅l γ ≺⇩l l' ⋅l γ"
    using literal.order.ground_subst_stability[OF l_grounding l'_grounding l_less_l'].

  then have "¬ is_maximal (l ⋅l γ) (C ⋅ γ)"
    using l'_γ_in_C_γ
    unfolding is_maximal_def literal.subst_comp_subst
    by fastforce

  then show False
    using l_grounding_is_maximal..
qed

lemma is_strictly_maximal_if_grounding_is_strictly_maximal:
  assumes
   l_in_C: "l ∈# C" and
   grounding: "clause.is_ground (C ⋅ γ)" and
   grounding_strictly_maximal: "is_strictly_maximal (l ⋅l γ) (C ⋅ γ)"
 shows
   "is_strictly_maximal l C"
  using
    is_maximal_if_grounding_is_maximal[OF
      l_in_C
      grounding
      is_maximal_if_is_strictly_maximal[OF grounding_strictly_maximal]
    ]
    grounding_strictly_maximal
  unfolding
    is_strictly_maximal_def is_maximal_def
    subst_clause_remove1_mset[OF l_in_C, symmetric]
    reflclp_iff
  by (metis in_diffD clause.subst_in_to_set_subst)

lemma unique_maximal_in_ground_clause:
  assumes
    "clause.is_ground C"
    "is_maximal l C"
    "is_maximal l' C"
  shows
    "l = l'"
  using assms clause.to_set_is_ground literal.order.not_less_eq
  unfolding is_maximal_def reflclp_iff
  by meson

lemma unique_strictly_maximal_in_ground_clause:
  assumes
    "clause.is_ground C"
    "is_strictly_maximal l C"
    "is_strictly_maximal l' C"
  shows
    "l = l'"
  using assms unique_maximal_in_ground_clause
  by blast

lemma less⇩l⇩G_rewrite [simp]: "multiset_extension.multiset_extension (≺⇩t⇩G) mset_lit = (≺⇩l⇩G)"
proof-
  interpret multiset_extension "(≺⇩t⇩G)" mset_lit
    by unfold_locales

  interpret relation_restriction
    "(λb1 b2. multp (≺⇩t) (mset_lit b1) (mset_lit b2))" literal.from_ground
    by unfold_locales

  show ?thesis
    unfolding multiset_extension_def  literal.order.multiset_extension_def R⇩r_def
    unfolding term.order.less⇩G_def literal.from_ground_def atom.from_ground_def
    by (metis term.inj_from_ground mset_lit_image_mset multp_image_mset_image_msetD
        multp_image_mset_image_msetI term.order.transp_on_less)
qed

lemma less⇩c⇩G_rewrite [simp]:
  "multiset_extension.multiset_extension (≺⇩l⇩G) (λx. x) = (≺⇩c⇩G)"
  unfolding less⇩l⇩G_rewrite
proof-
  interpret multiset_extension "(≺⇩l⇩G)" "λx. x"
    by unfold_locales

  interpret relation_restriction "multp (≺⇩l)" clause.from_ground
    by unfold_locales

  show ?thesis
    unfolding multiset_extension_def clause.order.multiset_extension_def R⇩r_def
    unfolding literal.order.less⇩G_def clause.from_ground_def
    by (metis literal.inj_from_ground literal.order.transp multp_image_mset_image_msetD
        multp_image_mset_image_msetI)
qed

lemma is_maximal_rewrite [simp]:
  "is_maximal_in_mset_wrt (≺⇩l⇩G) C l = is_maximal (literal.from_ground l) (clause.from_ground C)"
  unfolding literal.order.less⇩G_def is_maximal_def literal.order.restriction.is_maximal_in_mset_iff
  by (metis clause.ground_sub_in_ground clause.sub_in_ground_is_ground
      literal.order.order.strict_iff_order literal.to_ground_inverse)
 (* TODO: order.order *)
thm literal.order.order.strict_iff_order

lemma is_strictly_maximal_rewrite [simp]:
  "is_strictly_maximal_in_mset_wrt (≺⇩l⇩G) C l =
   is_strictly_maximal (literal.from_ground l) (clause.from_ground C)"
  unfolding
    literal.order.less⇩G_def is_strictly_maximal_def
    literal.order.restriction.is_strictly_maximal_in_mset_iff
    reflclp_iff
  by (metis (lifting) clause.ground_sub_in_ground clause.sub_in_ground_is_ground
      literal.obtain_grounding clause_from_ground_remove1_mset)

sublocale ground: ground_order_with_equality where
  less⇩t = "(≺⇩t⇩G)"
rewrites
  "multiset_extension.multiset_extension (≺⇩t⇩G) mset_lit = (≺⇩l⇩G)" and
  "multiset_extension.multiset_extension (≺⇩l⇩G) (λx. x) = (≺⇩c⇩G)" and
  "⋀l C. ground.is_maximal l C ⟷ is_maximal (literal.from_ground l) (clause.from_ground C)" and
  "⋀l C. ground.is_strictly_maximal l C ⟷ is_strictly_maximal (literal.from_ground l) (clause.from_ground C)"
  by unfold_locales auto

abbreviation ground_is_maximal where
  "ground_is_maximal l⇩G C⇩G ≡ is_maximal (literal.from_ground l⇩G) (clause.from_ground C⇩G)"

abbreviation ground_is_strictly_maximal where
  "ground_is_strictly_maximal l⇩G C⇩G ≡
     is_strictly_maximal (literal.from_ground l⇩G) (clause.from_ground C⇩G)"

(* TODO: naming *)
lemma less⇩t_less⇩l:
  assumes "t⇩1 ≺⇩t t⇩2"
  shows
    less⇩t_less⇩l_pos: "t⇩1 ≈ t⇩3 ≺⇩l t⇩2 ≈ t⇩3" and
    less⇩t_less⇩l_neg: "t⇩1 !≈ t⇩3 ≺⇩l t⇩2 !≈ t⇩3"
  using assms
  unfolding less⇩l_def
  by (auto simp: multp_add_mset multp_add_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 literal.order.less_if_all_lesseq_ex_less[OF assms[folded set_mset_set_uprod]].

lemma less⇩c_add_mset:
  assumes "l ≺⇩l l'" "C ≼⇩c C'"
  shows "add_mset l C ≺⇩c add_mset l' C'"
  using assms multp_add_mset_reflclp[OF literal.order.asymp literal.order.transp]
  unfolding less⇩c_def
  by blast

lemmas less⇩c_add_same [simp] =
  multp_add_same[OF literal.order.asymp literal.order.transp, folded less⇩c_def]

end

end