--- 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";
--- 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"
--- 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)
--- 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