author nipkow Thu, 04 Jun 2009 13:26:32 +0200 changeset 31438 a1c4c1500abe parent 31422 b8bdef62bfa6 child 31439 c02b3fd764f4
A few finite lemmas
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Fun.thy file | annotate | diff | comparison | revisions src/HOL/SetInterval.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Finite_Set.thy	Wed Jun 03 12:24:09 2009 -0700
+++ b/src/HOL/Finite_Set.thy	Thu Jun 04 13:26:32 2009 +0200
@@ -1333,6 +1333,10 @@
done

+lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
+  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
+unfolding setsum_diff1'[OF assms] by auto
+
(* By Jeremy Siek: *)

lemma setsum_diff_nat: ```
```--- a/src/HOL/Fun.thy	Wed Jun 03 12:24:09 2009 -0700
+++ b/src/HOL/Fun.thy	Thu Jun 04 13:26:32 2009 +0200
@@ -250,6 +250,10 @@
lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"

+lemma bij_betw_trans:
+  "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
+
lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
proof -
have i: "inj_on f A" and s: "f ` A = B"
@@ -300,6 +304,9 @@
apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
done

+lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
+by(blast dest: inj_onD)
+
lemma inj_on_image_Int:
"[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"
```--- a/src/HOL/SetInterval.thy	Wed Jun 03 12:24:09 2009 -0700
+++ b/src/HOL/SetInterval.thy	Thu Jun 04 13:26:32 2009 +0200
@@ -468,7 +468,6 @@
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)

-
lemma ex_bij_betw_nat_finite:
"finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
apply(drule finite_imp_nat_seg_image_inj_on)
@@ -479,6 +478,17 @@
"finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)

+lemma finite_same_card_bij:
+  "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
+apply(drule ex_bij_betw_finite_nat)
+apply(drule ex_bij_betw_nat_finite)
+apply(auto intro!:bij_betw_trans)
+done
+
+lemma ex_bij_betw_nat_finite_1:
+  "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
+by (rule finite_same_card_bij) auto
+

subsection {* Intervals of integers *}
```