src/HOL/Prod.thy
author nipkow
Sat Apr 22 13:25:31 1995 +0200 (1995-04-22)
changeset 1068 e0f2dffab506
parent 972 e61b058d58d2
child 1081 884c6ef06fbf
permissions -rw-r--r--
HOL.thy:

"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)


Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.


Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:

idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.


Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.
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@1068
    43
  "@pttrn"  :: "pttrns => pttrn"            ("'(_')")
nipkow@1068
    44
  ""        :: " pttrn           => pttrns" ("_")
nipkow@1068
    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@1068
    51
  "%(x,y,zs).b"   => "split(%x (y,zs).b)"
nipkow@1068
    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@1068
    78
nipkow@1068
    79
ML
nipkow@1068
    80
nipkow@1068
    81
local open Syntax
nipkow@1068
    82
nipkow@1068
    83
fun pttrn s = const"@pttrn" $ s;
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@1068
    98
  in case args of
nipkow@1068
    99
       [] => const"_abs" $ pttrn pats $ ft
nipkow@1068
   100
     | arg::rest =>
nipkow@1068
   101
         list_comb(const"_Let"$(const"_bind"$(pttrn pats)$arg)$ft, rest)
nipkow@1068
   102
  end
nipkow@1068
   103
nipkow@1068
   104
in
nipkow@1068
   105
nipkow@1068
   106
val print_translation = [("split", split_tr')];
nipkow@1068
   107
nipkow@1068
   108
end;