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