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