Re: [isabelle] proof statement fails



So maybe the following will work...

lemma "(2 :: nat) + 2 = 4"
  proof(auto)

On 7 Jul 2012, at 09:00, Lawrence Paulson wrote:

> If you write “proof", then some default proof method (depending on the form of your goal) will be attempted. I'm not sure what it is in this case, but it obviously failing. Write
> 
> 	proof -
> 
> to open a proof without attempting a proof method.
> 
> Similarly, if you try to develop a structured proof by experimenting with lines of the form “apply <method>", you may find that everything fails for no apparent reason. It is the same reason as before, and can be fixed by ensuring that your first line is “apply -". This is particularly important if you have chained facts.
> 
> Larry Paulson
> 
> 
> On 7 Jul 2012, at 07:51, Gergely Buday wrote:
> 
>> Hi,
>> 
>> I have written
>> 
>> theory Let
>> imports Main
>> begin
>> 
>> lemma "(2 :: nat) + 2 = 4"
>>   proof
>> 
>> Now, 'proof' results in
>> 
>> "empty result sequence -- proof command failed"
>> 
>> Otherwise, i.e. without Isar,
>> 
>> apply (auto)
>> 
>> finishes the proof, so the lemma itself is well-written. What else could fail?
>> 
>> - Gergely
>> 
> 
> 






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