src/HOL/Old_Number_Theory/Finite2.thy
author wenzelm
Sat Oct 10 16:26:23 2015 +0200 (2015-10-10)
changeset 61382 efac889fccbc
parent 61286 dcf7be51bf5d
child 64267 b9a1486e79be
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Old_Number_Theory/Finite2.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3 *)
     4 
     5 section \<open>Finite Sets and Finite Sums\<close>
     6 
     7 theory Finite2
     8 imports IntFact "~~/src/HOL/Library/Infinite_Set"
     9 begin
    10 
    11 text\<open>
    12   These are useful for combinatorial and number-theoretic counting
    13   arguments.
    14 \<close>
    15 
    16 
    17 subsection \<open>Useful properties of sums and products\<close>
    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
    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
    37 qed
    38 
    39 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
    40 by (simp add: of_nat_mult)
    41 
    42 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
    43     int(c) * int(card X)"
    44 by (simp add: of_nat_mult)
    45 
    46 lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
    47     c * setsum f A"
    48   by (induct set: finite) (auto simp add: distrib_left)
    49 
    50 
    51 subsection \<open>Cardinality of explicit finite sets\<close>
    52 
    53 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
    54 by (simp add: finite_subset)
    55 
    56 lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
    57   by (rule bounded_nat_set_is_finite) blast
    58 
    59 lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}"
    60 proof -
    61   have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto
    62   then show ?thesis by (auto simp add: bdd_nat_set_l_finite)
    63 qed
    64 
    65 lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
    66   apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
    67       int ` {(x :: nat). x < nat n}")
    68    apply (erule finite_surjI)
    69    apply (auto simp add: bdd_nat_set_l_finite image_def)
    70   apply (rule_tac x = "nat x" in exI, simp)
    71   done
    72 
    73 lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
    74   apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
    75    apply (erule ssubst)
    76    apply (rule bdd_int_set_l_finite)
    77   apply auto
    78   done
    79 
    80 lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
    81 proof -
    82   have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}"
    83     by auto
    84   then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset)
    85 qed
    86 
    87 lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
    88 proof -
    89   have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}"
    90     by auto
    91   then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset)
    92 qed
    93 
    94 lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
    95 proof (induct x)
    96   case 0
    97   show "card {y::nat . y < 0} = 0" by simp
    98 next
    99   case (Suc n)
   100   have "{y. y < Suc n} = insert n {y. y < n}"
   101     by auto
   102   then have "card {y. y < Suc n} = card (insert n {y. y < n})"
   103     by auto
   104   also have "... = Suc (card {y. y < n})"
   105     by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
   106   finally show "card {y. y < Suc n} = Suc n"
   107     using \<open>card {y. y < n} = n\<close> by simp
   108 qed
   109 
   110 lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
   111 proof -
   112   have "{y::nat. y \<le> x} = { y::nat. y < Suc x}"
   113     by auto
   114   then show ?thesis by (auto simp add: card_bdd_nat_set_l)
   115 qed
   116 
   117 lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
   118 proof -
   119   assume "0 \<le> n"
   120   have "inj_on (%y. int y) {y. y < nat n}"
   121     by (auto simp add: inj_on_def)
   122   hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
   123     by (rule card_image)
   124   also from \<open>0 \<le> n\<close> have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
   125     apply (auto simp add: zless_nat_eq_int_zless image_def)
   126     apply (rule_tac x = "nat x" in exI)
   127     apply (auto simp add: nat_0_le)
   128     done
   129   also have "card {y. y < nat n} = nat n"
   130     by (rule card_bdd_nat_set_l)
   131   finally show "card {y. 0 \<le> y & y < n} = nat n" .
   132 qed
   133 
   134 lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
   135   nat n + 1"
   136 proof -
   137   assume "0 \<le> n"
   138   moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto
   139   ultimately show ?thesis
   140     using card_bdd_int_set_l [of "n + 1"]
   141     by (auto simp add: nat_add_distrib)
   142 qed
   143 
   144 lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
   145     card {x. 0 < x & x \<le> n} = nat n"
   146 proof -
   147   assume "0 \<le> n"
   148   have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
   149     by (auto simp add: inj_on_def)
   150   hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
   151      card {x. 0 \<le> x & x < n}"
   152     by (rule card_image)
   153   also from \<open>0 \<le> n\<close> have "... = nat n"
   154     by (rule card_bdd_int_set_l)
   155   also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
   156     apply (auto simp add: image_def)
   157     apply (rule_tac x = "x - 1" in exI)
   158     apply arith
   159     done
   160   finally show "card {x. 0 < x & x \<le> n} = nat n" .
   161 qed
   162 
   163 lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
   164   card {x. 0 < x & x < n} = nat n - 1"
   165 proof -
   166   assume "0 < n"
   167   moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}"
   168     by simp
   169   ultimately show ?thesis
   170     using insert card_bdd_int_set_l_le [of "n - 1"]
   171     by (auto simp add: nat_diff_distrib)
   172 qed
   173 
   174 lemma int_card_bdd_int_set_l_l: "0 < n ==>
   175     int(card {x. 0 < x & x < n}) = n - 1"
   176   apply (auto simp add: card_bdd_int_set_l_l)
   177   done
   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 end