src/CCL/Type.thy
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 22 41dc6b189412
permissions -rw-r--r--
Initial revision
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"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  "+"           :: "[i set, i set] => i set"            (infixr 55)
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"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  TAll          :: "(i set => i set) => i set"          (binder "TALL " 55)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  TEx           :: "(i set => i set) => i set"          (binder "TEX " 55)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  Lift          :: "i set => i set"                     ("(3[_])")
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  "@Pi"         :: "[idt, i set, i set] => i set"       ("(3PROD _:_./ _)" [] 60)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  "@Sigma"      :: "[idt, i set, i set] => i set"       ("(3SUM _:_./ _)" [] 60)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  "@->"         :: "[i set, i set] => i set"            ("(_ ->/ _)"  [54, 53] 53)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  "@*"          :: "[i set, i set] => i set"            ("(_ */ _)" [56, 55] 55)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  "@Subtype"    :: "[idt, 'a set, o] => 'a set"         ("(1{_: _ ./ _})")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
translations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  "PROD x:A. B" => "Pi(A, %x. B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  "SUM x:A. B"  => "Sigma(A, %x. B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  "{x: A. B}"   == "Subtype(A, %x. B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  Unit_def          "Unit == {x.x=one}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  Bool_def          "Bool == {x.x=true | x=false}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  Plus_def           "A+B == {x. (EX a:A.x=inl(a)) | (EX b:B.x=inr(b))}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  Pi_def         "Pi(A,B) == {x.EX b.x=lam x.b(x) & (ALL x:A.b(x):B(x))}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  Sigma_def   "Sigma(A,B) == {x.EX a:A.EX b:B(a).x=<a,b>}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  Nat_def            "Nat == lfp(% X.Unit + X)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
  List_def       "List(A) == lfp(% X.Unit + A*X)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  Lists_def     "Lists(A) == gfp(% X.Unit + A*X)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  ILists_def   "ILists(A) == gfp(% X.{} + A*X)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  Tall_def   "TALL X.B(X) == Inter({X.EX Y.X=B(Y)})"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  Tex_def     "TEX X.B(X) == Union({X.EX Y.X=B(Y)})"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  Lift_def           "[A] == A Un {bot}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  SPLIT_def   "SPLIT(p,B) == Union({A.EX x y.p=<x,y> & A=B(x,y)})"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val parse_translation =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  [("@->", ndependent_tr "Pi"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
   ("@*", ndependent_tr "Sigma")];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val print_translation =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  [("Pi", dependent_tr' ("@Pi", "@->")),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
   ("Sigma", dependent_tr' ("@Sigma", "@*"))];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73