Theory Nonground_Clause

theory Nonground_Clause
  imports
    Nonground_Term
    Nonground_Clause_Generic
    Literal_Functor
begin

section ‹Nonground Clauses›

locale nonground_clause = "term": nonground_term
begin

subsection ‹Nonground Literals›

sublocale nonground_clause_generic where 
  atom_vars = term.vars and atom_subst = "(⋅t)" and atom_to_ground = term.to_ground and
  atom_from_ground = term.from_ground
  by unfold_locales

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

lemma obtain_from_neg_literal_subst:
  assumes "l ⋅l σ = Neg t'"
  obtains t
  where "l = Neg t" "t' = t ⋅t σ"
  using assms 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 Clauses›

lemmas clause_safe_unfolds =
  literal_to_ground_atom_to_ground
  literal_from_ground_atom_from_ground
  literal_from_ground_polarity_stable
  subst_literal
  vars_literal

end

end