Theory Untyped_Ordered_Resolution_Inference_System

theory Untyped_Ordered_Resolution_Inference_System
  imports 
    Untyped_Ordered_Resolution
    First_Order_Clause.Untyped_Calculus
    Grounded_Ordered_Resolution
begin

context untyped_ordered_resolution_calculus
begin

sublocale typed: ordered_resolution_calculus where
  welltyped = "λ_ _ (). True"
  by
    unfold_locales
    (auto intro: term.ground_exists simp: term.exists_imgu right_unique_def split: unit.splits)

declare
  typed.term.welltyped_renaming [simp del]
  typed.term.welltyped_subst_stability [simp del]
  typed.term.welltyped_subst_stability' [simp del]

(* TODO: Write own *)
abbreviation entails where
  "entails N N' ≡ typed.entails_𝒢 (empty_typed ` N) (empty_typed ` N')"

sublocale untyped_consequence_relation where 
  typed_bottom = "⊥⇩F" and typed_entails = typed.entails_𝒢 and
  bottom = bottom and entails = entails
proof unfold_locales 

  have "bottom = snd ` ⊥⇩F"
    using image_iff typed.bot_not_empty 
    by fastforce

  then show "bottom ≡ snd ` ⊥⇩F"
    by argo
qed

sublocale untyped_inference_system where 
  inferences = inferences and typed_inferences = typed.inferences
proof unfold_locales

  {
    fix 𝒱 D 𝒱' C
    have "typed.factoring (𝒱, D) (𝒱', C) ⟷ factoring D C"
      unfolding 𝒱_all_same[of 𝒱] 𝒱_all_same[of 𝒱']
    proof (rule iffI)
      assume "typed.factoring (empty_typed D) (empty_typed C)"

      then show "factoring D C"
      proof (cases rule: typed.factoring.cases)
        case typed_factoringI: factoringI

        then show ?thesis
          by (intro factoringI; (rule typed_factoringI)?)
      qed
    next
      assume "factoring D C"

      then show "typed.factoring (empty_typed D) (empty_typed C)"
      proof (cases rule: factoring.cases)
        case factoringI

        then show ?thesis
          by (intro typed.factoringI) (auto simp: case_unit_Unity)
      qed
    qed
  }

  then have "remove_types ` typed.factoring_inferences = factoring_inferences"
    by auto

  moreover {
    fix 𝒱⇩1 D 𝒱⇩2 E 𝒱⇩3 C
    have "typed.resolution (𝒱⇩1, D) (𝒱⇩2, E) (𝒱⇩3, C) ⟷ resolution D E C"
      unfolding 𝒱_all_same[of 𝒱⇩1] 𝒱_all_same[of 𝒱⇩2] 𝒱_all_same[of 𝒱⇩3]
    proof (rule iffI)
      assume "typed.resolution (empty_typed D) (empty_typed E) (empty_typed C)"

      then show "resolution D E C"
      proof (cases rule: typed.resolution.cases)
        case typed_resolutionI: resolutionI

        then show ?thesis
          by (intro resolutionI; (rule typed_resolutionI)?)
      qed
    next
      assume "resolution D E C"

      then show "typed.resolution (empty_typed D) (empty_typed E) (empty_typed C)"
      proof (cases rule: resolution.cases)
        case resolutionI

        show ?thesis
          by
            (intro typed.resolutionI; (rule resolutionI)?)
            (auto simp: case_unit_Unity)
      qed
    qed
  }

  then have "remove_types ` typed.resolution_inferences = resolution_inferences"
    by auto

  ultimately show "inferences ≡ remove_types ` typed.inferences"
    unfolding inferences_def typed.inferences_def image_Un
    by auto
qed

end

end