src/HOL/Bali/Table.thy
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13337 f75dfc606ac7
     1.1 --- a/src/HOL/Bali/Table.thy	Thu Feb 21 20:11:32 2002 +0100
     1.2 +++ b/src/HOL/Bali/Table.thy	Fri Feb 22 11:26:44 2002 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4  \end{itemize}
     1.5  *}
     1.6  
     1.7 -
     1.8  types ('a, 'b) table    (* table with key type 'a and contents type 'b *)
     1.9        = "'a \<leadsto> 'b"
    1.10        ('a, 'b) tables   (* non-unique table with key 'a and contents 'b *)
    1.11 @@ -148,6 +147,10 @@
    1.12   "\<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"
    1.13  by (auto simp add: filter_tab_def expand_fun_eq)
    1.14  
    1.15 +lemma filter_tab_all_False: 
    1.16 + "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
    1.17 +by (auto simp add: filter_tab_def expand_fun_eq)
    1.18 +
    1.19  lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
    1.20  apply (simp add: filter_tab_def expand_fun_eq)
    1.21  done
    1.22 @@ -180,6 +183,7 @@
    1.23      = filter_tab filterC (cond_override overC t s)"
    1.24  by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
    1.25  
    1.26 +
    1.27  section {* Misc. *}
    1.28  
    1.29  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"