src/CCL/Type.thy
author wenzelm
Mon, 25 Feb 2002 20:46:09 +0100
changeset 12936 84eb6c75cfe3
parent 3837 d7f033c74b38
child 14765 bafb24c150c1
permissions -rw-r--r--
clarify module dependencies;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      CCL/types.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Martin Coen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Types in CCL are defined as sets of terms.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
Type = Term +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  Subtype       :: "['a set, 'a => o] => 'a set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  Bool          :: "i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  Unit          :: "i set"
999
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    17
  "+"           :: "[i set, i set] => i set"         (infixr 55)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  Pi            :: "[i set, i => i set] => i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  Sigma         :: "[i set, i => i set] => i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  Nat           :: "i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  List          :: "i set => i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  Lists         :: "i set => i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  ILists        :: "i set => i set"
999
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    24
  TAll          :: "(i set => i set) => i set"       (binder "TALL " 55)
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    25
  TEx           :: "(i set => i set) => i set"       (binder "TEX " 55)
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    26
  Lift          :: "i set => i set"                  ("(3[_])")
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  SPLIT         :: "[i, [i, i] => i set] => i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
999
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    30
  "@Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 999
diff changeset
    31
                                [0,0,60] 60)
999
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    32
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    33
  "@Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 999
diff changeset
    34
                                [0,0,60] 60)
999
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    35
  
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    36
  "@->"         :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    37
  "@*"          :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
9bf3816298d0 Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents: 22
diff changeset
    38
  "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
translations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  "PROD x:A. B" => "Pi(A, %x. B)"
22
41dc6b189412 added parse rules for -> and *;
wenzelm
parents: 0
diff changeset
    42
  "A -> B"      => "Pi(A, _K(B))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  "SUM x:A. B"  => "Sigma(A, %x. B)"
22
41dc6b189412 added parse rules for -> and *;
wenzelm
parents: 0
diff changeset
    44
  "A * B"       => "Sigma(A, _K(B))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  "{x: A. B}"   == "Subtype(A, %x. B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    49
  Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    50
  Unit_def          "Unit == {x. x=one}"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    51
  Bool_def          "Bool == {x. x=true | x=false}"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    52
  Plus_def           "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    53
  Pi_def         "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    54
  Sigma_def   "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    55
  Nat_def            "Nat == lfp(% X. Unit + X)"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    56
  List_def       "List(A) == lfp(% X. Unit + A*X)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    58
  Lists_def     "Lists(A) == gfp(% X. Unit + A*X)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  ILists_def   "ILists(A) == gfp(% X.{} + A*X)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    61
  Tall_def   "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    62
  Tex_def     "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  Lift_def           "[A] == A Un {bot}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1474
diff changeset
    65
  SPLIT_def   "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val print_translation =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
  [("Pi", dependent_tr' ("@Pi", "@->")),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
   ("Sigma", dependent_tr' ("@Sigma", "@*"))];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75