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 ‹Unification_Combine.eunif_data
  (Unification_Combine.metadata (\<^binding>‹SIMPS_TO_unify›, Prio.HIGH),
  Simplifier_Unification.SIMPS_TO_unify @{thm eq_TrueI}
  |> Unification_Combinator.norm_unifier (Unification_Util.inst_norm_term'
      Mixed_Comb_Unification.norms_fo_hop_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 (Same.commit 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}
        Mixed_Comb_Unification.norms_fo_hop_comb_unify)
      (Unification_Util.inst_norm_term'
        Mixed_Comb_Unification.norms_fo_hop_comb_unify)
      (Mixed_Comb_Unification.fo_hop_comb_e_unify Unification_Util.unify_types
        unify_theory)
  in
    Unification_Combine.eunif_data
    (Unification_Combine.metadata (\<^binding>‹SIMPS_TO_UNIF_unify›, Prio.HIGH), simp_unif)
  end›]]

end