added lemmas
authornipkow
Sun Nov 21 15:44:20 2004 +0100 (2004-11-21)
changeset 15303eedbb8d22ca2
parent 15302 a643fcbc3468
child 15304 3514ca74ac54
added lemmas
src/HOL/Equiv_Relations.thy
src/HOL/Fun.thy
src/HOL/List.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Sun Nov 21 12:52:03 2004 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Sun Nov 21 15:44:20 2004 +0100
     1.3 @@ -320,6 +320,16 @@
     1.4      apply (simp_all add: Union_quotient equiv_type finite_quotient)
     1.5    done
     1.6  
     1.7 +lemma card_quotient_disjoint:
     1.8 + "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
     1.9 +apply(simp add:quotient_def)
    1.10 +apply(subst card_UN_disjoint)
    1.11 +   apply assumption
    1.12 +  apply simp
    1.13 + apply(fastsimp simp add:inj_on_def)
    1.14 +apply (simp add:setsum_constant_nat)
    1.15 +done
    1.16 +
    1.17  ML
    1.18  {*
    1.19  val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
     2.1 --- a/src/HOL/Fun.thy	Sun Nov 21 12:52:03 2004 +0100
     2.2 +++ b/src/HOL/Fun.thy	Sun Nov 21 15:44:20 2004 +0100
     2.3 @@ -158,6 +158,11 @@
     2.4       "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A"
     2.5  by (simp add: comp_def inj_on_def)
     2.6  
     2.7 +lemma inj_on_imageI: "inj_on (g o f) A \<Longrightarrow> inj_on g (f ` A)"
     2.8 +apply(simp add:inj_on_def image_def)
     2.9 +apply blast
    2.10 +done
    2.11 +
    2.12  lemma inj_on_contraD: "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)"
    2.13  by (unfold inj_on_def, blast)
    2.14  
    2.15 @@ -167,7 +172,7 @@
    2.16  lemma inj_on_empty[iff]: "inj_on f {}"
    2.17  by(simp add: inj_on_def)
    2.18  
    2.19 -lemma subset_inj_on: "[| A<=B; inj_on f B |] ==> inj_on f A"
    2.20 +lemma subset_inj_on: "[| inj_on f B; A <= B |] ==> inj_on f A"
    2.21  by (unfold inj_on_def, blast)
    2.22  
    2.23  lemma inj_on_Un:
    2.24 @@ -364,6 +369,9 @@
    2.25  lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
    2.26  by (rule ext, auto)
    2.27  
    2.28 +lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
    2.29 +by(fastsimp simp:inj_on_def image_def)
    2.30 +
    2.31  subsection{* overwrite *}
    2.32  
    2.33  lemma overwrite_emptyset[simp]: "f(g|{}) = f"
     3.1 --- a/src/HOL/List.thy	Sun Nov 21 12:52:03 2004 +0100
     3.2 +++ b/src/HOL/List.thy	Sun Nov 21 15:44:20 2004 +0100
     3.3 @@ -507,6 +507,12 @@
     3.4  lemma inj_map[iff]: "inj (map f) = inj f"
     3.5  by (blast dest: inj_mapD intro: inj_mapI)
     3.6  
     3.7 +lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
     3.8 +apply(rule inj_onI)
     3.9 +apply(erule map_inj_on)
    3.10 +apply(blast intro:inj_onI dest:inj_onD)
    3.11 +done
    3.12 +
    3.13  lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
    3.14  by (induct xs, auto)
    3.15  
     4.1 --- a/src/HOL/Map.thy	Sun Nov 21 12:52:03 2004 +0100
     4.2 +++ b/src/HOL/Map.thy	Sun Nov 21 15:44:20 2004 +0100
     4.3 @@ -130,6 +130,9 @@
     4.4    "((m(a|->b)) x = Some y) = (x = a \<and> b = y \<or> x \<noteq> a \<and> m x = Some y)"
     4.5  by auto
     4.6  
     4.7 +lemma image_map_upd[simp]: "x \<notin> A \<Longrightarrow> m(x \<mapsto> y) ` A = m ` A"
     4.8 +by fastsimp
     4.9 +
    4.10  lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
    4.11  apply (unfold image_def)
    4.12  apply (simp (no_asm_use) add: full_SetCompr_eq)
    4.13 @@ -523,4 +526,10 @@
    4.14  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
    4.15    by (fastsimp simp add: map_le_def)
    4.16  
    4.17 +lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
    4.18 +by (fastsimp simp add: map_le_def map_add_def dom_def)
    4.19 +
    4.20 +lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
    4.21 +by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)
    4.22 +
    4.23  end