author | blanchet |
Thu, 13 Mar 2014 13:18:13 +0100 | |
changeset 56085 | 3d11892ea537 |
parent 52697 | 6fb98a20c349 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Statespace/StateSpaceEx.thy |
25171 | 2 |
Author: Norbert Schirmer, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Examples \label{sec:Examples} *} |
|
6 |
theory StateSpaceEx |
|
7 |
imports StateSpaceLocale StateSpaceSyntax |
|
38838 | 8 |
begin |
25171 | 9 |
|
10 |
(*<*) |
|
11 |
syntax |
|
12 |
"_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900) |
|
13 |
(*>*) |
|
14 |
||
45358 | 15 |
text {* Did you ever dream about records with multiple inheritance? |
25171 | 16 |
Then you should definitely have a look at statespaces. They may be |
45358 | 17 |
what you are dreaming of. Or at least almost \dots *} |
25171 | 18 |
|
19 |
||
20 |
text {* Isabelle allows to add new top-level commands to the |
|
21 |
system. Building on the locale infrastructure, we provide a command |
|
22 |
\isacommand{statespace} like this:*} |
|
23 |
||
24 |
statespace vars = |
|
25 |
n::nat |
|
26 |
b::bool |
|
27 |
||
29247
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
28 |
print_locale vars_namespace |
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
29 |
print_locale vars_valuetypes |
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
30 |
print_locale vars |
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
31 |
|
25171 | 32 |
text {* \noindent This resembles a \isacommand{record} definition, |
33 |
but introduces sophisticated locale |
|
34 |
infrastructure instead of HOL type schemes. The resulting context |
|
35 |
postulates two distinct names @{term "n"} and @{term "b"} and |
|
36 |
projection~/ injection functions that convert from abstract values to |
|
37 |
@{typ "nat"} and @{text "bool"}. The logical content of the locale is: *} |
|
38 |
||
29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29248
diff
changeset
|
39 |
locale vars' = |
25171 | 40 |
fixes n::'name and b::'name |
41 |
assumes "distinct [n, b]" |
|
42 |
||
43 |
fixes project_nat::"'value \<Rightarrow> nat" and inject_nat::"nat \<Rightarrow> 'value" |
|
44 |
assumes "\<And>n. project_nat (inject_nat n) = n" |
|
45 |
||
46 |
fixes project_bool::"'value \<Rightarrow> bool" and inject_bool::"bool \<Rightarrow> 'value" |
|
47 |
assumes "\<And>b. project_bool (inject_bool b) = b" |
|
48 |
||
49 |
text {* \noindent The HOL predicate @{const "distinct"} describes |
|
50 |
distinctness of all names in the context. Locale @{text "vars'"} |
|
51 |
defines the raw logical content that is defined in the state space |
|
52 |
locale. We also maintain non-logical context information to support |
|
53 |
the user: |
|
54 |
||
55 |
\begin{itemize} |
|
56 |
||
57 |
\item Syntax for state lookup and updates that automatically inserts |
|
58 |
the corresponding projection and injection functions. |
|
59 |
||
60 |
\item Setup for the proof tools that exploit the distinctness |
|
61 |
information and the cancellation of projections and injections in |
|
62 |
deductions and simplifications. |
|
63 |
||
64 |
\end{itemize} |
|
65 |
||
66 |
This extra-logical information is added to the locale in form of |
|
67 |
declarations, which associate the name of a variable to the |
|
68 |
corresponding projection and injection functions to handle the syntax |
|
69 |
transformations, and a link from the variable name to the |
|
70 |
corresponding distinctness theorem. As state spaces are merged or |
|
71 |
extended there are multiple distinctness theorems in the context. Our |
|
72 |
declarations take care that the link always points to the strongest |
|
73 |
distinctness assumption. With these declarations in place, a lookup |
|
74 |
can be written as @{text "s\<cdot>n"}, which is translated to @{text |
|
75 |
"project_nat (s n)"}, and an update as @{text "s\<langle>n := 2\<rangle>"}, which is |
|
76 |
translated to @{text "s(n := inject_nat 2)"}. We can now establish the |
|
77 |
following lemma: *} |
|
78 |
||
79 |
lemma (in vars) foo: "s<n := 2>\<cdot>b = s\<cdot>b" by simp |
|
80 |
||
81 |
text {* \noindent Here the simplifier was able to refer to |
|
82 |
distinctness of @{term "b"} and @{term "n"} to solve the equation. |
|
83 |
The resulting lemma is also recorded in locale @{text "vars"} for |
|
84 |
later use and is automatically propagated to all its interpretations. |
|
85 |
Here is another example: *} |
|
86 |
||
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
45666
diff
changeset
|
87 |
statespace 'a varsX = NB: vars [n=N, b=B] + vars + x::'a |
25171 | 88 |
|
89 |
text {* \noindent The state space @{text "varsX"} imports two copies |
|
90 |
of the state space @{text "vars"}, where one has the variables renamed |
|
91 |
to upper-case letters, and adds another variable @{term "x"} of type |
|
92 |
@{typ "'a"}. This type is fixed inside the state space but may get |
|
93 |
instantiated later on, analogous to type parameters of an ML-functor. |
|
94 |
The distinctness assumption is now @{text "distinct [N, B, n, b, x]"}, |
|
95 |
from this we can derive both @{term "distinct [N,B]"} and @{term |
|
96 |
"distinct [n,b]"}, the distinction assumptions for the two versions of |
|
97 |
locale @{text "vars"} above. Moreover we have all necessary |
|
98 |
projection and injection assumptions available. These assumptions |
|
99 |
together allow us to establish state space @{term "varsX"} as an |
|
100 |
interpretation of both instances of locale @{term "vars"}. Hence we |
|
101 |
inherit both variants of theorem @{text "foo"}: @{text "s\<langle>N := 2\<rangle>\<cdot>B = |
|
102 |
s\<cdot>B"} as well as @{text "s\<langle>n := 2\<rangle>\<cdot>b = s\<cdot>b"}. These are immediate |
|
103 |
consequences of the locale interpretation action. |
|
104 |
||
105 |
The declarations for syntax and the distinctness theorems also observe |
|
106 |
the morphisms generated by the locale package due to the renaming |
|
107 |
@{term "n = N"}: *} |
|
108 |
||
109 |
lemma (in varsX) foo: "s\<langle>N := 2\<rangle>\<cdot>x = s\<cdot>x" by simp |
|
110 |
||
111 |
text {* To assure scalability towards many distinct names, the |
|
112 |
distinctness predicate is refined to operate on balanced trees. Thus |
|
113 |
we get logarithmic certificates for the distinctness of two names by |
|
114 |
the distinctness of the paths in the tree. Asked for the distinctness |
|
115 |
of two names, our tool produces the paths of the variables in the tree |
|
116 |
(this is implemented in SML, outside the logic) and returns a |
|
117 |
certificate corresponding to the different paths. Merging state |
|
118 |
spaces requires to prove that the combined distinctness assumption |
|
119 |
implies the distinctness assumptions of the components. Such a proof |
|
120 |
is of the order $m \cdot \log n$, where $n$ and $m$ are the number of |
|
121 |
nodes in the larger and smaller tree, respectively.*} |
|
122 |
||
123 |
text {* We continue with more examples. *} |
|
124 |
||
125 |
statespace 'a foo = |
|
126 |
f::"nat\<Rightarrow>nat" |
|
127 |
a::int |
|
128 |
b::nat |
|
129 |
c::'a |
|
130 |
||
131 |
||
132 |
||
133 |
lemma (in foo) foo1: |
|
134 |
shows "s\<langle>a := i\<rangle>\<cdot>a = i" |
|
135 |
by simp |
|
136 |
||
137 |
lemma (in foo) foo2: |
|
138 |
shows "(s\<langle>a:=i\<rangle>)\<cdot>a = i" |
|
139 |
by simp |
|
140 |
||
141 |
lemma (in foo) foo3: |
|
142 |
shows "(s\<langle>a:=i\<rangle>)\<cdot>b = s\<cdot>b" |
|
143 |
by simp |
|
144 |
||
145 |
lemma (in foo) foo4: |
|
146 |
shows "(s\<langle>a:=i,b:=j,c:=k,a:=x\<rangle>) = (s\<langle>b:=j,c:=k,a:=x\<rangle>)" |
|
147 |
by simp |
|
148 |
||
149 |
statespace bar = |
|
150 |
b::bool |
|
151 |
c::string |
|
152 |
||
153 |
lemma (in bar) bar1: |
|
154 |
shows "(s\<langle>b:=True\<rangle>)\<cdot>c = s\<cdot>c" |
|
155 |
by simp |
|
156 |
||
157 |
text {* You can define a derived state space by inheriting existing state spaces, renaming |
|
158 |
of components if you like, and by declaring new components. |
|
159 |
*} |
|
160 |
||
161 |
statespace ('a,'b) loo = 'a foo + bar [b=B,c=C] + |
|
162 |
X::'b |
|
163 |
||
164 |
lemma (in loo) loo1: |
|
165 |
shows "s\<langle>a:=i\<rangle>\<cdot>B = s\<cdot>B" |
|
166 |
proof - |
|
167 |
thm foo1 |
|
168 |
txt {* The Lemma @{thm [source] foo1} from the parent state space |
|
45358 | 169 |
is also available here: \begin{center}@{thm foo1}\end{center} *} |
25171 | 170 |
have "s<a:=i>\<cdot>a = i" |
171 |
by (rule foo1) |
|
172 |
thm bar1 |
|
173 |
txt {* Note the renaming of the parameters in Lemma @{thm [source] bar1}: |
|
45358 | 174 |
\begin{center}@{thm bar1}\end{center} *} |
25171 | 175 |
have "s<B:=True>\<cdot>C = s\<cdot>C" |
176 |
by (rule bar1) |
|
177 |
show ?thesis |
|
178 |
by simp |
|
179 |
qed |
|
180 |
||
181 |
||
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
45666
diff
changeset
|
182 |
statespace 'a dup = FA: 'a foo [f=F, a=A] + 'a foo + |
25171 | 183 |
x::int |
184 |
||
185 |
lemma (in dup) |
|
186 |
shows "s<a := i>\<cdot>x = s\<cdot>x" |
|
187 |
by simp |
|
188 |
||
189 |
lemma (in dup) |
|
190 |
shows "s<A := i>\<cdot>a = s\<cdot>a" |
|
191 |
by simp |
|
192 |
||
193 |
lemma (in dup) |
|
194 |
shows "s<A := i>\<cdot>x = s\<cdot>x" |
|
195 |
by simp |
|
196 |
||
197 |
||
45358 | 198 |
(* |
199 |
text "Hmm, I hoped this would work now..." |
|
29247
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
200 |
|
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
201 |
locale fooX = foo + |
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
202 |
assumes "s<a:=i>\<cdot>b = k" |
29248 | 203 |
*) |
29247
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
204 |
|
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
205 |
(* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *) |
25171 | 206 |
text {* There are known problems with syntax-declarations. They currently |
207 |
only work, when the context is already built. Hopefully this will be |
|
208 |
implemented correctly in future Isabelle versions. *} |
|
209 |
||
29247
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
210 |
(* |
25171 | 211 |
lemma |
28611 | 212 |
assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4" |
213 |
shows True |
|
214 |
proof |
|
29247
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
215 |
interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact |
25171 | 216 |
term "s<a := i>\<cdot>a = i" |
28611 | 217 |
qed |
29247
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
218 |
*) |
25171 | 219 |
(* |
220 |
lemma |
|
221 |
includes foo |
|
222 |
shows "s<a := i>\<cdot>a = i" |
|
223 |
*) |
|
224 |
||
225 |
text {* It would be nice to have nested state spaces. This is |
|
226 |
logically no problem. From the locale-implementation side this may be |
|
227 |
something like an 'includes' into a locale. When there is a more |
|
228 |
elaborate locale infrastructure in place this may be an easy exercise. |
|
229 |
*} |
|
230 |
||
45360 | 231 |
|
232 |
subsection {* Benchmarks *} |
|
233 |
||
234 |
text {* Here are some bigger examples for benchmarking. *} |
|
235 |
||
236 |
ML {* |
|
237 |
fun make_benchmark n = |
|
52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
50450
diff
changeset
|
238 |
writeln (Active.sendback_markup [] |
45360 | 239 |
("statespace benchmark" ^ string_of_int n ^ " =\n" ^ |
240 |
(cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n))))); |
|
241 |
*} |
|
242 |
||
243 |
text "0.2s" |
|
244 |
statespace benchmark100 = A1::nat A2::nat A3::nat A4::nat A5::nat |
|
245 |
A6::nat A7::nat A8::nat A9::nat A10::nat A11::nat A12::nat A13::nat |
|
246 |
A14::nat A15::nat A16::nat A17::nat A18::nat A19::nat A20::nat |
|
247 |
A21::nat A22::nat A23::nat A24::nat A25::nat A26::nat A27::nat |
|
248 |
A28::nat A29::nat A30::nat A31::nat A32::nat A33::nat A34::nat |
|
249 |
A35::nat A36::nat A37::nat A38::nat A39::nat A40::nat A41::nat |
|
250 |
A42::nat A43::nat A44::nat A45::nat A46::nat A47::nat A48::nat |
|
251 |
A49::nat A50::nat A51::nat A52::nat A53::nat A54::nat A55::nat |
|
252 |
A56::nat A57::nat A58::nat A59::nat A60::nat A61::nat A62::nat |
|
253 |
A63::nat A64::nat A65::nat A66::nat A67::nat A68::nat A69::nat |
|
254 |
A70::nat A71::nat A72::nat A73::nat A74::nat A75::nat A76::nat |
|
255 |
A77::nat A78::nat A79::nat A80::nat A81::nat A82::nat A83::nat |
|
256 |
A84::nat A85::nat A86::nat A87::nat A88::nat A89::nat A90::nat |
|
257 |
A91::nat A92::nat A93::nat A94::nat A95::nat A96::nat A97::nat |
|
258 |
A98::nat A99::nat A100::nat |
|
259 |
||
260 |
text "2.4s" |
|
261 |
statespace benchmark500 = A1::nat A2::nat A3::nat A4::nat A5::nat |
|
262 |
A6::nat A7::nat A8::nat A9::nat A10::nat A11::nat A12::nat A13::nat |
|
263 |
A14::nat A15::nat A16::nat A17::nat A18::nat A19::nat A20::nat |
|
264 |
A21::nat A22::nat A23::nat A24::nat A25::nat A26::nat A27::nat |
|
265 |
A28::nat A29::nat A30::nat A31::nat A32::nat A33::nat A34::nat |
|
266 |
A35::nat A36::nat A37::nat A38::nat A39::nat A40::nat A41::nat |
|
267 |
A42::nat A43::nat A44::nat A45::nat A46::nat A47::nat A48::nat |
|
268 |
A49::nat A50::nat A51::nat A52::nat A53::nat A54::nat A55::nat |
|
269 |
A56::nat A57::nat A58::nat A59::nat A60::nat A61::nat A62::nat |
|
270 |
A63::nat A64::nat A65::nat A66::nat A67::nat A68::nat A69::nat |
|
271 |
A70::nat A71::nat A72::nat A73::nat A74::nat A75::nat A76::nat |
|
272 |
A77::nat A78::nat A79::nat A80::nat A81::nat A82::nat A83::nat |
|
273 |
A84::nat A85::nat A86::nat A87::nat A88::nat A89::nat A90::nat |
|
274 |
A91::nat A92::nat A93::nat A94::nat A95::nat A96::nat A97::nat |
|
275 |
A98::nat A99::nat A100::nat A101::nat A102::nat A103::nat A104::nat |
|
276 |
A105::nat A106::nat A107::nat A108::nat A109::nat A110::nat A111::nat |
|
277 |
A112::nat A113::nat A114::nat A115::nat A116::nat A117::nat A118::nat |
|
278 |
A119::nat A120::nat A121::nat A122::nat A123::nat A124::nat A125::nat |
|
279 |
A126::nat A127::nat A128::nat A129::nat A130::nat A131::nat A132::nat |
|
280 |
A133::nat A134::nat A135::nat A136::nat A137::nat A138::nat A139::nat |
|
281 |
A140::nat A141::nat A142::nat A143::nat A144::nat A145::nat A146::nat |
|
282 |
A147::nat A148::nat A149::nat A150::nat A151::nat A152::nat A153::nat |
|
283 |
A154::nat A155::nat A156::nat A157::nat A158::nat A159::nat A160::nat |
|
284 |
A161::nat A162::nat A163::nat A164::nat A165::nat A166::nat A167::nat |
|
285 |
A168::nat A169::nat A170::nat A171::nat A172::nat A173::nat A174::nat |
|
286 |
A175::nat A176::nat A177::nat A178::nat A179::nat A180::nat A181::nat |
|
287 |
A182::nat A183::nat A184::nat A185::nat A186::nat A187::nat A188::nat |
|
288 |
A189::nat A190::nat A191::nat A192::nat A193::nat A194::nat A195::nat |
|
289 |
A196::nat A197::nat A198::nat A199::nat A200::nat A201::nat A202::nat |
|
290 |
A203::nat A204::nat A205::nat A206::nat A207::nat A208::nat A209::nat |
|
291 |
A210::nat A211::nat A212::nat A213::nat A214::nat A215::nat A216::nat |
|
292 |
A217::nat A218::nat A219::nat A220::nat A221::nat A222::nat A223::nat |
|
293 |
A224::nat A225::nat A226::nat A227::nat A228::nat A229::nat A230::nat |
|
294 |
A231::nat A232::nat A233::nat A234::nat A235::nat A236::nat A237::nat |
|
295 |
A238::nat A239::nat A240::nat A241::nat A242::nat A243::nat A244::nat |
|
296 |
A245::nat A246::nat A247::nat A248::nat A249::nat A250::nat A251::nat |
|
297 |
A252::nat A253::nat A254::nat A255::nat A256::nat A257::nat A258::nat |
|
298 |
A259::nat A260::nat A261::nat A262::nat A263::nat A264::nat A265::nat |
|
299 |
A266::nat A267::nat A268::nat A269::nat A270::nat A271::nat A272::nat |
|
300 |
A273::nat A274::nat A275::nat A276::nat A277::nat A278::nat A279::nat |
|
301 |
A280::nat A281::nat A282::nat A283::nat A284::nat A285::nat A286::nat |
|
302 |
A287::nat A288::nat A289::nat A290::nat A291::nat A292::nat A293::nat |
|
303 |
A294::nat A295::nat A296::nat A297::nat A298::nat A299::nat A300::nat |
|
304 |
A301::nat A302::nat A303::nat A304::nat A305::nat A306::nat A307::nat |
|
305 |
A308::nat A309::nat A310::nat A311::nat A312::nat A313::nat A314::nat |
|
306 |
A315::nat A316::nat A317::nat A318::nat A319::nat A320::nat A321::nat |
|
307 |
A322::nat A323::nat A324::nat A325::nat A326::nat A327::nat A328::nat |
|
308 |
A329::nat A330::nat A331::nat A332::nat A333::nat A334::nat A335::nat |
|
309 |
A336::nat A337::nat A338::nat A339::nat A340::nat A341::nat A342::nat |
|
310 |
A343::nat A344::nat A345::nat A346::nat A347::nat A348::nat A349::nat |
|
311 |
A350::nat A351::nat A352::nat A353::nat A354::nat A355::nat A356::nat |
|
312 |
A357::nat A358::nat A359::nat A360::nat A361::nat A362::nat A363::nat |
|
313 |
A364::nat A365::nat A366::nat A367::nat A368::nat A369::nat A370::nat |
|
314 |
A371::nat A372::nat A373::nat A374::nat A375::nat A376::nat A377::nat |
|
315 |
A378::nat A379::nat A380::nat A381::nat A382::nat A383::nat A384::nat |
|
316 |
A385::nat A386::nat A387::nat A388::nat A389::nat A390::nat A391::nat |
|
317 |
A392::nat A393::nat A394::nat A395::nat A396::nat A397::nat A398::nat |
|
318 |
A399::nat A400::nat A401::nat A402::nat A403::nat A404::nat A405::nat |
|
319 |
A406::nat A407::nat A408::nat A409::nat A410::nat A411::nat A412::nat |
|
320 |
A413::nat A414::nat A415::nat A416::nat A417::nat A418::nat A419::nat |
|
321 |
A420::nat A421::nat A422::nat A423::nat A424::nat A425::nat A426::nat |
|
322 |
A427::nat A428::nat A429::nat A430::nat A431::nat A432::nat A433::nat |
|
323 |
A434::nat A435::nat A436::nat A437::nat A438::nat A439::nat A440::nat |
|
324 |
A441::nat A442::nat A443::nat A444::nat A445::nat A446::nat A447::nat |
|
325 |
A448::nat A449::nat A450::nat A451::nat A452::nat A453::nat A454::nat |
|
326 |
A455::nat A456::nat A457::nat A458::nat A459::nat A460::nat A461::nat |
|
327 |
A462::nat A463::nat A464::nat A465::nat A466::nat A467::nat A468::nat |
|
328 |
A469::nat A470::nat A471::nat A472::nat A473::nat A474::nat A475::nat |
|
329 |
A476::nat A477::nat A478::nat A479::nat A480::nat A481::nat A482::nat |
|
330 |
A483::nat A484::nat A485::nat A486::nat A487::nat A488::nat A489::nat |
|
331 |
A490::nat A491::nat A492::nat A493::nat A494::nat A495::nat A496::nat |
|
332 |
A497::nat A498::nat A499::nat A500::nat |
|
333 |
||
334 |
text "9.0s" |
|
335 |
statespace benchmark1000 = A1::nat A2::nat A3::nat A4::nat A5::nat |
|
336 |
A6::nat A7::nat A8::nat A9::nat A10::nat A11::nat A12::nat A13::nat |
|
337 |
A14::nat A15::nat A16::nat A17::nat A18::nat A19::nat A20::nat |
|
338 |
A21::nat A22::nat A23::nat A24::nat A25::nat A26::nat A27::nat |
|
339 |
A28::nat A29::nat A30::nat A31::nat A32::nat A33::nat A34::nat |
|
340 |
A35::nat A36::nat A37::nat A38::nat A39::nat A40::nat A41::nat |
|
341 |
A42::nat A43::nat A44::nat A45::nat A46::nat A47::nat A48::nat |
|
342 |
A49::nat A50::nat A51::nat A52::nat A53::nat A54::nat A55::nat |
|
343 |
A56::nat A57::nat A58::nat A59::nat A60::nat A61::nat A62::nat |
|
344 |
A63::nat A64::nat A65::nat A66::nat A67::nat A68::nat A69::nat |
|
345 |
A70::nat A71::nat A72::nat A73::nat A74::nat A75::nat A76::nat |
|
346 |
A77::nat A78::nat A79::nat A80::nat A81::nat A82::nat A83::nat |
|
347 |
A84::nat A85::nat A86::nat A87::nat A88::nat A89::nat A90::nat |
|
348 |
A91::nat A92::nat A93::nat A94::nat A95::nat A96::nat A97::nat |
|
349 |
A98::nat A99::nat A100::nat A101::nat A102::nat A103::nat A104::nat |
|
350 |
A105::nat A106::nat A107::nat A108::nat A109::nat A110::nat A111::nat |
|
351 |
A112::nat A113::nat A114::nat A115::nat A116::nat A117::nat A118::nat |
|
352 |
A119::nat A120::nat A121::nat A122::nat A123::nat A124::nat A125::nat |
|
353 |
A126::nat A127::nat A128::nat A129::nat A130::nat A131::nat A132::nat |
|
354 |
A133::nat A134::nat A135::nat A136::nat A137::nat A138::nat A139::nat |
|
355 |
A140::nat A141::nat A142::nat A143::nat A144::nat A145::nat A146::nat |
|
356 |
A147::nat A148::nat A149::nat A150::nat A151::nat A152::nat A153::nat |
|
357 |
A154::nat A155::nat A156::nat A157::nat A158::nat A159::nat A160::nat |
|
358 |
A161::nat A162::nat A163::nat A164::nat A165::nat A166::nat A167::nat |
|
359 |
A168::nat A169::nat A170::nat A171::nat A172::nat A173::nat A174::nat |
|
360 |
A175::nat A176::nat A177::nat A178::nat A179::nat A180::nat A181::nat |
|
361 |
A182::nat A183::nat A184::nat A185::nat A186::nat A187::nat A188::nat |
|
362 |
A189::nat A190::nat A191::nat A192::nat A193::nat A194::nat A195::nat |
|
363 |
A196::nat A197::nat A198::nat A199::nat A200::nat A201::nat A202::nat |
|
364 |
A203::nat A204::nat A205::nat A206::nat A207::nat A208::nat A209::nat |
|
365 |
A210::nat A211::nat A212::nat A213::nat A214::nat A215::nat A216::nat |
|
366 |
A217::nat A218::nat A219::nat A220::nat A221::nat A222::nat A223::nat |
|
367 |
A224::nat A225::nat A226::nat A227::nat A228::nat A229::nat A230::nat |
|
368 |
A231::nat A232::nat A233::nat A234::nat A235::nat A236::nat A237::nat |
|
369 |
A238::nat A239::nat A240::nat A241::nat A242::nat A243::nat A244::nat |
|
370 |
A245::nat A246::nat A247::nat A248::nat A249::nat A250::nat A251::nat |
|
371 |
A252::nat A253::nat A254::nat A255::nat A256::nat A257::nat A258::nat |
|
372 |
A259::nat A260::nat A261::nat A262::nat A263::nat A264::nat A265::nat |
|
373 |
A266::nat A267::nat A268::nat A269::nat A270::nat A271::nat A272::nat |
|
374 |
A273::nat A274::nat A275::nat A276::nat A277::nat A278::nat A279::nat |
|
375 |
A280::nat A281::nat A282::nat A283::nat A284::nat A285::nat A286::nat |
|
376 |
A287::nat A288::nat A289::nat A290::nat A291::nat A292::nat A293::nat |
|
377 |
A294::nat A295::nat A296::nat A297::nat A298::nat A299::nat A300::nat |
|
378 |
A301::nat A302::nat A303::nat A304::nat A305::nat A306::nat A307::nat |
|
379 |
A308::nat A309::nat A310::nat A311::nat A312::nat A313::nat A314::nat |
|
380 |
A315::nat A316::nat A317::nat A318::nat A319::nat A320::nat A321::nat |
|
381 |
A322::nat A323::nat A324::nat A325::nat A326::nat A327::nat A328::nat |
|
382 |
A329::nat A330::nat A331::nat A332::nat A333::nat A334::nat A335::nat |
|
383 |
A336::nat A337::nat A338::nat A339::nat A340::nat A341::nat A342::nat |
|
384 |
A343::nat A344::nat A345::nat A346::nat A347::nat A348::nat A349::nat |
|
385 |
A350::nat A351::nat A352::nat A353::nat A354::nat A355::nat A356::nat |
|
386 |
A357::nat A358::nat A359::nat A360::nat A361::nat A362::nat A363::nat |
|
387 |
A364::nat A365::nat A366::nat A367::nat A368::nat A369::nat A370::nat |
|
388 |
A371::nat A372::nat A373::nat A374::nat A375::nat A376::nat A377::nat |
|
389 |
A378::nat A379::nat A380::nat A381::nat A382::nat A383::nat A384::nat |
|
390 |
A385::nat A386::nat A387::nat A388::nat A389::nat A390::nat A391::nat |
|
391 |
A392::nat A393::nat A394::nat A395::nat A396::nat A397::nat A398::nat |
|
392 |
A399::nat A400::nat A401::nat A402::nat A403::nat A404::nat A405::nat |
|
393 |
A406::nat A407::nat A408::nat A409::nat A410::nat A411::nat A412::nat |
|
394 |
A413::nat A414::nat A415::nat A416::nat A417::nat A418::nat A419::nat |
|
395 |
A420::nat A421::nat A422::nat A423::nat A424::nat A425::nat A426::nat |
|
396 |
A427::nat A428::nat A429::nat A430::nat A431::nat A432::nat A433::nat |
|
397 |
A434::nat A435::nat A436::nat A437::nat A438::nat A439::nat A440::nat |
|
398 |
A441::nat A442::nat A443::nat A444::nat A445::nat A446::nat A447::nat |
|
399 |
A448::nat A449::nat A450::nat A451::nat A452::nat A453::nat A454::nat |
|
400 |
A455::nat A456::nat A457::nat A458::nat A459::nat A460::nat A461::nat |
|
401 |
A462::nat A463::nat A464::nat A465::nat A466::nat A467::nat A468::nat |
|
402 |
A469::nat A470::nat A471::nat A472::nat A473::nat A474::nat A475::nat |
|
403 |
A476::nat A477::nat A478::nat A479::nat A480::nat A481::nat A482::nat |
|
404 |
A483::nat A484::nat A485::nat A486::nat A487::nat A488::nat A489::nat |
|
405 |
A490::nat A491::nat A492::nat A493::nat A494::nat A495::nat A496::nat |
|
406 |
A497::nat A498::nat A499::nat A500::nat A501::nat A502::nat A503::nat |
|
407 |
A504::nat A505::nat A506::nat A507::nat A508::nat A509::nat A510::nat |
|
408 |
A511::nat A512::nat A513::nat A514::nat A515::nat A516::nat A517::nat |
|
409 |
A518::nat A519::nat A520::nat A521::nat A522::nat A523::nat A524::nat |
|
410 |
A525::nat A526::nat A527::nat A528::nat A529::nat A530::nat A531::nat |
|
411 |
A532::nat A533::nat A534::nat A535::nat A536::nat A537::nat A538::nat |
|
412 |
A539::nat A540::nat A541::nat A542::nat A543::nat A544::nat A545::nat |
|
413 |
A546::nat A547::nat A548::nat A549::nat A550::nat A551::nat A552::nat |
|
414 |
A553::nat A554::nat A555::nat A556::nat A557::nat A558::nat A559::nat |
|
415 |
A560::nat A561::nat A562::nat A563::nat A564::nat A565::nat A566::nat |
|
416 |
A567::nat A568::nat A569::nat A570::nat A571::nat A572::nat A573::nat |
|
417 |
A574::nat A575::nat A576::nat A577::nat A578::nat A579::nat A580::nat |
|
418 |
A581::nat A582::nat A583::nat A584::nat A585::nat A586::nat A587::nat |
|
419 |
A588::nat A589::nat A590::nat A591::nat A592::nat A593::nat A594::nat |
|
420 |
A595::nat A596::nat A597::nat A598::nat A599::nat A600::nat A601::nat |
|
421 |
A602::nat A603::nat A604::nat A605::nat A606::nat A607::nat A608::nat |
|
422 |
A609::nat A610::nat A611::nat A612::nat A613::nat A614::nat A615::nat |
|
423 |
A616::nat A617::nat A618::nat A619::nat A620::nat A621::nat A622::nat |
|
424 |
A623::nat A624::nat A625::nat A626::nat A627::nat A628::nat A629::nat |
|
425 |
A630::nat A631::nat A632::nat A633::nat A634::nat A635::nat A636::nat |
|
426 |
A637::nat A638::nat A639::nat A640::nat A641::nat A642::nat A643::nat |
|
427 |
A644::nat A645::nat A646::nat A647::nat A648::nat A649::nat A650::nat |
|
428 |
A651::nat A652::nat A653::nat A654::nat A655::nat A656::nat A657::nat |
|
429 |
A658::nat A659::nat A660::nat A661::nat A662::nat A663::nat A664::nat |
|
430 |
A665::nat A666::nat A667::nat A668::nat A669::nat A670::nat A671::nat |
|
431 |
A672::nat A673::nat A674::nat A675::nat A676::nat A677::nat A678::nat |
|
432 |
A679::nat A680::nat A681::nat A682::nat A683::nat A684::nat A685::nat |
|
433 |
A686::nat A687::nat A688::nat A689::nat A690::nat A691::nat A692::nat |
|
434 |
A693::nat A694::nat A695::nat A696::nat A697::nat A698::nat A699::nat |
|
435 |
A700::nat A701::nat A702::nat A703::nat A704::nat A705::nat A706::nat |
|
436 |
A707::nat A708::nat A709::nat A710::nat A711::nat A712::nat A713::nat |
|
437 |
A714::nat A715::nat A716::nat A717::nat A718::nat A719::nat A720::nat |
|
438 |
A721::nat A722::nat A723::nat A724::nat A725::nat A726::nat A727::nat |
|
439 |
A728::nat A729::nat A730::nat A731::nat A732::nat A733::nat A734::nat |
|
440 |
A735::nat A736::nat A737::nat A738::nat A739::nat A740::nat A741::nat |
|
441 |
A742::nat A743::nat A744::nat A745::nat A746::nat A747::nat A748::nat |
|
442 |
A749::nat A750::nat A751::nat A752::nat A753::nat A754::nat A755::nat |
|
443 |
A756::nat A757::nat A758::nat A759::nat A760::nat A761::nat A762::nat |
|
444 |
A763::nat A764::nat A765::nat A766::nat A767::nat A768::nat A769::nat |
|
445 |
A770::nat A771::nat A772::nat A773::nat A774::nat A775::nat A776::nat |
|
446 |
A777::nat A778::nat A779::nat A780::nat A781::nat A782::nat A783::nat |
|
447 |
A784::nat A785::nat A786::nat A787::nat A788::nat A789::nat A790::nat |
|
448 |
A791::nat A792::nat A793::nat A794::nat A795::nat A796::nat A797::nat |
|
449 |
A798::nat A799::nat A800::nat A801::nat A802::nat A803::nat A804::nat |
|
450 |
A805::nat A806::nat A807::nat A808::nat A809::nat A810::nat A811::nat |
|
451 |
A812::nat A813::nat A814::nat A815::nat A816::nat A817::nat A818::nat |
|
452 |
A819::nat A820::nat A821::nat A822::nat A823::nat A824::nat A825::nat |
|
453 |
A826::nat A827::nat A828::nat A829::nat A830::nat A831::nat A832::nat |
|
454 |
A833::nat A834::nat A835::nat A836::nat A837::nat A838::nat A839::nat |
|
455 |
A840::nat A841::nat A842::nat A843::nat A844::nat A845::nat A846::nat |
|
456 |
A847::nat A848::nat A849::nat A850::nat A851::nat A852::nat A853::nat |
|
457 |
A854::nat A855::nat A856::nat A857::nat A858::nat A859::nat A860::nat |
|
458 |
A861::nat A862::nat A863::nat A864::nat A865::nat A866::nat A867::nat |
|
459 |
A868::nat A869::nat A870::nat A871::nat A872::nat A873::nat A874::nat |
|
460 |
A875::nat A876::nat A877::nat A878::nat A879::nat A880::nat A881::nat |
|
461 |
A882::nat A883::nat A884::nat A885::nat A886::nat A887::nat A888::nat |
|
462 |
A889::nat A890::nat A891::nat A892::nat A893::nat A894::nat A895::nat |
|
463 |
A896::nat A897::nat A898::nat A899::nat A900::nat A901::nat A902::nat |
|
464 |
A903::nat A904::nat A905::nat A906::nat A907::nat A908::nat A909::nat |
|
465 |
A910::nat A911::nat A912::nat A913::nat A914::nat A915::nat A916::nat |
|
466 |
A917::nat A918::nat A919::nat A920::nat A921::nat A922::nat A923::nat |
|
467 |
A924::nat A925::nat A926::nat A927::nat A928::nat A929::nat A930::nat |
|
468 |
A931::nat A932::nat A933::nat A934::nat A935::nat A936::nat A937::nat |
|
469 |
A938::nat A939::nat A940::nat A941::nat A942::nat A943::nat A944::nat |
|
470 |
A945::nat A946::nat A947::nat A948::nat A949::nat A950::nat A951::nat |
|
471 |
A952::nat A953::nat A954::nat A955::nat A956::nat A957::nat A958::nat |
|
472 |
A959::nat A960::nat A961::nat A962::nat A963::nat A964::nat A965::nat |
|
473 |
A966::nat A967::nat A968::nat A969::nat A970::nat A971::nat A972::nat |
|
474 |
A973::nat A974::nat A975::nat A976::nat A977::nat A978::nat A979::nat |
|
475 |
A980::nat A981::nat A982::nat A983::nat A984::nat A985::nat A986::nat |
|
476 |
A987::nat A988::nat A989::nat A990::nat A991::nat A992::nat A993::nat |
|
477 |
A994::nat A995::nat A996::nat A997::nat A998::nat A999::nat A1000::nat |
|
478 |
||
45394 | 479 |
lemma (in benchmark100) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp |
480 |
lemma (in benchmark500) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp |
|
481 |
lemma (in benchmark1000) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp |
|
482 |
||
25171 | 483 |
end |