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