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"?
-- Patrice Chalin, Assistant Professor - http://www.cs.concordia.ca/~chalin Dependable Software Research Group, CSE Department, Concordia University