src/HOL/Statespace/StateSpaceEx.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 38838 62f6ba39b3d4
child 41959 b460124855b8
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 (*  Title:      StateSpaceEx.thy
     2     Author:     Norbert Schirmer, TU Muenchen
     3 *)
     4 
     5 header {* Examples \label{sec:Examples} *}
     6 theory StateSpaceEx
     7 imports StateSpaceLocale StateSpaceSyntax
     8 begin
     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 
    31 print_locale vars_namespace
    32 print_locale vars_valuetypes
    33 print_locale vars
    34 
    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 
    42 locale vars' =
    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 
   201 text {* Hmm, I hoped this would work now...*}
   202 
   203 (*
   204 locale fooX = foo +
   205  assumes "s<a:=i>\<cdot>b = k"
   206 *)
   207 
   208 (* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *)
   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 
   213 (*
   214 lemma 
   215   assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
   216   shows True
   217 proof
   218   interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
   219   term "s<a := i>\<cdot>a = i"
   220 qed
   221 *)
   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