[isabelle-dev] HOL/ex/Set_Algebras

[Clemens Ballarin]

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 <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?
>
> Alex
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>