Theory ML_Unification.ML_Unification_HOL_Setup

✐‹creator "Kevin Kappelmann"›
section ‹Setup for HOL›
theory ML_Unification_HOL_Setup
  imports
    HOL.HOL
    ML_Unification_Hints
begin

lemma eq_eq_True: "P ≡ (P ≡ Trueprop True)" by standard+ simp_all
declare [[uhint config: hint_preprocessor = ‹Unification_Hints_Base.obj_logic_hint_preprocessor
  @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})›]]
and [[rec_uhint config: hint_preprocessor = ‹Unification_Hints_Base.obj_logic_hint_preprocessor
  @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})›]]

lemma eq_TrueI: "PROP P ⟹ PROP P ≡ Trueprop True" by (standard) simp
declare [[ucombine ‹Standard_Unification_Combine.eunif_data
  (Standard_Unification_Combine.metadata \<^binding>‹SIMPS_TO_unif› Prio.HIGH,
  Simplifier_Unification.SIMPS_TO_unify @{thm eq_TrueI}
  |> Unification_Combinator.norm_unifier (Unification_Util.inst_norm_term'
      Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify)
  |> K)›]]

declare [[ucombine ‹
  let open Term_Normalisation
    (*ignore changes of schematic variables to avoid loops due to index-raising of some tactics*)
    val eq_beta_eta_dummy_vars = apply2 (beta_eta_short #> dummy_vars) #> op aconv
    fun simp_unif unify_theory = Simplifier_Unification.simp_unify_progress eq_beta_eta_dummy_vars
      (Simplifier_Unification.SIMPS_TO_UNIF_unify @{thm eq_TrueI}
        Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify)
      (Unification_Util.inst_norm_term'
        Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify)
      (Standard_Mixed_Comb_Unification.first_higherp_comb_e_unify unify_theory)
  in
    Standard_Unification_Combine.eunif_data
    (Standard_Unification_Combine.metadata \<^binding>‹SIMPS_TO_UNIF_unif› Prio.HIGH, simp_unif)
  end›]]

end