author huffman Mon, 27 Feb 2012 14:07:59 +0100 changeset 46703 b103fffd587f parent 46702 202a09ba37d8 (current diff) parent 46701 879f5c76ffb6 (diff) child 46704 f800eb467515
merged
```--- a/src/HOL/Big_Operators.thy	Mon Feb 27 11:38:56 2012 +0100
+++ b/src/HOL/Big_Operators.thy	Mon Feb 27 14:07:59 2012 +0100
@@ -523,6 +523,25 @@
case insert thus ?case by (auto simp: add_strict_mono)
qed

+lemma setsum_strict_mono_ex1:
+assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
+shows "setsum f A < setsum g A"
+proof-
+  from assms(3) obtain a where a: "a:A" "f a < g a" by blast
+  have "setsum f A = setsum f ((A-{a}) \<union> {a})"
+  also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
+    using `finite A` by(subst setsum_Un_disjoint) auto
+  also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
+  also have "setsum f {a} < setsum g {a}" using a by simp
+  also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
+    using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
+  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
+qed
+
lemma setsum_negf:
"setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
proof (cases "finite A")```
```--- a/src/HOL/IsaMakefile	Mon Feb 27 11:38:56 2012 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 27 14:07:59 2012 +0100
@@ -61,7 +61,6 @@
HOL-Nitpick_Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
-  HOL-Quickcheck_Examples \
HOL-Quotient_Examples \
HOL-Predicate_Compile_Examples \
HOL-Prolog \
@@ -96,7 +95,7 @@
HOL-Nominal-Examples

all: test-no-smlnj test images-no-smlnj images
-full: all benchmark
+full: all benchmark HOL-Quickcheck_Examples
smlnj: test images

```
```--- a/src/HOL/List.thy	Mon Feb 27 11:38:56 2012 +0100
+++ b/src/HOL/List.thy	Mon Feb 27 14:07:59 2012 +0100
@@ -960,6 +960,8 @@

subsubsection {* @{text set} *}

+declare set.simps [code_post]  --"pretty output"
+
lemma finite_set [iff]: "finite (set xs)"
by (induct xs) auto
```
```--- a/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Feb 27 11:38:56 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Feb 27 14:07:59 2012 +0100
@@ -1,4 +1,5 @@
use_thys [
+  "Find_Unused_Assms_Examples",
"Quickcheck_Examples",
"Quickcheck_Lattice_Examples"
];```