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


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
  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"
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"?

Patrice Chalin, Assistant Professor - http://www.cs.concordia.ca/~chalin
Dependable Software Research Group, CSE Department, Concordia University

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