summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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 *)

6 header {* Examples \label{sec:Examples} *}

7 theory StateSpaceEx

8 imports StateSpaceLocale StateSpaceSyntax

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 (*>*)

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 *}

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:*}

29 statespace vars =

30 n::nat

31 b::bool

33 print_locale vars_namespace

34 print_locale vars_valuetypes

35 print_locale vars

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: *}

44 class_locale vars' =

45 fixes n::'name and b::'name

46 assumes "distinct [n, b]"

48 fixes project_nat::"'value \<Rightarrow> nat" and inject_nat::"nat \<Rightarrow> 'value"

49 assumes "\<And>n. project_nat (inject_nat n) = n"

51 fixes project_bool::"'value \<Rightarrow> bool" and inject_bool::"bool \<Rightarrow> 'value"

52 assumes "\<And>b. project_bool (inject_bool b) = b"

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:

60 \begin{itemize}

62 \item Syntax for state lookup and updates that automatically inserts

63 the corresponding projection and injection functions.

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.

69 \end{itemize}

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: *}

84 lemma (in vars) foo: "s<n := 2>\<cdot>b = s\<cdot>b" by simp

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: *}

92 statespace 'a varsX = vars [n=N, b=B] + vars + x::'a

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.

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"}: *}

114 lemma (in varsX) foo: "s\<langle>N := 2\<rangle>\<cdot>x = s\<cdot>x" by simp

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.*}

128 text {* We continue with more examples. *}

130 statespace 'a foo =

131 f::"nat\<Rightarrow>nat"

132 a::int

133 b::nat

134 c::'a

138 lemma (in foo) foo1:

139 shows "s\<langle>a := i\<rangle>\<cdot>a = i"

140 by simp

142 lemma (in foo) foo2:

143 shows "(s\<langle>a:=i\<rangle>)\<cdot>a = i"

144 by simp

146 lemma (in foo) foo3:

147 shows "(s\<langle>a:=i\<rangle>)\<cdot>b = s\<cdot>b"

148 by simp

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

154 statespace bar =

155 b::bool

156 c::string

158 lemma (in bar) bar1:

159 shows "(s\<langle>b:=True\<rangle>)\<cdot>c = s\<cdot>c"

160 by simp

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 *}

166 statespace ('a,'b) loo = 'a foo + bar [b=B,c=C] +

167 X::'b

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

187 statespace 'a dup = 'a foo [f=F, a=A] + 'a foo +

188 x::int

190 lemma (in dup)

191 shows "s<a := i>\<cdot>x = s\<cdot>x"

192 by simp

194 lemma (in dup)

195 shows "s<A := i>\<cdot>a = s\<cdot>a"

196 by simp

198 lemma (in dup)

199 shows "s<A := i>\<cdot>x = s\<cdot>x"

200 by simp

203 text {* Hmm, I hoped this would work now...*}

205 (*

206 locale fooX = foo +

207 assumes "s<a:=i>\<cdot>b = k"

208 *)

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. *}

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 *)

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 *}

236 end