Theory Unify_Assumption_Tactic

✐‹creator "Kevin Kappelmann"›
theory Unify_Assumption_Tactic
  imports
    Unify_Assumption_Tactic_Base
    ML_Unifiers
begin

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

ML‹
\<^functor_instance>‹struct_name: Standard_Unify_Assumption
  functor_name: Unify_Assumption
  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_Assumption.setup_attribute NONE›
local_setup ‹Standard_Unify_Assumption.setup_method NONE›


paragraph ‹Examples›

experiment
begin

lemma "PROP P ⟹ PROP P"
  by uassm

lemma
  assumes h: "⋀P. PROP P"
  shows "PROP P x"
  using h by uassm

schematic_goal "⋀x. PROP P (c :: 'a) ⟹ PROP ?Y (x :: 'a)"
  by uassm

schematic_goal a: "PROP ?P (y :: 'a) ⟹ PROP ?P (?x :: 'a)"
  by uassm ―‹compare the result with following call›
  (* by assumption *)

schematic_goal
  "PROP ?P (x :: 'a) ⟹ PROP P (?x :: 'a)"
  by uassm ―‹compare the result with following call›
  (* by assumption *)

schematic_goal
  "⋀x. PROP D ⟹ (⋀P y. PROP P y x) ⟹ PROP C ⟹ PROP P x"
  by (uassm unifier: Higher_Order_Unification.unify) ―‹the line below is equivalent›
  (* supply [[uassm unifier: Higher_Order_Unification.unify]] by uassm *)

text ‹Unlike @{method assumption}, @{method uassm} will not close the goal if the order of premises
of the assumption and the goal are different. Compare the following two examples:›

lemma "⋀x. PROP D ⟹ (⋀y. PROP A y ⟹ PROP B x) ⟹ PROP C ⟹ PROP A x ⟹ PROP B x"
  by uassm

lemma "⋀x. PROP D ⟹ (⋀y. PROP A y ⟹ PROP B x) ⟹ PROP A x ⟹ PROP C ⟹ PROP B x"
  by assumption
  (* by uassm *)
end

end