src/Cube/Cube.thy
changeset 0 a5a9c433f639
child 21 b5f8677e24e7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Cube/Cube.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,60 @@
     1.4 +(*  Title:      Cube/cube.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Barendregt's Lambda-Cube
    1.10 +*)
    1.11 +
    1.12 +Cube = Pure +
    1.13 +
    1.14 +types
    1.15 +  term, context, typing 0
    1.16 +
    1.17 +arities
    1.18 +  term :: logic
    1.19 +
    1.20 +consts
    1.21 +  Abs, Prod     :: "[term, term => term] => term"
    1.22 +  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
    1.23 +  Trueprop1     :: "typing => prop"                     ("(_)")
    1.24 +  MT_context    :: "context"                            ("")
    1.25 +  ""            :: "id => context"                      ("_ ")
    1.26 +  ""            :: "var => context"                     ("_ ")
    1.27 +  Context       :: "[typing, context] => context"       ("_ _")
    1.28 +  star          :: "term"                               ("*")
    1.29 +  box           :: "term"                               ("[]")
    1.30 +  "^"           :: "[term, term] => term"               (infixl 20)
    1.31 +  Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
    1.32 +  Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
    1.33 +  "->"          :: "[term, term] => term"               (infixr 10)
    1.34 +  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
    1.35 +
    1.36 +translations
    1.37 +  (prop) "x:X"  == (prop) "|- x:X"
    1.38 +  "Lam x:A. B"  == "Abs(A, %x. B)"
    1.39 +  "Pi x:A. B"   => "Prod(A, %x. B)"
    1.40 +
    1.41 +rules
    1.42 +  s_b           "*: []"
    1.43 +
    1.44 +  strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
    1.45 +  strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
    1.46 +
    1.47 +  app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
    1.48 +
    1.49 +  pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
    1.50 +
    1.51 +  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
    1.52 +\                   ==> Abs(A, f) : Prod(A, B)"
    1.53 +
    1.54 +  beta          "Abs(A, f)^a == f(a)"
    1.55 +
    1.56 +end
    1.57 +
    1.58 +
    1.59 +ML
    1.60 +
    1.61 +val parse_translation = [("op ->", ndependent_tr "Prod")];
    1.62 +val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
    1.63 +