Theory Unify_Fact_Tactic

✐‹creator "Kevin Kappelmann"›
subsection ‹Fact Tactic›
theory Unify_Fact_Tactic
  imports
    Unify_Fact_Tactic_Base
    ML_Unifiers
begin

paragraph ‹Summary›
text ‹Setup of fact tactic and examples.›

ML‹
  @{functor_instance struct_name = Standard_Unify_Fact
    and functor_name = Unify_Fact
    and id = ‹""›
    and more_args = ‹val init_args = {
      normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify,
      unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify
    }›}
›
local_setup ‹Standard_Unify_Fact.setup_attribute NONE›
local_setup ‹Standard_Unify_Fact.setup_method NONE›

paragraph ‹Examples›

experiment
begin
lemma
  assumes h: "⋀x y. PROP P x y"
  shows "PROP P x y"
  by (ufact h)

lemma
  assumes "⋀P y. PROP P y x"
  shows "PROP P x"
  by (ufact assms where unifier = Higher_Order_Unification.unify) ―‹the line below is equivalent›
  (* using [[ufact unifier = Higher_Order_Unification.unify]] by (ufact assms) *)

lemma
  assumes "⋀x y. PROP A x ⟹ PROP B x ⟹ PROP P x"
  shows "⋀x y. PROP A x ⟹ PROP B x ⟹ PROP P x"
  using assms by ufact
end

end