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