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 <[email protected]>:
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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
