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