Re: [isabelle] proof statement fails



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.