Email Gateway (Aug 18 2022 at 18:40): Email Gateway (Aug 18 2022 at 18:40):From: Christian Urban <urbanc@in.tum.de>
Hi John,
Mutual inductions can be a bit fiddly. Therefore inductive,
datatype and other tools provide an "*.inducts" rule. This
rule is essentially the projection of the "*.induct" rule.
(So no need to state the rule using conjunctions.) With this
the induct method can more easily figure out which induction
to perform. There used to be an example theory in the Isabelle
distribution which explains all bells and whistles of the
induct-method, but I cannot find it at the moment. Maybe others
can point to it. Below is a theory that should work in your example.
Hope this helps,
Christian
Ribbons.thy
Last updated: Nov 21 2024 at 12:39 UTC