src/ZF/ZF.thy
changeset 675 59a4fa76b590
parent 632 f9a3f77f71e8
child 690 b2bd1d5a3d16
equal deleted inserted replaced
674:41b59e4c78c4 675:59a4fa76b590
    14 arities
    14 arities
    15   i :: term
    15   i :: term
    16 
    16 
    17 consts
    17 consts
    18 
    18 
    19   "0"           :: "i"                  ("0")   (*the empty set*)
    19   "0"         :: "i"                  ("0")   (*the empty set*)
    20   Pow           :: "i => i"                     (*power sets*)
    20   Pow         :: "i => i"                     (*power sets*)
    21   Inf           :: "i"                          (*infinite set*)
    21   Inf         :: "i"                          (*infinite set*)
    22 
    22 
    23   (* Bounded Quantifiers *)
    23   (* Bounded Quantifiers *)
    24 
    24 
    25   Ball, Bex     :: "[i, i => o] => o"
    25   Ball, Bex   :: "[i, i => o] => o"
    26 
    26 
    27   (* General Union and Intersection *)
    27   (* General Union and Intersection *)
    28 
    28 
    29   Union, Inter  :: "i => i"
    29   Union,Inter :: "i => i"
    30 
    30 
    31   (* Variations on Replacement *)
    31   (* Variations on Replacement *)
    32 
    32 
    33   PrimReplace   :: "[i, [i, i] => o] => i"
    33   PrimReplace :: "[i, [i, i] => o] => i"
    34   Replace       :: "[i, [i, i] => o] => i"
    34   Replace     :: "[i, [i, i] => o] => i"
    35   RepFun        :: "[i, i => i] => i"
    35   RepFun      :: "[i, i => i] => i"
    36   Collect       :: "[i, i => o] => i"
    36   Collect     :: "[i, i => o] => i"
    37 
    37 
    38   (* Descriptions *)
    38   (* Descriptions *)
    39 
    39 
    40   The           :: "(i => o) => i"      (binder "THE " 10)
    40   The         :: "(i => o) => i"      (binder "THE " 10)
    41   if            :: "[o, i, i] => i"
    41   if          :: "[o, i, i] => i"
    42 
    42 
    43   (* Finite Sets *)
    43   (* Finite Sets *)
    44 
    44 
    45   Upair, cons   :: "[i, i] => i"
    45   Upair, cons :: "[i, i] => i"
    46   succ          :: "i => i"
    46   succ        :: "i => i"
    47 
    47 
    48   (* Ordered Pairing *)
    48   (* Ordered Pairing *)
    49 
    49 
    50   Pair          :: "[i, i] => i"
    50   Pair        :: "[i, i] => i"
    51   fst, snd      :: "i => i"
    51   fst, snd    :: "i => i"
    52   split         :: "[[i, i] => i, i] => i"
    52   split       :: "[[i, i] => i, i] => i"
    53   fsplit        :: "[[i, i] => o, i] => o"
    53   fsplit      :: "[[i, i] => o, i] => o"
    54 
    54 
    55   (* Sigma and Pi Operators *)
    55   (* Sigma and Pi Operators *)
    56 
    56 
    57   Sigma, Pi     :: "[i, i => i] => i"
    57   Sigma, Pi   :: "[i, i => i] => i"
    58 
    58 
    59   (* Relations and Functions *)
    59   (* Relations and Functions *)
    60 
    60 
    61   domain        :: "i => i"
    61   domain      :: "i => i"
    62   range         :: "i => i"
    62   range       :: "i => i"
    63   field         :: "i => i"
    63   field       :: "i => i"
    64   converse      :: "i => i"
    64   converse    :: "i => i"
    65   Lambda        :: "[i, i => i] => i"
    65   Lambda      :: "[i, i => i] => i"
    66   restrict      :: "[i, i] => i"
    66   restrict    :: "[i, i] => i"
    67 
    67 
    68   (* Infixes in order of decreasing precedence *)
    68   (* Infixes in order of decreasing precedence *)
    69 
    69 
    70   "``"          :: "[i, i] => i"    (infixl 90) (*image*)
    70   "``"        :: "[i, i] => i"    (infixl 90) (*image*)
    71   "-``"         :: "[i, i] => i"    (infixl 90) (*inverse image*)
    71   "-``"       :: "[i, i] => i"    (infixl 90) (*inverse image*)
    72   "`"           :: "[i, i] => i"    (infixl 90) (*function application*)
    72   "`"         :: "[i, i] => i"    (infixl 90) (*function application*)
    73 (*"*"           :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
    73 (*"*"         :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
    74   "Int"         :: "[i, i] => i"    (infixl 70) (*binary intersection*)
    74   "Int"       :: "[i, i] => i"    (infixl 70) (*binary intersection*)
    75   "Un"          :: "[i, i] => i"    (infixl 65) (*binary union*)
    75   "Un"        :: "[i, i] => i"    (infixl 65) (*binary union*)
    76   "-"           :: "[i, i] => i"    (infixl 65) (*set difference*)
    76   "-"         :: "[i, i] => i"    (infixl 65) (*set difference*)
    77 (*"->"          :: "[i, i] => i"    (infixr 60) (*function space*)*)
    77 (*"->"        :: "[i, i] => i"    (infixr 60) (*function space*)*)
    78   "<="          :: "[i, i] => o"    (infixl 50) (*subset relation*)
    78   "<="        :: "[i, i] => o"    (infixl 50) (*subset relation*)
    79   ":"           :: "[i, i] => o"    (infixl 50) (*membership relation*)
    79   ":"         :: "[i, i] => o"    (infixl 50) (*membership relation*)
    80 (*"~:"          :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
    80 (*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
    81 
    81 
    82 
    82 
    83 types
    83 types
    84   is
    84   is
    85 
    85 
    86 syntax
    86 syntax
    87   ""            :: "i => is"                    ("_")
    87   ""          :: "i => is"                 ("_")
    88   "@Enum"       :: "[i, is] => is"              ("_,/ _")
    88   "@Enum"     :: "[i, is] => is"           ("_,/ _")
    89   "~:"          :: "[i, i] => o"                (infixl 50)
    89   "~:"        :: "[i, i] => o"             (infixl 50)
    90   "@Finset"     :: "is => i"                    ("{(_)}")
    90   "@Finset"   :: "is => i"                 ("{(_)}")
    91   "@Tuple"      :: "[i, is] => i"               ("<(_,/ _)>")
    91   "@Tuple"    :: "[i, is] => i"            ("<(_,/ _)>")
    92   "@Collect"    :: "[idt, i, o] => i"           ("(1{_: _ ./ _})")
    92   "@Collect"  :: "[idt, i, o] => i"        ("(1{_: _ ./ _})")
    93   "@Replace"    :: "[idt, idt, i, o] => i"      ("(1{_ ./ _: _, _})")
    93   "@Replace"  :: "[idt, idt, i, o] => i"   ("(1{_ ./ _: _, _})")
    94   "@RepFun"     :: "[i, idt, i] => i"           ("(1{_ ./ _: _})")
    94   "@RepFun"   :: "[i, idt, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
    95   "@INTER"      :: "[idt, i, i] => i"           ("(3INT _:_./ _)" 10)
    95   "@INTER"    :: "[idt, i, i] => i"        ("(3INT _:_./ _)" 10)
    96   "@UNION"      :: "[idt, i, i] => i"           ("(3UN _:_./ _)" 10)
    96   "@UNION"    :: "[idt, i, i] => i"        ("(3UN _:_./ _)" 10)
    97   "@PROD"       :: "[idt, i, i] => i"           ("(3PROD _:_./ _)" 10)
    97   "@PROD"     :: "[idt, i, i] => i"        ("(3PROD _:_./ _)" 10)
    98   "@SUM"        :: "[idt, i, i] => i"           ("(3SUM _:_./ _)" 10)
    98   "@SUM"      :: "[idt, i, i] => i"        ("(3SUM _:_./ _)" 10)
    99   "->"          :: "[i, i] => i"                (infixr 60)
    99   "->"        :: "[i, i] => i"             (infixr 60)
   100   "*"           :: "[i, i] => i"                (infixr 80)
   100   "*"         :: "[i, i] => i"             (infixr 80)
   101   "@lam"        :: "[idt, i, i] => i"           ("(3lam _:_./ _)" 10)
   101   "@lam"      :: "[idt, i, i] => i"        ("(3lam _:_./ _)" 10)
   102   "@Ball"       :: "[idt, i, o] => o"           ("(3ALL _:_./ _)" 10)
   102   "@Ball"     :: "[idt, i, o] => o"        ("(3ALL _:_./ _)" 10)
   103   "@Bex"        :: "[idt, i, o] => o"           ("(3EX _:_./ _)" 10)
   103   "@Bex"      :: "[idt, i, o] => o"        ("(3EX _:_./ _)" 10)
   104 
   104 
   105 translations
   105 translations
   106   "x ~: y"      == "~ (x : y)"
   106   "x ~: y"      == "~ (x : y)"
   107   "{x, xs}"     == "cons(x, {xs})"
   107   "{x, xs}"     == "cons(x, {xs})"
   108   "{x}"         == "cons(x, 0)"
   108   "{x}"         == "cons(x, 0)"