*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] stuck on proof*From*: Ian Lynagh <igloo at earth.li>*Date*: Mon, 16 Aug 2010 17:16:40 +0100*User-agent*: Mutt/1.5.18 (2008-05-17)

Hi all, I'm stuck on a proof of lemma "(principalType e = Some t) ==> (STyping e t)" (details in attachment). I've managed to solve the EBool case with apply_end simp from "STypingBool" show "!!b. STyping (EBool b) TBool" apply simp . but I don't think this is a good proof: I'm sure using "apply_end simp" is bad style, and I don't think I should be copy/pasting "!!b. STyping (EBool b) TBool" from the proof state. Even "apply simp" I'm not sure is good style. I've therefore tried to write a better proof for the EInt case, but got nowhere. The attached script shows some of my meanderings. Has anyone got any hints, please? I'm also not sure what's going to happen when I get to a recursive case. I suspect "proof (cases e)" is not sufficient for the recursive case, but "proof (induct e)" doesn't look like it's generating the right goal for the recursive case (as t doesn't vary), and "proof (induct rule: SExpr.induct)" has the same problem. Again, can anyone point me in the right direction please? Incidentally, in proof general, the "Isabelle/Show me .../Facts" menu says "C-c C-a <h> <f>" next to it, but after typing just "ctrl-c ctrl-a h" emacs says "C-c C-a h is undefined". Any idea what's wrong? Thanks Ian

theory Simple imports Main begin datatype SExpr = EBool bool | EInt int | EGreaterThan SExpr SExpr datatype SType = TBool | TInt inductive STyping :: "SExpr => SType => bool" where STypingBool: "STyping (EBool b) TBool" | STypingInt: "STyping (EInt n) TInt" | STypingGreaterThan: "[| STyping lhs TInt; STyping rhs TInt |] ==> STyping (EGreaterThan lhs rhs) TBool" fun principalType :: "SExpr => SType option" where "principalType (EBool b) = Some TBool" | "principalType (EInt n) = Some TInt" | "principalType (EGreaterThan lhs rhs) = (case (principalType lhs, principalType rhs) of (Some TInt, Some TInt) => Some TBool | _ => None)" lemma "(principalType e = Some t) ==> (STyping e t)" proof (cases e) case EBool apply_end simp from "STypingBool" show "!!b. STyping (EBool b) TBool" apply simp . next case (EInt n) fix n assume "principalType (EInt n) = Some t" then have x : "principalType (EInt n) = Some TInt" by simp show ?thesis assume "t = TInt" then have "principalType (EInt int) = Some TInt" by simp show ?thesis have "t = TInt" show ?thesis have x : "principalType e = Some TInt" sorry have "t = TInt" with x show ?thesis fix x assume x : "principalType e = Some t" assume y : "e = EInt n" thus ?thesis by simp show ?thesis apply_end simp fix x thus ?thesis by simp from "STypingInt" show "!!int. STyping (EInt bool) TInt" apply simp . next case EGreaterThan sorry qed

**Follow-Ups**:**Re: [isabelle] stuck on proof***From:*Tobias Nipkow

**Re: [isabelle] stuck on proof***From:*Makarius

- Previous by Date: Re: [isabelle] Beginner's struggles
- Next by Date: Re: [isabelle] stuck on proof
- Previous by Thread: [isabelle] PhD position in Computational Logic at the University of Innsbruck
- Next by Thread: Re: [isabelle] stuck on proof
- 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