[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Stefan Berghofer]

Alexander Krauss wrote:
> I want to emphasize that the limitation of the code generator mentioned
> here not only applies to sets-as-predicates but also to
> maps-as-functions and other abstract types that are often specified in
> terms of functions (finite maps, almost constant maps, etc.). Thus,
> having good old 'a set back is does not fully solve this problem as a
> whole, just one (important) instance of it.
> 
> My view on this whole topic is outlined in the report I recently sent
> around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated
> since last time). In the long run, I would prefer to see flexible
> transport machinery to move stuff between isomorphic types.

Hi Alex,

thanks for your excellent report, I fully agree with this view. There is
often a tradeoff between executability and conciseness / abstractness of
specifications, so I don't think it is a good idea to tweak the logic in
such a way that it is more suitable for code generation. For example,
HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element
from the worklist, which is highly non-executable but more abstract, since
one does not have to commit to a particular strategy for selecting the element.

Greetings,
Stefan