25171
|
1 |
(* Title: StateSpaceEx.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Norbert Schirmer, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Examples \label{sec:Examples} *}
|
|
7 |
theory StateSpaceEx
|
|
8 |
imports StateSpaceLocale StateSpaceSyntax
|
|
9 |
|
|
10 |
begin
|
|
11 |
(* FIXME: Use proper keywords file *)
|
|
12 |
(*<*)
|
|
13 |
syntax
|
|
14 |
"_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900)
|
|
15 |
(*>*)
|
|
16 |
|
|
17 |
text {* Did you ever dream about records with multiple inheritance.
|
|
18 |
Then you should definitely have a look at statespaces. They may be
|
|
19 |
what you are dreaming of. Or at least almost...
|
|
20 |
*}
|
|
21 |
|
|
22 |
|
|
23 |
|
|
24 |
|
|
25 |
text {* Isabelle allows to add new top-level commands to the
|
|
26 |
system. Building on the locale infrastructure, we provide a command
|
|
27 |
\isacommand{statespace} like this:*}
|
|
28 |
|
|
29 |
statespace vars =
|
|
30 |
n::nat
|
|
31 |
b::bool
|
|
32 |
|
|
33 |
text {* \noindent This resembles a \isacommand{record} definition,
|
|
34 |
but introduces sophisticated locale
|
|
35 |
infrastructure instead of HOL type schemes. The resulting context
|
|
36 |
postulates two distinct names @{term "n"} and @{term "b"} and
|
|
37 |
projection~/ injection functions that convert from abstract values to
|
|
38 |
@{typ "nat"} and @{text "bool"}. The logical content of the locale is: *}
|
|
39 |
|
|
40 |
locale vars' =
|
|
41 |
fixes n::'name and b::'name
|
|
42 |
assumes "distinct [n, b]"
|
|
43 |
|
|
44 |
fixes project_nat::"'value \<Rightarrow> nat" and inject_nat::"nat \<Rightarrow> 'value"
|
|
45 |
assumes "\<And>n. project_nat (inject_nat n) = n"
|
|
46 |
|
|
47 |
fixes project_bool::"'value \<Rightarrow> bool" and inject_bool::"bool \<Rightarrow> 'value"
|
|
48 |
assumes "\<And>b. project_bool (inject_bool b) = b"
|
|
49 |
|
|
50 |
text {* \noindent The HOL predicate @{const "distinct"} describes
|
|
51 |
distinctness of all names in the context. Locale @{text "vars'"}
|
|
52 |
defines the raw logical content that is defined in the state space
|
|
53 |
locale. We also maintain non-logical context information to support
|
|
54 |
the user:
|
|
55 |
|
|
56 |
\begin{itemize}
|
|
57 |
|
|
58 |
\item Syntax for state lookup and updates that automatically inserts
|
|
59 |
the corresponding projection and injection functions.
|
|
60 |
|
|
61 |
\item Setup for the proof tools that exploit the distinctness
|
|
62 |
information and the cancellation of projections and injections in
|
|
63 |
deductions and simplifications.
|
|
64 |
|
|
65 |
\end{itemize}
|
|
66 |
|
|
67 |
This extra-logical information is added to the locale in form of
|
|
68 |
declarations, which associate the name of a variable to the
|
|
69 |
corresponding projection and injection functions to handle the syntax
|
|
70 |
transformations, and a link from the variable name to the
|
|
71 |
corresponding distinctness theorem. As state spaces are merged or
|
|
72 |
extended there are multiple distinctness theorems in the context. Our
|
|
73 |
declarations take care that the link always points to the strongest
|
|
74 |
distinctness assumption. With these declarations in place, a lookup
|
|
75 |
can be written as @{text "s\<cdot>n"}, which is translated to @{text
|
|
76 |
"project_nat (s n)"}, and an update as @{text "s\<langle>n := 2\<rangle>"}, which is
|
|
77 |
translated to @{text "s(n := inject_nat 2)"}. We can now establish the
|
|
78 |
following lemma: *}
|
|
79 |
|
|
80 |
lemma (in vars) foo: "s<n := 2>\<cdot>b = s\<cdot>b" by simp
|
|
81 |
|
|
82 |
text {* \noindent Here the simplifier was able to refer to
|
|
83 |
distinctness of @{term "b"} and @{term "n"} to solve the equation.
|
|
84 |
The resulting lemma is also recorded in locale @{text "vars"} for
|
|
85 |
later use and is automatically propagated to all its interpretations.
|
|
86 |
Here is another example: *}
|
|
87 |
|
|
88 |
statespace 'a varsX = vars [n=N, b=B] + vars + x::'a
|
|
89 |
|
|
90 |
text {* \noindent The state space @{text "varsX"} imports two copies
|
|
91 |
of the state space @{text "vars"}, where one has the variables renamed
|
|
92 |
to upper-case letters, and adds another variable @{term "x"} of type
|
|
93 |
@{typ "'a"}. This type is fixed inside the state space but may get
|
|
94 |
instantiated later on, analogous to type parameters of an ML-functor.
|
|
95 |
The distinctness assumption is now @{text "distinct [N, B, n, b, x]"},
|
|
96 |
from this we can derive both @{term "distinct [N,B]"} and @{term
|
|
97 |
"distinct [n,b]"}, the distinction assumptions for the two versions of
|
|
98 |
locale @{text "vars"} above. Moreover we have all necessary
|
|
99 |
projection and injection assumptions available. These assumptions
|
|
100 |
together allow us to establish state space @{term "varsX"} as an
|
|
101 |
interpretation of both instances of locale @{term "vars"}. Hence we
|
|
102 |
inherit both variants of theorem @{text "foo"}: @{text "s\<langle>N := 2\<rangle>\<cdot>B =
|
|
103 |
s\<cdot>B"} as well as @{text "s\<langle>n := 2\<rangle>\<cdot>b = s\<cdot>b"}. These are immediate
|
|
104 |
consequences of the locale interpretation action.
|
|
105 |
|
|
106 |
The declarations for syntax and the distinctness theorems also observe
|
|
107 |
the morphisms generated by the locale package due to the renaming
|
|
108 |
@{term "n = N"}: *}
|
|
109 |
|
|
110 |
lemma (in varsX) foo: "s\<langle>N := 2\<rangle>\<cdot>x = s\<cdot>x" by simp
|
|
111 |
|
|
112 |
text {* To assure scalability towards many distinct names, the
|
|
113 |
distinctness predicate is refined to operate on balanced trees. Thus
|
|
114 |
we get logarithmic certificates for the distinctness of two names by
|
|
115 |
the distinctness of the paths in the tree. Asked for the distinctness
|
|
116 |
of two names, our tool produces the paths of the variables in the tree
|
|
117 |
(this is implemented in SML, outside the logic) and returns a
|
|
118 |
certificate corresponding to the different paths. Merging state
|
|
119 |
spaces requires to prove that the combined distinctness assumption
|
|
120 |
implies the distinctness assumptions of the components. Such a proof
|
|
121 |
is of the order $m \cdot \log n$, where $n$ and $m$ are the number of
|
|
122 |
nodes in the larger and smaller tree, respectively.*}
|
|
123 |
|
|
124 |
text {* We continue with more examples. *}
|
|
125 |
|
|
126 |
statespace 'a foo =
|
|
127 |
f::"nat\<Rightarrow>nat"
|
|
128 |
a::int
|
|
129 |
b::nat
|
|
130 |
c::'a
|
|
131 |
|
|
132 |
|
|
133 |
|
|
134 |
lemma (in foo) foo1:
|
|
135 |
shows "s\<langle>a := i\<rangle>\<cdot>a = i"
|
|
136 |
by simp
|
|
137 |
|
|
138 |
lemma (in foo) foo2:
|
|
139 |
shows "(s\<langle>a:=i\<rangle>)\<cdot>a = i"
|
|
140 |
by simp
|
|
141 |
|
|
142 |
lemma (in foo) foo3:
|
|
143 |
shows "(s\<langle>a:=i\<rangle>)\<cdot>b = s\<cdot>b"
|
|
144 |
by simp
|
|
145 |
|
|
146 |
lemma (in foo) foo4:
|
|
147 |
shows "(s\<langle>a:=i,b:=j,c:=k,a:=x\<rangle>) = (s\<langle>b:=j,c:=k,a:=x\<rangle>)"
|
|
148 |
by simp
|
|
149 |
|
|
150 |
statespace bar =
|
|
151 |
b::bool
|
|
152 |
c::string
|
|
153 |
|
|
154 |
lemma (in bar) bar1:
|
|
155 |
shows "(s\<langle>b:=True\<rangle>)\<cdot>c = s\<cdot>c"
|
|
156 |
by simp
|
|
157 |
|
|
158 |
text {* You can define a derived state space by inheriting existing state spaces, renaming
|
|
159 |
of components if you like, and by declaring new components.
|
|
160 |
*}
|
|
161 |
|
|
162 |
statespace ('a,'b) loo = 'a foo + bar [b=B,c=C] +
|
|
163 |
X::'b
|
|
164 |
|
|
165 |
lemma (in loo) loo1:
|
|
166 |
shows "s\<langle>a:=i\<rangle>\<cdot>B = s\<cdot>B"
|
|
167 |
proof -
|
|
168 |
thm foo1
|
|
169 |
txt {* The Lemma @{thm [source] foo1} from the parent state space
|
|
170 |
is also available here: \begin{center}@{thm foo1}\end{center}.*}
|
|
171 |
have "s<a:=i>\<cdot>a = i"
|
|
172 |
by (rule foo1)
|
|
173 |
thm bar1
|
|
174 |
txt {* Note the renaming of the parameters in Lemma @{thm [source] bar1}:
|
|
175 |
\begin{center}@{thm bar1}\end{center}.*}
|
|
176 |
have "s<B:=True>\<cdot>C = s\<cdot>C"
|
|
177 |
by (rule bar1)
|
|
178 |
show ?thesis
|
|
179 |
by simp
|
|
180 |
qed
|
|
181 |
|
|
182 |
|
|
183 |
statespace 'a dup = 'a foo [f=F, a=A] + 'a foo +
|
|
184 |
x::int
|
|
185 |
|
|
186 |
lemma (in dup)
|
|
187 |
shows "s<a := i>\<cdot>x = s\<cdot>x"
|
|
188 |
by simp
|
|
189 |
|
|
190 |
lemma (in dup)
|
|
191 |
shows "s<A := i>\<cdot>a = s\<cdot>a"
|
|
192 |
by simp
|
|
193 |
|
|
194 |
lemma (in dup)
|
|
195 |
shows "s<A := i>\<cdot>x = s\<cdot>x"
|
|
196 |
by simp
|
|
197 |
|
|
198 |
|
|
199 |
text {* There are known problems with syntax-declarations. They currently
|
|
200 |
only work, when the context is already built. Hopefully this will be
|
|
201 |
implemented correctly in future Isabelle versions. *}
|
|
202 |
|
|
203 |
lemma
|
|
204 |
includes foo
|
|
205 |
shows True
|
|
206 |
term "s<a := i>\<cdot>a = i"
|
|
207 |
by simp
|
|
208 |
|
|
209 |
(*
|
|
210 |
lemma
|
|
211 |
includes foo
|
|
212 |
shows "s<a := i>\<cdot>a = i"
|
|
213 |
*)
|
|
214 |
|
|
215 |
text {* It would be nice to have nested state spaces. This is
|
|
216 |
logically no problem. From the locale-implementation side this may be
|
|
217 |
something like an 'includes' into a locale. When there is a more
|
|
218 |
elaborate locale infrastructure in place this may be an easy exercise.
|
|
219 |
*}
|
|
220 |
|
|
221 |
end
|