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

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

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

6 theory StateSpaceEx

7 imports StateSpaceLocale StateSpaceSyntax

8 begin

10 (*<*)

11 syntax

12 "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900)

13 (*>*)

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

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

27 statespace vars =

28 n::nat

29 b::bool

31 print_locale vars_namespace

32 print_locale vars_valuetypes

33 print_locale vars

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

42 locale vars' =

43 fixes n::'name and b::'name

44 assumes "distinct [n, b]"

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

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

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

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

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:

58 \begin{itemize}

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

61 the corresponding projection and injection functions.

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.

67 \end{itemize}

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

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

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

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

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.

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

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

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

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

128 statespace 'a foo =

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

130 a::int

131 b::nat

132 c::'a

136 lemma (in foo) foo1:

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

138 by simp

140 lemma (in foo) foo2:

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

142 by simp

144 lemma (in foo) foo3:

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

146 by simp

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

152 statespace bar =

153 b::bool

154 c::string

156 lemma (in bar) bar1:

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

158 by simp

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

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

165 X::'b

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

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

186 x::int

188 lemma (in dup)

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

190 by simp

192 lemma (in dup)

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

194 by simp

196 lemma (in dup)

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

198 by simp

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

203 (*

204 locale fooX = foo +

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

206 *)

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

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

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

234 end