0

1 
(* Title: Cube/cube.thy


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1993 University of Cambridge


5 


6 
Barendregt's LambdaCube


7 
*)


8 


9 
Cube = Pure +


10 


11 
types


12 
term, context, typing 0


13 


14 
arities


15 
term :: logic


16 


17 
consts


18 
Abs, Prod :: "[term, term => term] => term"


19 
Trueprop :: "[context, typing] => prop" ("(_/  _)")


20 
Trueprop1 :: "typing => prop" ("(_)")


21 
MT_context :: "context" ("")


22 
"" :: "id => context" ("_ ")


23 
"" :: "var => context" ("_ ")


24 
Context :: "[typing, context] => context" ("_ _")


25 
star :: "term" ("*")


26 
box :: "term" ("[]")


27 
"^" :: "[term, term] => term" (infixl 20)

21

28 
Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)


29 
Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)

0

30 
">" :: "[term, term] => term" (infixr 10)


31 
Has_type :: "[term, term] => typing" ("(_:/ _)" [0, 0] 5)


32 


33 
translations


34 
(prop) "x:X" == (prop) " x:X"


35 
"Lam x:A. B" == "Abs(A, %x. B)"


36 
"Pi x:A. B" => "Prod(A, %x. B)"

21

37 
"A > B" => "Prod(A, _K(B))"

0

38 


39 
rules


40 
s_b "*: []"


41 


42 
strip_s "[ A:*; a:A ==> G  x:X ] ==> a:A G  x:X"


43 
strip_b "[ A:[]; a:A ==> G  x:X ] ==> a:A G  x:X"


44 


45 
app "[ F:Prod(A, B); C:A ] ==> F^C: B(C)"


46 


47 
pi_ss "[ A:*; !!x. x:A ==> B(x):* ] ==> Prod(A, B):*"


48 


49 
lam_ss "[ A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* ] \


50 
\ ==> Abs(A, f) : Prod(A, B)"


51 


52 
beta "Abs(A, f)^a == f(a)"


53 


54 
end


55 


56 


57 
ML


58 


59 
val print_translation = [("Prod", dependent_tr' ("Pi", "op >"))];


60 
