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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev