0
|
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)"
|
22
|
38 |
"A -> B" => "Pi(A, _K(B))"
|
0
|
39 |
"SUM x:A. B" => "Sigma(A, %x. B)"
|
22
|
40 |
"A * B" => "Sigma(A, _K(B))"
|
0
|
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 |
|