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