1 (* Title: FOL/ex/NewLocaleTest.thy |
|
2 Author: Clemens Ballarin, TU Muenchen |
|
3 |
|
4 Testing environment for locale expressions --- experimental. |
|
5 *) |
|
6 |
|
7 theory NewLocaleTest |
|
8 imports NewLocaleSetup |
|
9 begin |
|
10 |
|
11 ML_val {* set Toplevel.debug *} |
|
12 |
|
13 |
|
14 typedecl int arities int :: "term" |
|
15 consts plus :: "int => int => int" (infixl "+" 60) |
|
16 zero :: int ("0") |
|
17 minus :: "int => int" ("- _") |
|
18 |
|
19 axioms |
|
20 int_assoc: "(x + y::int) + z = x + (y + z)" |
|
21 int_zero: "0 + x = x" |
|
22 int_minus: "(-x) + x = 0" |
|
23 int_minus2: "-(-x) = x" |
|
24 |
|
25 section {* Inference of parameter types *} |
|
26 |
|
27 locale param1 = fixes p |
|
28 print_locale! param1 |
|
29 |
|
30 locale param2 = fixes p :: 'b |
|
31 print_locale! param2 |
|
32 |
|
33 (* |
|
34 locale param_top = param2 r for r :: "'b :: {}" |
|
35 Fails, cannot generalise parameter. |
|
36 *) |
|
37 |
|
38 locale param3 = fixes p (infix ".." 50) |
|
39 print_locale! param3 |
|
40 |
|
41 locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50) |
|
42 print_locale! param4 |
|
43 |
|
44 |
|
45 subsection {* Incremental type constraints *} |
|
46 |
|
47 locale constraint1 = |
|
48 fixes prod (infixl "**" 65) |
|
49 assumes l_id: "x ** y = x" |
|
50 assumes assoc: "(x ** y) ** z = x ** (y ** z)" |
|
51 print_locale! constraint1 |
|
52 |
|
53 locale constraint2 = |
|
54 fixes p and q |
|
55 assumes "p = q" |
|
56 print_locale! constraint2 |
|
57 |
|
58 |
|
59 section {* Inheritance *} |
|
60 |
|
61 locale semi = |
|
62 fixes prod (infixl "**" 65) |
|
63 assumes assoc: "(x ** y) ** z = x ** (y ** z)" |
|
64 print_locale! semi thm semi_def |
|
65 |
|
66 locale lgrp = semi + |
|
67 fixes one and inv |
|
68 assumes lone: "one ** x = x" |
|
69 and linv: "inv(x) ** x = one" |
|
70 print_locale! lgrp thm lgrp_def lgrp_axioms_def |
|
71 |
|
72 locale add_lgrp = semi "op ++" for sum (infixl "++" 60) + |
|
73 fixes zero and neg |
|
74 assumes lzero: "zero ++ x = x" |
|
75 and lneg: "neg(x) ++ x = zero" |
|
76 print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def |
|
77 |
|
78 locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60) |
|
79 print_locale! rev_lgrp thm rev_lgrp_def |
|
80 |
|
81 locale hom = f: semi f + g: semi g for f and g |
|
82 print_locale! hom thm hom_def |
|
83 |
|
84 locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta |
|
85 print_locale! perturbation thm perturbation_def |
|
86 |
|
87 locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 |
|
88 print_locale! pert_hom thm pert_hom_def |
|
89 |
|
90 text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *} |
|
91 locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 |
|
92 print_locale! pert_hom' thm pert_hom'_def |
|
93 |
|
94 |
|
95 section {* Syntax declarations *} |
|
96 |
|
97 locale logic = |
|
98 fixes land (infixl "&&" 55) |
|
99 and lnot ("-- _" [60] 60) |
|
100 assumes assoc: "(x && y) && z = x && (y && z)" |
|
101 and notnot: "-- (-- x) = x" |
|
102 begin |
|
103 |
|
104 definition lor (infixl "||" 50) where |
|
105 "x || y = --(-- x && -- y)" |
|
106 |
|
107 end |
|
108 print_locale! logic |
|
109 |
|
110 locale use_decl = logic + semi "op ||" |
|
111 print_locale! use_decl thm use_decl_def |
|
112 |
|
113 locale extra_type = |
|
114 fixes a :: 'a |
|
115 and P :: "'a => 'b => o" |
|
116 begin |
|
117 |
|
118 definition test :: "'a => o" where |
|
119 "test(x) <-> (ALL b. P(x, b))" |
|
120 |
|
121 end |
|
122 |
|
123 term extra_type.test thm extra_type.test_def |
|
124 |
|
125 interpretation var: extra_type "0" "%x y. x = 0" . |
|
126 |
|
127 thm var.test_def |
|
128 |
|
129 |
|
130 section {* Foundational versions of theorems *} |
|
131 |
|
132 thm logic.assoc |
|
133 thm logic.lor_def |
|
134 |
|
135 |
|
136 section {* Defines *} |
|
137 |
|
138 locale logic_def = |
|
139 fixes land (infixl "&&" 55) |
|
140 and lor (infixl "||" 50) |
|
141 and lnot ("-- _" [60] 60) |
|
142 assumes assoc: "(x && y) && z = x && (y && z)" |
|
143 and notnot: "-- (-- x) = x" |
|
144 defines "x || y == --(-- x && -- y)" |
|
145 begin |
|
146 |
|
147 thm lor_def |
|
148 (* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *) |
|
149 |
|
150 lemma "x || y = --(-- x && --y)" |
|
151 by (unfold lor_def) (rule refl) |
|
152 |
|
153 end |
|
154 |
|
155 (* Inheritance of defines *) |
|
156 |
|
157 locale logic_def2 = logic_def |
|
158 begin |
|
159 |
|
160 lemma "x || y = --(-- x && --y)" |
|
161 by (unfold lor_def) (rule refl) |
|
162 |
|
163 end |
|
164 |
|
165 |
|
166 section {* Notes *} |
|
167 |
|
168 (* A somewhat arcane homomorphism example *) |
|
169 |
|
170 definition semi_hom where |
|
171 "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))" |
|
172 |
|
173 lemma semi_hom_mult: |
|
174 "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))" |
|
175 by (simp add: semi_hom_def) |
|
176 |
|
177 locale semi_hom_loc = prod: semi prod + sum: semi sum |
|
178 for prod and sum and h + |
|
179 assumes semi_homh: "semi_hom(prod, sum, h)" |
|
180 notes semi_hom_mult = semi_hom_mult [OF semi_homh] |
|
181 |
|
182 thm semi_hom_loc.semi_hom_mult |
|
183 (* unspecified, attribute not applied in backgroud theory !!! *) |
|
184 |
|
185 lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" |
|
186 by (rule semi_hom_mult) |
|
187 |
|
188 (* Referring to facts from within a context specification *) |
|
189 |
|
190 lemma |
|
191 assumes x: "P <-> P" |
|
192 notes y = x |
|
193 shows True .. |
|
194 |
|
195 |
|
196 section {* Theorem statements *} |
|
197 |
|
198 lemma (in lgrp) lcancel: |
|
199 "x ** y = x ** z <-> y = z" |
|
200 proof |
|
201 assume "x ** y = x ** z" |
|
202 then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc) |
|
203 then show "y = z" by (simp add: lone linv) |
|
204 qed simp |
|
205 print_locale! lgrp |
|
206 |
|
207 |
|
208 locale rgrp = semi + |
|
209 fixes one and inv |
|
210 assumes rone: "x ** one = x" |
|
211 and rinv: "x ** inv(x) = one" |
|
212 begin |
|
213 |
|
214 lemma rcancel: |
|
215 "y ** x = z ** x <-> y = z" |
|
216 proof |
|
217 assume "y ** x = z ** x" |
|
218 then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" |
|
219 by (simp add: assoc [symmetric]) |
|
220 then show "y = z" by (simp add: rone rinv) |
|
221 qed simp |
|
222 |
|
223 end |
|
224 print_locale! rgrp |
|
225 |
|
226 |
|
227 subsection {* Patterns *} |
|
228 |
|
229 lemma (in rgrp) |
|
230 assumes "y ** x = z ** x" (is ?a) |
|
231 shows "y = z" (is ?t) |
|
232 proof - |
|
233 txt {* Weird proof involving patterns from context element and conclusion. *} |
|
234 { |
|
235 assume ?a |
|
236 then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" |
|
237 by (simp add: assoc [symmetric]) |
|
238 then have ?t by (simp add: rone rinv) |
|
239 } |
|
240 note x = this |
|
241 show ?t by (rule x [OF `?a`]) |
|
242 qed |
|
243 |
|
244 |
|
245 section {* Interpretation between locales: sublocales *} |
|
246 |
|
247 sublocale lgrp < right: rgrp |
|
248 print_facts |
|
249 proof unfold_locales |
|
250 { |
|
251 fix x |
|
252 have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) |
|
253 then show "x ** one = x" by (simp add: assoc lcancel) |
|
254 } |
|
255 note rone = this |
|
256 { |
|
257 fix x |
|
258 have "inv(x) ** x ** inv(x) = inv(x) ** one" |
|
259 by (simp add: linv lone rone) |
|
260 then show "x ** inv(x) = one" by (simp add: assoc lcancel) |
|
261 } |
|
262 qed |
|
263 |
|
264 (* effect on printed locale *) |
|
265 |
|
266 print_locale! lgrp |
|
267 |
|
268 (* use of derived theorem *) |
|
269 |
|
270 lemma (in lgrp) |
|
271 "y ** x = z ** x <-> y = z" |
|
272 apply (rule rcancel) |
|
273 done |
|
274 |
|
275 (* circular interpretation *) |
|
276 |
|
277 sublocale rgrp < left: lgrp |
|
278 proof unfold_locales |
|
279 { |
|
280 fix x |
|
281 have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone) |
|
282 then show "one ** x = x" by (simp add: assoc [symmetric] rcancel) |
|
283 } |
|
284 note lone = this |
|
285 { |
|
286 fix x |
|
287 have "inv(x) ** (x ** inv(x)) = one ** inv(x)" |
|
288 by (simp add: rinv lone rone) |
|
289 then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel) |
|
290 } |
|
291 qed |
|
292 |
|
293 (* effect on printed locale *) |
|
294 |
|
295 print_locale! rgrp |
|
296 print_locale! lgrp |
|
297 |
|
298 |
|
299 (* Duality *) |
|
300 |
|
301 locale order = |
|
302 fixes less :: "'a => 'a => o" (infix "<<" 50) |
|
303 assumes refl: "x << x" |
|
304 and trans: "[| x << y; y << z |] ==> x << z" |
|
305 |
|
306 sublocale order < dual: order "%x y. y << x" |
|
307 apply unfold_locales apply (rule refl) apply (blast intro: trans) |
|
308 done |
|
309 |
|
310 print_locale! order (* Only two instances of order. *) |
|
311 |
|
312 locale order' = |
|
313 fixes less :: "'a => 'a => o" (infix "<<" 50) |
|
314 assumes refl: "x << x" |
|
315 and trans: "[| x << y; y << z |] ==> x << z" |
|
316 |
|
317 locale order_with_def = order' |
|
318 begin |
|
319 |
|
320 definition greater :: "'a => 'a => o" (infix ">>" 50) where |
|
321 "x >> y <-> y << x" |
|
322 |
|
323 end |
|
324 |
|
325 sublocale order_with_def < dual: order' "op >>" |
|
326 apply unfold_locales |
|
327 unfolding greater_def |
|
328 apply (rule refl) apply (blast intro: trans) |
|
329 done |
|
330 |
|
331 print_locale! order_with_def |
|
332 (* Note that decls come after theorems that make use of them. *) |
|
333 |
|
334 |
|
335 (* locale with many parameters --- |
|
336 interpretations generate alternating group A5 *) |
|
337 |
|
338 |
|
339 locale A5 = |
|
340 fixes A and B and C and D and E |
|
341 assumes eq: "A <-> B <-> C <-> D <-> E" |
|
342 |
|
343 sublocale A5 < 1: A5 _ _ D E C |
|
344 print_facts |
|
345 using eq apply (blast intro: A5.intro) done |
|
346 |
|
347 sublocale A5 < 2: A5 C _ E _ A |
|
348 print_facts |
|
349 using eq apply (blast intro: A5.intro) done |
|
350 |
|
351 sublocale A5 < 3: A5 B C A _ _ |
|
352 print_facts |
|
353 using eq apply (blast intro: A5.intro) done |
|
354 |
|
355 (* Any even permutation of parameters is subsumed by the above. *) |
|
356 |
|
357 print_locale! A5 |
|
358 |
|
359 |
|
360 (* Free arguments of instance *) |
|
361 |
|
362 locale trivial = |
|
363 fixes P and Q :: o |
|
364 assumes Q: "P <-> P <-> Q" |
|
365 begin |
|
366 |
|
367 lemma Q_triv: "Q" using Q by fast |
|
368 |
|
369 end |
|
370 |
|
371 sublocale trivial < x: trivial x _ |
|
372 apply unfold_locales using Q by fast |
|
373 |
|
374 print_locale! trivial |
|
375 |
|
376 context trivial begin thm x.Q [where ?x = True] end |
|
377 |
|
378 sublocale trivial < y: trivial Q Q |
|
379 by unfold_locales |
|
380 (* Succeeds since previous interpretation is more general. *) |
|
381 |
|
382 print_locale! trivial (* No instance for y created (subsumed). *) |
|
383 |
|
384 |
|
385 subsection {* Sublocale, then interpretation in theory *} |
|
386 |
|
387 interpretation int: lgrp "op +" "0" "minus" |
|
388 proof unfold_locales |
|
389 qed (rule int_assoc int_zero int_minus)+ |
|
390 |
|
391 thm int.assoc int.semi_axioms |
|
392 |
|
393 interpretation int2: semi "op +" |
|
394 by unfold_locales (* subsumed, thm int2.assoc not generated *) |
|
395 |
|
396 thm int.lone int.right.rone |
|
397 (* the latter comes through the sublocale relation *) |
|
398 |
|
399 |
|
400 subsection {* Interpretation in theory, then sublocale *} |
|
401 |
|
402 interpretation (* fol: *) logic "op +" "minus" |
|
403 (* FIXME declaration of qualified names *) |
|
404 by unfold_locales (rule int_assoc int_minus2)+ |
|
405 |
|
406 locale logic2 = |
|
407 fixes land (infixl "&&" 55) |
|
408 and lnot ("-- _" [60] 60) |
|
409 assumes assoc: "(x && y) && z = x && (y && z)" |
|
410 and notnot: "-- (-- x) = x" |
|
411 begin |
|
412 |
|
413 (* FIXME interpretation below fails |
|
414 definition lor (infixl "||" 50) where |
|
415 "x || y = --(-- x && -- y)" |
|
416 *) |
|
417 |
|
418 end |
|
419 |
|
420 sublocale logic < two: logic2 |
|
421 by unfold_locales (rule assoc notnot)+ |
|
422 |
|
423 thm two.assoc |
|
424 |
|
425 |
|
426 subsection {* Declarations and sublocale *} |
|
427 |
|
428 locale logic_a = logic |
|
429 locale logic_b = logic |
|
430 |
|
431 sublocale logic_a < logic_b |
|
432 by unfold_locales |
|
433 |
|
434 |
|
435 subsection {* Equations *} |
|
436 |
|
437 locale logic_o = |
|
438 fixes land (infixl "&&" 55) |
|
439 and lnot ("-- _" [60] 60) |
|
440 assumes assoc_o: "(x && y) && z <-> x && (y && z)" |
|
441 and notnot_o: "-- (-- x) <-> x" |
|
442 begin |
|
443 |
|
444 definition lor_o (infixl "||" 50) where |
|
445 "x || y <-> --(-- x && -- y)" |
|
446 |
|
447 end |
|
448 |
|
449 interpretation x!: logic_o "op &" "Not" |
|
450 where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y" |
|
451 proof - |
|
452 show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+ |
|
453 show "logic_o.lor_o(op &, Not, x, y) <-> x | y" |
|
454 by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast |
|
455 qed |
|
456 |
|
457 thm x.lor_o_def bool_logic_o |
|
458 |
|
459 lemma lor_triv: "z <-> z" .. |
|
460 |
|
461 lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast |
|
462 |
|
463 thm lor_triv [where z = True] (* Check strict prefix. *) |
|
464 x.lor_triv |
|
465 |
|
466 |
|
467 subsection {* Interpretation in proofs *} |
|
468 |
|
469 lemma True |
|
470 proof |
|
471 interpret "local": lgrp "op +" "0" "minus" |
|
472 by unfold_locales (* subsumed *) |
|
473 { |
|
474 fix zero :: int |
|
475 assume "!!x. zero + x = x" "!!x. (-x) + x = zero" |
|
476 then interpret local_fixed: lgrp "op +" zero "minus" |
|
477 by unfold_locales |
|
478 thm local_fixed.lone |
|
479 } |
|
480 assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero" |
|
481 then interpret local_free: lgrp "op +" zero "minus" for zero |
|
482 by unfold_locales |
|
483 thm local_free.lone [where ?zero = 0] |
|
484 qed |
|
485 |
|
486 end |
|