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 𝒱 μ t t' l D' C)

  {
    fix I :: "'t⇩G rel" and γ :: "'v ⇒ 't"

    let ?I = "upair ` I"

    assume
      refl_I: "refl I" and
      entails_ground_instances: "∀D⇩G ∈ ground_instances 𝒱 D. ?I ⊫ D⇩G" and
      C_is_ground: "clause.is_ground (C ⋅ γ)" and
      type_preserving_literals: "type_preserving_literals 𝒱 C" and
      type_preserving_γ: "type_preserving_on (clause.vars C) 𝒱 γ" and
      𝒱: "infinite_variables_per_type 𝒱"

    obtain γ' where
      γ'_is_ground_subst: "term.is_ground_subst γ'" and
      type_preserving_γ': "type_preserving 𝒱 γ'" and
      γ'_γ: "∀x ∈ clause.vars C. γ x = γ' x"
      using clause.type_preserving_ground_subst_extension[OF C_is_ground type_preserving_γ] .

    let ?D⇩G = "clause.to_ground (D ⋅ μ ⋅ γ')"
    let ?l⇩G = "literal.to_ground (l ⋅l μ ⋅l γ')"
    let ?D⇩G' = "clause.to_ground (D' ⋅ μ ⋅ γ')"
    let ?t⇩G = "term.to_ground (t ⋅t μ ⋅t γ')"
    let ?t⇩G' = "term.to_ground (t' ⋅t μ ⋅t γ')"

    note type_preserving_μ = eq_resolutionI(3)

    have "?D⇩G ∈ ground_instances 𝒱 D"
    proof (unfold ground_instances_def mem_Collect_eq fst_conv snd_conv, intro exI, intro 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 "type_preserving_on (clause.vars D) 𝒱 (μ ⊙ γ')"
        using 
          type_preserving_γ' type_preserving_μ γ'_is_ground_subst
          term.type_preserving_ground_compose_ground_subst
        by presburger
    next

      show "type_preserving_literals 𝒱 D" 
        using 
          eq_resolution_type_preserving_literals[OF eq_resolution[unfolded eq_resolutionI]] 
          type_preserving_literals
        unfolding eq_resolutionI
        by satx
    qed

    then have "?I ⊫ ?D⇩G"
      using entails_ground_instances
      by auto

    then obtain l⇩G where l⇩G_in_D: "l⇩G ∈# ?D⇩G" and I_models_l⇩G: "?I ⊫l l⇩G"
      by (auto simp: true_cls_def)

    have "l⇩G ≠ ?l⇩G"
    proof(rule notI)
      assume "l⇩G = ?l⇩G"

      then have [simp]: "l⇩G = ?t⇩G !≈ ?t⇩G'"
        unfolding eq_resolutionI
        by simp

      moreover have "atm_of l⇩G ∈ ?I"
      proof -
        have "?t⇩G = ?t⇩G'"
          using eq_resolutionI(4) term.is_imgu_unifies_pair
          by metis

        then show ?thesis
          using reflD[OF refl_I, of ?t⇩G]
          by auto
      qed

      ultimately show False
        using I_models_l⇩G
        by auto
    qed

    then have "l⇩G ∈# clause.to_ground (C ⋅ γ')"
      using l⇩G_in_D
      unfolding eq_resolutionI
      by simp

    then have "?I ⊫ clause.to_ground (C ⋅ γ)"
      using clause.subst_eq[OF γ'_γ[rule_format]] I_models_l⇩G
      by auto
  }

  then show ?thesis
    unfolding
      true_clss_def
      eq_resolutionI(1,2)
      ground_instances_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 l⇩1 μ t⇩1 t⇩1' 𝒱 t⇩2 l⇩2 D' t⇩2' C)

  {
    fix I :: "'t⇩G rel" and γ :: "'v ⇒ 't"

    let ?I = "upair ` I"

    assume
      trans_I: "trans I" and
      sym_I: "sym I" and
      entails_ground_instances: "∀D⇩G ∈ ground_instances 𝒱 D. ?I ⊫ D⇩G" and
      C_is_ground: "clause.is_ground (C ⋅ γ)" and
      type_preserving_literals: "type_preserving_literals 𝒱 C" and
      type_preserving_γ: "type_preserving_on (clause.vars C) 𝒱 γ" and
      𝒱: "infinite_variables_per_type 𝒱"

    obtain γ' where
      γ'_is_ground_subst: "term.is_ground_subst γ'" and
      type_preserving_γ': "type_preserving 𝒱 γ'" and
      γ'_γ: "∀x ∈ clause.vars C. γ x = γ' x"
      using clause.type_preserving_ground_subst_extension[OF C_is_ground type_preserving_γ].

    let ?D⇩G = "clause.to_ground (D ⋅ μ ⋅ γ')"
    let ?D⇩G' = "clause.to_ground (D' ⋅ μ ⋅ γ')"
    let ?l⇩G⇩1 = "literal.to_ground (l⇩1 ⋅l μ ⋅l γ')"
    let ?l⇩G⇩2 = "literal.to_ground (l⇩2 ⋅l μ ⋅l γ')"
    let ?t⇩G⇩1 = "term.to_ground (t⇩1 ⋅t μ ⋅t γ')"
    let ?t⇩G⇩1' = "term.to_ground (t⇩1' ⋅t μ ⋅t γ')"
    let ?t⇩G⇩2 = "term.to_ground (t⇩2 ⋅t μ ⋅t γ')"
    let ?t⇩G⇩2' = "term.to_ground (t⇩2' ⋅t μ ⋅t γ')"
    let ?C⇩G = "clause.to_ground (C ⋅ γ')"

    note type_preserving_μ = eq_factoringI(6)

    have "?D⇩G ∈ ground_instances 𝒱 D"
    proof (unfold ground_instances_def mem_Collect_eq fst_conv snd_conv, intro exI, intro 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 "type_preserving_on (clause.vars D) 𝒱 (μ ⊙ γ')"
        using 
          type_preserving_μ type_preserving_γ' γ'_is_ground_subst
          term.type_preserving_ground_compose_ground_subst
        by presburger
    next

      show "type_preserving_literals 𝒱 D"
        using type_preserving_literals
        unfolding 
          eq_factoringI
          eq_factoring_type_preserving_literals[OF eq_factoring[unfolded eq_factoringI]] .
    qed

    then have "?I ⊫ ?D⇩G"
      using entails_ground_instances
      by blast

    then obtain l⇩G where l⇩G_in_D⇩G: "l⇩G ∈# ?D⇩G" and I_models_l⇩G: "?I ⊫l l⇩G"
      by (auto simp: true_cls_def)

    have [simp]: "?t⇩G⇩2 = ?t⇩G⇩1"
      using eq_factoringI(7) term.is_imgu_unifies_pair
      by metis

    have [simp]: "?l⇩G⇩1 = ?t⇩G⇩1 ≈ ?t⇩G⇩1'"
      unfolding eq_factoringI
      by simp

    have [simp]: "?l⇩G⇩2 = ?t⇩G⇩2 ≈ ?t⇩G⇩2'"
      unfolding eq_factoringI
      by simp

    have [simp]: "?C⇩G = add_mset (?t⇩G⇩1 ≈ ?t⇩G⇩2') (add_mset (?t⇩G⇩1' !≈ ?t⇩G⇩2') ?D⇩G')"
      unfolding eq_factoringI
      by simp

    have "?I ⊫ clause.to_ground (C ⋅ γ)"
    proof(cases "l⇩G = ?l⇩G⇩1 ∨ l⇩G = ?l⇩G⇩2")
      case True

      then have "?I ⊫l ?t⇩G⇩1 ≈ ?t⇩G⇩1' ∨ ?I ⊫l ?t⇩G⇩1 ≈ ?t⇩G⇩2'"
        using I_models_l⇩G sym_I
        by (auto elim: symE)

      then have "?I ⊫l ?t⇩G⇩1 ≈ ?t⇩G⇩2' ∨ ?I ⊫l ?t⇩G⇩1' !≈ ?t⇩G⇩2'"
        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 "l⇩G ∈# ?D⇩G'"
        using l⇩G_in_D⇩G
        unfolding eq_factoringI
        by simp

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

      then show ?thesis
        using I_models_l⇩G
        by blast
    qed
  }

  then show ?thesis
    unfolding
      eq_factoringI(1, 2)
      ground.G_entails_def
      true_clss_def
      ground_instances_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 t⇩1 𝒱⇩3 μ t⇩2 c⇩1 t⇩1' t⇩2' l⇩1 l⇩2 E' D' C)

  {
    fix I :: "'t⇩G rel" and γ :: "'v ⇒ 't"

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

    assume
      trans_I: "trans I" and
      sym_I: "sym I" and
      compatible_with_ground_context_I: "compatible_with_context I" and
      E_entails_ground_instances: "∀E⇩G ∈ ground_instances 𝒱⇩1 E. ?I ⊫ E⇩G" and
      D_entails_ground_instances: "∀D⇩G ∈ ground_instances 𝒱⇩2 D. ?I ⊫ D⇩G" and
      C_is_ground: "clause.is_ground (C ⋅ γ)" and
      type_preserving_literals: "type_preserving_literals 𝒱⇩3 C" and
      type_preserving_γ: "type_preserving_on (clause.vars C) 𝒱⇩3 γ"

    obtain γ' where
      γ'_is_ground_subst: "term.is_ground_subst γ'" and
      type_preserving_γ': "type_preserving 𝒱⇩3 γ'" and
      γ'_γ: "∀x ∈ clause.vars C. γ x = γ' x"
      using clause.type_preserving_ground_subst_extension[OF C_is_ground type_preserving_γ] .

    let ?E⇩G = "clause.to_ground (E ⋅ ρ⇩1 ⋅ μ ⋅ γ')"
    let ?D⇩G = "clause.to_ground (D ⋅ ρ⇩2 ⋅ μ ⋅ γ')"

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

    let ?E⇩G' = "clause.to_ground (E' ⋅ ρ⇩1 ⋅ μ ⋅ γ')"
    let ?D⇩G' = "clause.to_ground (D' ⋅ ρ⇩2 ⋅ μ ⋅ γ')"

    let ?c⇩G⇩1 = "context.to_ground (c⇩1 ⋅t⇩c ρ⇩1 ⋅t⇩c μ ⋅t⇩c γ')"
    let ?t⇩G⇩1 = "term.to_ground (t⇩1 ⋅t ρ⇩1 ⋅t μ ⋅t γ')"
    let ?t⇩G⇩1' = "term.to_ground (t⇩1' ⋅t ρ⇩1 ⋅t μ ⋅t γ')"
    let ?t⇩G⇩2 = "term.to_ground (t⇩2 ⋅t ρ⇩2 ⋅t μ ⋅t γ')"
    let ?t⇩G⇩2' = "term.to_ground (t⇩2' ⋅t ρ⇩2 ⋅t μ ⋅t γ')"

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

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

    note [simp] = 𝒫_simps[OF superpositionI(4)]

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

    note type_preserving_μ = superpositionI(11)
     
    have type_preserving_μ_γ:
      "type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 (μ ⊙ γ')"
      using 
        type_preserving_γ' type_preserving_μ  γ'_is_ground_subst
        term.type_preserving_ground_compose_ground_subst
      by presburger

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

    have "?E⇩G ∈ ground_instances 𝒱⇩1 E"
    proof (unfold ground_instances_def mem_Collect_eq fst_conv snd_conv, 
            intro exI, 
            intro conjI 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 "type_preserving_on (clause.vars E) 𝒱⇩1 (ρ⇩1 ⊙ μ ⊙ γ')"
        using
          type_preserving_μ_γ
          type_preserving_ρ_μ_γ[OF superpositionI(7, 24) _ superpositionI(22)]
        by (simp add: clause.vars_subst term.assoc)
    next

      show "type_preserving_literals 𝒱⇩1 E"
        using 
          type_preserving_literals
          superposition_type_preserving_literals[OF superposition[unfolded superpositionI]]
        unfolding superpositionI
        by satx
    qed

    then have entails_E⇩G: "?I ⊫ ?E⇩G"
      using E_entails_ground_instances
      by blast

    have "?D⇩G ∈ ground_instances 𝒱⇩2 D"
    proof (unfold ground_instances_def mem_Collect_eq fst_conv snd_conv,
            intro exI,
            intro conjI 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 "type_preserving_on (clause.vars D) 𝒱⇩2 (ρ⇩2 ⊙ μ ⊙ γ')"
        using
          type_preserving_μ_γ
          type_preserving_ρ_μ_γ[OF superpositionI(8, 25) _ superpositionI(23)]
        by (simp add: term.assoc clause.vars_subst)
    next

      show "type_preserving_literals 𝒱⇩2 D"
        using 
          type_preserving_literals
          superposition_type_preserving_literals[OF superposition[unfolded superpositionI]]
        unfolding superpositionI
        by satx  
    qed

    then have entails_D⇩G: "?I ⊫ ?D⇩G"
      using D_entails_ground_instances
      by blast

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

      interpret clause_entailment where I = 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 superpositionI(12)]

      from literal_cases[OF superpositionI(4)]
      have "¬ ?I ⊫l ?l⇩G⇩1 ∨ ¬ ?I ⊫l ?l⇩G⇩2"
      proof cases
        case Pos: 1

        show ?thesis
          using False symmetric_upair_context_congruence
          unfolding Pos unfolds
          by (auto simp: sym term.is_imgu_unifies_pair[OF superpositionI(12)])
      next
        case Neg: 2

        show ?thesis
          using False symmetric_upair_context_congruence
          unfolding Neg unfolds
          by (auto simp: sym term.is_imgu_unifies_pair[OF superpositionI(12)])
      qed

      then have "?I ⊫ ?E⇩G' ∨ ?I ⊫ ?D⇩G'"
        using entails_D⇩G entails_E⇩G
        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 
      ground_instances_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 select⇩G where select⇩G: "select⇩G ∈ select⇩G⇩s"
    using Q_nonempty by blast

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

  fix ι
  assume "ι ∈ inferences"

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

end