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