Theory Unify_Resolve_Tactics

✐‹creator "Kevin Kappelmann"›
subsection ‹Resolution Tactics›
theory Unify_Resolve_Tactics
  imports
    Unify_Resolve_Tactics_Base
    ML_Unifiers
begin

paragraph ‹Summary›
text ‹Setup of resolution tactics and examples.›

ML‹
  @{functor_instance struct_name = Standard_Unify_Resolve
    and functor_name = Unify_Resolve
    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_Resolve_Args.PM.key Unify_Resolve_Args.PM.any),
      chained = SOME (Unify_Resolve_Args.PCM.key Unify_Resolve_Args.PCM.resolve)
    }›}
›
local_setup ‹Standard_Unify_Resolve.setup_attribute NONE›
local_setup ‹Standard_Unify_Resolve.setup_method NONE›

paragraph ‹Examples›

experiment
begin

lemma
  assumes h: "⋀x. PROP D x ⟹ PROP C x"
  shows "⋀x. PROP A x ⟹ PROP B x ⟹ PROP C x"
  apply (urule h) ―‹the line below is equivalent›
  (* apply (rule h) *)
  oops

lemma
  assumes h: "PROP C x"
  shows "PROP C x"
  by (urule h where unifier = First_Order_Unification.unify) ―‹the line below is equivalent›
  (* using [[urule unifier = First_Order_Unification.unify]] by (urule h) *)

lemma
  assumes h: "⋀x. PROP A x ⟹ PROP D x"
  shows "⋀x. PROP A x ⟹ PROP B x ⟹ PROP C x"
  ―‹use (r,e,d,f) to specify the resolution mode (resolution, elim, dest, forward)›
  apply (urule (d) h) ―‹the line below is equivalent›
  (* apply (drule h) *)
  oops

lemma
  assumes h1: "⋀x. PROP A x ⟹ PROP D x"
  and h2: "⋀x. PROP D x ⟹ PROP E x"
  shows "⋀x. PROP A x ⟹ PROP B x ⟹ PROP C x"
  ―‹use (rr,re,rd,rf) to use repetition; in particular: ‹(urule (rr)) ≃ intro››
  apply (urule (rd) h1 h2)
  oops


text‹You can specify how chained facts should be used. By default, @{method urule} works like
@{method rule}: it uses chained facts to resolve against the premises of the passed rules.›

lemma
  assumes h1: "⋀x. (PROP F x ⟹ PROP E x) ⟹ PROP C x"
  and h2: "⋀x. PROP F x ⟹ PROP E x"
  shows "⋀x. PROP A x ⟹ PROP B x ⟹ PROP C x"
  ―‹Compare all of the following calls:›
  (* apply (rule h1) *)
  (* apply (urule h1) *)
  (* using h2 apply (rule h1) *)
  (* using h2 apply (urule h1) *)
  using h2 apply (urule h1 where chained = fact)
  (* using h2 apply (urule h1 where chained = insert) *)
  done

text‹You can specify whether any or every rule must resolve against the goal:›

lemma
  assumes h1: "⋀x y. PROP C y ⟹ PROP D x ⟹ PROP C x"
  and h2: "⋀x y. PROP C x ⟹ PROP D x"
  and h3: "⋀x y. PROP C x"
  shows "⋀x. PROP A x ⟹ PROP B x ⟹ PROP C x"
  using h3 apply (urule h1 h2 where mode = every)
  (* using h3 apply (urule h1 h2) *)
  done

lemma
  assumes h1: "⋀x y. PROP C y ⟹ PROP A x ⟹ PROP C x"
  and h2: "⋀x y. PROP C x ⟹ PROP B x ⟹ PROP D x"
  and h3: "⋀x y. PROP C x"
  shows "⋀x. PROP A x ⟹ PROP B x ⟹ PROP C x"
  using h3 apply (urule (d) h1 h2 where mode = every)
  oops

end

end