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