1 (* Title: Cube/cube |
1 (* Title: Cube/Cube.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1990 University of Cambridge |
4 Copyright 1990 University of Cambridge |
5 |
5 |
6 For cube.thy. The systems of the Lambda-cube that extend simple types |
6 For Cube.thy. The systems of the Lambda-cube that extend simple types |
7 *) |
7 *) |
8 |
8 |
9 open Cube; |
9 open Cube; |
10 |
10 |
11 val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss]; |
11 val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss]; |
12 |
12 |
13 val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],[],None) |
13 val L2_thy = |
14 [ |
14 Cube.thy |
15 ("pi_bs", "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"), |
15 |> add_axioms |
16 |
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):* |] \ |
17 ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \ |
18 \ ==> Abs(A,f) : Prod(A,B)") |
18 \ ==> Abs(A,f) : Prod(A,B)")] |
19 ]; |
19 |> add_thyname "L2"; |
20 |
20 |
21 val lam_bs = get_axiom L2_thy "lam_bs"; |
21 val lam_bs = get_axiom L2_thy "lam_bs"; |
22 val pi_bs = get_axiom L2_thy "pi_bs"; |
22 val pi_bs = get_axiom L2_thy "pi_bs"; |
23 |
23 |
24 val L2 = simple @ [lam_bs,pi_bs]; |
24 val L2 = simple @ [lam_bs,pi_bs]; |
25 |
25 |
26 val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],[],None) |
26 val Lomega_thy = |
27 [ |
27 Cube.thy |
28 ("pi_bb", "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"), |
28 |> add_axioms |
29 |
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):[] |] \ |
30 ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \ |
31 \ ==> Abs(A,f) : Prod(A,B)") |
31 \ ==> Abs(A,f) : Prod(A,B)")] |
32 ]; |
32 |> add_thyname "Lomega"; |
33 |
33 |
34 val lam_bb = get_axiom Lomega_thy "lam_bb"; |
34 val lam_bb = get_axiom Lomega_thy "lam_bb"; |
35 val pi_bb = get_axiom Lomega_thy "pi_bb"; |
35 val pi_bb = get_axiom Lomega_thy "pi_bb"; |
36 val Lomega = simple @ [lam_bb,pi_bb]; |
36 val Lomega = simple @ [lam_bb,pi_bb]; |
37 |
37 |
38 val LOmega_thy = merge_theories(L2_thy,Lomega_thy); |
38 val LOmega_thy = merge_theories(L2_thy,Lomega_thy); |
39 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb]; |
39 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb]; |
40 |
40 |
41 val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],[],None) |
41 val LP_thy = |
42 [ |
42 Cube.thy |
43 ("pi_sb", "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"), |
43 |> add_axioms |
44 |
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):[] |] \ |
45 ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \ |
46 \ ==> Abs(A,f) : Prod(A,B)") |
46 \ ==> Abs(A,f) : Prod(A,B)")] |
47 ]; |
47 |> add_thyname "LP"; |
48 |
48 |
49 val lam_sb = get_axiom LP_thy "lam_sb"; |
49 val lam_sb = get_axiom LP_thy "lam_sb"; |
50 val pi_sb = get_axiom LP_thy "pi_sb"; |
50 val pi_sb = get_axiom LP_thy "pi_sb"; |
51 val LP = simple @ [lam_sb,pi_sb]; |
51 val LP = simple @ [lam_sb,pi_sb]; |
52 |
52 |