[isabelle] question about "fun"

Dear all,

I was trying to produce a "fun" definition that given a list produces
a couple of lists (the following definition of "gener" is just a
simplified version where my question already arises).

fun gener :: "'a list => (nat list * 'a list)"
  gener_Cons: "gener (a # b # l) =
  (if a = b then (0 # fst (gener (b # l)), snd (gener (b # l)))
     else (fst (gener l), snd (gener l)))"
  |gener_Nil: "gener a = ([], a)"

Somehow, the induction rule associated to the previous definition:

thm gener.induct

has the following aspect:

\<And> a b l. [| a = b ==> ?P (b # l); a = b ==> ?P (b # l); a
\<noteq> b ==> ?P l; a \<noteq> b ==> ?P l |] ==> ?P (a # b # l);
 ?P []; \<And>v. ?P [v] |]
==> ?P ?a0.0

where both cases "a = b" and "a \<noteq> b" appear twice, which does
not pose any limitation but may result a bit annoying when trying to
number hypothesis.

May somebody know a way to avoid this behaviour?

Thanks in advance,


Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

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