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
    and functor_name = Unify_Assumption
    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_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›
  (* using [[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