src/HOL/Finite_Set.thy
changeset 15111 c108189645f8
parent 15074 277b3a4da341
child 15124 1d9b4fcd222d
equal deleted inserted replaced
15110:78b5636eabc7 15111:c108189645f8
   519   apply (induct set: Finites, simp)
   519   apply (induct set: Finites, simp)
   520   apply (simp add: le_SucI finite_imageI card_insert_if)
   520   apply (simp add: le_SucI finite_imageI card_insert_if)
   521   done
   521   done
   522 
   522 
   523 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
   523 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
   524   apply (induct set: Finites, simp_all, atomize, safe)
   524 by (induct set: Finites, simp_all)
   525    apply (unfold inj_on_def, blast)
       
   526   apply (subst card_insert_disjoint)
       
   527     apply (erule finite_imageI, blast, blast)
       
   528   done
       
   529 
   525 
   530 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   526 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   531   by (simp add: card_seteq card_image)
   527   by (simp add: card_seteq card_image)
       
   528 
       
   529 lemma eq_card_imp_inj_on:
       
   530   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
       
   531 apply(induct rule:finite_induct)
       
   532  apply simp
       
   533 apply(frule card_image_le[where f = f])
       
   534 apply(simp add:card_insert_if split:if_splits)
       
   535 done
       
   536 
       
   537 lemma inj_on_iff_eq_card:
       
   538   "finite A ==> inj_on f A = (card(f ` A) = card A)"
       
   539 by(blast intro: card_image eq_card_imp_inj_on)
   532 
   540 
   533 
   541 
   534 subsubsection {* Cardinality of the Powerset *}
   542 subsubsection {* Cardinality of the Powerset *}
   535 
   543 
   536 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
   544 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
   811     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   819     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   812   by (simp add: setsum_def LC.fold_insert [OF LC.intro] add_left_commute)
   820   by (simp add: setsum_def LC.fold_insert [OF LC.intro] add_left_commute)
   813 
   821 
   814 lemma setsum_reindex [rule_format]:
   822 lemma setsum_reindex [rule_format]:
   815      "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   823      "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   816 apply (rule finite_induct, assumption, force)
   824 by (rule finite_induct, auto)
   817 apply (rule impI, auto)
       
   818 apply (simp add: inj_on_def)
       
   819 apply (subgoal_tac "f x \<notin> f ` F")
       
   820 apply (subgoal_tac "finite (f ` F)")
       
   821 apply (auto simp add: setsum_insert)
       
   822 apply (simp add: inj_on_def)
       
   823 done
       
   824 
   825 
   825 lemma setsum_reindex_id:
   826 lemma setsum_reindex_id:
   826      "finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)"
   827      "finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)"
   827 by (auto simp add: setsum_reindex id_o)
   828 by (auto simp add: setsum_reindex id_o)
   828 
   829 
  1088   by (auto simp add: setprod_def LC_def LC.fold_insert
  1089   by (auto simp add: setprod_def LC_def LC.fold_insert
  1089       mult_left_commute)
  1090       mult_left_commute)
  1090 
  1091 
  1091 lemma setprod_reindex [rule_format]:
  1092 lemma setprod_reindex [rule_format]:
  1092      "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
  1093      "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
  1093 apply (rule finite_induct, assumption, force)
  1094 by (rule finite_induct, auto)
  1094 apply (rule impI, auto)
       
  1095 apply (simp add: inj_on_def)
       
  1096 apply (subgoal_tac "f x \<notin> f ` F")
       
  1097 apply (subgoal_tac "finite (f ` F)")
       
  1098 apply (auto simp add: setprod_insert)
       
  1099 apply (simp add: inj_on_def)
       
  1100 done
       
  1101 
  1095 
  1102 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
  1096 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
  1103     setprod f B = setprod id (f ` B)"
  1097     setprod f B = setprod id (f ` B)"
  1104 by (auto simp add: setprod_reindex id_o)
  1098 by (auto simp add: setprod_reindex id_o)
  1105 
  1099