*To*: Alexander Krauss <krauss at in.tum.de>, Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] sets in HOL/CF*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Thu, 2 Sep 2010 23:27:49 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4C800224.5040709@in.tum.de>*References*: <1283420967.29045.6.camel@kirk> <AANLkTikGOm7V=-ZC8f0QX4HO58nzS5uR_BYesg4Eh26F@mail.gmail.com> <4C800224.5040709@in.tum.de>

Am 02.09.2010 um 21:59 schrieb Alexander Krauss: > Brian Huffman wrote: >> If you want to be able to define a function of type "nat -> nat set" >> with fixrec, it turns out that fixrec can do it, but it requires you >> to do some work to set things up first. > > A related remark: A recursive function that returns a set can also be defined using the inductive(_set) package. You have to rephrase the definition using introduction rules, and manually derive the recursive equations afterwards, but that is usually straightforward. Actually, Lukas's newly introduced "inductive_simps" command makes it easier than ever to derive recursive equations from inductive definitions. I think it's in Isabelle2009-2. I'm not aware of any documentation (beyond a few uses in Isabelle theories, which you can grep for) but it works pretty much like "inductive_cases". Jasmin

**References**:**[isabelle] sets in HOL/CF***From:*Joachim Breitner

**Re: [isabelle] sets in HOL/CF***From:*Brian Huffman

**Re: [isabelle] sets in HOL/CF***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
- Next by Date: Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
- Previous by Thread: Re: [isabelle] sets in HOL/CF
- Next by Thread: [isabelle] introduction rule for order bounded quantifiers.
- Cl-isabelle-users September 2010 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