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