added some inj_on thms
authornipkow
Wed Aug 04 19:11:02 2004 +0200 (2004-08-04)
changeset 15111c108189645f8
parent 15110 78b5636eabc7
child 15112 6f0772a94299
added some inj_on thms
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Aug 04 19:10:45 2004 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Aug 04 19:11:02 2004 +0200
     1.3 @@ -521,15 +521,23 @@
     1.4    done
     1.5  
     1.6  lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
     1.7 -  apply (induct set: Finites, simp_all, atomize, safe)
     1.8 -   apply (unfold inj_on_def, blast)
     1.9 -  apply (subst card_insert_disjoint)
    1.10 -    apply (erule finite_imageI, blast, blast)
    1.11 -  done
    1.12 +by (induct set: Finites, simp_all)
    1.13  
    1.14  lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
    1.15    by (simp add: card_seteq card_image)
    1.16  
    1.17 +lemma eq_card_imp_inj_on:
    1.18 +  "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
    1.19 +apply(induct rule:finite_induct)
    1.20 + apply simp
    1.21 +apply(frule card_image_le[where f = f])
    1.22 +apply(simp add:card_insert_if split:if_splits)
    1.23 +done
    1.24 +
    1.25 +lemma inj_on_iff_eq_card:
    1.26 +  "finite A ==> inj_on f A = (card(f ` A) = card A)"
    1.27 +by(blast intro: card_image eq_card_imp_inj_on)
    1.28 +
    1.29  
    1.30  subsubsection {* Cardinality of the Powerset *}
    1.31  
    1.32 @@ -813,14 +821,7 @@
    1.33  
    1.34  lemma setsum_reindex [rule_format]:
    1.35       "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
    1.36 -apply (rule finite_induct, assumption, force)
    1.37 -apply (rule impI, auto)
    1.38 -apply (simp add: inj_on_def)
    1.39 -apply (subgoal_tac "f x \<notin> f ` F")
    1.40 -apply (subgoal_tac "finite (f ` F)")
    1.41 -apply (auto simp add: setsum_insert)
    1.42 -apply (simp add: inj_on_def)
    1.43 -done
    1.44 +by (rule finite_induct, auto)
    1.45  
    1.46  lemma setsum_reindex_id:
    1.47       "finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)"
    1.48 @@ -1090,14 +1091,7 @@
    1.49  
    1.50  lemma setprod_reindex [rule_format]:
    1.51       "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
    1.52 -apply (rule finite_induct, assumption, force)
    1.53 -apply (rule impI, auto)
    1.54 -apply (simp add: inj_on_def)
    1.55 -apply (subgoal_tac "f x \<notin> f ` F")
    1.56 -apply (subgoal_tac "finite (f ` F)")
    1.57 -apply (auto simp add: setprod_insert)
    1.58 -apply (simp add: inj_on_def)
    1.59 -done
    1.60 +by (rule finite_induct, auto)
    1.61  
    1.62  lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
    1.63      setprod f B = setprod id (f ` B)"
     2.1 --- a/src/HOL/Fun.thy	Wed Aug 04 19:10:45 2004 +0200
     2.2 +++ b/src/HOL/Fun.thy	Wed Aug 04 19:11:02 2004 +0200
     2.3 @@ -162,9 +162,30 @@
     2.4  lemma inj_singleton: "inj (%s. {s})"
     2.5  by (simp add: inj_on_def)
     2.6  
     2.7 +lemma inj_on_empty[iff]: "inj_on f {}"
     2.8 +by(simp add: inj_on_def)
     2.9 +
    2.10  lemma subset_inj_on: "[| A<=B; inj_on f B |] ==> inj_on f A"
    2.11  by (unfold inj_on_def, blast)
    2.12  
    2.13 +lemma inj_on_Un:
    2.14 + "inj_on f (A Un B) =
    2.15 +  (inj_on f A & inj_on f B & f`(A-B) Int f`(B-A) = {})"
    2.16 +apply(unfold inj_on_def)
    2.17 +apply (blast intro:sym)
    2.18 +done
    2.19 +
    2.20 +lemma inj_on_insert[iff]:
    2.21 +  "inj_on f (insert a A) = (inj_on f A & f a ~: f`(A-{a}))"
    2.22 +apply(unfold inj_on_def)
    2.23 +apply (blast intro:sym)
    2.24 +done
    2.25 +
    2.26 +lemma inj_on_diff: "inj_on f A ==> inj_on f (A-B)"
    2.27 +apply(unfold inj_on_def)
    2.28 +apply (blast)
    2.29 +done
    2.30 +
    2.31  
    2.32  subsection{*The Predicate @{term surj}: Surjectivity*}
    2.33