Theory Grounded_Selection_Function

theory Grounded_Selection_Function
  imports
    Nonground_Selection_Function
    Nonground_Typing
    HOL_Extra
begin

context nonground_typing
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) ⋅ γ) ∧
    clause.is_welltyped_ground_instance C 𝒱 γ"

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

lemma obtain_subst_stable_on_select_grounding:
  fixes select :: "('f, 'v) select"
  obtains select⇩G where
    "select_subst_stability_on select select⇩G N"
    "is_select_grounding select select⇩G"
proof-
  let ?N⇩G = "⋃(clause.welltyped_ground_instances ` N)"

  {
    fix C 𝒱 γ
    assume
      "(C, 𝒱) ∈ N"
      "clause.is_welltyped_ground_instance C 𝒱 γ"

    then have
      "∃γ'. ∃(C', 𝒱')∈N. ∃select⇩G.
        select_subst_stability_on_clause select select⇩G (clause.to_ground (C ⋅ γ)) C' 𝒱' γ'"
      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 clause.welltyped_ground_instances_def
    by auto

  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 (no_types, 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 select +
  nonground_typing ℱ
  for
    select :: "('f, 'v :: infinite) atom clause ⇒ ('f, 'v) atom clause" and
    ℱ :: "('f, 'ty) fun_types" +
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