Theory First_Order_Clause.Nonground_Clause_Generic

theory Nonground_Clause_Generic
  imports
    Nonground_Term
    Multiset_Extra
    Multiset_Grounding_Lifting
    Saturation_Framework_Extensions.Clausal_Calculus
begin

section ‹Nonground Clauses and Substitutions›


subsection ‹Setup for lifting from terms›

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 = comp_subst
  by unfold_locales

end

locale nonground_clause_generic =
  literal: term_based_lifting where
  sub_vars = atom_vars and sub_subst = atom_subst and sub_to_ground = atom_to_ground and
  sub_from_ground = atom_from_ground and map = map_literal and to_set = set_literal and
  to_ground_map = map_literal and from_ground_map = map_literal and ground_map = map_literal and
  to_set_ground = set_literal
for
  atom_from_ground :: "'g ⇒ 'a" and
  atom_to_ground :: "'a ⇒ 'g" and
  atom_subst :: "'a ⇒ ('v ⇒ 't) ⇒ 'a" and
  atom_vars :: "'a ⇒ 'v set"
begin

subsection ‹Nonground Literals›

(* TODO? *)
notation atom_subst (infixl "⋅a" 66)
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 ⟷ literal.sub.is_ground (atm_of l)"
  by (simp add: literal.vars_def set_literal_atm_of)

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]..

end

locale groundable_nonground_clause = 
  nonground_clause_generic where atom_subst = atom_subst
for 
  atom_subst :: "'a ⇒ ('v ⇒ 't) ⇒ 'a"  and
  is_ground_instance :: "'env ⇒ 'a clause ⇒ ('v ⇒ 't) ⇒ bool" +
assumes is_ground_instance_is_ground:
  "⋀Γ C γ. is_ground_instance Γ C γ ⟹ clause.is_ground (C ⋅ γ)"
begin

definition ground_instances where
  "ground_instances Γ C = { clause.to_ground (C ⋅ γ) | γ. is_ground_instance Γ C γ }"

end

end