Re: [isabelle] "PROOF FAILED for depth4"



On Thu, Apr 8, 2010 at 12:34 PM, Alexander Krauss <krauss at in.tum.de> wrote:

>  > lemma te_zero: "EX func t. func t = 0"
>>  >
>>  > proof (intro exI)
>>  >
>>  >  show "F s = 0"
>>  >
>>  >
>>
>> Thanks for the help. Unfortunately, I get an error from this, saying that
>> it can't solve goal by exported rule: F s = 0. Any hint on this will be
>> appreciated.
>>
>
> You may need to add type annotations to make sure that the types in your
> lemma statement are not more general than you want. Switch on "Isabelle ->
> Settings -> Show Types".
>
>
I see. However, why can't the types in the lemma be more general even the
function is existentially quantified? Can't a' and b' be instantiated to
real for F s = 0 in the proof?

Thanks
Steve


> Alex
>




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