Theory First_Order_Superposition_Soundness

theory First_Order_Superposition_Soundness
  imports Grounded_First_Order_Superposition

begin

subsection ‹Soundness›

context grounded_first_order_superposition_calculus
begin

abbreviation entailsF (infix "⊫F" 50) where
  "entailsF ≡ lifting.entails_𝒢"

lemma welltyped_extension:
  assumes "clause.is_ground (C ⋅ γ)" "welltypedσ_on (clause.vars C) typeof_fun 𝒱 γ" 
  obtains γ'
  where 
    "term_subst.is_ground_subst γ'" 
    "welltypedσ typeof_fun 𝒱 γ'" 
    "∀x ∈ clause.vars C. γ x = γ' x"
  using assms function_symbols
proof-
  define γ' where "⋀x. γ' x ≡ 
    if x ∈ clause.vars C 
    then γ x else 
    Fun (SOME f. typeof_fun f = ([], 𝒱 x)) []"

  have "term_subst.is_ground_subst γ'"
    unfolding  term_subst.is_ground_subst_def
  proof(intro allI)
    fix t
    show "term.is_ground (t ⋅t γ')"
    proof(induction t)
      case (Var x)
      then show ?case
        using assms(1) 
        unfolding γ'_def  term_subst.is_ground_subst_def  is_ground_iff
        by(auto simp: clause.variable_grounding)
    next
      case Fun
      then show ?case
        by simp
    qed
  qed

  moreover have "welltypedσ typeof_fun 𝒱 γ'"
  proof-
    have "⋀x. ⟦∀x∈clause.vars C. First_Order_Type_System.welltyped typeof_fun 𝒱 (γ x) (𝒱 x);
          ⋀τ. ∃f. typeof_fun f = ([], τ); x ∉ clause.vars C⟧
         ⟹ First_Order_Type_System.welltyped typeof_fun 𝒱
              (Fun (SOME f. typeof_fun f = ([], 𝒱 x)) []) (𝒱 x)"
      by (meson First_Order_Type_System.welltyped.intros(2) list_all2_Nil someI_ex)

    then show ?thesis    
      using assms(2) function_symbols
      unfolding γ'_def welltypedσ_def welltypedσ_on_def
      by auto
  qed

  moreover have "∀x ∈ clause.vars C. γ x = γ' x"
    unfolding γ'_def
    by auto

  ultimately show ?thesis
    using that
    by blast
qed

lemma vars_subst: "⋃ (term.vars ` ρ ` term.vars t) = term.vars (t ⋅t ρ)"
  by(induction t) auto

lemma vars_substa: "⋃ (term.vars ` ρ ` atom.vars a) = atom.vars (a ⋅a ρ)"
  using vars_subst
  unfolding atom.vars_def atom.subst_def
  by (smt (verit) SUP_UNION Sup.SUP_cong UN_extend_simps(10) uprod.set_map)

lemma vars_substl: "⋃ (term.vars ` ρ ` literal.vars l) = literal.vars (l ⋅l ρ)"
  unfolding literal.vars_def literal.subst_def set_literal_atm_of
  by (metis (no_types, lifting) UN_insert Union_image_empty literal.map_sel vars_substa)

lemma vars_substc: "⋃ (term.vars ` ρ ` clause.vars C) = clause.vars (C ⋅ ρ)"
  using vars_substl
  unfolding clause.vars_def clause.subst_def
  by fastforce

lemma eq_resolution_sound:
  assumes step: "eq_resolution P C"
  shows "{P} ⊫F {C}"
  using step
proof (cases P C rule: eq_resolution.cases)
  case (eq_resolutionI P L P' s1 s2 μ 𝒱 C)

  { 
    fix I :: "'f gterm rel" and γ :: "('f, 'v) subst"

    let ?I = "upair ` I"

    assume
      refl_I: "refl I" and 
      premise: 
      "∀PG. (∃γ'. PG = clause.to_ground (P ⋅ γ') ∧ term_subst.is_ground_subst γ'
             ∧ welltypedc typeof_fun 𝒱 P ∧ welltypedσ_on (clause.vars P) typeof_fun 𝒱 γ') 
            ⟶ ?I ⊫ PG" and
      grounding: "term_subst.is_ground_subst γ" and
      wt: "welltypedc typeof_fun 𝒱 C" "welltypedσ_on (clause.vars C) typeof_fun 𝒱 γ"

    have grounding': "clause.is_ground (C ⋅ γ)"
      using grounding
      by (simp add: clause.is_ground_subst_is_ground)

    obtain γ' where
      γ': "term_subst.is_ground_subst γ'" "welltypedσ typeof_fun 𝒱 γ'" 
      "∀x ∈ clause.vars C. γ x = γ' x"
      using welltyped_extension[OF grounding' wt(2)].

    let ?P = "clause.to_ground (P ⋅ μ ⋅ γ')"
    let ?L = "literal.to_ground (L ⋅l μ ⋅l γ')"
    let ?P' = "clause.to_ground (P' ⋅ μ ⋅ γ')"
    let ?s1 = "term.to_ground (s1 ⋅t μ ⋅t γ')"
    let ?s2 = "term.to_ground (s2 ⋅t μ ⋅t γ')"

    have "welltypedc typeof_fun 𝒱 (P' ⋅ μ)"
      using eq_resolutionI(8) wt(1)
      by blast

    moreover have welltyped_μ: "welltypedσ typeof_fun 𝒱 μ"
      using eq_resolutionI(6) wt(1)
      by auto

    ultimately have welltyped_P': "welltypedc typeof_fun 𝒱 P'"
      using welltypedσ_welltypedc
      by blast

    from welltyped_μ have "welltypedσ_on (clause.vars C) typeof_fun 𝒱 (μ ⊙ γ')"
      using γ'(2)
      by (simp add: subst_compose_def welltypedσ_def welltypedσ_on_def welltypedσ_welltyped)

    moreover have "welltypedc typeof_fun 𝒱 (add_mset (s1 !≈ s2) P')"
      using eq_resolutionI(6) welltyped_add_literal[OF welltyped_P'] wt(1)
      by auto

    ultimately have "?I ⊫ ?P"
      using premise[rule_format, of ?P, OF exI, of "μ ⊙ γ'"] γ'(1) 
        term_subst.is_ground_subst_comp_right eq_resolutionI
      by (smt (verit, ccfv_threshold) γ'(2) clause.comp_subst.left.monoid_action_compatibility 
          subst_compose_def welltypedσ_def welltypedσ_on_def welltypedσ_welltyped)

    then obtain L' where L'_in_P: "L' ∈# ?P" and I_models_L': "?I ⊫l L'"
      by (auto simp: true_cls_def)

    have [simp]: "?P = add_mset ?L ?P'"
      by (simp add: clause.to_ground_def eq_resolutionI(3) subst_clause_add_mset)

    have [simp]: "?L = (Neg (Upair ?s1 ?s2))"
      unfolding  eq_resolutionI(4) atom.to_ground_def literal.to_ground_def
      by clause_auto

    have [simp]: "?s1 = ?s2"
      using term_subst.subst_imgu_eq_subst_imgu[OF eq_resolutionI(5)] by simp

    have "is_neg ?L"
      by (simp add: literal.to_ground_def eq_resolutionI(4) subst_literal)

    have "?I ⊫ clause.to_ground (C ⋅ γ)"
    proof(cases "L' = ?L")
      case True

      then have "?I ⊫l (Neg (atm_of ?L))"
        using I_models_L' by simp

      moreover have "atm_of L' ∈ ?I"
        using True reflD[OF refl_I, of ?s1] by auto

      ultimately show ?thesis
        using True by blast
    next
      case False
      then have "L' ∈# clause.to_ground (P' ⋅ μ ⋅ γ')"
        using L'_in_P by force

      then have "L' ∈# clause.to_ground (C ⋅ γ')"
        unfolding eq_resolutionI.

      then show ?thesis
        using I_models_L' 
        by (metis γ'(3) clause.subst_eq true_cls_def)
    qed
  }

  then show ?thesis
    unfolding ground.G_entails_def true_clss_def clause_groundings_def
    using eq_resolutionI(1, 2) by auto
qed

lemma eq_factoring_sound:
  assumes step: "eq_factoring P C"
  shows "{P} ⊫F {C}"
  using step
proof (cases P C rule: eq_factoring.cases)
  case (eq_factoringI P L1 L2 P' s1 s1' t2 t2' μ 𝒱 C)

  have  
    "⋀I γ ℱG. ⟦
        trans I; 
        sym I;
        ∀PG. (∃γ'. PG = clause.to_ground (P ⋅ γ') ∧ term_subst.is_ground_subst γ'
              ∧ welltypedc typeof_fun 𝒱 P ∧ welltypedσ_on (clause.vars P) typeof_fun 𝒱 γ') 
            ⟶ upair ` I ⊫ PG; 
       term_subst.is_ground_subst γ;
       welltypedc typeof_fun 𝒱 C; welltypedσ_on (clause.vars C) typeof_fun 𝒱 γ
     ⟧ ⟹ upair  ` I ⊫ clause.to_ground (C ⋅ γ)"
  proof-
    fix I :: "'f gterm rel" and γ :: "'v ⇒ ('f, 'v) Term.term"

    let ?I = "upair ` I"

    assume
      trans_I: "trans I" and 
      sym_I: "sym I" and 
      premise: 
      "∀PG. (∃γ'. PG = clause.to_ground (P ⋅ γ') ∧ term_subst.is_ground_subst γ'
             ∧ welltypedc typeof_fun 𝒱 P ∧ welltypedσ_on (clause.vars P) typeof_fun 𝒱 γ') 
              ⟶ ?I ⊫ PG" and
      grounding: "term_subst.is_ground_subst γ" and
      wt: "welltypedc typeof_fun 𝒱 C" "welltypedσ_on (clause.vars C) typeof_fun 𝒱 γ"

    obtain γ' where
      γ': "term_subst.is_ground_subst γ'" "welltypedσ typeof_fun 𝒱 γ'" 
      "∀x ∈ clause.vars C. γ x = γ' x"
      using welltyped_extension
      using grounding wt(2)
      by (smt (verit, ccfv_threshold) clause.ground_subst_iff_base_ground_subst 
          clause.is_ground_subst_is_ground)

    let ?P = "clause.to_ground (P ⋅ μ ⋅ γ')"
    let ?P' = "clause.to_ground (P' ⋅ μ ⋅ γ')"
    let ?L1 = "literal.to_ground (L1 ⋅l μ ⋅l γ')"
    let ?L2 = "literal.to_ground (L2 ⋅l μ ⋅l γ')"
    let ?s1 = "term.to_ground (s1 ⋅t μ ⋅t γ')"
    let ?s1' = "term.to_ground (s1' ⋅t μ ⋅t γ')"
    let ?t2 = "term.to_ground (t2 ⋅t μ ⋅t γ')"
    let ?t2' = "term.to_ground (t2' ⋅t μ ⋅t γ')"
    let ?C = "clause.to_ground (C ⋅ γ')"

    have wt':
      "welltypedc typeof_fun 𝒱 (P' ⋅ μ)" 
      "welltypedl typeof_fun 𝒱 (s1 ≈ t2' ⋅l μ)" 
      "welltypedl typeof_fun 𝒱 (s1' !≈ t2' ⋅l μ)"
      using wt(1)
      unfolding eq_factoringI(11) welltypedc_add_mset subst_clause_add_mset
      by auto

    moreover have welltyped_μ: "welltypedσ typeof_fun 𝒱 μ"
      using eq_factoringI(10) wt(1)
      by blast

    ultimately have welltyped_P': "welltypedc typeof_fun 𝒱 P'"
      using welltypedσ_welltypedc
      by blast

    have xx: "welltypedl typeof_fun 𝒱 (s1 ≈ t2')" "welltypedl typeof_fun 𝒱 (s1' !≈ t2')"
      using wt'(2, 3) welltypedσ_welltypedl[OF welltyped_μ]
      by auto

    then have welltyped_L1: "welltypedl typeof_fun 𝒱 (s1 ≈ s1')"
      unfolding welltypedl_def welltypeda_def
      using right_uniqueD[OF welltyped_right_unique] 
      by (smt (verit, best) insert_iff set_uprod_simps literal.sel)

    have welltyped_L2: "welltypedl typeof_fun 𝒱 (t2 ≈ t2')"
      using xx right_uniqueD[OF welltyped_right_unique] eq_factoringI(10) wt(1)
      unfolding welltypedl_def welltypeda_def
      by (smt (verit) insert_iff set_uprod_simps literal.sel(1))

    from welltyped_μ have "welltypedσ typeof_fun 𝒱 (μ ⊙ γ')"
      using wt(2) γ'
      by (simp add: subst_compose_def welltypedσ_def welltypedσ_welltyped)

    moreover have "welltypedc typeof_fun 𝒱 P"
      unfolding eq_factoringI welltypedc_add_mset
      using welltyped_P'  welltyped_L1 welltyped_L2
      by blast

    ultimately have "?I ⊫ ?P"
      using 
        premise[rule_format, of ?P, OF exI, of "μ ⊙ γ'"] 
        term_subst.is_ground_subst_comp_right γ'(1)
      by (metis clause.subst_comp_subst welltypedσ_def welltypedσ_on_def)

    then obtain L' where L'_in_P: "L' ∈# ?P" and I_models_L': "?I ⊫l L'"
      by (auto simp: true_cls_def)

    then have s1_equals_t2: "?t2 = ?s1"
      using term_subst.subst_imgu_eq_subst_imgu[OF eq_factoringI(9)]
      by simp

    have L1: "?L1 = ?s1 ≈ ?s1'"
      unfolding literal.to_ground_def eq_factoringI(4) atom.to_ground_def
      by (simp add: atom.subst_def subst_literal)

    have L2: "?L2 = ?t2 ≈ ?t2'"
      unfolding literal.to_ground_def eq_factoringI(5) atom.to_ground_def
      by (simp add: atom.subst_def subst_literal)

    have C: "?C = add_mset (?s1 ≈ ?t2') (add_mset (Neg (Upair ?s1' ?t2')) ?P')"
      unfolding eq_factoringI 
      by (simp add: clause.to_ground_def literal.to_ground_def atom.subst_def subst_clause_add_mset 
          subst_literal atom.to_ground_def)

    show "?I ⊫ clause.to_ground (C ⋅ γ)"
    proof(cases "L' = ?L1 ∨ L' = ?L2")
      case True

      then have "I ⊫l Pos (?s1, ?s1') ∨ I ⊫l Pos (?s1, ?t2')"
        using true_lit_uprod_iff_true_lit_prod[OF sym_I] I_models_L'
        by (metis L1 L2 s1_equals_t2)

      then have "I ⊫l Pos (?s1, ?t2') ∨ I ⊫l Neg (?s1', ?t2')"
        by (meson transD trans_I true_lit_simps(1) true_lit_simps(2))

      then have "?I ⊫l ?s1 ≈ ?t2' ∨ ?I ⊫l Neg (Upair ?s1' ?t2')"
        unfolding true_lit_uprod_iff_true_lit_prod[OF sym_I].

      then show ?thesis
        using clause.subst_eq γ'(3) C
        by (smt (verit, best) true_cls_add_mset)
    next
      case False
      then have "L' ∈# ?P'"
        using L'_in_P
        unfolding eq_factoringI
        by (simp add: clause.to_ground_def subst_clause_add_mset)

      then have "L' ∈# clause.to_ground (C ⋅ γ)"
        using clause.subst_eq γ'(3) C
        by fastforce

      then show ?thesis
        using I_models_L' by blast
    qed
  qed

  then show ?thesis
    unfolding ground.G_entails_def true_clss_def clause_groundings_def
    using eq_factoringI(1,2) by auto
qed

lemma superposition_sound:
  assumes step: "superposition P2 P1 C"
  shows "{P1, P2} ⊫F {C}"
  using step
proof (cases P2 P1 C rule: superposition.cases)
  case (superpositionI ρ1 ρ2 P1  P2 L1 P1' L2 P2' 𝒫 s1 u1 s1' t2 t2' μ 𝒱3 𝒱1 𝒱2 C)

  have 
    "⋀I γ. ⟦
        refl I;
        trans I; 
        sym I;
        compatible_with_gctxt I;
        ∀PG. (∃γ'. PG = clause.to_ground (P1 ⋅ γ') ∧ term_subst.is_ground_subst γ' ∧ 
              welltypedc typeof_fun 𝒱1 P1 ∧ welltypedσ_on (clause.vars P1) typeof_fun 𝒱1 γ' ∧ 
              all_types 𝒱1) ⟶ upair ` I ⊫ PG;
        ∀PG. (∃γ'. PG = clause.to_ground (P2 ⋅ γ') ∧ term_subst.is_ground_subst γ' ∧ 
              welltypedc typeof_fun 𝒱2 P2 ∧ welltypedσ_on (clause.vars P2) typeof_fun 𝒱2 γ' ∧ 
              all_types 𝒱2) ⟶ upair ` I ⊫ PG;
        term_subst.is_ground_subst γ; welltypedc typeof_fun 𝒱3 C; 
        welltypedσ_on (clause.vars C) typeof_fun 𝒱3 γ; all_types 𝒱3
     ⟧ ⟹ (λ(x, y). Upair x y) ` I ⊫ clause.to_ground (C ⋅ γ)"
  proof -
    fix I :: "'f gterm rel" and γ :: "'v ⇒ ('f, 'v) Term.term"

    let ?I = "(λ(x, y). Upair x y) ` I"

    assume 
      refl_I: "refl I" and 
      trans_I: "trans I" and 
      sym_I: "sym I" and 
      compatible_with_ground_context_I: "compatible_with_gctxt I" and
      premise1: 
      "∀PG. (∃γ'. PG = clause.to_ground (P1 ⋅ γ') ∧ term_subst.is_ground_subst γ' 
              ∧ welltypedc typeof_fun 𝒱1 P1 ∧ welltypedσ_on (clause.vars P1) typeof_fun 𝒱1 γ' 
              ∧ all_types 𝒱1) ⟶?I ⊫ PG" and
      premise2: 
      "∀PG. (∃γ'. PG = clause.to_ground (P2 ⋅ γ') ∧ term_subst.is_ground_subst γ' 
              ∧ welltypedc typeof_fun 𝒱2 P2 ∧ welltypedσ_on (clause.vars P2) typeof_fun 𝒱2 γ'
              ∧ all_types 𝒱2) ⟶ ?I ⊫ PG" and 
      grounding: "term_subst.is_ground_subst γ" "welltypedc typeof_fun 𝒱3 C" 
      "welltypedσ_on (clause.vars C) typeof_fun 𝒱3 γ" "all_types 𝒱3"

    have grounding': "clause.is_ground (C ⋅ γ)"
      using grounding
      by (simp add: clause.is_ground_subst_is_ground)

    obtain γ' where
      γ': "term_subst.is_ground_subst γ'" "welltypedσ typeof_fun 𝒱3 γ'" 
      "∀x ∈ clause.vars C. γ x = γ' x"
      using welltyped_extension[OF grounding' grounding(3)].

    let ?P1 = "clause.to_ground (P1 ⋅ ρ1⋅ μ ⋅ γ')"
    let ?P2 = "clause.to_ground (P2 ⋅ ρ2 ⋅ μ ⋅ γ')"

    let ?L1 = "literal.to_ground (L1 ⋅l ρ1 ⋅l μ ⋅l γ')"
    let ?L2 = "literal.to_ground (L2 ⋅l ρ2 ⋅l μ ⋅l γ')"

    let ?P1' = "clause.to_ground (P1' ⋅ ρ1 ⋅ μ ⋅ γ')"
    let ?P2' = "clause.to_ground (P2' ⋅ ρ2 ⋅ μ ⋅ γ')"

    let ?s1 = "context.to_ground (s1 ⋅tc ρ1 ⋅tc μ ⋅tc γ')"
    let ?s1' = "term.to_ground (s1' ⋅t ρ1 ⋅t μ ⋅t γ')"
    let ?t2 = "term.to_ground (t2 ⋅t ρ2 ⋅t μ ⋅t γ')"
    let ?t2' = "term.to_ground (t2' ⋅t ρ2 ⋅t μ ⋅t γ')"
    let ?u1 = "term.to_ground (u1 ⋅t ρ1 ⋅t μ ⋅t γ')"

    let ?𝒫 = "if 𝒫 = Pos then Pos else Neg"

    let ?C = "clause.to_ground (C ⋅ γ')"

    have ground_subst: 
      "term_subst.is_ground_subst (ρ1 ⊙ μ ⊙ γ')" 
      "term_subst.is_ground_subst (ρ2 ⊙ μ ⊙ γ')"
      "term_subst.is_ground_subst (μ ⊙ γ')"
      using term_subst.is_ground_subst_comp_right[OF γ'(1)]
      by blast+

    have xx: "∀x∈term.vars (t2 ⋅t ρ2). 𝒱2 (the_inv ρ2 (Var x)) = 𝒱3 x" 
      "∀x∈term.vars (t2' ⋅t ρ2). 𝒱2 (the_inv ρ2 (Var x)) = 𝒱3 x"
      using superpositionI(16)
      by (simp_all add: clause.vars_def local.superpositionI(11) local.superpositionI(8) 
          subst_atom subst_clause_add_mset subst_literal(1) vars_atom vars_literal(1))

    have wt_t: "∃τ. welltyped typeof_fun 𝒱3 (t2 ⋅t ρ2) τ ∧ welltyped typeof_fun 𝒱3 (t2' ⋅t ρ2 ⋅t μ) τ"
    proof-
      have " ⋀τ τ'.
       ⟦⋀τ τ'.
           ⟦has_type typeof_fun 𝒱3 (t2 ⋅t ρ2) τ; has_type typeof_fun 𝒱3 (t2' ⋅t ρ2) τ'⟧ ⟹ τ = τ';
        ∀L∈#(P1' ⋅ ρ1 + P2' ⋅ ρ2) ⋅ μ.
           ∃τ. ∀t∈set_uprod (atm_of L). First_Order_Type_System.welltyped typeof_fun 𝒱3 t τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱3 (u1 ⋅t ρ1) τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱3 (t2 ⋅t ρ2) τ; welltypedσ typeof_fun 𝒱3 μ;
        𝒫 = Pos;
        First_Order_Type_System.welltyped typeof_fun 𝒱3
         (s1 ⋅tc ρ1 ⋅tc μ)⟨t2' ⋅t ρ2 ⋅t μ⟩ τ';
        First_Order_Type_System.welltyped typeof_fun 𝒱3 (s1' ⋅t ρ1 ⋅t μ) τ'⟧
       ⟹ ∃τ. First_Order_Type_System.welltyped typeof_fun 𝒱3 (t2 ⋅t ρ2) τ ∧
               First_Order_Type_System.welltyped typeof_fun 𝒱3 (t2' ⋅t ρ2 ⋅t μ) τ"
        "⋀τ τ'.
       ⟦⋀τ τ'.
           ⟦has_type typeof_fun 𝒱3 (t2 ⋅t ρ2) τ; has_type typeof_fun 𝒱3 (t2' ⋅t ρ2) τ'⟧ ⟹ τ = τ';
        ∀L∈#(P1' ⋅ ρ1 + P2' ⋅ ρ2) ⋅ μ.
           ∃τ. ∀t∈set_uprod (atm_of L). First_Order_Type_System.welltyped typeof_fun 𝒱3 t τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱3 (u1 ⋅t ρ1) τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱3 (t2 ⋅t ρ2) τ; welltypedσ typeof_fun 𝒱3 μ;
        𝒫 = Neg;
        First_Order_Type_System.welltyped typeof_fun 𝒱3 (s1 ⋅tc ρ1 ⋅tc μ)⟨t2' ⋅t ρ2 ⋅t μ⟩ τ';
        First_Order_Type_System.welltyped typeof_fun 𝒱3 (s1' ⋅t ρ1 ⋅t μ) τ'⟧
       ⟹ ∃τ. First_Order_Type_System.welltyped typeof_fun 𝒱3 (t2 ⋅t ρ2) τ ∧
               First_Order_Type_System.welltyped typeof_fun 𝒱3 (t2' ⋅t ρ2 ⋅t μ) τ"
        by (metis welltypedκ' welltypedσ_welltyped welltyped_has_type)+

      then show ?thesis
        using grounding(2) superpositionI(9, 14, 19)
        unfolding superpositionI welltypedc_def welltypedl_def welltypeda_def subst_clause_add_mset
        unfolding xx[THEN has_type_renaming_weaker[OF superpositionI(5)]] 
        by(auto simp: welltypedκ' subst_literal subst_atom)
    qed

    have wt_P1: "welltypedc typeof_fun 𝒱1 P1" 
    proof-
      have xx: "∀x∈clause.vars (P1' ⋅ ρ1). 𝒱1 (the_inv ρ1 (Var x)) = 𝒱3 x"
        using superpositionI(15)
        unfolding superpositionI subst_clause_add_mset
        by clause_simp

      have wt_P1': "welltypedc typeof_fun 𝒱1 P1'"
      proof-
        have "⟦welltypedl typeof_fun 𝒱3 (𝒫 (Upair (s1 ⋅tc ρ1)⟨t2' ⋅t ρ2⟩ (s1' ⋅t ρ1)) ⋅l μ);
             welltypedc typeof_fun 𝒱3 (P1' ⋅ ρ1 ⋅ μ);
             welltypedc typeof_fun 𝒱3 (P2' ⋅ ρ2 ⋅ μ)⟧
             ⟹ welltypedc typeof_fun 𝒱1 P1'"
          unfolding welltypedc_renaming_weaker[OF superpositionI(4) xx] 
          using superpositionI(14) welltypedσ_welltypedc 
          by blast

        then show ?thesis
          using grounding(2)
          unfolding superpositionI subst_clause_add_mset subst_clause_plus welltypedc_add_mset 
            welltypedc_plus
          by auto
      qed

      from wt_t have x1:
        "∃τ. welltyped typeof_fun 𝒱3 (s1 ⋅tc ρ1)⟨u1 ⋅t ρ1⟩ τ ∧ welltyped typeof_fun 𝒱3 (s1' ⋅t ρ1) τ"
      proof-
        have "∃τ. welltyped typeof_fun 𝒱3 (s1 ⋅tc ρ1 ⋅tc μ)⟨t2' ⋅t ρ2 ⋅t μ⟩ τ ∧
               welltyped typeof_fun 𝒱3 (s1' ⋅t ρ1 ⋅t μ) τ"
          using grounding(2) superpositionI(9, 14, 15) 
          unfolding superpositionI welltypedc_def welltypedl_def welltypeda_def
          by clause_auto

        then have "∃τ. welltyped typeof_fun 𝒱3 (s1 ⋅tc ρ1 ⋅tc μ)⟨u1 ⋅t ρ1 ⋅t μ⟩ τ ∧
               welltyped typeof_fun 𝒱3 (s1' ⋅t ρ1 ⋅t μ) τ"
          by (meson local.superpositionI(14) welltypedκ welltypedσ_welltyped wt_t)

        then show ?thesis
          by (metis local.superpositionI(14) subst_apply_term_ctxt_apply_distrib 
              welltypedσ_welltyped)
      qed

      then have "∃τ. welltyped typeof_fun 𝒱1 s1⟨u1⟩ τ ∧ welltyped typeof_fun 𝒱1 s1' τ"
      proof-
        have x1': " ⋀τ. ⟦∀x∈literal.vars ((s1 ⋅tc ρ1)⟨u1 ⋅t ρ1⟩ ≈ s1' ⋅t ρ1) ∪ clause.vars (P1' ⋅ ρ1).
             𝒱1 (the_inv ρ1 (Var x)) = 𝒱3 x;
          ⋀t 𝒱 𝒱' ℱ τ.
             ∀x∈term.vars (t ⋅t ρ1). 𝒱 (the_inv ρ1 (Var x)) = 𝒱' x ⟹
             First_Order_Type_System.welltyped ℱ 𝒱 t τ =
             First_Order_Type_System.welltyped ℱ 𝒱' (t ⋅t ρ1) τ;
          First_Order_Type_System.welltyped typeof_fun 𝒱3 (s1 ⋅tc ρ1)⟨u1 ⋅t ρ1⟩ τ;
          First_Order_Type_System.welltyped typeof_fun 𝒱3 (s1' ⋅t ρ1) τ; 𝒫 = Pos⟧
         ⟹ ∃τ. First_Order_Type_System.welltyped typeof_fun 𝒱1 s1⟨u1⟩ τ ∧
                 First_Order_Type_System.welltyped typeof_fun 𝒱1 s1' τ"
          "⋀τ. ⟦∀x∈literal.vars ((s1 ⋅tc ρ1)⟨u1 ⋅t ρ1⟩ !≈ s1' ⋅t ρ1) ∪ clause.vars (P1' ⋅ ρ1).
             𝒱1 (the_inv ρ1 (Var x)) = 𝒱3 x;
          ⋀t 𝒱 𝒱' ℱ τ.
             ∀x∈term.vars (t ⋅t ρ1). 𝒱 (the_inv ρ1 (Var x)) = 𝒱' x ⟹
             First_Order_Type_System.welltyped ℱ 𝒱 t τ =
             First_Order_Type_System.welltyped ℱ 𝒱' (t ⋅t ρ1) τ;
          First_Order_Type_System.welltyped typeof_fun 𝒱3 (s1 ⋅tc ρ1)⟨u1 ⋅t ρ1⟩ τ;
          First_Order_Type_System.welltyped typeof_fun 𝒱3 (s1' ⋅t ρ1) τ; 𝒫 = Neg⟧
         ⟹ ∃τ. First_Order_Type_System.welltyped typeof_fun 𝒱1 s1⟨u1⟩ τ ∧
                 First_Order_Type_System.welltyped typeof_fun 𝒱1 s1' τ"
          by clause_simp (metis (mono_tags) Un_iff welltyped_renaming_weaker[OF superpositionI(4)] 
              subst_apply_term_ctxt_apply_distrib vars_term_ctxt_apply)+

        with x1 show ?thesis
          using superpositionI(15)  superpositionI(9) 
            welltyped_renaming_weaker[OF superpositionI(4)] 
          unfolding superpositionI subst_clause_add_mset vars_clause_add_mset
          by(auto simp: welltypedκ' subst_literal subst_atom)
      qed

      then show ?thesis
        using grounding(2) superpositionI(9, 14) wt_P1'
        unfolding superpositionI welltypedc_def welltypedl_def welltypeda_def subst_clause_add_mset 
          subst_clause_plus
        by auto
    qed

    have wt_P2: "welltypedc typeof_fun 𝒱2 P2"
    proof-
      have xx: "∀x∈clause.vars (P2' ⋅ ρ2). 𝒱2 (the_inv ρ2 (Var x)) = 𝒱3 x"
        using superpositionI(16)
        unfolding superpositionI subst_clause_add_mset
        by clause_simp

      have wt_P2': "welltypedc typeof_fun 𝒱2 P2'"
        using grounding(2)
        unfolding superpositionI subst_clause_add_mset subst_clause_plus welltypedc_add_mset 
          welltypedc_plus welltypedc_renaming_weaker[OF superpositionI(5) xx] 
        using superpositionI(14) welltypedσ_welltypedc by blast

      have tt: "∃τ. welltyped typeof_fun 𝒱3 (t2 ⋅t ρ2) τ ∧ welltyped typeof_fun 𝒱3 (t2' ⋅t ρ2) τ"
        using wt_t
        by (meson superpositionI(14) welltypedσ_welltyped)

      show ?thesis
      proof-
        have "∃τ. welltyped typeof_fun 𝒱2 t2 τ ∧ welltyped typeof_fun 𝒱2 t2' τ"
          using superpositionI(16) welltyped_renaming_weaker[OF superpositionI(5)]
          unfolding superpositionI
          by (metis (no_types, lifting) Un_iff subst_atom subst_clause_add_mset subst_literal(1) tt 
              vars_atom vars_clause_add_mset vars_literal(1))

        with wt_P2' show ?thesis
          unfolding welltypedc_def welltypedl_def welltypeda_def  superpositionI
          by auto
      qed
    qed

    have wt_μ_γ: "welltypedσ typeof_fun 𝒱3 (μ ⊙ γ')"
      by (metis γ'(2) local.superpositionI(14) subst_compose_def welltypedσ_def 
          welltypedσ_welltyped)

    have wt_γ: "welltypedσ_on  (clause.vars P1) typeof_fun 𝒱1 (ρ1 ⊙ μ ⊙ γ')" 
      "welltypedσ_on (clause.vars P2) typeof_fun 𝒱2 (ρ2 ⊙  μ ⊙ γ')"
      using
        superpositionI(15, 16)
        welltypedσ_renaming_ground_subst_weaker[OF superpositionI(4) wt_μ_γ superpositionI(17) 
          ground_subst(3)]
        welltypedσ_renaming_ground_subst_weaker[OF superpositionI(5) wt_μ_γ superpositionI(18)
          ground_subst(3)]
      unfolding vars_substc
      by (simp_all add: subst_compose_assoc)

    have "?I ⊫ ?P1"
      using premise1[rule_format, of ?P1, OF exI, of "ρ1 ⊙ μ ⊙ γ'"] ground_subst wt_P1 wt_γ 
        superpositionI(27)
      by auto

    moreover have "?I ⊫ ?P2"
      using premise2[rule_format, of ?P2, OF exI, of "ρ2 ⊙ μ ⊙ γ'"] ground_subst wt_P2 wt_γ 
        superpositionI(28)
      by auto

    ultimately obtain L1' L2' 
      where
        L1'_in_P1: "L1' ∈# ?P1" and 
        I_models_L1': "?I ⊫l L1'" and
        L2'_in_P2: "L2' ∈# ?P2" and 
        I_models_L2': "?I ⊫l L2'"
      by (auto simp: true_cls_def)

    have u1_equals_t2: "?t2 = ?u1"
      using term_subst.subst_imgu_eq_subst_imgu[OF superpositionI(13)]
      by argo

    have s1_u1: "?s1⟨?u1⟩G = term.to_ground (s1 ⋅tc ρ1 ⋅tc μ ⋅tc γ')⟨u1 ⋅t ρ1 ⋅t μ ⋅t γ'⟩"
      using 
        ground_term_with_context(1)[OF 
          context.is_ground_subst_is_ground
          term_subst.is_ground_subst_is_ground
          ]
        γ'(1)
      by auto

    have s1_t2': "(?s1)⟨?t2'⟩G  = term.to_ground (s1 ⋅tc ρ1 ⋅tc μ ⋅tc γ')⟨t2' ⋅t ρ2 ⋅t μ ⋅t γ'⟩"
      using 
        ground_term_with_context(1)[OF 
          context.is_ground_subst_is_ground
          term_subst.is_ground_subst_is_ground
          ]
        γ'(1) 
      by auto

    have 𝒫_pos_or_neg: "𝒫 = Pos ∨ 𝒫 = Neg"
      using superpositionI(9) by blast

    then have L1: "?L1 = ?𝒫 (Upair ?s1⟨?u1⟩G ?s1')"
      using s1_u1
      unfolding superpositionI literal.to_ground_def atom.to_ground_def
      by clause_auto   

    have "literal.to_ground
         ((s1 ⋅tc ρ1 ⋅tc μ ⋅tc γ')⟨t2' ⋅t ρ2 ⋅t μ ⋅t γ'⟩ ≈ s1' ⋅t ρ1 ⋅t μ ⋅t γ') =
        term.to_ground (s1 ⋅tc ρ1 ⋅tc μ ⋅tc γ')⟨t2' ⋅t ρ2 ⋅t μ ⋅t γ'⟩ ≈
        term.to_ground (s1' ⋅t ρ1 ⋅t μ ⋅t γ')"
      by (metis atom.to_ground_def ground_atom_in_ground_literal(1) map_uprod_simps)

    moreover have "literal.to_ground
         ((s1 ⋅tc ρ1 ⋅tc μ ⋅tc γ')⟨t2' ⋅t ρ2 ⋅t μ ⋅t γ'⟩ !≈ s1' ⋅t ρ1 ⋅t μ ⋅t γ') =
        term.to_ground (s1 ⋅tc ρ1 ⋅tc μ ⋅tc γ' )⟨t2' ⋅t ρ2 ⋅t μ ⋅t γ'⟩ !≈
        term.to_ground (s1' ⋅t ρ1 ⋅t μ ⋅t γ')"
      by (metis atom.to_ground_def ground_atom_in_ground_literal(2) map_uprod_simps)

    ultimately have C: "?C = add_mset (?𝒫 (Upair (?s1)⟨?t2'⟩G (?s1'))) (?P1' + ?P2')"
      using 𝒫_pos_or_neg
      unfolding 
        s1_t2' 
        superpositionI 
        clause.to_ground_def 
        subst_clause_add_mset 
        subst_clause_plus 
      by (auto simp: subst_atom subst_literal)

    show "?I ⊫ clause.to_ground (C ⋅ γ)"
    proof (cases "L1' = ?L1")
      case L1'_def: True
      then have "?I ⊫l ?L1"
        using superpositionI
        using I_models_L1' by blast

      show ?thesis
      proof (cases "L2' = ?L2")
        case L2'_def: True

        then have ts_in_I: "(?t2, ?t2') ∈ I"
          using I_models_L2' true_lit_uprod_iff_true_lit_prod[OF sym_I] superpositionI(11)
          unfolding literal.to_ground_def  atom.to_ground_def  
          by (smt (verit) literal.simps(9) map_uprod_simps atom.subst_def subst_literal 
              true_lit_simps(1)) 

        have ?thesis if "𝒫 = Pos"
        proof -
          from that have "(?s1⟨?t2⟩G, ?s1') ∈ I"
            using I_models_L1' L1'_def L1 true_lit_uprod_iff_true_lit_prod[OF sym_I] u1_equals_t2
            unfolding superpositionI 
            by (smt (verit, best) true_lit_simps(1))

          then have "(?s1⟨?t2'⟩G, ?s1') ∈ I"
            using ts_in_I compatible_with_ground_context_I refl_I sym_I trans_I
            by (meson compatible_with_gctxtD refl_onD1 symD trans_onD)

          then have "?I ⊫l ?s1⟨?t2'⟩G  ≈ ?s1'"
            by blast

          then show ?thesis 
            unfolding C that
            by (smt (verit) C γ'(3) clause.subst_eq that true_cls_def union_single_eq_member)
        qed

        moreover have ?thesis if "𝒫 = Neg"
        proof -
          from that have "(?s1⟨?t2⟩G, ?s1') ∉ I"
            using I_models_L1' L1'_def L1 true_lit_uprod_iff_true_lit_prod[OF sym_I] u1_equals_t2
            unfolding superpositionI 
            by (smt (verit, ccfv_threshold) literals_distinct(2) true_lit_simps(2))

          then have "(?s1⟨?t2'⟩G, ?s1') ∉ I"
            using ts_in_I compatible_with_ground_context_I trans_I
            by (meson compatible_with_gctxtD transD)

          then have "?I ⊫l Neg (Upair ?s1⟨?t2'⟩G  ?s1')"
            by (meson true_lit_uprod_iff_true_lit_prod(2) sym_I true_lit_simps(2))

          then show ?thesis 
            unfolding C that
            by (smt (verit, best) C γ'(3) calculation clause.subst_eq true_cls_def 
                union_single_eq_member)
        qed

        ultimately show ?thesis
          using 𝒫_pos_or_neg by blast
      next
        case False
        then have "L2' ∈# ?P2'"
          using L2'_in_P2
          unfolding superpositionI
          by (simp add:  clause.to_ground_def subst_clause_add_mset)

        then have "?I ⊫ ?P2'"
          using I_models_L2' by blast

        then show ?thesis
          unfolding superpositionI 
          by (smt (verit, ccfv_SIG) C γ'(3) clause.subst_eq local.superpositionI(26) true_cls_union 
              union_mset_add_mset_left)
      qed
    next
      case False
      then have "L1' ∈# ?P1'"
        using L1'_in_P1
        unfolding superpositionI 
        by (simp add:  clause.to_ground_def  subst_clause_add_mset)

      then have "?I ⊫ ?P1'"
        using I_models_L1' by blast

      then show ?thesis 
        unfolding superpositionI
        by (smt (verit, best) C γ'(3) clause.subst_eq local.superpositionI(26) true_cls_union 
            union_mset_add_mset_right)
    qed
  qed

  then show ?thesis 
    unfolding ground.G_entails_def clause_groundings_def true_clss_def superpositionI(1-3)
    by auto
qed

end

sublocale grounded_first_order_superposition_calculus ⊆ 
  sound_inference_system inferences "⊥F" "(⊫F)"
proof unfold_locales
  fix ι
  assume "ι ∈ inferences"
  then show "set (prems_of ι) ⊫F {concl_of ι}"
    using 
      eq_factoring_sound
      eq_resolution_sound
      superposition_sound
    unfolding inferences_def ground.G_entails_def
    by auto
qed

sublocale first_order_superposition_calculus ⊆ 
  sound_inference_system inferences "⊥F" entails_𝒢
proof unfold_locales
  obtain selectG where selectG: "selectG ∈ selectGs"
    using Q_nonempty by blast

  then interpret grounded_first_order_superposition_calculus
    where selectG = selectG
    by unfold_locales (simp add: selectGs_def)

  show "⋀ι. ι ∈ inferences ⟹ entails_𝒢 (set (prems_of ι)) {concl_of ι}"
    using sound
    unfolding entails_def
    by blast
qed

end