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
  functor_name: Unify_Fact
  id: ‹""›
  more_args: ‹val init_args = {
    normalisers = SOME Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify,
    unifier = SOME Standard_Mixed_Comb_Unification.first_higherp_comb_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 unifier: Higher_Order_Unification.unify) ―‹the line below is equivalent› *)
  supply [[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