(* Title: HOL/Quadratic_Reciprocity/Finite2.thy ID: $Id: Finite2.thy,v 1.8 2004/12/12 15:25:47 nipkow Exp $ Authors: Jeremy Avigad, David Gray, and Adam Kramer *) header {*Finite Sets and Finite Sums*} theory Finite2 imports IntFact begin text{*These are useful for combinatorial and number-theoretic counting arguments.*} text{*Note. This theory is being revised. See the web page \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} (******************************************************************) (* *) (* Useful properties of sums and products *) (* *) (******************************************************************) subsection {* Useful properties of sums and products *} lemma setsum_same_function_zcong: assumes a: "∀x ∈ S. [f x = g x](mod m)" shows "[setsum f S = setsum g S] (mod m)" proof cases assume "finite S" thus ?thesis using a by induct (simp_all add: zcong_zadd) next assume "infinite S" thus ?thesis by(simp add:setsum_def) qed lemma setprod_same_function_zcong: assumes a: "∀x ∈ S. [f x = g x](mod m)" shows "[setprod f S = setprod g S] (mod m)" proof cases assume "finite S" thus ?thesis using a by induct (simp_all add: zcong_zmult) next assume "infinite S" thus ?thesis by(simp add:setprod_def) qed lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)" apply (induct set: Finites) apply (auto simp add: left_distrib right_distrib int_eq_of_nat) done lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = int(c) * int(card X)" apply (induct set: Finites) apply (auto simp add: zadd_zmult_distrib2) done lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = c * setsum f A" apply (induct set: Finites, auto) by (auto simp only: zadd_zmult_distrib2) (******************************************************************) (* *) (* Cardinality of some explicit finite sets *) (* *) (******************************************************************) subsection {* Cardinality of explicit finite sets *} lemma finite_surjI: "[| B ⊆ f ` A; finite A |] ==> finite B" by (simp add: finite_subset finite_imageI) lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}" apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite) by auto lemma bdd_nat_set_le_finite: "finite { y::nat . y ≤ x }" apply (subgoal_tac "{ y::nat . y ≤ x } = { y::nat . y < Suc x}") by (auto simp add: bdd_nat_set_l_finite) lemma bdd_int_set_l_finite: "finite { x::int . 0 ≤ x & x < n}" apply (subgoal_tac " {(x :: int). 0 ≤ x & x < n} ⊆ int ` {(x :: nat). x < nat n}") apply (erule finite_surjI) apply (auto simp add: bdd_nat_set_l_finite image_def) apply (rule_tac x = "nat x" in exI, simp) done lemma bdd_int_set_le_finite: "finite {x::int. 0 ≤ x & x ≤ n}" apply (subgoal_tac "{x. 0 ≤ x & x ≤ n} = {x. 0 ≤ x & x < n + 1}") apply (erule ssubst) apply (rule bdd_int_set_l_finite) by auto lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}" apply (subgoal_tac "{x::int. 0 < x & x < n} ⊆ {x::int. 0 ≤ x & x < n}") by (auto simp add: bdd_int_set_l_finite finite_subset) lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x ≤ n}" apply (subgoal_tac "{x::int. 0 < x & x ≤ n} ⊆ {x::int. 0 ≤ x & x ≤ n}") by (auto simp add: bdd_int_set_le_finite finite_subset) lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x" apply (induct_tac x, force) proof - fix n::nat assume "card {y. y < n} = n" have "{y. y < Suc n} = insert n {y. y < n}" by auto then have "card {y. y < Suc n} = card (insert n {y. y < n})" by auto also have "... = Suc (card {y. y < n})" apply (rule card_insert_disjoint) by (auto simp add: bdd_nat_set_l_finite) finally show "card {y. y < Suc n} = Suc n" by (simp add: prems) qed lemma card_bdd_nat_set_le: "card { y::nat. y ≤ x} = Suc x" apply (subgoal_tac "{ y::nat. y ≤ x} = { y::nat. y < Suc x}") by (auto simp add: card_bdd_nat_set_l) lemma card_bdd_int_set_l: "0 ≤ (n::int) ==> card {y. 0 ≤ y & y < n} = nat n" proof - fix n::int assume "0 ≤ n" have "inj_on (%y. int y) {y. y < nat n}" by (auto simp add: inj_on_def) hence "card (int ` {y. y < nat n}) = card {y. y < nat n}" by (rule card_image) also from prems have "int ` {y. y < nat n} = {y. 0 ≤ y & y < n}" apply (auto simp add: zless_nat_eq_int_zless image_def) apply (rule_tac x = "nat x" in exI) by (auto simp add: nat_0_le) also have "card {y. y < nat n} = nat n" by (rule card_bdd_nat_set_l) finally show "card {y. 0 ≤ y & y < n} = nat n" . qed lemma card_bdd_int_set_le: "0 ≤ (n::int) ==> card {y. 0 ≤ y & y ≤ n} = nat n + 1" apply (subgoal_tac "{y. 0 ≤ y & y ≤ n} = {y. 0 ≤ y & y < n+1}") apply (insert card_bdd_int_set_l [of "n+1"]) by (auto simp add: nat_add_distrib) lemma card_bdd_int_set_l_le: "0 ≤ (n::int) ==> card {x. 0 < x & x ≤ n} = nat n" proof - fix n::int assume "0 ≤ n" have "inj_on (%x. x+1) {x. 0 ≤ x & x < n}" by (auto simp add: inj_on_def) hence "card ((%x. x+1) ` {x. 0 ≤ x & x < n}) = card {x. 0 ≤ x & x < n}" by (rule card_image) also from prems have "... = nat n" by (rule card_bdd_int_set_l) also have "(%x. x + 1) ` {x. 0 ≤ x & x < n} = {x. 0 < x & x<= n}" apply (auto simp add: image_def) apply (rule_tac x = "x - 1" in exI) by arith finally show "card {x. 0 < x & x ≤ n} = nat n". qed lemma card_bdd_int_set_l_l: "0 < (n::int) ==> card {x. 0 < x & x < n} = nat n - 1" apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x ≤ n - 1}") apply (insert card_bdd_int_set_l_le [of "n - 1"]) by (auto simp add: nat_diff_distrib) lemma int_card_bdd_int_set_l_l: "0 < n ==> int(card {x. 0 < x & x < n}) = n - 1" apply (auto simp add: card_bdd_int_set_l_l) apply (subgoal_tac "Suc 0 ≤ nat n") apply (auto simp add: zdiff_int [THEN sym]) apply (subgoal_tac "0 < nat n", arith) by (simp add: zero_less_nat_eq) lemma int_card_bdd_int_set_l_le: "0 ≤ n ==> int(card {x. 0 < x & x ≤ n}) = n" by (auto simp add: card_bdd_int_set_l_le) (******************************************************************) (* *) (* Cartesian products of finite sets *) (* *) (******************************************************************) subsection {* Cardinality of finite cartesian products *} (* FIXME could be useful in general but not needed here lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) ∪ (A <*> B)" by blast *) (******************************************************************) (* *) (* Sums and products over finite sets *) (* *) (******************************************************************) subsection {* Lemmas for counting arguments *} lemma setsum_bij_eq: "[| finite A; finite B; f ` A ⊆ B; inj_on f A; g ` B ⊆ A; inj_on g B |] ==> setsum g B = setsum (g o f) A" apply (frule_tac h = g and f = f in setsum_reindex) apply (subgoal_tac "setsum g B = setsum g (f ` A)") apply (simp add: inj_on_def) apply (subgoal_tac "card A = card B") apply (drule_tac A = "f ` A" and B = B in card_seteq) apply (auto simp add: card_image) apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) apply (frule_tac A = B and B = A and f = g in card_inj_on_le) by auto lemma setprod_bij_eq: "[| finite A; finite B; f ` A ⊆ B; inj_on f A; g ` B ⊆ A; inj_on g B |] ==> setprod g B = setprod (g o f) A" apply (frule_tac h = g and f = f in setprod_reindex) apply (subgoal_tac "setprod g B = setprod g (f ` A)") apply (simp add: inj_on_def) apply (subgoal_tac "card A = card B") apply (drule_tac A = "f ` A" and B = B in card_seteq) apply (auto simp add: card_image) apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto) end
lemma setsum_same_function_zcong:
∀x∈S. [f x = g x] (mod m) ==> [setsum f S = setsum g S] (mod m)
lemma setprod_same_function_zcong:
∀x∈S. [f x = g x] (mod m) ==> [setprod f S = setprod g S] (mod m)
lemma setsum_const:
finite X ==> (∑x∈X. c) = c * int (card X)
lemma setsum_const2:
finite X ==> int (∑x∈X. c) = int c * int (card X)
lemma setsum_const_mult:
finite A ==> (∑x∈A. c * f x) = c * setsum f A
lemma finite_surjI:
[| B ⊆ f ` A; finite A |] ==> finite B
lemma bdd_nat_set_l_finite:
finite {y. y < x}
lemma bdd_nat_set_le_finite:
finite {y. y ≤ x}
lemma bdd_int_set_l_finite:
finite {x. 0 ≤ x ∧ x < n}
lemma bdd_int_set_le_finite:
finite {x. 0 ≤ x ∧ x ≤ n}
lemma bdd_int_set_l_l_finite:
finite {x. 0 < x ∧ x < n}
lemma bdd_int_set_l_le_finite:
finite {x. 0 < x ∧ x ≤ n}
lemma card_bdd_nat_set_l:
card {y. y < x} = x
lemma card_bdd_nat_set_le:
card {y. y ≤ x} = Suc x
lemma card_bdd_int_set_l:
0 ≤ n ==> card {y. 0 ≤ y ∧ y < n} = nat n
lemma card_bdd_int_set_le:
0 ≤ n ==> card {y. 0 ≤ y ∧ y ≤ n} = nat n + 1
lemma card_bdd_int_set_l_le:
0 ≤ n ==> card {x. 0 < x ∧ x ≤ n} = nat n
lemma card_bdd_int_set_l_l:
0 < n ==> card {x. 0 < x ∧ x < n} = nat n - 1
lemma int_card_bdd_int_set_l_l:
0 < n ==> int (card {x. 0 < x ∧ x < n}) = n - 1
lemma int_card_bdd_int_set_l_le:
0 ≤ n ==> int (card {x. 0 < x ∧ x ≤ n}) = n
lemma setsum_bij_eq:
[| finite A; finite B; f ` A ⊆ B; inj_on f A; g ` B ⊆ A; inj_on g B |] ==> setsum g B = setsum (g o f) A
lemma setprod_bij_eq:
[| finite A; finite B; f ` A ⊆ B; inj_on f A; g ` B ⊆ A; inj_on g B |] ==> setprod g B = setprod (g o f) A