[isabelle] malformed dependency



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,
header {* Principia Metaphysica *}

theory PM
imports CPure

begin

classes type
classes trm < type
classes frm < type
defaultsort frm

global

typedecl bool
typedecl obj

arities
 bool  :: frm
 obj   :: trm
 "fun" :: (trm, frm) frm

judgment
 Trueprop :: "bool => prop"                             ("(_)" 5)

consts
 Equ   :: "[bool, bool] => bool"                        (infixr "<->" 25)
 All   :: "(('a :: type) => bool) => bool"              (binder "ALL " 10)
 Box   :: "bool => bool"                                ("[]_" [50] 50)
 Enc   :: "[obj, obj => bool] => bool"                  ("_$_" [99,99] 50)
 EqE  :: "[obj, obj] => bool"                           (infix " =E " 50)
 Eq   :: "[('a :: type), 'a] => bool"                   (infix "=" 50)

local

defs (overloaded)
 Eq_frm0_def:  "(p :: bool) = q  ==  (%y :: obj. p) = (%y. q)"
 Eq_frm1_def:  "F = G  ==  [] (ALL x. x$F <-> x$G)"
(* this last definition is the source of the error *)
 EqX_frmN_def: "(F :: obj => obj => ('a :: frm)) = G  ==
                  ALL x. (%y. F y x) = (%y. G y x)"

end







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.