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 \<subseteq>"
where "power.meet = (\<lambda>A \<in> Pow X. \<lambda>B \<in> Pow
X. A \<inter> B)"
and "power.dual.meet = (\<lambda>A \<in> Pow X. \<lambda>B
\<in> Pow X. A \<union> 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 <kra...@in.tum.de>:
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
