420

1 
(* Title: Cube/Cube.ML

0

2 
ID: $Id$

420

3 
Author: Tobias Nipkow

0

4 
Copyright 1990 University of Cambridge


5 

420

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

0

7 
*)


8 


9 
open Cube;


10 


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


12 

420

13 
val L2_thy =


14 
Cube.thy


15 
> add_axioms


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


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


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


19 
> add_thyname "L2";

0

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 

420

26 
val Lomega_thy =


27 
Cube.thy


28 
> add_axioms


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


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


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


32 
> add_thyname "Lomega";

0

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 

420

41 
val LP_thy =


42 
Cube.thy


43 
> add_axioms


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


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


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


47 
> add_thyname "LP";

0

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];
