src/HOL/NumberTheory/Finite2.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 15402 97204f3b4705 child 18369 694ea14ab4f2 permissions -rw-r--r--
Constant "If" is now local
```     1 (*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
```
```     2     ID:         \$Id\$
```
```     3     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
```
```     4 *)
```
```     5
```
```     6 header {*Finite Sets and Finite Sums*}
```
```     7
```
```     8 theory Finite2
```
```     9 imports IntFact
```
```    10 begin
```
```    11
```
```    12 text{*These are useful for combinatorial and number-theoretic counting
```
```    13 arguments.*}
```
```    14
```
```    15 text{*Note.  This theory is being revised.  See the web page
```
```    16 \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
```
```    17
```
```    18 (******************************************************************)
```
```    19 (*                                                                *)
```
```    20 (* Useful properties of sums and products                         *)
```
```    21 (*                                                                *)
```
```    22 (******************************************************************)
```
```    23
```
```    24 subsection {* Useful properties of sums and products *}
```
```    25
```
```    26 lemma setsum_same_function_zcong:
```
```    27 assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
```
```    28 shows "[setsum f S = setsum g S] (mod m)"
```
```    29 proof cases
```
```    30   assume "finite S"
```
```    31   thus ?thesis using a by induct (simp_all add: zcong_zadd)
```
```    32 next
```
```    33   assume "infinite S" thus ?thesis by(simp add:setsum_def)
```
```    34 qed
```
```    35
```
```    36 lemma setprod_same_function_zcong:
```
```    37 assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
```
```    38 shows "[setprod f S = setprod g S] (mod m)"
```
```    39 proof cases
```
```    40   assume "finite S"
```
```    41   thus ?thesis using a by induct (simp_all add: zcong_zmult)
```
```    42 next
```
```    43   assume "infinite S" thus ?thesis by(simp add:setprod_def)
```
```    44 qed
```
```    45
```
```    46 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
```
```    47   apply (induct set: Finites)
```
```    48   apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
```
```    49   done
```
```    50
```
```    51 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
```
```    52     int(c) * int(card X)"
```
```    53   apply (induct set: Finites)
```
```    54   apply (auto simp add: zadd_zmult_distrib2)
```
```    55 done
```
```    56
```
```    57 lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
```
```    58     c * setsum f A"
```
```    59   apply (induct set: Finites, auto)
```
```    60   by (auto simp only: zadd_zmult_distrib2)
```
```    61
```
```    62 (******************************************************************)
```
```    63 (*                                                                *)
```
```    64 (* Cardinality of some explicit finite sets                       *)
```
```    65 (*                                                                *)
```
```    66 (******************************************************************)
```
```    67
```
```    68 subsection {* Cardinality of explicit finite sets *}
```
```    69
```
```    70 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
```
```    71 by (simp add: finite_subset finite_imageI)
```
```    72
```
```    73 lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}"
```
```    74 apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
```
```    75 by auto
```
```    76
```
```    77 lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }"
```
```    78 apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
```
```    79 by (auto simp add: bdd_nat_set_l_finite)
```
```    80
```
```    81 lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}"
```
```    82 apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
```
```    83     int ` {(x :: nat). x < nat n}")
```
```    84 apply (erule finite_surjI)
```
```    85 apply (auto simp add: bdd_nat_set_l_finite image_def)
```
```    86 apply (rule_tac x = "nat x" in exI, simp)
```
```    87 done
```
```    88
```
```    89 lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
```
```    90 apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
```
```    91 apply (erule ssubst)
```
```    92 apply (rule bdd_int_set_l_finite)
```
```    93 by auto
```
```    94
```
```    95 lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
```
```    96 apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
```
```    97 by (auto simp add: bdd_int_set_l_finite finite_subset)
```
```    98
```
```    99 lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
```
```   100 apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
```
```   101 by (auto simp add: bdd_int_set_le_finite finite_subset)
```
```   102
```
```   103 lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
```
```   104 apply (induct_tac x, force)
```
```   105 proof -
```
```   106   fix n::nat
```
```   107   assume "card {y. y < n} = n"
```
```   108   have "{y. y < Suc n} = insert n {y. y < n}"
```
```   109     by auto
```
```   110   then have "card {y. y < Suc n} = card (insert n {y. y < n})"
```
```   111     by auto
```
```   112   also have "... = Suc (card {y. y < n})"
```
```   113     apply (rule card_insert_disjoint)
```
```   114     by (auto simp add: bdd_nat_set_l_finite)
```
```   115   finally show "card {y. y < Suc n} = Suc n"
```
```   116     by (simp add: prems)
```
```   117 qed
```
```   118
```
```   119 lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
```
```   120 apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
```
```   121 by (auto simp add: card_bdd_nat_set_l)
```
```   122
```
```   123 lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
```
```   124 proof -
```
```   125   fix n::int
```
```   126   assume "0 \<le> n"
```
```   127   have "inj_on (%y. int y) {y. y < nat n}"
```
```   128     by (auto simp add: inj_on_def)
```
```   129   hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
```
```   130     by (rule card_image)
```
```   131   also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
```
```   132     apply (auto simp add: zless_nat_eq_int_zless image_def)
```
```   133     apply (rule_tac x = "nat x" in exI)
```
```   134     by (auto simp add: nat_0_le)
```
```   135   also have "card {y. y < nat n} = nat n"
```
```   136     by (rule card_bdd_nat_set_l)
```
```   137   finally show "card {y. 0 \<le> y & y < n} = nat n" .
```
```   138 qed
```
```   139
```
```   140 lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
```
```   141   nat n + 1"
```
```   142 apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
```
```   143 apply (insert card_bdd_int_set_l [of "n+1"])
```
```   144 by (auto simp add: nat_add_distrib)
```
```   145
```
```   146 lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
```
```   147     card {x. 0 < x & x \<le> n} = nat n"
```
```   148 proof -
```
```   149   fix n::int
```
```   150   assume "0 \<le> n"
```
```   151   have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
```
```   152     by (auto simp add: inj_on_def)
```
```   153   hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
```
```   154      card {x. 0 \<le> x & x < n}"
```
```   155     by (rule card_image)
```
```   156   also from prems have "... = nat n"
```
```   157     by (rule card_bdd_int_set_l)
```
```   158   also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
```
```   159     apply (auto simp add: image_def)
```
```   160     apply (rule_tac x = "x - 1" in exI)
```
```   161     by arith
```
```   162   finally show "card {x. 0 < x & x \<le> n} = nat n".
```
```   163 qed
```
```   164
```
```   165 lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
```
```   166     card {x. 0 < x & x < n} = nat n - 1"
```
```   167   apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
```
```   168   apply (insert card_bdd_int_set_l_le [of "n - 1"])
```
```   169   by (auto simp add: nat_diff_distrib)
```
```   170
```
```   171 lemma int_card_bdd_int_set_l_l: "0 < n ==>
```
```   172     int(card {x. 0 < x & x < n}) = n - 1"
```
```   173   apply (auto simp add: card_bdd_int_set_l_l)
```
```   174   apply (subgoal_tac "Suc 0 \<le> nat n")
```
```   175   apply (auto simp add: zdiff_int [THEN sym])
```
```   176   apply (subgoal_tac "0 < nat n", arith)
```
```   177   by (simp add: zero_less_nat_eq)
```
```   178
```
```   179 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
```
```   180     int(card {x. 0 < x & x \<le> n}) = n"
```
```   181   by (auto simp add: card_bdd_int_set_l_le)
```
```   182
```
```   183 (******************************************************************)
```
```   184 (*                                                                *)
```
```   185 (* Cartesian products of finite sets                              *)
```
```   186 (*                                                                *)
```
```   187 (******************************************************************)
```
```   188
```
```   189 subsection {* Cardinality of finite cartesian products *}
```
```   190
```
```   191 (* FIXME could be useful in general but not needed here
```
```   192 lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
```
```   193   by blast
```
```   194  *)
```
```   195
```
```   196 (******************************************************************)
```
```   197 (*                                                                *)
```
```   198 (* Sums and products over finite sets                             *)
```
```   199 (*                                                                *)
```
```   200 (******************************************************************)
```
```   201
```
```   202 subsection {* Lemmas for counting arguments *}
```
```   203
```
```   204 lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
```
```   205     g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
```
```   206 apply (frule_tac h = g and f = f in setsum_reindex)
```
```   207 apply (subgoal_tac "setsum g B = setsum g (f ` A)")
```
```   208 apply (simp add: inj_on_def)
```
```   209 apply (subgoal_tac "card A = card B")
```
```   210 apply (drule_tac A = "f ` A" and B = B in card_seteq)
```
```   211 apply (auto simp add: card_image)
```
```   212 apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
```
```   213 apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
```
```   214 by auto
```
```   215
```
```   216 lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
```
```   217     g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
```
```   218   apply (frule_tac h = g and f = f in setprod_reindex)
```
```   219   apply (subgoal_tac "setprod g B = setprod g (f ` A)")
```
```   220   apply (simp add: inj_on_def)
```
```   221   apply (subgoal_tac "card A = card B")
```
```   222   apply (drule_tac A = "f ` A" and B = B in card_seteq)
```
```   223   apply (auto simp add: card_image)
```
```   224   apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
```
```   225 by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
```
```   226
```
`   227 end`