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.