# [isabelle] Problem with mutual induction

Hello everyone,
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':
----------8<-------------
(* Problem with mutual induction *)
theory foobar
imports Main
begin
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?
Thank you very much for an answer!
Kind regards
Mattias
--
Mattias Ulbrich
Logik und Formale Methoden (Prof. Dr. P.H. Schmitt)
Institut für Theoretische Informatik lfm.iti.uka.de
Universität Karlsruhe

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