author  wenzelm 
Wed, 10 Oct 2012 15:01:20 +0200  
changeset 49752  2bbb0013ff82 
parent 45242  401f91ed8a93 
child 52143  36ffe23b25f8 
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 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

13 
ML {* 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

14 
structure Rules = Named_Thms 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

15 
( 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

16 
val name = @{binding rules} 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

17 
val description = "Cube inference rules" 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

18 
) 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

19 
*} 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

20 
setup Rules.setup 
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

21 

17252  22 
typedecl "term" 
23 
typedecl "context" 

24 
typedecl typing 

25 

45241  26 
axiomatization 
27 
Abs :: "[term, term => term] => term" and 

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

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

30 
MT_context :: "context" and 

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

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

45242  33 
box :: "term" ("\<box>") and 
45241  34 
app :: "[term, term] => term" (infixl "^" 20) and 
35 
Has_type :: "[term, term] => typing" 

17252  36 

45241  37 
nonterminal context' and typing' 
17252  38 

39 
syntax 

45242  40 
"_Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)") 
45241  41 
"_Trueprop1" :: "typing' => prop" ("(_)") 
42 
"" :: "id => context'" ("_") 

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

44 
"_MT_context" :: "context'" ("") 

45 
"_Context" :: "[typing', context'] => context'" ("_ _") 

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

45242  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) 

17252  50 

51 
translations 

45241  52 
"_Trueprop(G, t)" == "CONST Trueprop(G, t)" 
45242  53 
("prop") "x:X" == ("prop") "\<turnstile> x:X" 
45241  54 
"_MT_context" == "CONST MT_context" 
55 
"_Context" == "CONST Context" 

56 
"_Has_type" == "CONST Has_type" 

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

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

17252  60 

61 
syntax (xsymbols) 

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

35113  64 
print_translation {* 
42284  65 
[(@{const_syntax Prod}, 
66 
Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] 

35113  67 
*} 
17252  68 

45241  69 
axiomatization where 
45242  70 
s_b: "*: \<box>" and 
17252  71 

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

17252  74 

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

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

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

17252  81 

45241  82 
beta: "Abs(A, f)^a == f(a)" 
17252  83 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

84 
lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss 
17252  85 

86 
lemma imp_elim: 

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

90 
lemma pi_elim: 

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

41526  92 
shows "PROP P" by (rule app assms)+ 
17252  93 

94 

95 
locale L2 = 

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

17252  98 
==> Abs(A,f) : Prod(A,B)" 
45242  99 
begin 
17252  100 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

101 
lemmas [rules] = lam_bs pi_bs 
45242  102 

103 
end 

17252  104 

17260  105 

17252  106 
locale Lomega = 
107 
assumes 

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

17252  110 
==> Abs(A,f) : Prod(A,B)" 
45242  111 
begin 
17252  112 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

113 
lemmas [rules] = lam_bb pi_bb 
45242  114 

115 
end 

17252  116 

117 

118 
locale LP = 

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

17252  121 
==> Abs(A,f) : Prod(A,B)" 
45241  122 
begin 
17252  123 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

124 
lemmas [rules] = lam_sb pi_sb 
45241  125 

126 
end 

17252  127 

17260  128 

17252  129 
locale LP2 = LP + L2 
45241  130 
begin 
17252  131 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

132 
lemmas [rules] = lam_bs pi_bs lam_sb pi_sb 
45241  133 

134 
end 

17252  135 

17260  136 

17252  137 
locale Lomega2 = L2 + Lomega 
45241  138 
begin 
17252  139 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

140 
lemmas [rules] = lam_bs pi_bs lam_bb pi_bb 
45241  141 

142 
end 

17252  143 

17260  144 

17252  145 
locale LPomega = LP + Lomega 
45241  146 
begin 
17252  147 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

148 
lemmas [rules] = lam_bb pi_bb lam_sb pi_sb 
45241  149 

150 
end 

17252  151 

17260  152 

17252  153 
locale CC = L2 + LP + Lomega 
45241  154 
begin 
17252  155 

49752
2bbb0013ff82
modernized dynamic "rules"  avoid rebinding of static facts;
wenzelm
parents:
45242
diff
changeset

156 
lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb 
17252  157 

158 
end 

45241  159 

160 
end 