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