Hi Christian,
> 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}"there is a couple of issues you are hitting at here. A. The (re-)introduction of the set type constructor See http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01736.html for one possible entry into the motivation and discussion concerning that. B. The default code generation for setup You can always turn back to sets-as-predicates by code_datatype Collect and then proving appropriate theorems for the set operation etc. – this would fir best into a library theory which could then be part of the distribution. But I guess your issue is mainly with… C. Relations Both kinds of relations 'a => 'a => bool and ('a * 'a) set are present in their own right, but with disjoint developments in the HOL theoris. Note that you can convert between both using pred/set conversions, the same infrastructure as inductive_set is using. So, if you want predicate relations, it seems to be best to convert your stuff to them, filling existing gaps in the HOL theories by additional definitions and suitable pred/set conversion declarations. See theory "Relation" for examples for making use of pred/set conversions by means of attributes "to_set" and "to_pred"; and declarations of pred/set conversions by means of attribute "pred_set_conv". Unfortunately, there is no reference for them in the Isabelle Reference Manual. Maybe one day this is subsumed by an emerging generic »lifting« infrastructure. Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
