ballarin at in.tum.de
Fri Apr 13 20:47:02 CEST 2012
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
Quoting Alexander Krauss <krauss at 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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev