*To*: Ian Lynagh <igloo at earth.li>*Subject*: Re: [isabelle] stuck on proof*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 17 Aug 2010 10:07:53 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20100816161640.GB16241@matrix.chaos.earth.li>*References*: <20100816161640.GB16241@matrix.chaos.earth.li>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

lemma "(principalType e = Some t) ==> (STyping e t)" apply (induct e arbitrary: t) apply (auto simp: STyping.intros split:option.splits SType.splits) done split: ... instructs auto (or simp) to split case expressions for certain types automatically. Tobias Ian Lynagh schrieb: > 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 > >

**Follow-Ups**:**Re: [isabelle] stuck on proof***From:*Lars Noschinski

**Re: [isabelle] stuck on proof***From:*Ian Lynagh

**References**:**[isabelle] stuck on proof***From:*Ian Lynagh

- Previous by Date: [isabelle] stuck on proof
- Next by Date: Re: [isabelle] stuck on proof
- Previous by Thread: [isabelle] stuck on proof
- 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