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.›

MLfunctor_instancestruct_name: Standard_Unify_Resolve
  functor_name: Unify_Resolve
  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_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 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 chained: fact)
  (* using h2 apply (urule h1 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 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 mode: every)
  oops

end

end