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