# 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:
```
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.