Theory Ordered_Resolution_Soundness

theory Ordered_Resolution_Soundness
  imports Grounded_Ordered_Resolution
begin

subsection ‹Soundness›

context grounded_ordered_resolution_calculus
begin

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

lemma factoring_sound:
  assumes factoring: "factoring D C"
  shows "{D} ⊫⇩F {C}"
  using factoring
proof (cases D C rule: factoring.cases)
  case (factoringI D l⇩1 μ 𝒱 t⇩1 t⇩2 l⇩2 D' C)

  {
    fix I :: "'t⇩G set" and γ :: 'subst

    assume
      entails_ground_instances: "∀D⇩G ∈ ground_instances 𝒱 D. I ⊫ D⇩G" and
      C_is_ground: "clause.is_ground (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 ⋅v γ = x ⋅v γ'"
      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⇩2 = "term.to_ground (t⇩2 ⋅t μ ⋅t γ')"
    let ?C⇩G = "clause.to_ground (C ⋅ γ')"

    have type_preserving_μ: "type_preserving_on (clause.vars D) 𝒱 μ"
      using factoringI(5)
      by blast

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

    have [simp]: "t⇩1 ⋅t μ ⋅t γ' =  t⇩1 ⋅t μ ⋅t γ"
      using γ'_γ term.subst_eq 
      unfolding factoringI
      by fastforce

    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
    qed

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

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

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

lemma resolution_sound:
  assumes resolution: "resolution D E C"
  shows "{E, D} ⊫⇩F {C}"
  using resolution
proof (cases D E C rule: resolution.cases)
  case (resolutionI 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D 𝒱⇩3 μ t⇩1 t⇩2 l⇩1 l⇩2 E' D' C)
  
  {
    fix I :: "'t⇩G set" and γ :: 'subst

    assume
      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_γ: "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 ⋅v γ = x ⋅v γ'"
      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 ?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 ?C⇩G = "clause.to_ground (C ⋅ γ')"

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

    have type_preserving_μ: "type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 μ"
      using resolutionI(9)
      by blast

    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 resolutionI)

      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 resolutionI(6, 18) _ resolutionI(16)]
        by (simp add: term.assoc clause.vars_subst)
    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 resolutionI)

      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 resolutionI(7, 19) _ resolutionI(17)]
        by (simp add: term.assoc clause.vars_subst)
    qed

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

    have "I ⊫ clause.to_ground (C ⋅ γ')"
    proof -
      have [simp]: "?t⇩G⇩1 = ?t⇩G⇩2"
        using resolutionI(10) term.is_imgu_unifies_pair
        by metis

      have [simp]: "?l⇩G⇩1 = Neg ?t⇩G⇩1"
        unfolding resolutionI
        by simp

      have [simp]: "?l⇩G⇩2 = Pos ?t⇩G⇩2"
        unfolding resolutionI
        by simp

      have [simp]: "?E⇩G = add_mset ?l⇩G⇩1 ?E⇩G'"
        unfolding resolutionI
        by simp

      have [simp]: "?D⇩G = add_mset ?l⇩G⇩2 ?D⇩G'"
        unfolding resolutionI
        by simp

      have "¬ I ⊫l ?l⇩G⇩1 ∨ ¬ I ⊫l ?l⇩G⇩2"
        by simp

      then have "I ⊫ ?E⇩G' ∨ I ⊫ ?D⇩G'"
        using entails_E⇩G entails_D⇩G
        by force

      moreover have "?C⇩G = ?E⇩G' + ?D⇩G'"
        unfolding resolutionI
        by simp

      ultimately show ?thesis
        by auto
    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 resolutionI(1-3)
    by auto   
qed

sublocale sound_inference_system inferences "⊥⇩F" "(⊫⇩F)"
proof unfold_locales
fix ι

  assume "ι ∈ inferences"

  then show "set (prems_of ι) ⊫⇩F {concl_of ι}"
    using
      factoring_sound
      resolution_sound
    unfolding inferences_def ground.G_entails_def
    by auto
qed

end

sublocale ordered_resolution_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_ordered_resolution_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