Theory Unification_Attributes

✐‹creator "Kevin Kappelmann"›
theory Unification_Attributes
  imports
    Unification_Attributes_Base
    ML_Unifiers
begin

paragraph ‹Summary›
text ‹Setup of OF attribute with adjustable unifier.›

ML‹
  @{functor_instance struct_name = Standard_Unify_OF
    and functor_name = Unify_OF
    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,
      mode = SOME (Unify_OF_Args.PM.key Unify_OF_Args.PM.fact)
    }›}
›
local_setup ‹Standard_Unify_OF.setup_attribute NONE›

paragraph ‹Examples›

experiment
begin
lemma
  assumes h1: "(PROP A ⟹ PROP D) ⟹ PROP E ⟹ PROP C"
  assumes h2: "PROP B ⟹ PROP D"
  and h3: "PROP F ⟹ PROP E"
  shows "(PROP A ⟹ PROP B) ⟹ PROP F ⟹ PROP C"
  by (fact h1[uOF h2 h3 where mode = resolve]) ―‹the line below is equivalent›
  (* by (fact h1[OF h2 h3]) *)

lemma
  assumes h1: "(PROP A ⟹ PROP A)"
  assumes h2: "(PROP A ⟹ PROP A) ⟹ PROP B"
  shows "PROP B"
  by (fact h2[uOF h1]) ―‹the line below is equivalent›
  (* by (fact h2[uOF h1 where mode = fact]) *)
  ―‹Note: @{attribute OF} would not work in this case:›
  (* thm h2[OF h1] *)

lemma
  assumes h1: "⋀x y z. PROP P x y ⟹ PROP P y y ⟹ (PROP A ⟹ PROP A) ⟹
    (PROP A ⟹ PROP B) ⟹ PROP C"
  and h2: "⋀x y. PROP P x y"
  and h3 : "PROP A ⟹ PROP A"
  and h4 : "PROP D ⟹ PROP B"
  shows "(PROP A ⟹ PROP D) ⟹ PROP C"
  by (fact h1[uOF h2 h2 h3, uOF h4 where mode = resolve])

lemma
  assumes h1: "⋀P x. PROP P x ⟹ PROP E P x"
  and h2: "PROP P x"
  shows "PROP E P x"
  by (fact h1[uOF h2]) ―‹the following line does not work (multiple unifiers error)›
  (* by (fact h1[OF h2]) *)

text‹We can also specify the unifier to be used:›

lemma
  assumes h1: "⋀P. PROP P ⟹ PROP E"
  and h2: "⋀P. PROP P"
  shows "PROP E"
  by (fact h1[uOF h2 where unifier = First_Order_Unification.unify]) ―‹the line below is equivalent›
  (* using [[uOF unifier = First_Order_Unification.unify]] by (fact h1[uOF h2]) *)
end

end