src/ZF/ZF.thy
 changeset 675 59a4fa76b590 parent 632 f9a3f77f71e8 child 690 b2bd1d5a3d16
equal 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)"`