Theory Nonground_Clause

theory Nonground_Clause
  imports
    Ground_Clause
    Nonground_Term
    Nonground_Context
    Clausal_Calculus_Extra
    Multiset_Extra
    Multiset_Grounding_Lifting
begin

(* TODO: These are clauses with equality *)
section ‹Nonground Clauses and Substitutions›

type_synonym 'f ground_atom = "'f gatom"
type_synonym ('f, 'v) atom = "('f, 'v) term uprod"

locale term_based_multiset_lifting =
  term_based_lifting where
  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
begin

sublocale multiset_grounding_lifting where
  id_subst = Var and comp_subst = "(⊙)"
  by unfold_locales

end

locale nonground_clause = nonground_term_with_context
begin

subsection ‹Nonground Atoms›

sublocale atom: term_based_lifting where
  sub_subst = "(⋅t)" and sub_vars = term.vars and map = map_uprod and to_set = set_uprod and
  sub_to_ground = term.to_ground and sub_from_ground = term.from_ground and
  to_ground_map = map_uprod and from_ground_map = map_uprod and ground_map = map_uprod and
  to_set_ground = set_uprod
  by unfold_locales

notation atom.subst (infixl "⋅a" 67)

lemma vars_atom [simp]: "atom.vars (Upair t⇩1 t⇩2) = term.vars t⇩1 ∪ term.vars t⇩2"
  by (simp_all add: atom.vars_def)

lemma subst_atom [simp]:
  "Upair t⇩1 t⇩2 ⋅a σ = Upair (t⇩1 ⋅t σ) (t⇩2 ⋅t σ)"
  unfolding atom.subst_def
  by simp_all

lemma atom_from_ground_term_from_ground [simp]:
  "atom.from_ground (Upair t⇩G⇩1 t⇩G⇩2) = Upair (term.from_ground t⇩G⇩1) (term.from_ground t⇩G⇩2)"
  by (simp add: atom.from_ground_def)

lemma atom_to_ground_term_to_ground [simp]:
  "atom.to_ground (Upair t⇩1 t⇩2) = Upair (term.to_ground t⇩1) (term.to_ground t⇩2)"
  by (simp add: atom.to_ground_def)

lemma atom_is_ground_term_is_ground [simp]:
  "atom.is_ground (Upair t⇩1 t⇩2) ⟷ term.is_ground t⇩1 ∧ term.is_ground t⇩2"
  by simp

lemma obtain_from_atom_subst:
  assumes "Upair t⇩1' t⇩2' = a ⋅a σ"
  obtains t⇩1 t⇩2
  where "a = Upair t⇩1 t⇩2" "t⇩1' = t⇩1 ⋅t σ" "t⇩2' = t⇩2 ⋅t σ"
  using assms
  unfolding atom.subst_def
  by(cases a) force

subsection ‹Nonground Literals›

sublocale literal: term_based_lifting where
  sub_subst = atom.subst and sub_vars = atom.vars and map = map_literal and
  to_set = set_literal and sub_to_ground = atom.to_ground and
  sub_from_ground = atom.from_ground and to_ground_map = map_literal and
  from_ground_map = map_literal and ground_map = map_literal and to_set_ground = set_literal
  by unfold_locales

notation literal.subst (infixl "⋅l" 66)

lemma vars_literal [simp]:
  "literal.vars (Pos a) = atom.vars a"
  "literal.vars (Neg a) = atom.vars a"
  "literal.vars ((if b then Pos else Neg) a) = atom.vars a"
  by (simp_all add: literal.vars_def)

lemma subst_literal [simp]:
  "Pos a ⋅l σ = Pos (a ⋅a σ)"
  "Neg a ⋅l σ = Neg (a ⋅a σ)"
  "atm_of (l ⋅l σ) = atm_of l ⋅a σ"
  unfolding literal.subst_def
  using literal.map_sel
  by auto

lemma subst_literal_if [simp]:
  "(if b then Pos else Neg) a ⋅l ρ = (if b then Pos else Neg) (a ⋅a ρ)"
  by simp

lemma subst_polarity_stable:
  shows
    subst_neg_stable [simp]: "is_neg (l ⋅l σ) ⟷ is_neg l" and
    subst_pos_stable [simp]: "is_pos (l ⋅l σ) ⟷ is_pos l"
  by (simp_all add: literal.subst_def)

declare literal.discI [intro]

lemma literal_from_ground_atom_from_ground [simp]:
  "literal.from_ground (Neg a⇩G) = Neg (atom.from_ground a⇩G)"
  "literal.from_ground (Pos a⇩G) = Pos (atom.from_ground a⇩G)"
  by (simp_all add: literal.from_ground_def)

lemma literal_from_ground_polarity_stable [simp]:
  shows
    neg_literal_from_ground_stable: "is_neg (literal.from_ground l⇩G) ⟷ is_neg l⇩G" and
    pos_literal_from_ground_stable: "is_pos (literal.from_ground l⇩G) ⟷ is_pos l⇩G"
  by (simp_all add: literal.from_ground_def)

lemma literal_to_ground_atom_to_ground [simp]:
  "literal.to_ground (Pos a) = Pos (atom.to_ground a)"
  "literal.to_ground (Neg a) = Neg (atom.to_ground a)"
  by (simp_all add: literal.to_ground_def)

lemma literal_is_ground_atom_is_ground [intro]:
  "literal.is_ground l ⟷ atom.is_ground (atm_of l)"
  by (simp add: literal.vars_def set_literal_atm_of)

lemma obtain_from_pos_literal_subst:
  assumes "l ⋅l σ = t⇩1' ≈ t⇩2'"
  obtains t⇩1 t⇩2
  where "l = t⇩1 ≈ t⇩2" "t⇩1' = t⇩1 ⋅t σ" "t⇩2' = t⇩2 ⋅t σ"
  using assms obtain_from_atom_subst subst_pos_stable
  by (metis is_pos_def literal.sel(1) subst_literal(3))

lemma obtain_from_neg_literal_subst:
  assumes "l ⋅l σ = t⇩1' !≈ t⇩2'"
  obtains t⇩1 t⇩2
  where "l = t⇩1 !≈ t⇩2" "t⇩1 ⋅t σ = t⇩1'" "t⇩2 ⋅t σ = t⇩2'"
  using assms obtain_from_atom_subst subst_neg_stable
  by (metis literal.collapse(2) literal.disc(2) literal.sel(2) subst_literal(3))

lemmas obtain_from_literal_subst = obtain_from_pos_literal_subst obtain_from_neg_literal_subst

subsection ‹Nonground Literals - Alternative›

lemma uprod_literal [simp]:
  fixes l
  shows
  "functional_substitution_lifting.subst (⋅t) map_uprod_literal l σ = l ⋅l σ"
  "functional_substitution_lifting.vars term.vars uprod_literal_to_set l = literal.vars l"
  "grounding_lifting.from_ground term.from_ground map_uprod_literal l⇩G = literal.from_ground l⇩G"
  "grounding_lifting.to_ground term.to_ground map_uprod_literal l = literal.to_ground l"
proof -
  interpret term_based_lifting where
    sub_vars = term.vars and sub_subst = "(⋅t)" and map = map_uprod_literal and
    to_set = uprod_literal_to_set and sub_to_ground = term.to_ground and
    sub_from_ground = term.from_ground 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
    by unfold_locales

  fix l :: "('f, 'v) atom literal" and σ

  show "subst l σ = l ⋅l σ"
    unfolding subst_def literal.subst_def atom.subst_def
    by simp

  show "vars l = literal.vars l"
    unfolding atom.vars_def vars_def literal.vars_def
    by(cases l) simp_all

  fix l⇩G:: "'f ground_atom literal"
  show "from_ground l⇩G = literal.from_ground l⇩G"
    unfolding from_ground_def literal.from_ground_def atom.from_ground_def..

  fix l :: "('f, 'v) atom literal"
  show "to_ground l = literal.to_ground l"
    unfolding to_ground_def literal.to_ground_def atom.to_ground_def..
qed

lemma uprod_literal_subst_eq_literal_subst: "map_uprod_literal (λt. t ⋅t σ) l = l ⋅l σ"
  unfolding atom.subst_def literal.subst_def
  by auto

lemma uprod_literal_vars_eq_literal_vars: "⋃ (term.vars ` uprod_literal_to_set l) = literal.vars l"
  unfolding literal.vars_def atom.vars_def
  by(cases l) simp_all

lemma uprod_literal_from_ground_eq_literal_from_ground:
  "map_uprod_literal term.from_ground l⇩G = literal.from_ground l⇩G"
  unfolding literal.from_ground_def atom.from_ground_def ..

lemma uprod_literal_to_ground_eq_literal_to_ground:
  "map_uprod_literal term.to_ground l = literal.to_ground l"
  unfolding literal.to_ground_def atom.to_ground_def ..

sublocale uprod_literal: term_based_lifting where
  sub_subst = "(⋅t)" and sub_vars = term.vars and map = map_uprod_literal and
  to_set = uprod_literal_to_set and sub_to_ground = term.to_ground and
  sub_from_ground = term.from_ground 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
rewrites
  "⋀l σ. uprod_literal.subst l σ = literal.subst l σ" and
  "⋀l. uprod_literal.vars l = literal.vars l" and
  "⋀l⇩G. uprod_literal.from_ground l⇩G = literal.from_ground l⇩G" and
  "⋀l. uprod_literal.to_ground l = literal.to_ground l"
  by unfold_locales simp_all

lemma mset_literal_from_ground:
  "mset_lit (literal.from_ground l) = image_mset term.from_ground (mset_lit l)"
  by (simp add: uprod_literal.from_ground_def mset_lit_image_mset)

subsection ‹Nonground Clauses›

sublocale clause: term_based_multiset_lifting where
  sub_subst = literal.subst and sub_vars = literal.vars and sub_to_ground = literal.to_ground and
  sub_from_ground = literal.from_ground
  by unfold_locales

notation clause.subst (infixl "⋅" 67)

lemmas clause_submset_vars_clause_subset [intro] =
  clause.to_set_subset_vars_subset[OF set_mset_mono]

lemmas sub_ground_clause = clause.to_set_subset_is_ground[OF set_mset_mono]

lemma subst_clause_remove1_mset [simp]:
  assumes "l ∈# C"
  shows "remove1_mset l C ⋅ σ = remove1_mset (l ⋅l σ) (C ⋅ σ)"
  unfolding clause.subst_def image_mset_remove1_mset_if
  using assms
  by simp

lemma clause_from_ground_remove1_mset [simp]:
  "clause.from_ground (remove1_mset l⇩G C⇩G) =
    remove1_mset (literal.from_ground l⇩G) (clause.from_ground C⇩G)"
  unfolding clause.from_ground_def image_mset_remove1_mset[OF literal.inj_from_ground]..

lemmas clause_safe_unfolds =
  atom_to_ground_term_to_ground
  literal_to_ground_atom_to_ground
  atom_from_ground_term_from_ground
  literal_from_ground_atom_from_ground
  literal_from_ground_polarity_stable
  subst_atom
  subst_literal
  vars_atom
  vars_literal

end

end