*To*: chalin at cs.concordia.ca*Subject*: Re: [isabelle] simple proof over inductively defined relation (operational semantics)*From*: nipkow at in.tum.de*Date*: Sat, 21 Jan 2006 10:20:22 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43D185CE.4010109@cs.concordia.ca> (message from Patrice Chalin on Fri, 20 Jan 2006 19:52:30 -0500)*References*: <43D185CE.4010109@cs.concordia.ca>

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 > How do I prove not_false? I haven't been able to find a way. As an intermediate goal you prove "NotB FalseB -e-> Not False". > Along similar lines how does one prove that "2 : even" given the > inductive definition of even found in the Isabelle tutorial. apply(rule step, rule zero) or apply(simp) or apply(blast) or thm step[OF zero] or .... Tobias

**Follow-Ups**:

**References**:**[isabelle] simple proof over inductively defined relation (operational semantics)***From:*Patrice Chalin

- Previous by Date: [isabelle] subst_tac?
- Next by Date: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Previous by Thread: [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