[isabelle-dev] Strange interaction of locales and constant definitions

[Clemens Ballarin]

This is a fairly complex interaction of structure declarations, the  
overloaded constant "pow" aka (^) and parsing of a locale expression.   
It would be interesting to see whether this problem is already present  
in early 2009 or was introduced later.  HOL-Algebra has not changed  
much since 2009.

Clemens


Quoting Lars Noschinski <noschinl at in.tum.de>:

> Hi everyone,
>
> I am encountering a very strange interaction of the definition of  
> specific constants with locale declarations in HOL-Algebra (as of  
> 06db08182c4b; but the behaviour also seems to exist in 2013).
>
> To reproduce this behaviour, insert the following code in  
> "~~/src/HOL/Algebra/Module.thy", before the definition of the  
> "module" locale:
>
> -----------------------------------------------------------
> context group begin
> definition f :: "'a ?'a" where
>    "f ? (?x. x (^) (0::int))"
> end
> -----------------------------------------------------------
>
> (interestingly, the right hand side of the constant matters; e.g.  
> simply  using "undefined" or "%x. x" will not produce an error).
>
> When doing so, the locale declaration will throw an error:
>
> -----------------------------------------------------------
> Type unification failed
>
> Type error in application: incompatible operand type
>
> Operator:  smult :: (??'a, 'c, ??'b) module_scheme ? ??'a ? 'c ? 'c
> Operand:   M :: ('c, 'd) ring_scheme
> -----------------------------------------------------------
>
> It is probably relevant that both locales on which "module" depends  
> depend recursively on "group".
>
> I can recover from this error by
>   - removing the stray "(structure)" declaration from M (the implicit
>     argument R of cring is already a structure),
>   - giving M an explicit type and
>   - making R an explicit argument with an explicit type.
>
> (The type annotations are those which are inferred automatically if  
> I don't define the constant f)
>
> I.e., if I replace the head of the locale declaration by
>
> -----------------------------------------------------------
> locale module = R: cring R + M: abelian_group M
>     for M :: "('a, 'd, 'c) module_scheme"
>     and R :: "('a, 'b) ring_scheme" (structure) +
> -----------------------------------------------------------
>
> the locale can be defined.
>
> Has anybody an idea what is going on there?
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>