src/HOL/Finite_Set.thy

   apply (induct set: Finites, simp)
   apply (simp add: le_SucI finite_imageI card_insert_if)
   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 *}
 
 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)

     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   by (simp add: setsum_def LC.fold_insert [OF LC.intro] add_left_commute)
 
 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)"
 by (auto simp add: setsum_reindex id_o)
 

   by (auto simp add: setprod_def LC_def LC.fold_insert
       mult_left_commute)
 
 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)"
 by (auto simp add: setprod_reindex id_o)