# Re: [isabelle] Eliminating two quantifiers in structural proof

On Sun, 16 Sep 2012, Alfio Martini wrote:

Forgot this one:
theorem th11d:
"∀x. ∀y. P x y ==> P a b"
proof -
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])
qed

`Yet more examples on this thread, using native natural deduction
``statements in Isabelle/Pure, without any auxiliary HOL connectives getting
``in the way:
`
lemma
assumes "⋀x y. P x y"
shows "P a b"
proof -
from `P a b` show ?thesis .
qed

`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:
`
notepad
begin
assume "⋀x y. P x y"
note `P a b`
have "P a b" by fact
end

`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.
`
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*