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 where hint_preprocessor = ‹Unification_Hints_Base.obj_logic_hint_preprocessor
  @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})›]]
and [[rec_uhint where 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 add = ‹Standard_Unification_Combine.eunif_data
  (Simplifier_Unification.SIMPS_TO_unify @{thm eq_TrueI}
  |> Unification_Combinator.norm_closed_unifier
    (Unification_Util.inst_norm_term'
      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
  |> Unification_Combinator.unifier_from_closed_unifier
  |> K)
  (Standard_Unification_Combine.metadata \<^binding>‹SIMPS_TO_unif› Prio.HIGH)›]]

declare [[ucombine add = ‹Standard_Unification_Combine.eunif_data
  (Simplifier_Unification.simp_unify_progress Envir.aeconv
    (Simplifier_Unification.SIMPS_TO_UNIF_unify @{thm eq_TrueI})
    (Unification_Util.inst_norm_term'
      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
    Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify
    Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify
  |> K)
  (Standard_Unification_Combine.metadata \<^binding>‹SIMPS_TO_UNIF_unif› Prio.HIGH)›]]


end