[isabelle-dev] sets and code generation

[Christian Sternagel]

On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
> 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
Sorry I don't quite get it. op |>  is already defined to be of type 
"('f, 'v) term rel" (and used heavily as a set). So the above equation 
would not be well-typed. Is your suggestion to change op |> into a 
predicate?

cheers

chris