[isabelle-dev] sets and code generation

Christian Sternagel c-sterna at jaist.ac.jp
Wed Mar 21 09:08:29 CET 2012

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 



More information about the isabelle-dev mailing list