src/HOL/NumberTheory/Finite2.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15402 97204f3b4705
child 18369 694ea14ab4f2
permissions -rw-r--r--
Constant "If" is now local
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
paulson@13871
    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
paulson@13871
    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)
paulson@13871
    55
done
paulson@13871
    56
paulson@13871
    57
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = 
nipkow@15392
    58
    c * setsum f A"
paulson@13871
    59
  apply (induct set: Finites, auto)
nipkow@15392
    60
  by (auto simp only: zadd_zmult_distrib2)
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"
paulson@13871
    71
by (simp add: finite_subset finite_imageI)
paulson@13871
    72
nipkow@15392
    73
lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}"
paulson@13871
    74
apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
paulson@13871
    75
by auto
paulson@13871
    76
nipkow@15392
    77
lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }"
paulson@13871
    78
apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
paulson@13871
    79
by (auto simp add: bdd_nat_set_l_finite)
paulson@13871
    80
nipkow@15392
    81
lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}"
paulson@13871
    82
apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> 
nipkow@15392
    83
    int ` {(x :: nat). x < nat n}")
paulson@13871
    84
apply (erule finite_surjI)
paulson@13871
    85
apply (auto simp add: bdd_nat_set_l_finite image_def)
paulson@13871
    86
apply (rule_tac x = "nat x" in exI, simp) 
paulson@13871
    87
done
paulson@13871
    88
nipkow@15392
    89
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
paulson@13871
    90
apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
paulson@13871
    91
apply (erule ssubst)
paulson@13871
    92
apply (rule bdd_int_set_l_finite)
paulson@13871
    93
by auto
paulson@13871
    94
nipkow@15392
    95
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
paulson@13871
    96
apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
paulson@13871
    97
by (auto simp add: bdd_int_set_l_finite finite_subset)
paulson@13871
    98
nipkow@15392
    99
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
paulson@13871
   100
apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
paulson@13871
   101
by (auto simp add: bdd_int_set_le_finite finite_subset)
paulson@13871
   102
nipkow@15392
   103
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
paulson@13871
   104
apply (induct_tac x, force)
nipkow@15392
   105
proof -
nipkow@15392
   106
  fix n::nat
nipkow@15392
   107
  assume "card {y. y < n} = n" 
nipkow@15392
   108
  have "{y. y < Suc n} = insert n {y. y < n}"
paulson@13871
   109
    by auto
nipkow@15392
   110
  then have "card {y. y < Suc n} = card (insert n {y. y < n})"
paulson@13871
   111
    by auto
nipkow@15392
   112
  also have "... = Suc (card {y. y < n})"
paulson@13871
   113
    apply (rule card_insert_disjoint)
paulson@13871
   114
    by (auto simp add: bdd_nat_set_l_finite)
nipkow@15392
   115
  finally show "card {y. y < Suc n} = Suc n" 
paulson@13871
   116
    by (simp add: prems)
nipkow@15392
   117
qed
paulson@13871
   118
nipkow@15392
   119
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
paulson@13871
   120
apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
paulson@13871
   121
by (auto simp add: card_bdd_nat_set_l)
paulson@13871
   122
nipkow@15392
   123
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
nipkow@15392
   124
proof -
nipkow@15392
   125
  fix n::int
nipkow@15392
   126
  assume "0 \<le> n"
nipkow@15402
   127
  have "inj_on (%y. int y) {y. y < nat n}"
paulson@13871
   128
    by (auto simp add: inj_on_def)
nipkow@15402
   129
  hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
paulson@13871
   130
    by (rule card_image)
nipkow@15392
   131
  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
paulson@13871
   132
    apply (auto simp add: zless_nat_eq_int_zless image_def)
paulson@13871
   133
    apply (rule_tac x = "nat x" in exI)
paulson@13871
   134
    by (auto simp add: nat_0_le)
nipkow@15392
   135
  also have "card {y. y < nat n} = nat n" 
paulson@13871
   136
    by (rule card_bdd_nat_set_l)
nipkow@15392
   137
  finally show "card {y. 0 \<le> y & y < n} = nat n" .
nipkow@15392
   138
qed
paulson@13871
   139
paulson@13871
   140
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
nipkow@15392
   141
  nat n + 1"
paulson@13871
   142
apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
paulson@13871
   143
apply (insert card_bdd_int_set_l [of "n+1"])
paulson@13871
   144
by (auto simp add: nat_add_distrib)
paulson@13871
   145
paulson@13871
   146
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> 
nipkow@15392
   147
    card {x. 0 < x & x \<le> n} = nat n"
nipkow@15392
   148
proof -
nipkow@15392
   149
  fix n::int
nipkow@15392
   150
  assume "0 \<le> n"
nipkow@15402
   151
  have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
paulson@13871
   152
    by (auto simp add: inj_on_def)
nipkow@15402
   153
  hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
nipkow@15392
   154
     card {x. 0 \<le> x & x < n}"
paulson@13871
   155
    by (rule card_image)
nipkow@15392
   156
  also from prems have "... = nat n"
paulson@13871
   157
    by (rule card_bdd_int_set_l)
nipkow@15392
   158
  also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
paulson@13871
   159
    apply (auto simp add: image_def)
paulson@13871
   160
    apply (rule_tac x = "x - 1" in exI)
paulson@13871
   161
    by arith
nipkow@15392
   162
  finally show "card {x. 0 < x & x \<le> n} = nat n".
nipkow@15392
   163
qed
paulson@13871
   164
paulson@13871
   165
lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
nipkow@15392
   166
    card {x. 0 < x & x < n} = nat n - 1"
paulson@13871
   167
  apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
paulson@13871
   168
  apply (insert card_bdd_int_set_l_le [of "n - 1"])
paulson@13871
   169
  by (auto simp add: nat_diff_distrib)
paulson@13871
   170
paulson@13871
   171
lemma int_card_bdd_int_set_l_l: "0 < n ==> 
nipkow@15392
   172
    int(card {x. 0 < x & x < n}) = n - 1"
paulson@13871
   173
  apply (auto simp add: card_bdd_int_set_l_l)
paulson@13871
   174
  apply (subgoal_tac "Suc 0 \<le> nat n")
paulson@13871
   175
  apply (auto simp add: zdiff_int [THEN sym])
paulson@13871
   176
  apply (subgoal_tac "0 < nat n", arith)
paulson@13871
   177
  by (simp add: zero_less_nat_eq)
paulson@13871
   178
paulson@13871
   179
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> 
nipkow@15392
   180
    int(card {x. 0 < x & x \<le> n}) = n"
paulson@13871
   181
  by (auto simp add: card_bdd_int_set_l_le)
paulson@13871
   182
paulson@13871
   183
(******************************************************************)
paulson@13871
   184
(*                                                                *)
paulson@13871
   185
(* Cartesian products of finite sets                              *)
paulson@13871
   186
(*                                                                *)
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
paulson@13871
   196
(******************************************************************)
paulson@13871
   197
(*                                                                *)
paulson@13871
   198
(* Sums and products over finite sets                             *)
paulson@13871
   199
(*                                                                *)
paulson@13871
   200
(******************************************************************)
paulson@13871
   201
paulson@13871
   202
subsection {* Lemmas for counting arguments *}
paulson@13871
   203
paulson@13871
   204
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
nipkow@15392
   205
    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
nipkow@15392
   206
apply (frule_tac h = g and f = f in setsum_reindex)
nipkow@15392
   207
apply (subgoal_tac "setsum g B = setsum g (f ` A)")
paulson@13871
   208
apply (simp add: inj_on_def)
paulson@13871
   209
apply (subgoal_tac "card A = card B")
paulson@13871
   210
apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   211
apply (auto simp add: card_image)
paulson@13871
   212
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
paulson@13871
   213
apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
paulson@13871
   214
by auto
paulson@13871
   215
nipkow@15392
   216
lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
nipkow@15392
   217
    g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
nipkow@15392
   218
  apply (frule_tac h = g and f = f in setprod_reindex)
nipkow@15392
   219
  apply (subgoal_tac "setprod g B = setprod g (f ` A)") 
paulson@13871
   220
  apply (simp add: inj_on_def)
paulson@13871
   221
  apply (subgoal_tac "card A = card B")
paulson@13871
   222
  apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   223
  apply (auto simp add: card_image)
paulson@13871
   224
  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
paulson@13871
   225
by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
paulson@13871
   226
nipkow@15392
   227
end