# HG changeset patch
# User nipkow
# Date 1101048260 -3600
# Node ID eedbb8d22ca28b5fb7ff07ff8a02daae58550e35
# Parent  a643fcbc3468c4c3135bac3721a0478a2d6d1dcf
added lemmas

diff -r a643fcbc3468 -r eedbb8d22ca2 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Sun Nov 21 12:52:03 2004 +0100
+++ b/src/HOL/Equiv_Relations.thy	Sun Nov 21 15:44:20 2004 +0100
@@ -320,6 +320,16 @@
     apply (simp_all add: Union_quotient equiv_type finite_quotient)
   done
 
+lemma card_quotient_disjoint:
+ "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
+apply(simp add:quotient_def)
+apply(subst card_UN_disjoint)
+   apply assumption
+  apply simp
+ apply(fastsimp simp add:inj_on_def)
+apply (simp add:setsum_constant_nat)
+done
+
 ML
 {*
 val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
diff -r a643fcbc3468 -r eedbb8d22ca2 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Nov 21 12:52:03 2004 +0100
+++ b/src/HOL/Fun.thy	Sun Nov 21 15:44:20 2004 +0100
@@ -158,6 +158,11 @@
      "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A"
 by (simp add: comp_def inj_on_def)
 
+lemma inj_on_imageI: "inj_on (g o f) A \<Longrightarrow> inj_on g (f ` A)"
+apply(simp add:inj_on_def image_def)
+apply blast
+done
+
 lemma inj_on_contraD: "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)"
 by (unfold inj_on_def, blast)
 
@@ -167,7 +172,7 @@
 lemma inj_on_empty[iff]: "inj_on f {}"
 by(simp add: inj_on_def)
 
-lemma subset_inj_on: "[| A<=B; inj_on f B |] ==> inj_on f A"
+lemma subset_inj_on: "[| inj_on f B; A <= B |] ==> inj_on f A"
 by (unfold inj_on_def, blast)
 
 lemma inj_on_Un:
@@ -364,6 +369,9 @@
 lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
 by (rule ext, auto)
 
+lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
+by(fastsimp simp:inj_on_def image_def)
+
 subsection{* overwrite *}
 
 lemma overwrite_emptyset[simp]: "f(g|{}) = f"
diff -r a643fcbc3468 -r eedbb8d22ca2 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Nov 21 12:52:03 2004 +0100
+++ b/src/HOL/List.thy	Sun Nov 21 15:44:20 2004 +0100
@@ -507,6 +507,12 @@
 lemma inj_map[iff]: "inj (map f) = inj f"
 by (blast dest: inj_mapD intro: inj_mapI)
 
+lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
+apply(rule inj_onI)
+apply(erule map_inj_on)
+apply(blast intro:inj_onI dest:inj_onD)
+done
+
 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
 by (induct xs, auto)
 
diff -r a643fcbc3468 -r eedbb8d22ca2 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Nov 21 12:52:03 2004 +0100
+++ b/src/HOL/Map.thy	Sun Nov 21 15:44:20 2004 +0100
@@ -130,6 +130,9 @@
   "((m(a|->b)) x = Some y) = (x = a \<and> b = y \<or> x \<noteq> a \<and> m x = Some y)"
 by auto
 
+lemma image_map_upd[simp]: "x \<notin> A \<Longrightarrow> m(x \<mapsto> y) ` A = m ` A"
+by fastsimp
+
 lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
 apply (unfold image_def)
 apply (simp (no_asm_use) add: full_SetCompr_eq)
@@ -523,4 +526,10 @@
 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   by (fastsimp simp add: map_le_def)
 
+lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
+by (fastsimp simp add: map_le_def map_add_def dom_def)
+
+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"
+by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)
+
 end