Theory Grounded_Superposition

theory Grounded_Superposition
  imports
    Superposition
    Ground_Superposition

    First_Order_Clause.Grounded_Selection_Function
    First_Order_Clause.Nonground_Inference
    Saturation_Framework.Lifting_to_Non_Ground_Calculi
begin

locale grounded_superposition_calculus =
  superposition_calculus where select = select and ℱ = ℱ +
  grounded_selection_function where select = select and ℱ = ℱ
  for
    select :: "('f, 'v :: infinite) select" and
    ℱ :: "('f, 'ty) fun_types"
begin

sublocale nonground_inference.

sublocale ground: ground_superposition_calculus where
  less⇩t = "(≺⇩t⇩G)" and select = select⇩G
rewrites
  "multiset_extension.multiset_extension (≺⇩t⇩G) mset_lit = (≺⇩l⇩G)" and
  "multiset_extension.multiset_extension (≺⇩l⇩G) (λx. x) = (≺⇩c⇩G)" and
  "⋀l C. ground.is_maximal l C ⟷ is_maximal (literal.from_ground l) (clause.from_ground C)" and
  "⋀l C. ground.is_strictly_maximal l C ⟷
    is_strictly_maximal (literal.from_ground l) (clause.from_ground C)"
  by unfold_locales simp_all

abbreviation is_inference_ground_instance_one_premise where
  "is_inference_ground_instance_one_premise D C ι⇩G γ ≡
     case (D, C) of ((D, 𝒱'), (C, 𝒱)) ⇒
      inference.is_ground (Infer [D] C ⋅ι γ) ∧
      ι⇩G = inference.to_ground (Infer [D] C ⋅ι γ) ∧
      clause.is_welltyped 𝒱 D ∧
      term.subst.is_welltyped_on (clause.vars C) 𝒱 γ ∧
      clause.is_welltyped 𝒱 C ∧
      𝒱 = 𝒱' ∧
      infinite_variables_per_type 𝒱"

abbreviation is_inference_ground_instance_two_premises where
  "is_inference_ground_instance_two_premises D E C ι⇩G γ ρ⇩1 ρ⇩2 ≡
    case (D, E, C) of ((D, 𝒱⇩2), (E, 𝒱⇩1), (C, 𝒱⇩3)) ⇒
          term_subst.is_renaming ρ⇩1
        ∧ term_subst.is_renaming ρ⇩2
        ∧ clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {}
        ∧ inference.is_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C ⋅ι γ)
        ∧ ι⇩G = inference.to_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C ⋅ι γ)
        ∧ clause.is_welltyped 𝒱⇩1 E
        ∧ clause.is_welltyped 𝒱⇩2 D
        ∧ term.subst.is_welltyped_on (clause.vars C) 𝒱⇩3 γ
        ∧ clause.is_welltyped 𝒱⇩3 C
        ∧ infinite_variables_per_type 𝒱⇩1
        ∧ infinite_variables_per_type 𝒱⇩2
        ∧ infinite_variables_per_type 𝒱⇩3"

abbreviation is_inference_ground_instance where
  "is_inference_ground_instance ι ι⇩G γ ≡
  (case ι of
      Infer [D] C ⇒ is_inference_ground_instance_one_premise D C ι⇩G γ
    | Infer [D, E] C ⇒ ∃ρ⇩1 ρ⇩2. is_inference_ground_instance_two_premises D E C ι⇩G γ ρ⇩1 ρ⇩2
    | _ ⇒ False)
  ∧ ι⇩G ∈ ground.G_Inf"

definition inference_ground_instances where
  "inference_ground_instances ι = { ι⇩G | ι⇩G γ. is_inference_ground_instance ι ι⇩G γ }"

lemma is_inference_ground_instance:
  "is_inference_ground_instance ι ι⇩G γ ⟹ ι⇩G ∈ inference_ground_instances ι"
  unfolding inference_ground_instances_def
  by blast

lemma is_inference_ground_instance_one_premise:
  assumes "is_inference_ground_instance_one_premise D C ι⇩G γ" "ι⇩G ∈ ground.G_Inf"
  shows "ι⇩G ∈ inference_ground_instances (Infer [D] C)"
  using assms
  unfolding inference_ground_instances_def
  by auto

lemma is_inference_ground_instance_two_premises:
  assumes "is_inference_ground_instance_two_premises D E C ι⇩G γ ρ⇩1 ρ⇩2" "ι⇩G ∈ ground.G_Inf"
  shows "ι⇩G ∈ inference_ground_instances (Infer [D, E] C)"
  using assms
  unfolding inference_ground_instances_def
  by auto

lemma ground_inference⇩_concl_in_welltyped_ground_instances:
  assumes "ι⇩G ∈ inference_ground_instances ι"
  shows "concl_of ι⇩G ∈ clause.welltyped_ground_instances (concl_of ι)"
proof-
  obtain "premises" C 𝒱 where
    ι: "ι = Infer premises (C, 𝒱)"
    using Calculus.inference.exhaust
    by (metis prod.collapse)

  show ?thesis
    using assms
    unfolding ι inference_ground_instances_def clause.welltyped_ground_instances_def
    by (cases "premises" rule: list_4_cases) auto
qed

lemma ground_inference_red_in_welltyped_ground_instances_of_concl:
  assumes "ι⇩G ∈ inference_ground_instances ι"
  shows "ι⇩G ∈ ground.Red_I (clause.welltyped_ground_instances (concl_of ι))"
proof-
  from assms have "ι⇩G ∈ ground.G_Inf"
    unfolding inference_ground_instances_def
    by blast

  moreover have "concl_of ι⇩G ∈ clause.welltyped_ground_instances (concl_of ι)"
    using assms ground_inference⇩_concl_in_welltyped_ground_instances
    by auto

  ultimately show "ι⇩G ∈ ground.Red_I (clause.welltyped_ground_instances (concl_of ι))"
    using ground.Red_I_of_Inf_to_N
    by blast
qed

thm option.sel

sublocale lifting:
  tiebreaker_lifting
    "⊥⇩F"
    inferences
    ground.G_Bot
    ground.G_entails
    ground.G_Inf
    ground.GRed_I
    ground.GRed_F
    clause.welltyped_ground_instances
    "Some ∘ inference_ground_instances"
    typed_tiebreakers
proof(unfold_locales; (intro impI typed_tiebreakers.wfp typed_tiebreakers.transp)?)

  show "⊥⇩F ≠ {}"
    using exists_infinite_variables_per_type[OF types_ordLeq_variables]
    by blast
next
  fix bottom
  assume "bottom ∈ ⊥⇩F"

  then show "clause.welltyped_ground_instances bottom ≠ {}"
    unfolding clause.welltyped_ground_instances_def
    by auto
next
  fix bottom
  assume "bottom ∈ ⊥⇩F"

  then show "clause.welltyped_ground_instances bottom ⊆ ground.G_Bot"
    unfolding clause.welltyped_ground_instances_def
    by auto
next
  fix C :: "('f, 'v, 'ty) typed_clause"

  assume "clause.welltyped_ground_instances C ∩ ground.G_Bot ≠ {}"

  moreover then have "fst C = {#}"
    unfolding clause.welltyped_ground_instances_def
    by simp

  then have "C = ({#}, snd C)"
    by (metis split_pairs)

  ultimately show "C ∈ ⊥⇩F"
    unfolding clause.welltyped_ground_instances_def
    by blast
next
  fix ι :: "('f, 'v, 'ty) typed_clause inference"

  show "the ((Some ∘ inference_ground_instances) ι) ⊆
          ground.GRed_I (clause.welltyped_ground_instances (concl_of ι))"
    using ground_inference_red_in_welltyped_ground_instances_of_concl
    by auto
qed

end

context superposition_calculus
begin

sublocale
  lifting_intersection
    inferences
    "{{#}}"
    select⇩G⇩s
    "ground_superposition_calculus.G_Inf (≺⇩t⇩G)"
    "λ_. ground_superposition_calculus.G_entails"
    "ground_superposition_calculus.GRed_I (≺⇩t⇩G)"
    "λ_. ground_superposition_calculus.GRed_F (≺⇩t⇩G)"
    "⊥⇩F"
    "λ_. clause.welltyped_ground_instances"
    "λselect⇩G. Some ∘ (grounded_superposition_calculus.inference_ground_instances (≺⇩t) select⇩G ℱ)"
    typed_tiebreakers
proof(unfold_locales; (intro ballI)?)
  show "select⇩G⇩s ≠ {}"
    using select⇩G_simple
    unfolding select⇩G⇩s_def
    by blast
next
  fix select⇩G
  assume "select⇩G ∈ select⇩G⇩s"

  then interpret grounded_superposition_calculus
    where select⇩G = select⇩G
    by unfold_locales (simp add: select⇩G⇩s_def)

  show "consequence_relation ground.G_Bot ground.G_entails"
    using ground.consequence_relation_axioms.

  show "tiebreaker_lifting
          ⊥⇩F
          inferences
          ground.G_Bot
          ground.G_entails
          ground.G_Inf
          ground.GRed_I
          ground.GRed_F
          clause.welltyped_ground_instances
          (Some ∘ inference_ground_instances)
          typed_tiebreakers"
    by unfold_locales
qed

end

end