Re: [isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations
Hi Lars, I have now patches queued to enabled all of the commented out theorems and pred_set_conv declarations, except for the generalited versions of SUP_UN_eq and INF_INT_eq. Using generalized versions of SUP_UN_eq changes the theorems generated by inductive set in a negative way: inductive_set TFin :: 'a set set \Rightarrow 'a set set set for S :: 'a set set where succI: x : TFin S \Longrightarrow succ S x : TFin S | Pow_UnionI: Y : Pow(TFin S) \Longrightarrow Union(Y) : TFin S generates for example the theorem: TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ (⋃i ∈ ?Y. i) ∈ TFin ?S instead of: TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ ⋃?Y ∈ TFin ?S I would suggest to push the changes as they are now since they are a step into the right direction; I have to look at the remaining problem separately. Thanks a lot, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ 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
I have now patches queued to enabled all of the commented out theorems and pred_set_conv declarations, except for the generalited versions of SUP_UN_eq and INF_INT_eq. Using generalized versions of SUP_UN_eq changes the theorems generated by inductive set in a negative way: inductive_set TFin :: 'a set set \Rightarrow 'a set set set for S :: 'a set set where succI: x : TFin S \Longrightarrow succ S x : TFin S | Pow_UnionI: Y : Pow(TFin S) \Longrightarrow Union(Y) : TFin S generates for example the theorem: TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ (⋃i ∈ ?Y. i) ∈ TFin ?S instead of: TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ ⋃?Y ∈ TFin ?S When I adapted Relation.thy, it appeared to me suspicious that SUP_UN_eq and INF_INT_eq where not as general as they would naturally be; maybe the problem you experience now has been experienced already by Stefan when he introduced this. Stefan, does this sound somehow familiar to you? Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ 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
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
[isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations
Hi all, recently I did some work to setup Stefan's ancient pred_set_conv utility for relation predicates like sym(p) etc., see http://isabelle.in.tum.de/reports/Isabelle/file/tip/src/HOL/Relation.thy A few couple of things then came to surface: * Naming: »inductive_set foo« yields »foop« as the name of the corresponding predicate, whereas e.g. »wf« has »wfP«. We should consolidate this. I personally have a slight preference for lower case »p«. * Abbreviation vs. constant: considering that both kinds of relations coexist, constants would be better for all twins. The pred_set_conv utility can convert theorems on the fly if needed. * 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. Maybe one day prep_set_conv can be subsumed by a generic lifting machinery a la quotient, Cheers, 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
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, this looks like a bug. The culprit seems to be function mk_to_pred_inst in inductive_set.ML, which does not handle variables of type ... = T set properly. A similar problem might also occur with to_set. I'll try to fix this before the next release. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
