Theory ML_Unification.ML_Unifiers

✐‹creator "Kevin Kappelmann"›
theory ML_Unifiers
  imports
    ML_Functor_Instances
    ML_Priorities
    ML_Unifiers_Base
    Simps_To
begin

paragraph ‹Summary›
text ‹More unifiers.›

paragraph ‹Derived Unifiers›

ML_file‹higher_order_pattern_decomp_unification.ML›
ML_file‹var_higher_order_pattern_unification.ML›

subparagraph ‹Unification via Simplification›

lemma eq_if_SIMPS_TO_UNIF_if_SIMPS_TO_UNIF:
  assumes "PROP SIMPS_TO_UNIF t t'"
  and "PROP SIMPS_TO_UNIF s t'"
  shows "s ≡ t"
  using assms by (simp add: SIMPS_TO_eq SIMPS_TO_UNIF_eq)

ML_file‹simplifier_unification.ML›

paragraph ‹Combining Unifiers›

ML_file‹unification_combine.ML›
ML‹
  @{functor_instance struct_name = Standard_Unification_Combine
    and functor_name = Unification_Combine
    and id = ‹""›}
›
local_setup ‹Standard_Unification_Combine.setup_attribute NONE›

paragraph ‹Mixture of Unifiers›

ML_file‹mixed_unification.ML›
ML‹
  @{functor_instance struct_name = Standard_Mixed_Unification
    and functor_name = Mixed_Unification
    and id = ‹""›
    and more_args = ‹structure UC = Standard_Unification_Combine›}
›

declare [[ucombine add = ‹Standard_Unification_Combine.eunif_data
  (Var_Higher_Order_Pattern_Unification.e_unify Unification_Combinator.fail_unify
  |> Unification_Combinator.norm_unifier
    (Unification_Util.inst_norm_term'
      Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
  |> K)
  (Standard_Unification_Combine.metadata \<^binding>‹var_hop_unif› Prio.HIGH)›]]

declare [[ucombine add = ‹
  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
    val unif = Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify
    val norms = Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify
  in
    Standard_Unification_Combine.eunif_data
      (Simplifier_Unification.simp_unify_progress eq_beta_eta_dummy_vars
        (Simplifier_Unification.simp_unify norms unif norms)
        (Unification_Util.inst_norm_term' norms)
        unif
      |> Type_Unification.e_unify Unification_Util.unify_types
      |> K)
      (Standard_Unification_Combine.default_metadata \<^binding>‹simp_unif›)
  end›]]

end