*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] simple proof question*From*: Ian Lynagh <igloo at earth.li>*Date*: Fri, 13 Aug 2010 12:06:44 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4C64F75F.9010702@in.tum.de>*References*: <20100813013625.GA1433@matrix.chaos.earth.li> <4C64F75F.9010702@in.tum.de>*User-agent*: Mutt/1.5.18 (2008-05-17)

Hi Tobias, On Fri, Aug 13, 2010 at 09:42:23AM +0200, Tobias Nipkow wrote: > > outermost universal quantifiers can and should > be dropped. Just write "STyping (EBool b, TBool)". Aha, thanks! > inductive_cases STypingE[elim!]: > "STyping (EBool b, t)" > > The resulting lemma STypingE is what you need. The magic "[elim!]" tells > auto and blast and friends to apply this rule eagerly. Now your proof > should just be > > from this have "t = TBool" by auto Do you mean like this?: lemma "((e, t) \<in> STyping) ==> (principalType e = Some t)" proof (induct e) case EBool from this have "t = TBool" by auto If so, the "by auto" fails with: *** Failed to finish proof *** At command "by". Thanks Ian

**Follow-Ups**:**Re: [isabelle] simple proof question***From:*Tobias Nipkow

**References**:**[isabelle] simple proof question***From:*Ian Lynagh

**Re: [isabelle] simple proof question***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Working with Vector Spaces
- Next by Date: Re: [isabelle] simple proof question
- Previous by Thread: Re: [isabelle] simple proof question
- Next by Thread: Re: [isabelle] simple proof question
- Cl-isabelle-users August 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