src/HOL/Prod.thy
changeset 2260 b59781f2b809
parent 1765 5db6b3ea0e28
child 2393 651fce76c86c
     1.1 --- a/src/HOL/Prod.thy	Wed Nov 27 16:48:19 1996 +0100
     1.2 +++ b/src/HOL/Prod.thy	Wed Nov 27 16:51:15 1996 +0100
     1.3 @@ -9,7 +9,8 @@
     1.4  
     1.5  Prod = Fun + equalities +
     1.6  
     1.7 -(** Products **)
     1.8 +
     1.9 +(** products **)
    1.10  
    1.11  (* type definition *)
    1.12  
    1.13 @@ -21,6 +22,9 @@
    1.14    ('a, 'b) "*"          (infixr 20)
    1.15      = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
    1.16  
    1.17 +syntax (symbols)
    1.18 +  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
    1.19 +
    1.20  
    1.21  (* abstract constants and syntax *)
    1.22  
    1.23 @@ -32,30 +36,37 @@
    1.24    Pair          :: "['a, 'b] => 'a * 'b"
    1.25    Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
    1.26  
    1.27 -(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
    1.28 +
    1.29 +(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
    1.30 +
    1.31  types pttrns
    1.32  
    1.33  syntax
    1.34 -  "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
    1.35 +  "@Tuple"      :: "['a, args] => 'a * 'b"      ("(1'(_,/ _'))")
    1.36  
    1.37 -  "@pttrn"  :: [pttrn,pttrns] => pttrn              ("'(_,/_')")
    1.38 -  ""        ::  pttrn         => pttrns             ("_")
    1.39 -  "@pttrns" :: [pttrn,pttrns] => pttrns             ("_,/_")
    1.40 +  "@pttrn"      :: [pttrn, pttrns] => pttrn     ("'(_,/_')")
    1.41 +  ""            :: pttrn => pttrns              ("_")
    1.42 +  "@pttrns"     :: [pttrn, pttrns] => pttrns    ("_,/_")
    1.43  
    1.44 -  "@Sigma"  :: "[idt,'a set,'b set] => ('a * 'b)set"
    1.45 -               ("(3SIGMA _:_./ _)" 10)
    1.46 -  "@Times"  :: "['a set, 'a => 'b set] => ('a * 'b) set"
    1.47 -               ("_ Times _" [81,80] 80)
    1.48 +  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3SIGMA _:_./ _)" 10)
    1.49 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
    1.50  
    1.51  translations
    1.52    "(x, y, z)"   == "(x, (y, z))"
    1.53    "(x, y)"      == "Pair x y"
    1.54  
    1.55 -  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
    1.56 -  "%(x,y).b"      == "split(%x y.b)"
    1.57 +  "%(x,y,zs).b" == "split(%x (y,zs).b)"
    1.58 +  "%(x,y).b"    == "split(%x y.b)"
    1.59 +
    1.60 +  "SIGMA x:A.B" => "Sigma A (%x.B)"
    1.61 +  "A Times B"   => "Sigma A (_K B)"
    1.62  
    1.63 -  "SIGMA x:A. B"  =>  "Sigma A (%x.B)"
    1.64 -  "A Times B"     =>  "Sigma A (_K B)"
    1.65 +syntax (symbols)
    1.66 +  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    1.67 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
    1.68 +
    1.69 +
    1.70 +(* definitions *)
    1.71  
    1.72  defs
    1.73    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.74 @@ -65,7 +76,9 @@
    1.75    prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    1.76    Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    1.77  
    1.78 -(** Unit **)
    1.79 +
    1.80 +
    1.81 +(** unit **)
    1.82  
    1.83  typedef (Unit)
    1.84    unit = "{p. p = True}"