--- a/src/HOL/Bali/Table.thy Thu Feb 21 20:11:32 2002 +0100
+++ b/src/HOL/Bali/Table.thy Fri Feb 22 11:26:44 2002 +0100
@@ -31,7 +31,6 @@
\end{itemize}
*}
-
types ('a, 'b) table (* table with key type 'a and contents type 'b *)
= "'a \<leadsto> 'b"
('a, 'b) tables (* non-unique table with key 'a and contents 'b *)
@@ -148,6 +147,10 @@
"\<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"
by (auto simp add: filter_tab_def expand_fun_eq)
+lemma filter_tab_all_False:
+ "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
+by (auto simp add: filter_tab_def expand_fun_eq)
+
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
apply (simp add: filter_tab_def expand_fun_eq)
done
@@ -180,6 +183,7 @@
= filter_tab filterC (cond_override overC t s)"
by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
+
section {* Misc. *}
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"