[isabelle-dev] Relation_Power.thy

[Florian Haftmann]

The overloaded infix syntax ^ for different power operations (natural
power in monoids, function power, relation power) turns more and more
unsatisfactory for a couple of reasons, e.g.:

* The abuse of the type class mechanism to achieve the ^ syntax for
funpow and relpow hinders the enforcement of the strict class parameter
instantiation policy and produces legacy feature warnings.
* The nature of ^ as a class operations implies the existence of class
recpower which leads to strange duplications in the class hierarchy in
the HOL-Complex theories.
* Anyway, the ^ does only cover particular cases, not e.g. real ^
rat etc.

A short investigation yields that actually funpow and relpow are rarely
used, relpow even not in the HOL-Complex theories but rather in
particular application examples (typically things  like Jinja etc.).

There have been some thoughts to provide a mechanism of overloaded
abbreviations or something similar to eliminate that problem, but
meanwhile, considering the rare usages of funpow and relpow, I would
suggest the conservative solution:

* funpow is defined as a separate primrec in theory Nat, without special
syntax.
* The remainder of theory Relation_Power is moved to Library, with a new
infix syntax (e.g. ^^) for relpow.
* The simple pow ^ then is just a primrec in class comm_monoid_mult.
* classes power and recpower disappear, also the corresponding duplications.

Opinions?

Florian
-- next part --
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080902/d526bc4b/attachment.vcf
-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080902/d526bc4b/attachment.pgp

[isabelle-dev] Relation_Power.thy

[Makarius]

On Tue, 2 Sep 2008, David Aspinall wrote:

   \caret:funpow
 
   \caret:relpow
 
 This is already supported in the X-Symbol replacement in the CVS version of
 Proof General, by the way, although Isabelle's lexer currently only allows
 syntax like \caret1 and \caret2.

The \symbol notation is more fundamental, below lexing even.  It is 
actually fashioned after Java's \u for UTF-16 chars, but we do not 
depend on unicode encoding variants of course.

You can achieve the above name space effect of symbols already via 
something like \caret_funpow, which is presently unused because LaTeX 
output is a bit strange (as for \caret1).  This means \foo_bar and 
\foo42 are both unlikely to be used already for something else.

There is also a more compositional way to produce symbol variants: 
\^control\symbol.  Here nothing needs to be changed in Isabelle, only 
the UI needs to provide sane input methods and proper display (without the 
flashing of x-symbol for \^sub for example).


Makarius

[isabelle-dev] Relation_Power.thy

[David Aspinall]

 You can achieve the above name space effect of symbols already via 
 something like \caret_funpow,

Aha -- we can easily do this in PG then instead of \caret1.

 which is presently unused because LaTeX 
 output is a bit strange (as for \caret1). 

The idea is to make the output the same as \caret, of course (with the 
disadvantage that you can't wave your mouse over a piece of paper).

  - D.

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.