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 
