Re: [isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations
Florian Haftmann wrote: * This is mainly a question to Stefan: there are some theorems commented out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes. I guess this is due to a higher-order situation, but I would be reassuring if you can confirm that. Hi Florian, I have fixed this bug now, see changeset b1d15637381a. Note that converting the above theorem (and the other theorems in Relation.thy marked with FIXME) to predicate notation requires the generalized versions of theorems INF_INT_eq2 and SUP_UN_eq2, which should replace the more specific versions. Unfortunately, the Relation theory is currently a bit of a mess. Larger blocks of conversion lemmas are commented out for no good reason, which means that they are not tested by our nightly builds, and for some of them it still remains to be examined whether they can be added to the database of predicate/set conversion rules by default without breaking any of the examples in the AFP. What is the strategy for cleaning up this theory? Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations
Hi Stefan, I have fixed this bug now, see changeset b1d15637381a. Note that converting the above theorem (and the other theorems in Relation.thy marked with FIXME) to predicate notation requires the generalized versions of theorems INF_INT_eq2 and SUP_UN_eq2, which should replace the more specific versions. Unfortunately, the Relation theory is currently a bit of a mess. Larger blocks of conversion lemmas are commented out for no good reason well, the history is that I have not yet commented *in* them yet, just marked them (among a couple of declarations) as CANDIDATE. So, anybody who wants to go ahead can just comment in them and run the regular regression (for which I do not expected any difficulties). 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
