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

nipkow at wrote:
    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"
As an intermediate goal you prove "NotB FalseB -e-> Not False".
I managed to find ways to avoid having to write intermediate lemmas which I will illustrate on a slightly more complex B _expression_:
lemma "AndB TrueB (NotB FalseB) -e-> True"
  apply(insert TrueB)
  apply(drule AndB)
  apply(insert FalseB)
  apply(drule NotB)
  apply simp+

lemma "AndB TrueB (NotB FalseB) -e-> True"
  apply(subgoal_tac "True = (True & True)", erule ssubst)
  apply(rule AndB, auto)
  apply(subgoal_tac "True = (Not False)", erule ssubst)
  apply(rule NotB, auto)
Hence forward proofs seem to do the trick.  Is this the way to handle it or is there a simpler way?
Thank you for you help as I learn the ropes.

Patrice Chalin, Assistant Professor -
Dependable Software Research Group, CSE Department, Concordia University

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