Theory Ground_Superposition_Soundness

theory Ground_Superposition_Soundness
  imports Ground_Superposition
begin

lemma (in ground_superposition_calculus) soundness_ground_superposition:
  assumes
    step: "superposition P1 P2 C"
  shows "G_entails {P1, P2} {C}"
  using step
proof (cases P1 P2 C rule: superposition.cases)
  case (superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')

  show ?thesis
    unfolding G_entails_def true_clss_singleton
    unfolding true_clss_insert
  proof (intro allI impI, elim conjE)
    fix I :: "'t rel"
    let ?I' = "(λ(t⇩1, t). Upair t⇩1 t) ` I"
    assume "refl I" and "trans I" and "sym I" and "compatible_with_context I" and
      "?I' ⊫ P1" and "?I' ⊫ P2"
    then obtain K1 K2 where
      "K1 ∈# P1" and "?I' ⊫l K1" and "K2 ∈# P2" and "?I' ⊫l K2"
      by (auto simp: true_cls_def)

    show "?I' ⊫ C"
    proof (cases "K2 = 𝒫 (Upair s⟨t⟩ s')")
      case K1_def: True
      hence "?I' ⊫l 𝒫 (Upair s⟨t⟩ s')"
        using ‹?I' ⊫l K2› by simp

      show ?thesis
      proof (cases "K1 = Pos (Upair t t')")
        case K2_def: True
        hence "(t, t') ∈ I"
          using ‹?I' ⊫l K1› true_lit_uprod_iff_true_lit_prod[OF ‹sym I›] by simp

        have ?thesis if "𝒫 = Pos"
        proof -
          from that have "(s⟨t⟩, s') ∈ I"
            using ‹?I' ⊫l K2› K1_def true_lit_uprod_iff_true_lit_prod[OF ‹sym I›] by simp
          hence "(s⟨t'⟩, s') ∈ I"
            using ‹(t, t') ∈ I›
            using ‹compatible_with_context I› ‹refl I› ‹sym I› ‹trans I›
            by (metis compatible_with_contextD[of I t' t s] symE[of I t t']
                transE[of I "s⟨t'⟩" "s⟨t⟩" s'])
          hence "?I' ⊫l s⟨t'⟩ ≈ s'"
            by blast
          thus ?thesis
            unfolding superpositionI that
            by simp
        qed

        moreover have ?thesis if "𝒫 = Neg"
        proof -
          from that have "(s⟨t⟩, s') ∉ I"
            using ‹?I' ⊫l K2› K1_def true_lit_uprod_iff_true_lit_prod[OF ‹sym I›] by simp
          hence "(s⟨t'⟩, s') ∉ I"
            using ‹(t, t') ∈ I›
            using ‹compatible_with_context I› ‹trans I›
            by (metis compatible_with_contextD transD)
          hence "?I' ⊫l Neg (Upair s⟨t'⟩ s')"
            by (meson ‹sym I› true_lit_simps(2) true_lit_uprod_iff_true_lit_prod(2))
          thus ?thesis
            unfolding superpositionI that by simp
        qed

        ultimately show ?thesis
          using ‹𝒫 ∈ {Pos, Neg}› by auto
      next
        case False
        hence "K1 ∈# P⇩2'"
          using ‹K1 ∈# P1›
          unfolding superpositionI by simp
        hence "?I' ⊫ P⇩2'"
          using ‹?I' ⊫l K1› by blast
        thus ?thesis
          unfolding superpositionI by simp
      qed
    next
      case False
      hence "K2 ∈# P⇩1'"
        using ‹K2 ∈# P2›
        unfolding superpositionI by simp
      hence "?I' ⊫ P⇩1'"
        using ‹?I' ⊫l K2› by blast
      thus ?thesis
        unfolding superpositionI by simp
    qed
  qed
qed

lemma (in ground_superposition_calculus) soundness_ground_eq_resolution:
  assumes step: "eq_resolution P C"
  shows "G_entails {P} {C}"
  using step
proof (cases P C rule: eq_resolution.cases)
  case (eq_resolutionI L D' t)
  show ?thesis
    unfolding G_entails_def true_clss_singleton
  proof (intro allI impI)
    fix I :: "'t rel"
    assume "refl I" and "(λ(t⇩1, t⇩2). Upair t⇩1 t⇩2) ` I ⊫ P"
    then obtain K where "K ∈# P" and "(λ(t⇩1, t⇩2). Upair t⇩1 t⇩2) ` I ⊫l K"
      by (auto simp: true_cls_def)
    hence "K ≠ L"
      by (metis ‹refl I› eq_resolutionI(2) pair_imageI reflD true_lit_simps(2))
    hence "K ∈# C"
      using ‹K ∈# P› ‹P = add_mset L D'› ‹C = D'› by simp
    thus "(λ(t⇩1, t⇩2). Upair t⇩1 t⇩2) ` I ⊫ C"
      using ‹(λ(t⇩1, t⇩2). Upair t⇩1 t⇩2) ` I ⊫l K› by blast
  qed
qed

lemma (in ground_superposition_calculus) soundness_ground_eq_factoring:
  assumes step: "eq_factoring P C"
  shows "G_entails {P} {C}"
  using step
proof (cases P C rule: eq_factoring.cases)
  case (eq_factoringI L⇩1 L⇩2 P' t t' t'')
  show ?thesis
    unfolding G_entails_def true_clss_singleton
  proof (intro allI impI)
    fix I :: "'t rel"
    let ?I' = "(λ(t⇩1, t). Upair t⇩1 t) ` I"
    assume "trans I" and "sym I" and "?I' ⊫ P"
    then obtain K where
      "K ∈# P" and "?I' ⊫l K"
      by (auto simp: true_cls_def)

    show "?I' ⊫ C"
    proof (cases "K = L⇩1 ∨ K = L⇩2")
      case True
      hence "I ⊫l Pos (t, t') ∨ I ⊫l Pos (t, t'')"
        unfolding eq_factoringI
        using ‹?I' ⊫l K› true_lit_uprod_iff_true_lit_prod[OF ‹sym I›] by metis
      hence "I ⊫l Pos (t, t'') ∨ I ⊫l Neg (t', t'')"
      proof (elim disjE)
        assume "I ⊫l Pos (t, t')"
        then show ?thesis
          unfolding true_lit_simps
          by (metis ‹trans I› transD)
      next
        assume "I ⊫l Pos (t, t'')"
        then show ?thesis
          by simp
      qed
      hence "?I' ⊫l Pos (Upair t t'') ∨ ?I' ⊫l Neg (Upair t' t'')"
        unfolding true_lit_uprod_iff_true_lit_prod[OF ‹sym I›] .
      thus ?thesis
        unfolding eq_factoringI
        by (metis true_cls_add_mset)
    next
      case False
      hence "K ∈# P'"
        using ‹K ∈# P›
        unfolding eq_factoringI
        by auto
      hence "K ∈# C"
        by (simp add: eq_factoringI(1,2,7))
      thus ?thesis
        using ‹(λ(t⇩1, t). Upair t⇩1 t) ` I ⊫l K› by blast
    qed
  qed
qed

sublocale ground_superposition_calculus ⊆ sound_inference_system where
  Inf = G_Inf and
  Bot = G_Bot and
  entails = G_entails
proof unfold_locales
  show "⋀ι. ι ∈ G_Inf ⟹ G_entails (set (prems_of ι)) {concl_of ι}"
    unfolding G_Inf_def
    using soundness_ground_superposition
    using soundness_ground_eq_resolution
    using soundness_ground_eq_factoring
    by (auto simp: G_entails_def)
qed

end