author nipkow Thu, 16 Aug 2012 15:08:42 +0200 changeset 48849 722de4ae08cb parent 48824 45d0e40b07af child 48850 efb8641b4944
abstracted lemmas
 src/HOL/Big_Operators.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Big_Operators.thy	Wed Aug 15 23:06:17 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Thu Aug 16 15:08:42 2012 +0200
@@ -39,11 +39,66 @@
then show ?thesis unfolding `A = B` by simp
qed

+lemma strong_F_cong [cong]:
+  "\<lbrakk> A = B; !!x. x:B =simp=> g x = h x \<rbrakk>
+   \<Longrightarrow> F (%x. g x) A = F (%x. h x) B"
+by (rule F_cong) (simp_all add: simp_implies_def)
+
lemma F_neutral[simp]: "F (%i. 1) A = 1"
by (cases "finite A") (simp_all add: neutral)

lemma F_neutral': "ALL a:A. g a = 1 \<Longrightarrow> F g A = 1"
-by (simp cong: F_cong)
+by simp
+
+lemma F_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow> F g A = F g (A - B) * F g B"
+by (metis Diff_partition union_disjoint Diff_disjoint finite_Un inf_commute sup_commute)
+
+lemma F_mono_neutral_cong_left:
+  assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
+  and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
+proof-
+  have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
+  have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
+  from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
+    by (auto intro: finite_subset)
+  show ?thesis using assms(4)
+    by (simp add: union_disjoint[OF f d, unfolded eq[symmetric]] F_neutral'[OF assms(3)])
+qed
+
+lemmas F_mono_neutral_cong_right = F_mono_neutral_cong_left[symmetric]
+
+lemma F_mono_neutral_left:
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
+by(blast intro: F_mono_neutral_cong_left)
+
+lemmas F_mono_neutral_right = F_mono_neutral_left[symmetric]
+
+lemma F_delta:
+  assumes fS: "finite S"
+  shows "F (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
+proof-
+  let ?f = "(\<lambda>k. if k=a then b k else 1)"
+  { assume a: "a \<notin> S"
+    hence "\<forall>k\<in>S. ?f k = 1" by simp
+    hence ?thesis  using a by simp }
+  moreover
+  { assume a: "a \<in> S"
+    let ?A = "S - {a}"
+    let ?B = "{a}"
+    have eq: "S = ?A \<union> ?B" using a by blast
+    have dj: "?A \<inter> ?B = {}" by simp
+    from fS have fAB: "finite ?A" "finite ?B" by auto
+    have "F ?f S = F ?f ?A * F ?f ?B"
+      using union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
+      by simp
+    then have ?thesis  using a by simp }
+  ultimately show ?thesis by blast
+qed
+
+lemma F_delta':
+  assumes fS: "finite S" shows
+  "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
+using F_delta[OF fS, of a b, symmetric] by (auto intro: F_cong)

lemma If_cases:
fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
@@ -144,14 +199,14 @@
assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B"
proof -
interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
-  from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD)
+  from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex o_def dest!:finite_imageD)
qed

+lemma setsum_reindex_id:
"inj_on f B ==> setsum f B = setsum id (f ` B)"

+lemma setsum_reindex_nonzero:
assumes fS: "finite S"
and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
shows "setsum h (f ` S) = setsum (h o f) S"
@@ -160,7 +215,7 @@
case 1 thus ?case by simp
next
case (2 x F)
-  {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
+  { assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
then obtain y where y: "y \<in> F" "f x = f y" by auto
from "2.hyps" y have xy: "x \<noteq> y" by auto

@@ -169,120 +224,81 @@
also have "\<dots> = setsum (h o f) (insert x F)"
unfolding setsum.insert[OF `finite F` `x\<notin>F`]
using h0
-      apply simp
+      apply (simp cong del:setsum.strong_F_cong)
apply (rule "2.hyps"(3))
apply (rule_tac y="y" in  "2.prems")
apply simp_all
done
-    finally have ?case .}
+    finally have ?case . }
moreover
-  {assume fxF: "f x \<notin> f ` F"
+  { assume fxF: "f x \<notin> f ` F"
have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
using fxF "2.hyps" by simp
also have "\<dots> = setsum (h o f) (insert x F)"
unfolding setsum.insert[OF `finite F` `x\<notin>F`]
-      apply simp
+      apply (simp cong del:setsum.strong_F_cong)
apply (rule cong [OF refl [of "op + (h (f x))"]])
apply (rule "2.hyps"(3))
apply (rule_tac y="y" in  "2.prems")
apply simp_all
done
-    finally have ?case .}
+    finally have ?case . }
ultimately show ?case by blast
qed

+lemma setsum_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
-  by (cases "finite A") (auto intro: setsum.cong)
+by (fact setsum.F_cong)

+lemma strong_setsum_cong:
"A = B ==> (!!x. x:B =simp=> f x = g x)
==> setsum (%x. f x) A = setsum (%x. g x) B"
-  by (rule setsum_cong) (simp_all add: simp_implies_def)
+by (fact setsum.strong_F_cong)

-lemma (in comm_monoid_add) setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
-  by (auto intro: setsum_cong)
+lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
+by (auto intro: setsum_cong)

+lemma setsum_reindex_cong:
"[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
==> setsum h B = setsum g A"

lemmas setsum_0 = setsum.F_neutral
lemmas setsum_0' = setsum.F_neutral'

-lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
+lemma setsum_Un_Int: "finite A ==> finite B ==>
setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-  by (fact setsum.union_inter)
+by (fact setsum.union_inter)

-lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B
+lemma setsum_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
-  by (fact setsum.union_disjoint)
+by (fact setsum.union_disjoint)
+
+lemma setsum_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
+    setsum f A = setsum f (A - B) + setsum f B"
+by(fact setsum.F_subset_diff)

lemma setsum_mono_zero_left:
-  assumes fT: "finite T" and ST: "S \<subseteq> T"
-  and z: "\<forall>i \<in> T - S. f i = 0"
-  shows "setsum f S = setsum f T"
-proof-
-  have eq: "T = S \<union> (T - S)" using ST by blast
-  have d: "S \<inter> (T - S) = {}" using ST by blast
-  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
-  show ?thesis
-  by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
-qed
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 0 \<rbrakk> \<Longrightarrow> setsum f S = setsum f T"
+by(fact setsum.F_mono_neutral_left)

-lemma setsum_mono_zero_right:
-  "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
-by(blast intro!: setsum_mono_zero_left[symmetric])
+lemmas setsum_mono_zero_right = setsum.F_mono_neutral_right

lemma setsum_mono_zero_cong_left:
-  assumes fT: "finite T" and ST: "S \<subseteq> T"
-  and z: "\<forall>i \<in> T - S. g i = 0"
-  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
-  shows "setsum f S = setsum g T"
-proof-
-  have eq: "T = S \<union> (T - S)" using ST by blast
-  have d: "S \<inter> (T - S) = {}" using ST by blast
-  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
-  show ?thesis
-    using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
-qed
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
+  \<Longrightarrow> setsum f S = setsum g T"
+by(fact setsum.F_mono_neutral_cong_left)

-lemma setsum_mono_zero_cong_right:
-  assumes fT: "finite T" and ST: "S \<subseteq> T"
-  and z: "\<forall>i \<in> T - S. f i = 0"
-  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
-  shows "setsum f T = setsum g S"
-using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto
+lemmas setsum_mono_zero_cong_right = setsum.F_mono_neutral_cong_right

-lemma setsum_delta:
-  assumes fS: "finite S"
-  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
-proof-
-  let ?f = "(\<lambda>k. if k=a then b k else 0)"
-  {assume a: "a \<notin> S"
-    hence "\<forall> k\<in> S. ?f k = 0" by simp
-    hence ?thesis  using a by simp}
-  moreover
-  {assume a: "a \<in> S"
-    let ?A = "S - {a}"
-    let ?B = "{a}"
-    have eq: "S = ?A \<union> ?B" using a by blast
-    have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto
-    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
-      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
-      by simp
-    then have ?thesis  using a by simp}
-  ultimately show ?thesis by blast
-qed
-lemma setsum_delta':
-  assumes fS: "finite S" shows
-  "setsum (\<lambda>k. if a = k then b k else 0) S =
-     (if a\<in> S then b a else 0)"
-  using setsum_delta[OF fS, of a b, symmetric]
-  by (auto intro: setsum_cong)
+lemma setsum_delta: "finite S \<Longrightarrow>
+  setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
+by(fact setsum.F_delta)
+
+lemma setsum_delta': "finite S \<Longrightarrow>
+  setsum (\<lambda>k. if a = k then b k else 0) S = (if a\<in> S then b a else 0)"
+by(fact setsum.F_delta')

lemma setsum_restrict_set:
assumes fA: "finite A"
@@ -906,18 +922,18 @@

lemma setprod_reindex:
"inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
-by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
+by(auto simp: setprod_def fold_image_reindex o_def dest!:finite_imageD)

lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"

lemma setprod_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
-by(fastforce simp: setprod_def intro: fold_image_cong)
+by(fact setprod.F_cong)

-lemma strong_setprod_cong[cong]:
+lemma strong_setprod_cong:
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
-by(fastforce simp: simp_implies_def setprod_def intro: fold_image_cong)
+by(fact setprod.strong_F_cong)

lemma setprod_reindex_cong: "inj_on f A ==>
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
@@ -951,56 +967,36 @@

lemma setprod_Un_Int: "finite A ==> finite B
==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
+by (fact setprod.union_inter)

lemma setprod_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
-by (subst setprod_Un_Int [symmetric], auto)
+by (fact setprod.union_disjoint)
+
+lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
+    setprod f A = setprod f (A - B) * setprod f B"
+by(fact setprod.F_subset_diff)

-lemma setprod_mono_one_left:
-  assumes fT: "finite T" and ST: "S \<subseteq> T"
-  and z: "\<forall>i \<in> T - S. f i = 1"
-  shows "setprod f S = setprod f T"
-proof-
-  have eq: "T = S \<union> (T - S)" using ST by blast
-  have d: "S \<inter> (T - S) = {}" using ST by blast
-  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
-  show ?thesis
-  by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
-qed
+lemma setprod_mono_one_left:
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
+by(fact setprod.F_mono_neutral_left)

-lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
+lemmas setprod_mono_one_right = setprod.F_mono_neutral_right

-lemma setprod_delta:
-  assumes fS: "finite S"
-  shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
-proof-
-  let ?f = "(\<lambda>k. if k=a then b k else 1)"
-  {assume a: "a \<notin> S"
-    hence "\<forall> k\<in> S. ?f k = 1" by simp
-    hence ?thesis  using a by (simp add: setprod_1) }
-  moreover
-  {assume a: "a \<in> S"
-    let ?A = "S - {a}"
-    let ?B = "{a}"
-    have eq: "S = ?A \<union> ?B" using a by blast
-    have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto
-    have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
-    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
-      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
-      by simp
-    then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
-  ultimately show ?thesis by blast
-qed
+lemma setprod_mono_one_cong_left:
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
+  \<Longrightarrow> setprod f S = setprod g T"
+by(fact setprod.F_mono_neutral_cong_left)
+
+lemmas setprod_mono_one_cong_right = setprod.F_mono_neutral_cong_right

-lemma setprod_delta':
-  assumes fS: "finite S" shows
-  "setprod (\<lambda>k. if a = k then b k else 1) S =
-     (if a\<in> S then b a else 1)"
-  using setprod_delta[OF fS, of a b, symmetric]
-  by (auto intro: setprod_cong)
+lemma setprod_delta: "finite S \<Longrightarrow>
+  setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
+by(fact setprod.F_delta)

+lemma setprod_delta': "finite S \<Longrightarrow>
+  setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
+by(fact setprod.F_delta')

lemma setprod_UN_disjoint:
"finite I ==> (ALL i:I. finite (A i)) ==>
@@ -1030,7 +1026,7 @@
apply (cases "finite B")
apply (cases "A={}", simp)