author  ballarin 
Mon, 11 Apr 2005 12:34:34 +0200  
changeset 15696  1da4ce092c0b 
parent 15624  484178635bd8 
child 15763  b901a127ac73 
permissions  rwrr 
15596  1 
(* Title: FOL/ex/LocaleTest.thy 
2 
ID: $Id$ 

3 
Author: Clemens Ballarin 

4 
Copyright (c) 2005 by Clemens Ballarin 

5 

6 
Collection of regression tests for locales. 

7 
*) 

8 

9 
header {* Test of Locale instantiation *} 

10 

11 
theory LocaleTest = FOL: 

12 

15696  13 
ML {* set quick_and_dirty *} (* allow for thm command in batch mode *) 
14 
ML {* set Toplevel.debug *} 

15 
ML {* set show_hyps *} 

16 
ML {* set show_sorts *} 

17 

18 
section {* interpretation *} 

19 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

20 
(* interpretation input syntax *) 
15596  21 

22 
locale L 

23 
locale M = fixes a and b and c 

24 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

25 
interpretation test [simp]: L + M a b c [x y z] . 
15596  26 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

27 
print_interps L 
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

28 
print_interps M 
15596  29 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

30 
interpretation test [simp]: L print_interps M . 
15596  31 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

32 
interpretation L . 
15596  33 

34 
(* processing of locale expression *) 

35 

36 
locale A = fixes a assumes asm_A: "a = a" 

37 

38 
locale (open) B = fixes b assumes asm_B [simp]: "b = b" 

39 

40 
locale C = A + B + assumes asm_C: "c = c" 

41 
(* TODO: independent type var in c, prohibit locale declaration *) 

42 

43 
locale D = A + B + fixes d defines def_D: "d == (a = b)" 

44 

15696  45 
theorem (in A) 
46 
includes D 

47 
shows True .. 

48 

49 
theorem (in D) True .. 

15596  50 

51 
typedecl i 

52 
arities i :: "term" 

53 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

54 

4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

55 
interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro) 
15596  56 
(* both X and Y get type 'b since 'b is the internal type of parameter b, 
57 
not wanted, but put up with for now. *) 

58 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

59 
print_interps A 
15596  60 

15696  61 
(* possible accesses *) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

62 
thm p1.a.asm_A thm LocaleTest.p1.a.asm_A 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

63 
thm LocaleTest.asm_A thm p1.asm_A 
15696  64 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

65 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

66 
(* without prefix *) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

67 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

68 
interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

69 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

70 
print_interps A 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

71 

15696  72 
(* possible accesses *) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

73 
thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A 
15696  74 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

75 

4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

76 
interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute) 
15596  77 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

78 
print_interps D 
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

79 

4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

80 
thm p2.a.asm_A 
15696  81 

15596  82 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

83 
interpretation p3: D [X Y] . 
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

84 

4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

85 
(* duplicate: not registered *) 
15696  86 

87 
(* thm p3.a.asm_A *) 

88 

15596  89 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

90 
print_interps A 
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

91 
print_interps B 
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

92 
print_interps C 
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

93 
print_interps D 
15596  94 

15696  95 
(* not permitted 
96 

97 
interpretation p4: A ["?x::?'a1"] apply (rule A.intro) apply rule done 

98 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

99 
print_interps A 
15696  100 
*) 
15596  101 

15696  102 
interpretation p10: D + D a' b' d' [X Y _ U V _] by (auto intro: A.intro) 
103 

104 
corollary (in D) th_x: True .. 

105 

106 
(* possible accesses: for each registration *) 

107 

108 
thm p2.th_x thm p3.th_x thm p10.th_x 

109 

110 
lemma (in D) th_y: "d == (a = b)" . 

111 

112 
thm p2.th_y thm p3.th_y thm p10.th_y 

113 

114 
lemmas (in D) th_z = th_y 

115 

116 
thm p2.th_z 

117 

118 
thm asm_A 

119 

120 
section {* Interpretation in proof contexts *} 

15596  121 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

122 
theorem True 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

123 
proof  
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

124 
fix alpha::i and beta::i and gamma::i 
15696  125 
have alpha_A: "A(alpha)" by (auto intro: A.intro) 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

126 
then interpret p5: A [alpha] . 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

127 
print_interps A 
15696  128 
thm p5.asm_A 
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

129 
interpret p6: C [alpha beta] by (auto intro: C_axioms.intro) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

130 
print_interps A (* p6 not added! *) 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

131 
print_interps C 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

132 
qed rule 
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

133 

15696  134 
theorem (in A) True 
135 
proof  

136 
print_interps A 

137 
fix beta and gamma 

138 
interpret p9: D [a beta _] 

139 
(* no proof obligation for A !!! *) 

140 
apply  apply (rule refl) apply assumption done 

141 
qed rule 

15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

142 

484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset

143 

15696  144 
(* Definition involving free variable *) 
145 

146 
ML {* reset show_sorts *} 

147 

148 
locale E = fixes e defines e_def: "e(x) == x & x" 

149 
notes e_def2 = e_def 

150 

151 
lemma (in E) True thm e_def by fast 

152 

153 
interpretation p7: E ["(%x. x)"] by simp 

154 

155 
(* TODO: goal mustn't be betareduced here, is doesn't match metahyp *) 

156 

157 
thm p7.e_def2 

158 

159 
locale E' = fixes e defines e_def: "e == (%x. x & x)" 

160 
notes e_def2 = e_def 

161 

162 
interpretation p7': E' ["(%x. x)"] by simp 

163 

164 
thm p7'.e_def2 

165 

166 
(* Definition involving free variable in assm *) 

167 

168 
locale (open) F = fixes f assumes asm_F: "f > x" 

169 
notes asm_F2 = asm_F 

170 

171 
interpretation p8: F ["False"] by fast 

172 

173 
thm p8.asm_F2 

174 

175 
subsection {* Locale without assumptions *} 

176 

177 
locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]] 

178 

179 
lemma "[ P; Q ] ==> P & Q" 

180 
proof  

181 
interpret my: L1 . txt {* No chained fact required. *} 

182 
assume Q and P txt {* order reversed *} 

183 
then show "P & Q" .. txt {* Applies @{thm my.rev_conjI}. *} 

184 
qed 

185 

186 
locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]] 

187 

188 
lemma "[ P; Q ] ==> P & Q" 

189 
proof  

190 
interpret [intro]: L11 . txt {* Attribute supplied at instantiation. *} 

191 
assume Q and P 

192 
then show "P & Q" .. 

193 
qed 

194 

195 
subsection {* Simple locale with assumptions *} 

196 

197 
consts bin :: "[i, i] => i" (infixl "#" 60) 

198 

199 
axioms i_assoc: "(x # y) # z = x # (y # z)" 

200 
i_comm: "x # y = y # x" 

201 

202 
locale L2 = 

203 
fixes OP (infixl "+" 60) 

204 
assumes assoc: "(x + y) + z = x + (y + z)" 

205 
and comm: "x + y = y + x" 

206 

207 
lemma (in L2) lcomm: "x + (y + z) = y + (x + z)" 

208 
proof  

209 
have "x + (y + z) = (x + y) + z" by (simp add: assoc) 

210 
also have "... = (y + x) + z" by (simp add: comm) 

211 
also have "... = y + (x + z)" by (simp add: assoc) 

212 
finally show ?thesis . 

213 
qed 

214 

215 
lemmas (in L2) AC = comm assoc lcomm 

216 

217 
lemma "(x::i) # y # z # w = y # x # w # z" 

218 
proof  

219 
interpret my: L2 ["op #"] by (rule L2.intro [of "op #", OF i_assoc i_comm]) 

220 
txt {* Chained fact required to discharge assumptions of @{text L2} 

221 
and instantiate parameters. *} 

222 
show ?thesis by (simp only: my.OP.AC) (* or simply AC *) 

223 
qed 

224 

225 
subsection {* Nested locale with assumptions *} 

226 

227 
locale L3 = 

228 
fixes OP (infixl "+" 60) 

229 
assumes assoc: "(x + y) + z = x + (y + z)" 

230 

231 
locale L4 = L3 + 

232 
assumes comm: "x + y = y + x" 

233 

234 
lemma (in L4) lcomm: "x + (y + z) = y + (x + z)" 

235 
proof  

236 
have "x + (y + z) = (x + y) + z" by (simp add: assoc) 

237 
also have "... = (y + x) + z" by (simp add: comm) 

238 
also have "... = y + (x + z)" by (simp add: assoc) 

239 
finally show ?thesis . 

240 
qed 

241 

242 
lemmas (in L4) AC = comm assoc lcomm 

243 

244 
lemma "(x::i) # y # z # w = y # x # w # z" 

245 
proof  

246 
interpret my: L4 ["op #"] 

247 
by (auto intro: L3.intro L4_axioms.intro i_assoc i_comm) 

248 
show ?thesis by (simp only: my.OP.AC) (* or simply AC *) 

249 
qed 

250 

251 
subsection {* Locale with definition *} 

252 

253 
text {* This example is admittedly not very creative :) *} 

254 

255 
locale L5 = L4 + var A + 

256 
defines A_def: "A == True" 

257 

258 
lemma (in L5) lem: A 

259 
by (unfold A_def) rule 

260 

261 
lemma "L5(op #) ==> True" 

262 
proof  

263 
assume "L5(op #)" 

264 
then interpret L5 ["op #"] by (auto intro: L5.axioms) 

265 
show ?thesis by (rule lem) (* lem instantiated to True *) 

266 
qed 

267 

268 
subsection {* Instantiation in a context with target *} 

269 

270 
lemma (in L4) 

271 
fixes A (infixl "$" 60) 

272 
assumes A: "L4(A)" 

273 
shows "(x::i) $ y $ z $ w = y $ x $ w $ z" 

274 
proof  

275 
from A interpret A: L4 ["A"] by (auto intro: L4.axioms) 

276 
show ?thesis by (simp only: A.OP.AC) 

277 
qed 

278 

15596  279 
end 