Theory ML_Unification.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
  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 use 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