author | wenzelm |
Mon, 25 Feb 2002 20:46:09 +0100 | |
changeset 12936 | 84eb6c75cfe3 |
parent 3837 | d7f033c74b38 |
child 14765 | bafb24c150c1 |
permissions | -rw-r--r-- |
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" |
|
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 | 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" |
|
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 | 27 |
|
28 |
SPLIT :: "[i, [i, i] => i set] => i set" |
|
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 | 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 | 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 | 39 |
|
40 |
translations |
|
41 |
"PROD x:A. B" => "Pi(A, %x. B)" |
|
22 | 42 |
"A -> B" => "Pi(A, _K(B))" |
0 | 43 |
"SUM x:A. B" => "Sigma(A, %x. B)" |
22 | 44 |
"A * B" => "Sigma(A, _K(B))" |
0 | 45 |
"{x: A. B}" == "Subtype(A, %x. B)" |
46 |
||
47 |
rules |
|
48 |
||
3837 | 49 |
Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}" |
50 |
Unit_def "Unit == {x. x=one}" |
|
51 |
Bool_def "Bool == {x. x=true | x=false}" |
|
52 |
Plus_def "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
|
53 |
Pi_def "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" |
|
54 |
Sigma_def "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" |
|
55 |
Nat_def "Nat == lfp(% X. Unit + X)" |
|
56 |
List_def "List(A) == lfp(% X. Unit + A*X)" |
|
0 | 57 |
|
3837 | 58 |
Lists_def "Lists(A) == gfp(% X. Unit + A*X)" |
0 | 59 |
ILists_def "ILists(A) == gfp(% X.{} + A*X)" |
60 |
||
3837 | 61 |
Tall_def "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" |
62 |
Tex_def "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" |
|
0 | 63 |
Lift_def "[A] == A Un {bot}" |
64 |
||
3837 | 65 |
SPLIT_def "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})" |
0 | 66 |
|
67 |
end |
|
68 |
||
69 |
||
70 |
ML |
|
71 |
||
72 |
val print_translation = |
|
73 |
[("Pi", dependent_tr' ("@Pi", "@->")), |
|
74 |
("Sigma", dependent_tr' ("@Sigma", "@*"))]; |
|
75 |