# [isabelle] simple proof over inductively defined relation (operational semantics)

 Hi, Consider the following simplified version of HOL/IMP/Expr.thy: ```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 ``` 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"? 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:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.