Re: [isabelle-dev] NEWS
Johannes, On Mon, 2013-04-22 at 16:39 +0200, Johannes Hölzl wrote: * Introduce type class conditional_complete_lattice: Like a complete lattice but does not assume the existence of the top and bottom elements. The name conditional complete lattice suggests a special kind of complete lattice. However, without top and bottom elements, this structure is not a complete lattice at all. In the literature, it is therefore more aptly called conditionally complete lattice. I propose to retain the -ly suffix in the name of the type class. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package
Hi Brian thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense that internal constants (like case_guard) are not visible anymore. However, your example is still not printed as expected (assuming that the output should be equal to the input in this case): (case x of (a, b) ⇒ λ(c, d). e) y I think, the proper resolution to this is to have an uncheck phase for turning prod_case e intro λ(x, y). e x y before the case translation uncheck phase. Maybe Makarius or Stefan could comment on this. Then, I could have a look. Dmitriy On 24.04.2013 02:10, Brian Huffman wrote: I discovered a problem with the pretty-printing of some terms (I am using revision 4392eb046a97). term (λ(a, b) (c, d). e) x y case_guard True x (case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e case_nil) y :: 'e I assume this is a result of the recent changes to the handling of case expressions? - Brian On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote: * Nested case expressions are now translated in a separate check phase rather than during parsing. The data for case combinators is separated from the datatype package. The declaration attribute case_tr can be used to register new case combinators: declare [[case_translation case_combinator constructor1 ... constructorN]] This refers to Isabelle/bdaa1582dc8b Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel tray...@in.tum.de wrote: Hi Brian thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense that internal constants (like case_guard) are not visible anymore. Thanks for taking care of this so quickly! However, your example is still not printed as expected (assuming that the output should be equal to the input in this case): (case x of (a, b) = λ(c, d). e) y Usually prod_case is printed as a tuple-lambda when partially applied, and as a case expression when fully applied. So considering that the underlying term in my example is prod_case (λa b. prod_case (λc d. e)) x y, the above output makes perfect sense. I think, the proper resolution to this is to have an uncheck phase for turning prod_case e intro λ(x, y). e x y before the case translation uncheck phase. Maybe Makarius or Stefan could comment on this. Then, I could have a look. Dmitriy Although previous Isabelle versions had output equal to the input in this case, it seems a bit strange for (λ(a, b) (c, d). e) to be printed as a lambda if applied to 0 or 2 arguments, and as a case if applied to 1. I'm not sure it's worth complicating the pretty printer just to get this behavior back. - Brian On 24.04.2013 02:10, Brian Huffman wrote: I discovered a problem with the pretty-printing of some terms (I am using revision 4392eb046a97). term (λ(a, b) (c, d). e) x y case_guard True x (case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e case_nil) y :: 'e I assume this is a result of the recent changes to the handling of case expressions? - Brian On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote: * Nested case expressions are now translated in a separate check phase rather than during parsing. The data for case combinators is separated from the datatype package. The declaration attribute case_tr can be used to register new case combinators: declare [[case_translation case_combinator constructor1 ... constructorN]] This refers to Isabelle/bdaa1582dc8b Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
But for the moment I will leave this aside anyway. Still one thing to add: http://isabelle.in.tum.de/repos/isabelle/rev/cb154917a496 avoids the odd reinit entirely, the critical lines being fun add_dependency locale dep_morph mixin export = (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export # activate_local_theory dep_morph mixin export which add both an dependency *and* provide the facts in the context of the current local theory. Also, interpretation confined within blocks essentially boils down to the singleton line val activate_local_theory = Local_Theory.target ooo activate_proof; This is a great triumph of the »local everything« approach. 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] Interpretation in arbitrary targets.
Hi, Am Mittwoch, den 24.04.2013, 19:16 +0200 schrieb Florian Haftmann: This is a great triumph of the »local everything« approach. I’m not sure that I understand all that is going on, but I have the feeling that the theory that I’m working on will greatly benefit from your development, and I’m looking forward to Isabelle 2013-2 (or 2014). So thanks in advance from my side! Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
