A few finite lemmas
authornipkow
Thu Jun 04 13:26:32 2009 +0200 (2009-06-04)
changeset 31438a1c4c1500abe
parent 31422 b8bdef62bfa6
child 31439 c02b3fd764f4
A few finite lemmas
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Jun 03 12:24:09 2009 -0700
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Jun 04 13:26:32 2009 +0200
     1.3 @@ -1333,6 +1333,10 @@
     1.4  apply (auto simp add: insert_Diff_if add_ac)
     1.5  done
     1.6  
     1.7 +lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
     1.8 +  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
     1.9 +unfolding setsum_diff1'[OF assms] by auto
    1.10 +
    1.11  (* By Jeremy Siek: *)
    1.12  
    1.13  lemma setsum_diff_nat: 
     2.1 --- a/src/HOL/Fun.thy	Wed Jun 03 12:24:09 2009 -0700
     2.2 +++ b/src/HOL/Fun.thy	Thu Jun 04 13:26:32 2009 +0200
     2.3 @@ -250,6 +250,10 @@
     2.4  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
     2.5  by (simp add: bij_betw_def)
     2.6  
     2.7 +lemma bij_betw_trans:
     2.8 +  "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
     2.9 +by(auto simp add:bij_betw_def comp_inj_on)
    2.10 +
    2.11  lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
    2.12  proof -
    2.13    have i: "inj_on f A" and s: "f ` A = B"
    2.14 @@ -300,6 +304,9 @@
    2.15  apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
    2.16  done
    2.17  
    2.18 +lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
    2.19 +by(blast dest: inj_onD)
    2.20 +
    2.21  lemma inj_on_image_Int:
    2.22     "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"
    2.23  apply (simp add: inj_on_def, blast)
     3.1 --- a/src/HOL/SetInterval.thy	Wed Jun 03 12:24:09 2009 -0700
     3.2 +++ b/src/HOL/SetInterval.thy	Thu Jun 04 13:26:32 2009 +0200
     3.3 @@ -468,7 +468,6 @@
     3.4  lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
     3.5    by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
     3.6  
     3.7 -
     3.8  lemma ex_bij_betw_nat_finite:
     3.9    "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
    3.10  apply(drule finite_imp_nat_seg_image_inj_on)
    3.11 @@ -479,6 +478,17 @@
    3.12    "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
    3.13  by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
    3.14  
    3.15 +lemma finite_same_card_bij:
    3.16 +  "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
    3.17 +apply(drule ex_bij_betw_finite_nat)
    3.18 +apply(drule ex_bij_betw_nat_finite)
    3.19 +apply(auto intro!:bij_betw_trans)
    3.20 +done
    3.21 +
    3.22 +lemma ex_bij_betw_nat_finite_1:
    3.23 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
    3.24 +by (rule finite_same_card_bij) auto
    3.25 +
    3.26  
    3.27  subsection {* Intervals of integers *}
    3.28