src/HOL/NumberTheory/Finite2.thy
author wenzelm
Thu Dec 08 12:50:04 2005 +0100 (2005-12-08)
changeset 18369 694ea14ab4f2
parent 15402 97204f3b4705
child 19670 2e4a143c73c5
permissions -rw-r--r--
tuned sources and proofs
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
nipkow@15392
     9
imports IntFact
nipkow@15392
    10
begin
paulson@13871
    11
paulson@13871
    12
text{*These are useful for combinatorial and number-theoretic counting
paulson@13871
    13
arguments.*}
paulson@13871
    14
paulson@13871
    15
text{*Note.  This theory is being revised.  See the web page
paulson@13871
    16
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
paulson@13871
    17
paulson@13871
    18
(******************************************************************)
paulson@13871
    19
(*                                                                *)
nipkow@15392
    20
(* Useful properties of sums and products                         *)
paulson@13871
    21
(*                                                                *)
paulson@13871
    22
(******************************************************************)
paulson@13871
    23
paulson@13871
    24
subsection {* Useful properties of sums and products *}
paulson@13871
    25
wenzelm@18369
    26
lemma setsum_same_function_zcong:
nipkow@15392
    27
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
nipkow@15392
    28
shows "[setsum f S = setsum g S] (mod m)"
nipkow@15392
    29
proof cases
nipkow@15392
    30
  assume "finite S"
nipkow@15392
    31
  thus ?thesis using a by induct (simp_all add: zcong_zadd)
nipkow@15392
    32
next
nipkow@15392
    33
  assume "infinite S" thus ?thesis by(simp add:setsum_def)
nipkow@15392
    34
qed
paulson@13871
    35
nipkow@15392
    36
lemma setprod_same_function_zcong:
nipkow@15392
    37
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
nipkow@15392
    38
shows "[setprod f S = setprod g S] (mod m)"
nipkow@15392
    39
proof cases
nipkow@15392
    40
  assume "finite S"
nipkow@15392
    41
  thus ?thesis using a by induct (simp_all add: zcong_zmult)
nipkow@15392
    42
next
nipkow@15392
    43
  assume "infinite S" thus ?thesis by(simp add:setprod_def)
nipkow@15392
    44
qed
paulson@13871
    45
nipkow@15392
    46
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
paulson@13871
    47
  apply (induct set: Finites)
paulson@15047
    48
  apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
paulson@15047
    49
  done
paulson@13871
    50
wenzelm@18369
    51
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
nipkow@15392
    52
    int(c) * int(card X)"
paulson@13871
    53
  apply (induct set: Finites)
paulson@13871
    54
  apply (auto simp add: zadd_zmult_distrib2)
wenzelm@18369
    55
  done
paulson@13871
    56
wenzelm@18369
    57
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
nipkow@15392
    58
    c * setsum f A"
wenzelm@18369
    59
  by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
wenzelm@18369
    60
paulson@13871
    61
paulson@13871
    62
(******************************************************************)
paulson@13871
    63
(*                                                                *)
paulson@13871
    64
(* Cardinality of some explicit finite sets                       *)
paulson@13871
    65
(*                                                                *)
nipkow@15392
    66
(******************************************************************)
paulson@13871
    67
paulson@13871
    68
subsection {* Cardinality of explicit finite sets *}
paulson@13871
    69
nipkow@15392
    70
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
wenzelm@18369
    71
  by (simp add: finite_subset finite_imageI)
paulson@13871
    72
wenzelm@18369
    73
lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
wenzelm@18369
    74
  by (rule bounded_nat_set_is_finite) blast
paulson@13871
    75
wenzelm@18369
    76
lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}"
wenzelm@18369
    77
proof -
wenzelm@18369
    78
  have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto
wenzelm@18369
    79
  then show ?thesis by (auto simp add: bdd_nat_set_l_finite)
wenzelm@18369
    80
qed
paulson@13871
    81
wenzelm@18369
    82
lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
wenzelm@18369
    83
apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
nipkow@15392
    84
    int ` {(x :: nat). x < nat n}")
paulson@13871
    85
apply (erule finite_surjI)
paulson@13871
    86
apply (auto simp add: bdd_nat_set_l_finite image_def)
wenzelm@18369
    87
apply (rule_tac x = "nat x" in exI, simp)
paulson@13871
    88
done
paulson@13871
    89
nipkow@15392
    90
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
paulson@13871
    91
apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
paulson@13871
    92
apply (erule ssubst)
paulson@13871
    93
apply (rule bdd_int_set_l_finite)
wenzelm@18369
    94
apply auto
wenzelm@18369
    95
done
paulson@13871
    96
nipkow@15392
    97
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
wenzelm@18369
    98
proof -
wenzelm@18369
    99
  have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}"
wenzelm@18369
   100
    by auto
wenzelm@18369
   101
  then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset)
wenzelm@18369
   102
qed
paulson@13871
   103
nipkow@15392
   104
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
wenzelm@18369
   105
proof -
wenzelm@18369
   106
  have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}"
wenzelm@18369
   107
    by auto
wenzelm@18369
   108
  then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset)
wenzelm@18369
   109
qed
paulson@13871
   110
nipkow@15392
   111
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
wenzelm@18369
   112
proof (induct x)
wenzelm@18369
   113
  show "card {y::nat . y < 0} = 0" by simp
wenzelm@18369
   114
next
nipkow@15392
   115
  fix n::nat
wenzelm@18369
   116
  assume "card {y. y < n} = n"
nipkow@15392
   117
  have "{y. y < Suc n} = insert n {y. y < n}"
paulson@13871
   118
    by auto
nipkow@15392
   119
  then have "card {y. y < Suc n} = card (insert n {y. y < n})"
paulson@13871
   120
    by auto
nipkow@15392
   121
  also have "... = Suc (card {y. y < n})"
wenzelm@18369
   122
    by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
wenzelm@18369
   123
  finally show "card {y. y < Suc n} = Suc n"
paulson@13871
   124
    by (simp add: prems)
nipkow@15392
   125
qed
paulson@13871
   126
nipkow@15392
   127
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
wenzelm@18369
   128
proof -
wenzelm@18369
   129
  have "{y::nat. y \<le> x} = { y::nat. y < Suc x}"
wenzelm@18369
   130
    by auto
wenzelm@18369
   131
  then show ?thesis by (auto simp add: card_bdd_nat_set_l)
wenzelm@18369
   132
qed
paulson@13871
   133
nipkow@15392
   134
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
nipkow@15392
   135
proof -
nipkow@15392
   136
  assume "0 \<le> n"
nipkow@15402
   137
  have "inj_on (%y. int y) {y. y < nat n}"
paulson@13871
   138
    by (auto simp add: inj_on_def)
nipkow@15402
   139
  hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
paulson@13871
   140
    by (rule card_image)
nipkow@15392
   141
  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
paulson@13871
   142
    apply (auto simp add: zless_nat_eq_int_zless image_def)
paulson@13871
   143
    apply (rule_tac x = "nat x" in exI)
wenzelm@18369
   144
    apply (auto simp add: nat_0_le)
wenzelm@18369
   145
    done
wenzelm@18369
   146
  also have "card {y. y < nat n} = nat n"
paulson@13871
   147
    by (rule card_bdd_nat_set_l)
nipkow@15392
   148
  finally show "card {y. 0 \<le> y & y < n} = nat n" .
nipkow@15392
   149
qed
paulson@13871
   150
wenzelm@18369
   151
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
nipkow@15392
   152
  nat n + 1"
wenzelm@18369
   153
proof -
wenzelm@18369
   154
  assume "0 \<le> n"
wenzelm@18369
   155
  moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto
wenzelm@18369
   156
  ultimately show ?thesis
wenzelm@18369
   157
    using card_bdd_int_set_l [of "n + 1"]
wenzelm@18369
   158
    by (auto simp add: nat_add_distrib)
wenzelm@18369
   159
qed
paulson@13871
   160
wenzelm@18369
   161
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
nipkow@15392
   162
    card {x. 0 < x & x \<le> n} = nat n"
nipkow@15392
   163
proof -
nipkow@15392
   164
  assume "0 \<le> n"
nipkow@15402
   165
  have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
paulson@13871
   166
    by (auto simp add: inj_on_def)
wenzelm@18369
   167
  hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
nipkow@15392
   168
     card {x. 0 \<le> x & x < n}"
paulson@13871
   169
    by (rule card_image)
wenzelm@18369
   170
  also from `0 \<le> n` have "... = nat n"
paulson@13871
   171
    by (rule card_bdd_int_set_l)
nipkow@15392
   172
  also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
paulson@13871
   173
    apply (auto simp add: image_def)
paulson@13871
   174
    apply (rule_tac x = "x - 1" in exI)
wenzelm@18369
   175
    apply arith
wenzelm@18369
   176
    done
wenzelm@18369
   177
  finally show "card {x. 0 < x & x \<le> n} = nat n" .
nipkow@15392
   178
qed
paulson@13871
   179
wenzelm@18369
   180
lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
wenzelm@18369
   181
  card {x. 0 < x & x < n} = nat n - 1"
wenzelm@18369
   182
proof -
wenzelm@18369
   183
  assume "0 < n"
wenzelm@18369
   184
  moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}"
wenzelm@18369
   185
    by simp
wenzelm@18369
   186
  ultimately show ?thesis
wenzelm@18369
   187
    using insert card_bdd_int_set_l_le [of "n - 1"]
wenzelm@18369
   188
    by (auto simp add: nat_diff_distrib)
wenzelm@18369
   189
qed
paulson@13871
   190
wenzelm@18369
   191
lemma int_card_bdd_int_set_l_l: "0 < n ==>
nipkow@15392
   192
    int(card {x. 0 < x & x < n}) = n - 1"
paulson@13871
   193
  apply (auto simp add: card_bdd_int_set_l_l)
paulson@13871
   194
  apply (subgoal_tac "Suc 0 \<le> nat n")
wenzelm@18369
   195
  apply (auto simp add: zdiff_int [symmetric])
paulson@13871
   196
  apply (subgoal_tac "0 < nat n", arith)
wenzelm@18369
   197
  apply (simp add: zero_less_nat_eq)
wenzelm@18369
   198
  done
paulson@13871
   199
wenzelm@18369
   200
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
nipkow@15392
   201
    int(card {x. 0 < x & x \<le> n}) = n"
paulson@13871
   202
  by (auto simp add: card_bdd_int_set_l_le)
paulson@13871
   203
paulson@13871
   204
(******************************************************************)
paulson@13871
   205
(*                                                                *)
paulson@13871
   206
(* Cartesian products of finite sets                              *)
paulson@13871
   207
(*                                                                *)
paulson@13871
   208
(******************************************************************)
paulson@13871
   209
paulson@13871
   210
subsection {* Cardinality of finite cartesian products *}
paulson@13871
   211
nipkow@15402
   212
(* FIXME could be useful in general but not needed here
nipkow@15402
   213
lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
paulson@13871
   214
  by blast
nipkow@15402
   215
 *)
paulson@13871
   216
paulson@13871
   217
(******************************************************************)
paulson@13871
   218
(*                                                                *)
paulson@13871
   219
(* Sums and products over finite sets                             *)
paulson@13871
   220
(*                                                                *)
paulson@13871
   221
(******************************************************************)
paulson@13871
   222
paulson@13871
   223
subsection {* Lemmas for counting arguments *}
paulson@13871
   224
wenzelm@18369
   225
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
nipkow@15392
   226
    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
nipkow@15392
   227
apply (frule_tac h = g and f = f in setsum_reindex)
nipkow@15392
   228
apply (subgoal_tac "setsum g B = setsum g (f ` A)")
paulson@13871
   229
apply (simp add: inj_on_def)
paulson@13871
   230
apply (subgoal_tac "card A = card B")
paulson@13871
   231
apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   232
apply (auto simp add: card_image)
paulson@13871
   233
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
paulson@13871
   234
apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
wenzelm@18369
   235
apply auto
wenzelm@18369
   236
done
paulson@13871
   237
wenzelm@18369
   238
lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
nipkow@15392
   239
    g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
nipkow@15392
   240
  apply (frule_tac h = g and f = f in setprod_reindex)
wenzelm@18369
   241
  apply (subgoal_tac "setprod g B = setprod g (f ` A)")
paulson@13871
   242
  apply (simp add: inj_on_def)
paulson@13871
   243
  apply (subgoal_tac "card A = card B")
paulson@13871
   244
  apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   245
  apply (auto simp add: card_image)
paulson@13871
   246
  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
wenzelm@18369
   247
  apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
wenzelm@18369
   248
  done
paulson@13871
   249
wenzelm@18369
   250
end