Theory Grounded_First_Order_Superposition

theory Grounded_First_Order_Superposition
  imports 
    First_Order_Superposition
    Ground_Superposition_Completeness
begin

context ground_superposition_calculus
begin

abbreviation eq_resolution_inferences where
  "eq_resolution_inferences ≡  {Infer [P] C | P C. ground_eq_resolution P C}"

abbreviation eq_factoring_inferences where
  "eq_factoring_inferences ≡  {Infer [P] C | P C.  ground_eq_factoring P C}"

abbreviation superposition_inferences where
  "superposition_inferences ≡ {Infer [P2, P1] C | P1 P2 C. ground_superposition P2 P1 C}"

end

locale grounded_first_order_superposition_calculus =
  first_order_superposition_calculus select _ _ typeof_fun +
  grounded_first_order_select select
  for 
    select :: "('f, 'v :: infinite) select" and
    typeof_fun :: "('f, 'ty) fun_types"
begin

sublocale ground: ground_superposition_calculus where
  less_trm = "(≺⇩t⇩G)" and select = select⇩G
  by unfold_locales (rule ground_critical_pair_theorem)

definition is_inference_grounding where
  "is_inference_grounding ι ι⇩G γ ρ⇩1 ρ⇩2 ≡
    (case ι of
        Infer [(premise, 𝒱')] (conclusion, 𝒱) ⇒
           term_subst.is_ground_subst γ
        ∧ ι⇩G = Infer [clause.to_ground (premise ⋅ γ)] (clause.to_ground (conclusion ⋅ γ))
        ∧ welltyped⇩c typeof_fun 𝒱 premise 
        ∧ welltyped⇩σ_on (clause.vars conclusion) typeof_fun 𝒱 γ
        ∧ welltyped⇩c typeof_fun 𝒱 conclusion
        ∧ 𝒱 = 𝒱'
        ∧ all_types 𝒱
      | Infer [(premise⇩2, 𝒱⇩2), (premise⇩1, 𝒱⇩1)] (conclusion, 𝒱⇩3) ⇒ 
          term_subst.is_renaming ρ⇩1
        ∧ term_subst.is_renaming ρ⇩2
        ∧ clause.vars (premise⇩1 ⋅ ρ⇩1) ∩ clause.vars (premise⇩2 ⋅ ρ⇩2) = {}
        ∧ term_subst.is_ground_subst γ
        ∧ ι⇩G =
            Infer
              [clause.to_ground (premise⇩2 ⋅ ρ⇩2 ⋅ γ), clause.to_ground (premise⇩1 ⋅ ρ⇩1 ⋅ γ)]
              (clause.to_ground (conclusion ⋅ γ))
        ∧ welltyped⇩c typeof_fun 𝒱⇩1 premise⇩1
        ∧ welltyped⇩c typeof_fun 𝒱⇩2 premise⇩2
        ∧ welltyped⇩σ_on (clause.vars conclusion) typeof_fun 𝒱⇩3 γ
        ∧ welltyped⇩c typeof_fun 𝒱⇩3 conclusion
        ∧ all_types 𝒱⇩1 ∧ all_types 𝒱⇩2 ∧ all_types 𝒱⇩3
      | _ ⇒ False
     )
  ∧ ι⇩G ∈ ground.G_Inf"

definition inference_groundings where 
  "inference_groundings ι = { ι⇩G | ι⇩G γ ρ⇩1 ρ⇩2. is_inference_grounding ι ι⇩G γ ρ⇩1 ρ⇩2 }"

lemma is_inference_grounding_inference_groundings: 
  "is_inference_grounding ι ι⇩G γ ρ⇩1 ρ⇩2  ⟹ ι⇩G ∈ inference_groundings ι"
  unfolding inference_groundings_def
  by blast

lemma inference⇩G_concl_in_clause_grounding: 
  assumes "ι⇩G ∈ inference_groundings ι"
  shows "concl_of ι⇩G ∈ clause_groundings typeof_fun (concl_of ι)"
proof-
  obtain premises⇩G conlcusion⇩G where
    ι⇩G: "ι⇩G = Infer premises⇩G conlcusion⇩G"
    using Calculus.inference.exhaust by blast

  obtain "premises" "conclusion" 𝒱 where
    ι: "ι = Infer premises (conclusion, 𝒱)"
    using Calculus.inference.exhaust
    by (metis prod.collapse)

  obtain γ where
    "clause.is_ground (conclusion ⋅ γ)"
    "conlcusion⇩G = clause.to_ground (conclusion ⋅ γ)"
    "welltyped⇩c typeof_fun 𝒱 conclusion ∧ welltyped⇩σ_on (clause.vars conclusion) typeof_fun 𝒱 γ ∧ 
    term_subst.is_ground_subst γ ∧ all_types 𝒱"
  proof-
    have "⋀γ ρ⇩1 ρ⇩2.
       ⟦⋀γ. ⟦clause.vars (conclusion ⋅ γ) = {}; conlcusion⇩G = clause.to_ground (conclusion ⋅ γ);
              First_Order_Type_System.welltyped⇩c typeof_fun 𝒱 conclusion ∧
              welltyped⇩σ_on (clause.vars conclusion) typeof_fun 𝒱 γ ∧
              term_subst.is_ground_subst γ ∧ all_types 𝒱⟧
             ⟹ thesis;
        Infer premises⇩G conlcusion⇩G ∈ ground.G_Inf;
        case premises of [] ⇒ False
        | [(premise, 𝒱')] ⇒
            term_subst.is_ground_subst γ ∧
            Infer premises⇩G conlcusion⇩G =
            Infer [clause.to_ground (premise ⋅ γ)] (clause.to_ground (conclusion ⋅ γ)) ∧
            First_Order_Type_System.welltyped⇩c typeof_fun 𝒱 premise ∧
            welltyped⇩σ_on (clause.vars conclusion) typeof_fun 𝒱 γ ∧
            First_Order_Type_System.welltyped⇩c typeof_fun 𝒱 conclusion ∧ 𝒱 = 𝒱' ∧ all_types 𝒱
        | [(premise, 𝒱'), (premise⇩1, 𝒱⇩1)] ⇒
            clause.is_renaming ρ⇩1 ∧
            clause.is_renaming ρ⇩2 ∧
            clause.vars (premise⇩1 ⋅ ρ⇩1) ∩ clause.vars (premise ⋅ ρ⇩2) = {} ∧
            term_subst.is_ground_subst γ ∧
            Infer premises⇩G conlcusion⇩G =
            Infer [clause.to_ground (premise ⋅ ρ⇩2 ⋅ γ), clause.to_ground (premise⇩1 ⋅ ρ⇩1 ⋅ γ)]
             (clause.to_ground (conclusion ⋅ γ)) ∧
            First_Order_Type_System.welltyped⇩c typeof_fun 𝒱⇩1 premise⇩1 ∧
            First_Order_Type_System.welltyped⇩c typeof_fun 𝒱' premise ∧
            welltyped⇩σ_on (clause.vars conclusion) typeof_fun 𝒱 γ ∧
            First_Order_Type_System.welltyped⇩c typeof_fun 𝒱 conclusion ∧
            all_types 𝒱⇩1 ∧ all_types 𝒱' ∧ all_types 𝒱
        | (premise, 𝒱') # (premise⇩1, 𝒱⇩1) # a # lista ⇒ False⟧
       ⟹ thesis"
      by(auto simp: clause.is_ground_subst_is_ground split: list.splits)
        (metis list_4_cases prod.exhaust_sel) 

     then show ?thesis
      using that assms 
      unfolding inference_groundings_def ι ι⇩G Calculus.inference.case
      by (auto simp: is_inference_grounding_def)
  qed

  then show ?thesis
    unfolding ι ι⇩G clause_groundings_def
    by auto
qed  

lemma inference⇩G_red_in_clause_grounding_of_concl: 
  assumes "ι⇩G ∈ inference_groundings ι"
  shows "ι⇩G ∈ ground.Red_I (clause_groundings typeof_fun (concl_of ι))"
proof-
  from assms have "ι⇩G ∈ ground.G_Inf"
    unfolding inference_groundings_def is_inference_grounding_def
    by blast

  moreover have "concl_of ι⇩G ∈ clause_groundings typeof_fun  (concl_of ι)"
    using assms inference⇩G_concl_in_clause_grounding
    by auto

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

lemma obtain_welltyped_ground_subst:
  obtains γ :: "('f, 'v) subst" and ℱ⇩G :: "('f, 'ty) fun_types"
  where "welltyped⇩σ typeof_fun 𝒱 γ" "term_subst.is_ground_subst γ"
proof-
 
  define γ :: "('f, 'v) subst" where
    "⋀x. γ x ≡ Fun (SOME f. typeof_fun f = ([], 𝒱 x)) []"


  moreover have "welltyped⇩σ typeof_fun 𝒱 γ"
  proof-
    have "⋀x. First_Order_Type_System.welltyped typeof_fun 𝒱
          (Fun (SOME f. typeof_fun f = ([], 𝒱 x)) []) (𝒱 x)"
      by (meson function_symbols list_all2_Nil someI_ex welltyped.Fun)

    then show ?thesis
      unfolding welltyped⇩σ_def γ_def
      by auto
  qed

  moreover have "term_subst.is_ground_subst γ"
    unfolding term_subst.is_ground_subst_def γ_def
    by (smt (verit) Nil_is_map_conv equals0D eval_term.simps(2) is_ground_iff is_ground_trm_iff_ident_forall_subst)

  ultimately show ?thesis
    using that
    by blast
qed


lemma welltyped⇩σ_on_empty: "welltyped⇩σ_on {} ℱ 𝒱 σ"
  unfolding welltyped⇩σ_on_def
  by simp  

sublocale lifting: 
    tiebreaker_lifting
          "⊥⇩F"
          inferences 
          ground.G_Bot
          ground.G_entails
          ground.G_Inf 
          ground.GRed_I
          ground.GRed_F 
          "clause_groundings typeof_fun"
          "(Some ∘ inference_groundings)"
          typed_tiebreakers
proof unfold_locales
  show "⊥⇩F ≠ {}"
    using all_types'[OF variables]
    by blast
next
  fix bottom
  assume "bottom ∈ ⊥⇩F"

  then show "clause_groundings typeof_fun bottom ≠ {}"
    unfolding clause_groundings_def
    using welltyped⇩σ_Var
  proof -
    have "∃f. welltyped⇩σ_on (clause.vars {#}) typeof_fun (snd bottom) f ∧ 
          First_Order_Type_System.welltyped⇩c typeof_fun (snd bottom) {#} ∧ 
          term_subst.is_ground_subst f"
      by (metis First_Order_Type_System.welltyped⇩c_def empty_clause_is_ground ex_in_conv 
          set_mset_eq_empty_iff term.obtain_ground_subst welltyped⇩σ_on_empty)

    then show "{clause.to_ground (fst bottom ⋅ f) |f. term_subst.is_ground_subst f 
        ∧ First_Order_Type_System.welltyped⇩c typeof_fun (snd bottom) (fst bottom) 
        ∧ welltyped⇩σ_on (clause.vars (fst bottom)) typeof_fun (snd bottom) f 
        ∧ all_types (snd bottom)} ≠ {}"
      using ‹bottom ∈ ⊥⇩F› by force
  qed
next
  fix bottom
  assume "bottom ∈ ⊥⇩F"
  then show "clause_groundings typeof_fun bottom ⊆ ground.G_Bot"
    unfolding clause_groundings_def
    by clause_auto
next
  fix clause
  show "clause_groundings typeof_fun clause ∩ ground.G_Bot ≠ {} ⟶ clause ∈ ⊥⇩F"
    unfolding clause_groundings_def clause.to_ground_def clause.subst_def
    by (smt (verit) disjoint_insert(1) image_mset_is_empty_iff inf_bot_right mem_Collect_eq 
        prod.exhaust_sel)
next
  fix ι :: "('f, 'v, 'ty) typed_clause inference"

  show "the ((Some ∘ inference_groundings) ι) ⊆ 
      ground.GRed_I (clause_groundings typeof_fun (concl_of ι))"
    using inference⇩G_red_in_clause_grounding_of_concl
    by auto
next
  show "⋀clause⇩G. po_on (typed_tiebreakers clause⇩G) UNIV"
    unfolding po_on_def
    using wellfounded_typed_tiebreakers
    by simp
next
  show "⋀clause⇩G. Restricted_Predicates.wfp_on (typed_tiebreakers clause⇩G) UNIV"
    using wellfounded_typed_tiebreakers
    by simp
qed

end

sublocale first_order_superposition_calculus ⊆
  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_groundings typeof_fun" 
    "λselect⇩G. Some ∘
      (grounded_first_order_superposition_calculus.inference_groundings (≺⇩t) select⇩G typeof_fun)"
    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_first_order_superposition_calculus
    where select⇩G = select⇩G
    apply unfold_locales
    by(simp add: select⇩G⇩s_def)

  show "consequence_relation ground.G_Bot ground.G_entails"
    using ground.consequence_relation_axioms.
next
   fix select⇩G
   assume "select⇩G ∈ select⇩G⇩s"
 
   then interpret grounded_first_order_superposition_calculus
    where select⇩G = select⇩G
    by unfold_locales (simp add: select⇩G⇩s_def)

  show "tiebreaker_lifting
          ⊥⇩F
          inferences 
          ground.G_Bot
          ground.G_entails
          ground.G_Inf 
          ground.GRed_I
          ground.GRed_F 
          (clause_groundings typeof_fun)
          (Some ∘ inference_groundings)
          typed_tiebreakers"
    by unfold_locales
qed

end