[isabelle-dev] problems with the class-package

[Amine Chaieb]

Dear all,


Jeremy (and I) are encountering some (to us) strange problems with the
class-package (it might also be the locale-part, so your expertise is
highly welcome here). I am using Isabelle version 20 minutes ago.


Attached is a small theory illustrating the problem. Originally, line 32
looked like:

  embed_nat_even: "!!x. even (embed_nat x) = even x" and


but now Isabelle complains about types (apparently inside even_odd we
are not allowed to use even with a different type, even if we have
already provided an instance).


Anyway, when we introduce a silly definition or abbreviation even_nat
which is even over nat, we get the following strange error that some
tactic in class-package failed. Any idea what this is? In the best case
of course someone could tell how to fix it, so we can at least process
the theory...

Here is the error:


*** Tactic failed.
*** The error(s) above occurred for the goal statement:
*** (!!x::nat. image_nat (embed_nat_class.embed_nat x))
*** ==> (!!x::'a::type.
***         image_nat x ==> embed_nat_class.embed_nat (return_nat x) = x)
***     ==> (!!(x::nat) y::nat.
***             (embed_nat_class.embed_nat x = embed_nat_class.embed_nat
y) =
***             (x = y))
***         ==> (!!(x::nat) y::nat.
***                 (embed_nat_class.embed_nat x
***                  < embed_nat_class.embed_nat y) =
***                 (x < y))
***             ==> (!!(x::nat) y::nat.
***                     (embed_nat_class.embed_nat x
***                      <= embed_nat_class.embed_nat y) =
***                     (x <= y))
***                 ==> (!!(x::nat) y::nat.
***                         (embed_nat_class.embed_nat x dvd
***                          embed_nat_class.embed_nat y) =
***                         (x dvd y))
***                     ==> (!!x::nat.
***                             even (embed_nat_class.embed_nat x) =
even_nat x)
***                         ==> (0::'a::type) = embed_nat_class.embed_nat 0
***                             ==> (1::'a::type) =
embed_nat_class.embed_nat 1
***                                 ==> (2::'a::type) =
***                                     embed_nat_class.embed_nat 2
***                                     ==> (3::'a::type) =
***   embed_nat_class.embed_nat 3
***   ==> (!!(x::nat) y::nat.
***           embed_nat_class.embed_nat x + embed_nat_class.embed_nat y =
***           embed_nat_class.embed_nat (x + y))
***       ==> (!!(x::nat) y::nat.
***               y <= x
***               ==> embed_nat_class.embed_nat x -
***                   embed_nat_class.embed_nat y =
***                   embed_nat_class.embed_nat (x - y))
***           ==> (!!(x::nat) y::nat.
***                   embed_nat_class.embed_nat x *
***                   embed_nat_class.embed_nat y =
***                   embed_nat_class.embed_nat (x * y))
***               ==> (!!(x::nat) n::nat.
***                       embed_nat_class.embed_nat x ^ n =
***                       embed_nat_class.embed_nat (x ^ n))
***                   ==> (!!(x::nat) y::nat.
***                           embed_nat_class.embed_nat x div
***                           embed_nat_class.embed_nat y =
***                           embed_nat_class.embed_nat (x div y))
***                       ==> (!!(x::nat) y::nat.
***                               embed_nat_class.embed_nat x mod
***                               embed_nat_class.embed_nat y =
***                               embed_nat_class.embed_nat (x mod y))
***                           ==> ??.Strange.embed_nat op * op div op
mod op -
***                                (1::'a::type) op <= op < op +
(0::'a::type)
***                                number_of even op ^
embed_nat_class.embed_nat
***                                return_nat image_nat
*** At command "class".


Best wishes,

Amine.



-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Strange.thy
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090123/11939013/attachment-0001.ksh>