src/Cube/Cube.thy
changeset 4583 6d9be46ea566
parent 3796 60c788035e54
child 11260 b736de4cb913
equal deleted inserted replaced
4582:c5cfd00e4f28 4583:6d9be46ea566
     1 (*  Title:      Cube/Cube.thy
       
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow
       
     4     Copyright   1993  University of Cambridge
       
     5 
     1 
     6 Barendregt's Lambda-Cube
     2 Cube = Base + L2 + Lomega + LP + LP2 + LOmega + LPomega + CC
     7 *)
       
     8 
     3 
     9 Cube = Pure +
       
    10 
       
    11 types
       
    12   term  context  typing
       
    13 
       
    14 arities
       
    15   term :: logic
       
    16 
       
    17 consts
       
    18   Abs, Prod     :: "[term, term => term] => term"
       
    19   Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
       
    20   MT_context    :: "context"                            ("")
       
    21   Context       :: "[typing, context] => context"       ("_ _")
       
    22   star          :: "term"                               ("*")
       
    23   box           :: "term"                               ("[]")
       
    24   "^"           :: "[term, term] => term"               (infixl 20)
       
    25   Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
       
    26 
       
    27 syntax
       
    28   Trueprop1     :: "typing => prop"                     ("(_)")
       
    29   ""            :: "id => context"                      ("_ ")
       
    30   ""            :: "var => context"                     ("_ ")
       
    31   Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
       
    32   Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
       
    33   "->"          :: "[term, term] => term"               (infixr 10)
       
    34 
       
    35 translations
       
    36   (prop) "x:X"  == (prop) "|- x:X"
       
    37   "Lam x:A. B"  == "Abs(A, %x. B)"
       
    38   "Pi x:A. B"   => "Prod(A, %x. B)"
       
    39   "A -> B"      => "Prod(A, _K(B))"
       
    40 
       
    41 rules
       
    42   s_b           "*: []"
       
    43 
       
    44   strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
       
    45   strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
       
    46 
       
    47   app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
       
    48 
       
    49   pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
       
    50 
       
    51   lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] 
       
    52                    ==> Abs(A, f) : Prod(A, B)"
       
    53 
       
    54   beta          "Abs(A, f)^a == f(a)"
       
    55 
       
    56 end
       
    57 
       
    58 
       
    59 ML
       
    60 
       
    61 val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
       
    62