*To*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Subject*: Re: [isabelle] Recursion on finite sets*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Thu, 13 Nov 2008 11:45:18 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <491BCDF3.1090806@ipd.info.uni-karlsruhe.de>*References*: <491BCDF3.1090806@ipd.info.uni-karlsruhe.de>*User-agent*: Mozilla-Thunderbird 2.0.0.17 (X11/20081018)

Hi Andreas,

But I would rather like to have some function finite_rec :: "('b set =>'b => 'a => 'a) => 'a => 'b set => 'a" that satisfies"finite_rec f z {} = z" and "[| finite A; ~ (x : A) |] ==> finite f z (insert x A) = f A x (finite_rec f A z)" for all "well-formed" functions f.

Hmmm... How would you specify well-formed? It seems this is not easy... As far as I know, Finite_Set.fold is all we have at the moment. Alex

**References**:**[isabelle] Recursion on finite sets***From:*Andreas Lochbihler

- Previous by Date: [isabelle] New AFP entry: Secure information flow and program logics
- Next by Date: Re: [isabelle] Recursion on finite sets
- Previous by Thread: [isabelle] Recursion on finite sets
- Next by Thread: Re: [isabelle] Recursion on finite sets
- Cl-isabelle-users November 2008 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