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