Re: [isabelle] schematic variables and assumption



Dear Makarius,

The corresponding Isar proof I had done, which follows the procedural one
below was this one:

lemma
assumes p: "(¬ (∀ x . P x))"
shows "(∃ x . ¬ P x)"
  proof (rule ccontr)
     assume h1: "¬ (∃x. ¬ P x)"
     have  "∀x. P x"
       proof (rule allI)
         fix x0
         show "P x0"
           proof (rule ccontr)
             assume "¬ P x0"
             from this have "∃ x. ¬P x" by (rule exI)
             with h1 show False by (rule notE)
          qed
       qed
     with p show False by (rule notE)
  qed

But since I am still learning Isar, it does not look as elegant as yours!

best!
On Wed, May 16, 2012 at 1:55 PM, Makarius <makarius at sketis.net> wrote:

> 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<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




-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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