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
