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

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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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