Email Gateway (Aug 18 2022 at 10:21): Email Gateway (Aug 18 2022 at 10:21):From: kostas pouliasis <kpoul@softlab.ntua.gr>
Hi all,
I am trying to define the identity between relations in "The Theory
of Abstract Objects" ( http://mally.stanford.edu/)
The beginning of my theory (actually, only what is relevant to my
question below) is in the attachment.
The last definition produces this error:
Malformed dependency of constant Eq(obj ^ obj ^ 'a) -> Eq(obj ^ 'a)
*** (restriction Eq(obj ^ obj ^ 'a) from "PM.EqX_frmN_def")
*** The error(s) above occurred in definition "EqX_frmN_def":
*** "F = G : ALL x. (ly. F y x) = (ly. G y x)"
*** At command "defs".
From this, I conclude that Isabelle does not understand that my
definition is well defined, i.e. that the type "obj => obj => 'a"
is "smaller", in some sense, than "obj => 'a".
The error goes away if I force the polymorphic type 'a to be a
specific type (e.g. bool).
Any ideas on how I can solve this? I'm not interested in infinite
types, but Isabelle seems to be worried about them.
Thanks,
principia.thy
Email Gateway (Aug 18 2022 at 10:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Isabelle's check for non-circularity of overloaded definitions restricts
checked overloaded definitions to overloading patterns similiar to what
is possible in Haskell 1.0; if this is not enough and you trust your
definitions not to introduce inconsistencies (by a suitable meta-proof),
you may turn the check of by writing
defs (unchecked)
instead of
defs (overloaded)
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 10:22):From: Steven Obua <obua@in.tum.de>
As Florian states in the above, when using defs(unchecked), you are on
your own; especially, your definitions are just axioms then, which you
have to trust, and which might introduce inconsistencies.
In order to circumvent this problem, you can use together with
defs(unchecked) my package for checking overloaded definitions. It is
more powerful than the built-in test of Isabelle and might be able to
prove the consistency of your definitions (and it also tells you when
your definitions are definitely circular and such). You can find it at
http://www4.in.tum.de/~obua/checkdefs. Don't hesitate to ask me if you
have more questions,
Steven
Email Gateway (Aug 18 2022 at 10:22):From: Steven Obua <obua@in.tum.de>
There is now a new version of the mentioned package available that works
together with the latest Isabelle repository version. It proves that
your definitions in theory PM are OK.
Steven
Last updated: May 03 2024 at 04:19 UTC