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

4026

15 
> PureThy.add_store_axioms

420

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)")]

3771

19 
> Theory.add_name "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

4026

28 
> PureThy.add_store_axioms

420

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)")]

3771

32 
> Theory.add_name "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 

3884

38 
val LOmega_thy = merge_theories "LOmega" (L2_thy,Lomega_thy);

0

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


40 

420

41 
val LP_thy =


42 
Cube.thy

4026

43 
> PureThy.add_store_axioms

420

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)")]

3771

47 
> Theory.add_name "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 

3884

53 
val LP2_thy = merge_theories "LP2" (L2_thy,LP_thy);

0

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


55 

3884

56 
val LPomega_thy = merge_theories "LPomega" (LP_thy,Lomega_thy);

0

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


58 

3884

59 
val CC_thy = merge_theories "CC" (L2_thy,LPomega_thy);

0

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