Re: [isabelle] schematic variables and assumption



Such a step would not be sound. You can only unify ?x with terms containing no bound variables. Variable capture is never allowed.

Your example is quite tricky to prove in a natural deduction calculus. Of course, it's trivial if you use automation.

Larry Paulson


On 15 May 2012, at 12:31, Viorel Preoteasa 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
> 






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