src/HOL/Statespace/StateSpaceEx.thy
author ballarin
Thu Oct 16 17:19:47 2008 +0200 (2008-10-16)
changeset 28611 983c1855a7af
parent 25171 4a9c25bffc9b
child 29235 2d62b637fa80
permissions -rw-r--r--
More occurrences of 'includes' gone.
     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   assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
   205   shows True
   206 proof
   207   interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
   208   term "s<a := i>\<cdot>a = i"
   209 qed
   210 
   211 (*
   212 lemma 
   213   includes foo
   214   shows "s<a := i>\<cdot>a = i"
   215 *)
   216 
   217 text {* It would be nice to have nested state spaces. This is
   218 logically no problem. From the locale-implementation side this may be
   219 something like an 'includes' into a locale. When there is a more
   220 elaborate locale infrastructure in place this may be an easy exercise.
   221 *} 
   222 
   223 end