# Re: [isabelle] schematic variables and assumption

```On Tue, 15 May 2012, Alfio Martini wrote:

```
```If I am not wrong, this is a classical conjecture. Here goes a
possible proof:

lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)"
apply (rule ccontr)
apply (erule notE)
apply (rule allI)
apply (rule ccontr)
apply (erule notE)
apply (rule exI)
apply (assumption)
done
```
```
```
We've been an the same point just yesterday in our Isabelle tutorial at Paris Sud point, but nobody could give me the proof on the spot. See http://www.lri.fr/~wenzel/Isabelle_Orsay_2012/Calculation.thy Exercise (2) about the Drinker's principle.
```
```
The idea was to play with proof structure and automated tools to bridge the gaps, and show the possibilities and limitations of this approach. The question of the assignment "Do you believe the proof?" (a skeleton involving 3 "blast" steps) was answered negatively by everybody. Afterwards I've made a fully explicit Isar proof, and managed to convince at least half of the audience that this is correct classical nonsense.
```
```
To complete my own exercise from yesterday, here is now de_Morgan as above (using the more generic rule classical instead of ccontr) together with the explicit version of the Drinker's principle:
```
lemma de_Morgan:
assumes "¬ (∀x. P x)"
shows "∃x. ¬ P x"
proof (rule classical)
assume "¬ (∃x. ¬ P x)"
have "∀x. P x"
proof
fix x show "P x"
proof (rule classical)
assume "¬ P x"
then have "∃x. ¬ P x" ..
with `¬ (∃x. ¬ P x)` show ?thesis ..
qed
qed
with `¬ (∀x. P x)` show ?thesis ..
qed

theorem "∃a. drunk a ⟶ (∀x. drunk x)"
proof cases
assume "∀x. drunk x"
fix a
have "drunk a ⟶ (∀x. drunk x)"
using `∀x. drunk x` ..
then show ?thesis ..
next
assume "¬ (∀x. drunk x)"
then have "∃a. ¬ drunk a" by (rule de_Morgan)
then obtain a where "¬ drunk a" ..
have "drunk a ⟶ (∀x. drunk x)"
proof
assume "drunk a"
with `¬ drunk a` show "∀x. drunk x" by contradiction
qed
then show ?thesis ..
qed

```
For demonstration purposes in such Pure examples, I usually refer to previous facts literally with `prop`, to avoid the Spaghetti tendency of named references like *, **, *** or 1, 2, 3 etc.
```

Makarius```

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