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.