# Re: [isabelle] finite sets and code generation, once again

• 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)"

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
Description: OpenPGP digital signature

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