3773

1 

17252

2 
header {* Barendregt's LambdaCube *}


3 


4 
theory Cube


5 
imports Pure


6 
begin


7 


8 
typedecl "term"


9 
typedecl "context"


10 
typedecl typing


11 


12 
nonterminals


13 
context_ typing_


14 


15 
consts


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


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


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


19 
MT_context :: "context"


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


21 
star :: "term" ("*")


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


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


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


25 


26 
syntax


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


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


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


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


31 
MT_context :: "context_" ("")


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


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


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


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


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


37 


38 
translations

17260

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


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


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


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

17252

43 


44 
syntax (xsymbols)


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


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


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


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


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


50 


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


52 


53 
axioms


54 
s_b: "*: []"


55 


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


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


58 


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

0

60 

17252

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


62 


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


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


65 


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


67 


68 
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss


69 
lemmas rules = simple


70 


71 
lemma imp_elim:


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


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


74 


75 
lemma pi_elim:


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


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


78 


79 


80 
locale L2 =


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


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


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


84 


85 
lemmas (in L2) rules = simple lam_bs pi_bs


86 

17260

87 

17252

88 
locale Lomega =


89 
assumes


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


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


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


93 


94 
lemmas (in Lomega) rules = simple lam_bb pi_bb


95 


96 


97 
locale LP =


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


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


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


101 


102 
lemmas (in LP) rules = simple lam_sb pi_sb


103 

17260

104 

17252

105 
locale LP2 = LP + L2


106 


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


108 

17260

109 

17252

110 
locale Lomega2 = L2 + Lomega


111 


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


113 

17260

114 

17252

115 
locale LPomega = LP + Lomega


116 


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


118 

17260

119 

17252

120 
locale CC = L2 + LP + Lomega


121 


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


123 


124 
end
