src/HOL/Prod.thy
author nipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114 c8dfb56a7e95
parent 1081 884c6ef06fbf
child 1273 6960ec882bca
permissions -rw-r--r--
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
clasohm@923
     1
(*  Title:      HOL/Prod.thy
clasohm@923
     2
    ID:         Prod.thy,v 1.5 1994/08/19 09:04:27 lcp Exp
clasohm@923
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1992  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Ordered Pairs and the Cartesian product type.
clasohm@923
     7
The unit type.
clasohm@923
     8
*)
clasohm@923
     9
clasohm@923
    10
Prod = Fun +
clasohm@923
    11
clasohm@923
    12
(** Products **)
clasohm@923
    13
clasohm@923
    14
(* type definition *)
clasohm@923
    15
clasohm@923
    16
consts
clasohm@923
    17
  Pair_Rep      :: "['a, 'b] => ['a, 'b] => bool"
clasohm@923
    18
clasohm@923
    19
defs
clasohm@923
    20
  Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
clasohm@923
    21
clasohm@923
    22
subtype (Prod)
clasohm@923
    23
  ('a, 'b) "*"          (infixr 20)
clasohm@923
    24
    = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
clasohm@923
    25
clasohm@923
    26
clasohm@923
    27
(* abstract constants and syntax *)
clasohm@923
    28
clasohm@923
    29
consts
clasohm@923
    30
  fst           :: "'a * 'b => 'a"
clasohm@923
    31
  snd           :: "'a * 'b => 'b"
clasohm@923
    32
  split         :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
clasohm@923
    33
  prod_fun      :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
clasohm@923
    34
  Pair          :: "['a, 'b] => 'a * 'b"
clasohm@923
    35
  Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
clasohm@923
    36
nipkow@1068
    37
(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
nipkow@1068
    38
types pttrns
nipkow@1068
    39
clasohm@923
    40
syntax
clasohm@972
    41
  "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
clasohm@923
    42
nipkow@1114
    43
  "@pttrn"  :: "[pttrn,pttrns] => pttrn"              ("'(_,/_')")
nipkow@1114
    44
  ""        :: " pttrn         => pttrns"             ("_")
nipkow@1114
    45
  "@pttrns" :: "[pttrn,pttrns] => pttrns"             ("_,/_")
nipkow@1068
    46
clasohm@923
    47
translations
clasohm@972
    48
  "(x, y, z)"   == "(x, (y, z))"
clasohm@972
    49
  "(x, y)"      == "Pair x y"
clasohm@923
    50
nipkow@1114
    51
  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
nipkow@1114
    52
  "%(x,y).b"      == "split(%x y.b)"
nipkow@1068
    53
(* The <= direction fails if split has more than one argument because
nipkow@1068
    54
   ast-matching fails. Otherwise it would work fine *)
nipkow@1068
    55
clasohm@923
    56
defs
clasohm@923
    57
  Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
clasohm@972
    58
  fst_def       "fst(p) == @a. ? b. p = (a, b)"
clasohm@972
    59
  snd_def       "snd(p) == @b. ? a. p = (a, b)"
clasohm@923
    60
  split_def     "split c p == c (fst p) (snd p)"
clasohm@972
    61
  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
clasohm@972
    62
  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
clasohm@923
    63
clasohm@923
    64
clasohm@923
    65
clasohm@923
    66
(** Unit **)
clasohm@923
    67
clasohm@923
    68
subtype (Unit)
clasohm@923
    69
  unit = "{p. p = True}"
clasohm@923
    70
clasohm@923
    71
consts
clasohm@972
    72
  "()"          :: "unit"                           ("'(')")
clasohm@923
    73
clasohm@923
    74
defs
clasohm@972
    75
  Unity_def     "() == Abs_Unit(True)"
clasohm@923
    76
clasohm@923
    77
end
nipkow@1114
    78
(*
nipkow@1068
    79
ML
nipkow@1068
    80
nipkow@1068
    81
local open Syntax
nipkow@1068
    82
nipkow@1114
    83
fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
nipkow@1068
    84
fun pttrns s t = const"@pttrns" $ s $ t;
nipkow@1068
    85
nipkow@1068
    86
fun split2(Abs(x,T,t)) =
nipkow@1068
    87
      let val (pats,u) = split1 t
nipkow@1068
    88
      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
nipkow@1068
    89
  | split2(Const("split",_) $ r) =
nipkow@1068
    90
      let val (pats,s) = split2(r)
nipkow@1068
    91
          val (pats2,t) = split1(s)
nipkow@1068
    92
      in (pttrns (pttrn pats) pats2, t) end
nipkow@1068
    93
and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
nipkow@1068
    94
  | split1(Const("split",_)$t) = split2(t);
nipkow@1068
    95
nipkow@1068
    96
fun split_tr'(t::args) =
nipkow@1068
    97
  let val (pats,ft) = split2(t)
nipkow@1081
    98
  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
nipkow@1068
    99
nipkow@1068
   100
in
nipkow@1068
   101
nipkow@1068
   102
val print_translation = [("split", split_tr')];
nipkow@1068
   103
nipkow@1068
   104
end;
nipkow@1114
   105
*)