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