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