Re: [isabelle] simple proof over inductively defined relation (operational semantics)
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.
As an intermediate goal you prove "NotB FalseB -e-> Not False".
> Along similar lines how does one prove that "2 : even" given the
> inductive definition of even found in the Isabelle tutorial.
apply(rule step, rule zero)
thm step[OF zero]
This archive was generated by a fusion of
Pipermail (Mailman edition) and