Theory Superposition_Soundness

theory Superposition_Soundness
  imports
    First_Order_Clause.Nonground_Entailment
    
    Grounded_Superposition
    Superposition_Welltypedness_Preservation
begin

subsection ‹Soundness›

context grounded_superposition_calculus
begin

notation lifting.entails_𝒢 (infix "F" 50)

lemma eq_resolution_sound:
  assumes eq_resolution: "eq_resolution D C"
  shows "{D} F {C}"
  using eq_resolution
proof (cases D C rule: eq_resolution.cases)
  case (eq_resolutionI D l D' t t' 𝒱 μ C)

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

    let ?I = "upair ` I"

    assume
      refl_I: "refl I" and
      entails_groundings: "DG  clause_groundings (D, 𝒱). ?I  DG" and
      C_is_ground: "clause.is_ground (C  γ)" and
      C_is_welltyped: "clause.is_welltyped 𝒱 C" and
      γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars C) 𝒱 γ" and
      𝒱: "infinite_variables_per_type 𝒱"

    obtain γ' where
      γ'_is_ground_subst: "term_subst.is_ground_subst γ'" and
      γ'_is_welltyped: "term.subst.is_welltyped 𝒱 γ'" and
      γ'_γ: "x  clause.vars C. γ x = γ' x"
      using clause.is_welltyped.ground_subst_extension[OF C_is_ground γ_is_welltyped].

    let ?DG = "clause.to_ground (D  μ  γ')"
    let ?lG = "literal.to_ground (l ⋅l μ ⋅l γ')"
    let ?DG' = "clause.to_ground (D'  μ  γ')"
    let ?tG = "term.to_ground (t ⋅t μ ⋅t γ')"
    let ?tG' = "term.to_ground (t' ⋅t μ ⋅t γ')"

    have μ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱 μ"
      using eq_resolutionI
      by meson

    have "?DG  clause_groundings (D, 𝒱)"
    proof(unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv, intro exI conjI 𝒱)
      show "clause.to_ground (D  μ  γ') = clause.to_ground (D  μ  γ')"
        by simp
    next
      show "clause.is_ground (D  μ  γ')"
        using γ'_is_ground_subst clause.is_ground_subst_is_ground
        by auto
    next
      show "clause.is_welltyped 𝒱 D"
       using C_is_welltyped
       unfolding 
         eq_resolution_preserves_typing[OF eq_resolution[unfolded eq_resolutionI(1, 2)]].
    next
      show "term.subst.is_welltyped_on (clause.vars D) 𝒱 (μ  γ')"
        using γ'_is_welltyped μ_is_welltyped
        by (simp add: subst_compose_def)
    qed

    then have "?I  ?DG"
      using entails_groundings
      by auto 

    then obtain lG where lG_in_D: "lG ∈# ?DG" and I_models_lG: "?I ⊫l lG"
      by (auto simp: true_cls_def)

    have "lG  ?lG"
    proof(rule notI)
      assume "lG = ?lG"

      then have [simp]: "lG = ?tG !≈ ?tG'"
        unfolding eq_resolutionI
        by simp

      moreover have "atm_of lG  ?I"
      proof-
        have "?tG = ?tG'"
          using eq_resolutionI(5) term_subst.is_imgu_unifies_pair
          by metis

        then show ?thesis
          using reflD[OF refl_I, of ?tG]
          by auto
      qed

      ultimately show False
        using I_models_lG
        by auto
    qed

    then have "lG ∈# clause.to_ground (C  γ')"
      using lG_in_D
      unfolding eq_resolutionI
      by simp

    then have "?I  clause.to_ground (C  γ)"
      using clause.subst_eq[OF γ'_γ[rule_format]] I_models_lG
      by auto
  }
  
  then show ?thesis
    unfolding
      true_clss_def 
      eq_resolutionI(1,2)
      clause_groundings_def
      ground.G_entails_def
    by auto
qed

lemma eq_factoring_sound:
  assumes eq_factoring: "eq_factoring D C"
  shows "{D} F {C}"
  using eq_factoring
proof (cases D C rule: eq_factoring.cases)
  case (eq_factoringI D l1 l2 D' t1 t1' t2 t2' μ 𝒱 C)

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

    let ?I = "upair ` I"

    assume
      trans_I: "trans I" and
      sym_I: "sym I" and
      entails_groundings: "DG  clause_groundings (D, 𝒱). ?I  DG" and
      C_is_ground: "clause.is_ground (C  γ)" and
      C_is_welltyped: "clause.is_welltyped 𝒱 C" and
      γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars C) 𝒱 γ" and
      𝒱: "infinite_variables_per_type 𝒱"

    obtain γ' where
      γ'_is_ground_subst: "term_subst.is_ground_subst γ'" and
      γ'_is_welltyped: "term.subst.is_welltyped 𝒱 γ'" and
      γ'_γ: "x  clause.vars C. γ x = γ' x"
      using clause.is_welltyped.ground_subst_extension[OF C_is_ground γ_is_welltyped].

    let ?DG = "clause.to_ground (D  μ  γ')"
    let ?DG' = "clause.to_ground (D'  μ  γ')"
    let ?lG1 = "literal.to_ground (l1 ⋅l μ ⋅l γ')"
    let ?lG2 = "literal.to_ground (l2 ⋅l μ ⋅l γ')"
    let ?tG1 = "term.to_ground (t1 ⋅t μ ⋅t γ')"
    let ?tG1' = "term.to_ground (t1' ⋅t μ ⋅t γ')"
    let ?tG2 = "term.to_ground (t2 ⋅t μ ⋅t γ')"
    let ?tG2' = "term.to_ground (t2' ⋅t μ ⋅t γ')"
    let ?CG = "clause.to_ground (C  γ')"

    have μ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱 μ"
      using eq_factoringI(9)
      by blast

    have "?DG  clause_groundings (D, 𝒱)"
    proof(unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv, intro exI conjI 𝒱)
      show "clause.to_ground (D  μ  γ') = clause.to_ground (D  μ  γ')"
        by simp
    next
      show "clause.is_ground (D  μ  γ')"
        using γ'_is_ground_subst clause.is_ground_subst_is_ground
        by auto
    next
      show "clause.is_welltyped 𝒱 D"
         using C_is_welltyped
         unfolding eq_factoring_preserves_typing[OF eq_factoring[unfolded eq_factoringI(1, 2)]].
    next
      show "term.subst.is_welltyped_on (clause.vars D) 𝒱 (μ  γ')"
        using μ_is_welltyped γ'_is_welltyped
        by (simp add: subst_compose_def)
    qed

    then have "?I  ?DG"
      using entails_groundings
      by blast

    then obtain lG where lG_in_DG: "lG ∈# ?DG" and I_models_lG: "?I ⊫l lG"
      by (auto simp: true_cls_def)

    have [simp]: "?tG2 = ?tG1"
      using eq_factoringI(9) term_subst.is_imgu_unifies_pair
      by metis

    have [simp]: "?lG1 = ?tG1  ?tG1'"
      unfolding eq_factoringI
      by simp

    have [simp]: "?lG2 = ?tG2  ?tG2'"
      unfolding eq_factoringI
      by simp

    have [simp]: "?CG = add_mset (?tG1  ?tG2') (add_mset (?tG1' !≈ ?tG2') ?DG')"
      unfolding eq_factoringI 
      by simp

    have "?I  clause.to_ground (C  γ)"
    proof(cases "lG = ?lG1  lG = ?lG2")
      case True

      then have "?I ⊫l ?tG1  ?tG1'  ?I ⊫l ?tG1  ?tG2'"
        using I_models_lG sym_I
        by(auto elim: symE)

      then have "?I ⊫l ?tG1  ?tG2'  ?I ⊫l ?tG1' !≈ ?tG2'"
        using sym_I trans_I
        by(auto dest: transD)

      then show ?thesis
        using clause.subst_eq[OF γ'_γ[rule_format]] sym_I
        by auto
    next
      case False

      then have "lG ∈# ?DG'"
        using lG_in_DG
        unfolding eq_factoringI
        by simp

      then have "lG ∈# clause.to_ground (C  γ)"
        using clause.subst_eq[OF γ'_γ[rule_format]]
        by simp

      then show ?thesis
        using I_models_lG 
        by blast
    qed
  }

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

lemma superposition_sound:
  assumes superposition: "superposition D E C"
  shows "{E, D} F {C}"
  using superposition
proof (cases D E C rule: superposition.cases)
  case (superpositionI 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' 𝒫 c1 t1 t1' t2 t2' 𝒱3 μ C)

  {
    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
      E_entails_groundings: "EG  clause_groundings (E, 𝒱1). ?I  EG" and
      D_entails_groundings: "DG  clause_groundings (D, 𝒱2). ?I  DG" and
      C_is_ground: "clause.is_ground (C  γ)" and
      C_is_welltyped: "clause.is_welltyped 𝒱3 C" and
      γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars C) 𝒱3 γ"

    obtain γ' where
      γ'_is_ground_subst: "term_subst.is_ground_subst γ'" and
      γ'_is_welltyped: "term.subst.is_welltyped 𝒱3 γ'" and
      γ'_γ: "x  clause.vars C. γ x = γ' x"
      using clause.is_welltyped.ground_subst_extension[OF C_is_ground γ_is_welltyped].

    let ?EG = "clause.to_ground (E  ρ1  μ  γ')"
    let ?DG = "clause.to_ground (D  ρ2  μ  γ')"

    let ?lG1 = "literal.to_ground (l1 ⋅l ρ1 ⋅l μ ⋅l γ')"
    let ?lG2 = "literal.to_ground (l2 ⋅l ρ2 ⋅l μ ⋅l γ')"

    let ?EG' = "clause.to_ground (E'  ρ1  μ  γ')"
    let ?DG' = "clause.to_ground (D'  ρ2  μ  γ')"

    let ?cG1 = "context.to_ground (c1 ⋅tc ρ1 ⋅tc μ ⋅tc γ')"
    let ?tG1 = "term.to_ground (t1 ⋅t ρ1 ⋅t μ ⋅t γ')"
    let ?tG1' = "term.to_ground (t1' ⋅t ρ1 ⋅t μ ⋅t γ')"
    let ?tG2 = "term.to_ground (t2 ⋅t ρ2 ⋅t μ ⋅t γ')"
    let ?tG2' = "term.to_ground (t2' ⋅t ρ2 ⋅t μ ⋅t γ')"

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

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

    have 𝒫_subst [simp]: "a σ. 𝒫 a ⋅l σ = 𝒫 (a ⋅a σ)"
      using superpositionI(11)
      by auto

    have [simp]: "𝒱 a. literal.is_welltyped 𝒱 (𝒫 a)  atom.is_welltyped 𝒱 a"
      using superpositionI(11)
      by (auto simp: literal_is_welltyped_iff_atm_of)

    have [simp]: "a. literal.vars (𝒫 a) = atom.vars a"
      using superpositionI(11)
      by auto

    have μ_γ'_is_ground_subst:
      "term_subst.is_ground_subst (μ  γ')"
      using term.is_ground_subst_comp_right[OF γ'_is_ground_subst].

    have μ_is_welltyped:
      "term.subst.is_welltyped_on (clause.vars (E  ρ1)  clause.vars (D  ρ2)) 𝒱3 μ"
      using superpositionI(15)
      by blast

    have D_is_welltyped: "clause.is_welltyped 𝒱2 D"
      using superposition_preserves_typing_D[OF 
          superposition[unfolded superpositionI(1-3)] 
          C_is_welltyped].

    have E_is_welltyped: "clause.is_welltyped 𝒱1 E"
      using superposition_preserves_typing_E[OF 
          superposition[unfolded superpositionI(1-3)] 
          C_is_welltyped].

    have is_welltyped_μ_γ: 
      "term.subst.is_welltyped_on (clause.vars (E  ρ1)  clause.vars (D  ρ2)) 𝒱3 (μ  γ')"
      using γ'_is_welltyped μ_is_welltyped
      by (simp add: term.welltyped.typed_subst_compose)

    note is_welltyped_ρ_μ_γ = term.welltyped.renaming_ground_subst[OF _ _ _ μ_γ'_is_ground_subst]

    have "?EG  clause_groundings (E, 𝒱1)"
    proof(
        unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv, 
        intro exI conjI E_is_welltyped superpositionI)

      show "clause.to_ground (E  ρ1  μ  γ') = clause.to_ground (E  ρ1  μ  γ')"
        by simp
    next

      show "clause.is_ground (E  ρ1  μ  γ')"  
        using γ'_is_ground_subst clause.is_ground_subst_is_ground
        by auto
    next

      show "term.subst.is_welltyped_on (clause.vars E) 𝒱1 (ρ1  μ  γ')"
        using
          is_welltyped_μ_γ
          is_welltyped_ρ_μ_γ[OF
            superpositionI(6) _  superpositionI(18, 16)[unfolded clause.vars_subst]]
        by (simp add: subst_compose_assoc clause.vars_subst)
    qed

    then have entails_EG: "?I  ?EG"
      using E_entails_groundings
      by blast

    have "?DG  clause_groundings (D, 𝒱2)"
    proof(
        unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv, 
        intro exI conjI D_is_welltyped superpositionI)

      show "clause.to_ground (D  ρ2  μ  γ') = clause.to_ground (D  ρ2  μ  γ')"
        by simp
    next
      show "clause.is_ground (D  ρ2  μ  γ')"  
        using γ'_is_ground_subst clause.is_ground_subst_is_ground
        by auto
    next

      show "term.subst.is_welltyped_on (clause.vars D) 𝒱2 (ρ2  μ  γ')"
        using 
          is_welltyped_μ_γ
          is_welltyped_ρ_μ_γ[OF
            superpositionI(7) _ superpositionI(19, 17)[unfolded clause.vars_subst]]
        by (simp add: subst_compose_assoc clause.vars_subst)
    qed

    then have entails_DG: "?I  ?DG"
      using D_entails_groundings
      by blast

    have "?I  clause.to_ground (C  γ')"
    proof(cases "?I ⊫l literal.to_ground (𝒫 (Upair (c1 ⋅tc ρ1)t2' ⋅t ρ2 (t1' ⋅t ρ1)) ⋅l μ ⋅l γ')")
      case True
      then show ?thesis
        unfolding superpositionI
        by simp
    next
      case False

      have imgu: "term.is_imgu μ {{t1 ⋅t ρ1, t2 ⋅t ρ2}}"
        using superpositionI(15)
        by blast

      interpret clause_entailment I
        by unfold_locales (rule trans_I sym_I compatible_with_ground_context_I)+

      note unfolds =
        superpositionI
        context.safe_unfolds
        clause_safe_unfolds
        literal_entails_unfolds
        term.is_imgu_unifies_pair[OF imgu]

      from literal_cases[OF superpositionI(11)]
      have "¬ ?I ⊫l ?lG1  ¬ ?I ⊫l ?lG2"
      proof cases
        case Pos: 1

        show ?thesis
          using False symmetric_upair_context_congruence
          unfolding Pos unfolds
          by blast
      next
        case Neg: 2

        show ?thesis
          using False symmetric_upair_context_congruence
          unfolding Neg unfolds
          by blast
      qed

      then have "?I  ?EG'  ?I  ?DG'"
        using entails_DG entails_EG
        unfolding superpositionI
        by auto

      then show ?thesis
        unfolding superpositionI
        by simp
    qed

    then have "?I  clause.to_ground (C  γ)"
      by (metis γ'_γ clause.subst_eq)
  }

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

end

sublocale grounded_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 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_superposition_calculus
    where selectG = selectG
    by unfold_locales (simp add: selectGs_def)

  fix ι
  assume "ι  inferences"

  then show "entails_𝒢 (set (prems_of ι)) {concl_of ι}"
    unfolding entails_def
    using sound
    by blast
qed

end