Re: [isabelle] question about "fun"



Hi Jesus,

fun gener :: "'a list => (nat list * 'a list)"
  where
  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

I think you mean that you would prefer to have the case distinction a = b vs a ~= b built into the induction rule, instead of having to do it yourself each time you apply it. The function package never does such things automatically, in order to have a predictable berhaviour. If you know what rule you would like to see, you can also state it yourself and use the "induct_scheme" method to derive it, usually almost automatically. See ch. 5 of my thesis for details
(http://www4.in.tum.de/~krauss/diss/krauss_phd.pdf).

Cheers,
Alex






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