*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] simple proof question*From*: Ian Lynagh <igloo at earth.li>*Date*: Fri, 13 Aug 2010 02:36:25 +0100*User-agent*: Mutt/1.5.18 (2008-05-17)

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)" is the only constructor matching that pattern. My best guess was proof (cases this) 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

theory Simple imports Main begin datatype SExpr = EBool bool | EInt int | EIfThenElse SExpr SExpr SExpr | EGreaterThan SExpr SExpr | EBoolToInt SExpr datatype SType = TBool | TInt inductive STyping :: "(SExpr * SType) => bool" where STypingBool: "forall (b :: bool) ==> STyping (EBool b, TBool)" | STypingInt: "forall (n :: int) ==> STyping (EInt n, TInt)" | STypingIfThenElse: "[| STyping (guard, TBool); STyping (exprTrue, t); STyping (exprFalse, t) |] ==> STyping (EIfThenElse guard exprTrue exprFalse, t)" | STypingGreaterThan: "[| STyping (lhs, TInt); STyping (rhs, TInt) |] ==> STyping (EGreaterThan lhs rhs, TBool)" | STypingBoolToInt: "STyping (b, TBool) ==> STyping (EBoolToInt b, TInt)" fun principalType :: "SExpr => SType option" where "principalType (EBool b) = Some TBool" | "principalType (EInt n) = Some TInt" | "principalType (EIfThenElse guard exprTrue exprFalse) = (case (principalType guard, principalType exprTrue, principalType exprFalse) of (Some TBool, Some t1, Some t2) => if t1 = t2 then Some t1 else None | _ => None)" | "principalType (EGreaterThan lhs rhs) = (case (principalType lhs, principalType rhs) of (Some TInt, Some TInt) => Some TBool | _ => None)" | "principalType (EBoolToInt b) = (case principalType b of Some TBool => Some TInt | _ => None)" lemma "((e, t) \<in> STyping) ==> (principalType e = Some t)" proof (induct e) case EBool from this have "t = TBool" (* The next line gives: *** empty result sequence -- proof command failed *** At command "proof". *) proof (cases this)

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

- Previous by Date: [isabelle] Unfolding setsum
- Next by Date: Re: [isabelle] class instance of a record extension
- Previous by Thread: Re: [isabelle] Unfolding setsum
- 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