Theory Ground_Ordered_Resolution_Soundness

theory Ground_Ordered_Resolution_Soundness
  imports Ground_Ordered_Resolution
begin

context ground_ordered_resolution_calculus
begin

lemma soundness_ground_resolution:
  assumes
    step: "resolution D E C"
  shows "G_entails {D, E} {C}"
  using step
proof (cases D E C rule: resolution.cases)
  case (resolutionI l⇩1 l⇩2 E' D' t)

  show ?thesis
    unfolding G_entails_def true_clss_singleton
    unfolding true_clss_insert
  proof (intro allI impI, elim conjE)
    fix I :: "'t set"
    assume "I ⊫ E" and "I ⊫ D"

    then obtain k⇩1 k⇩2 :: "'t literal" where
      "k⇩1 ∈# E" and "I ⊫l k⇩1" and "k⇩2 ∈# D" and "I ⊫l k⇩2"
      by (auto simp: true_cls_def)

    show "I ⊫ C"
    proof (cases "k⇩1 = l⇩1")
      case K1_def: True

      hence "I ⊫l l⇩1"
        using ‹I ⊫l k⇩1› 
        by simp

      show ?thesis
      proof (cases "k⇩2 = l⇩2")
        case K2_def: True

        hence "I ⊫l l⇩2"
          using ‹I ⊫l k⇩2› 
          by simp

        hence False
          using ‹I ⊫l l⇩1› local.resolutionI(7,8) by auto

        thus ?thesis ..
      next
        case False

        hence "k⇩2 ∈# D'"
          using ‹k⇩2 ∈# D›
          unfolding resolutionI
          by simp

        hence "I ⊫ D'"
          using ‹I ⊫l k⇩2› 
          by blast

        thus ?thesis
          unfolding resolutionI 
          by simp
      qed
    next
      case False

      hence "k⇩1 ∈# E'"
        using ‹k⇩1 ∈# E›
        unfolding resolutionI 
        by simp

      hence "I ⊫ E'"
        using ‹I ⊫l k⇩1› 
        by blast

      thus ?thesis
        unfolding resolutionI 
        by simp
    qed
  qed
qed

lemma soundness_ground_factoring:
  assumes step: "factoring D C"
  shows "G_entails {D} {C}"
  using step
proof (cases D C rule: factoring.cases)
  case (factoringI l D' t)

  show ?thesis
    unfolding G_entails_def true_clss_singleton
  proof (intro allI impI)
    fix I :: "'t set"
    assume "I ⊫ D"

    then obtain k :: "'t literal" where
      "k ∈# D" and "I ⊫l k"
      by (auto simp: true_cls_def)

    show "I ⊫ C"
    proof (cases "k = l")
      case True

      hence "I ⊫l l"
        using ‹I ⊫l k› 
        by metis

      thus ?thesis
        unfolding factoringI
        by (metis true_cls_add_mset)
    next
      case False

      hence "k ∈# D'"
        using ‹k ∈# D›
        unfolding factoringI
        by auto

      hence "k ∈# C"
        unfolding factoringI
        by simp

      thus ?thesis
        using ‹I ⊫l k› 
        by blast
    qed
  qed
qed

sublocale sound_inference_system where
  Inf = G_Inf and
  Bot = G_Bot and
  entails = G_entails
proof unfold_locales
  fix ι
  assume "ι ∈ G_Inf"

  then show "G_entails (set (prems_of ι)) {concl_of ι}"
    unfolding G_Inf_def
    using soundness_ground_resolution soundness_ground_factoring
    by auto
qed

end

end