--- a/src/Cube/Base.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
--- a/src/Cube/Base.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(* Title: Cube/Base.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1993 University of Cambridge
-
-Barendregt's Lambda-Cube.
-*)
-
-Base = Pure +
-
-types
- term
-
-types
- context typing
-nonterminals
- context_ typing_
-
-consts
- Abs, Prod :: "[term, term => term] => term"
- Trueprop :: "[context, typing] => prop"
- MT_context :: "context"
- Context :: "[typing, context] => context"
- star :: "term" ("*")
- box :: "term" ("[]")
- "^" :: "[term, term] => term" (infixl 20)
- Has_type :: "[term, term] => typing"
-
-syntax
- Trueprop :: "[context_, typing_] => prop" ("(_/ |- _)")
- Trueprop1 :: "typing_ => prop" ("(_)")
- "" :: "id => context_" ("_")
- "" :: "var => context_" ("_")
- MT_context :: "context_" ("")
- Context :: "[typing_, context_] => context_" ("_ _")
- Has_type :: "[term, term] => typing_" ("(_:/ _)" [0, 0] 5)
- Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
- Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
- "->" :: "[term, term] => term" (infixr 10)
-
-translations
- (prop) "x:X" == (prop) "|- x:X"
- "Lam x:A. B" == "Abs(A, %x. B)"
- "Pi x:A. B" => "Prod(A, %x. B)"
- "A -> B" => "Prod(A, _K(B))"
-
-syntax (xsymbols)
- Trueprop :: "[context_, typing_] => prop" ("(_/ \\<turnstile> _)")
- box :: "term" ("\\<box>")
- Lam :: "[idt, term, term] => term" ("(3\\<Lambda>_:_./ _)" [0, 0, 0] 10)
- Pi :: "[idt, term, term] => term" ("(3\\<Pi>_:_./ _)" [0, 0] 10)
- "op ->" :: "[term, term] => term" (infixr "\\<rightarrow>" 10)
-
-
-rules
- s_b "*: []"
-
- strip_s "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X"
- strip_b "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
-
- app "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
-
- pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
-
- lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
- ==> Abs(A, f) : Prod(A, B)"
-
- beta "Abs(A, f)^a == f(a)"
-
-end
-
-
-ML
-
-val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
-
--- a/src/Cube/CC.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];
--- a/src/Cube/CC.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-
-CC = L2 + LP + Lomega
-
--- a/src/Cube/L2.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val L2 = simple @ [lam_bs,pi_bs];
--- a/src/Cube/L2.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-
-L2 = Base +
-
-rules
- pi_bs "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
- lam_bs "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
- ==> Abs(A,f) : Prod(A,B)"
-
-end
--- a/src/Cube/LP.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val LP = simple @ [lam_sb,pi_sb];
--- a/src/Cube/LP.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-
-LP = Base +
-
-rules
- pi_sb "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
- lam_sb "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
- ==> Abs(A,f) : Prod(A,B)"
-
-end
--- a/src/Cube/LP2.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];
--- a/src/Cube/LP2.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-LP2 = LP + L2
--- a/src/Cube/LPomega.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];
--- a/src/Cube/LPomega.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-LPomega = LP + Lomega
--- a/src/Cube/Lomega.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val Lomega = simple @ [lam_bb,pi_bb];
--- a/src/Cube/Lomega.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-
-Lomega = Base +
-
-rules
- pi_bb "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
- lam_bb "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
- ==> Abs(A,f) : Prod(A,B)"
-
-end
--- a/src/Cube/Lomega2.ML Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val Lomega2 = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
--- a/src/Cube/Lomega2.thy Sat Sep 03 18:00:48 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-Lomega2 = L2 + Lomega