Theory Unify_Resolve_Tactics
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)
oops
lemma
assumes h: "PROP C x"
shows "PROP C x"
by (urule h unifier: First_Order_Unification.unify)
lemma
assumes h: "⋀x. PROP A x ⟹ PROP D x"
shows "⋀x. PROP A x ⟹ PROP B x ⟹ PROP C x"
apply (urule (d) 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"
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"
using h2 apply (urule h1 chained: fact)
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)
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