0

1 
(* Title: Cube/cube


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1990 University of Cambridge


5 


6 
For cube.thy. The systems of the Lambdacube that extend simple types


7 
*)


8 


9 
open Cube;


10 


11 
val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];


12 


13 
val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],None)


14 
[


15 
("pi_bs", "[ A:[]; !!x. x:A ==> B(x):* ] ==> Prod(A,B):*"),


16 


17 
("lam_bs", "[ A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* ] \


18 
\ ==> Abs(A,f) : Prod(A,B)")


19 
];


20 


21 
val lam_bs = get_axiom L2_thy "lam_bs";


22 
val pi_bs = get_axiom L2_thy "pi_bs";


23 


24 
val L2 = simple @ [lam_bs,pi_bs];


25 


26 
val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],None)


27 
[


28 
("pi_bb", "[ A:[]; !!x. x:A ==> B(x):[] ] ==> Prod(A,B):[]"),


29 


30 
("lam_bb", "[ A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] ] \


31 
\ ==> Abs(A,f) : Prod(A,B)")


32 
];


33 


34 
val lam_bb = get_axiom Lomega_thy "lam_bb";


35 
val pi_bb = get_axiom Lomega_thy "pi_bb";


36 
val Lomega = simple @ [lam_bb,pi_bb];


37 


38 
val LOmega_thy = merge_theories(L2_thy,Lomega_thy);


39 
val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];


40 


41 
val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],None)


42 
[


43 
("pi_sb", "[ A:*; !!x. x:A ==> B(x):[] ] ==> Prod(A,B):[]"),


44 


45 
("lam_sb", "[ A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] ] \


46 
\ ==> Abs(A,f) : Prod(A,B)")


47 
];


48 


49 
val lam_sb = get_axiom LP_thy "lam_sb";


50 
val pi_sb = get_axiom LP_thy "pi_sb";


51 
val LP = simple @ [lam_sb,pi_sb];


52 


53 
val LP2_thy = merge_theories(L2_thy,LP_thy);


54 
val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];


55 


56 
val LPomega_thy = merge_theories(LP_thy,Lomega_thy);


57 
val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];


58 


59 
val CC_thy = merge_theories(L2_thy,LPomega_thy);


60 
val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];
