# HG changeset patch
# User nipkow
# Date 1091639462 -7200
# Node ID c108189645f81369b8ed4c3517e3ac9d020b3ea9
# Parent  78b5636eabc79dd005264d13c0a7e2eb2a1d3d75
added some inj_on thms

diff -r 78b5636eabc7 -r c108189645f8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 04 19:10:45 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 04 19:11:02 2004 +0200
@@ -521,15 +521,23 @@
   done
 
 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
-  apply (induct set: Finites, simp_all, atomize, safe)
-   apply (unfold inj_on_def, blast)
-  apply (subst card_insert_disjoint)
-    apply (erule finite_imageI, blast, blast)
-  done
+by (induct set: Finites, simp_all)
 
 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   by (simp add: card_seteq card_image)
 
+lemma eq_card_imp_inj_on:
+  "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
+apply(induct rule:finite_induct)
+ apply simp
+apply(frule card_image_le[where f = f])
+apply(simp add:card_insert_if split:if_splits)
+done
+
+lemma inj_on_iff_eq_card:
+  "finite A ==> inj_on f A = (card(f ` A) = card A)"
+by(blast intro: card_image eq_card_imp_inj_on)
+
 
 subsubsection {* Cardinality of the Powerset *}
 
@@ -813,14 +821,7 @@
 
 lemma setsum_reindex [rule_format]:
      "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
-apply (rule finite_induct, assumption, force)
-apply (rule impI, auto)
-apply (simp add: inj_on_def)
-apply (subgoal_tac "f x \<notin> f ` F")
-apply (subgoal_tac "finite (f ` F)")
-apply (auto simp add: setsum_insert)
-apply (simp add: inj_on_def)
-done
+by (rule finite_induct, auto)
 
 lemma setsum_reindex_id:
      "finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)"
@@ -1090,14 +1091,7 @@
 
 lemma setprod_reindex [rule_format]:
      "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
-apply (rule finite_induct, assumption, force)
-apply (rule impI, auto)
-apply (simp add: inj_on_def)
-apply (subgoal_tac "f x \<notin> f ` F")
-apply (subgoal_tac "finite (f ` F)")
-apply (auto simp add: setprod_insert)
-apply (simp add: inj_on_def)
-done
+by (rule finite_induct, auto)
 
 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
     setprod f B = setprod id (f ` B)"
diff -r 78b5636eabc7 -r c108189645f8 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Aug 04 19:10:45 2004 +0200
+++ b/src/HOL/Fun.thy	Wed Aug 04 19:11:02 2004 +0200
@@ -162,9 +162,30 @@
 lemma inj_singleton: "inj (%s. {s})"
 by (simp add: inj_on_def)
 
+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"
 by (unfold inj_on_def, blast)
 
+lemma inj_on_Un:
+ "inj_on f (A Un B) =
+  (inj_on f A & inj_on f B & f`(A-B) Int f`(B-A) = {})"
+apply(unfold inj_on_def)
+apply (blast intro:sym)
+done
+
+lemma inj_on_insert[iff]:
+  "inj_on f (insert a A) = (inj_on f A & f a ~: f`(A-{a}))"
+apply(unfold inj_on_def)
+apply (blast intro:sym)
+done
+
+lemma inj_on_diff: "inj_on f A ==> inj_on f (A-B)"
+apply(unfold inj_on_def)
+apply (blast)
+done
+
 
 subsection{*The Predicate @{term surj}: Surjectivity*}