*To*: Steve W <s.wong.731 at googlemail.com>*Subject*: Re: [isabelle] "PROOF FAILED for depth4"*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Thu, 08 Apr 2010 16:21:29 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <k2t12d162d01004080713p1bb56cc6o691ac0f97e17bf3b@mail.gmail.com>*References*: <0016e6d9772208555a0483b7eb79@google.com> <4BBDBF57.5070002@in.tum.de> <k2t12d162d01004080713p1bb56cc6o691ac0f97e17bf3b@mail.gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

> 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 eventhe function is existentially quantified? Can't a' and b' beinstantiated to real for F s = 0 in the proof?

In HOL it is not possible to express existential quantification over types. Alex

**References**:**Re: [isabelle] "PROOF FAILED for depth4"***From:*Alexander Krauss

**Re: [isabelle] "PROOF FAILED for depth4"***From:*Steve W

- Previous by Date: Re: [isabelle] "PROOF FAILED for depth4"
- Next by Date: [isabelle] WST Deadline Extended (April 18)
- Previous by Thread: Re: [isabelle] "PROOF FAILED for depth4"
- Next by Thread: [isabelle] WST Deadline Extended (April 18)
- Cl-isabelle-users April 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list