[isabelle] easy going with trivial cases in inductive proofs



Hi,

I am trying to use the Isar proof language to write nice inductive
proofs. Some of my proofs have two or three interesting cases and a ton
of trivial cases dealt with by a line for each case, eg:

case Lookup thus ?case by auto next
case Seq thus ?case by auto next
case Update thus ?case by auto next
case UpdateA thus ?case by auto next

Is there some way to tell Isabelle using Isar that for the yet to be
proved cases do:

case * thus ?case by auto next

It just not fun having to write a line for each trivial case.

Carsten

--
It is forbidden to kill; therefore all murderers are punished unless they kill
in large numbers and to the sound of trumpets.                       Voltaire.





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