--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 01 09:31:10 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 01 19:53:30 2011 +0200
@@ -397,10 +397,6 @@
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
by (metis affine_affine_hull hull_same mem_def)
-lemma setsum_restrict_set'': assumes "finite A"
- shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x then f x else 0)"
- unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] ..
-
subsection {* Some explicit formulations (from Lars Schewe). *}
lemma affine: fixes V::"'a::real_vector set"
--- a/src/HOL/Predicate.thy Mon Aug 01 09:31:10 2011 -0700
+++ b/src/HOL/Predicate.thy Mon Aug 01 19:53:30 2011 +0200
@@ -741,11 +741,12 @@
by simp
lemma closure_of_bool_cases [no_atp]:
-assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
-assumes "f = (%u. True) \<Longrightarrow> P f"
-shows "P f"
+ fixes f :: "unit \<Rightarrow> bool"
+ assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
+ assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
+ shows "P f"
proof -
- have "f = (%u. False) \<or> f = (%u. True)"
+ have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
apply (cases "f ()")
apply (rule disjI2)
apply (rule ext)
@@ -758,19 +759,18 @@
qed
lemma unit_pred_cases:
-assumes "P \<bottom>"
-assumes "P (single ())"
-shows "P Q"
-using assms
-unfolding bot_pred_def Collect_def empty_def single_def
-apply (cases Q)
-apply simp
-apply (rule_tac f="fun" in closure_of_bool_cases)
-apply auto
-apply (subgoal_tac "(%x. () = x) = (%x. True)")
-apply auto
-done
-
+ assumes "P \<bottom>"
+ assumes "P (single ())"
+ shows "P Q"
+using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
+ fix f
+ assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
+ then have "P (Pred f)"
+ by (cases _ f rule: closure_of_bool_cases) simp_all
+ moreover assume "Q = Pred f"
+ ultimately show "P Q" by simp
+qed
+
lemma holds_if_pred:
"holds (if_pred b) = b"
unfolding if_pred_eq holds_eq
--- a/src/HOL/SetInterval.thy Mon Aug 01 09:31:10 2011 -0700
+++ b/src/HOL/SetInterval.thy Mon Aug 01 19:53:30 2011 +0200
@@ -14,6 +14,7 @@
context ord
begin
+
definition
lessThan :: "'a => 'a set" ("(1{..<_})") where
"{..<u} == {x. x < u}"
@@ -1162,12 +1163,18 @@
(if m <= n then f m - f(n + 1) else 0)"
by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
-lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
+lemma setsum_restrict_set':
+ "finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)"
+ by (simp add: setsum_restrict_set [symmetric] Int_def)
+
+lemma setsum_restrict_set'':
+ "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x then f x else 0)"
+ by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])
lemma setsum_setsum_restrict:
- "finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
- by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
- (rule setsum_commute)
+ "finite S \<Longrightarrow> finite T \<Longrightarrow>
+ setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y \<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
+ by (simp add: setsum_restrict_set'') (rule setsum_commute)
lemma setsum_image_gen: assumes fS: "finite S"
shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"