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