# Re: [isabelle] schematic variables and assumption

Dear Viorel,
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
Best!
On Tue, May 15, 2012 at 8:31 AM, Viorel Preoteasa
<viorel.preoteasa at abo.fi>wrote:
> Hello,
>
> I have the following lemma:
>
> lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)"
> apply (rule exI)
> apply (rule notI)
> apply (erule notE)
> apply (rule allI)
> apply assumption
>
> After the the rule "apply (rule allI)" the goal becomes:
> ⋀x. P ?x ⟹ P x
>
> I do not understand why "apply assumption" fail at this point.
> I would expect that ?x is unified with x and the proof succeed.
>
> Best regards,
>
> Viorel Preoteasa
>
>
--
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.*