equal
deleted
inserted
replaced
1 (* Title: HOL/Bali/Table.thy |
1 (* Title: HOL/Bali/Table.thy |
2 Author: David von Oheimb |
2 Author: David von Oheimb |
3 *) |
3 *) |
4 header {* Abstract tables and their implementation as lists *} |
4 subsection {* Abstract tables and their implementation as lists *} |
5 |
5 |
6 theory Table imports Basis begin |
6 theory Table imports Basis begin |
7 |
7 |
8 text {* |
8 text {* |
9 design issues: |
9 design issues: |
33 = "'a \<rightharpoonup> 'b" |
33 = "'a \<rightharpoonup> 'b" |
34 type_synonym ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *} |
34 type_synonym ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *} |
35 = "'a \<Rightarrow> 'b set" |
35 = "'a \<Rightarrow> 'b set" |
36 |
36 |
37 |
37 |
38 section "map of / table of" |
38 subsubsection "map of / table of" |
39 |
39 |
40 abbreviation |
40 abbreviation |
41 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *} |
41 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *} |
42 where "table_of \<equiv> map_of" |
42 where "table_of \<equiv> map_of" |
43 |
43 |
47 (* ### To map *) |
47 (* ### To map *) |
48 lemma map_add_find_left[simp]: "n k = None \<Longrightarrow> (m ++ n) k = m k" |
48 lemma map_add_find_left[simp]: "n k = None \<Longrightarrow> (m ++ n) k = m k" |
49 by (simp add: map_add_def) |
49 by (simp add: map_add_def) |
50 |
50 |
51 |
51 |
52 section {* Conditional Override *} |
52 subsubsection {* Conditional Override *} |
53 |
53 |
54 definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where |
54 definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where |
55 |
55 |
56 --{* when merging tables old and new, only override an entry of table old when |
56 --{* when merging tables old and new, only override an entry of table old when |
57 the condition cond holds *} |
57 the condition cond holds *} |
93 apply (rule_tac B="dom s \<union> dom t" in finite_subset) |
93 apply (rule_tac B="dom s \<union> dom t" in finite_subset) |
94 apply (rule dom_cond_override) |
94 apply (rule dom_cond_override) |
95 by (rule finite_UnI) |
95 by (rule finite_UnI) |
96 |
96 |
97 |
97 |
98 section {* Filter on Tables *} |
98 subsubsection {* Filter on Tables *} |
99 |
99 |
100 definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" |
100 definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" |
101 where |
101 where |
102 "filter_tab c t = (\<lambda>k. (case t k of |
102 "filter_tab c t = (\<lambda>k. (case t k of |
103 None \<Rightarrow> None |
103 None \<Rightarrow> None |
177 cond_override overC (filter_tab filterC t) (filter_tab filterC s) |
177 cond_override overC (filter_tab filterC t) (filter_tab filterC s) |
178 = filter_tab filterC (cond_override overC t s)" |
178 = filter_tab filterC (cond_override overC t s)" |
179 by (auto simp add: fun_eq_iff cond_override_def filter_tab_def ) |
179 by (auto simp add: fun_eq_iff cond_override_def filter_tab_def ) |
180 |
180 |
181 |
181 |
182 section {* Misc *} |
182 subsubsection {* Misc *} |
183 |
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" |
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" |
185 apply (erule rev_mp) |
185 apply (erule rev_mp) |
186 apply (induct l) |
186 apply (induct l) |
187 apply simp |
187 apply simp |
287 \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" |
287 \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" |
288 ("_ hiding _ under _ entails _" 20) |
288 ("_ hiding _ under _ entails _" 20) |
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)" |
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)" |
290 |
290 |
291 |
291 |
292 section "Untables" |
292 subsubsection "Untables" |
293 |
293 |
294 lemma Un_tablesI [intro]: "t \<in> ts \<Longrightarrow> x \<in> t k \<Longrightarrow> x \<in> Un_tables ts k" |
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) |
295 by (auto simp add: Un_tables_def) |
296 |
296 |
297 lemma Un_tablesD [dest!]: "x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k" |
297 lemma Un_tablesD [dest!]: "x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k" |
299 |
299 |
300 lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})" |
300 lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})" |
301 by (simp add: Un_tables_def) |
301 by (simp add: Un_tables_def) |
302 |
302 |
303 |
303 |
304 section "overrides" |
304 subsubsection "overrides" |
305 |
305 |
306 lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m" |
306 lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m" |
307 by (simp add: overrides_t_def) |
307 by (simp add: overrides_t_def) |
308 |
308 |
309 lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m" |
309 lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m" |
320 |
320 |
321 lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k" |
321 lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k" |
322 by (simp add: overrides_t_def) |
322 by (simp add: overrides_t_def) |
323 |
323 |
324 |
324 |
325 section "hiding entails" |
325 subsubsection "hiding entails" |
326 |
326 |
327 lemma hiding_entailsD: |
327 lemma hiding_entailsD: |
328 "t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y" |
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) |
329 by (simp add: hiding_entails_def) |
330 |
330 |
333 |
333 |
334 lemma hiding_empty_entails [simp]: "t hiding empty entails R" |
334 lemma hiding_empty_entails [simp]: "t hiding empty entails R" |
335 by (simp add: hiding_entails_def) |
335 by (simp add: hiding_entails_def) |
336 |
336 |
337 |
337 |
338 section "cond hiding entails" |
338 subsubsection "cond hiding entails" |
339 |
339 |
340 lemma cond_hiding_entailsD: |
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" |
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) |
342 by (simp add: cond_hiding_entails_def) |
343 |
343 |