author  wenzelm 
Sat, 17 Sep 2005 17:35:26 +0200  
changeset 17456  bcf7544875b2 
parent 14765  bafb24c150c1 
child 17782  b3846df9d643 
permissions  rwrr 
17456  1 
(* Title: CCL/Type.thy 
0  2 
ID: $Id$ 
3 
Author: Martin Coen 

4 
Copyright 1993 University of Cambridge 

5 
*) 

6 

17456  7 
header {* Types in CCL are defined as sets of terms *} 
8 

9 
theory Type 

10 
imports Term 

11 
begin 

0  12 

13 
consts 

14 

15 
Subtype :: "['a set, 'a => o] => 'a set" 

16 
Bool :: "i set" 

17 
Unit :: "i set" 

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

18 
"+" :: "[i set, i set] => i set" (infixr 55) 
0  19 
Pi :: "[i set, i => i set] => i set" 
20 
Sigma :: "[i set, i => i set] => i set" 

21 
Nat :: "i set" 

22 
List :: "i set => i set" 

23 
Lists :: "i set => i set" 

24 
ILists :: "i set => i set" 

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

25 
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

26 
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

27 
Lift :: "i set => i set" ("(3[_])") 
0  28 

29 
SPLIT :: "[i, [i, i] => i set] => i set" 

30 

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

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

34 

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

35 
"@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" 
1474  36 
[0,0,60] 60) 
17456  37 

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

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

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

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

42 
translations 

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

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

17456  49 
print_translation {* 
50 
[("Pi", dependent_tr' ("@Pi", "@>")), 

51 
("Sigma", dependent_tr' ("@Sigma", "@*"))] *} 

0  52 

17456  53 
axioms 
54 
Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" 

55 
Unit_def: "Unit == {x. x=one}" 

56 
Bool_def: "Bool == {x. x=true  x=false}" 

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

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

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

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

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

0  62 

17456  63 
Lists_def: "Lists(A) == gfp(% X. Unit + A*X)" 
64 
ILists_def: "ILists(A) == gfp(% X.{} + A*X)" 

0  65 

17456  66 
Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" 
67 
Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" 

68 
Lift_def: "[A] == A Un {bot}" 

0  69 

17456  70 
SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})" 
71 

72 
ML {* use_legacy_bindings (the_context ()) *} 

0  73 

74 
end 