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