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