author | ballarin |
Mon, 18 Apr 2005 09:25:23 +0200 | |
changeset 15763 | b901a127ac73 |
parent 15696 | 1da4ce092c0b |
child 15837 | 7a567dcd4cda |
permissions | -rw-r--r-- |
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 |
|
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
57 |
print_interps A |
15596 | 58 |
|
15696 | 59 |
(* possible accesses *) |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
60 |
thm p1.a.asm_A thm LocaleTest.p1.a.asm_A |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15696
diff
changeset
|
61 |
thm p1.asm_A thm LocaleTest.p1.asm_A |
15696 | 62 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
63 |
|
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
64 |
(* without prefix *) |
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 |
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
|
67 |
|
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
68 |
print_interps A |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
69 |
|
15696 | 70 |
(* possible accesses *) |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
71 |
thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A |
15696 | 72 |
|
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
73 |
|
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
74 |
interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute) |
15596 | 75 |
|
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
76 |
print_interps D |
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
77 |
|
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
78 |
thm p2.a.asm_A |
15696 | 79 |
|
15596 | 80 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
81 |
interpretation p3: D [X Y] . |
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
82 |
|
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
83 |
(* duplicate: not registered *) |
15696 | 84 |
|
85 |
(* thm p3.a.asm_A *) |
|
86 |
||
15596 | 87 |
|
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
88 |
print_interps A |
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
89 |
print_interps B |
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
90 |
print_interps C |
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
91 |
print_interps D |
15596 | 92 |
|
15696 | 93 |
(* not permitted |
94 |
||
95 |
interpretation p4: A ["?x::?'a1"] apply (rule A.intro) apply rule done |
|
96 |
||
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
97 |
print_interps A |
15696 | 98 |
*) |
15596 | 99 |
|
15696 | 100 |
interpretation p10: D + D a' b' d' [X Y _ U V _] by (auto intro: A.intro) |
101 |
||
102 |
corollary (in D) th_x: True .. |
|
103 |
||
104 |
(* possible accesses: for each registration *) |
|
105 |
||
106 |
thm p2.th_x thm p3.th_x thm p10.th_x |
|
107 |
||
108 |
lemma (in D) th_y: "d == (a = b)" . |
|
109 |
||
110 |
thm p2.th_y thm p3.th_y thm p10.th_y |
|
111 |
||
112 |
lemmas (in D) th_z = th_y |
|
113 |
||
114 |
thm p2.th_z |
|
115 |
||
116 |
thm asm_A |
|
117 |
||
118 |
section {* Interpretation in proof contexts *} |
|
15596 | 119 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
120 |
theorem True |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
121 |
proof - |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
122 |
fix alpha::i and beta::i and gamma::i |
15696 | 123 |
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
|
124 |
then interpret p5: A [alpha] . |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
125 |
print_interps A |
15696 | 126 |
thm p5.asm_A |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
127 |
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
|
128 |
print_interps A (* p6 not added! *) |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
129 |
print_interps C |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
130 |
qed rule |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
131 |
|
15696 | 132 |
theorem (in A) True |
133 |
proof - |
|
134 |
print_interps A |
|
135 |
fix beta and gamma |
|
136 |
interpret p9: D [a beta _] |
|
137 |
(* no proof obligation for A !!! *) |
|
138 |
apply - apply (rule refl) apply assumption done |
|
139 |
qed rule |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
140 |
|
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15598
diff
changeset
|
141 |
|
15696 | 142 |
(* Definition involving free variable *) |
143 |
||
144 |
ML {* reset show_sorts *} |
|
145 |
||
146 |
locale E = fixes e defines e_def: "e(x) == x & x" |
|
147 |
notes e_def2 = e_def |
|
148 |
||
149 |
lemma (in E) True thm e_def by fast |
|
150 |
||
151 |
interpretation p7: E ["(%x. x)"] by simp |
|
152 |
||
153 |
(* TODO: goal mustn't be beta-reduced here, is doesn't match meta-hyp *) |
|
154 |
||
155 |
thm p7.e_def2 |
|
156 |
||
157 |
locale E' = fixes e defines e_def: "e == (%x. x & x)" |
|
158 |
notes e_def2 = e_def |
|
159 |
||
160 |
interpretation p7': E' ["(%x. x)"] by simp |
|
161 |
||
162 |
thm p7'.e_def2 |
|
163 |
||
164 |
(* Definition involving free variable in assm *) |
|
165 |
||
166 |
locale (open) F = fixes f assumes asm_F: "f --> x" |
|
167 |
notes asm_F2 = asm_F |
|
168 |
||
169 |
interpretation p8: F ["False"] by fast |
|
170 |
||
171 |
thm p8.asm_F2 |
|
172 |
||
173 |
subsection {* Locale without assumptions *} |
|
174 |
||
175 |
locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]] |
|
176 |
||
177 |
lemma "[| P; Q |] ==> P & Q" |
|
178 |
proof - |
|
179 |
interpret my: L1 . txt {* No chained fact required. *} |
|
180 |
assume Q and P txt {* order reversed *} |
|
181 |
then show "P & Q" .. txt {* Applies @{thm my.rev_conjI}. *} |
|
182 |
qed |
|
183 |
||
184 |
locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]] |
|
185 |
||
186 |
lemma "[| P; Q |] ==> P & Q" |
|
187 |
proof - |
|
188 |
interpret [intro]: L11 . txt {* Attribute supplied at instantiation. *} |
|
189 |
assume Q and P |
|
190 |
then show "P & Q" .. |
|
191 |
qed |
|
192 |
||
193 |
subsection {* Simple locale with assumptions *} |
|
194 |
||
195 |
consts bin :: "[i, i] => i" (infixl "#" 60) |
|
196 |
||
197 |
axioms i_assoc: "(x # y) # z = x # (y # z)" |
|
198 |
i_comm: "x # y = y # x" |
|
199 |
||
200 |
locale L2 = |
|
201 |
fixes OP (infixl "+" 60) |
|
202 |
assumes assoc: "(x + y) + z = x + (y + z)" |
|
203 |
and comm: "x + y = y + x" |
|
204 |
||
205 |
lemma (in L2) lcomm: "x + (y + z) = y + (x + z)" |
|
206 |
proof - |
|
207 |
have "x + (y + z) = (x + y) + z" by (simp add: assoc) |
|
208 |
also have "... = (y + x) + z" by (simp add: comm) |
|
209 |
also have "... = y + (x + z)" by (simp add: assoc) |
|
210 |
finally show ?thesis . |
|
211 |
qed |
|
212 |
||
213 |
lemmas (in L2) AC = comm assoc lcomm |
|
214 |
||
215 |
lemma "(x::i) # y # z # w = y # x # w # z" |
|
216 |
proof - |
|
217 |
interpret my: L2 ["op #"] by (rule L2.intro [of "op #", OF i_assoc i_comm]) |
|
218 |
txt {* Chained fact required to discharge assumptions of @{text L2} |
|
219 |
and instantiate parameters. *} |
|
220 |
show ?thesis by (simp only: my.OP.AC) (* or simply AC *) |
|
221 |
qed |
|
222 |
||
223 |
subsection {* Nested locale with assumptions *} |
|
224 |
||
225 |
locale L3 = |
|
226 |
fixes OP (infixl "+" 60) |
|
227 |
assumes assoc: "(x + y) + z = x + (y + z)" |
|
228 |
||
229 |
locale L4 = L3 + |
|
230 |
assumes comm: "x + y = y + x" |
|
231 |
||
232 |
lemma (in L4) lcomm: "x + (y + z) = y + (x + z)" |
|
233 |
proof - |
|
234 |
have "x + (y + z) = (x + y) + z" by (simp add: assoc) |
|
235 |
also have "... = (y + x) + z" by (simp add: comm) |
|
236 |
also have "... = y + (x + z)" by (simp add: assoc) |
|
237 |
finally show ?thesis . |
|
238 |
qed |
|
239 |
||
240 |
lemmas (in L4) AC = comm assoc lcomm |
|
241 |
||
242 |
lemma "(x::i) # y # z # w = y # x # w # z" |
|
243 |
proof - |
|
244 |
interpret my: L4 ["op #"] |
|
245 |
by (auto intro: L3.intro L4_axioms.intro i_assoc i_comm) |
|
246 |
show ?thesis by (simp only: my.OP.AC) (* or simply AC *) |
|
247 |
qed |
|
248 |
||
249 |
subsection {* Locale with definition *} |
|
250 |
||
251 |
text {* This example is admittedly not very creative :-) *} |
|
252 |
||
253 |
locale L5 = L4 + var A + |
|
254 |
defines A_def: "A == True" |
|
255 |
||
256 |
lemma (in L5) lem: A |
|
257 |
by (unfold A_def) rule |
|
258 |
||
259 |
lemma "L5(op #) ==> True" |
|
260 |
proof - |
|
261 |
assume "L5(op #)" |
|
262 |
then interpret L5 ["op #"] by (auto intro: L5.axioms) |
|
263 |
show ?thesis by (rule lem) (* lem instantiated to True *) |
|
264 |
qed |
|
265 |
||
266 |
subsection {* Instantiation in a context with target *} |
|
267 |
||
268 |
lemma (in L4) |
|
269 |
fixes A (infixl "$" 60) |
|
270 |
assumes A: "L4(A)" |
|
271 |
shows "(x::i) $ y $ z $ w = y $ x $ w $ z" |
|
272 |
proof - |
|
273 |
from A interpret A: L4 ["A"] by (auto intro: L4.axioms) |
|
274 |
show ?thesis by (simp only: A.OP.AC) |
|
275 |
qed |
|
276 |
||
15596 | 277 |
end |