*To*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Subject*: Re: [isabelle] question about "fun"*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Thu, 17 Sep 2009 10:49:13 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

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

(http://www4.in.tum.de/~krauss/diss/krauss_phd.pdf). Cheers, Alex

- Previous by Date: Re: [isabelle] Induction rules of the function package
- Next by Date: Re: [isabelle] Induction rules of the function package
- Previous by Thread: [isabelle] question about "fun"
- Next by Thread: [isabelle] counter example checking from ML
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list