author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45242  401f91ed8a93 
child 49752  2bbb0013ff82 
permissions  rwrr 
22809  1 
(* Title: Cube/Cube.thy 
2 
Author: Tobias Nipkow 

3 
*) 

3773  4 

17252  5 
header {* Barendregt's LambdaCube *} 
6 

7 
theory Cube 

8 
imports Pure 

9 
begin 

10 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
35256
diff
changeset

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

12 

17252  13 
typedecl "term" 
14 
typedecl "context" 

15 
typedecl typing 

16 

45241  17 
axiomatization 
18 
Abs :: "[term, term => term] => term" and 

19 
Prod :: "[term, term => term] => term" and 

20 
Trueprop :: "[context, typing] => prop" and 

21 
MT_context :: "context" and 

22 
Context :: "[typing, context] => context" and 

23 
star :: "term" ("*") and 

45242  24 
box :: "term" ("\<box>") and 
45241  25 
app :: "[term, term] => term" (infixl "^" 20) and 
26 
Has_type :: "[term, term] => typing" 

17252  27 

45241  28 
nonterminal context' and typing' 
17252  29 

30 
syntax 

45242  31 
"_Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)") 
45241  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) 

45242  38 
"_Lam" :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10) 
39 
"_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) 

40 
"_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10) 

17252  41 

42 
translations 

45241  43 
"_Trueprop(G, t)" == "CONST Trueprop(G, t)" 
45242  44 
("prop") "x:X" == ("prop") "\<turnstile> x:X" 
45241  45 
"_MT_context" == "CONST MT_context" 
46 
"_Context" == "CONST Context" 

47 
"_Has_type" == "CONST Has_type" 

45242  48 
"\<Lambda> x:A. B" == "CONST Abs(A, %x. B)" 
49 
"\<Pi> x:A. B" => "CONST Prod(A, %x. B)" 

50 
"A \<rightarrow> B" => "CONST Prod(A, %_. B)" 

17252  51 

52 
syntax (xsymbols) 

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

35113  55 
print_translation {* 
42284  56 
[(@{const_syntax Prod}, 
57 
Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] 

35113  58 
*} 
17252  59 

45241  60 
axiomatization where 
45242  61 
s_b: "*: \<box>" and 
17252  62 

45242  63 
strip_s: "[ A:*; a:A ==> G \<turnstile> x:X ] ==> a:A G \<turnstile> x:X" and 
64 
strip_b: "[ A:\<box>; a:A ==> G \<turnstile> x:X ] ==> a:A G \<turnstile> x:X" and 

17252  65 

45241  66 
app: "[ F:Prod(A, B); C:A ] ==> F^C: B(C)" and 
0  67 

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

45241  70 
lam_ss: "[ A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* ] 
71 
==> Abs(A, f) : Prod(A, B)" and 

17252  72 

45241  73 
beta: "Abs(A, f)^a == f(a)" 
17252  74 

75 
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss 

76 
lemmas rules = simple 

77 

78 
lemma imp_elim: 

45242  79 
assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B ==> PROP P" 
41526  80 
shows "PROP P" by (rule app assms)+ 
17252  81 

82 
lemma pi_elim: 

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

41526  84 
shows "PROP P" by (rule app assms)+ 
17252  85 

86 

87 
locale L2 = 

45242  88 
assumes pi_bs: "[ A:\<box>; !!x. x:A ==> B(x):* ] ==> Prod(A,B):*" 
89 
and lam_bs: "[ A:\<box>; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* ] 

17252  90 
==> Abs(A,f) : Prod(A,B)" 
45242  91 
begin 
17252  92 

45242  93 
lemmas rules = simple lam_bs pi_bs 
94 

95 
end 

17252  96 

17260  97 

17252  98 
locale Lomega = 
99 
assumes 

45242  100 
pi_bb: "[ A:\<box>; !!x. x:A ==> B(x):\<box> ] ==> Prod(A,B):\<box>" 
101 
and lam_bb: "[ A:\<box>; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):\<box> ] 

17252  102 
==> Abs(A,f) : Prod(A,B)" 
45242  103 
begin 
17252  104 

45242  105 
lemmas rules = simple lam_bb pi_bb 
106 

107 
end 

17252  108 

109 

110 
locale LP = 

45242  111 
assumes pi_sb: "[ A:*; !!x. x:A ==> B(x):\<box> ] ==> Prod(A,B):\<box>" 
112 
and lam_sb: "[ A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):\<box> ] 

17252  113 
==> Abs(A,f) : Prod(A,B)" 
45241  114 
begin 
17252  115 

45241  116 
lemmas rules = simple lam_sb pi_sb 
117 

118 
end 

17252  119 

17260  120 

17252  121 
locale LP2 = LP + L2 
45241  122 
begin 
17252  123 

45241  124 
lemmas rules = simple lam_bs pi_bs lam_sb pi_sb 
125 

126 
end 

17252  127 

17260  128 

17252  129 
locale Lomega2 = L2 + Lomega 
45241  130 
begin 
17252  131 

45241  132 
lemmas rules = simple lam_bs pi_bs lam_bb pi_bb 
133 

134 
end 

17252  135 

17260  136 

17252  137 
locale LPomega = LP + Lomega 
45241  138 
begin 
17252  139 

45241  140 
lemmas rules = simple lam_bb pi_bb lam_sb pi_sb 
141 

142 
end 

17252  143 

17260  144 

17252  145 
locale CC = L2 + LP + Lomega 
45241  146 
begin 
17252  147 

45241  148 
lemmas rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb 
17252  149 

150 
end 

45241  151 

152 
end 