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