src/HOL/NumberTheory/Finite2.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15109 bba563cdd997 child 15392 290bc97038c7 permissions -rw-r--r--
import -> imports
 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 \ 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; \x \ 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; \x \ 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; \x \ 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; \x \ 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 \ B) * gsetprod g (A \ 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 \ B = {} |] ==> ``` paulson@13871 ` 73` ``` gsetprod g (A \ 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@15047 ` 79` ``` apply (auto simp add: left_distrib right_distrib int_eq_of_nat) ``` paulson@15047 ` 80` ``` done ``` paulson@13871 ` 81` paulson@13871 ` 82` ```lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = ``` paulson@13871 ` 83` ``` int(c) * int(card X)"; ``` paulson@13871 ` 84` ``` apply (induct set: Finites) ``` paulson@13871 ` 85` ``` apply (auto simp add: zadd_zmult_distrib2) ``` paulson@13871 ` 86` ```done ``` paulson@13871 ` 87` paulson@13871 ` 88` ```lemma setsum_minus: "finite A ==> setsum (%x. ((f x)::int) - g x) A = ``` paulson@13871 ` 89` ``` setsum f A - setsum g A"; ``` paulson@13871 ` 90` ``` by (induct set: Finites, auto) ``` paulson@13871 ` 91` paulson@13871 ` 92` ```lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = ``` paulson@13871 ` 93` ``` c * setsum f A"; ``` paulson@13871 ` 94` ``` apply (induct set: Finites, auto) ``` paulson@13871 ` 95` ``` by (auto simp only: zadd_zmult_distrib2) ``` paulson@13871 ` 96` paulson@13871 ` 97` ```lemma setsum_non_neg: "[| finite A; \x \ A. (0::int) \ f x |] ==> ``` paulson@13871 ` 98` ``` 0 \ setsum f A"; ``` paulson@13871 ` 99` ``` by (induct set: Finites, auto) ``` paulson@13871 ` 100` paulson@13871 ` 101` ```lemma gsetprod_const: "finite X ==> gsetprod (%x. (c :: int)) X = c ^ (card X)"; ``` paulson@13871 ` 102` ``` apply (induct set: Finites) ``` paulson@13871 ` 103` ```by auto ``` paulson@13871 ` 104` paulson@13871 ` 105` ```(******************************************************************) ``` paulson@13871 ` 106` ```(* *) ``` paulson@13871 ` 107` ```(* Cardinality of some explicit finite sets *) ``` paulson@13871 ` 108` ```(* *) ``` paulson@13871 ` 109` ```(******************************************************************); ``` paulson@13871 ` 110` paulson@13871 ` 111` ```subsection {* Cardinality of explicit finite sets *} ``` paulson@13871 ` 112` paulson@13871 ` 113` ```lemma finite_surjI: "[| B \ f ` A; finite A |] ==> finite B"; ``` paulson@13871 ` 114` ```by (simp add: finite_subset finite_imageI) ``` paulson@13871 ` 115` paulson@13871 ` 116` ```lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}"; ``` paulson@13871 ` 117` ```apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite) ``` paulson@13871 ` 118` ```by auto ``` paulson@13871 ` 119` paulson@13871 ` 120` ```lemma bdd_nat_set_le_finite: "finite { y::nat . y \ x }"; ``` paulson@13871 ` 121` ```apply (subgoal_tac "{ y::nat . y \ x } = { y::nat . y < Suc x}") ``` paulson@13871 ` 122` ```by (auto simp add: bdd_nat_set_l_finite) ``` paulson@13871 ` 123` paulson@13871 ` 124` ```lemma bdd_int_set_l_finite: "finite { x::int . 0 \ x & x < n}"; ``` paulson@13871 ` 125` ```apply (subgoal_tac " {(x :: int). 0 \ x & x < n} \ ``` paulson@13871 ` 126` ``` int ` {(x :: nat). x < nat n}"); ``` paulson@13871 ` 127` ```apply (erule finite_surjI) ``` paulson@13871 ` 128` ```apply (auto simp add: bdd_nat_set_l_finite image_def) ``` paulson@13871 ` 129` ```apply (rule_tac x = "nat x" in exI, simp) ``` paulson@13871 ` 130` ```done ``` paulson@13871 ` 131` paulson@13871 ` 132` ```lemma bdd_int_set_le_finite: "finite {x::int. 0 \ x & x \ n}"; ``` paulson@13871 ` 133` ```apply (subgoal_tac "{x. 0 \ x & x \ n} = {x. 0 \ x & x < n + 1}") ``` paulson@13871 ` 134` ```apply (erule ssubst) ``` paulson@13871 ` 135` ```apply (rule bdd_int_set_l_finite) ``` paulson@13871 ` 136` ```by auto ``` paulson@13871 ` 137` paulson@13871 ` 138` ```lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"; ``` paulson@13871 ` 139` ```apply (subgoal_tac "{x::int. 0 < x & x < n} \ {x::int. 0 \ x & x < n}") ``` paulson@13871 ` 140` ```by (auto simp add: bdd_int_set_l_finite finite_subset) ``` paulson@13871 ` 141` paulson@13871 ` 142` ```lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \ n}"; ``` paulson@13871 ` 143` ```apply (subgoal_tac "{x::int. 0 < x & x \ n} \ {x::int. 0 \ x & x \ n}") ``` paulson@13871 ` 144` ```by (auto simp add: bdd_int_set_le_finite finite_subset) ``` paulson@13871 ` 145` paulson@13871 ` 146` ```lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"; ``` paulson@13871 ` 147` ```apply (induct_tac x, force) ``` paulson@13871 ` 148` ```proof -; ``` paulson@13871 ` 149` ``` fix n::nat; ``` paulson@13871 ` 150` ``` assume "card {y. y < n} = n"; ``` paulson@13871 ` 151` ``` have "{y. y < Suc n} = insert n {y. y < n}"; ``` paulson@13871 ` 152` ``` by auto ``` paulson@13871 ` 153` ``` then have "card {y. y < Suc n} = card (insert n {y. y < n})"; ``` paulson@13871 ` 154` ``` by auto ``` paulson@13871 ` 155` ``` also have "... = Suc (card {y. y < n})"; ``` paulson@13871 ` 156` ``` apply (rule card_insert_disjoint) ``` paulson@13871 ` 157` ``` by (auto simp add: bdd_nat_set_l_finite) ``` paulson@13871 ` 158` ``` finally show "card {y. y < Suc n} = Suc n"; ``` paulson@13871 ` 159` ``` by (simp add: prems) ``` paulson@13871 ` 160` ```qed; ``` paulson@13871 ` 161` paulson@13871 ` 162` ```lemma card_bdd_nat_set_le: "card { y::nat. y \ x} = Suc x"; ``` paulson@13871 ` 163` ```apply (subgoal_tac "{ y::nat. y \ x} = { y::nat. y < Suc x}") ``` paulson@13871 ` 164` ```by (auto simp add: card_bdd_nat_set_l) ``` paulson@13871 ` 165` paulson@13871 ` 166` ```lemma card_bdd_int_set_l: "0 \ (n::int) ==> card {y. 0 \ y & y < n} = nat n"; ``` paulson@13871 ` 167` ```proof -; ``` paulson@13871 ` 168` ``` fix n::int; ``` paulson@13871 ` 169` ``` assume "0 \ n"; ``` paulson@13871 ` 170` ``` have "finite {y. y < nat n}"; ``` paulson@13871 ` 171` ``` by (rule bdd_nat_set_l_finite) ``` paulson@13871 ` 172` ``` moreover have "inj_on (%y. int y) {y. y < nat n}"; ``` paulson@13871 ` 173` ``` by (auto simp add: inj_on_def) ``` paulson@13871 ` 174` ``` ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}"; ``` paulson@13871 ` 175` ``` by (rule card_image) ``` paulson@13871 ` 176` ``` also from prems have "int ` {y. y < nat n} = {y. 0 \ y & y < n}"; ``` paulson@13871 ` 177` ``` apply (auto simp add: zless_nat_eq_int_zless image_def) ``` paulson@13871 ` 178` ``` apply (rule_tac x = "nat x" in exI) ``` paulson@13871 ` 179` ``` by (auto simp add: nat_0_le) ``` paulson@13871 ` 180` ``` also; have "card {y. y < nat n} = nat n" ``` paulson@13871 ` 181` ``` by (rule card_bdd_nat_set_l) ``` paulson@13871 ` 182` ``` finally show "card {y. 0 \ y & y < n} = nat n"; .; ``` paulson@13871 ` 183` ```qed; ``` paulson@13871 ` 184` paulson@13871 ` 185` ```lemma card_bdd_int_set_le: "0 \ (n::int) ==> card {y. 0 \ y & y \ n} = ``` paulson@13871 ` 186` ``` nat n + 1"; ``` paulson@13871 ` 187` ```apply (subgoal_tac "{y. 0 \ y & y \ n} = {y. 0 \ y & y < n+1}") ``` paulson@13871 ` 188` ```apply (insert card_bdd_int_set_l [of "n+1"]) ``` paulson@13871 ` 189` ```by (auto simp add: nat_add_distrib) ``` paulson@13871 ` 190` paulson@13871 ` 191` ```lemma card_bdd_int_set_l_le: "0 \ (n::int) ==> ``` paulson@13871 ` 192` ``` card {x. 0 < x & x \ n} = nat n"; ``` paulson@13871 ` 193` ```proof -; ``` paulson@13871 ` 194` ``` fix n::int; ``` paulson@13871 ` 195` ``` assume "0 \ n"; ``` paulson@13871 ` 196` ``` have "finite {x. 0 \ x & x < n}"; ``` paulson@13871 ` 197` ``` by (rule bdd_int_set_l_finite) ``` paulson@13871 ` 198` ``` moreover have "inj_on (%x. x+1) {x. 0 \ x & x < n}"; ``` paulson@13871 ` 199` ``` by (auto simp add: inj_on_def) ``` paulson@13871 ` 200` ``` ultimately have "card ((%x. x+1) ` {x. 0 \ x & x < n}) = ``` paulson@13871 ` 201` ``` card {x. 0 \ x & x < n}"; ``` paulson@13871 ` 202` ``` by (rule card_image) ``` paulson@13871 ` 203` ``` also from prems have "... = nat n"; ``` paulson@13871 ` 204` ``` by (rule card_bdd_int_set_l) ``` paulson@13871 ` 205` ``` also; have "(%x. x + 1) ` {x. 0 \ x & x < n} = {x. 0 < x & x<= n}"; ``` paulson@13871 ` 206` ``` apply (auto simp add: image_def) ``` paulson@13871 ` 207` ``` apply (rule_tac x = "x - 1" in exI) ``` paulson@13871 ` 208` ``` by arith ``` paulson@13871 ` 209` ``` finally; show "card {x. 0 < x & x \ n} = nat n";.; ``` paulson@13871 ` 210` ```qed; ``` paulson@13871 ` 211` paulson@13871 ` 212` ```lemma card_bdd_int_set_l_l: "0 < (n::int) ==> ``` paulson@13871 ` 213` ``` card {x. 0 < x & x < n} = nat n - 1"; ``` paulson@13871 ` 214` ``` apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \ n - 1}") ``` paulson@13871 ` 215` ``` apply (insert card_bdd_int_set_l_le [of "n - 1"]) ``` paulson@13871 ` 216` ``` by (auto simp add: nat_diff_distrib) ``` paulson@13871 ` 217` paulson@13871 ` 218` ```lemma int_card_bdd_int_set_l_l: "0 < n ==> ``` paulson@13871 ` 219` ``` int(card {x. 0 < x & x < n}) = n - 1"; ``` paulson@13871 ` 220` ``` apply (auto simp add: card_bdd_int_set_l_l) ``` paulson@13871 ` 221` ``` apply (subgoal_tac "Suc 0 \ nat n") ``` paulson@13871 ` 222` ``` apply (auto simp add: zdiff_int [THEN sym]) ``` paulson@13871 ` 223` ``` apply (subgoal_tac "0 < nat n", arith) ``` paulson@13871 ` 224` ``` by (simp add: zero_less_nat_eq) ``` paulson@13871 ` 225` paulson@13871 ` 226` ```lemma int_card_bdd_int_set_l_le: "0 \ n ==> ``` paulson@13871 ` 227` ``` int(card {x. 0 < x & x \ n}) = n"; ``` paulson@13871 ` 228` ``` by (auto simp add: card_bdd_int_set_l_le) ``` paulson@13871 ` 229` paulson@13871 ` 230` ```(******************************************************************) ``` paulson@13871 ` 231` ```(* *) ``` paulson@13871 ` 232` ```(* Cartesian products of finite sets *) ``` paulson@13871 ` 233` ```(* *) ``` paulson@13871 ` 234` ```(******************************************************************) ``` paulson@13871 ` 235` paulson@13871 ` 236` ```subsection {* Cardinality of finite cartesian products *} ``` paulson@13871 ` 237` paulson@13871 ` 238` ```lemma insert_Sigma [simp]: "~(A = {}) ==> ``` paulson@13871 ` 239` ``` (insert x A) <*> B = ({ x } <*> B) \ (A <*> B)"; ``` paulson@13871 ` 240` ``` by blast ``` paulson@13871 ` 241` paulson@13871 ` 242` ```lemma cartesian_product_finite: "[| finite A; finite B |] ==> ``` paulson@13871 ` 243` ``` finite (A <*> B)"; ``` paulson@13871 ` 244` ``` apply (rule_tac F = A in finite_induct) ``` paulson@13871 ` 245` ``` by auto ``` paulson@13871 ` 246` paulson@13871 ` 247` ```lemma cartesian_product_card_a [simp]: "finite A ==> ``` paulson@13871 ` 248` ``` card({x} <*> A) = card(A)"; ``` paulson@13871 ` 249` ``` apply (subgoal_tac "inj_on (%y .(x,y)) A"); ``` paulson@13871 ` 250` ``` apply (frule card_image, assumption) ``` paulson@13871 ` 251` ``` apply (subgoal_tac "(Pair x ` A) = {x} <*> A"); ``` paulson@13871 ` 252` ``` by (auto simp add: inj_on_def) ``` paulson@13871 ` 253` paulson@13871 ` 254` ```lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> ``` paulson@13871 ` 255` ``` card (A <*> B) = card(A) * card(B)"; ``` paulson@13871 ` 256` ``` apply (rule_tac F = A in finite_induct, auto) ``` paulson@14430 ` 257` ``` done ``` paulson@13871 ` 258` paulson@13871 ` 259` ```(******************************************************************) ``` paulson@13871 ` 260` ```(* *) ``` paulson@13871 ` 261` ```(* Sums and products over finite sets *) ``` paulson@13871 ` 262` ```(* *) ``` paulson@13871 ` 263` ```(******************************************************************) ``` paulson@13871 ` 264` paulson@13871 ` 265` ```subsection {* Reindexing sums and products *} ``` paulson@13871 ` 266` paulson@13871 ` 267` ```lemma sum_prop [rule_format]: "finite B ==> ``` paulson@13871 ` 268` ``` inj_on f B --> setsum h (f ` B) = setsum (h \ f) B"; ``` nipkow@15109 ` 269` ```by (rule finite_induct, auto) ``` paulson@13871 ` 270` paulson@13871 ` 271` ```lemma sum_prop_id: "finite B ==> inj_on f B ==> ``` paulson@13871 ` 272` ``` setsum f B = setsum id (f ` B)"; ``` paulson@13871 ` 273` ```by (auto simp add: sum_prop id_o) ``` paulson@13871 ` 274` paulson@13871 ` 275` ```lemma prod_prop [rule_format]: "finite B ==> ``` paulson@13871 ` 276` ``` inj_on f B --> gsetprod h (f ` B) = gsetprod (h \ f) B"; ``` paulson@13871 ` 277` ``` apply (rule finite_induct, assumption, force) ``` paulson@13871 ` 278` ``` apply (rule impI) ``` paulson@13871 ` 279` ``` apply (auto simp add: inj_on_def) ``` paulson@13871 ` 280` ``` apply (subgoal_tac "f x \ f ` F") ``` paulson@13871 ` 281` ``` apply (subgoal_tac "finite (f ` F)"); ``` paulson@13871 ` 282` ```by (auto simp add: gsetprod_insert) ``` paulson@13871 ` 283` paulson@13871 ` 284` ```lemma prod_prop_id: "[| finite B; inj_on f B |] ==> ``` paulson@13871 ` 285` ``` gsetprod id (f ` B) = (gsetprod f B)"; ``` paulson@13871 ` 286` ``` by (simp add: prod_prop id_o) ``` paulson@13871 ` 287` paulson@13871 ` 288` ```subsection {* Lemmas for counting arguments *} ``` paulson@13871 ` 289` paulson@13871 ` 290` ```lemma finite_union_finite_subsets: "[| finite A; \X \ A. finite X |] ==> ``` paulson@13871 ` 291` ``` finite (Union A)"; ``` paulson@13871 ` 292` ```apply (induct set: Finites) ``` paulson@13871 ` 293` ```by auto ``` paulson@13871 ` 294` paulson@13871 ` 295` ```lemma finite_index_UNION_finite_sets: "finite A ==> ``` paulson@13871 ` 296` ``` (\x \ A. finite (f x)) --> finite (UNION A f)"; ``` paulson@13871 ` 297` ```by (induct_tac rule: finite_induct, auto) ``` paulson@13871 ` 298` paulson@13871 ` 299` ```lemma card_union_disjoint_sets: "finite A ==> ``` paulson@13871 ` 300` ``` ((\X \ A. finite X) & (\X \ A. \Y \ A. X \ Y --> X \ Y = {})) ==> ``` paulson@13871 ` 301` ``` card (Union A) = setsum card A"; ``` paulson@13871 ` 302` ``` apply auto ``` paulson@13871 ` 303` ``` apply (induct set: Finites, auto) ``` paulson@13871 ` 304` ``` apply (frule_tac B = "Union F" and A = x in card_Un_Int) ``` paulson@13871 ` 305` ```by (auto simp add: finite_union_finite_subsets) ``` paulson@13871 ` 306` paulson@13871 ` 307` ```(* ``` paulson@13871 ` 308` ``` We just duplicated something in the standard library: the next lemma ``` paulson@13871 ` 309` ``` is setsum_UN_disjoint in Finite_Set ``` paulson@13871 ` 310` paulson@13871 ` 311` ```lemma setsum_indexed_union_disjoint_sets [rule_format]: "finite A ==> ``` paulson@13871 ` 312` ``` ((\x \ A. finite (g x)) & ``` paulson@13871 ` 313` ``` (\x \ A. \y \ A. x \ y --> (g x) \ (g y) = {})) --> ``` paulson@13871 ` 314` ``` setsum f (UNION A g) = setsum (%x. setsum f (g x)) A"; ``` paulson@13871 ` 315` ```apply (induct_tac rule: finite_induct) ``` paulson@13871 ` 316` ```apply (assumption, simp, clarify) ``` paulson@13871 ` 317` ```apply (subgoal_tac "g x \ (UNION F g) = {}"); ``` paulson@13871 ` 318` ```apply (subgoal_tac "finite (UNION F g)"); ``` paulson@13871 ` 319` ```apply (simp add: setsum_Un_disjoint) ``` paulson@13871 ` 320` ```by (auto simp add: finite_index_UNION_finite_sets) ``` paulson@13871 ` 321` paulson@13871 ` 322` ```*) ``` paulson@13871 ` 323` paulson@13871 ` 324` ```lemma int_card_eq_setsum [rule_format]: "finite A ==> ``` paulson@13871 ` 325` ``` int (card A) = setsum (%x. 1) A"; ``` paulson@13871 ` 326` ``` by (erule finite_induct, auto) ``` paulson@13871 ` 327` paulson@13871 ` 328` ```lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==> ``` paulson@13871 ` 329` ``` ((\x \ A. finite (g x)) & ``` paulson@13871 ` 330` ``` (\x \ A. \y \ A. x \ y --> (g x) \ (g y) = {})) --> ``` paulson@13871 ` 331` ``` card (UNION A g) = setsum (%x. card (g x)) A"; ``` paulson@13871 ` 332` ```apply clarify ``` paulson@13871 ` 333` ```apply (frule_tac f = "%x.(1::nat)" and A = g in ``` paulson@13871 ` 334` ``` setsum_UN_disjoint); ``` paulson@13871 ` 335` ```apply assumption+; ``` paulson@13871 ` 336` ```apply (subgoal_tac "finite (UNION A g)"); ``` paulson@13871 ` 337` ```apply (subgoal_tac "(\x \ UNION A g. 1) = (\x \ A. \x \ g x. 1)"); ``` paulson@13871 ` 338` ```apply (auto simp only: card_eq_setsum) ``` paulson@13871 ` 339` ```apply (erule setsum_same_function) ``` paulson@14485 ` 340` ```by auto; ``` paulson@13871 ` 341` paulson@13871 ` 342` ```lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> ``` paulson@13871 ` 343` ``` ((\x \ A. finite (g x)) & ``` paulson@13871 ` 344` ``` (\x \ A. \y \ A. x \ y --> (g x) \ (g y) = {})) --> ``` paulson@13871 ` 345` ``` int(card (UNION A g)) = setsum (%x. int( card (g x))) A"; ``` paulson@13871 ` 346` ```apply clarify ``` paulson@13871 ` 347` ```apply (frule_tac f = "%x.(1::int)" and A = g in ``` paulson@13871 ` 348` ``` setsum_UN_disjoint); ``` paulson@13871 ` 349` ```apply assumption+; ``` paulson@13871 ` 350` ```apply (subgoal_tac "finite (UNION A g)"); ``` paulson@13871 ` 351` ```apply (subgoal_tac "(\x \ UNION A g. 1) = (\x \ A. \x \ g x. 1)"); ``` paulson@13871 ` 352` ```apply (auto simp only: int_card_eq_setsum) ``` paulson@13871 ` 353` ```apply (erule setsum_same_function) ``` paulson@13871 ` 354` ```by (auto simp add: int_card_eq_setsum) ``` paulson@13871 ` 355` paulson@13871 ` 356` ```lemma setsum_bij_eq: "[| finite A; finite B; f ` A \ B; inj_on f A; ``` paulson@13871 ` 357` ``` g ` B \ A; inj_on g B |] ==> setsum g B = setsum (g \ f) A"; ``` paulson@13871 ` 358` ```apply (frule_tac h = g and f = f in sum_prop, auto) ``` paulson@13871 ` 359` ```apply (subgoal_tac "setsum g B = setsum g (f ` A)"); ``` paulson@13871 ` 360` ```apply (simp add: inj_on_def) ``` paulson@13871 ` 361` ```apply (subgoal_tac "card A = card B") ``` paulson@13871 ` 362` ```apply (drule_tac A = "f ` A" and B = B in card_seteq) ``` paulson@13871 ` 363` ```apply (auto simp add: card_image) ``` paulson@13871 ` 364` ```apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) ``` paulson@13871 ` 365` ```apply (frule_tac A = B and B = A and f = g in card_inj_on_le) ``` paulson@13871 ` 366` ```by auto ``` paulson@13871 ` 367` paulson@13871 ` 368` ```lemma gsetprod_bij_eq: "[| finite A; finite B; f ` A \ B; inj_on f A; ``` paulson@13871 ` 369` ``` g ` B \ A; inj_on g B |] ==> gsetprod g B = gsetprod (g \ f) A"; ``` paulson@13871 ` 370` ``` apply (frule_tac h = g and f = f in prod_prop, auto) ``` paulson@13871 ` 371` ``` apply (subgoal_tac "gsetprod g B = gsetprod g (f ` A)"); ``` paulson@13871 ` 372` ``` apply (simp add: inj_on_def) ``` paulson@13871 ` 373` ``` apply (subgoal_tac "card A = card B") ``` paulson@13871 ` 374` ``` apply (drule_tac A = "f ` A" and B = B in card_seteq) ``` paulson@13871 ` 375` ``` apply (auto simp add: card_image) ``` paulson@13871 ` 376` ``` apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) ``` paulson@13871 ` 377` ```by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto) ``` paulson@13871 ` 378` paulson@13871 ` 379` ```lemma setsum_union_disjoint_sets [rule_format]: "finite A ==> ``` paulson@13871 ` 380` ``` ((\X \ A. finite X) & (\X \ A. \Y \ A. X \ Y --> X \ Y = {})) ``` paulson@13871 ` 381` ``` --> setsum f (Union A) = setsum (%x. setsum f x) A"; ``` paulson@13871 ` 382` ```apply (induct_tac rule: finite_induct) ``` paulson@13871 ` 383` ```apply (assumption, simp, clarify) ``` paulson@13871 ` 384` ```apply (subgoal_tac "x \ (Union F) = {}"); ``` paulson@13871 ` 385` ```apply (subgoal_tac "finite (Union F)"); ``` paulson@13871 ` 386` ``` by (auto simp add: setsum_Un_disjoint Union_def) ``` paulson@13871 ` 387` paulson@13871 ` 388` ```lemma gsetprod_union_disjoint_sets [rule_format]: "[| ``` paulson@13871 ` 389` ``` finite (A :: int set set); ``` paulson@13871 ` 390` ``` (\X \ A. finite (X :: int set)); ``` paulson@13871 ` 391` ``` (\X \ A. (\Y \ A. (X :: int set) \ (Y :: int set) --> ``` paulson@13871 ` 392` ``` (X \ Y) = {})) |] ==> ``` paulson@13871 ` 393` ``` ( gsetprod (f :: int => int) (Union A) = gsetprod (%x. gsetprod f x) A)"; ``` paulson@13871 ` 394` ``` apply (induct set: Finites) ``` paulson@13871 ` 395` ``` apply (auto simp add: gsetprod_empty) ``` paulson@13871 ` 396` ``` apply (subgoal_tac "gsetprod f (x \ Union F) = ``` paulson@13871 ` 397` ``` gsetprod f x * gsetprod f (Union F)"); ``` paulson@13871 ` 398` ``` apply simp ``` paulson@13871 ` 399` ``` apply (rule gsetprod_Un_disjoint) ``` paulson@13871 ` 400` ```by (auto simp add: gsetprod_Un_disjoint Union_def) ``` paulson@13871 ` 401` paulson@13871 ` 402` ```lemma gsetprod_disjoint_sets: "[| finite A; ``` paulson@13871 ` 403` ``` \X \ A. finite X; ``` paulson@13871 ` 404` ``` \X \ A. \Y \ A. (X \ Y --> X \ Y = {}) |] ==> ``` paulson@13871 ` 405` ``` gsetprod id (Union A) = gsetprod (gsetprod id) A"; ``` paulson@13871 ` 406` ``` apply (rule_tac f = id in gsetprod_union_disjoint_sets) ``` paulson@13871 ` 407` ``` by auto ``` paulson@13871 ` 408` paulson@13871 ` 409` ```lemma setprod_disj_sets: "[| finite (A::int set set); ``` paulson@13871 ` 410` ``` \X \ A. finite X; ``` paulson@13871 ` 411` ``` \X \ A. \Y \ A. (X \ Y --> X \ Y = {}) |] ==> ``` paulson@13871 ` 412` ``` setprod (Union A) = gsetprod (%x. setprod x) A"; ``` paulson@13871 ` 413` ``` by (auto simp add: setprod_gsetprod_id gsetprod_disjoint_sets) ``` paulson@13871 ` 414` paulson@13871 ` 415` ```end; ```