author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 67443 | 3abf6a722518 |
child 68451 | c34aa23a1fb6 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/Table.thy |
12854 | 2 |
Author: David von Oheimb |
3 |
*) |
|
62042 | 4 |
subsection \<open>Abstract tables and their implementation as lists\<close> |
12854 | 5 |
|
16417 | 6 |
theory Table imports Basis begin |
12854 | 7 |
|
62042 | 8 |
text \<open> |
12854 | 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} |
|
62042 | 30 |
\<close> |
12854 | 31 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
32 |
type_synonym ('a, 'b) table \<comment> \<open>table with key type 'a and contents type 'b\<close> |
14134 | 33 |
= "'a \<rightharpoonup> 'b" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
34 |
type_synonym ('a, 'b) tables \<comment> \<open>non-unique table with key 'a and contents 'b\<close> |
12854 | 35 |
= "'a \<Rightarrow> 'b set" |
36 |
||
37 |
||
58887 | 38 |
subsubsection "map of / table of" |
12854 | 39 |
|
34939 | 40 |
abbreviation |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
41 |
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" \<comment> \<open>concrete table\<close> |
35355
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 |
|
62042 | 52 |
subsubsection \<open>Conditional Override\<close> |
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 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
56 |
\<comment> \<open>when merging tables old and new, only override an entry of table old when |
62042 | 57 |
the condition cond holds\<close> |
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 |
|
62042 | 98 |
subsubsection \<open>Filter on Tables\<close> |
12854 | 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 |
|
62042 | 182 |
subsubsection \<open>Misc\<close> |
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: |
|
55518
1ddb2edf5ceb
folded 'Option.set' into BNF-generated 'set_option'
blanchet
parents:
46584
diff
changeset
|
193 |
"\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> set_option (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 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
279 |
\<comment> \<open>variant for unique table:\<close> |
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 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
285 |
\<comment> \<open>variant for a unique table and conditional overriding:\<close> |
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 |
|
58887 | 292 |
subsubsection "Untables" |
12854 | 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 |
||
58887 | 304 |
subsubsection "overrides" |
12854 | 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 |
|
58887 | 325 |
subsubsection "hiding entails" |
12854 | 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 |
|
58887 | 338 |
subsubsection "cond hiding entails" |
12854 | 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?*) |
|
61069 | 364 |
primrec atleast_free :: "('a \<rightharpoonup> 'b) => nat => bool" |
37956 | 365 |
where |
366 |
"atleast_free m 0 = True" |
|
67613 | 367 |
| atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None \<and> (\<forall>b. atleast_free (m(a\<mapsto>b)) n))" |
12854 | 368 |
|
369 |
lemma atleast_free_weaken [rule_format (no_asm)]: |
|
67613 | 370 |
"\<forall>m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n" |
12854 | 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: |
|
67613 | 380 |
"[| h a = None; \<forall>obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)" |
12854 | 381 |
by force |
382 |
||
383 |
declare fun_upd_apply [simp del] |
|
384 |
lemma atleast_free_SucD_lemma [rule_format (no_asm)]: |
|
67613 | 385 |
"\<forall>m a. m a = None \<longrightarrow> (\<forall>c. atleast_free (m(a\<mapsto>c)) n) \<longrightarrow> |
386 |
(\<forall>b d. a \<noteq> b \<longrightarrow> atleast_free (m(b\<mapsto>d)) n)" |
|
12854 | 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 |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58887
diff
changeset
|
399 |
apply (tactic "smp_tac @{context} 2 1") |
12854 | 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 |