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