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