src/HOL/Product_Type.thy
changeset 10213 01c2744a3786
child 10289 475ea668c67d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Oct 12 18:44:35 2000 +0200
     1.3 @@ -0,0 +1,109 @@
     1.4 +(*  Title:      HOL/Product_Type.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Ordered Pairs and the Cartesian product type.
    1.10 +The unit type.
    1.11 +*)
    1.12 +
    1.13 +Product_Type = Fun + equalities +
    1.14 +
    1.15 +
    1.16 +(** products **)
    1.17 +
    1.18 +(* type definition *)
    1.19 +
    1.20 +constdefs
    1.21 +  Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
    1.22 +  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    1.23 +
    1.24 +global
    1.25 +
    1.26 +typedef (Prod)
    1.27 +  ('a, 'b) "*"          (infixr 20)
    1.28 +    = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
    1.29 +
    1.30 +syntax (symbols)
    1.31 +  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
    1.32 +
    1.33 +syntax (HTML output)
    1.34 +  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
    1.35 +
    1.36 +
    1.37 +(* abstract constants and syntax *)
    1.38 +
    1.39 +consts
    1.40 +  fst           :: "'a * 'b => 'a"
    1.41 +  snd           :: "'a * 'b => 'b"
    1.42 +  split         :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
    1.43 +  prod_fun      :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
    1.44 +  Pair          :: "['a, 'b] => 'a * 'b"
    1.45 +  Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
    1.46 +
    1.47 +
    1.48 +(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
    1.49 +
    1.50 +nonterminals
    1.51 +  tuple_args patterns
    1.52 +
    1.53 +syntax
    1.54 +  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
    1.55 +  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
    1.56 +  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
    1.57 +  "_pattern"    :: [pttrn, patterns] => pttrn           ("'(_,/ _')")
    1.58 +  ""            :: pttrn => patterns                    ("_")
    1.59 +  "_patterns"   :: [pttrn, patterns] => patterns        ("_,/ _")
    1.60 +  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
    1.61 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
    1.62 +
    1.63 +translations
    1.64 +  "(x, y)"       == "Pair x y"
    1.65 +  "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
    1.66 +  "%(x,y,zs).b"  == "split(%x (y,zs).b)"
    1.67 +  "%(x,y).b"     == "split(%x y. b)"
    1.68 +  "_abs (Pair x y) t" => "%(x,y).t"
    1.69 +  (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
    1.70 +     The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
    1.71 +
    1.72 +  "SIGMA x:A. B" => "Sigma A (%x. B)"
    1.73 +  "A <*> B"      => "Sigma A (_K B)"
    1.74 +
    1.75 +syntax (symbols)
    1.76 +  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
    1.77 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
    1.78 +
    1.79 +
    1.80 +(* definitions *)
    1.81 +
    1.82 +local
    1.83 +
    1.84 +defs
    1.85 +  Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.86 +  fst_def       "fst p == @a. ? b. p = (a, b)"
    1.87 +  snd_def       "snd p == @b. ? a. p = (a, b)"
    1.88 +  split_def     "split == (%c p. c (fst p) (snd p))"
    1.89 +  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    1.90 +  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    1.91 +
    1.92 +
    1.93 +
    1.94 +(** unit **)
    1.95 +
    1.96 +global
    1.97 +
    1.98 +typedef  unit = "{True}"
    1.99 +
   1.100 +consts
   1.101 +  "()"          :: unit                           ("'(')")
   1.102 +
   1.103 +local
   1.104 +
   1.105 +defs
   1.106 +  Unity_def     "() == Abs_unit True"
   1.107 +
   1.108 +end
   1.109 +
   1.110 +ML
   1.111 +
   1.112 +val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];