author  paulson 
Wed, 21 Dec 2005 12:02:57 +0100  
changeset 18447  da548623916a 
parent 16417  9bc16273c2d4 
child 24038  18182c4aec9e 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Table.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

5 
header {* Abstract tables and their implementation as lists *} 

6 

16417  7 
theory Table imports Basis begin 
12854  8 

9 
text {* 

10 
design issues: 

11 
\begin{itemize} 

12 
\item definition of table: infinite map vs. list vs. finite set 

13 
list chosen, because: 

14 
\begin{itemize} 

15 
\item[+] a priori finite 

16 
\item[+] lookup is more operational than for finite set 

17 
\item[] not very abstract, but function table converts it to abstract 

18 
mapping 

19 
\end{itemize} 

20 
\item coding of lookup result: Some/None vs. value/arbitrary 

21 
Some/None chosen, because: 

22 
\begin{itemize} 

23 
\item[++] makes definedness check possible (applies also to finite set), 

24 
which is important for the type standard, hiding/overriding, etc. 

25 
(though it may perhaps be possible at least for the operational semantics 

26 
to treat programs as infinite, i.e. where classes, fields, methods etc. 

27 
of any name are considered to be defined) 

28 
\item[] sometimes awkward case distinctions, alleviated by operator 'the' 

29 
\end{itemize} 

30 
\end{itemize} 

31 
*} 

32 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

33 
types ('a, 'b) table {* table with key type 'a and contents type 'b *} 
14134  34 
= "'a \<rightharpoonup> 'b" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

35 
('a, 'b) tables {* nonunique table with key 'a and contents 'b *} 
12854  36 
= "'a \<Rightarrow> 'b set" 
37 

38 

39 
section "map of / table of" 

40 

41 
syntax 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

42 
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" {* concrete table *} 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

43 

12854  44 
translations 
45 
"table_of" == "map_of" 

46 

14134  47 
(type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Option.option" 
48 
(type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b" 

12854  49 

50 
(* ### To map *) 

14025  51 
lemma map_add_find_left[simp]: 
12854  52 
"n k = None \<Longrightarrow> (m ++ n) k = m k" 
14025  53 
by (simp add: map_add_def) 
12854  54 

55 
section {* Conditional Override *} 

56 
constdefs 

57 
cond_override:: 

58 
"('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" 

59 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

60 
{* when merging tables old and new, only override an entry of table old when 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

61 
the condition cond holds *} 
12854  62 
"cond_override cond old new \<equiv> 
63 
\<lambda> k. 

64 
(case new k of 

65 
None \<Rightarrow> old k 

66 
 Some new_val \<Rightarrow> (case old k of 

67 
None \<Rightarrow> Some new_val 

68 
 Some old_val \<Rightarrow> (if cond new_val old_val 

69 
then Some new_val 

70 
else Some old_val)))" 

71 

72 
lemma cond_override_empty1[simp]: "cond_override c empty t = t" 

73 
by (simp add: cond_override_def expand_fun_eq) 

74 

75 
lemma cond_override_empty2[simp]: "cond_override c t empty = t" 

76 
by (simp add: cond_override_def expand_fun_eq) 

77 

78 
lemma cond_override_None[simp]: 

79 
"old k = None \<Longrightarrow> (cond_override c old new) k = new k" 

80 
by (simp add: cond_override_def) 

81 

82 
lemma cond_override_override: 

83 
"\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 

84 
\<Longrightarrow> (cond_override C old new) k = Some nv" 

85 
by (auto simp add: cond_override_def) 

86 

87 
lemma cond_override_noOverride: 

88 
"\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 

89 
\<Longrightarrow> (cond_override C old new) k = Some ov" 

90 
by (auto simp add: cond_override_def) 

91 

92 
lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t" 

93 
by (auto simp add: cond_override_def dom_def) 

94 

95 
lemma finite_dom_cond_override: 

96 
"\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))" 

97 
apply (rule_tac B="dom s \<union> dom t" in finite_subset) 

98 
apply (rule dom_cond_override) 

99 
by (rule finite_UnI) 

100 

101 
section {* Filter on Tables *} 

102 

103 
constdefs 

104 
filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" 

105 
"filter_tab c t \<equiv> \<lambda> k. (case t k of 

106 
None \<Rightarrow> None 

107 
 Some x \<Rightarrow> if c k x then Some x else None)" 

108 

109 
lemma filter_tab_empty[simp]: "filter_tab c empty = empty" 

110 
by (simp add: filter_tab_def empty_def) 

111 

112 
lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t" 

113 
by (simp add: expand_fun_eq filter_tab_def) 

114 

115 
lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty" 

116 
by (simp add: expand_fun_eq filter_tab_def empty_def) 

117 

118 
lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t" 

119 
by (auto simp add: filter_tab_def ran_def) 

120 

121 
lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}" 

122 
apply (auto simp add: filter_tab_def) 

123 
apply (drule sym, blast) 

124 
done 

125 

126 
lemma finite_range_filter_tab: 

127 
"finite (range t) \<Longrightarrow> finite (range (filter_tab c t))" 

128 
apply (rule_tac B="range t \<union> {None} " in finite_subset) 

129 
apply (rule filter_tab_range_subset) 

130 
apply (auto intro: finite_UnI) 

131 
done 

132 

133 
lemma filter_tab_SomeD[dest!]: 

134 
"filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x" 

135 
by (auto simp add: filter_tab_def) 

136 

137 
lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x" 

138 
by (simp add: filter_tab_def) 

139 

140 
lemma filter_tab_all_True: 

141 
"\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t" 

142 
apply (auto simp add: filter_tab_def expand_fun_eq) 

143 
done 

144 

145 
lemma filter_tab_all_True_Some: 

146 
"\<lbrakk>\<forall> k y. t k = Some y \<longrightarrow> p k y; t k = Some v\<rbrakk> \<Longrightarrow> filter_tab p t k = Some v" 

147 
by (auto simp add: filter_tab_def expand_fun_eq) 

148 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

149 
lemma filter_tab_all_False: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

150 
"\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

151 
by (auto simp add: filter_tab_def expand_fun_eq) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

152 

12854  153 
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None" 
154 
apply (simp add: filter_tab_def expand_fun_eq) 

155 
done 

156 

157 
lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t" 

158 
by (auto simp add: filter_tab_def dom_def) 

159 

160 
lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b" 

161 
by (auto simp add: expand_fun_eq filter_tab_def) 

162 

163 
lemma finite_dom_filter_tab: 

164 
"finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))" 

165 
apply (rule_tac B="dom t" in finite_subset) 

166 
by (rule filter_tab_dom_subset) 

167 

168 

169 
lemma filter_tab_weaken: 

170 
"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 

171 
\<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y 

172 
\<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b" 

13601  173 
apply (force simp add: filter_tab_def) 
12854  174 
done 
175 

176 
lemma cond_override_filter: 

177 
"\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 

178 
\<Longrightarrow> (\<not> overC new old \<longrightarrow> \<not> filterC k new) \<and> 

179 
(overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new) 

180 
\<rbrakk> \<Longrightarrow> 

181 
cond_override overC (filter_tab filterC t) (filter_tab filterC s) 

182 
= filter_tab filterC (cond_override overC t s)" 

183 
by (auto simp add: expand_fun_eq cond_override_def filter_tab_def ) 

184 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

185 

12854  186 
section {* Misc. *} 
187 

188 
lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y" 

189 
apply (erule make_imp) 

190 
apply (induct l) 

191 
apply simp 

192 
apply (simp (no_asm)) 

193 
apply auto 

194 
done 

195 

196 
lemma Ball_set_tableD: 

197 
"\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x" 

198 
apply (frule Ball_set_table) 

199 
by auto 

200 

201 
declare map_of_SomeD [elim] 

202 

203 
lemma table_of_Some_in_set: 

204 
"table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l" 

205 
by auto 

206 

207 
lemma set_get_eq: 

208 
"unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)" 

18447  209 
by (auto dest!: weak_map_of_SomeI) 
12854  210 

211 
lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))" 

13585  212 
apply (rule inj_onI) 
12854  213 
apply auto 
214 
done 

215 

216 
lemma table_of_mapconst_SomeI: 

217 
"\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow> 

218 
table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y" 

219 
apply (induct t) 

220 
apply auto 

221 
done 

222 

223 
lemma table_of_mapconst_NoneI: 

224 
"\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow> 

225 
table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None" 

226 
apply (induct t) 

227 
apply auto 

228 
done 

229 

230 
lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard] 

231 

232 
lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow> 

233 
table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)" 

234 
apply (induct_tac "t") 

235 
apply auto 

236 
done 

237 

238 
lemma table_of_remap_SomeD [rule_format (no_asm)]: 

239 
"table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow> 

240 
table_of t (k, k') = Some x" 

241 
apply (induct_tac "t") 

242 
apply auto 

243 
done 

244 

245 
lemma table_of_mapf_Some [rule_format (no_asm)]: "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> 

246 
table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x" 

247 
apply (induct_tac "t") 

248 
apply auto 

249 
done 

250 

251 
lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]: 

252 
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)" 

253 
apply (induct_tac "t") 

254 
apply auto 

255 
done 

256 

257 
lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]: 

258 
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<longrightarrow> (table_of t k = None)" 

259 
apply (induct_tac "t") 

260 
apply auto 

261 
done 

262 

263 
lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]: 

264 
"table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x" 

265 
apply (induct_tac "t") 

266 
apply auto 

267 
done 

268 
lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]: 

269 
"table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x 

270 
\<longrightarrow> C = snd ek \<and> table_of t (fst ek) = Some x" 

271 
apply (induct_tac "t") 

272 
apply auto 

273 
done 

274 

275 
lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 

276 
(table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))" 

14025  277 
apply (simp) 
278 
apply (rule map_add_Some_iff) 

12854  279 
done 
280 

281 
lemma table_of_filter_unique_SomeD [rule_format (no_asm)]: 

282 
"table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z" 

283 
apply (induct xs) 

284 
apply (auto del: map_of_SomeD intro!: map_of_SomeD) 

285 
done 

286 

287 

288 
consts 

289 
Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables" 

290 
overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> 

291 
('a, 'b) tables" (infixl "\<oplus>\<oplus>" 100) 

292 
hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> 

293 
('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hidings _ entails _" 20) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

294 
{* variant for unique table: *} 
12854  295 
hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow> 
296 
('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hiding _ entails _" 20) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

297 
{* variant for a unique table and conditional overriding: *} 
12854  298 
cond_hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table 
299 
\<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" 

300 
("_ hiding _ under _ entails _" 20) 

301 

302 
defs 

303 
Un_tables_def: "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k" 

304 
overrides_t_def: "s \<oplus>\<oplus> t \<equiv> \<lambda>k. if t k = {} then s k else t k" 

305 
hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y" 

306 
hiding_entails_def: "t hiding s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y" 

307 
cond_hiding_entails_def: "t hiding s under C entails R 

308 
\<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y" 

309 

310 
section "Untables" 

311 

312 
lemma Un_tablesI [intro]: "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k" 

313 
apply (simp add: Un_tables_def) 

314 
apply auto 

315 
done 

316 

317 
lemma Un_tablesD [dest!]: "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k" 

318 
apply (simp add: Un_tables_def) 

319 
apply auto 

320 
done 

321 

322 
lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})" 

323 
apply (unfold Un_tables_def) 

324 
apply (simp (no_asm)) 

325 
done 

326 

327 

328 
section "overrides" 

329 

330 
lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m" 

331 
apply (unfold overrides_t_def) 

332 
apply (simp (no_asm)) 

333 
done 

334 
lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m" 

335 
apply (unfold overrides_t_def) 

336 
apply (simp (no_asm)) 

337 
done 

338 

339 
lemma overrides_t_Some_iff: 

340 
"(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)" 

341 
by (simp add: overrides_t_def) 

342 

343 
lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!] 

344 

345 
lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k" 

346 
by (simp add: overrides_t_def) 

347 

348 
lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k" 

349 
by (simp add: overrides_t_def) 

350 

351 
section "hiding entails" 

352 

353 
lemma hiding_entailsD: 

354 
"\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y" 

355 
by (simp add: hiding_entails_def) 

356 

357 
lemma empty_hiding_entails: "empty hiding s entails R" 

358 
by (simp add: hiding_entails_def) 

359 

360 
lemma hiding_empty_entails: "t hiding empty entails R" 

361 
by (simp add: hiding_entails_def) 

362 
declare empty_hiding_entails [simp] hiding_empty_entails [simp] 

363 

364 
section "cond hiding entails" 

365 

366 
lemma cond_hiding_entailsD: 

367 
"\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y" 

368 
by (simp add: cond_hiding_entails_def) 

369 

370 
lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R" 

371 
by (simp add: cond_hiding_entails_def) 

372 

373 
lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R" 

374 
by (simp add: cond_hiding_entails_def) 

375 

376 
lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y" 

377 
by (simp add: hidings_entails_def) 

378 

379 
lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R" 

380 
apply (unfold hidings_entails_def) 

381 
apply (simp (no_asm)) 

382 
done 

383 

384 
lemma empty_hidings_entails: 

385 
"(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def) 

386 
by (simp (no_asm)) 

387 
declare empty_hidings_entails [intro!] hidings_empty_entails [intro!] 

388 

389 

390 

391 
(*###TO Map?*) 

392 
consts 

393 
atleast_free :: "('a ~=> 'b) => nat => bool" 

394 
primrec 

395 
"atleast_free m 0 = True" 

396 
atleast_free_Suc: 

397 
"atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a>b)) n))" 

398 

399 
lemma atleast_free_weaken [rule_format (no_asm)]: 

400 
"!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n" 

401 
apply (induct_tac "n") 

402 
apply (simp (no_asm)) 

403 
apply clarify 

404 
apply (simp (no_asm)) 

405 
apply (drule atleast_free_Suc [THEN iffD1]) 

406 
apply fast 

407 
done 

408 

409 
lemma atleast_free_SucI: 

410 
"[ h a = None; !obj. atleast_free (h(a>obj)) n ] ==> atleast_free h (Suc n)" 

411 
by force 

412 

413 
declare fun_upd_apply [simp del] 

414 
lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 

415 
" !m a. m a = None > (!c. atleast_free (m(a>c)) n) > 

416 
(!b d. a ~= b > atleast_free (m(b>d)) n)" 

417 
apply (induct_tac "n") 

418 
apply auto 

419 
apply (rule_tac x = "a" in exI) 

420 
apply (rule conjI) 

421 
apply (force simp add: fun_upd_apply) 

422 
apply (erule_tac V = "m a = None" in thin_rl) 

423 
apply clarify 

424 
apply (subst fun_upd_twist) 

425 
apply (erule not_sym) 

426 
apply (rename_tac "ba") 

427 
apply (drule_tac x = "ba" in spec) 

428 
apply clarify 

429 
apply (tactic "smp_tac 2 1") 

430 
apply (erule (1) notE impE) 

431 
apply (case_tac "aa = b") 

432 
apply fast+ 

433 
done 

434 
declare fun_upd_apply [simp] 

435 

436 
lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a>b)) n" 

437 
apply auto 

438 
apply (case_tac "aa = a") 

439 
apply auto 

440 
apply (erule atleast_free_SucD_lemma) 

441 
apply auto 

442 
done 

443 

444 
declare atleast_free_Suc [simp del] 

445 
end 