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›

paragraph ‹Unification via Tactics›

ML_file‹tactic_unification.ML›

subparagraph ‹Unification via Simplification›

lemma eq_if_SIMPS_TO_UNIF_if_SIMPS_TO:
  assumes "PROP SIMPS_TO 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 = ‹Standard_Unification_Combine.eunif_data
  (Simplifier_Unification.simp_unify_progress Envir.aeconv Simplifier_Unification.simp_unify
    (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
  |> Type_Unification.e_unify Unification_Util.unify_types
  |> K)
  (Standard_Unification_Combine.default_metadata \<^binding>‹simp_unif›)
  ›]]

end