Re: [isabelle-dev] HOL/ex/Set_Algebras
Hi Clemens, >> the story behind is not about syntax. It is really about the >> simultaneous definitions. For a motivation, you can have a look at the >> tutorial on code generation, section »Further issues«, »Locales and >> interpretation«, where the pattern behind interpretation plus definition >> is spelt out using the constant »funpows«. > > This looks to me like a special case, but maybe one that is encountered > frequently when generating code. What do you intend to do? Provide a > special version of interpretation for code generation? the intension is: def (in foo) bar where … --[ interpretation foo: … ]--> def (in -) bar where … rather than def (in foo) bar where … --[ interpretation foo: … ]--> abbreviation (in -) bar where … with --[ … ]--> being the interpretation morphism. The interpretation + defines pattern was something which could be accomplished rather simple, so I decided to make an experimental start with this in December 2010. 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] HOL/ex/Set_Algebras
Hi Florian, Thanks for the clarification. Its purpose might have been to make the interpretation notationally simpler. the story behind is not about syntax. It is really about the simultaneous definitions. For a motivation, you can have a look at the tutorial on code generation, section »Further issues«, »Locales and interpretation«, where the pattern behind interpretation plus definition is spelt out using the constant »funpows«. This looks to me like a special case, but maybe one that is encountered frequently when generating code. What do you intend to do? Provide a special version of interpretation for code generation? Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/ex/Set_Algebras
Hi Clemens, > If you follow up the imported theory, you will find some code that > provides a clone of the interpretation command (under the same name!) > with some added functionality (definitions). > Its purpose > might have been to make the interpretation notationally simpler. the story behind is not about syntax. It is really about the simultaneous definitions. For a motivation, you can have a look at the tutorial on code generation, section »Further issues«, »Locales and interpretation«, where the pattern behind interpretation plus definition is spelt out using the constant »funpows«. I have this clone on my todo list, actually the leading point on my after-release todo list, and hope to be able to get rid of it, but I have to study mixins before in depth. 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] HOL/ex/Set_Algebras
Hi Alex, > while backporting HOL/Library/Set_Algebras to use type classes again (a > remaining point of the 'a set transition), thanks for doing this! > I noticed that there is now a > clone of that file in HOL/ex. > What should we do with the clone? Are there maybe other examples that > can demonstrate interpretations with simultaneous definitions, so that > we can simply remove it? Now, there are (IMP). So it is ok that this has gone. It still served the purpose to remind me of a few things, but these are on my list anyway. 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] HOL/ex/Set_Algebras
I wondered when somebody would ask this. What's going on here is a hack, and I'm not very happy about it. If you follow up the imported theory, you will find some code that provides a clone of the interpretation command (under the same name!) with some added functionality (definitions). This clone is used in some theories about operational semantics throughout HOL. I have not fully understood what the clone does, but the code is outdated, and I believe it can be gotten rid of easily. I don't see any added value in a command that makes both definitions and an interpretation. Its purpose might have been to make the interpretation notationally simpler. But that's no longer required, since 'where' clauses in interpretation now anticipate the syntax of the interpreted context, which makes writing left hand sides of the equations in the 'where' clauses easier. (I hope what I write makes sense to anybody at all.) For example, one may write interpretation power: lattice "Pow X" "op \" where "power.meet = (\A \ Pow X. \B \ Pow X. A \ B)" and "power.dual.meet = (\A \ Pow X. \B \ Pow X. A \ B)" where the locale 'lattice' has the (pseudo-)constants 'meet' and 'dual.meet'. If you look at a similar example in src/HOL/ex/LocaleTest2.thy (interpretation in line 490) you will see that this used to be a lot clumsier, involving the foundational constants. Clemens Quoting Alexander Krauss : Hi all, while backporting HOL/Library/Set_Algebras to use type classes again (a remaining point of the 'a set transition), I noticed that there is now a clone of that file in HOL/ex. The changelog says: changeset: 41581:c34415351b6d user:haftmann date:Sat Jan 15 20:05:29 2011 +0100 summary: experimental variant of interpretation with simultaneous definitions, plus example Unfortunately, nothing in the file itself states what it should demonstrate. Instead, the original comments remain, so there is plenty of opportunity for getting totally confused. What should we do with the clone? Are there maybe other examples that can demonstrate interpretations with simultaneous definitions, so that we can simply remove it? Alex ___ 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
[isabelle-dev] HOL/ex/Set_Algebras
Hi all, while backporting HOL/Library/Set_Algebras to use type classes again (a remaining point of the 'a set transition), I noticed that there is now a clone of that file in HOL/ex. The changelog says: changeset: 41581:c34415351b6d user:haftmann date:Sat Jan 15 20:05:29 2011 +0100 summary: experimental variant of interpretation with simultaneous definitions, plus example Unfortunately, nothing in the file itself states what it should demonstrate. Instead, the original comments remain, so there is plenty of opportunity for getting totally confused. What should we do with the clone? Are there maybe other examples that can demonstrate interpretations with simultaneous definitions, so that we can simply remove it? Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
