summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Statespace/StateSpaceEx.thy

changeset 25171 | 4a9c25bffc9b |

child 28611 | 983c1855a7af |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 24 18:36:09 2007 +0200 1.3 @@ -0,0 +1,221 @@ 1.4 +(* Title: StateSpaceEx.thy 1.5 + ID: $Id$ 1.6 + Author: Norbert Schirmer, TU Muenchen 1.7 +*) 1.8 + 1.9 +header {* Examples \label{sec:Examples} *} 1.10 +theory StateSpaceEx 1.11 +imports StateSpaceLocale StateSpaceSyntax 1.12 + 1.13 +begin 1.14 +(* FIXME: Use proper keywords file *) 1.15 +(*<*) 1.16 +syntax 1.17 + "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900) 1.18 +(*>*) 1.19 + 1.20 +text {* Did you ever dream about records with multiple inheritance. 1.21 +Then you should definitely have a look at statespaces. They may be 1.22 +what you are dreaming of. Or at least almost... 1.23 +*} 1.24 + 1.25 + 1.26 + 1.27 + 1.28 +text {* Isabelle allows to add new top-level commands to the 1.29 +system. Building on the locale infrastructure, we provide a command 1.30 +\isacommand{statespace} like this:*} 1.31 + 1.32 +statespace vars = 1.33 + n::nat 1.34 + b::bool 1.35 + 1.36 +text {* \noindent This resembles a \isacommand{record} definition, 1.37 +but introduces sophisticated locale 1.38 +infrastructure instead of HOL type schemes. The resulting context 1.39 +postulates two distinct names @{term "n"} and @{term "b"} and 1.40 +projection~/ injection functions that convert from abstract values to 1.41 +@{typ "nat"} and @{text "bool"}. The logical content of the locale is: *} 1.42 + 1.43 +locale vars' = 1.44 + fixes n::'name and b::'name 1.45 + assumes "distinct [n, b]" 1.46 + 1.47 + fixes project_nat::"'value \<Rightarrow> nat" and inject_nat::"nat \<Rightarrow> 'value" 1.48 + assumes "\<And>n. project_nat (inject_nat n) = n" 1.49 + 1.50 + fixes project_bool::"'value \<Rightarrow> bool" and inject_bool::"bool \<Rightarrow> 'value" 1.51 + assumes "\<And>b. project_bool (inject_bool b) = b" 1.52 + 1.53 +text {* \noindent The HOL predicate @{const "distinct"} describes 1.54 +distinctness of all names in the context. Locale @{text "vars'"} 1.55 +defines the raw logical content that is defined in the state space 1.56 +locale. We also maintain non-logical context information to support 1.57 +the user: 1.58 + 1.59 +\begin{itemize} 1.60 + 1.61 +\item Syntax for state lookup and updates that automatically inserts 1.62 +the corresponding projection and injection functions. 1.63 + 1.64 +\item Setup for the proof tools that exploit the distinctness 1.65 +information and the cancellation of projections and injections in 1.66 +deductions and simplifications. 1.67 + 1.68 +\end{itemize} 1.69 + 1.70 +This extra-logical information is added to the locale in form of 1.71 +declarations, which associate the name of a variable to the 1.72 +corresponding projection and injection functions to handle the syntax 1.73 +transformations, and a link from the variable name to the 1.74 +corresponding distinctness theorem. As state spaces are merged or 1.75 +extended there are multiple distinctness theorems in the context. Our 1.76 +declarations take care that the link always points to the strongest 1.77 +distinctness assumption. With these declarations in place, a lookup 1.78 +can be written as @{text "s\<cdot>n"}, which is translated to @{text 1.79 +"project_nat (s n)"}, and an update as @{text "s\<langle>n := 2\<rangle>"}, which is 1.80 +translated to @{text "s(n := inject_nat 2)"}. We can now establish the 1.81 +following lemma: *} 1.82 + 1.83 +lemma (in vars) foo: "s<n := 2>\<cdot>b = s\<cdot>b" by simp 1.84 + 1.85 +text {* \noindent Here the simplifier was able to refer to 1.86 +distinctness of @{term "b"} and @{term "n"} to solve the equation. 1.87 +The resulting lemma is also recorded in locale @{text "vars"} for 1.88 +later use and is automatically propagated to all its interpretations. 1.89 +Here is another example: *} 1.90 + 1.91 +statespace 'a varsX = vars [n=N, b=B] + vars + x::'a 1.92 + 1.93 +text {* \noindent The state space @{text "varsX"} imports two copies 1.94 +of the state space @{text "vars"}, where one has the variables renamed 1.95 +to upper-case letters, and adds another variable @{term "x"} of type 1.96 +@{typ "'a"}. This type is fixed inside the state space but may get 1.97 +instantiated later on, analogous to type parameters of an ML-functor. 1.98 +The distinctness assumption is now @{text "distinct [N, B, n, b, x]"}, 1.99 +from this we can derive both @{term "distinct [N,B]"} and @{term 1.100 +"distinct [n,b]"}, the distinction assumptions for the two versions of 1.101 +locale @{text "vars"} above. Moreover we have all necessary 1.102 +projection and injection assumptions available. These assumptions 1.103 +together allow us to establish state space @{term "varsX"} as an 1.104 +interpretation of both instances of locale @{term "vars"}. Hence we 1.105 +inherit both variants of theorem @{text "foo"}: @{text "s\<langle>N := 2\<rangle>\<cdot>B = 1.106 +s\<cdot>B"} as well as @{text "s\<langle>n := 2\<rangle>\<cdot>b = s\<cdot>b"}. These are immediate 1.107 +consequences of the locale interpretation action. 1.108 + 1.109 +The declarations for syntax and the distinctness theorems also observe 1.110 +the morphisms generated by the locale package due to the renaming 1.111 +@{term "n = N"}: *} 1.112 + 1.113 +lemma (in varsX) foo: "s\<langle>N := 2\<rangle>\<cdot>x = s\<cdot>x" by simp 1.114 + 1.115 +text {* To assure scalability towards many distinct names, the 1.116 +distinctness predicate is refined to operate on balanced trees. Thus 1.117 +we get logarithmic certificates for the distinctness of two names by 1.118 +the distinctness of the paths in the tree. Asked for the distinctness 1.119 +of two names, our tool produces the paths of the variables in the tree 1.120 +(this is implemented in SML, outside the logic) and returns a 1.121 +certificate corresponding to the different paths. Merging state 1.122 +spaces requires to prove that the combined distinctness assumption 1.123 +implies the distinctness assumptions of the components. Such a proof 1.124 +is of the order $m \cdot \log n$, where $n$ and $m$ are the number of 1.125 +nodes in the larger and smaller tree, respectively.*} 1.126 + 1.127 +text {* We continue with more examples. *} 1.128 + 1.129 +statespace 'a foo = 1.130 + f::"nat\<Rightarrow>nat" 1.131 + a::int 1.132 + b::nat 1.133 + c::'a 1.134 + 1.135 + 1.136 + 1.137 +lemma (in foo) foo1: 1.138 + shows "s\<langle>a := i\<rangle>\<cdot>a = i" 1.139 + by simp 1.140 + 1.141 +lemma (in foo) foo2: 1.142 + shows "(s\<langle>a:=i\<rangle>)\<cdot>a = i" 1.143 + by simp 1.144 + 1.145 +lemma (in foo) foo3: 1.146 + shows "(s\<langle>a:=i\<rangle>)\<cdot>b = s\<cdot>b" 1.147 + by simp 1.148 + 1.149 +lemma (in foo) foo4: 1.150 + shows "(s\<langle>a:=i,b:=j,c:=k,a:=x\<rangle>) = (s\<langle>b:=j,c:=k,a:=x\<rangle>)" 1.151 + by simp 1.152 + 1.153 +statespace bar = 1.154 + b::bool 1.155 + c::string 1.156 + 1.157 +lemma (in bar) bar1: 1.158 + shows "(s\<langle>b:=True\<rangle>)\<cdot>c = s\<cdot>c" 1.159 + by simp 1.160 + 1.161 +text {* You can define a derived state space by inheriting existing state spaces, renaming 1.162 +of components if you like, and by declaring new components. 1.163 +*} 1.164 + 1.165 +statespace ('a,'b) loo = 'a foo + bar [b=B,c=C] + 1.166 + X::'b 1.167 + 1.168 +lemma (in loo) loo1: 1.169 + shows "s\<langle>a:=i\<rangle>\<cdot>B = s\<cdot>B" 1.170 +proof - 1.171 + thm foo1 1.172 + txt {* The Lemma @{thm [source] foo1} from the parent state space 1.173 + is also available here: \begin{center}@{thm foo1}\end{center}.*} 1.174 + have "s<a:=i>\<cdot>a = i" 1.175 + by (rule foo1) 1.176 + thm bar1 1.177 + txt {* Note the renaming of the parameters in Lemma @{thm [source] bar1}: 1.178 + \begin{center}@{thm bar1}\end{center}.*} 1.179 + have "s<B:=True>\<cdot>C = s\<cdot>C" 1.180 + by (rule bar1) 1.181 + show ?thesis 1.182 + by simp 1.183 +qed 1.184 + 1.185 + 1.186 +statespace 'a dup = 'a foo [f=F, a=A] + 'a foo + 1.187 + x::int 1.188 + 1.189 +lemma (in dup) 1.190 + shows "s<a := i>\<cdot>x = s\<cdot>x" 1.191 + by simp 1.192 + 1.193 +lemma (in dup) 1.194 + shows "s<A := i>\<cdot>a = s\<cdot>a" 1.195 + by simp 1.196 + 1.197 +lemma (in dup) 1.198 + shows "s<A := i>\<cdot>x = s\<cdot>x" 1.199 + by simp 1.200 + 1.201 + 1.202 +text {* There are known problems with syntax-declarations. They currently 1.203 +only work, when the context is already built. Hopefully this will be 1.204 +implemented correctly in future Isabelle versions. *} 1.205 + 1.206 +lemma 1.207 + includes foo 1.208 + shows True 1.209 + term "s<a := i>\<cdot>a = i" 1.210 + by simp 1.211 + 1.212 +(* 1.213 +lemma 1.214 + includes foo 1.215 + shows "s<a := i>\<cdot>a = i" 1.216 +*) 1.217 + 1.218 +text {* It would be nice to have nested state spaces. This is 1.219 +logically no problem. From the locale-implementation side this may be 1.220 +something like an 'includes' into a locale. When there is a more 1.221 +elaborate locale infrastructure in place this may be an easy exercise. 1.222 +*} 1.223 + 1.224 +end