author | wenzelm |
Mon, 19 Oct 2015 20:29:29 +0200 | |
changeset 61487 | f8cb97e0fd0b |
parent 61268 | abe08fb15a12 |
child 61489 | b8d375aee0df |
permissions | -rw-r--r-- |
37134 | 1 |
(* Title: FOL/ex/Locale_Test/Locale_Test1.thy |
2 |
Author: Clemens Ballarin, TU Muenchen |
|
3 |
||
4 |
Test environment for the locale implementation. |
|
5 |
*) |
|
6 |
||
7 |
theory Locale_Test1 |
|
8 |
imports FOL |
|
9 |
begin |
|
10 |
||
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
53367
diff
changeset
|
11 |
typedecl int |
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
53367
diff
changeset
|
12 |
instance int :: "term" .. |
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
53367
diff
changeset
|
13 |
|
37134 | 14 |
consts plus :: "int => int => int" (infixl "+" 60) |
15 |
zero :: int ("0") |
|
16 |
minus :: "int => int" ("- _") |
|
17 |
||
41779 | 18 |
axiomatization where |
19 |
int_assoc: "(x + y::int) + z = x + (y + z)" and |
|
20 |
int_zero: "0 + x = x" and |
|
21 |
int_minus: "(-x) + x = 0" and |
|
37134 | 22 |
int_minus2: "-(-x) = x" |
23 |
||
60770 | 24 |
section \<open>Inference of parameter types\<close> |
37134 | 25 |
|
26 |
locale param1 = fixes p |
|
27 |
print_locale! param1 |
|
28 |
||
29 |
locale param2 = fixes p :: 'b |
|
30 |
print_locale! param2 |
|
31 |
||
32 |
(* |
|
33 |
locale param_top = param2 r for r :: "'b :: {}" |
|
34 |
Fails, cannot generalise parameter. |
|
35 |
*) |
|
36 |
||
37 |
locale param3 = fixes p (infix ".." 50) |
|
38 |
print_locale! param3 |
|
39 |
||
40 |
locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50) |
|
41 |
print_locale! param4 |
|
42 |
||
43 |
||
60770 | 44 |
subsection \<open>Incremental type constraints\<close> |
37134 | 45 |
|
46 |
locale constraint1 = |
|
47 |
fixes prod (infixl "**" 65) |
|
48 |
assumes l_id: "x ** y = x" |
|
49 |
assumes assoc: "(x ** y) ** z = x ** (y ** z)" |
|
50 |
print_locale! constraint1 |
|
51 |
||
52 |
locale constraint2 = |
|
53 |
fixes p and q |
|
54 |
assumes "p = q" |
|
55 |
print_locale! constraint2 |
|
56 |
||
57 |
||
60770 | 58 |
section \<open>Inheritance\<close> |
37134 | 59 |
|
60 |
locale semi = |
|
61 |
fixes prod (infixl "**" 65) |
|
62 |
assumes assoc: "(x ** y) ** z = x ** (y ** z)" |
|
63 |
print_locale! semi thm semi_def |
|
64 |
||
65 |
locale lgrp = semi + |
|
66 |
fixes one and inv |
|
67 |
assumes lone: "one ** x = x" |
|
68 |
and linv: "inv(x) ** x = one" |
|
69 |
print_locale! lgrp thm lgrp_def lgrp_axioms_def |
|
70 |
||
71 |
locale add_lgrp = semi "op ++" for sum (infixl "++" 60) + |
|
72 |
fixes zero and neg |
|
73 |
assumes lzero: "zero ++ x = x" |
|
74 |
and lneg: "neg(x) ++ x = zero" |
|
75 |
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def |
|
76 |
||
77 |
locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60) |
|
78 |
print_locale! rev_lgrp thm rev_lgrp_def |
|
79 |
||
80 |
locale hom = f: semi f + g: semi g for f and g |
|
81 |
print_locale! hom thm hom_def |
|
82 |
||
83 |
locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta |
|
84 |
print_locale! perturbation thm perturbation_def |
|
85 |
||
86 |
locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 |
|
87 |
print_locale! pert_hom thm pert_hom_def |
|
88 |
||
60770 | 89 |
text \<open>Alternative expression, obtaining nicer names in @{text "semi f"}.\<close> |
37134 | 90 |
locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 |
91 |
print_locale! pert_hom' thm pert_hom'_def |
|
92 |
||
93 |
||
60770 | 94 |
section \<open>Syntax declarations\<close> |
37134 | 95 |
|
96 |
locale logic = |
|
97 |
fixes land (infixl "&&" 55) |
|
98 |
and lnot ("-- _" [60] 60) |
|
99 |
assumes assoc: "(x && y) && z = x && (y && z)" |
|
100 |
and notnot: "-- (-- x) = x" |
|
101 |
begin |
|
102 |
||
103 |
definition lor (infixl "||" 50) where |
|
104 |
"x || y = --(-- x && -- y)" |
|
105 |
||
106 |
end |
|
107 |
print_locale! logic |
|
108 |
||
49756
28e37eab4e6f
added some ad-hoc namespace prefixes to avoid duplicate facts;
wenzelm
parents:
43543
diff
changeset
|
109 |
locale use_decl = l: logic + semi "op ||" |
37134 | 110 |
print_locale! use_decl thm use_decl_def |
111 |
||
112 |
locale extra_type = |
|
113 |
fixes a :: 'a |
|
114 |
and P :: "'a => 'b => o" |
|
115 |
begin |
|
116 |
||
117 |
definition test :: "'a => o" where |
|
118 |
"test(x) <-> (ALL b. P(x, b))" |
|
119 |
||
120 |
end |
|
121 |
||
122 |
term extra_type.test thm extra_type.test_def |
|
123 |
||
124 |
interpretation var?: extra_type "0" "%x y. x = 0" . |
|
125 |
||
126 |
thm var.test_def |
|
127 |
||
128 |
||
60770 | 129 |
text \<open>Under which circumstances term syntax remains active.\<close> |
37134 | 130 |
|
131 |
locale "syntax" = |
|
132 |
fixes p1 :: "'a => 'b" |
|
133 |
and p2 :: "'b => o" |
|
134 |
begin |
|
135 |
||
136 |
definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))" |
|
137 |
definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)" |
|
138 |
||
139 |
thm d1_def d2_def |
|
140 |
||
141 |
end |
|
142 |
||
143 |
thm syntax.d1_def syntax.d2_def |
|
144 |
||
145 |
locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o" |
|
146 |
begin |
|
147 |
||
148 |
thm d1_def d2_def (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *) |
|
149 |
||
60770 | 150 |
ML \<open> |
37134 | 151 |
fun check_syntax ctxt thm expected = |
152 |
let |
|
56036 | 153 |
val obtained = |
61268 | 154 |
Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm; |
37134 | 155 |
in |
156 |
if obtained <> expected |
|
157 |
then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.") |
|
158 |
else () |
|
159 |
end; |
|
60770 | 160 |
\<close> |
37134 | 161 |
|
41305
42967939ea81
actually enable show_hyps option, unlike local_setup in 6da953d30f48 which merely affects the (temporary) auxiliary context;
wenzelm
parents:
41272
diff
changeset
|
162 |
declare [[show_hyps]] |
41271
6da953d30f48
Enable show_hyps, which appears to be set in batch mode but in an interactive session.
ballarin
parents:
39557
diff
changeset
|
163 |
|
60770 | 164 |
ML \<open> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61268
diff
changeset
|
165 |
check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p1(?x))"; |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61268
diff
changeset
|
166 |
check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)"; |
60770 | 167 |
\<close> |
37134 | 168 |
|
169 |
end |
|
170 |
||
171 |
locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o" |
|
172 |
begin |
|
173 |
||
174 |
thm d1_def d2_def |
|
175 |
(* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *) |
|
176 |
||
60770 | 177 |
ML \<open> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61268
diff
changeset
|
178 |
check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) \<longleftrightarrow> \<not> p2(p3(?x))"; |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61268
diff
changeset
|
179 |
check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)"; |
60770 | 180 |
\<close> |
37134 | 181 |
|
182 |
end |
|
183 |
||
184 |
||
60770 | 185 |
section \<open>Foundational versions of theorems\<close> |
37134 | 186 |
|
187 |
thm logic.assoc |
|
188 |
thm logic.lor_def |
|
189 |
||
190 |
||
60770 | 191 |
section \<open>Defines\<close> |
37134 | 192 |
|
193 |
locale logic_def = |
|
194 |
fixes land (infixl "&&" 55) |
|
195 |
and lor (infixl "||" 50) |
|
196 |
and lnot ("-- _" [60] 60) |
|
197 |
assumes assoc: "(x && y) && z = x && (y && z)" |
|
198 |
and notnot: "-- (-- x) = x" |
|
199 |
defines "x || y == --(-- x && -- y)" |
|
200 |
begin |
|
201 |
||
202 |
thm lor_def |
|
203 |
||
204 |
lemma "x || y = --(-- x && --y)" |
|
205 |
by (unfold lor_def) (rule refl) |
|
206 |
||
207 |
end |
|
208 |
||
209 |
(* Inheritance of defines *) |
|
210 |
||
211 |
locale logic_def2 = logic_def |
|
212 |
begin |
|
213 |
||
214 |
lemma "x || y = --(-- x && --y)" |
|
215 |
by (unfold lor_def) (rule refl) |
|
216 |
||
217 |
end |
|
218 |
||
219 |
||
60770 | 220 |
section \<open>Notes\<close> |
37134 | 221 |
|
222 |
(* A somewhat arcane homomorphism example *) |
|
223 |
||
224 |
definition semi_hom where |
|
225 |
"semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))" |
|
226 |
||
227 |
lemma semi_hom_mult: |
|
228 |
"semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))" |
|
229 |
by (simp add: semi_hom_def) |
|
230 |
||
231 |
locale semi_hom_loc = prod: semi prod + sum: semi sum |
|
232 |
for prod and sum and h + |
|
233 |
assumes semi_homh: "semi_hom(prod, sum, h)" |
|
234 |
notes semi_hom_mult = semi_hom_mult [OF semi_homh] |
|
235 |
||
236 |
thm semi_hom_loc.semi_hom_mult |
|
237 |
(* unspecified, attribute not applied in backgroud theory !!! *) |
|
238 |
||
239 |
lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" |
|
240 |
by (rule semi_hom_mult) |
|
241 |
||
242 |
(* Referring to facts from within a context specification *) |
|
243 |
||
244 |
lemma |
|
245 |
assumes x: "P <-> P" |
|
246 |
notes y = x |
|
247 |
shows True .. |
|
248 |
||
249 |
||
60770 | 250 |
section \<open>Theorem statements\<close> |
37134 | 251 |
|
252 |
lemma (in lgrp) lcancel: |
|
253 |
"x ** y = x ** z <-> y = z" |
|
254 |
proof |
|
255 |
assume "x ** y = x ** z" |
|
256 |
then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc) |
|
257 |
then show "y = z" by (simp add: lone linv) |
|
258 |
qed simp |
|
259 |
print_locale! lgrp |
|
260 |
||
261 |
||
262 |
locale rgrp = semi + |
|
263 |
fixes one and inv |
|
264 |
assumes rone: "x ** one = x" |
|
265 |
and rinv: "x ** inv(x) = one" |
|
266 |
begin |
|
267 |
||
268 |
lemma rcancel: |
|
269 |
"y ** x = z ** x <-> y = z" |
|
270 |
proof |
|
271 |
assume "y ** x = z ** x" |
|
272 |
then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" |
|
273 |
by (simp add: assoc [symmetric]) |
|
274 |
then show "y = z" by (simp add: rone rinv) |
|
275 |
qed simp |
|
276 |
||
277 |
end |
|
278 |
print_locale! rgrp |
|
279 |
||
280 |
||
60770 | 281 |
subsection \<open>Patterns\<close> |
37134 | 282 |
|
283 |
lemma (in rgrp) |
|
284 |
assumes "y ** x = z ** x" (is ?a) |
|
285 |
shows "y = z" (is ?t) |
|
286 |
proof - |
|
60770 | 287 |
txt \<open>Weird proof involving patterns from context element and conclusion.\<close> |
37134 | 288 |
{ |
289 |
assume ?a |
|
290 |
then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" |
|
291 |
by (simp add: assoc [symmetric]) |
|
292 |
then have ?t by (simp add: rone rinv) |
|
293 |
} |
|
294 |
note x = this |
|
60770 | 295 |
show ?t by (rule x [OF \<open>?a\<close>]) |
37134 | 296 |
qed |
297 |
||
298 |
||
60770 | 299 |
section \<open>Interpretation between locales: sublocales\<close> |
37134 | 300 |
|
301 |
sublocale lgrp < right: rgrp |
|
302 |
print_facts |
|
303 |
proof unfold_locales |
|
304 |
{ |
|
305 |
fix x |
|
306 |
have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) |
|
307 |
then show "x ** one = x" by (simp add: assoc lcancel) |
|
308 |
} |
|
309 |
note rone = this |
|
310 |
{ |
|
311 |
fix x |
|
312 |
have "inv(x) ** x ** inv(x) = inv(x) ** one" |
|
313 |
by (simp add: linv lone rone) |
|
314 |
then show "x ** inv(x) = one" by (simp add: assoc lcancel) |
|
315 |
} |
|
316 |
qed |
|
317 |
||
318 |
(* effect on printed locale *) |
|
319 |
||
320 |
print_locale! lgrp |
|
321 |
||
322 |
(* use of derived theorem *) |
|
323 |
||
324 |
lemma (in lgrp) |
|
325 |
"y ** x = z ** x <-> y = z" |
|
326 |
apply (rule rcancel) |
|
327 |
done |
|
328 |
||
329 |
(* circular interpretation *) |
|
330 |
||
331 |
sublocale rgrp < left: lgrp |
|
332 |
proof unfold_locales |
|
333 |
{ |
|
334 |
fix x |
|
335 |
have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone) |
|
336 |
then show "one ** x = x" by (simp add: assoc [symmetric] rcancel) |
|
337 |
} |
|
338 |
note lone = this |
|
339 |
{ |
|
340 |
fix x |
|
341 |
have "inv(x) ** (x ** inv(x)) = one ** inv(x)" |
|
342 |
by (simp add: rinv lone rone) |
|
343 |
then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel) |
|
344 |
} |
|
345 |
qed |
|
346 |
||
347 |
(* effect on printed locale *) |
|
348 |
||
349 |
print_locale! rgrp |
|
350 |
print_locale! lgrp |
|
351 |
||
352 |
||
353 |
(* Duality *) |
|
354 |
||
355 |
locale order = |
|
356 |
fixes less :: "'a => 'a => o" (infix "<<" 50) |
|
357 |
assumes refl: "x << x" |
|
358 |
and trans: "[| x << y; y << z |] ==> x << z" |
|
359 |
||
360 |
sublocale order < dual: order "%x y. y << x" |
|
361 |
apply unfold_locales apply (rule refl) apply (blast intro: trans) |
|
362 |
done |
|
363 |
||
364 |
print_locale! order (* Only two instances of order. *) |
|
365 |
||
366 |
locale order' = |
|
367 |
fixes less :: "'a => 'a => o" (infix "<<" 50) |
|
368 |
assumes refl: "x << x" |
|
369 |
and trans: "[| x << y; y << z |] ==> x << z" |
|
370 |
||
371 |
locale order_with_def = order' |
|
372 |
begin |
|
373 |
||
374 |
definition greater :: "'a => 'a => o" (infix ">>" 50) where |
|
375 |
"x >> y <-> y << x" |
|
376 |
||
377 |
end |
|
378 |
||
379 |
sublocale order_with_def < dual: order' "op >>" |
|
380 |
apply unfold_locales |
|
381 |
unfolding greater_def |
|
382 |
apply (rule refl) apply (blast intro: trans) |
|
383 |
done |
|
384 |
||
385 |
print_locale! order_with_def |
|
386 |
(* Note that decls come after theorems that make use of them. *) |
|
387 |
||
388 |
||
389 |
(* locale with many parameters --- |
|
390 |
interpretations generate alternating group A5 *) |
|
391 |
||
392 |
||
393 |
locale A5 = |
|
394 |
fixes A and B and C and D and E |
|
395 |
assumes eq: "A <-> B <-> C <-> D <-> E" |
|
396 |
||
397 |
sublocale A5 < 1: A5 _ _ D E C |
|
398 |
print_facts |
|
399 |
using eq apply (blast intro: A5.intro) done |
|
400 |
||
401 |
sublocale A5 < 2: A5 C _ E _ A |
|
402 |
print_facts |
|
403 |
using eq apply (blast intro: A5.intro) done |
|
404 |
||
405 |
sublocale A5 < 3: A5 B C A _ _ |
|
406 |
print_facts |
|
407 |
using eq apply (blast intro: A5.intro) done |
|
408 |
||
409 |
(* Any even permutation of parameters is subsumed by the above. *) |
|
410 |
||
411 |
print_locale! A5 |
|
412 |
||
413 |
||
414 |
(* Free arguments of instance *) |
|
415 |
||
416 |
locale trivial = |
|
417 |
fixes P and Q :: o |
|
418 |
assumes Q: "P <-> P <-> Q" |
|
419 |
begin |
|
420 |
||
421 |
lemma Q_triv: "Q" using Q by fast |
|
422 |
||
423 |
end |
|
424 |
||
425 |
sublocale trivial < x: trivial x _ |
|
426 |
apply unfold_locales using Q by fast |
|
427 |
||
428 |
print_locale! trivial |
|
429 |
||
430 |
context trivial begin thm x.Q [where ?x = True] end |
|
431 |
||
432 |
sublocale trivial < y: trivial Q Q |
|
433 |
by unfold_locales |
|
434 |
(* Succeeds since previous interpretation is more general. *) |
|
435 |
||
436 |
print_locale! trivial (* No instance for y created (subsumed). *) |
|
437 |
||
438 |
||
60770 | 439 |
subsection \<open>Sublocale, then interpretation in theory\<close> |
37134 | 440 |
|
441 |
interpretation int?: lgrp "op +" "0" "minus" |
|
442 |
proof unfold_locales |
|
443 |
qed (rule int_assoc int_zero int_minus)+ |
|
444 |
||
445 |
thm int.assoc int.semi_axioms |
|
446 |
||
447 |
interpretation int2?: semi "op +" |
|
448 |
by unfold_locales (* subsumed, thm int2.assoc not generated *) |
|
449 |
||
60770 | 450 |
ML \<open>(Global_Theory.get_thms @{theory} "int2.assoc"; |
56138 | 451 |
raise Fail "thm int2.assoc was generated") |
60770 | 452 |
handle ERROR _ => ([]:thm list);\<close> |
37134 | 453 |
|
454 |
thm int.lone int.right.rone |
|
455 |
(* the latter comes through the sublocale relation *) |
|
456 |
||
457 |
||
60770 | 458 |
subsection \<open>Interpretation in theory, then sublocale\<close> |
37134 | 459 |
|
460 |
interpretation fol: logic "op +" "minus" |
|
461 |
by unfold_locales (rule int_assoc int_minus2)+ |
|
462 |
||
463 |
locale logic2 = |
|
464 |
fixes land (infixl "&&" 55) |
|
465 |
and lnot ("-- _" [60] 60) |
|
466 |
assumes assoc: "(x && y) && z = x && (y && z)" |
|
467 |
and notnot: "-- (-- x) = x" |
|
468 |
begin |
|
469 |
||
470 |
definition lor (infixl "||" 50) where |
|
471 |
"x || y = --(-- x && -- y)" |
|
472 |
||
473 |
end |
|
474 |
||
475 |
sublocale logic < two: logic2 |
|
476 |
by unfold_locales (rule assoc notnot)+ |
|
477 |
||
478 |
thm fol.two.assoc |
|
479 |
||
480 |
||
60770 | 481 |
subsection \<open>Declarations and sublocale\<close> |
37134 | 482 |
|
483 |
locale logic_a = logic |
|
484 |
locale logic_b = logic |
|
485 |
||
486 |
sublocale logic_a < logic_b |
|
487 |
by unfold_locales |
|
488 |
||
489 |
||
60770 | 490 |
subsection \<open>Interpretation\<close> |
53366 | 491 |
|
60770 | 492 |
subsection \<open>Rewrite morphism\<close> |
37134 | 493 |
|
494 |
locale logic_o = |
|
495 |
fixes land (infixl "&&" 55) |
|
496 |
and lnot ("-- _" [60] 60) |
|
497 |
assumes assoc_o: "(x && y) && z <-> x && (y && z)" |
|
498 |
and notnot_o: "-- (-- x) <-> x" |
|
499 |
begin |
|
500 |
||
501 |
definition lor_o (infixl "||" 50) where |
|
502 |
"x || y <-> --(-- x && -- y)" |
|
503 |
||
504 |
end |
|
505 |
||
506 |
interpretation x: logic_o "op &" "Not" |
|
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
41779
diff
changeset
|
507 |
where bool_logic_o: "x.lor_o(x, y) <-> x | y" |
37134 | 508 |
proof - |
509 |
show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+ |
|
510 |
show "logic_o.lor_o(op &, Not, x, y) <-> x | y" |
|
511 |
by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast |
|
512 |
qed |
|
513 |
||
514 |
thm x.lor_o_def bool_logic_o |
|
515 |
||
516 |
lemma lor_triv: "z <-> z" .. |
|
517 |
||
518 |
lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast |
|
519 |
||
520 |
thm lor_triv [where z = True] (* Check strict prefix. *) |
|
521 |
x.lor_triv |
|
522 |
||
523 |
||
60770 | 524 |
subsection \<open>Inheritance of rewrite morphisms\<close> |
37134 | 525 |
|
526 |
locale reflexive = |
|
527 |
fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50) |
|
528 |
assumes refl: "x \<sqsubseteq> x" |
|
529 |
begin |
|
530 |
||
531 |
definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y" |
|
532 |
||
533 |
end |
|
534 |
||
41779 | 535 |
axiomatization |
536 |
gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and |
|
537 |
gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o" |
|
538 |
where |
|
539 |
grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and |
|
540 |
grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y" |
|
37134 | 541 |
|
60770 | 542 |
text \<open>Setup\<close> |
37134 | 543 |
|
544 |
locale mixin = reflexive |
|
545 |
begin |
|
546 |
lemmas less_thm = less_def |
|
547 |
end |
|
548 |
||
549 |
interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
550 |
proof - |
|
551 |
show "mixin(gle)" by unfold_locales (rule grefl) |
|
552 |
note reflexive = this[unfolded mixin_def] |
|
553 |
show "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
554 |
by (simp add: reflexive.less_def[OF reflexive] gless_def) |
|
555 |
qed |
|
556 |
||
60770 | 557 |
text \<open>Rewrite morphism propagated along the locale hierarchy\<close> |
37134 | 558 |
|
559 |
locale mixin2 = mixin |
|
560 |
begin |
|
561 |
lemmas less_thm2 = less_def |
|
562 |
end |
|
563 |
||
564 |
interpretation le: mixin2 gle |
|
565 |
by unfold_locales |
|
566 |
||
53366 | 567 |
thm le.less_thm2 (* rewrite morphism applied *) |
37134 | 568 |
lemma "gless(x, y) <-> gle(x, y) & x ~= y" |
569 |
by (rule le.less_thm2) |
|
570 |
||
60770 | 571 |
text \<open>Rewrite morphism does not leak to a side branch.\<close> |
37134 | 572 |
|
573 |
locale mixin3 = reflexive |
|
574 |
begin |
|
575 |
lemmas less_thm3 = less_def |
|
576 |
end |
|
577 |
||
578 |
interpretation le: mixin3 gle |
|
579 |
by unfold_locales |
|
580 |
||
53366 | 581 |
thm le.less_thm3 (* rewrite morphism not applied *) |
37134 | 582 |
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3) |
583 |
||
60770 | 584 |
text \<open>Rewrite morphism only available in original context\<close> |
37134 | 585 |
|
586 |
locale mixin4_base = reflexive |
|
587 |
||
588 |
locale mixin4_mixin = mixin4_base |
|
589 |
||
590 |
interpretation le: mixin4_mixin gle |
|
591 |
where "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
592 |
proof - |
|
593 |
show "mixin4_mixin(gle)" by unfold_locales (rule grefl) |
|
594 |
note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def] |
|
595 |
show "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
596 |
by (simp add: reflexive.less_def[OF reflexive] gless_def) |
|
597 |
qed |
|
598 |
||
599 |
locale mixin4_copy = mixin4_base |
|
600 |
begin |
|
601 |
lemmas less_thm4 = less_def |
|
602 |
end |
|
603 |
||
604 |
locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le |
|
605 |
begin |
|
606 |
lemmas less_thm4' = less_def |
|
607 |
end |
|
608 |
||
609 |
interpretation le4: mixin4_combined gle' gle |
|
610 |
by unfold_locales (rule grefl') |
|
611 |
||
53366 | 612 |
thm le4.less_thm4' (* rewrite morphism not applied *) |
37134 | 613 |
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" |
614 |
by (rule le4.less_thm4') |
|
615 |
||
60770 | 616 |
text \<open>Inherited rewrite morphism applied to new theorem\<close> |
37134 | 617 |
|
618 |
locale mixin5_base = reflexive |
|
619 |
||
620 |
locale mixin5_inherited = mixin5_base |
|
621 |
||
622 |
interpretation le5: mixin5_base gle |
|
623 |
where "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
624 |
proof - |
|
625 |
show "mixin5_base(gle)" by unfold_locales |
|
626 |
note reflexive = this[unfolded mixin5_base_def mixin_def] |
|
627 |
show "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
628 |
by (simp add: reflexive.less_def[OF reflexive] gless_def) |
|
629 |
qed |
|
630 |
||
631 |
interpretation le5: mixin5_inherited gle |
|
632 |
by unfold_locales |
|
633 |
||
634 |
lemmas (in mixin5_inherited) less_thm5 = less_def |
|
635 |
||
53366 | 636 |
thm le5.less_thm5 (* rewrite morphism applied *) |
37134 | 637 |
lemma "gless(x, y) <-> gle(x, y) & x ~= y" |
638 |
by (rule le5.less_thm5) |
|
639 |
||
60770 | 640 |
text \<open>Rewrite morphism pushed down to existing inherited locale\<close> |
37134 | 641 |
|
642 |
locale mixin6_base = reflexive |
|
643 |
||
644 |
locale mixin6_inherited = mixin5_base |
|
645 |
||
646 |
interpretation le6: mixin6_base gle |
|
647 |
by unfold_locales |
|
648 |
interpretation le6: mixin6_inherited gle |
|
649 |
by unfold_locales |
|
650 |
interpretation le6: mixin6_base gle |
|
651 |
where "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
652 |
proof - |
|
653 |
show "mixin6_base(gle)" by unfold_locales |
|
654 |
note reflexive = this[unfolded mixin6_base_def mixin_def] |
|
655 |
show "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
656 |
by (simp add: reflexive.less_def[OF reflexive] gless_def) |
|
657 |
qed |
|
658 |
||
659 |
lemmas (in mixin6_inherited) less_thm6 = less_def |
|
660 |
||
661 |
thm le6.less_thm6 (* mixin applied *) |
|
662 |
lemma "gless(x, y) <-> gle(x, y) & x ~= y" |
|
663 |
by (rule le6.less_thm6) |
|
664 |
||
60770 | 665 |
text \<open>Existing rewrite morphism inherited through sublocale relation\<close> |
37134 | 666 |
|
667 |
locale mixin7_base = reflexive |
|
668 |
||
669 |
locale mixin7_inherited = reflexive |
|
670 |
||
671 |
interpretation le7: mixin7_base gle |
|
672 |
where "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
673 |
proof - |
|
674 |
show "mixin7_base(gle)" by unfold_locales |
|
675 |
note reflexive = this[unfolded mixin7_base_def mixin_def] |
|
676 |
show "reflexive.less(gle, x, y) <-> gless(x, y)" |
|
677 |
by (simp add: reflexive.less_def[OF reflexive] gless_def) |
|
678 |
qed |
|
679 |
||
680 |
interpretation le7: mixin7_inherited gle |
|
681 |
by unfold_locales |
|
682 |
||
683 |
lemmas (in mixin7_inherited) less_thm7 = less_def |
|
684 |
||
53366 | 685 |
thm le7.less_thm7 (* before, rewrite morphism not applied *) |
37134 | 686 |
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" |
687 |
by (rule le7.less_thm7) |
|
688 |
||
689 |
sublocale mixin7_inherited < mixin7_base |
|
690 |
by unfold_locales |
|
691 |
||
692 |
lemmas (in mixin7_inherited) less_thm7b = less_def |
|
693 |
||
694 |
thm le7.less_thm7b (* after, mixin applied *) |
|
695 |
lemma "gless(x, y) <-> gle(x, y) & x ~= y" |
|
696 |
by (rule le7.less_thm7b) |
|
697 |
||
698 |
||
60770 | 699 |
text \<open>This locale will be interpreted in later theories.\<close> |
37134 | 700 |
|
701 |
locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le' |
|
702 |
||
703 |
||
60770 | 704 |
subsection \<open>Rewrite morphisms in sublocale\<close> |
41272 | 705 |
|
60770 | 706 |
text \<open>Simulate a specification of left groups where unit and inverse are defined |
41272 | 707 |
rather than specified. This is possible, but not in FOL, due to the lack of a |
60770 | 708 |
selection operator.\<close> |
41272 | 709 |
|
710 |
axiomatization glob_one and glob_inv |
|
711 |
where glob_lone: "prod(glob_one(prod), x) = x" |
|
712 |
and glob_linv: "prod(glob_inv(prod, x), x) = glob_one(prod)" |
|
713 |
||
714 |
locale dgrp = semi |
|
715 |
begin |
|
716 |
||
717 |
definition one where "one = glob_one(prod)" |
|
718 |
||
719 |
lemma lone: "one ** x = x" |
|
720 |
unfolding one_def by (rule glob_lone) |
|
721 |
||
722 |
definition inv where "inv(x) = glob_inv(prod, x)" |
|
723 |
||
724 |
lemma linv: "inv(x) ** x = one" |
|
725 |
unfolding one_def inv_def by (rule glob_linv) |
|
726 |
||
727 |
end |
|
728 |
||
729 |
sublocale lgrp < "def": dgrp |
|
730 |
where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)" |
|
731 |
proof - |
|
732 |
show "dgrp(prod)" by unfold_locales |
|
733 |
from this interpret d: dgrp . |
|
734 |
-- Unit |
|
735 |
have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def) |
|
736 |
also have "... = glob_one(prod) ** one" by (simp add: rone) |
|
737 |
also have "... = one" by (simp add: glob_lone) |
|
738 |
finally show "dgrp.one(prod) = one" . |
|
739 |
-- Inverse |
|
740 |
then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv) |
|
741 |
then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel) |
|
742 |
qed |
|
743 |
||
744 |
print_locale! lgrp |
|
745 |
||
746 |
context lgrp begin |
|
747 |
||
60770 | 748 |
text \<open>Equations stored in target\<close> |
41272 | 749 |
|
750 |
lemma "dgrp.one(prod) = one" by (rule one_equation) |
|
751 |
lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation) |
|
752 |
||
60770 | 753 |
text \<open>Rewrite morphisms applied\<close> |
41272 | 754 |
|
755 |
lemma "one = glob_one(prod)" by (rule one_def) |
|
756 |
lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def) |
|
757 |
||
758 |
end |
|
759 |
||
60770 | 760 |
text \<open>Interpreted versions\<close> |
41272 | 761 |
|
762 |
lemma "0 = glob_one (op +)" by (rule int.def.one_def) |
|
763 |
lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def) |
|
764 |
||
60770 | 765 |
text \<open>Roundup applies rewrite morphisms at declaration level in DFS tree\<close> |
51515 | 766 |
|
767 |
locale roundup = fixes x assumes true: "x <-> True" |
|
768 |
||
769 |
sublocale roundup \<subseteq> sub: roundup x where "x <-> True & True" |
|
770 |
apply unfold_locales apply (simp add: true) done |
|
771 |
lemma (in roundup) "True & True <-> True" by (rule sub.true) |
|
772 |
||
41272 | 773 |
|
60770 | 774 |
section \<open>Interpretation in named contexts\<close> |
53367
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
775 |
|
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
776 |
locale container |
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
777 |
begin |
59897 | 778 |
interpretation "private"!: roundup True by unfold_locales rule |
53367
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
779 |
lemmas true_copy = private.true |
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
780 |
end |
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
781 |
|
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
782 |
context container begin |
60770 | 783 |
ML \<open>(Context.>> (fn generic => let val context = Context.proof_of generic |
53367
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
784 |
val _ = Proof_Context.get_thms context "private.true" in generic end); |
56138 | 785 |
raise Fail "thm private.true was persisted") |
60770 | 786 |
handle ERROR _ => ([]:thm list);\<close> |
53367
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
787 |
thm true_copy |
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
788 |
end |
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
789 |
|
1f383542226b
New test case: interpretation in named contexts is not persistent.
ballarin
parents:
53366
diff
changeset
|
790 |
|
60770 | 791 |
section \<open>Interpretation in proofs\<close> |
37134 | 792 |
|
793 |
lemma True |
|
794 |
proof |
|
795 |
interpret "local": lgrp "op +" "0" "minus" |
|
796 |
by unfold_locales (* subsumed *) |
|
797 |
{ |
|
798 |
fix zero :: int |
|
799 |
assume "!!x. zero + x = x" "!!x. (-x) + x = zero" |
|
800 |
then interpret local_fixed: lgrp "op +" zero "minus" |
|
801 |
by unfold_locales |
|
802 |
thm local_fixed.lone |
|
41435 | 803 |
print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus |
37134 | 804 |
} |
805 |
assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero" |
|
806 |
then interpret local_free: lgrp "op +" zero "minus" for zero |
|
807 |
by unfold_locales |
|
808 |
thm local_free.lone [where ?zero = 0] |
|
809 |
qed |
|
810 |
||
38108 | 811 |
lemma True |
812 |
proof |
|
813 |
{ |
|
814 |
fix pand and pnot and por |
|
815 |
assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))" |
|
816 |
and pnotnot: "!!x. pnot(pnot(x)) <-> x" |
|
817 |
and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" |
|
818 |
interpret loc: logic_o pand pnot |
|
819 |
where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" (* FIXME *) |
|
820 |
proof - |
|
821 |
show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales |
|
822 |
fix x y |
|
823 |
show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" |
|
824 |
by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric]) |
|
825 |
qed |
|
38109 | 826 |
print_interps logic_o |
38108 | 827 |
have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def) |
828 |
} |
|
829 |
qed |
|
830 |
||
37134 | 831 |
end |