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