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