src/HOL/Finite_Set.thy

 (*  Title:      HOL/Finite_Set.thy
     ID:         $Id$
     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
                 Additions by Jeremy Avigad in Feb 2004
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Finite sets *}
 
 theory Finite_Set = Divides + Power + Inductive:

 lemma setsum_insert [simp]:
     "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"
+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
-
-lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
-    setsum f B = setsum id (f ` B)"
+done
+
+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)
-
-lemma setsum_reindex_cong: "finite A ==> inj_on f A ==>
-    B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
-  by (frule setsum_reindex, assumption, simp)
 
 lemma setsum_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   apply (case_tac "finite B")
    prefer 2 apply (simp add: setsum_def, simp)

   apply (erule ssubst)
   apply (drule spec)
   apply (erule (1) notE impE)
   apply (simp add: Ball_def del:insert_Diff_single)
   done
+
+lemma setsum_reindex_cong:
+     "[|finite A; inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
+      ==> setsum h B = setsum g A"
+  by (simp add: setsum_reindex cong: setsum_cong) 
 
 lemma setsum_0: "setsum (%i. 0) A = 0"
   apply (case_tac "finite A")
    prefer 2 apply (simp add: setsum_def)
   apply (erule finite_induct, auto)

 
 lemma card_inj_on_le:
     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
 apply (subgoal_tac "finite A") 
  apply (force intro: card_mono simp add: card_image [symmetric])
-apply (blast intro: Finite_Set.finite_imageD dest: finite_subset) 
+apply (blast intro: finite_imageD dest: finite_subset) 
 done
 
 lemma card_bij_eq:
     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
        finite A; finite B |] ==> card A = card B"