# HG changeset patch
# User nipkow
# Date 1109699332 -3600
# Node ID 03d4347b071d3f45d7a52b03b7b7983940fcd8cc
# Parent  2b3f9c493259eaadd9ec0f2ff2f88bece0b0c43b
integrated Jeremy's FiniteLib

diff -r 2b3f9c493259 -r 03d4347b071d src/HOL/Finite_Set.thy
--- 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")
diff -r 2b3f9c493259 -r 03d4347b071d src/HOL/Integ/IntDef.thy
--- 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"
diff -r 2b3f9c493259 -r 03d4347b071d src/HOL/Set.thy
--- 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)
diff -r 2b3f9c493259 -r 03d4347b071d src/HOL/SetInterval.thy
--- 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}"