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