Re: [isabelle-dev] Towards the next release
We have a somewhat useful tool for expanding word equalities/inequalities bitwise, based on a part of some work Sascha and I did back in 2010. I've been meaning to push it up to the distribution for years, this will probably be a good time. The main reason I'm telling you this is that I'm now more likely to actually do it. Yours, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ 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
Re: [isabelle-dev] [isabelle] Status of HOL/Import
On Sun, 4 Mar 2012, Cezary Kaliszyk wrote: Makarius once suggested an antiquotation, that does something like 'print_theorems'. I have not investigated how to implement one? Pretty printing into latex source is not a big deal, if you are satisfied with regular multiline output in the "display" style of the document preparation system. If you are more ambitious, say you want some tabular stuff in Latex, then some experts on LatexSugar and Christian Urban can help. Alternatively, the pretty printing can be done in plain HTML. Yet more alternatively, you can just make an interactive print command, say like 'print_theory'. In Isabelle/jEdit the target will be HTML anyway. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
> but I would > suggest waiting a week or two for the new import and trying to get > the maps correct there. Ack. 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] [isabelle] Status of HOL/Import
Hi Florian, On Sun, Mar 04, 2012 at 10:15:38AM +0100, Florian Haftmann wrote: > I've been working on the Importer stuff, not very deeply, but separating > HOL4 and HOL Light contents, stripping generic parts of any name > reference to HOL4, etc. [...] Great! > There could be done a lot more on the ML stuff to introduce basic coding > practice there, of course, but for the moment I will leave that aside. As I mentioned to you privately, we (w Alex) are trying to write a new better import. So before working on the old one too much, lets first see which parts are reused and which will not. > Two questions: > a) There is a README; maybe you would like to update it according to > your current expertise? > b) After the pred/set issue, the generated HOL Light theories must be > regenerated. Do you have time to accomplish this? Alternatively, I > could follow the README instructions as soon as available. There are two issues; first: This is not as straightforward as it seems; apparently some of the constant maps have types that are not valid anymore (for example INSERT), so it is not going to work immediately. One can update it with most of the constant maps removed immediately; but I would suggest waiting a week or two for the new import and trying to get the maps correct there. But more importantly, the concept of generating these files and then replaying them with 'sorrys' is very strange in an LCF approach. Having built the session once, one can checkpoint the image and this is much nicer than the generated sources. The only thing this needs instead is some way to generate documentation. Makarius once suggested an antiquotation, that does something like 'print_theorems'. I have not investigated how to implement one? Cheers, Cezary ___ 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] [isabelle] Status of HOL/Import
Hi Cezary, I've been working on the Importer stuff, not very deeply, but separating HOL4 and HOL Light contents, stripping generic parts of any name reference to HOL4, etc. The visible change is that most parts can now be directly edited using jEdit, which is the base for any further refinement. I do not claim that the naming terminology I have invented is the best (it surely isn't), but now it should not be difficult to improve it, in case. There could be done a lot more on the ML stuff to introduce basic coding practice there, of course, but for the moment I will leave that aside. Two questions: a) There is a README; maybe you would like to update it according to your current expertise? b) After the pred/set issue, the generated HOL Light theories must be regenerated. Do you have time to accomplish this? Alternatively, I could follow the README instructions as soon as available. And, n.b.: HOL4_PROOFS is now named IMPORTER_PROOFS. > However there is still the question of what to do with the HOL4 > import; as the old exporter > seems to be lost and I don't think people are interested in writing a new > one... Well, keep it »as it is« at the moment… ;-) 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
