equal
deleted
inserted
replaced
51 lemma map_add_find_left[simp]: |
51 lemma map_add_find_left[simp]: |
52 "n k = None \<Longrightarrow> (m ++ n) k = m k" |
52 "n k = None \<Longrightarrow> (m ++ n) k = m k" |
53 by (simp add: map_add_def) |
53 by (simp add: map_add_def) |
54 |
54 |
55 section {* Conditional Override *} |
55 section {* Conditional Override *} |
56 constdefs |
56 definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where |
57 cond_override:: |
|
58 "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" |
|
59 |
57 |
60 --{* when merging tables old and new, only override an entry of table old when |
58 --{* when merging tables old and new, only override an entry of table old when |
61 the condition cond holds *} |
59 the condition cond holds *} |
62 "cond_override cond old new \<equiv> |
60 "cond_override cond old new \<equiv> |
63 \<lambda> k. |
61 \<lambda> k. |
98 apply (rule dom_cond_override) |
96 apply (rule dom_cond_override) |
99 by (rule finite_UnI) |
97 by (rule finite_UnI) |
100 |
98 |
101 section {* Filter on Tables *} |
99 section {* Filter on Tables *} |
102 |
100 |
103 constdefs |
101 definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where |
104 filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" |
|
105 "filter_tab c t \<equiv> \<lambda> k. (case t k of |
102 "filter_tab c t \<equiv> \<lambda> k. (case t k of |
106 None \<Rightarrow> None |
103 None \<Rightarrow> None |
107 | Some x \<Rightarrow> if c k x then Some x else None)" |
104 | Some x \<Rightarrow> if c k x then Some x else None)" |
108 |
105 |
109 lemma filter_tab_empty[simp]: "filter_tab c empty = empty" |
106 lemma filter_tab_empty[simp]: "filter_tab c empty = empty" |