author  nipkow 
Fri, 25 Jul 2003 17:21:22 +0200  
changeset 14134  0fdf5708c7a8 
parent 14025  d9b155757dc8 
child 14981  e73f8140af78 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Table.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 
header {* Abstract tables and their implementation as lists *} 

7 

8 
theory Table = Basis: 

9 

10 
text {* 

11 
design issues: 

12 
\begin{itemize} 

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

14 
list chosen, because: 

15 
\begin{itemize} 

16 
\item[+] a priori finite 

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

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

19 
mapping 

20 
\end{itemize} 

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

22 
Some/None chosen, because: 

23 
\begin{itemize} 

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

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

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

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

28 
of any name are considered to be defined) 

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

30 
\end{itemize} 

31 
\end{itemize} 

32 
*} 

33 

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

34 
types ('a, 'b) table {* table with key type 'a and contents type 'b *} 
14134  35 
= "'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

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

39 

40 
section "map of / table of" 

41 

42 
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

43 
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

44 

12854  45 
translations 
46 
"table_of" == "map_of" 

47 

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

12854  50 

51 
(* ### To map *) 

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

56 
section {* Conditional Override *} 

57 
constdefs 

58 
cond_override:: 

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

60 

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

61 
{* 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

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

65 
(case new k of 

66 
None \<Rightarrow> old k 

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

68 
None \<Rightarrow> Some new_val 

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

70 
then Some new_val 

71 
else Some old_val)))" 

72 

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

74 
by (simp add: cond_override_def expand_fun_eq) 

75 

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

77 
by (simp add: cond_override_def expand_fun_eq) 

78 

79 
lemma cond_override_None[simp]: 

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

81 
by (simp add: cond_override_def) 

82 

83 
lemma cond_override_override: 

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

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

86 
by (auto simp add: cond_override_def) 

87 

88 
lemma cond_override_noOverride: 

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

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

91 
by (auto simp add: cond_override_def) 

92 

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

94 
by (auto simp add: cond_override_def dom_def) 

95 

96 
lemma finite_dom_cond_override: 

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

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

99 
apply (rule dom_cond_override) 

100 
by (rule finite_UnI) 

101 

102 
section {* Filter on Tables *} 

103 

104 
constdefs 

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

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

107 
None \<Rightarrow> None 

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

109 

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

111 
by (simp add: filter_tab_def empty_def) 

112 

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

114 
by (simp add: expand_fun_eq filter_tab_def) 

115 

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

117 
by (simp add: expand_fun_eq filter_tab_def empty_def) 

118 

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

120 
by (auto simp add: filter_tab_def ran_def) 

121 

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

123 
apply (auto simp add: filter_tab_def) 

124 
apply (drule sym, blast) 

125 
done 

126 

127 
lemma finite_range_filter_tab: 

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

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

130 
apply (rule filter_tab_range_subset) 

131 
apply (auto intro: finite_UnI) 

132 
done 

133 

134 
lemma filter_tab_SomeD[dest!]: 

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

136 
by (auto simp add: filter_tab_def) 

137 

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

139 
by (simp add: filter_tab_def) 

140 

141 
lemma filter_tab_all_True: 

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

143 
apply (auto simp add: filter_tab_def expand_fun_eq) 

144 
done 

145 

146 
lemma filter_tab_all_True_Some: 

147 
"\<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" 

148 
by (auto simp add: filter_tab_def expand_fun_eq) 

149 

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

150 
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

151 
"\<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

152 
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

153 

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

156 
done 

157 

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

159 
by (auto simp add: filter_tab_def dom_def) 

160 

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

162 
by (auto simp add: expand_fun_eq filter_tab_def) 

163 

164 
lemma finite_dom_filter_tab: 

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

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

167 
by (rule filter_tab_dom_subset) 

168 

169 

170 
lemma filter_tab_weaken: 

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

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

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

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

177 
lemma cond_override_filter: 

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

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

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

181 
\<rbrakk> \<Longrightarrow> 

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

183 
= filter_tab filterC (cond_override overC t s)" 

184 
by (auto simp add: expand_fun_eq cond_override_def filter_tab_def ) 

185 

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

186 

12854  187 
section {* Misc. *} 
188 

189 
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" 

190 
apply (erule make_imp) 

191 
apply (induct l) 

192 
apply simp 

193 
apply (simp (no_asm)) 

194 
apply auto 

195 
done 

196 

197 
lemma Ball_set_tableD: 

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

199 
apply (frule Ball_set_table) 

200 
by auto 

201 

202 
declare map_of_SomeD [elim] 

203 

204 
lemma table_of_Some_in_set: 

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

206 
by auto 

207 

208 
lemma set_get_eq: 

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

210 
apply safe 

211 
apply (fast dest!: weak_map_of_SomeI) 

212 
apply auto 

213 
done 

214 

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

13585  216 
apply (rule inj_onI) 
12854  217 
apply auto 
218 
done 

219 

220 
lemma table_of_mapconst_SomeI: 

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

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

223 
apply (induct t) 

224 
apply auto 

225 
done 

226 

227 
lemma table_of_mapconst_NoneI: 

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

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

230 
apply (induct t) 

231 
apply auto 

232 
done 

233 

234 
lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard] 

235 

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

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

238 
apply (induct_tac "t") 

239 
apply auto 

240 
done 

241 

242 
lemma table_of_remap_SomeD [rule_format (no_asm)]: 

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

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

245 
apply (induct_tac "t") 

246 
apply auto 

247 
done 

248 

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

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

251 
apply (induct_tac "t") 

252 
apply auto 

253 
done 

254 

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

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

257 
apply (induct_tac "t") 

258 
apply auto 

259 
done 

260 

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

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

263 
apply (induct_tac "t") 

264 
apply auto 

265 
done 

266 

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

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

269 
apply (induct_tac "t") 

270 
apply auto 

271 
done 

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

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

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

275 
apply (induct_tac "t") 

276 
apply auto 

277 
done 

278 

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

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

14025  281 
apply (simp) 
282 
apply (rule map_add_Some_iff) 

12854  283 
done 
284 

285 
lemma table_of_filter_unique_SomeD [rule_format (no_asm)]: 

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

287 
apply (induct xs) 

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

289 
done 

290 

291 

292 
consts 

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

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

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

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

297 
('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

298 
{* variant for unique table: *} 
12854  299 
hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow> 
300 
('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

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

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

305 

306 
defs 

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

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

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

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

311 
cond_hiding_entails_def: "t hiding s under C entails R 

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

313 

314 
section "Untables" 

315 

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

317 
apply (simp add: Un_tables_def) 

318 
apply auto 

319 
done 

320 

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

322 
apply (simp add: Un_tables_def) 

323 
apply auto 

324 
done 

325 

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

327 
apply (unfold Un_tables_def) 

328 
apply (simp (no_asm)) 

329 
done 

330 

331 

332 
section "overrides" 

333 

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

335 
apply (unfold overrides_t_def) 

336 
apply (simp (no_asm)) 

337 
done 

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

339 
apply (unfold overrides_t_def) 

340 
apply (simp (no_asm)) 

341 
done 

342 

343 
lemma overrides_t_Some_iff: 

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

345 
by (simp add: overrides_t_def) 

346 

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

348 

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

350 
by (simp add: overrides_t_def) 

351 

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

353 
by (simp add: overrides_t_def) 

354 

355 
section "hiding entails" 

356 

357 
lemma hiding_entailsD: 

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

359 
by (simp add: hiding_entails_def) 

360 

361 
lemma empty_hiding_entails: "empty hiding s entails R" 

362 
by (simp add: hiding_entails_def) 

363 

364 
lemma hiding_empty_entails: "t hiding empty entails R" 

365 
by (simp add: hiding_entails_def) 

366 
declare empty_hiding_entails [simp] hiding_empty_entails [simp] 

367 

368 
section "cond hiding entails" 

369 

370 
lemma cond_hiding_entailsD: 

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

372 
by (simp add: cond_hiding_entails_def) 

373 

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

375 
by (simp add: cond_hiding_entails_def) 

376 

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

378 
by (simp add: cond_hiding_entails_def) 

379 

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

381 
by (simp add: hidings_entails_def) 

382 

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

384 
apply (unfold hidings_entails_def) 

385 
apply (simp (no_asm)) 

386 
done 

387 

388 
lemma empty_hidings_entails: 

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

390 
by (simp (no_asm)) 

391 
declare empty_hidings_entails [intro!] hidings_empty_entails [intro!] 

392 

393 

394 

395 
(*###TO Map?*) 

396 
consts 

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

398 
primrec 

399 
"atleast_free m 0 = True" 

400 
atleast_free_Suc: 

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

402 

403 
lemma atleast_free_weaken [rule_format (no_asm)]: 

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

405 
apply (induct_tac "n") 

406 
apply (simp (no_asm)) 

407 
apply clarify 

408 
apply (simp (no_asm)) 

409 
apply (drule atleast_free_Suc [THEN iffD1]) 

410 
apply fast 

411 
done 

412 

413 
lemma atleast_free_SucI: 

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

415 
by force 

416 

417 
declare fun_upd_apply [simp del] 

418 
lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 

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

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

421 
apply (induct_tac "n") 

422 
apply auto 

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

424 
apply (rule conjI) 

425 
apply (force simp add: fun_upd_apply) 

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

427 
apply clarify 

428 
apply (subst fun_upd_twist) 

429 
apply (erule not_sym) 

430 
apply (rename_tac "ba") 

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

432 
apply clarify 

433 
apply (tactic "smp_tac 2 1") 

434 
apply (erule (1) notE impE) 

435 
apply (case_tac "aa = b") 

436 
apply fast+ 

437 
done 

438 
declare fun_upd_apply [simp] 

439 

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

441 
apply auto 

442 
apply (case_tac "aa = a") 

443 
apply auto 

444 
apply (erule atleast_free_SucD_lemma) 

445 
apply auto 

446 
done 

447 

448 
declare atleast_free_Suc [simp del] 

449 
end 