[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':


(*   Problem with mutual induction   *)

theory foobar
imports Main

datatype foo = Foo bar | Empty
  and bar = Bar foo

(* this works: thesis has two parts *)
  shows "P (f::foo) (b::bar)"
  and True
apply (induct b and f)

(* this does NOT work: Error message
*** empty result sequence -- proof command failed
*** At command "apply".
  shows "P (f::foo) (b::bar)"
apply (induct b and f)


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 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.