# 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.*