[isabelle-dev] sets and code generation

[Lukas Bulwahn]

On 03/21/2012 08:36 AM, Christian Sternagel wrote:
> Hi there,
>
> since set is a proper type some code equations that used to work, no 
> longer do, e.g.,
>
> "op |> = {(x, y). supt_impl x y}"
>
> as a code equation leads to an error stating that terms (x and y are 
> first-order terms) do not support the enum class. Since the possible 
> terms (using strings as function symbols and variables) cannot be 
> enumerated in a (finite) list, I can also not introduce an enum instance.

Introducing 'a set as a type constructor now allows us to refine the set 
operations to operations on lists (by Florian's way of data refinement 
for code generation).
However, this now disallows the execution of "op |>" on the type "... 
set". To execute this, you have to move this specification to predicates 
('a => bool):

Define "op |> = (%(x, y). supt_impl x y)"


Lukas