src/HOL/Old_Number_Theory/Finite2.thy
author haftmann
Tue Sep 01 15:39:33 2009 +0200 (2009-09-01)
changeset 32479 521cc9bf2958
parent 25592 src/HOL/NumberTheory/Finite2.thy@e8ddaf6bf5df
child 38159 e9b4835a54ee
permissions -rw-r--r--
some reorganization of number theory
     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 Main IntFact Infinite_Set
    10 begin
    11 
    12 text{*
    13   These are useful for combinatorial and number-theoretic counting
    14   arguments.
    15 *}
    16 
    17 
    18 subsection {* Useful properties of sums and products *}
    19 
    20 lemma setsum_same_function_zcong:
    21   assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    22   shows "[setsum f S = setsum g S] (mod m)"
    23 proof cases
    24   assume "finite S"
    25   thus ?thesis using a by induct (simp_all add: zcong_zadd)
    26 next
    27   assume "infinite S" thus ?thesis by(simp add:setsum_def)
    28 qed
    29 
    30 lemma setprod_same_function_zcong:
    31   assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    32   shows "[setprod f S = setprod g S] (mod m)"
    33 proof cases
    34   assume "finite S"
    35   thus ?thesis using a by induct (simp_all add: zcong_zmult)
    36 next
    37   assume "infinite S" thus ?thesis by(simp add:setprod_def)
    38 qed
    39 
    40 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
    41   apply (induct set: finite)
    42   apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
    43   done
    44 
    45 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
    46     int(c) * int(card X)"
    47   apply (induct set: finite)
    48   apply (auto simp add: zadd_zmult_distrib2)
    49   done
    50 
    51 lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
    52     c * setsum f A"
    53   by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
    54 
    55 
    56 subsection {* Cardinality of explicit finite sets *}
    57 
    58 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
    59   by (simp add: finite_subset finite_imageI)
    60 
    61 lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
    62   by (rule bounded_nat_set_is_finite) blast
    63 
    64 lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}"
    65 proof -
    66   have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto
    67   then show ?thesis by (auto simp add: bdd_nat_set_l_finite)
    68 qed
    69 
    70 lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
    71   apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
    72       int ` {(x :: nat). x < nat n}")
    73    apply (erule finite_surjI)
    74    apply (auto simp add: bdd_nat_set_l_finite image_def)
    75   apply (rule_tac x = "nat x" in exI, simp)
    76   done
    77 
    78 lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
    79   apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
    80    apply (erule ssubst)
    81    apply (rule bdd_int_set_l_finite)
    82   apply auto
    83   done
    84 
    85 lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
    86 proof -
    87   have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}"
    88     by auto
    89   then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset)
    90 qed
    91 
    92 lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
    93 proof -
    94   have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}"
    95     by auto
    96   then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset)
    97 qed
    98 
    99 lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
   100 proof (induct x)
   101   case 0
   102   show "card {y::nat . y < 0} = 0" by simp
   103 next
   104   case (Suc n)
   105   have "{y. y < Suc n} = insert n {y. y < n}"
   106     by auto
   107   then have "card {y. y < Suc n} = card (insert n {y. y < n})"
   108     by auto
   109   also have "... = Suc (card {y. y < n})"
   110     by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
   111   finally show "card {y. y < Suc n} = Suc n"
   112     using `card {y. y < n} = n` by simp
   113 qed
   114 
   115 lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
   116 proof -
   117   have "{y::nat. y \<le> x} = { y::nat. y < Suc x}"
   118     by auto
   119   then show ?thesis by (auto simp add: card_bdd_nat_set_l)
   120 qed
   121 
   122 lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
   123 proof -
   124   assume "0 \<le> n"
   125   have "inj_on (%y. int y) {y. y < nat n}"
   126     by (auto simp add: inj_on_def)
   127   hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
   128     by (rule card_image)
   129   also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
   130     apply (auto simp add: zless_nat_eq_int_zless image_def)
   131     apply (rule_tac x = "nat x" in exI)
   132     apply (auto simp add: nat_0_le)
   133     done
   134   also have "card {y. y < nat n} = nat n"
   135     by (rule card_bdd_nat_set_l)
   136   finally show "card {y. 0 \<le> y & y < n} = nat n" .
   137 qed
   138 
   139 lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
   140   nat n + 1"
   141 proof -
   142   assume "0 \<le> n"
   143   moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto
   144   ultimately show ?thesis
   145     using card_bdd_int_set_l [of "n + 1"]
   146     by (auto simp add: nat_add_distrib)
   147 qed
   148 
   149 lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
   150     card {x. 0 < x & x \<le> n} = nat n"
   151 proof -
   152   assume "0 \<le> n"
   153   have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
   154     by (auto simp add: inj_on_def)
   155   hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
   156      card {x. 0 \<le> x & x < n}"
   157     by (rule card_image)
   158   also from `0 \<le> n` have "... = nat n"
   159     by (rule card_bdd_int_set_l)
   160   also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
   161     apply (auto simp add: image_def)
   162     apply (rule_tac x = "x - 1" in exI)
   163     apply arith
   164     done
   165   finally show "card {x. 0 < x & x \<le> n} = nat n" .
   166 qed
   167 
   168 lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
   169   card {x. 0 < x & x < n} = nat n - 1"
   170 proof -
   171   assume "0 < n"
   172   moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}"
   173     by simp
   174   ultimately show ?thesis
   175     using insert card_bdd_int_set_l_le [of "n - 1"]
   176     by (auto simp add: nat_diff_distrib)
   177 qed
   178 
   179 lemma int_card_bdd_int_set_l_l: "0 < n ==>
   180     int(card {x. 0 < x & x < n}) = n - 1"
   181   apply (auto simp add: card_bdd_int_set_l_l)
   182   done
   183 
   184 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
   185     int(card {x. 0 < x & x \<le> n}) = n"
   186   by (auto simp add: card_bdd_int_set_l_le)
   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 text {* Lemmas for counting arguments. *}
   197 
   198 lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
   199     g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
   200   apply (frule_tac h = g and f = f in setsum_reindex)
   201   apply (subgoal_tac "setsum g B = setsum g (f ` A)")
   202    apply (simp add: inj_on_def)
   203   apply (subgoal_tac "card A = card B")
   204    apply (drule_tac A = "f ` A" and B = B in card_seteq)
   205      apply (auto simp add: card_image)
   206   apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   207   apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
   208     apply auto
   209   done
   210 
   211 lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
   212     g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
   213   apply (frule_tac h = g and f = f in setprod_reindex)
   214   apply (subgoal_tac "setprod g B = setprod g (f ` A)")
   215    apply (simp add: inj_on_def)
   216   apply (subgoal_tac "card A = card B")
   217    apply (drule_tac A = "f ` A" and B = B in card_seteq)
   218      apply (auto simp add: card_image)
   219   apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   220   apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   221   done
   222 
   223 end