*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] simple proof over inductively defined relation (operational semantics)*From*: Patrice Chalin <chalin at cs.concordia.ca>*Date*: Fri, 20 Jan 2006 19:52:30 -0500*User-agent*: Thunderbird 1.4 (Windows/20050908)

Hi, Consider the following simplified version of HOL/IMP/Expr.thy: How do I prove not_false? I haven't been able to find a way. Of course, if I change the True to (Not False) it becomes easy because that matches the NotB rule, but in general given a B term, bb, which I know should be True, how to I prove "bb -e-> True"?theory OpSemB = Main: datatype B = TrueB | FalseB | NotB B | ... consts eval :: "(B * bool) set" syntax "_eval" :: "B => bool => bool" (infixl "-e->" 50) translations "b -e-> b'" == "(b,b') : eval" 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 Along similar lines how does one prove that "2 : even" given the inductive definition of even found in the Isabelle tutorial. My guess was that I would need the equivalent of a 2_def rule. How might I prove, e.g. "22 : even"? Thanks, Patrice -- Patrice Chalin, Assistant Professor - http://www.cs.concordia.ca/~chalin Dependable Software Research Group, CSE Department, Concordia University |

**Follow-Ups**:

- Previous by Date: [isabelle] European Master's Program in Computational Logic
- Next by Date: [isabelle] subst_tac?
- Previous by Thread: [isabelle] European Master's Program in Computational Logic
- 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