*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] finite sets and code generation, once again*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 14 Jul 2010 11:32:38 +0200*Organization*: TU München, Lehrstuhl Software and Systems Engineering*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.10) Gecko/20100527 Thunderbird/3.0.5

Hi Peter, > Anyway, I wanted to follow up your suggestion about using lists. Given the advice in Executable_Set and what you've said to Tjark, would you now suggest Fset instead? If so, can you perhaps sketch for me how Fset is used (there aren't any examples in the distribution)? a small sketch using a contrived example: Suppose we have the following operation on sets which shall be implemented: definition foo :: "nat ⇒ nat set ⇒ nat set" where "foo n A = insert n {n ∈ A. n mod 2 = 0}" To turn this executable, we formally define a lifted counterpart operating on fsets: definition foo' :: "nat ⇒ nat fset ⇒ nat fset" where [simp]: "foo' n A = Fset (foo n (member A))" Note that this should be done as thumb as possible, using the Fset and member conversions. The more stylized the lifted definition is, the easier the proofs are. Using [simp] yields reasonable ad-hoc automation. This definition is immediately followed by its dual, expressing foo in terms of foo': lemma [code]: "foo n A = member (foo' n (Fset A))" by simp The final step is to transfer the code equation of foo to a similar code equation for foo': lemma [code]: "foo' n A = Fset.insert n (Fset.filter (\<lambda>n. n mod 2 = 0) A)" by (simp add: foo_def) This lifting must be done for all operations involving sets in their type signature. I hope to provide automation for this one day. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] Finding the instantiation of a variable
- Next by Date: [isabelle] PhD Position in Automated Reasoning Using Machine Learning (vacancy number 62.58.10)
- Previous by Thread: Re: [isabelle] locales and 'types'
- Next by Thread: Re: [isabelle] finite sets and code generation, once again
- Cl-isabelle-users July 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