Theory First_Order_Clause.Nonground_Order_Generic

theory Nonground_Order_Generic
  imports
    Nonground_Clause_Generic
    Nonground_Term_Order
    Term_Order_Lifting
    Ground_Order_Generic
begin

section ‹Nonground Order›

locale nonground_order_lifting =
  grounding_lifting +
  order: ground_total_multiset_extension +
  order: ground_subst_stable_multiset_extension

locale nonground_term_based_order_lifting =
  "term": nonground_term +
  nonground_order_lifting where
  id_subst = Var 
for less⇩t

locale nonground_order_generic =
  "term": nonground_term where
  Var = "Var :: 'v ⇒ 't" and term_to_ground = "term_to_ground :: 't ⇒ 't⇩G" +
 
  nonground_clause_generic where
  atom_subst = atom_subst and atom_from_ground = atom_from_ground +

  restricted_term_order_lifting where
  pos_to_mset = pos_to_mset and restriction = "range term.from_ground" +

  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" +

  "term": nonground_term_order +

  ground: atom_to_mset where pos_to_mset = ground_pos_to_mset and neg_to_mset = ground_neg_to_mset
for 
  pos_to_mset :: "'a ⇒ 't multiset" and 
  atom_subst :: "'a ⇒ ('v ⇒ 't) ⇒ 'a" and
  atom_from_ground :: "'a⇩G ⇒ 'a" and
  ground_pos_to_mset ground_neg_to_mset :: "'a⇩G ⇒ 't⇩G multiset" +
assumes
  ground_pos_to_mset:
  "⋀a. image_mset term.from_ground (ground_pos_to_mset a) = pos_to_mset (atom_from_ground a)" and
  ground_neg_to_mset:
  "⋀a. image_mset term.from_ground (ground_neg_to_mset a) = neg_to_mset (atom_from_ground a)"
begin

(* 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)

(* TODO: Find way to call clause.order.sub = literal.order *)
notation clause.order.sub.less⇩G (infix "≺⇩l⇩G" 50)
notation clause.order.sub.less_eq⇩G (infix "≼⇩l⇩G" 50)

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 clause.order.sub.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
        clause.order.sub.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 clause.order.sub.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 clause.order.sub.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

 (* TODO: order.order *)
thm literal.order.order.strict_iff_order

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)"

sublocale ground: ground_order_generic where
  less⇩t = "(≺⇩t⇩G)" and pos_to_mset = ground_pos_to_mset and neg_to_mset = ground_neg_to_mset
rewrites
  less⇩l⇩G_rewrite [simp]:
  "multiset_extension.multiset_extension (≺⇩t⇩G) ground.literal_to_mset = (≺⇩l⇩G)" and
  less⇩c⇩G_rewrite [simp]: "multiset_extension.multiset_extension (≺⇩l⇩G) (λx. x) = (≺⇩c⇩G)" and
  is_maximal_rewrite [simp]: "⋀l⇩G C⇩G. ground.is_maximal l⇩G C⇩G ⟷ ground_is_maximal l⇩G C⇩G" and
  is_strictly_maximal_rewrite [simp]:
  "⋀l⇩G C⇩G. ground.is_strictly_maximal l⇩G C⇩G ⟷ ground_is_strictly_maximal l⇩G C⇩G" and
  "ground.literal_order_restriction = UNIV"
proof (unfold_locales; (rule ground.inj_pos_to_mset ground.inj_neg_to_mset ground.pos_neg_neq)?)

  interpret ground: ground_order_generic where
    less⇩t = "(≺⇩t⇩G)" and pos_to_mset = ground_pos_to_mset and neg_to_mset = ground_neg_to_mset
    using ground.inj_pos_to_mset ground.inj_neg_to_mset ground.pos_neg_neq
    by unfold_locales auto

  interpret multiset_extension "(≺⇩t⇩G)" ground.literal_to_mset
    by unfold_locales

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

  have literal_to_mset: "literal_to_mset (map_literal atom_from_ground l) =
            image_mset term.from_ground (ground.literal_to_mset l)" for l
    by (cases l) (auto simp: ground_pos_to_mset ground_neg_to_mset)

  show less⇩l⇩G_rewrite: "ground.literal.order.multiset_extension = (≺⇩l⇩G)"
    unfolding
      ground.literal.order.multiset_extension_def 
      literal.order.multiset_extension_def
      R⇩r_def
    unfolding 
      literal.from_ground_def 
      literal_to_mset
      term.order.less⇩G_def
    using 
      multp_image_mset_image_msetI[OF _ term.order.transp]
      multp_image_mset_image_msetD[OF _ term.order.transp]
      term.inj_from_ground 
    by metis

  fix l⇩G C⇩G
  show "ground.is_maximal l⇩G C⇩G ⟷ ground_is_maximal l⇩G C⇩G"
    unfolding
      ground.is_maximal_def
      is_maximal_def
      less⇩l⇩G_rewrite
      clause.order.sub.restriction.is_maximal_in_mset_iff
      clause.order.sub.less⇩r_def
    by (simp add: clause.to_set_from_ground image_iff)

  show "ground.is_strictly_maximal l⇩G C⇩G ⟷ ground_is_strictly_maximal l⇩G C⇩G"
    unfolding
      ground.is_strictly_maximal_def
      is_strictly_maximal_def
      less⇩l⇩G_rewrite
      clause.order.sub.restriction.is_strictly_maximal_in_mset_iff
      clause.order.sub.less⇩r_def
      reflclp_iff
    by (metis (lifting) clause.ground_sub_in_ground clause.sub_in_ground_is_ground 
        clause_from_ground_remove1_mset literal.obtain_grounding)

  show "{b. set_mset (ground.literal_to_mset b) ⊆ UNIV} = UNIV"
    by auto
next

  interpret multiset_extension "(≺⇩l⇩G)" "λx. x"
    by unfold_locales

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

  show less⇩c⇩G_rewrite: "(≺⇩m) = (≺⇩c⇩G)"
    unfolding multiset_extension_def clause.order.multiset_extension_def R⇩r_def
    unfolding clause.order.sub.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 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

locale context_compatible_nonground_order_generic = 
  nonground_order_generic +

  "term": context_compatible_nonground_term_order +

  clause.order: subst_update_stable_multiset_extension 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" and id_subst = Var and base_vars = term.vars and base_less = less⇩t and
  base_subst = "(⋅t)"

end