Email Gateway (Aug 18 2022 at 13:06): Email Gateway (Aug 18 2022 at 13:06):From: Christoph Feller <c_feller@informatik.uni-kl.de>
Hallo,
I have with a hidden extra type variable again and again I have no
clue what exactly went wrong. I've made a small example:
class testC = type +
fixes from_nat :: "nat => 'a"
and to_nat :: "'a => nat"
locale Test =
fixes dummy :: "'a::testC"
assumes dd: "ALL z::'a::testC. to_nat z ~= 0"
begin
definition ftest :: "nat => 'a list" where "ftest n == [from_nat n]"
inductive test::"nat => nat => bool"
where
"((ftest a)::'a list) = ((ftest b)::'a list) ==> test a b"
...
I thought the locale not only fixed dummy but also 'a so that it isn't
necessarily an extra type variable in the inductive definition. Am I
wrong or is there another mistake in my example?
Thanks in advance,
Christoph
Email Gateway (Aug 18 2022 at 13:06):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Christoph Feller <c_feller@informatik.uni-kl.de>:
Hi Christoph,
I think you are right to expect this to work.
When you define a locale like "Test", the locale package defines a
predicate of the same name, which encodes all of the locale
assumptions. Usually the predicate takes all of the parameters from
"fixes" declarations as arguments. However, locales like your "Test"
example require some special treatment. For example:
thm Test_def
Test TYPE(?'a::testC) == ALL z::?'a::testC. to_nat z ~= 0
As you can see, the locale predicate "Test" does not depend on the
locale parameter "dummy", but it still depends on the type variable 'a.
I would have expected the locale package to use the same trick to
encode functions like your "test". That is, an extra hidden
TYPE(?'a::testC) parameter should be added to make the type checker
happy. I would consider this to be a bug in the locale implementation.
By the way, the following definition does work inside the locale.
Just like your inductive definition of "test", it uses type variable
'a on the right-hand side, but no type variable appears in the type of
the constant. The only difference is that this one also uses the
locale constant "dummy" on the right-hand side.
definition
test2 :: "nat => bool"
where
"test2 n = (((ftest n) :: 'a list) = [dummy])"
Email Gateway (Aug 18 2022 at 13:07):From: Christoph Feller <c_feller@informatik.uni-kl.de>
Hallo Brian,
Thanks for your answer. So I shouldn't count on there being a solution
to this problem apart from adding dummy variables into my definitions?
Well, it's not a big problem, it will probably just make some
definitions a bit less elegant.
Christoph
Last updated: May 03 2024 at 08:18 UTC