Re: [isabelle] Eliminating two quantifiers in structural proof
On Sun, 16 Sep 2012, Alfio Martini wrote:
Forgot this one:
"∀x. ∀y. P x y ==> P a b"
assume "∀x. ∀y. P x y"
from this have "∀y. P a y" by (rule spec[where x =a])
from this show "P a b" by (rule spec[where x=b])
Yet more examples on this thread, using native natural deduction
statements in Isabelle/Pure, without any auxiliary HOL connectives getting
in the way:
assumes "⋀x y. P x y"
shows "P a b"
from `P a b` show ?thesis .
Using the Pure quantifier in the assumption, you get arbitrary instances
of the proposition for free, using unification behind the scenes. The
backquote notation is a "literal fact reference", stating an instance of
something you have already visibly in the proof context.
Here is the same, without the initial goal statement getting between you
and the understanding of natural deduction reasoning in a local context:
assume "⋀x y. P x y"
note `P a b`
have "P a b" by fact
So you build up a context with some general fact, and then project
instances from it. The backquote and "by fact" form are operationally
equalivalent, but the latter works via a local result with nested goal
state. Both forms have there uses in practical applications.
This archive was generated by a fusion of
Pipermail (Mailman edition) and