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



nipkow at in.tum.de wrote:
    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
...
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+
done

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)
done
  
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.

Cheers,
Patrice
-- 
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.