src/ZF/ZF.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/ZF.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/ZF.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -16,68 +16,68 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  "0"         :: "i"                  ("0")   (*the empty set*)
     1.8 -  Pow         :: "i => i"                     (*power sets*)
     1.9 -  Inf         :: "i"                          (*infinite set*)
    1.10 +  "0"         :: i                  ("0")   (*the empty set*)
    1.11 +  Pow         :: i => i                     (*power sets*)
    1.12 +  Inf         :: i                          (*infinite set*)
    1.13  
    1.14    (* Bounded Quantifiers *)
    1.15  
    1.16 -  Ball, Bex   :: "[i, i => o] => o"
    1.17 +  Ball, Bex   :: [i, i => o] => o
    1.18  
    1.19    (* General Union and Intersection *)
    1.20  
    1.21 -  Union,Inter :: "i => i"
    1.22 +  Union,Inter :: i => i
    1.23  
    1.24    (* Variations on Replacement *)
    1.25  
    1.26 -  PrimReplace :: "[i, [i, i] => o] => i"
    1.27 -  Replace     :: "[i, [i, i] => o] => i"
    1.28 -  RepFun      :: "[i, i => i] => i"
    1.29 -  Collect     :: "[i, i => o] => i"
    1.30 +  PrimReplace :: [i, [i, i] => o] => i
    1.31 +  Replace     :: [i, [i, i] => o] => i
    1.32 +  RepFun      :: [i, i => i] => i
    1.33 +  Collect     :: [i, i => o] => i
    1.34  
    1.35    (* Descriptions *)
    1.36  
    1.37 -  The         :: "(i => o) => i"      (binder "THE " 10)
    1.38 -  if          :: "[o, i, i] => i"
    1.39 +  The         :: (i => o) => i      (binder "THE " 10)
    1.40 +  if          :: [o, i, i] => i
    1.41  
    1.42    (* Finite Sets *)
    1.43  
    1.44 -  Upair, cons :: "[i, i] => i"
    1.45 -  succ        :: "i => i"
    1.46 +  Upair, cons :: [i, i] => i
    1.47 +  succ        :: i => i
    1.48  
    1.49    (* Ordered Pairing *)
    1.50  
    1.51 -  Pair        :: "[i, i] => i"
    1.52 -  fst, snd    :: "i => i"
    1.53 -  split       :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
    1.54 +  Pair        :: [i, i] => i
    1.55 +  fst, snd    :: i => i
    1.56 +  split       :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
    1.57  
    1.58    (* Sigma and Pi Operators *)
    1.59  
    1.60 -  Sigma, Pi   :: "[i, i => i] => i"
    1.61 +  Sigma, Pi   :: [i, i => i] => i
    1.62  
    1.63    (* Relations and Functions *)
    1.64  
    1.65 -  domain      :: "i => i"
    1.66 -  range       :: "i => i"
    1.67 -  field       :: "i => i"
    1.68 -  converse    :: "i => i"
    1.69 -  function    :: "i => o"	    	(*is a relation a function?*)
    1.70 -  Lambda      :: "[i, i => i] => i"
    1.71 -  restrict    :: "[i, i] => i"
    1.72 +  domain      :: i => i
    1.73 +  range       :: i => i
    1.74 +  field       :: i => i
    1.75 +  converse    :: i => i
    1.76 +  function    :: i => o	    	(*is a relation a function?*)
    1.77 +  Lambda      :: [i, i => i] => i
    1.78 +  restrict    :: [i, i] => i
    1.79  
    1.80    (* Infixes in order of decreasing precedence *)
    1.81  
    1.82 -  "``"        :: "[i, i] => i"    (infixl 90) (*image*)
    1.83 -  "-``"       :: "[i, i] => i"    (infixl 90) (*inverse image*)
    1.84 -  "`"         :: "[i, i] => i"    (infixl 90) (*function application*)
    1.85 -(*"*"         :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
    1.86 -  "Int"       :: "[i, i] => i"    (infixl 70) (*binary intersection*)
    1.87 -  "Un"        :: "[i, i] => i"    (infixl 65) (*binary union*)
    1.88 -  "-"         :: "[i, i] => i"    (infixl 65) (*set difference*)
    1.89 -(*"->"        :: "[i, i] => i"    (infixr 60) (*function space*)*)
    1.90 -  "<="        :: "[i, i] => o"    (infixl 50) (*subset relation*)
    1.91 -  ":"         :: "[i, i] => o"    (infixl 50) (*membership relation*)
    1.92 -(*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
    1.93 +  "``"        :: [i, i] => i    (infixl 90) (*image*)
    1.94 +  "-``"       :: [i, i] => i    (infixl 90) (*inverse image*)
    1.95 +  "`"         :: [i, i] => i    (infixl 90) (*function application*)
    1.96 +(*"*"         :: [i, i] => i    (infixr 80) (*Cartesian product*)*)
    1.97 +  "Int"       :: [i, i] => i    (infixl 70) (*binary intersection*)
    1.98 +  "Un"        :: [i, i] => i    (infixl 65) (*binary union*)
    1.99 +  "-"         :: [i, i] => i    (infixl 65) (*set difference*)
   1.100 +(*"->"        :: [i, i] => i    (infixr 60) (*function space*)*)
   1.101 +  "<="        :: [i, i] => o    (infixl 50) (*subset relation*)
   1.102 +  ":"         :: [i, i] => o    (infixl 50) (*membership relation*)
   1.103 +(*"~:"        :: [i, i] => o    (infixl 50) (*negated membership relation*)*)
   1.104  
   1.105  
   1.106  types
   1.107 @@ -85,29 +85,29 @@
   1.108    pttrns
   1.109  
   1.110  syntax
   1.111 -  ""          :: "i => is"                   ("_")
   1.112 -  "@Enum"     :: "[i, is] => is"             ("_,/ _")
   1.113 -  "~:"        :: "[i, i] => o"               (infixl 50)
   1.114 -  "@Finset"   :: "is => i"                   ("{(_)}")
   1.115 -  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
   1.116 -  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
   1.117 -  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
   1.118 -  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
   1.119 -  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
   1.120 -  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
   1.121 -  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
   1.122 -  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
   1.123 -  "->"        :: "[i, i] => i"               (infixr 60)
   1.124 -  "*"         :: "[i, i] => i"               (infixr 80)
   1.125 -  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
   1.126 -  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
   1.127 -  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
   1.128 +  ""          :: i => is                   ("_")
   1.129 +  "@Enum"     :: [i, is] => is             ("_,/ _")
   1.130 +  "~:"        :: [i, i] => o               (infixl 50)
   1.131 +  "@Finset"   :: is => i                   ("{(_)}")
   1.132 +  "@Tuple"    :: [i, is] => i              ("<(_,/ _)>")
   1.133 +  "@Collect"  :: [pttrn, i, o] => i        ("(1{_: _ ./ _})")
   1.134 +  "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _: _, _})")
   1.135 +  "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _: _})" [51,0,51])
   1.136 +  "@INTER"    :: [pttrn, i, i] => i        ("(3INT _:_./ _)" 10)
   1.137 +  "@UNION"    :: [pttrn, i, i] => i        ("(3UN _:_./ _)" 10)
   1.138 +  "@PROD"     :: [pttrn, i, i] => i        ("(3PROD _:_./ _)" 10)
   1.139 +  "@SUM"      :: [pttrn, i, i] => i        ("(3SUM _:_./ _)" 10)
   1.140 +  "->"        :: [i, i] => i               (infixr 60)
   1.141 +  "*"         :: [i, i] => i               (infixr 80)
   1.142 +  "@lam"      :: [pttrn, i, i] => i        ("(3lam _:_./ _)" 10)
   1.143 +  "@Ball"     :: [pttrn, i, o] => o        ("(3ALL _:_./ _)" 10)
   1.144 +  "@Bex"      :: [pttrn, i, o] => o        ("(3EX _:_./ _)" 10)
   1.145  
   1.146    (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
   1.147  
   1.148 -  "@pttrn"  :: "pttrns => pttrn"            ("<_>")
   1.149 -  ""        :: " pttrn           => pttrns" ("_")
   1.150 -  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
   1.151 +  "@pttrn"  :: pttrns => pttrn            ("<_>")
   1.152 +  ""        ::  pttrn           => pttrns ("_")
   1.153 +  "@pttrns" :: [pttrn,pttrns]   => pttrns ("_,/_")
   1.154  
   1.155  translations
   1.156    "x ~: y"      == "~ (x : y)"