author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 26956  1309a6a0a29f 
child 35054  a5db9779b026 
permissions  rwrr 
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 

26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
24783
diff
changeset

12 
setup PureThy.old_appl_syntax_setup 
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
24783
diff
changeset

13 

17252  14 
typedecl "term" 
15 
typedecl "context" 

16 
typedecl typing 

17 

18 
nonterminals 

24783  19 
context' typing' 
17252  20 

21 
consts 

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

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

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

25 
MT_context :: "context" 

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

27 
star :: "term" ("*") 

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

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

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

31 

32 
syntax 

24783  33 
Trueprop :: "[context', typing'] => prop" ("(_/  _)") 
34 
Trueprop1 :: "typing' => prop" ("(_)") 

35 
"" :: "id => context'" ("_") 

36 
"" :: "var => context'" ("_") 

37 
MT_context :: "context'" ("") 

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

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

17252  40 
Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) 
41 
Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) 

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

43 

44 
translations 

17260  45 
("prop") "x:X" == ("prop") " x:X" 
46 
"Lam x:A. B" == "Abs(A, %x. B)" 

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

17782  48 
"A > B" => "Prod(A, %_. B)" 
17252  49 

50 
syntax (xsymbols) 

24783  51 
Trueprop :: "[context', typing'] => prop" ("(_/ \<turnstile> _)") 
17252  52 
box :: "term" ("\<box>") 
53 
Lam :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10) 

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

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

56 

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

58 

59 
axioms 

60 
s_b: "*: []" 

61 

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

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

64 

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

0  66 

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

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

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

71 

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

73 

74 
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss 

75 
lemmas rules = simple 

76 

77 
lemma imp_elim: 

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

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

80 

81 
lemma pi_elim: 

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

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

84 

85 

86 
locale L2 = 

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

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

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

90 

91 
lemmas (in L2) rules = simple lam_bs pi_bs 

92 

17260  93 

17252  94 
locale Lomega = 
95 
assumes 

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

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

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

99 

100 
lemmas (in Lomega) rules = simple lam_bb pi_bb 

101 

102 

103 
locale LP = 

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

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

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

107 

108 
lemmas (in LP) rules = simple lam_sb pi_sb 

109 

17260  110 

17252  111 
locale LP2 = LP + L2 
112 

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

114 

17260  115 

17252  116 
locale Lomega2 = L2 + Lomega 
117 

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

119 

17260  120 

17252  121 
locale LPomega = LP + Lomega 
122 

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

124 

17260  125 

17252  126 
locale CC = L2 + LP + Lomega 
127 

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

129 

130 
end 