Re: [isabelle] strange error message



It is worth mentioning that Isabelle is based on a logical framework. Therefore inference rules such as allE are not built in, and variants (e.g. with different variable names) are easily introduced. 

Simple examples such as the one you include in your message (there are many in the documentation) are obviously good for learning, but as you gain experience, you will see that Isabelleâs built-in notions of abstraction and generalisation provide ways of plugging values into theorems without having to do low-level reasoning with quantifiers.

Larry Paulson


> On 13 Oct 2015, at 11:09, Christian Sternagel <c.sternagel at gmail.com> wrote:
> 
> Dear Michel,
> 
> the name ("x" and "y" in your examples) refers to variables of the fact
> you are using, which is "allE", not to names inside the current goal.
> 
> allE: âx. ?P x â (?P ?x â ?R) â ?R
> 
> As you can see, there is an "x" in "allE", but not "y", hence the error
> message.
> 
> hope this helps
> 
> chris
> 
> On 10/12/2015 05:58 PM, michel levy wrote:
>> I am a french beginner in Isabelle.
>> I write this very short theory with jEdit
>> 
>> theory all
>> imports Main
>> begin
>>  lemma "â x. P(w,x) â P(w,a)"
>>  apply(erule_tac x ="a" in allE)
>> *Her**e I have the goal P(w,a) ==> P(w,a)*
>>  oops
>> 
>>  lemma "â y. P(w,y) â P(w,a)"
>>  apply(erule_tac y= "a" in allE)
>> *Here I have the unexpected message No such variable in theorem : "?y"*
>>  oops
>> 
>> Why this difference between these proofs ?
>> 
> 





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