Theory Nonground_Selection_Function

theory Nonground_Selection_Function
  imports
    Nonground_Clause
    Selection_Function
begin

type_synonym 'f ground_select = "'f ground_atom clause ⇒ 'f ground_atom clause"
type_synonym ('f, 'v) select = "('f, 'v) atom clause ⇒ ('f, 'v) atom clause"

context nonground_clause
begin

definition is_select_grounding :: "('f, 'v) select ⇒ 'f ground_select ⇒ bool" where
  "is_select_grounding select select⇩G ≡ ∀C⇩G. ∃C γ.
    clause.is_ground (C ⋅ γ) ∧
    C⇩G = clause.to_ground (C ⋅ γ) ∧
    select⇩G C⇩G = clause.to_ground ((select C) ⋅ γ)"

end

locale nonground_selection_function =
  nonground_clause +
  selection_function select
  for select :: "('f, 'v) atom clause ⇒ ('f, 'v) atom clause"
begin

abbreviation is_grounding :: "'f ground_select ⇒ bool" where
  "is_grounding select⇩G ≡ is_select_grounding select select⇩G"

definition select⇩G⇩s where
  "select⇩G⇩s = { select⇩G. is_grounding select⇩G }"

definition select⇩G_simple where
  "select⇩G_simple C = clause.to_ground (select (clause.from_ground C))"

lemma select⇩G_simple: "is_grounding select⇩G_simple"
  unfolding is_select_grounding_def select⇩G_simple_def
  by (metis clause.from_ground_inverse clause.ground_is_ground clause.subst_id_subst)

lemma select_is_ground:
  assumes "clause.is_ground C"
  shows "clause.is_ground (select C)"
  using select_subset sub_ground_clause assms
  by metis

lemma is_ground_in_selection:
  assumes "l ∈# select (clause.from_ground C)"
  shows "literal.is_ground l"
  using assms clause.sub_in_ground_is_ground select_subset
  by blast

lemma ground_literal_in_selection:
  assumes "clause.is_ground C" "l⇩G ∈# clause.to_ground C"
  shows "literal.from_ground l⇩G ∈# C"
  using assms
  by (metis clause.to_ground_inverse clause.ground_sub_in_ground)

lemma select_ground_subst:
  assumes "clause.is_ground (C ⋅ γ)"
  shows "clause.is_ground (select C ⋅ γ)"
  using assms
  by (metis image_mset_subseteq_mono select_subset sub_ground_clause clause.subst_def)

lemma select_neg_subst:
  assumes "l ∈# select C ⋅ γ"
  shows "is_neg l"
  using assms subst_neg_stable select_negative_literals
  unfolding clause.subst_def
  by blast

lemma select_vars_subset: "⋀C. clause.vars (select C) ⊆ clause.vars C"
  by (simp add: clause_submset_vars_clause_subset select_subset)

end

end