nipkow at in.tum.de wrote:
I managed to find ways to avoid having to write intermediate lemmas which I will illustrate on a slightly more complex B _expression_: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".
Hence forward proofs seem to do the trick. Is this the way to handle it or is there a simpler way?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
Thank you for you help as I learn the ropes.
-- Patrice Chalin, Assistant Professor - http://www.cs.concordia.ca/~chalin Dependable Software Research Group, CSE Department, Concordia University