src/HOL/Old_Number_Theory/Finite2.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 57129 7edb7550663e child 58889 5b7a9633cfa8 permissions -rw-r--r--
simpler proof
```     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
```
```    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   apply (induct set: finite)
```
```    41   apply (auto simp add: distrib_right distrib_left)
```
```    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: distrib_left)
```
```    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: distrib_left)
```
```    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 end
```