src/Cube/cube.ML
author wenzelm
Tue, 20 May 1997 19:29:50 +0200
changeset 3257 4e3724e0659f
parent 203 4a213aaca3d9
permissions -rw-r--r--
README generation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	Cube/cube
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Tobias Nipkow
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1990  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For cube.thy.  The systems of the Lambda-cube that extend simple types
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Cube;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
203
4a213aaca3d9 added empty type-abbr field to extend_theory
nipkow
parents: 0
diff changeset
    13
val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],[],None)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
[
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  ("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
\	==> Abs(A,f) : Prod(A,B)")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
val lam_bs = get_axiom L2_thy "lam_bs";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val pi_bs = get_axiom L2_thy "pi_bs";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
val L2 = simple @ [lam_bs,pi_bs];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
203
4a213aaca3d9 added empty type-abbr field to extend_theory
nipkow
parents: 0
diff changeset
    26
val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],[],None)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
[
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  ("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
\	==> Abs(A,f) : Prod(A,B)")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val lam_bb = get_axiom Lomega_thy "lam_bb";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
val pi_bb = get_axiom Lomega_thy "pi_bb";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val Lomega = simple @ [lam_bb,pi_bb];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val LOmega_thy = merge_theories(L2_thy,Lomega_thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
203
4a213aaca3d9 added empty type-abbr field to extend_theory
nipkow
parents: 0
diff changeset
    41
val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],[],None)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
[
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  ("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
\	==> Abs(A,f) : Prod(A,B)")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val lam_sb = get_axiom LP_thy "lam_sb";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
val pi_sb = get_axiom LP_thy "pi_sb";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val LP = simple @ [lam_sb,pi_sb];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val LP2_thy = merge_theories(L2_thy,LP_thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val LPomega_thy = merge_theories(LP_thy,Lomega_thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val CC_thy = merge_theories(L2_thy,LPomega_thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];