--- a/src/HOL/Finite_Set.thy Tue Mar 01 05:44:13 2005 +0100
+++ b/src/HOL/Finite_Set.thy Tue Mar 01 18:48:52 2005 +0100
@@ -895,8 +895,11 @@
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
+lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
+ by (rule setsum_cong[OF refl], auto);
+
lemma setsum_reindex_cong:
- "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|]
+ "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
==> setsum h B = setsum g A"
by (simp add: setsum_reindex cong: setsum_cong)
@@ -1066,6 +1069,17 @@
by (simp add: setsum_def)
qed
+lemma setsum_strict_mono:
+fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
+assumes fin_ne: "finite A" "A \<noteq> {}"
+shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A"
+using fin_ne
+proof (induct rule: finite_ne_induct)
+ case singleton thus ?case by simp
+next
+ case insert thus ?case by (auto simp: add_strict_mono)
+qed
+
lemma setsum_negf:
"setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
proof (cases "finite A")
--- a/src/HOL/Integ/IntDef.thy Tue Mar 01 05:44:13 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy Tue Mar 01 18:48:52 2005 +0100
@@ -764,31 +764,31 @@
text{*By Jeremy Avigad*}
-lemma setsum_of_nat: "of_nat (setsum f A) = setsum (of_nat \<circ> f) A"
+lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
apply (case_tac "finite A")
apply (erule finite_induct, auto)
done
-lemma setsum_of_int: "of_int (setsum f A) = setsum (of_int \<circ> f) A"
+lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
apply (case_tac "finite A")
apply (erule finite_induct, auto)
done
-lemma int_setsum: "int (setsum f A) = setsum (int \<circ> f) A"
- by (simp add: int_eq_of_nat setsum_of_nat)
+lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
+ by (simp add: int_eq_of_nat of_nat_setsum)
-lemma setprod_of_nat: "of_nat (setprod f A) = setprod (of_nat \<circ> f) A"
+lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
apply (case_tac "finite A")
apply (erule finite_induct, auto)
done
-lemma setprod_of_int: "of_int (setprod f A) = setprod (of_int \<circ> f) A"
+lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
apply (case_tac "finite A")
apply (erule finite_induct, auto)
done
-lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
- by (simp add: int_eq_of_nat setprod_of_nat)
+lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
+ by (simp add: int_eq_of_nat of_nat_setprod)
lemma setprod_nonzero_nat:
"finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
--- a/src/HOL/Set.thy Tue Mar 01 05:44:13 2005 +0100
+++ b/src/HOL/Set.thy Tue Mar 01 18:48:52 2005 +0100
@@ -520,6 +520,10 @@
apply (rule Collect_mem_eq)
done
+(* Due to Brian Huffman *)
+lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
+by(auto intro:set_ext)
+
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
-- {* Anti-symmetry of the subset relation. *}
by (rules intro: set_ext subsetD)
--- a/src/HOL/SetInterval.thy Tue Mar 01 05:44:13 2005 +0100
+++ b/src/HOL/SetInterval.thy Tue Mar 01 18:48:52 2005 +0100
@@ -168,26 +168,18 @@
subsection {*Two-sided intervals*}
-text {* @{text greaterThanLessThan} *}
-
lemma greaterThanLessThan_iff [simp]:
"(i : {l<..<u}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
-text {* @{text atLeastLessThan} *}
-
lemma atLeastLessThan_iff [simp]:
"(i : {l..<u}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
-text {* @{text greaterThanAtMost} *}
-
lemma greaterThanAtMost_iff [simp]:
"(i : {l<..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
-text {* @{text atLeastAtMost} *}
-
lemma atLeastAtMost_iff [simp]:
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
@@ -196,6 +188,16 @@
If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
seems to take forever (more than one hour). *}
+subsubsection{* Emptyness and singletons *}
+
+lemma atLeastAtMost_empty [simp]: "n < m ==> {m::'a::order..n} = {}";
+ by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
+
+lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n::'a::order} = {}"
+by (auto simp add: atLeastLessThan_def)
+
+lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}";
+ by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
subsection {* Intervals of natural numbers *}
@@ -268,12 +270,6 @@
lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
by (simp add: atLeastLessThan_def)
-lemma atLeastLessThan_self [simp]: "{n::'a::order..<n} = {}"
-by (auto simp add: atLeastLessThan_def)
-
-lemma atLeastLessThan_empty: "n \<le> m ==> {m..<n::'a::order} = {}"
-by (auto simp add: atLeastLessThan_def)
-
subsubsection {* Intervals of nats with @{term Suc} *}
text{*Not a simprule because the RHS is too messy.*}
@@ -301,6 +297,9 @@
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
greaterThanLessThan_def)
+lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
+by (auto simp add: atLeastAtMost_def)
+
subsubsection {* Finiteness *}
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
@@ -389,8 +388,6 @@
apply (subst image_atLeastZeroLessThan_int, assumption)
apply (rule finite_imageI)
apply auto
- apply (subgoal_tac "{0..<u} = {}")
- apply auto
done
lemma image_atLeastLessThan_int_shift:
@@ -615,8 +612,14 @@
setsum f {a..<b} = setsum g {c..<d}"
by(rule setsum_cong, simp_all)
+lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
+ (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
+by (auto simp:add_ac atLeastAtMostSuc_conv)
+
+(* FIXME delete
lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
by (simp add:lessThan_Suc)
+*)
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"