12854
|
1 |
(* Title: isabelle/Bali/Table.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 1997 Technische Universitaet Muenchen
|
|
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 |
|
|
34 |
|
|
35 |
types ('a, 'b) table (* table with key type 'a and contents type 'b *)
|
|
36 |
= "'a \<leadsto> 'b"
|
|
37 |
('a, 'b) tables (* non-unique table with key 'a and contents 'b *)
|
|
38 |
= "'a \<Rightarrow> 'b set"
|
|
39 |
|
|
40 |
|
|
41 |
section "map of / table of"
|
|
42 |
|
|
43 |
syntax
|
|
44 |
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" (* concrete table *)
|
|
45 |
|
|
46 |
translations
|
|
47 |
"table_of" == "map_of"
|
|
48 |
|
|
49 |
(type)"'a \<leadsto> 'b" <= (type)"'a \<Rightarrow> 'b Option.option"
|
|
50 |
(type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
|
|
51 |
|
|
52 |
(* ### To map *)
|
|
53 |
lemma override_find_left[simp]:
|
|
54 |
"n k = None \<Longrightarrow> (m ++ n) k = m k"
|
|
55 |
by (simp add: override_def)
|
|
56 |
|
|
57 |
section {* Conditional Override *}
|
|
58 |
constdefs
|
|
59 |
cond_override::
|
|
60 |
"('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"
|
|
61 |
|
|
62 |
(* when merging tables old and new, only override an entry of table old when
|
|
63 |
the condition cond holds *)
|
|
64 |
"cond_override cond old new \<equiv>
|
|
65 |
\<lambda> k.
|
|
66 |
(case new k of
|
|
67 |
None \<Rightarrow> old k
|
|
68 |
| Some new_val \<Rightarrow> (case old k of
|
|
69 |
None \<Rightarrow> Some new_val
|
|
70 |
| Some old_val \<Rightarrow> (if cond new_val old_val
|
|
71 |
then Some new_val
|
|
72 |
else Some old_val)))"
|
|
73 |
|
|
74 |
lemma cond_override_empty1[simp]: "cond_override c empty t = t"
|
|
75 |
by (simp add: cond_override_def expand_fun_eq)
|
|
76 |
|
|
77 |
lemma cond_override_empty2[simp]: "cond_override c t empty = t"
|
|
78 |
by (simp add: cond_override_def expand_fun_eq)
|
|
79 |
|
|
80 |
lemma cond_override_None[simp]:
|
|
81 |
"old k = None \<Longrightarrow> (cond_override c old new) k = new k"
|
|
82 |
by (simp add: cond_override_def)
|
|
83 |
|
|
84 |
lemma cond_override_override:
|
|
85 |
"\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk>
|
|
86 |
\<Longrightarrow> (cond_override C old new) k = Some nv"
|
|
87 |
by (auto simp add: cond_override_def)
|
|
88 |
|
|
89 |
lemma cond_override_noOverride:
|
|
90 |
"\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk>
|
|
91 |
\<Longrightarrow> (cond_override C old new) k = Some ov"
|
|
92 |
by (auto simp add: cond_override_def)
|
|
93 |
|
|
94 |
lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
|
|
95 |
by (auto simp add: cond_override_def dom_def)
|
|
96 |
|
|
97 |
lemma finite_dom_cond_override:
|
|
98 |
"\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
|
|
99 |
apply (rule_tac B="dom s \<union> dom t" in finite_subset)
|
|
100 |
apply (rule dom_cond_override)
|
|
101 |
by (rule finite_UnI)
|
|
102 |
|
|
103 |
section {* Filter on Tables *}
|
|
104 |
|
|
105 |
constdefs
|
|
106 |
filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
|
|
107 |
"filter_tab c t \<equiv> \<lambda> k. (case t k of
|
|
108 |
None \<Rightarrow> None
|
|
109 |
| Some x \<Rightarrow> if c k x then Some x else None)"
|
|
110 |
|
|
111 |
lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
|
|
112 |
by (simp add: filter_tab_def empty_def)
|
|
113 |
|
|
114 |
lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
|
|
115 |
by (simp add: expand_fun_eq filter_tab_def)
|
|
116 |
|
|
117 |
lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
|
|
118 |
by (simp add: expand_fun_eq filter_tab_def empty_def)
|
|
119 |
|
|
120 |
lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
|
|
121 |
by (auto simp add: filter_tab_def ran_def)
|
|
122 |
|
|
123 |
lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
|
|
124 |
apply (auto simp add: filter_tab_def)
|
|
125 |
apply (drule sym, blast)
|
|
126 |
done
|
|
127 |
|
|
128 |
lemma finite_range_filter_tab:
|
|
129 |
"finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
|
|
130 |
apply (rule_tac B="range t \<union> {None} " in finite_subset)
|
|
131 |
apply (rule filter_tab_range_subset)
|
|
132 |
apply (auto intro: finite_UnI)
|
|
133 |
done
|
|
134 |
|
|
135 |
lemma filter_tab_SomeD[dest!]:
|
|
136 |
"filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
|
|
137 |
by (auto simp add: filter_tab_def)
|
|
138 |
|
|
139 |
lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
|
|
140 |
by (simp add: filter_tab_def)
|
|
141 |
|
|
142 |
lemma filter_tab_all_True:
|
|
143 |
"\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
|
|
144 |
apply (auto simp add: filter_tab_def expand_fun_eq)
|
|
145 |
done
|
|
146 |
|
|
147 |
lemma filter_tab_all_True_Some:
|
|
148 |
"\<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"
|
|
149 |
by (auto simp add: filter_tab_def expand_fun_eq)
|
|
150 |
|
|
151 |
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
|
|
152 |
apply (simp add: filter_tab_def expand_fun_eq)
|
|
153 |
done
|
|
154 |
|
|
155 |
lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
|
|
156 |
by (auto simp add: filter_tab_def dom_def)
|
|
157 |
|
|
158 |
lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
|
|
159 |
by (auto simp add: expand_fun_eq filter_tab_def)
|
|
160 |
|
|
161 |
lemma finite_dom_filter_tab:
|
|
162 |
"finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
|
|
163 |
apply (rule_tac B="dom t" in finite_subset)
|
|
164 |
by (rule filter_tab_dom_subset)
|
|
165 |
|
|
166 |
|
|
167 |
lemma filter_tab_weaken:
|
|
168 |
"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b;
|
|
169 |
\<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
|
|
170 |
\<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
|
|
171 |
apply (auto simp add: filter_tab_def)
|
|
172 |
done
|
|
173 |
|
|
174 |
lemma cond_override_filter:
|
|
175 |
"\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk>
|
|
176 |
\<Longrightarrow> (\<not> overC new old \<longrightarrow> \<not> filterC k new) \<and>
|
|
177 |
(overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
|
|
178 |
\<rbrakk> \<Longrightarrow>
|
|
179 |
cond_override overC (filter_tab filterC t) (filter_tab filterC s)
|
|
180 |
= filter_tab filterC (cond_override overC t s)"
|
|
181 |
by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
|
|
182 |
|
|
183 |
section {* Misc. *}
|
|
184 |
|
|
185 |
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"
|
|
186 |
apply (erule make_imp)
|
|
187 |
apply (induct l)
|
|
188 |
apply simp
|
|
189 |
apply (simp (no_asm))
|
|
190 |
apply auto
|
|
191 |
done
|
|
192 |
|
|
193 |
lemma Ball_set_tableD:
|
|
194 |
"\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
|
|
195 |
apply (frule Ball_set_table)
|
|
196 |
by auto
|
|
197 |
|
|
198 |
declare map_of_SomeD [elim]
|
|
199 |
|
|
200 |
lemma table_of_Some_in_set:
|
|
201 |
"table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
|
|
202 |
by auto
|
|
203 |
|
|
204 |
lemma set_get_eq:
|
|
205 |
"unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
|
|
206 |
apply safe
|
|
207 |
apply (fast dest!: weak_map_of_SomeI)
|
|
208 |
apply auto
|
|
209 |
done
|
|
210 |
|
|
211 |
lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
|
|
212 |
apply (rule injI)
|
|
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))"
|
|
277 |
apply (simp only: map_of_override [THEN sym])
|
|
278 |
apply (rule override_Some_iff)
|
|
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)
|
|
294 |
(* variant for unique table: *)
|
|
295 |
hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow>
|
|
296 |
('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hiding _ entails _" 20)
|
|
297 |
(* variant for a unique table and conditional overriding: *)
|
|
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
|