22809

1 
(* Title: Cube/Cube.thy


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
*)

3773

5 

17252

6 
header {* Barendregt's LambdaCube *}


7 


8 
theory Cube


9 
imports Pure


10 
begin


11 


12 
typedecl "term"


13 
typedecl "context"


14 
typedecl typing


15 


16 
nonterminals


17 
context_ typing_


18 


19 
consts


20 
Abs :: "[term, term => term] => term"


21 
Prod :: "[term, term => term] => term"


22 
Trueprop :: "[context, typing] => prop"


23 
MT_context :: "context"


24 
Context :: "[typing, context] => context"


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


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


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


28 
Has_type :: "[term, term] => typing"


29 


30 
syntax


31 
Trueprop :: "[context_, typing_] => prop" ("(_/  _)")


32 
Trueprop1 :: "typing_ => prop" ("(_)")


33 
"" :: "id => context_" ("_")


34 
"" :: "var => context_" ("_")


35 
MT_context :: "context_" ("")


36 
Context :: "[typing_, context_] => context_" ("_ _")


37 
Has_type :: "[term, term] => typing_" ("(_:/ _)" [0, 0] 5)


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


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


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


41 


42 
translations

17260

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


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


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

17782

46 
"A > B" => "Prod(A, %_. B)"

17252

47 


48 
syntax (xsymbols)


49 
Trueprop :: "[context_, typing_] => prop" ("(_/ \<turnstile> _)")


50 
box :: "term" ("\<box>")


51 
Lam :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)


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


53 
arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10)


54 


55 
print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}


56 


57 
axioms


58 
s_b: "*: []"


59 


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


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


62 


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

0

64 

17252

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


66 


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


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


69 


70 
beta: "Abs(A, f)^a == f(a)"


71 


72 
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss


73 
lemmas rules = simple


74 


75 
lemma imp_elim:


76 
assumes "f:A>B" and "a:A" and "f^a:B ==> PROP P"


77 
shows "PROP P" by (rule app prems)+


78 


79 
lemma pi_elim:


80 
assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"


81 
shows "PROP P" by (rule app prems)+


82 


83 


84 
locale L2 =


85 
assumes pi_bs: "[ A:[]; !!x. x:A ==> B(x):* ] ==> Prod(A,B):*"


86 
and lam_bs: "[ A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* ]


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


88 


89 
lemmas (in L2) rules = simple lam_bs pi_bs


90 

17260

91 

17252

92 
locale Lomega =


93 
assumes


94 
pi_bb: "[ A:[]; !!x. x:A ==> B(x):[] ] ==> Prod(A,B):[]"


95 
and lam_bb: "[ A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] ]


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


97 


98 
lemmas (in Lomega) rules = simple lam_bb pi_bb


99 


100 


101 
locale LP =


102 
assumes pi_sb: "[ A:*; !!x. x:A ==> B(x):[] ] ==> Prod(A,B):[]"


103 
and lam_sb: "[ A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] ]


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


105 


106 
lemmas (in LP) rules = simple lam_sb pi_sb


107 

17260

108 

17252

109 
locale LP2 = LP + L2


110 


111 
lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb


112 

17260

113 

17252

114 
locale Lomega2 = L2 + Lomega


115 


116 
lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb


117 

17260

118 

17252

119 
locale LPomega = LP + Lomega


120 


121 
lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb


122 

17260

123 

17252

124 
locale CC = L2 + LP + Lomega


125 


126 
lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb


127 


128 
end
