*To*: Ian Lynagh <igloo at earth.li>*Subject*: Re: [isabelle] simple proof question*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 13 Aug 2010 09:42:23 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20100813013625.GA1433@matrix.chaos.earth.li>*References*: <20100813013625.GA1433@matrix.chaos.earth.li>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

Ian Lynagh schrieb: > Hi all, > > I'm trying to write a simple proof in Isabelle, but I'm a little lost. I > wonder if anyone can help me please? I've attached the script I have so > far. > > At the point at which I am stuck, I have > using this: > (EBool bool_, t) : STyping > and I want to show that "t = TBool", which must be true as > STypingBool: "forall (b :: bool) ==> STyping (EBool b, TBool)" For a start, your "forall (b :: bool) ==>" is a bit weird. Isabelle accepted it but had to interpret "forall" as a free function variable to make sense of it. Probably not what you meant. Note that "forall" is not Isabelle speak, and that outermost universal quantifiers can and should be dropped. Just write "STyping (EBool b, TBool)". Now the proof. > is the only constructor matching that pattern. My best guess was > proof (cases this) You cannot do a case distintinction on a theorem ("this") but only on a term. This suggests proof (cases t) Although this step works, it does not get you anywhere. Before you start the whole proof you should deduce some elimination rules that allow you to move from "(EBool b, t) : STyping" to "t = TBool". This can be done automatically: 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 Important: you will have to extend STypingE with other cases, at least inductive_cases STypingE[elim!]: "STyping (EBool b, t)" "STyping (EInt n, t)" Tobias > but that says > *** empty result sequence -- proof command failed > *** At command "proof". > Can anyone give me a pointer in the right direction please? > > > I'm also not sure why I can't do > apply simpl > immediately after > case EBool > ? My goal here was to try to get "principalType (EBool bool)" to reduce. > > > Finally, I'd also be very interested to know if the general structure > looks sensible, or if there would be a more sensible way to write this > sort of proof. > > > Thanks > Ian > >

**Follow-Ups**:**Re: [isabelle] simple proof question***From:*Ian Lynagh

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

- Previous by Date: Re: [isabelle] Unfolding setsum
- Next by Date: Re: [isabelle] Comparing square roots
- Previous by Thread: [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