src/Cube/Cube.thy
changeset 4583 6d9be46ea566
parent 3796 60c788035e54
child 11260 b736de4cb913
--- a/src/Cube/Cube.thy	Mon Jan 19 16:26:11 1998 +0100
+++ b/src/Cube/Cube.thy	Tue Jan 20 18:26:26 1998 +0100
@@ -1,62 +1,3 @@
-(*  Title:      Cube/Cube.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1993  University of Cambridge
-
-Barendregt's Lambda-Cube
-*)
-
-Cube = Pure +
-
-types
-  term  context  typing
-
-arities
-  term :: logic
-
-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"             ("(_:/ _)" [0, 0] 5)
 
-syntax
-  Trueprop1     :: "typing => prop"                     ("(_)")
-  ""            :: "id => context"                      ("_ ")
-  ""            :: "var => context"                     ("_ ")
-  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))"
-
-rules
-  s_b           "*: []"
+Cube = Base + L2 + Lomega + LP + LP2 + LOmega + LPomega + CC
 
-  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 ->"))];
-