[isabelle] Case split for inductive definitions in Isar



Hi

I have a proof in which I wish to perform a case split as the proof method. Normally, I would just say

proof (cases A)

for something which was defined by primrec, or if I wanted to do a case split on its truth value. However, what I want to do a case split on was defined as an inductive datatype. I don't want to do induction, just a case split. I can do this "by hand", by proving a lemma which says "if the conclusion holds, then it must come from one of the clauses", and then use "moreover" blocks but this is cumbersome. Is there a way to call this proof method in Isar?

Thanks

Peter





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