*To*: nipkow at in.tum.de*Subject*: Re: [isabelle] simple proof over inductively defined relation (operational semantics)*From*: Patrice Chalin <chalin at cs.concordia.ca>*Date*: Sat, 21 Jan 2006 15:04:29 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20060121092022.2511639B29@atbroy30>*References*: <43D185CE.4010109@cs.concordia.ca> <20060121092022.2511639B29@atbroy30>*User-agent*: Thunderbird 1.4 (Windows/20050908)

nipkow at in.tum.de wrote:
I managed to find ways to avoid having to write intermediate lemmas which I will illustrate on a slightly more complex B _expression_:inductive eval intros TrueB: "TrueB -e-> True" FalseB: "FalseB -e-> False" NotB: "b -e-> b' ==> NotB b -e-> Not b'" lemmas eval.intros [intro] lemma not_false: "NotB FalseB -e-> True" oops ... As an intermediate goal you prove "NotB FalseB -e-> Not False". Hence forward proofs seem to do the trick. Is this the way to handle it or is there a simpler way? Thank you for you help as I learn the ropes. Cheers, Patrice -- Patrice Chalin, Assistant Professor - http://www.cs.concordia.ca/~chalin Dependable Software Research Group, CSE Department, Concordia University |

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Next by Date: [isabelle] proving that a value is outside of an inductively defined set
- Previous by Thread: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Next by Thread: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Cl-isabelle-users January 2006 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