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



    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
      
> 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)
or
apply(simp)
or
apply(blast)
or
thm step[OF zero]
or
....

Tobias





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