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
  functor_name: Unify_OF
  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,
    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 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 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 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 unifier: First_Order_Unification.unify]) ―‹the line below is equivalent›
  (* supply [[uOF unifier: First_Order_Unification.unify]] by (fact h1[uOF h2]) *)
end

end