author  wenzelm 
Fri, 21 May 2004 21:14:18 +0200  
changeset 14765  bafb24c150c1 
parent 3837  d7f033c74b38 
child 17456  bcf7544875b2 
permissions  rwrr 
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 

14765  30 
syntax 
999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

31 
"@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" 
1474  32 
[0,0,60] 60) 
999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

33 

9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

34 
"@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" 
1474  35 
[0,0,60] 60) 
999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

36 

9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

37 
"@>" :: "[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

38 
"@*" :: "[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

39 
"@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") 
0  40 

41 
translations 

42 
"PROD x:A. B" => "Pi(A, %x. B)" 

22  43 
"A > B" => "Pi(A, _K(B))" 
0  44 
"SUM x:A. B" => "Sigma(A, %x. B)" 
22  45 
"A * B" => "Sigma(A, _K(B))" 
0  46 
"{x: A. B}" == "Subtype(A, %x. B)" 
47 

48 
rules 

49 

3837  50 
Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}" 
51 
Unit_def "Unit == {x. x=one}" 

52 
Bool_def "Bool == {x. x=true  x=false}" 

53 
Plus_def "A+B == {x. (EX a:A. x=inl(a))  (EX b:B. x=inr(b))}" 

54 
Pi_def "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" 

55 
Sigma_def "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" 

56 
Nat_def "Nat == lfp(% X. Unit + X)" 

57 
List_def "List(A) == lfp(% X. Unit + A*X)" 

0  58 

3837  59 
Lists_def "Lists(A) == gfp(% X. Unit + A*X)" 
0  60 
ILists_def "ILists(A) == gfp(% X.{} + A*X)" 
61 

3837  62 
Tall_def "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" 
63 
Tex_def "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" 

0  64 
Lift_def "[A] == A Un {bot}" 
65 

3837  66 
SPLIT_def "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})" 
0  67 

68 
end 

69 

70 

71 
ML 

72 

73 
val print_translation = 

74 
[("Pi", dependent_tr' ("@Pi", "@>")), 

75 
("Sigma", dependent_tr' ("@Sigma", "@*"))]; 

76 