author  wenzelm 
Sat, 22 Oct 2011 16:44:34 +0200  
changeset 45241  87950f752099 
parent 42284  326f57825e1a 
child 45242  401f91ed8a93 
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 

24 
box :: "term" ("[]") and 

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

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

17252  27 

45241  28 
notation (xsymbols) 
29 
box ("\<box>") 

30 

31 
nonterminal context' and typing' 

17252  32 

33 
syntax 

45241  34 
"_Trueprop" :: "[context', typing'] => prop" ("(_/  _)") 
35 
"_Trueprop1" :: "typing' => prop" ("(_)") 

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

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

38 
"_MT_context" :: "context'" ("") 

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

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

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

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

43 
"_arrow" :: "[term, term] => term" (infixr ">" 10) 

17252  44 

45 
translations 

45241  46 
"_Trueprop(G, t)" == "CONST Trueprop(G, t)" 
17260  47 
("prop") "x:X" == ("prop") " x:X" 
45241  48 
"_MT_context" == "CONST MT_context" 
49 
"_Context" == "CONST Context" 

50 
"_Has_type" == "CONST Has_type" 

35256  51 
"Lam x:A. B" == "CONST Abs(A, %x. B)" 
52 
"Pi x:A. B" => "CONST Prod(A, %x. B)" 

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

17252  54 

55 
syntax (xsymbols) 

45241  56 
"_Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)") 
35256  57 
"_Lam" :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10) 
58 
"_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) 

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

17252  60 

35113  61 
print_translation {* 
42284  62 
[(@{const_syntax Prod}, 
63 
Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] 

35113  64 
*} 
17252  65 

45241  66 
axiomatization where 
67 
s_b: "*: []" and 

17252  68 

45241  69 
strip_s: "[ A:*; a:A ==> G  x:X ] ==> a:A G  x:X" and 
70 
strip_b: "[ A:[]; a:A ==> G  x:X ] ==> a:A G  x:X" and 

17252  71 

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

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

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

17252  78 

45241  79 
beta: "Abs(A, f)^a == f(a)" 
17252  80 

81 
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss 

82 
lemmas rules = simple 

83 

84 
lemma imp_elim: 

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

41526  86 
shows "PROP P" by (rule app assms)+ 
17252  87 

88 
lemma pi_elim: 

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

41526  90 
shows "PROP P" by (rule app assms)+ 
17252  91 

92 

93 
locale L2 = 

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

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

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

97 

98 
lemmas (in L2) rules = simple lam_bs pi_bs 

99 

17260  100 

17252  101 
locale Lomega = 
102 
assumes 

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

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

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

106 

107 
lemmas (in Lomega) rules = simple lam_bb pi_bb 

108 

109 

110 
locale LP = 

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

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

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 