src/HOL/Big_Operators.thy
author hoelzl
Thu, 26 May 2011 14:12:03 +0200
changeset 42986 11fd8c04ea24
parent 42871 1c0b99f950d9
child 44845 5e51075cbd97
permissions -rw-r--r--
generalize setsum_cases
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35719
99b6152aedf5 split off theory Big_Operators from theory Finite_Set
haftmann
parents: 35577
diff changeset
     1
(*  Title:      HOL/Big_Operators.thy
12396
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     2
    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
     3
                with contributions by Jeremy Avigad
12396
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     4
*)
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     5
35719
99b6152aedf5 split off theory Big_Operators from theory Finite_Set
haftmann
parents: 35577
diff changeset
     6
header {* Big operators and finite (non-empty) sets *}
26041
c2e15e65165f locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents: 25571
diff changeset
     7
35719
99b6152aedf5 split off theory Big_Operators from theory Finite_Set
haftmann
parents: 35577
diff changeset
     8
theory Big_Operators
35722
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
     9
imports Plain
26041
c2e15e65165f locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents: 25571
diff changeset
    10
begin
c2e15e65165f locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents: 25571
diff changeset
    11
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    12
subsection {* Generic monoid operation over a set *}
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    13
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    14
no_notation times (infixl "*" 70)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    15
no_notation Groups.one ("1")
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    16
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    17
locale comm_monoid_big = comm_monoid +
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    18
  fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    19
  assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    20
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    21
sublocale comm_monoid_big < folding_image proof
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    22
qed (simp add: F_eq)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    23
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    24
context comm_monoid_big
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    25
begin
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    26
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    27
lemma infinite [simp]:
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    28
  "\<not> finite A \<Longrightarrow> F g A = 1"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    29
  by (simp add: F_eq)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    30
42986
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    31
lemma F_cong:
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    32
  assumes "A = B" "\<And>x. x \<in> B \<Longrightarrow> h x = g x"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    33
  shows "F h A = F g B"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    34
proof cases
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    35
  assume "finite A"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    36
  with assms show ?thesis unfolding `A = B` by (simp cong: cong)
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    37
next
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    38
  assume "\<not> finite A"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    39
  then show ?thesis unfolding `A = B` by simp
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    40
qed
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    41
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    42
lemma If_cases:
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    43
  fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    44
  assumes fA: "finite A"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    45
  shows "F (\<lambda>x. if P x then h x else g x) A =
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    46
         F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    47
proof-
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    48
  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    49
          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    50
    by blast+
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    51
  from fA 
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    52
  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    53
  let ?g = "\<lambda>x. if P x then h x else g x"
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    54
  from union_disjoint[OF f a(2), of ?g] a(1)
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    55
  show ?thesis
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    56
    by (subst (1 2) F_cong) simp_all
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    57
qed
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
    58
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    59
end
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    60
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    61
text {* for ad-hoc proofs for @{const fold_image} *}
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    62
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    63
lemma (in comm_monoid_add) comm_monoid_mult:
36635
080b755377c0 locale predicates of classes carry a mandatory "class" prefix
haftmann
parents: 36622
diff changeset
    64
  "class.comm_monoid_mult (op +) 0"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    65
proof qed (auto intro: add_assoc add_commute)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    66
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    67
notation times (infixl "*" 70)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    68
notation Groups.one ("1")
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    69
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    70
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    71
subsection {* Generalized summation over a set *}
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    72
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    73
definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    74
  "setsum f A = (if finite A then fold_image (op +) f 0 A else 0)"
26041
c2e15e65165f locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents: 25571
diff changeset
    75
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    76
sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
    77
qed (fact setsum_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    78
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
    79
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21249
diff changeset
    80
  Setsum  ("\<Sum>_" [1000] 999) where
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
    81
  "\<Sum>A == setsum (%x. x) A"
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
    82
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    83
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    84
written @{text"\<Sum>x\<in>A. e"}. *}
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    85
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    86
syntax
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
    87
  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    88
syntax (xsymbols)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
    89
  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    90
syntax (HTML output)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
    91
  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    92
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    93
translations -- {* Beware of argument permutation! *}
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
    94
  "SUM i:A. b" == "CONST setsum (%i. b) A"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
    95
  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    96
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    97
text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    98
 @{text"\<Sum>x|P. e"}. *}
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
    99
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   100
syntax
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   101
  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   102
syntax (xsymbols)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   103
  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   104
syntax (HTML output)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   105
  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   106
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   107
translations
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   108
  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   109
  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   110
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   111
print_translation {*
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   112
let
35115
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   113
  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   114
        if x <> y then raise Match
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   115
        else
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   116
          let
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 41550
diff changeset
   117
            val x' = Syntax_Trans.mark_bound x;
35115
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   118
            val t' = subst_bound (x', t);
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   119
            val P' = subst_bound (x', P);
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 41550
diff changeset
   120
          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
35115
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   121
    | setsum_tr' _ = raise Match;
446c5063e4fd modernized translations;
wenzelm
parents: 35034
diff changeset
   122
in [(@{const_syntax setsum}, setsum_tr')] end
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   123
*}
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   124
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   125
lemma setsum_empty:
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   126
  "setsum f {} = 0"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   127
  by (fact setsum.empty)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   128
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   129
lemma setsum_insert:
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   130
  "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   131
  by (fact setsum.insert)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   132
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   133
lemma setsum_infinite:
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   134
  "~ finite A ==> setsum f A = 0"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   135
  by (fact setsum.infinite)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   136
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   137
lemma (in comm_monoid_add) setsum_reindex:
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   138
  assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   139
proof -
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   140
  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   141
  from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   142
qed
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   143
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   144
lemma (in comm_monoid_add) setsum_reindex_id:
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   145
  "inj_on f B ==> setsum f B = setsum id (f ` B)"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   146
  by (simp add: setsum_reindex)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   147
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   148
lemma (in comm_monoid_add) setsum_reindex_nonzero: 
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   149
  assumes fS: "finite S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   150
  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"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   151
  shows "setsum h (f ` S) = setsum (h o f) S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   152
using nz
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   153
proof(induct rule: finite_induct[OF fS])
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   154
  case 1 thus ?case by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   155
next
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   156
  case (2 x F) 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   157
  {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   158
    then obtain y where y: "y \<in> F" "f x = f y" by auto 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   159
    from "2.hyps" y have xy: "x \<noteq> y" by auto
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   160
    
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   161
    from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   162
    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   163
    also have "\<dots> = setsum (h o f) (insert x F)" 
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   164
      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   165
      using h0
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   166
      apply simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   167
      apply (rule "2.hyps"(3))
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   168
      apply (rule_tac y="y" in  "2.prems")
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   169
      apply simp_all
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   170
      done
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   171
    finally have ?case .}
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   172
  moreover
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   173
  {assume fxF: "f x \<notin> f ` F"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   174
    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   175
      using fxF "2.hyps" by simp 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   176
    also have "\<dots> = setsum (h o f) (insert x F)"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   177
      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   178
      apply simp
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   179
      apply (rule cong [OF refl [of "op + (h (f x))"]])
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   180
      apply (rule "2.hyps"(3))
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   181
      apply (rule_tac y="y" in  "2.prems")
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   182
      apply simp_all
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   183
      done
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   184
    finally have ?case .}
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   185
  ultimately show ?case by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   186
qed
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   187
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   188
lemma (in comm_monoid_add) setsum_cong:
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   189
  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   190
  by (cases "finite A") (auto intro: setsum.cong)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   191
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   192
lemma (in comm_monoid_add) strong_setsum_cong [cong]:
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16632
diff changeset
   193
  "A = B ==> (!!x. x:B =simp=> f x = g x)
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16632
diff changeset
   194
   ==> setsum (%x. f x) A = setsum (%x. g x) B"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   195
  by (rule setsum_cong) (simp_all add: simp_implies_def)
16632
ad2895beef79 Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents: 16550
diff changeset
   196
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   197
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"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   198
  by (auto intro: setsum_cong)
15554
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   199
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   200
lemma (in comm_monoid_add) setsum_reindex_cong:
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   201
   "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   202
    ==> setsum h B = setsum g A"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   203
  by (simp add: setsum_reindex)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   204
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   205
lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   206
  by (cases "finite A") (erule finite_induct, auto)
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   207
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   208
lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   209
  by (simp add:setsum_cong)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   210
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   211
lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   212
  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   213
  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   214
  by (fact setsum.union_inter)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   215
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   216
lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   217
  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   218
  by (fact setsum.union_disjoint)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   219
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   220
lemma setsum_mono_zero_left: 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   221
  assumes fT: "finite T" and ST: "S \<subseteq> T"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   222
  and z: "\<forall>i \<in> T - S. f i = 0"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   223
  shows "setsum f S = setsum f T"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   224
proof-
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   225
  have eq: "T = S \<union> (T - S)" using ST by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   226
  have d: "S \<inter> (T - S) = {}" using ST by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   227
  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   228
  show ?thesis 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   229
  by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   230
qed
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   231
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   232
lemma setsum_mono_zero_right: 
30837
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   233
  "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   234
by(blast intro!: setsum_mono_zero_left[symmetric])
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   235
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   236
lemma setsum_mono_zero_cong_left: 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   237
  assumes fT: "finite T" and ST: "S \<subseteq> T"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   238
  and z: "\<forall>i \<in> T - S. g i = 0"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   239
  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   240
  shows "setsum f S = setsum g T"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   241
proof-
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   242
  have eq: "T = S \<union> (T - S)" using ST by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   243
  have d: "S \<inter> (T - S) = {}" using ST by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   244
  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   245
  show ?thesis 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   246
    using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   247
qed
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   248
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   249
lemma setsum_mono_zero_cong_right: 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   250
  assumes fT: "finite T" and ST: "S \<subseteq> T"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   251
  and z: "\<forall>i \<in> T - S. f i = 0"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   252
  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   253
  shows "setsum f T = setsum g S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   254
using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   255
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   256
lemma setsum_delta: 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   257
  assumes fS: "finite S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   258
  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   259
proof-
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   260
  let ?f = "(\<lambda>k. if k=a then b k else 0)"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   261
  {assume a: "a \<notin> S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   262
    hence "\<forall> k\<in> S. ?f k = 0" by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   263
    hence ?thesis  using a by simp}
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   264
  moreover 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   265
  {assume a: "a \<in> S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   266
    let ?A = "S - {a}"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   267
    let ?B = "{a}"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   268
    have eq: "S = ?A \<union> ?B" using a by blast 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   269
    have dj: "?A \<inter> ?B = {}" by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   270
    from fS have fAB: "finite ?A" "finite ?B" by auto  
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   271
    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   272
      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   273
      by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   274
    then have ?thesis  using a by simp}
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   275
  ultimately show ?thesis by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   276
qed
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   277
lemma setsum_delta': 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   278
  assumes fS: "finite S" shows 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   279
  "setsum (\<lambda>k. if a = k then b k else 0) S = 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   280
     (if a\<in> S then b a else 0)"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   281
  using setsum_delta[OF fS, of a b, symmetric] 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   282
  by (auto intro: setsum_cong)
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   283
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   284
lemma setsum_restrict_set:
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   285
  assumes fA: "finite A"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   286
  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   287
proof-
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   288
  from fA have fab: "finite (A \<inter> B)" by auto
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   289
  have aba: "A \<inter> B \<subseteq> A" by blast
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   290
  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   291
  from setsum_mono_zero_left[OF fA aba, of ?g]
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   292
  show ?thesis by simp
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   293
qed
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   294
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   295
lemma setsum_cases:
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   296
  assumes fA: "finite A"
35577
43b93e294522 Generalized setsum_cases
hoelzl
parents: 35416
diff changeset
   297
  shows "setsum (\<lambda>x. if P x then f x else g x) A =
43b93e294522 Generalized setsum_cases
hoelzl
parents: 35416
diff changeset
   298
         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
42986
11fd8c04ea24 generalize setsum_cases
hoelzl
parents: 42871
diff changeset
   299
  using setsum.If_cases[OF fA] .
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   300
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   301
(*But we can't get rid of finite I. If infinite, although the rhs is 0, 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   302
  the lhs need not be, since UNION I A could still be finite.*)
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   303
lemma (in comm_monoid_add) setsum_UN_disjoint:
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   304
  assumes "finite I" and "ALL i:I. finite (A i)"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   305
    and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   306
  shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   307
proof -
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   308
  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   309
  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   310
qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   311
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   312
text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   313
directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   314
lemma setsum_Union_disjoint:
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   315
  "[| (ALL A:C. finite A);
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   316
      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   317
   ==> setsum f (Union C) = setsum (setsum f) C"
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   318
apply (cases "finite C") 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   319
 prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   320
  apply (frule setsum_UN_disjoint [of C id f])
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   321
 apply (unfold Union_def id_def, assumption+)
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   322
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   323
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   324
(*But we can't get rid of finite A. If infinite, although the lhs is 0, 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   325
  the rhs need not be, since SIGMA A B could still be finite.*)
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   326
lemma (in comm_monoid_add) setsum_Sigma:
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   327
  assumes "finite A" and  "ALL x:A. finite (B x)"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   328
  shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   329
proof -
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   330
  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   331
  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   332
qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   333
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   334
text{*Here we can eliminate the finiteness assumptions, by cases.*}
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   335
lemma setsum_cartesian_product: 
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   336
   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   337
apply (cases "finite A") 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   338
 apply (cases "finite B") 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   339
  apply (simp add: setsum_Sigma)
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   340
 apply (cases "A={}", simp)
15543
0024472afce7 more setsum tuning
nipkow
parents: 15542
diff changeset
   341
 apply (simp) 
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   342
apply (auto simp add: setsum_def
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   343
            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   344
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   345
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   346
lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   347
  by (cases "finite A") (simp_all add: setsum.distrib)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   348
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   349
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   350
subsubsection {* Properties in more restricted classes of structures *}
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   351
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   352
lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   353
apply (case_tac "finite A")
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   354
 prefer 2 apply (simp add: setsum_def)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   355
apply (erule rev_mp)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   356
apply (erule finite_induct, auto)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   357
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   358
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   359
lemma setsum_eq_0_iff [simp]:
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   360
    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   361
by (induct set: finite) auto
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   362
30859
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   363
lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   364
  (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   365
apply(erule finite_induct)
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   366
apply (auto simp add:add_is_1)
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   367
done
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   368
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   369
lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
29eb80cef6b7 added setsum_eq_1_iff
nipkow
parents: 30844
diff changeset
   370
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   371
lemma setsum_Un_nat: "finite A ==> finite B ==>
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   372
  (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   373
  -- {* For the natural numbers, we have subtraction. *}
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29509
diff changeset
   374
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   375
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   376
lemma setsum_Un: "finite A ==> finite B ==>
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   377
  (setsum f (A Un B) :: 'a :: ab_group_add) =
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   378
   setsum f A + setsum f B - setsum f (A Int B)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29509
diff changeset
   379
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   380
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   381
lemma (in comm_monoid_add) setsum_eq_general_reverses:
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   382
  assumes fS: "finite S" and fT: "finite T"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   383
  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   384
  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   385
  shows "setsum f S = setsum g T"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   386
proof -
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   387
  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   388
  show ?thesis
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   389
  apply (simp add: setsum_def fS fT)
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   390
  apply (rule fold_image_eq_general_inverses)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   391
  apply (rule fS)
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   392
  apply (erule kh)
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   393
  apply (erule hk)
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   394
  done
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   395
qed
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   396
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   397
lemma (in comm_monoid_add) setsum_Un_zero:  
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   398
  assumes fS: "finite S" and fT: "finite T"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   399
  and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   400
  shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   401
proof -
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   402
  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   403
  show ?thesis
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   404
  using fS fT
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   405
  apply (simp add: setsum_def)
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   406
  apply (rule fold_image_Un_one)
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   407
  using I0 by auto
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   408
qed
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   409
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   410
lemma setsum_UNION_zero: 
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   411
  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   412
  and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   413
  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   414
  using fSS f0
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   415
proof(induct rule: finite_induct[OF fS])
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   416
  case 1 thus ?case by simp
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   417
next
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   418
  case (2 T F)
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   419
  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35171
diff changeset
   420
    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35171
diff changeset
   421
  from fTF have fUF: "finite (\<Union>F)" by auto
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   422
  from "2.prems" TF fTF
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   423
  show ?case 
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   424
    by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   425
qed
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   426
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   427
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   428
  (if a:A then setsum f A - f a else setsum f A)"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   429
apply (case_tac "finite A")
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   430
 prefer 2 apply (simp add: setsum_def)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   431
apply (erule finite_induct)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   432
 apply (auto simp add: insert_Diff_if)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   433
apply (drule_tac a = a in mk_disjoint_insert, auto)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   434
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   435
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   436
lemma setsum_diff1: "finite A \<Longrightarrow>
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   437
  (setsum f (A - {a}) :: ('a::ab_group_add)) =
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   438
  (if a:A then setsum f A - f a else setsum f A)"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   439
by (erule finite_induct) (auto simp add: insert_Diff_if)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   440
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   441
lemma setsum_diff1'[rule_format]:
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   442
  "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   443
apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   444
apply (auto simp add: insert_Diff_if add_ac)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   445
done
15552
8ab8e425410b added setsum_diff1' which holds in more general cases than setsum_diff1
obua
parents: 15543
diff changeset
   446
31438
a1c4c1500abe A few finite lemmas
nipkow
parents: 31380
diff changeset
   447
lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
a1c4c1500abe A few finite lemmas
nipkow
parents: 31380
diff changeset
   448
  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
a1c4c1500abe A few finite lemmas
nipkow
parents: 31380
diff changeset
   449
unfolding setsum_diff1'[OF assms] by auto
a1c4c1500abe A few finite lemmas
nipkow
parents: 31380
diff changeset
   450
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   451
(* By Jeremy Siek: *)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   452
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   453
lemma setsum_diff_nat: 
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   454
assumes "finite B" and "B \<subseteq> A"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   455
shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   456
using assms
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   457
proof induct
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   458
  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   459
next
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   460
  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   461
    and xFinA: "insert x F \<subseteq> A"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   462
    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   463
  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   464
  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   465
    by (simp add: setsum_diff1_nat)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   466
  from xFinA have "F \<subseteq> A" by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   467
  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   468
  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   469
    by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   470
  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   471
  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   472
    by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   473
  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   474
  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   475
    by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   476
  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   477
qed
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   478
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   479
lemma setsum_diff:
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   480
  assumes le: "finite A" "B \<subseteq> A"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   481
  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   482
proof -
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   483
  from le have finiteB: "finite B" using finite_subset by auto
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   484
  show ?thesis using finiteB le
21575
89463ae2612d tuned proofs;
wenzelm
parents: 21409
diff changeset
   485
  proof induct
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   486
    case empty
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   487
    thus ?case by auto
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   488
  next
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   489
    case (insert x F)
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   490
    thus ?case using le finiteB 
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   491
      by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   492
  qed
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   493
qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   494
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   495
lemma setsum_mono:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   496
  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   497
  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   498
proof (cases "finite K")
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   499
  case True
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   500
  thus ?thesis using le
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   501
  proof induct
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   502
    case empty
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   503
    thus ?case by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   504
  next
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   505
    case insert
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   506
    thus ?case using add_mono by fastsimp
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   507
  qed
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   508
next
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   509
  case False
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   510
  thus ?thesis
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   511
    by (simp add: setsum_def)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   512
qed
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   513
15554
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   514
lemma setsum_strict_mono:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   515
  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   516
  assumes "finite A"  "A \<noteq> {}"
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   517
    and "!!x. x:A \<Longrightarrow> f x < g x"
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   518
  shows "setsum f A < setsum g A"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   519
  using assms
15554
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   520
proof (induct rule: finite_ne_induct)
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   521
  case singleton thus ?case by simp
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   522
next
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   523
  case insert thus ?case by (auto simp: add_strict_mono)
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   524
qed
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15552
diff changeset
   525
15535
nipkow
parents: 15532
diff changeset
   526
lemma setsum_negf:
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   527
  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
15535
nipkow
parents: 15532
diff changeset
   528
proof (cases "finite A")
22262
96ba62dff413 Adapted to new inductive definition package.
berghofe
parents: 21733
diff changeset
   529
  case True thus ?thesis by (induct set: finite) auto
15535
nipkow
parents: 15532
diff changeset
   530
next
nipkow
parents: 15532
diff changeset
   531
  case False thus ?thesis by (simp add: setsum_def)
nipkow
parents: 15532
diff changeset
   532
qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   533
15535
nipkow
parents: 15532
diff changeset
   534
lemma setsum_subtractf:
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   535
  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   536
    setsum f A - setsum g A"
15535
nipkow
parents: 15532
diff changeset
   537
proof (cases "finite A")
nipkow
parents: 15532
diff changeset
   538
  case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
nipkow
parents: 15532
diff changeset
   539
next
nipkow
parents: 15532
diff changeset
   540
  case False thus ?thesis by (simp add: setsum_def)
nipkow
parents: 15532
diff changeset
   541
qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   542
15535
nipkow
parents: 15532
diff changeset
   543
lemma setsum_nonneg:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   544
  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   545
  shows "0 \<le> setsum f A"
15535
nipkow
parents: 15532
diff changeset
   546
proof (cases "finite A")
nipkow
parents: 15532
diff changeset
   547
  case True thus ?thesis using nn
21575
89463ae2612d tuned proofs;
wenzelm
parents: 21409
diff changeset
   548
  proof induct
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   549
    case empty then show ?case by simp
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   550
  next
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   551
    case (insert x F)
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   552
    then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   553
    with insert show ?case by simp
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   554
  qed
15535
nipkow
parents: 15532
diff changeset
   555
next
nipkow
parents: 15532
diff changeset
   556
  case False thus ?thesis by (simp add: setsum_def)
nipkow
parents: 15532
diff changeset
   557
qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   558
15535
nipkow
parents: 15532
diff changeset
   559
lemma setsum_nonpos:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   560
  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   561
  shows "setsum f A \<le> 0"
15535
nipkow
parents: 15532
diff changeset
   562
proof (cases "finite A")
nipkow
parents: 15532
diff changeset
   563
  case True thus ?thesis using np
21575
89463ae2612d tuned proofs;
wenzelm
parents: 21409
diff changeset
   564
  proof induct
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   565
    case empty then show ?case by simp
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   566
  next
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   567
    case (insert x F)
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   568
    then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   569
    with insert show ?case by simp
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   570
  qed
15535
nipkow
parents: 15532
diff changeset
   571
next
nipkow
parents: 15532
diff changeset
   572
  case False thus ?thesis by (simp add: setsum_def)
nipkow
parents: 15532
diff changeset
   573
qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   574
36622
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   575
lemma setsum_nonneg_leq_bound:
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   576
  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   577
  assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   578
  shows "f i \<le> B"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   579
proof -
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   580
  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   581
    using assms by (auto intro!: setsum_nonneg)
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   582
  moreover
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   583
  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   584
    using assms by (simp add: setsum_diff1)
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   585
  ultimately show ?thesis by auto
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   586
qed
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   587
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   588
lemma setsum_nonneg_0:
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   589
  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   590
  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   591
  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   592
  shows "f i = 0"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   593
  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36409
diff changeset
   594
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   595
lemma setsum_mono2:
36303
80e3f43306cf sharpened constraint (c.f. 4e7f5b22dd7d)
haftmann
parents: 36079
diff changeset
   596
fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   597
assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   598
shows "setsum f A \<le> setsum f B"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   599
proof -
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   600
  have "setsum f A \<le> setsum f A + setsum f (B-A)"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   601
    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   602
  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   603
    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   604
  also have "A \<union> (B-A) = B" using sub by blast
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   605
  finally show ?thesis .
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   606
qed
15542
ee6cd48cf840 more fine tuniung
nipkow
parents: 15539
diff changeset
   607
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   608
lemma setsum_mono3: "finite B ==> A <= B ==> 
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   609
    ALL x: B - A. 
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   610
      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   611
        setsum f A <= setsum f B"
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   612
  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   613
  apply (erule ssubst)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   614
  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   615
  apply simp
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   616
  apply (rule add_left_mono)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   617
  apply (erule setsum_nonneg)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   618
  apply (subst setsum_Un_disjoint [THEN sym])
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   619
  apply (erule finite_subset, assumption)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   620
  apply (rule finite_subset)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   621
  prefer 2
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   622
  apply assumption
32698
be4b248616c0 inf/sup_absorb are no default simp rules any longer
haftmann
parents: 32697
diff changeset
   623
  apply (auto simp add: sup_absorb2)
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   624
done
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   625
19279
48b527d0331b Renamed setsum_mult to setsum_right_distrib.
ballarin
parents: 18493
diff changeset
   626
lemma setsum_right_distrib: 
22934
64ecb3d6790a generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents: 22917
diff changeset
   627
  fixes f :: "'a => ('b::semiring_0)"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   628
  shows "r * setsum f A = setsum (%n. r * f n) A"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   629
proof (cases "finite A")
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   630
  case True
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   631
  thus ?thesis
21575
89463ae2612d tuned proofs;
wenzelm
parents: 21409
diff changeset
   632
  proof induct
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   633
    case empty thus ?case by simp
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   634
  next
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   635
    case (insert x A) thus ?case by (simp add: right_distrib)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   636
  qed
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   637
next
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   638
  case False thus ?thesis by (simp add: setsum_def)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   639
qed
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   640
17149
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   641
lemma setsum_left_distrib:
22934
64ecb3d6790a generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents: 22917
diff changeset
   642
  "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
17149
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   643
proof (cases "finite A")
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   644
  case True
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   645
  then show ?thesis
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   646
  proof induct
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   647
    case empty thus ?case by simp
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   648
  next
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   649
    case (insert x A) thus ?case by (simp add: left_distrib)
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   650
  qed
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   651
next
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   652
  case False thus ?thesis by (simp add: setsum_def)
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   653
qed
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   654
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   655
lemma setsum_divide_distrib:
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   656
  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   657
proof (cases "finite A")
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   658
  case True
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   659
  then show ?thesis
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   660
  proof induct
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   661
    case empty thus ?case by simp
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   662
  next
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   663
    case (insert x A) thus ?case by (simp add: add_divide_distrib)
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   664
  qed
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   665
next
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   666
  case False thus ?thesis by (simp add: setsum_def)
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   667
qed
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   668
15535
nipkow
parents: 15532
diff changeset
   669
lemma setsum_abs[iff]: 
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   670
  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   671
  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
15535
nipkow
parents: 15532
diff changeset
   672
proof (cases "finite A")
nipkow
parents: 15532
diff changeset
   673
  case True
nipkow
parents: 15532
diff changeset
   674
  thus ?thesis
21575
89463ae2612d tuned proofs;
wenzelm
parents: 21409
diff changeset
   675
  proof induct
15535
nipkow
parents: 15532
diff changeset
   676
    case empty thus ?case by simp
nipkow
parents: 15532
diff changeset
   677
  next
nipkow
parents: 15532
diff changeset
   678
    case (insert x A)
nipkow
parents: 15532
diff changeset
   679
    thus ?case by (auto intro: abs_triangle_ineq order_trans)
nipkow
parents: 15532
diff changeset
   680
  qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   681
next
15535
nipkow
parents: 15532
diff changeset
   682
  case False thus ?thesis by (simp add: setsum_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   683
qed
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   684
15535
nipkow
parents: 15532
diff changeset
   685
lemma setsum_abs_ge_zero[iff]: 
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   686
  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   687
  shows "0 \<le> setsum (%i. abs(f i)) A"
15535
nipkow
parents: 15532
diff changeset
   688
proof (cases "finite A")
nipkow
parents: 15532
diff changeset
   689
  case True
nipkow
parents: 15532
diff changeset
   690
  thus ?thesis
21575
89463ae2612d tuned proofs;
wenzelm
parents: 21409
diff changeset
   691
  proof induct
15535
nipkow
parents: 15532
diff changeset
   692
    case empty thus ?case by simp
nipkow
parents: 15532
diff changeset
   693
  next
36977
71c8973a604b declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
huffman
parents: 36635
diff changeset
   694
    case (insert x A) thus ?case by auto
15535
nipkow
parents: 15532
diff changeset
   695
  qed
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   696
next
15535
nipkow
parents: 15532
diff changeset
   697
  case False thus ?thesis by (simp add: setsum_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   698
qed
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   699
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   700
lemma abs_setsum_abs[simp]: 
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
   701
  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   702
  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   703
proof (cases "finite A")
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   704
  case True
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   705
  thus ?thesis
21575
89463ae2612d tuned proofs;
wenzelm
parents: 21409
diff changeset
   706
  proof induct
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   707
    case empty thus ?case by simp
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   708
  next
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   709
    case (insert a A)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   710
    hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   711
    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   712
    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16760
diff changeset
   713
      by (simp del: abs_of_nonneg)
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   714
    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   715
    finally show ?case .
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   716
  qed
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   717
next
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   718
  case False thus ?thesis by (simp add: setsum_def)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   719
qed
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15535
diff changeset
   720
31080
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   721
lemma setsum_Plus:
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   722
  fixes A :: "'a set" and B :: "'b set"
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   723
  assumes fin: "finite A" "finite B"
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   724
  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   725
proof -
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   726
  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   727
  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 39302
diff changeset
   728
    by auto
31080
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   729
  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   730
  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   731
  ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   732
qed
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   733
21ffc770ebc0 lemmas by Andreas Lochbihler
nipkow
parents: 31017
diff changeset
   734
17149
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   735
text {* Commuting outer and inner summation *}
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   736
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   737
lemma setsum_commute:
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   738
  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   739
proof (simp add: setsum_cartesian_product)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   740
  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   741
    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
17149
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   742
    (is "?s = _")
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   743
    apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   744
    apply (simp add: split_def)
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   745
    done
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   746
  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
17149
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   747
    (is "_ = ?t")
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   748
    apply (simp add: swap_product)
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   749
    done
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   750
  finally show "?s = ?t" .
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   751
qed
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   752
19279
48b527d0331b Renamed setsum_mult to setsum_right_distrib.
ballarin
parents: 18493
diff changeset
   753
lemma setsum_product:
22934
64ecb3d6790a generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents: 22917
diff changeset
   754
  fixes f :: "'a => ('b::semiring_0)"
19279
48b527d0331b Renamed setsum_mult to setsum_right_distrib.
ballarin
parents: 18493
diff changeset
   755
  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
48b527d0331b Renamed setsum_mult to setsum_right_distrib.
ballarin
parents: 18493
diff changeset
   756
  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
48b527d0331b Renamed setsum_mult to setsum_right_distrib.
ballarin
parents: 18493
diff changeset
   757
34223
dce32a1e05fe added lemmas
nipkow
parents: 34114
diff changeset
   758
lemma setsum_mult_setsum_if_inj:
dce32a1e05fe added lemmas
nipkow
parents: 34114
diff changeset
   759
fixes f :: "'a => ('b::semiring_0)"
dce32a1e05fe added lemmas
nipkow
parents: 34114
diff changeset
   760
shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
dce32a1e05fe added lemmas
nipkow
parents: 34114
diff changeset
   761
  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
dce32a1e05fe added lemmas
nipkow
parents: 34114
diff changeset
   762
by(auto simp: setsum_product setsum_cartesian_product
dce32a1e05fe added lemmas
nipkow
parents: 34114
diff changeset
   763
        intro!:  setsum_reindex_cong[symmetric])
dce32a1e05fe added lemmas
nipkow
parents: 34114
diff changeset
   764
35722
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   765
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   766
apply (cases "finite A")
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   767
apply (erule finite_induct)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   768
apply (auto simp add: algebra_simps)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   769
done
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   770
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   771
lemma setsum_bounded:
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   772
  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   773
  shows "setsum f A \<le> of_nat(card A) * K"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   774
proof (cases "finite A")
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   775
  case True
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   776
  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   777
next
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   778
  case False thus ?thesis by (simp add: setsum_def)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   779
qed
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   780
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   781
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   782
subsubsection {* Cardinality as special case of @{const setsum} *}
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   783
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   784
lemma card_eq_setsum:
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   785
  "card A = setsum (\<lambda>x. 1) A"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   786
  by (simp only: card_def setsum_def)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   787
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   788
lemma card_UN_disjoint:
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   789
  "finite I ==> (ALL i:I. finite (A i)) ==>
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   790
   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   791
   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   792
apply (simp add: card_eq_setsum del: setsum_constant)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   793
apply (subgoal_tac
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   794
         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   795
apply (simp add: setsum_UN_disjoint del: setsum_constant)
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   796
apply simp
35722
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   797
done
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   798
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   799
lemma card_Union_disjoint:
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   800
  "finite C ==> (ALL A:C. finite A) ==>
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   801
   (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   802
   ==> card (Union C) = setsum card C"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   803
apply (frule card_UN_disjoint [of C id])
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   804
apply (unfold Union_def id_def, assumption+)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   805
done
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   806
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   807
text{*The image of a finite set can be expressed using @{term fold_image}.*}
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   808
lemma image_eq_fold_image:
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   809
  "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   810
proof (induct rule: finite_induct)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   811
  case empty then show ?case by simp
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   812
next
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   813
  interpret ab_semigroup_mult "op Un"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   814
    proof qed auto
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   815
  case insert 
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   816
  then show ?case by simp
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   817
qed
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   818
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   819
subsubsection {* Cardinality of products *}
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   820
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   821
lemma card_SigmaI [simp]:
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   822
  "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   823
  \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   824
by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   825
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   826
(*
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   827
lemma SigmaI_insert: "y \<notin> A ==>
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   828
  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   829
  by auto
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   830
*)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   831
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   832
lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   833
  by (cases "finite A \<and> finite B")
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   834
    (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   835
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   836
lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   837
by (simp add: card_cartesian_product)
69419a09a7ff moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents: 35719
diff changeset
   838
17149
e2b19c92ef51 Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents: 17085
diff changeset
   839
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   840
subsection {* Generalized product over a set *}
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   841
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   842
definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   843
  "setprod f A = (if finite A then fold_image (op *) f 1 A else 1)"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   844
35938
93faaa15c3d5 sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
huffman
parents: 35831
diff changeset
   845
sublocale comm_monoid_mult < setprod!: comm_monoid_big "op *" 1 setprod proof
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   846
qed (fact setprod_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   847
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   848
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21249
diff changeset
   849
  Setprod  ("\<Prod>_" [1000] 999) where
19535
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   850
  "\<Prod>A == setprod (%x. x) A"
e4fdeb32eadf replaced syntax/translations by abbreviation;
wenzelm
parents: 19363
diff changeset
   851
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   852
syntax
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   853
  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   854
syntax (xsymbols)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   855
  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   856
syntax (HTML output)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   857
  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
16550
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   858
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   859
translations -- {* Beware of argument permutation! *}
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   860
  "PROD i:A. b" == "CONST setprod (%i. b) A" 
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   861
  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
16550
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   862
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   863
text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   864
 @{text"\<Prod>x|P. e"}. *}
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   865
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   866
syntax
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   867
  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
16550
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   868
syntax (xsymbols)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   869
  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
16550
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   870
syntax (HTML output)
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
   871
  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
16550
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   872
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   873
translations
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   874
  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   875
  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
16550
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
   876
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   877
lemma setprod_empty: "setprod f {} = 1"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   878
  by (fact setprod.empty)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   879
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   880
lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   881
    setprod f (insert a A) = f a * setprod f A"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   882
  by (fact setprod.insert)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   883
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   884
lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
   885
  by (fact setprod.infinite)
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   886
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   887
lemma setprod_reindex:
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   888
   "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   889
by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   890
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   891
lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   892
by (auto simp add: setprod_reindex)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   893
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   894
lemma setprod_cong:
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   895
  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   896
by(fastsimp simp: setprod_def intro: fold_image_cong)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   897
30837
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   898
lemma strong_setprod_cong[cong]:
16632
ad2895beef79 Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents: 16550
diff changeset
   899
  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   900
by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
16632
ad2895beef79 Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents: 16550
diff changeset
   901
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   902
lemma setprod_reindex_cong: "inj_on f A ==>
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   903
    B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   904
by (frule setprod_reindex, simp)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   905
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   906
lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   907
  and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   908
  shows "setprod h B = setprod g A"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   909
proof-
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   910
    have "setprod h B = setprod (h o f) A"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   911
      by (simp add: B setprod_reindex[OF i, of h])
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   912
    then show ?thesis apply simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   913
      apply (rule setprod_cong)
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   914
      apply simp
30837
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   915
      by (simp add: eq)
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   916
qed
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   917
30260
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   918
lemma setprod_Un_one:  
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   919
  assumes fS: "finite S" and fT: "finite T"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   920
  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   921
  shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   922
  using fS fT
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   923
  apply (simp add: setprod_def)
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   924
  apply (rule fold_image_Un_one)
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   925
  using I0 by auto
be39acd3ac85 Added general theorems for fold_image, setsum and set_prod
chaieb
parents: 29966
diff changeset
   926
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   927
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   928
lemma setprod_1: "setprod (%i. 1) A = 1"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   929
apply (case_tac "finite A")
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   930
apply (erule finite_induct, auto simp add: mult_ac)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   931
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   932
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   933
lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   934
apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   935
apply (erule ssubst, rule setprod_1)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   936
apply (rule setprod_cong, auto)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   937
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   938
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   939
lemma setprod_Un_Int: "finite A ==> finite B
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   940
    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
   941
by(simp add: setprod_def fold_image_Un_Int[symmetric])
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   942
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   943
lemma setprod_Un_disjoint: "finite A ==> finite B
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   944
  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   945
by (subst setprod_Un_Int [symmetric], auto)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   946
30837
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   947
lemma setprod_mono_one_left: 
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   948
  assumes fT: "finite T" and ST: "S \<subseteq> T"
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   949
  and z: "\<forall>i \<in> T - S. f i = 1"
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   950
  shows "setprod f S = setprod f T"
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   951
proof-
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   952
  have eq: "T = S \<union> (T - S)" using ST by blast
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   953
  have d: "S \<inter> (T - S) = {}" using ST by blast
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   954
  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   955
  show ?thesis
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   956
  by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   957
qed
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   958
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   959
lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30729
diff changeset
   960
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   961
lemma setprod_delta: 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   962
  assumes fS: "finite S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   963
  shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   964
proof-
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   965
  let ?f = "(\<lambda>k. if k=a then b k else 1)"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   966
  {assume a: "a \<notin> S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   967
    hence "\<forall> k\<in> S. ?f k = 1" by simp
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   968
    hence ?thesis  using a by (simp add: setprod_1) }
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   969
  moreover 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   970
  {assume a: "a \<in> S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   971
    let ?A = "S - {a}"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   972
    let ?B = "{a}"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   973
    have eq: "S = ?A \<union> ?B" using a by blast 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   974
    have dj: "?A \<inter> ?B = {}" by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   975
    from fS have fAB: "finite ?A" "finite ?B" by auto  
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   976
    have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   977
    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   978
      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   979
      by simp
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   980
    then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   981
  ultimately show ?thesis by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   982
qed
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   983
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   984
lemma setprod_delta': 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   985
  assumes fS: "finite S" shows 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   986
  "setprod (\<lambda>k. if a = k then b k else 1) S = 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   987
     (if a\<in> S then b a else 1)"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   988
  using setprod_delta[OF fS, of a b, symmetric] 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   989
  by (auto intro: setprod_cong)
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   990
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
   991
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   992
lemma setprod_UN_disjoint:
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   993
    "finite I ==> (ALL i:I. finite (A i)) ==>
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   994
        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   995
      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   996
  by (simp add: setprod_def fold_image_UN_disjoint)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   997
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   998
lemma setprod_Union_disjoint:
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
   999
  "[| (ALL A:C. finite A);
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1000
      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1001
   ==> setprod f (Union C) = setprod (setprod f) C"
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1002
apply (cases "finite C") 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1003
 prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1004
  apply (frule setprod_UN_disjoint [of C id f])
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1005
 apply (unfold Union_def id_def, assumption+)
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1006
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1007
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1008
lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
16550
e14b89d6ef13 fixed \<Prod> syntax
nipkow
parents: 15837
diff changeset
  1009
    (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
  1010
    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 40786
diff changeset
  1011
by(simp add:setprod_def fold_image_Sigma split_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1012
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1013
text{*Here we can eliminate the finiteness assumptions, by cases.*}
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1014
lemma setprod_cartesian_product: 
17189
b15f8e094874 patterns in setsum and setprod
paulson
parents: 17149
diff changeset
  1015
     "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1016
apply (cases "finite A") 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1017
 apply (cases "finite B") 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1018
  apply (simp add: setprod_Sigma)
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1019
 apply (cases "A={}", simp)
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1020
 apply (simp add: setprod_1) 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1021
apply (auto simp add: setprod_def
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1022
            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1023
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1024
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1025
lemma setprod_timesf:
15409
a063687d24eb new and stronger lemmas and improved simplification for finite sets
paulson
parents: 15402
diff changeset
  1026
     "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1027
by(simp add:setprod_def fold_image_distrib)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1028
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1029
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1030
subsubsection {* Properties in more restricted classes of structures *}
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1031
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1032
lemma setprod_eq_1_iff [simp]:
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1033
  "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1034
by (induct set: finite) auto
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1035
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1036
lemma setprod_zero:
23277
aa158e145ea3 generalize class constraints on some lemmas
huffman
parents: 23234
diff changeset
  1037
     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1038
apply (induct set: finite, force, clarsimp)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1039
apply (erule disjE, auto)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1040
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1041
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1042
lemma setprod_nonneg [rule_format]:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
  1043
   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
30841
0813afc97522 generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
huffman
parents: 30729
diff changeset
  1044
by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
0813afc97522 generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
huffman
parents: 30729
diff changeset
  1045
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
  1046
lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1047
  --> 0 < setprod f A"
30841
0813afc97522 generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
huffman
parents: 30729
diff changeset
  1048
by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1049
30843
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1050
lemma setprod_zero_iff[simp]: "finite A ==> 
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1051
  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1052
  (EX x: A. f x = 0)"
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1053
by (erule finite_induct, auto simp:no_zero_divisors)
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1054
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1055
lemma setprod_pos_nat:
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1056
  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1057
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1058
30863
5dc392a59bb7 Finite_Set: lemma
nipkow
parents: 30859
diff changeset
  1059
lemma setprod_pos_nat_iff[simp]:
5dc392a59bb7 Finite_Set: lemma
nipkow
parents: 30859
diff changeset
  1060
  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
5dc392a59bb7 Finite_Set: lemma
nipkow
parents: 30859
diff changeset
  1061
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
5dc392a59bb7 Finite_Set: lemma
nipkow
parents: 30859
diff changeset
  1062
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1063
lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1064
  (setprod f (A Un B) :: 'a ::{field})
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1065
   = setprod f A * setprod f B / setprod f (A Int B)"
30843
3419ca741dbf cleaned up setprod_zero-related lemmas
nipkow
parents: 30837
diff changeset
  1066
by (subst setprod_Un_Int [symmetric], auto)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1067
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1068
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1069
  (setprod f (A - {a}) :: 'a :: {field}) =
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1070
  (if a:A then setprod f A / f a else setprod f A)"
36303
80e3f43306cf sharpened constraint (c.f. 4e7f5b22dd7d)
haftmann
parents: 36079
diff changeset
  1071
  by (erule finite_induct) (auto simp add: insert_Diff_if)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1072
31906
b41d61c768e2 Removed unnecessary conditions concerning nonzero divisors
paulson
parents: 31465
diff changeset
  1073
lemma setprod_inversef: 
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36349
diff changeset
  1074
  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
31906
b41d61c768e2 Removed unnecessary conditions concerning nonzero divisors
paulson
parents: 31465
diff changeset
  1075
  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1076
by (erule finite_induct) auto
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1077
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1078
lemma setprod_dividef:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36349
diff changeset
  1079
  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
31916
f3227bb306a4 recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
wenzelm
parents: 31907
diff changeset
  1080
  shows "finite A
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1081
    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1082
apply (subgoal_tac
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1083
         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1084
apply (erule ssubst)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1085
apply (subst divide_inverse)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1086
apply (subst setprod_timesf)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1087
apply (subst setprod_inversef, assumption+, rule refl)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1088
apply (rule setprod_cong, rule refl)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1089
apply (subst divide_inverse, auto)
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1090
done
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1091
29925
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1092
lemma setprod_dvd_setprod [rule_format]: 
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1093
    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1094
  apply (cases "finite A")
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1095
  apply (induct set: finite)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1096
  apply (auto simp add: dvd_def)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1097
  apply (rule_tac x = "k * ka" in exI)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1098
  apply (simp add: algebra_simps)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1099
done
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1100
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1101
lemma setprod_dvd_setprod_subset:
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1102
  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1103
  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1104
  apply (unfold dvd_def, blast)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1105
  apply (subst setprod_Un_disjoint [symmetric])
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1106
  apply (auto elim: finite_subset intro: setprod_cong)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1107
done
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1108
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1109
lemma setprod_dvd_setprod_subset2:
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1110
  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1111
      setprod f A dvd setprod g B"
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1112
  apply (rule dvd_trans)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1113
  apply (rule setprod_dvd_setprod, erule (1) bspec)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1114
  apply (erule (1) setprod_dvd_setprod_subset)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1115
done
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1116
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1117
lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1118
    (f i ::'a::comm_semiring_1) dvd setprod f A"
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1119
by (induct set: finite) (auto intro: dvd_mult)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1120
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1121
lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1122
    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1123
  apply (cases "finite A")
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1124
  apply (induct set: finite)
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1125
  apply auto
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1126
done
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29923
diff changeset
  1127
35171
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1128
lemma setprod_mono:
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1129
  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1130
  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1131
  shows "setprod f A \<le> setprod g A"
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1132
proof (cases "finite A")
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1133
  case True
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1134
  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1135
  proof (induct A rule: finite_subset_induct)
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1136
    case (insert a F)
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1137
    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1138
      unfolding setprod_insert[OF insert(1,3)]
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1139
      using assms[rule_format,OF insert(2)] insert
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1140
      by (auto intro: mult_mono mult_nonneg_nonneg)
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1141
  qed auto
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1142
  thus ?thesis by simp
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1143
qed auto
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1144
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1145
lemma abs_setprod:
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1146
  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1147
  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1148
proof (cases "finite A")
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1149
  case True thus ?thesis
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35171
diff changeset
  1150
    by induct (auto simp add: field_simps abs_mult)
35171
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1151
qed auto
28f824c7addc Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents: 35115
diff changeset
  1152
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30863
diff changeset
  1153
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1154
apply (erule finite_induct)
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35171
diff changeset
  1155
apply auto
28853
69eb69659bf3 Added new fold operator and renamed the old oe to fold_image.
nipkow
parents: 28823
diff changeset
  1156
done
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
  1157
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1158
lemma setprod_gen_delta:
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1159
  assumes fS: "finite S"
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30863
diff changeset
  1160
  shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)"
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1161
proof-
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1162
  let ?f = "(\<lambda>k. if k=a then b k else c)"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1163
  {assume a: "a \<notin> S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1164
    hence "\<forall> k\<in> S. ?f k = c" by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1165
    hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1166
  moreover 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1167
  {assume a: "a \<in> S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1168
    let ?A = "S - {a}"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1169
    let ?B = "{a}"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1170
    have eq: "S = ?A \<union> ?B" using a by blast 
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1171
    have dj: "?A \<inter> ?B = {}" by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1172
    from fS have fAB: "finite ?A" "finite ?B" by auto  
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1173
    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1174
      apply (rule setprod_cong) by auto
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1175
    have cA: "card ?A = card S - 1" using fS a by auto
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1176
    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1177
    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1178
      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1179
      by simp
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1180
    then have ?thesis using a cA
36349
39be26d1bc28 class division_ring_inverse_zero
haftmann
parents: 36303
diff changeset
  1181
      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
29674
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1182
  ultimately show ?thesis by blast
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1183
qed
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1184
3857d7eba390 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents: 29609
diff changeset
  1185
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1186
subsection {* Versions of @{const inf} and @{const sup} on non-empty sets *}
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1187
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1188
no_notation times (infixl "*" 70)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1189
no_notation Groups.one ("1")
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1190
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1191
locale semilattice_big = semilattice +
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1192
  fixes F :: "'a set \<Rightarrow> 'a"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1193
  assumes F_eq: "finite A \<Longrightarrow> F A = fold1 (op *) A"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1194
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1195
sublocale semilattice_big < folding_one_idem proof
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1196
qed (simp_all add: F_eq)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1197
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1198
notation times (infixl "*" 70)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1199
notation Groups.one ("1")
22917
3c56b12fd946 localized Min/Max
haftmann
parents: 22616
diff changeset
  1200
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1201
context lattice
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1202
begin
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1203
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1204
definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) where
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1205
  "Inf_fin = fold1 inf"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1206
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1207
definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) where
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1208
  "Sup_fin = fold1 sup"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1209
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1210
end
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1211
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1212
sublocale lattice < Inf_fin!: semilattice_big inf Inf_fin proof
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1213
qed (simp add: Inf_fin_def)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1214
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1215
sublocale lattice < Sup_fin!: semilattice_big sup Sup_fin proof
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1216
qed (simp add: Sup_fin_def)
22917
3c56b12fd946 localized Min/Max
haftmann
parents: 22616
diff changeset
  1217
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34223
diff changeset
  1218
context semilattice_inf
26041
c2e15e65165f locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents: 25571
diff changeset
  1219
begin
c2e15e65165f locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents: 25571
diff changeset
  1220
36635
080b755377c0 locale predicates of classes carry a mandatory "class" prefix
haftmann
parents: 36622
diff changeset
  1221
lemma ab_semigroup_idem_mult_inf:
080b755377c0 locale predicates of classes carry a mandatory "class" prefix
haftmann
parents: 36622
diff changeset
  1222
  "class.ab_semigroup_idem_mult inf"
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1223
proof qed (rule inf_assoc inf_commute inf_idem)+
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1224
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1225
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
42871
1c0b99f950d9 names of fold_set locales resemble name of characteristic property more closely
haftmann
parents: 42284
diff changeset
  1226
by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]])
35816
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1227
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1228
lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1229
by (induct pred: finite) (auto intro: le_infI1)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1230
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1231
lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1232
proof(induct arbitrary: a pred:finite)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1233
  case empty thus ?case by simp
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1234
next
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1235
  case (insert x A)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1236
  show ?case
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1237
  proof cases
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1238
    assume "A = {}" thus ?thesis using insert by simp
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1239
  next
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1240
    assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1241
  qed
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1242
qed
2449e026483d generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents: 35722
diff changeset
  1243
26041
c2e15e65165f locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents: 25571
diff changeset
  1244
lemma below_fold1_iff: