# HG changeset patch # User wenzelm # Date 1125776592 -7200 # Node ID 84fcead1f20b2871d408f23af6b04955294770d1 # Parent 158ef530c153d9076d69b867e6aa05d6cf377af1 obsolete (see Cube.thy); diff -r 158ef530c153 -r 84fcead1f20b src/Cube/Base.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/Base.thy --- 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" ("(_/ \\ _)") - box :: "term" ("\\") - Lam :: "[idt, term, term] => term" ("(3\\_:_./ _)" [0, 0, 0] 10) - Pi :: "[idt, term, term] => term" ("(3\\_:_./ _)" [0, 0] 10) - "op ->" :: "[term, term] => term" (infixr "\\" 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 ->"))]; - diff -r 158ef530c153 -r 84fcead1f20b src/Cube/CC.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/CC.thy --- 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 - diff -r 158ef530c153 -r 84fcead1f20b src/Cube/L2.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/L2.thy --- 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 diff -r 158ef530c153 -r 84fcead1f20b src/Cube/LP.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/LP.thy --- 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 diff -r 158ef530c153 -r 84fcead1f20b src/Cube/LP2.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/LP2.thy --- 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 diff -r 158ef530c153 -r 84fcead1f20b src/Cube/LPomega.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/LPomega.thy --- 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 diff -r 158ef530c153 -r 84fcead1f20b src/Cube/Lomega.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/Lomega.thy --- 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 diff -r 158ef530c153 -r 84fcead1f20b src/Cube/Lomega2.ML --- 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]; diff -r 158ef530c153 -r 84fcead1f20b src/Cube/Lomega2.thy --- 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