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