# Re: [isabelle] Problem with mutual induction

```On Tue, 21 Oct 2008, Mattias Ulbrich wrote:

> I experienced problems with a HOL formalisation written for an older
> version of Isabelle. It successfully makes use of several mutual
> inductions but I cannot redo these proofs in Isabelle2008.
>
> The problem boils down to the observation that a mutual induction can
> only be performed if a proof obligation has at least two 'parts':

> datatype foo = Foo bar | Empty
>   and bar = Bar foo
>
> (* this works: thesis has two parts *)
> lemma
>   shows "P (f::foo) (b::bar)"
>   and True
> apply (induct b and f)
> sorry
>
> (* this does NOT work: Error message
> *** empty result sequence -- proof command failed
> *** At command "apply".
> *)
> lemma
>   shows "P (f::foo) (b::bar)"
> apply (induct b and f)
> sorry
>
> ----------8<-------------
>
> Is this behaviour intended? Shouldn't be the induction also possible in
> the second case?

Yes, the "induct" method merely assembles given induction rules in a
certain way (that is occasionally hard to analyse when things go wrong)
expecting that the goal structure matches the basic rule outline. Writing
(induct b and f) refers to the simultaneous rule of the corresponding
simultaneous type.

Maybe src/HOL/Induct/Common_Patterns.thy helps to get a practical grip on
how things work.  There are further sophistications of induct in the
pipeline, and there might also be some kind of interactive proof scheme
synthesis coming at some later stage.

Since "projected inductions" where some predicates are always True are a
common case, the packages that produce induction rules could do a bit
better in providing these additional version: foo.induct and bar.induct
where one part of the full foo_bar.inducts is already instantiated with
True.

If you have a dire need for such rules you may also produce them yourself
for your specific definitions.  The "induct" method will accept them when
specified with "rule: ..." for example.

Makarius

```

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