Theory First_Order_Clause.Grounded_Selection_Function

theory Grounded_Selection_Function
  imports
    Nonground_Selection_Function
    HOL_Extra
begin

context groundable_nonground_clause
begin

abbreviation select_subst_stability_on_clause where
  "select_subst_stability_on_clause select select⇩G C⇩G Γ C γ ≡
    C ⋅ γ = clause.from_ground C⇩G ∧
    select⇩G C⇩G = clause.to_ground ((select C) ⋅ γ) ∧
    is_ground_instance Γ C γ"

abbreviation uncurried_ground_instances where
  "uncurried_ground_instances C ≡ ground_instances (fst C) (snd C)"

abbreviation select_subst_stability_on where
  "select_subst_stability_on select select⇩G N ≡
    ∀C⇩G ∈ ⋃ (uncurried_ground_instances ` N). ∃(e, C) ∈ N. ∃γ.
      select_subst_stability_on_clause select select⇩G C⇩G e C γ"

lemma obtain_subst_stable_on_select_grounding:
  fixes select :: "'a select"
  obtains select⇩G where
    "select_subst_stability_on select select⇩G N"
    "is_select_grounding select select⇩G"
proof -
  let ?N⇩G = "⋃(uncurried_ground_instances ` N)"

  {
    fix Γ C γ
    assume
      "(Γ, C) ∈ N"
      "is_ground_instance Γ C γ"

    then have
      "∃γ'. ∃(Γ', C')∈N. ∃select⇩G.
         select_subst_stability_on_clause select select⇩G (clause.to_ground (C ⋅ γ)) Γ' C' γ'"
      using is_ground_instance_is_ground
      by (intro exI[of _ γ], intro bexI[of _ "(Γ, C)"]) auto
  }

  then have
    "∀C⇩G ∈ ?N⇩G. ∃γ. ∃(Γ, C) ∈ N. ∃select⇩G. select_subst_stability_on_clause select select⇩G C⇩G Γ C γ"
    unfolding ground_instances_def
    by force

  then have select⇩G_exists_for_premises:
     "∀C⇩G ∈ ?N⇩G. ∃select⇩G γ. ∃(Γ, C) ∈ N. select_subst_stability_on_clause select select⇩G C⇩G Γ C γ"
    by blast

  obtain select⇩G_on_groundings where
    select⇩G_on_groundings: "select_subst_stability_on select select⇩G_on_groundings N"
    using Ball_Ex_comm(1)[OF select⇩G_exists_for_premises]
    unfolding prod.case_eq_if
    by fast

  define select⇩G where
    "⋀C⇩G. select⇩G C⇩G = (
        if C⇩G ∈ ?N⇩G
        then select⇩G_on_groundings C⇩G
        else clause.to_ground (select (clause.from_ground C⇩G))
    )"

  have grounding: "is_select_grounding select select⇩G"
    using select⇩G_on_groundings
    unfolding is_select_grounding_def select⇩G_def prod.case_eq_if
    by (metis (lifting) clause.from_ground_inverse clause.ground_is_ground clause.subst_id_subst)

  show ?thesis
    using that[OF _ grounding] select⇩G_on_groundings
    unfolding select⇩G_def
    by fastforce
qed

end

locale grounded_selection_function =
  nonground_selection_function where select = select and atom_subst = atom_subst +
  groundable_nonground_clause where atom_subst = atom_subst
  for               
    select :: "'a select" and
    atom_subst :: "'a ⇒ ('v ⇒ 't) ⇒ 'a" +
fixes select⇩G
assumes select⇩G: "is_select_grounding select select⇩G"
begin

abbreviation subst_stability_on where
  "subst_stability_on N ≡ select_subst_stability_on select select⇩G N"

lemma select⇩G_subset: "select⇩G C ⊆# C"
  using select⇩G
  unfolding is_select_grounding_def
  by (metis select_subset clause.to_ground_def image_mset_subseteq_mono clause.subst_def)

lemma select⇩G_negative_literals:
  assumes "l⇩G ∈# select⇩G C⇩G"
  shows "is_neg l⇩G"
proof -
  obtain C γ where
    is_ground: "clause.is_ground (C ⋅ γ)" and
    select⇩G: "select⇩G C⇩G = clause.to_ground (select C ⋅ γ)"
    using select⇩G
    unfolding is_select_grounding_def
    by blast

  show ?thesis
    using
      ground_literal_in_selection[
        OF select_ground_subst[OF is_ground] assms[unfolded select⇩G],
        THEN select_neg_subst
        ]
    by simp

qed

sublocale ground: selection_function select⇩G
  by unfold_locales (simp_all add: select⇩G_subset select⇩G_negative_literals)

end

end