src/HOL/NumberTheory/Finite2.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14485 ea2707645af8
child 15047 fa62de5862b9
permissions -rw-r--r--
Merged in license change from Isabelle2004
paulson@13871
     1
(*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
kleing@14981
     2
    ID:         $Id$
paulson@13871
     3
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
paulson@13871
     4
*)
paulson@13871
     5
paulson@13871
     6
header {*Finite Sets and Finite Sums*}
paulson@13871
     7
paulson@13871
     8
theory Finite2 = Main + IntFact:;
paulson@13871
     9
paulson@13871
    10
text{*These are useful for combinatorial and number-theoretic counting
paulson@13871
    11
arguments.*}
paulson@13871
    12
paulson@13871
    13
text{*Note.  This theory is being revised.  See the web page
paulson@13871
    14
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
paulson@13871
    15
paulson@13871
    16
(******************************************************************)
paulson@13871
    17
(*                                                                *)
paulson@13871
    18
(* gsetprod: A generalized set product function, for ints only.   *)
paulson@13871
    19
(* Note that "setprod", as defined in IntFact, is equivalent to   *)
paulson@13871
    20
(*   our "gsetprod id".                                           *) 
paulson@13871
    21
(*                                                                *)
paulson@13871
    22
(******************************************************************)
paulson@13871
    23
paulson@13871
    24
consts
paulson@13871
    25
  gsetprod :: "('a => int) => 'a set => int"
paulson@13871
    26
paulson@13871
    27
defs
paulson@13871
    28
  gsetprod_def: "gsetprod f A ==  if finite A then fold (op * o f) 1 A else 1";
paulson@13871
    29
paulson@13871
    30
lemma gsetprod_empty [simp]: "gsetprod f {} = 1";
paulson@13871
    31
  by (auto simp add: gsetprod_def)
paulson@13871
    32
paulson@13871
    33
lemma gsetprod_insert [simp]: "[| finite A; a \<notin> A |] ==> 
paulson@13871
    34
    gsetprod f (insert a A) = f a * gsetprod f A";
paulson@13871
    35
  by (simp add: gsetprod_def LC_def LC.fold_insert)
paulson@13871
    36
paulson@13871
    37
(******************************************************************)
paulson@13871
    38
(*                                                                *)
paulson@13871
    39
(* Useful properties of sums and products                         *)
paulson@13871
    40
(*                                                                *)
paulson@13871
    41
(******************************************************************);
paulson@13871
    42
paulson@13871
    43
subsection {* Useful properties of sums and products *}
paulson@13871
    44
paulson@13871
    45
lemma setprod_gsetprod_id: "setprod A = gsetprod id A";
paulson@13871
    46
  by (auto simp add: setprod_def gsetprod_def)
paulson@13871
    47
paulson@13871
    48
lemma setsum_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
paulson@13871
    49
    setsum f S = setsum g S";
paulson@13871
    50
by (induct set: Finites, auto)
paulson@13871
    51
paulson@13871
    52
lemma gsetprod_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
paulson@13871
    53
  gsetprod f S = gsetprod g S";
paulson@13871
    54
by (induct set: Finites, auto)
paulson@13871
    55
paulson@13871
    56
lemma setsum_same_function_zcong: 
paulson@13871
    57
   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
paulson@13871
    58
     ==> [setsum f S = setsum g S] (mod m)";
paulson@13871
    59
   by (induct set: Finites, auto simp add: zcong_zadd)
paulson@13871
    60
paulson@13871
    61
lemma gsetprod_same_function_zcong: 
paulson@13871
    62
   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
paulson@13871
    63
     ==> [gsetprod f S = gsetprod g S] (mod m)";
paulson@13871
    64
by (induct set: Finites, auto simp add: zcong_zmult)
paulson@13871
    65
paulson@13871
    66
lemma gsetprod_Un_Int: "finite A ==> finite B
paulson@13871
    67
    ==> gsetprod g (A \<union> B) * gsetprod g (A \<inter> B) = 
paulson@13871
    68
    gsetprod g A * gsetprod g B";
paulson@13871
    69
  apply (induct set: Finites)
paulson@13871
    70
by (auto simp add: Int_insert_left insert_absorb)
paulson@13871
    71
paulson@13871
    72
lemma gsetprod_Un_disjoint: "[| finite A; finite B; A \<inter> B = {} |] ==> 
paulson@13871
    73
    gsetprod g (A \<union> B) = gsetprod g A * gsetprod g B";
paulson@13871
    74
  apply (subst gsetprod_Un_Int [symmetric])
paulson@13871
    75
by auto
paulson@13871
    76
paulson@13871
    77
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
paulson@13871
    78
  apply (induct set: Finites)
paulson@13871
    79
by (auto simp add: zadd_zmult_distrib2)
paulson@13871
    80
paulson@13871
    81
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = 
paulson@13871
    82
    int(c) * int(card X)";
paulson@13871
    83
  apply (induct set: Finites)
paulson@13871
    84
  apply (auto simp add: zadd_zmult_distrib2)
paulson@13871
    85
done
paulson@13871
    86
paulson@13871
    87
lemma setsum_minus: "finite A ==> setsum (%x. ((f x)::int) - g x) A = 
paulson@13871
    88
  setsum f A - setsum g A";
paulson@13871
    89
  by (induct set: Finites, auto)
paulson@13871
    90
paulson@13871
    91
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = 
paulson@13871
    92
    c * setsum f A";
paulson@13871
    93
  apply (induct set: Finites, auto)
paulson@13871
    94
  by (auto simp only: zadd_zmult_distrib2) 
paulson@13871
    95
paulson@13871
    96
lemma setsum_non_neg: "[| finite A; \<forall>x \<in> A. (0::int) \<le> f x |] ==>
paulson@13871
    97
    0 \<le>  setsum f A";
paulson@13871
    98
  by (induct set: Finites, auto)
paulson@13871
    99
paulson@13871
   100
lemma gsetprod_const: "finite X ==> gsetprod (%x. (c :: int)) X = c ^ (card X)";
paulson@13871
   101
  apply (induct set: Finites)
paulson@13871
   102
by auto
paulson@13871
   103
paulson@13871
   104
(******************************************************************)
paulson@13871
   105
(*                                                                *)
paulson@13871
   106
(* Cardinality of some explicit finite sets                       *)
paulson@13871
   107
(*                                                                *)
paulson@13871
   108
(******************************************************************);
paulson@13871
   109
paulson@13871
   110
subsection {* Cardinality of explicit finite sets *}
paulson@13871
   111
paulson@13871
   112
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B";
paulson@13871
   113
by (simp add: finite_subset finite_imageI)
paulson@13871
   114
paulson@13871
   115
lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}";
paulson@13871
   116
apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
paulson@13871
   117
by auto
paulson@13871
   118
paulson@13871
   119
lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }";
paulson@13871
   120
apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
paulson@13871
   121
by (auto simp add: bdd_nat_set_l_finite)
paulson@13871
   122
paulson@13871
   123
lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}";
paulson@13871
   124
apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> 
paulson@13871
   125
    int ` {(x :: nat). x < nat n}");
paulson@13871
   126
apply (erule finite_surjI)
paulson@13871
   127
apply (auto simp add: bdd_nat_set_l_finite image_def)
paulson@13871
   128
apply (rule_tac x = "nat x" in exI, simp) 
paulson@13871
   129
done
paulson@13871
   130
paulson@13871
   131
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}";
paulson@13871
   132
apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
paulson@13871
   133
apply (erule ssubst)
paulson@13871
   134
apply (rule bdd_int_set_l_finite)
paulson@13871
   135
by auto
paulson@13871
   136
paulson@13871
   137
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}";
paulson@13871
   138
apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
paulson@13871
   139
by (auto simp add: bdd_int_set_l_finite finite_subset)
paulson@13871
   140
paulson@13871
   141
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}";
paulson@13871
   142
apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
paulson@13871
   143
by (auto simp add: bdd_int_set_le_finite finite_subset)
paulson@13871
   144
paulson@13871
   145
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x";
paulson@13871
   146
apply (induct_tac x, force)
paulson@13871
   147
proof -;
paulson@13871
   148
  fix n::nat;
paulson@13871
   149
  assume "card {y. y < n} = n"; 
paulson@13871
   150
  have "{y. y < Suc n} = insert n {y. y < n}";
paulson@13871
   151
    by auto
paulson@13871
   152
  then have "card {y. y < Suc n} = card (insert n {y. y < n})";
paulson@13871
   153
    by auto
paulson@13871
   154
  also have "... = Suc (card {y. y < n})";
paulson@13871
   155
    apply (rule card_insert_disjoint)
paulson@13871
   156
    by (auto simp add: bdd_nat_set_l_finite)
paulson@13871
   157
  finally show "card {y. y < Suc n} = Suc n"; 
paulson@13871
   158
    by (simp add: prems)
paulson@13871
   159
qed;
paulson@13871
   160
paulson@13871
   161
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x";
paulson@13871
   162
apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
paulson@13871
   163
by (auto simp add: card_bdd_nat_set_l)
paulson@13871
   164
paulson@13871
   165
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n";
paulson@13871
   166
proof -;
paulson@13871
   167
  fix n::int;
paulson@13871
   168
  assume "0 \<le> n";
paulson@13871
   169
  have "finite {y. y < nat n}";
paulson@13871
   170
    by (rule bdd_nat_set_l_finite)
paulson@13871
   171
  moreover have "inj_on (%y. int y) {y. y < nat n}";
paulson@13871
   172
    by (auto simp add: inj_on_def)
paulson@13871
   173
  ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}";
paulson@13871
   174
    by (rule card_image)
paulson@13871
   175
  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}";
paulson@13871
   176
    apply (auto simp add: zless_nat_eq_int_zless image_def)
paulson@13871
   177
    apply (rule_tac x = "nat x" in exI)
paulson@13871
   178
    by (auto simp add: nat_0_le)
paulson@13871
   179
  also; have "card {y. y < nat n} = nat n" 
paulson@13871
   180
    by (rule card_bdd_nat_set_l)
paulson@13871
   181
  finally show "card {y. 0 \<le> y & y < n} = nat n"; .;
paulson@13871
   182
qed;
paulson@13871
   183
paulson@13871
   184
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
paulson@13871
   185
  nat n + 1";
paulson@13871
   186
apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
paulson@13871
   187
apply (insert card_bdd_int_set_l [of "n+1"])
paulson@13871
   188
by (auto simp add: nat_add_distrib)
paulson@13871
   189
paulson@13871
   190
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> 
paulson@13871
   191
    card {x. 0 < x & x \<le> n} = nat n";
paulson@13871
   192
proof -;
paulson@13871
   193
  fix n::int;
paulson@13871
   194
  assume "0 \<le> n";
paulson@13871
   195
  have "finite {x. 0 \<le> x & x < n}";
paulson@13871
   196
    by (rule bdd_int_set_l_finite)
paulson@13871
   197
  moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}";
paulson@13871
   198
    by (auto simp add: inj_on_def)
paulson@13871
   199
  ultimately have "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
paulson@13871
   200
     card {x. 0 \<le> x & x < n}";
paulson@13871
   201
    by (rule card_image)
paulson@13871
   202
  also from prems have "... = nat n";
paulson@13871
   203
    by (rule card_bdd_int_set_l)
paulson@13871
   204
  also; have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}";
paulson@13871
   205
    apply (auto simp add: image_def)
paulson@13871
   206
    apply (rule_tac x = "x - 1" in exI)
paulson@13871
   207
    by arith
paulson@13871
   208
  finally; show "card {x. 0 < x & x \<le> n} = nat n";.;
paulson@13871
   209
qed;
paulson@13871
   210
paulson@13871
   211
lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
paulson@13871
   212
    card {x. 0 < x & x < n} = nat n - 1";
paulson@13871
   213
  apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
paulson@13871
   214
  apply (insert card_bdd_int_set_l_le [of "n - 1"])
paulson@13871
   215
  by (auto simp add: nat_diff_distrib)
paulson@13871
   216
paulson@13871
   217
lemma int_card_bdd_int_set_l_l: "0 < n ==> 
paulson@13871
   218
    int(card {x. 0 < x & x < n}) = n - 1";
paulson@13871
   219
  apply (auto simp add: card_bdd_int_set_l_l)
paulson@13871
   220
  apply (subgoal_tac "Suc 0 \<le> nat n")
paulson@13871
   221
  apply (auto simp add: zdiff_int [THEN sym])
paulson@13871
   222
  apply (subgoal_tac "0 < nat n", arith)
paulson@13871
   223
  by (simp add: zero_less_nat_eq)
paulson@13871
   224
paulson@13871
   225
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> 
paulson@13871
   226
    int(card {x. 0 < x & x \<le> n}) = n";
paulson@13871
   227
  by (auto simp add: card_bdd_int_set_l_le)
paulson@13871
   228
paulson@13871
   229
(******************************************************************)
paulson@13871
   230
(*                                                                *)
paulson@13871
   231
(* Cartesian products of finite sets                              *)
paulson@13871
   232
(*                                                                *)
paulson@13871
   233
(******************************************************************)
paulson@13871
   234
paulson@13871
   235
subsection {* Cardinality of finite cartesian products *}
paulson@13871
   236
paulson@13871
   237
lemma insert_Sigma [simp]: "~(A = {}) ==>
paulson@13871
   238
  (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)";
paulson@13871
   239
  by blast
paulson@13871
   240
paulson@13871
   241
lemma cartesian_product_finite: "[| finite A; finite B |] ==> 
paulson@13871
   242
    finite (A <*> B)";
paulson@13871
   243
  apply (rule_tac F = A in finite_induct)
paulson@13871
   244
  by auto
paulson@13871
   245
paulson@13871
   246
lemma cartesian_product_card_a [simp]: "finite A ==> 
paulson@13871
   247
    card({x} <*> A) = card(A)"; 
paulson@13871
   248
  apply (subgoal_tac "inj_on (%y .(x,y)) A");
paulson@13871
   249
  apply (frule card_image, assumption)
paulson@13871
   250
  apply (subgoal_tac "(Pair x ` A) = {x} <*> A");
paulson@13871
   251
  by (auto simp add: inj_on_def)
paulson@13871
   252
paulson@13871
   253
lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
paulson@13871
   254
  card (A <*> B) = card(A) * card(B)";
paulson@13871
   255
  apply (rule_tac F = A in finite_induct, auto)
paulson@14430
   256
  done
paulson@13871
   257
paulson@13871
   258
(******************************************************************)
paulson@13871
   259
(*                                                                *)
paulson@13871
   260
(* Sums and products over finite sets                             *)
paulson@13871
   261
(*                                                                *)
paulson@13871
   262
(******************************************************************)
paulson@13871
   263
paulson@13871
   264
subsection {* Reindexing sums and products *}
paulson@13871
   265
paulson@13871
   266
lemma sum_prop [rule_format]: "finite B ==>
paulson@13871
   267
                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
paulson@13871
   268
apply (rule finite_induct, assumption, force)
paulson@13871
   269
apply (rule impI, auto)
paulson@13871
   270
apply (simp add: inj_on_def)
paulson@13871
   271
apply (subgoal_tac "f x \<notin> f ` F")
paulson@13871
   272
apply (subgoal_tac "finite (f ` F)");
paulson@13871
   273
apply (auto simp add: setsum_insert)
paulson@13871
   274
by (simp add: inj_on_def) 
paulson@13871
   275
paulson@13871
   276
lemma sum_prop_id: "finite B ==> inj_on f B ==> 
paulson@13871
   277
    setsum f B = setsum id (f ` B)";
paulson@13871
   278
by (auto simp add: sum_prop id_o)
paulson@13871
   279
paulson@13871
   280
lemma prod_prop [rule_format]: "finite B ==>
paulson@13871
   281
        inj_on f B --> gsetprod h (f ` B) = gsetprod (h \<circ> f) B";
paulson@13871
   282
  apply (rule finite_induct, assumption, force)
paulson@13871
   283
  apply (rule impI)
paulson@13871
   284
  apply (auto simp add: inj_on_def)
paulson@13871
   285
  apply (subgoal_tac "f x \<notin> f ` F")
paulson@13871
   286
  apply (subgoal_tac "finite (f ` F)");
paulson@13871
   287
by (auto simp add: gsetprod_insert)
paulson@13871
   288
paulson@13871
   289
lemma prod_prop_id: "[| finite B; inj_on f B |] ==> 
paulson@13871
   290
    gsetprod id (f ` B) = (gsetprod f B)";
paulson@13871
   291
  by (simp add: prod_prop id_o)
paulson@13871
   292
paulson@13871
   293
subsection {* Lemmas for counting arguments *}
paulson@13871
   294
paulson@13871
   295
lemma finite_union_finite_subsets: "[| finite A; \<forall>X \<in> A. finite X |] ==> 
paulson@13871
   296
    finite (Union A)";
paulson@13871
   297
apply (induct set: Finites)
paulson@13871
   298
by auto
paulson@13871
   299
paulson@13871
   300
lemma finite_index_UNION_finite_sets: "finite A ==> 
paulson@13871
   301
    (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)";
paulson@13871
   302
by (induct_tac rule: finite_induct, auto)
paulson@13871
   303
paulson@13871
   304
lemma card_union_disjoint_sets: "finite A ==> 
paulson@13871
   305
    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) ==> 
paulson@13871
   306
    card (Union A) = setsum card A";
paulson@13871
   307
  apply auto
paulson@13871
   308
  apply (induct set: Finites, auto)
paulson@13871
   309
  apply (frule_tac B = "Union F" and A = x in card_Un_Int)
paulson@13871
   310
by (auto simp add: finite_union_finite_subsets)
paulson@13871
   311
paulson@13871
   312
(*
paulson@13871
   313
  We just duplicated something in the standard library: the next lemma 
paulson@13871
   314
  is setsum_UN_disjoint in Finite_Set
paulson@13871
   315
paulson@13871
   316
lemma setsum_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
paulson@13871
   317
    ((\<forall>x \<in> A. finite (g x)) & 
paulson@13871
   318
    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
paulson@13871
   319
      setsum f (UNION A g) = setsum (%x. setsum f (g x)) A";
paulson@13871
   320
apply (induct_tac rule: finite_induct)
paulson@13871
   321
apply (assumption, simp, clarify)
paulson@13871
   322
apply (subgoal_tac "g x \<inter> (UNION F g) = {}");
paulson@13871
   323
apply (subgoal_tac "finite (UNION F g)");
paulson@13871
   324
apply (simp add: setsum_Un_disjoint)
paulson@13871
   325
by (auto simp add: finite_index_UNION_finite_sets)
paulson@13871
   326
paulson@13871
   327
*)
paulson@13871
   328
paulson@13871
   329
lemma int_card_eq_setsum [rule_format]: "finite A ==> 
paulson@13871
   330
    int (card A) = setsum (%x. 1) A";
paulson@13871
   331
  by (erule finite_induct, auto)
paulson@13871
   332
paulson@13871
   333
lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
paulson@13871
   334
    ((\<forall>x \<in> A. finite (g x)) & 
paulson@13871
   335
    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
paulson@13871
   336
      card (UNION A g) = setsum (%x. card (g x)) A";
paulson@13871
   337
apply clarify
paulson@13871
   338
apply (frule_tac f = "%x.(1::nat)" and A = g in 
paulson@13871
   339
    setsum_UN_disjoint);
paulson@13871
   340
apply assumption+;
paulson@13871
   341
apply (subgoal_tac "finite (UNION A g)");
paulson@13871
   342
apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
paulson@13871
   343
apply (auto simp only: card_eq_setsum)
paulson@13871
   344
apply (erule setsum_same_function)
paulson@14485
   345
by auto;
paulson@13871
   346
paulson@13871
   347
lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
paulson@13871
   348
    ((\<forall>x \<in> A. finite (g x)) & 
paulson@13871
   349
    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
paulson@13871
   350
       int(card (UNION A g)) = setsum (%x. int( card (g x))) A";
paulson@13871
   351
apply clarify
paulson@13871
   352
apply (frule_tac f = "%x.(1::int)" and A = g in 
paulson@13871
   353
    setsum_UN_disjoint);
paulson@13871
   354
apply assumption+;
paulson@13871
   355
apply (subgoal_tac "finite (UNION A g)");
paulson@13871
   356
apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
paulson@13871
   357
apply (auto simp only: int_card_eq_setsum)
paulson@13871
   358
apply (erule setsum_same_function)
paulson@13871
   359
by (auto simp add: int_card_eq_setsum)
paulson@13871
   360
paulson@13871
   361
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
paulson@13871
   362
    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A";
paulson@13871
   363
apply (frule_tac h = g and f = f in sum_prop, auto)
paulson@13871
   364
apply (subgoal_tac "setsum g B = setsum g (f ` A)");
paulson@13871
   365
apply (simp add: inj_on_def)
paulson@13871
   366
apply (subgoal_tac "card A = card B")
paulson@13871
   367
apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   368
apply (auto simp add: card_image)
paulson@13871
   369
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
paulson@13871
   370
apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
paulson@13871
   371
by auto
paulson@13871
   372
paulson@13871
   373
lemma gsetprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
paulson@13871
   374
    g ` B \<subseteq> A; inj_on g B |] ==> gsetprod g B = gsetprod (g \<circ> f) A";
paulson@13871
   375
  apply (frule_tac h = g and f = f in prod_prop, auto) 
paulson@13871
   376
  apply (subgoal_tac "gsetprod g B = gsetprod g (f ` A)"); 
paulson@13871
   377
  apply (simp add: inj_on_def)
paulson@13871
   378
  apply (subgoal_tac "card A = card B")
paulson@13871
   379
  apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   380
  apply (auto simp add: card_image)
paulson@13871
   381
  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
paulson@13871
   382
by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
paulson@13871
   383
paulson@13871
   384
lemma setsum_union_disjoint_sets [rule_format]: "finite A ==> 
paulson@13871
   385
    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) 
paulson@13871
   386
    --> setsum f (Union A) = setsum (%x. setsum f x) A";
paulson@13871
   387
apply (induct_tac rule: finite_induct)
paulson@13871
   388
apply (assumption, simp, clarify)
paulson@13871
   389
apply (subgoal_tac "x \<inter> (Union F) = {}");
paulson@13871
   390
apply (subgoal_tac "finite (Union F)");
paulson@13871
   391
  by (auto simp add: setsum_Un_disjoint Union_def)
paulson@13871
   392
paulson@13871
   393
lemma gsetprod_union_disjoint_sets [rule_format]: "[| 
paulson@13871
   394
    finite (A :: int set set); 
paulson@13871
   395
    (\<forall>X \<in> A. finite (X :: int set));
paulson@13871
   396
    (\<forall>X \<in> A. (\<forall>Y \<in> A. (X :: int set) \<noteq> (Y :: int set) --> 
paulson@13871
   397
      (X \<inter> Y) = {})) |] ==> 
paulson@13871
   398
  ( gsetprod (f :: int => int) (Union A) = gsetprod (%x. gsetprod f x) A)";
paulson@13871
   399
  apply (induct set: Finites)
paulson@13871
   400
  apply (auto simp add: gsetprod_empty) 
paulson@13871
   401
  apply (subgoal_tac "gsetprod f (x \<union> Union F) = 
paulson@13871
   402
    gsetprod f x * gsetprod f (Union F)");
paulson@13871
   403
  apply simp
paulson@13871
   404
  apply (rule gsetprod_Un_disjoint)
paulson@13871
   405
by (auto simp add: gsetprod_Un_disjoint Union_def)
paulson@13871
   406
paulson@13871
   407
lemma gsetprod_disjoint_sets: "[| finite A;
paulson@13871
   408
    \<forall>X \<in> A. finite X; 
paulson@13871
   409
    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
paulson@13871
   410
  gsetprod id (Union A) = gsetprod (gsetprod id) A";
paulson@13871
   411
  apply (rule_tac f = id in gsetprod_union_disjoint_sets)
paulson@13871
   412
  by auto
paulson@13871
   413
paulson@13871
   414
lemma setprod_disj_sets: "[| finite (A::int set set);
paulson@13871
   415
    \<forall>X \<in> A. finite X;
paulson@13871
   416
    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
paulson@13871
   417
  setprod (Union A) = gsetprod (%x. setprod x) A";
paulson@13871
   418
  by (auto simp add: setprod_gsetprod_id gsetprod_disjoint_sets)
paulson@13871
   419
paulson@13871
   420
end;