Theory Ordered_Resolution_Welltypedness_Preservation

theory Ordered_Resolution_Welltypedness_Preservation
  imports Grounded_Ordered_Resolution
begin

context ordered_resolution_calculus
begin

lemma factoring_preserves_typing:
  assumes factoring: "factoring (𝒱, D) (𝒱, C)"
  shows "clause.is_welltyped 𝒱 D ⟷ clause.is_welltyped 𝒱 C"
  using assms
proof (cases "(𝒱, D)" "(𝒱, C)" rule: factoring.cases)
  case (factoringI l⇩1 μ t⇩1 t⇩2 l⇩2 D')
 
  show ?thesis
  proof (rule iffI)
    assume "clause.is_welltyped 𝒱 D" 
    then show "clause.is_welltyped 𝒱 C"
      using factoringI
      by simp
  next
    assume C_is_welltyped: "clause.is_welltyped 𝒱 C" 

    note imgu = factoringI(3, 4)

    have "clause.is_welltyped 𝒱 (add_mset l⇩1 D')"
      using C_is_welltyped imgu
      unfolding factoringI
      by simp

    moreover have "literal.is_welltyped 𝒱 l⇩2"
      using C_is_welltyped term.imgu_same_type[OF imgu] imgu
      unfolding factoringI
      by force

    ultimately show "clause.is_welltyped 𝒱 D"
      unfolding factoringI
      by simp
  qed
qed

lemma resolution_preserves_typing:
  assumes
    resolution: "resolution (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C)" and
    D_is_welltyped: "clause.is_welltyped 𝒱⇩2 D" and
    E_is_welltyped: "clause.is_welltyped 𝒱⇩1 E"
  shows "clause.is_welltyped 𝒱⇩3 C"
  using resolution
proof (cases "(𝒱⇩2, D)" "(𝒱⇩1, E)" "(𝒱⇩3, C)" rule: resolution.cases)
  case (resolutionI ρ⇩1 ρ⇩2 μ t⇩1 t⇩2 l⇩1 l⇩2 E' D')

  note μ_type_preserving = resolutionI(6)

  have "clause.is_welltyped 𝒱⇩3 (E ⋅ ρ⇩1)"
    using E_is_welltyped clause.welltyped_renaming[OF resolutionI(3, 13)]
    by blast

  then have Eμ_is_welltyped: "clause.is_welltyped 𝒱⇩3 (E ⋅ ρ⇩1 ⊙ μ)"
    using μ_type_preserving
    by simp

  moreover have "clause.is_welltyped 𝒱⇩3 (D ⋅ ρ⇩2)"
    using D_is_welltyped clause.welltyped_renaming[OF resolutionI(4, 14)]
    by blast

  then have Dμ_is_welltyped: "clause.is_welltyped 𝒱⇩3 (D ⋅ ρ⇩2 ⊙ μ)"
    using μ_type_preserving
    by simp

  ultimately show ?thesis
    unfolding resolutionI
    by auto
qed

end

end