author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46584  a935175fe6b6 
child 55518  1ddb2edf5ceb 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Table.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

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

5 

16417  6 
theory Table imports Basis begin 
12854  7 

8 
text {* 

9 
design issues: 

10 
\begin{itemize} 

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

12 
list chosen, because: 

13 
\begin{itemize} 

14 
\item[+] a priori finite 

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

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

17 
mapping 

18 
\end{itemize} 

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

20 
Some/None chosen, because: 

21 
\begin{itemize} 

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

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

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

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

26 
of any name are considered to be defined) 

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

28 
\end{itemize} 

29 
\end{itemize} 

30 
*} 

31 

41778  32 
type_synonym ('a, 'b) table {* table with key type 'a and contents type 'b *} 
14134  33 
= "'a \<rightharpoonup> 'b" 
41778  34 
type_synonym ('a, 'b) tables {* nonunique table with key 'a and contents 'b *} 
12854  35 
= "'a \<Rightarrow> 'b set" 
36 

37 

38 
section "map of / table of" 

39 

34939  40 
abbreviation 
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
34939
diff
changeset

41 
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" {* concrete table *} 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
34939
diff
changeset

42 
where "table_of \<equiv> map_of" 
34939  43 

12854  44 
translations 
35431  45 
(type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b" 
12854  46 

47 
(* ### To map *) 

46584  48 
lemma map_add_find_left[simp]: "n k = None \<Longrightarrow> (m ++ n) k = m k" 
49 
by (simp add: map_add_def) 

50 

12854  51 

52 
section {* Conditional Override *} 

46584  53 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
34939
diff
changeset

54 
definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where 
12854  55 

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

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

57 
the condition cond holds *} 
37956  58 
"cond_override cond old new = 
59 
(\<lambda>k. 

12854  60 
(case new k of 
61 
None \<Rightarrow> old k 

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

63 
None \<Rightarrow> Some new_val 

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

65 
then Some new_val 

37956  66 
else Some old_val))))" 
12854  67 

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

46584  69 
by (simp add: cond_override_def fun_eq_iff) 
12854  70 

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

46584  72 
by (simp add: cond_override_def fun_eq_iff) 
12854  73 

74 
lemma cond_override_None[simp]: 

46584  75 
"old k = None \<Longrightarrow> (cond_override c old new) k = new k" 
76 
by (simp add: cond_override_def) 

12854  77 

78 
lemma cond_override_override: 

46584  79 
"\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
80 
\<Longrightarrow> (cond_override C old new) k = Some nv" 

81 
by (auto simp add: cond_override_def) 

12854  82 

83 
lemma cond_override_noOverride: 

46584  84 
"\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
85 
\<Longrightarrow> (cond_override C old new) k = Some ov" 

86 
by (auto simp add: cond_override_def) 

12854  87 

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

46584  89 
by (auto simp add: cond_override_def dom_def) 
12854  90 

91 
lemma finite_dom_cond_override: 

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

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

94 
apply (rule dom_cond_override) 

95 
by (rule finite_UnI) 

96 

46584  97 

12854  98 
section {* Filter on Tables *} 
99 

46584  100 
definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" 
101 
where 

102 
"filter_tab c t = (\<lambda>k. (case t k of 

103 
None \<Rightarrow> None 

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

12854  105 

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

107 
by (simp add: filter_tab_def empty_def) 

108 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

110 
by (simp add: fun_eq_iff filter_tab_def) 
12854  111 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

113 
by (simp add: fun_eq_iff filter_tab_def empty_def) 
12854  114 

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

116 
by (auto simp add: filter_tab_def ran_def) 

117 

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

119 
apply (auto simp add: filter_tab_def) 

120 
apply (drule sym, blast) 

121 
done 

122 

123 
lemma finite_range_filter_tab: 

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

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

126 
apply (rule filter_tab_range_subset) 

127 
apply (auto intro: finite_UnI) 

128 
done 

129 

130 
lemma filter_tab_SomeD[dest!]: 

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

132 
by (auto simp add: filter_tab_def) 

133 

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

135 
by (simp add: filter_tab_def) 

136 

137 
lemma filter_tab_all_True: 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

139 
apply (auto simp add: filter_tab_def fun_eq_iff) 
12854  140 
done 
141 

142 
lemma filter_tab_all_True_Some: 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

144 
by (auto simp add: filter_tab_def fun_eq_iff) 
12854  145 

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

146 
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

147 
"\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

149 

12854  150 
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

151 
apply (simp add: filter_tab_def fun_eq_iff) 
12854  152 
done 
153 

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

155 
by (auto simp add: filter_tab_def dom_def) 

156 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

158 
by (auto simp add: fun_eq_iff filter_tab_def) 
12854  159 

160 
lemma finite_dom_filter_tab: 

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

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

163 
by (rule filter_tab_dom_subset) 

164 

165 

166 
lemma filter_tab_weaken: 

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

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

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

46584  170 
by (force simp add: filter_tab_def) 
12854  171 

172 
lemma cond_override_filter: 

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

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

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

176 
\<rbrakk> \<Longrightarrow> 

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

178 
= filter_tab filterC (cond_override overC t s)" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

179 
by (auto simp add: fun_eq_iff cond_override_def filter_tab_def ) 
12854  180 

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

181 

46584  182 
section {* Misc *} 
12854  183 

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

24038  185 
apply (erule rev_mp) 
12854  186 
apply (induct l) 
187 
apply simp 

188 
apply (simp (no_asm)) 

189 
apply auto 

190 
done 

191 

192 
lemma Ball_set_tableD: 

30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
24194
diff
changeset

193 
"\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x" 
12854  194 
apply (frule Ball_set_table) 
195 
by auto 

196 

197 
declare map_of_SomeD [elim] 

198 

199 
lemma table_of_Some_in_set: 

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

201 
by auto 

202 

203 
lemma set_get_eq: 

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

18447  205 
by (auto dest!: weak_map_of_SomeI) 
12854  206 

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

13585  208 
apply (rule inj_onI) 
12854  209 
apply auto 
210 
done 

211 

212 
lemma table_of_mapconst_SomeI: 

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

46584  214 
table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y" 
215 
by (induct t) auto 

12854  216 

217 
lemma table_of_mapconst_NoneI: 

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

46584  219 
table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None" 
220 
by (induct t) auto 

12854  221 

45605  222 
lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI] 
12854  223 

46584  224 
lemma table_of_map_SomeI: "table_of t k = Some x \<Longrightarrow> 
12854  225 
table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)" 
46584  226 
by (induct t) auto 
12854  227 

46584  228 
lemma table_of_remap_SomeD: 
229 
"table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<Longrightarrow> 

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

231 
by (induct t) auto 

12854  232 

46584  233 
lemma table_of_mapf_Some: 
234 
"\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> 

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

236 
by (induct t) auto 

12854  237 

46584  238 
lemma table_of_mapf_SomeD [dest!]: 
239 
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<Longrightarrow> (\<exists>y\<in>table_of t k: z=f y)" 

240 
by (induct t) auto 

12854  241 

46584  242 
lemma table_of_mapf_NoneD [dest!]: 
243 
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<Longrightarrow> (table_of t k = None)" 

244 
by (induct t) auto 

12854  245 

46584  246 
lemma table_of_mapkey_SomeD [dest!]: 
247 
"table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<Longrightarrow> C = D \<and> table_of t k = Some x" 

248 
by (induct t) auto 

249 

250 
lemma table_of_mapkey_SomeD2 [dest!]: 

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

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

253 
by (induct t) auto 

12854  254 

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

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

14025  257 
apply (simp) 
258 
apply (rule map_add_Some_iff) 

12854  259 
done 
260 

261 
lemma table_of_filter_unique_SomeD [rule_format (no_asm)]: 

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

46584  263 
by (induct xs) (auto del: map_of_SomeD intro!: map_of_SomeD) 
12854  264 

265 

46212  266 
definition Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables" 
267 
where "Un_tables ts = (\<lambda>k. \<Union>t\<in>ts. t k)" 

37956  268 

46584  269 
definition overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables" 
270 
(infixl "\<oplus>\<oplus>" 100) 

37956  271 
where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)" 
272 

273 
definition 

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

275 
("_ hidings _ entails _" 20) 

276 
where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)" 

277 

278 
definition 

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

279 
{* variant for unique table: *} 
37956  280 
hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" 
281 
("_ hiding _ entails _" 20) 

282 
where "(t hiding s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)" 

283 

284 
definition 

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

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

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

37956  289 
where "(t hiding s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)" 
12854  290 

46584  291 

12854  292 
section "Untables" 
293 

46584  294 
lemma Un_tablesI [intro]: "t \<in> ts \<Longrightarrow> x \<in> t k \<Longrightarrow> x \<in> Un_tables ts k" 
295 
by (auto simp add: Un_tables_def) 

12854  296 

46584  297 
lemma Un_tablesD [dest!]: "x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k" 
298 
by (auto simp add: Un_tables_def) 

12854  299 

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

46584  301 
by (simp add: Un_tables_def) 
12854  302 

303 

304 
section "overrides" 

305 

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

46584  307 
by (simp add: overrides_t_def) 
308 

12854  309 
lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m" 
46584  310 
by (simp add: overrides_t_def) 
12854  311 

312 
lemma overrides_t_Some_iff: 

46584  313 
"(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)" 
314 
by (simp add: overrides_t_def) 

12854  315 

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

317 

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

46584  319 
by (simp add: overrides_t_def) 
12854  320 

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

46584  322 
by (simp add: overrides_t_def) 
323 

12854  324 

325 
section "hiding entails" 

326 

327 
lemma hiding_entailsD: 

46584  328 
"t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y" 
329 
by (simp add: hiding_entails_def) 

12854  330 

46584  331 
lemma empty_hiding_entails [simp]: "empty hiding s entails R" 
332 
by (simp add: hiding_entails_def) 

12854  333 

46584  334 
lemma hiding_empty_entails [simp]: "t hiding empty entails R" 
335 
by (simp add: hiding_entails_def) 

336 

12854  337 

338 
section "cond hiding entails" 

339 

340 
lemma cond_hiding_entailsD: 

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

342 
by (simp add: cond_hiding_entails_def) 

343 

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

345 
by (simp add: cond_hiding_entails_def) 

346 

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

348 
by (simp add: cond_hiding_entails_def) 

349 

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

351 
by (simp add: hidings_entails_def) 

352 

46584  353 
lemma hidings_empty_entails [intro!]: "t hidings (\<lambda>k. {}) entails R" 
12854  354 
apply (unfold hidings_entails_def) 
355 
apply (simp (no_asm)) 

356 
done 

357 

46584  358 
lemma empty_hidings_entails [intro!]: 
12854  359 
"(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def) 
360 
by (simp (no_asm)) 

361 

362 

363 
(*###TO Map?*) 

37956  364 
primrec atleast_free :: "('a ~=> 'b) => nat => bool" 
365 
where 

366 
"atleast_free m 0 = True" 

367 
 atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a>b)) n))" 

12854  368 

369 
lemma atleast_free_weaken [rule_format (no_asm)]: 

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

371 
apply (induct_tac "n") 

372 
apply (simp (no_asm)) 

373 
apply clarify 

374 
apply (simp (no_asm)) 

375 
apply (drule atleast_free_Suc [THEN iffD1]) 

376 
apply fast 

377 
done 

378 

379 
lemma atleast_free_SucI: 

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

381 
by force 

382 

383 
declare fun_upd_apply [simp del] 

384 
lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 

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

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

387 
apply (induct_tac "n") 

388 
apply auto 

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

390 
apply (rule conjI) 

391 
apply (force simp add: fun_upd_apply) 

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

393 
apply clarify 

394 
apply (subst fun_upd_twist) 

395 
apply (erule not_sym) 

396 
apply (rename_tac "ba") 

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

398 
apply clarify 

399 
apply (tactic "smp_tac 2 1") 

400 
apply (erule (1) notE impE) 

401 
apply (case_tac "aa = b") 

402 
apply fast+ 

403 
done 

404 
declare fun_upd_apply [simp] 

405 

46584  406 
lemma atleast_free_SucD: "atleast_free h (Suc n) ==> atleast_free (h(a>b)) n" 
12854  407 
apply auto 
408 
apply (case_tac "aa = a") 

409 
apply auto 

410 
apply (erule atleast_free_SucD_lemma) 

411 
apply auto 

412 
done 

413 

414 
declare atleast_free_Suc [simp del] 

46584  415 

12854  416 
end 