src/HOL/NumberTheory/Finite2.thy
author nipkow
Thu Dec 09 18:30:59 2004 +0100 (2004-12-09)
changeset 15392 290bc97038c7
parent 15109 bba563cdd997
child 15402 97204f3b4705
permissions -rw-r--r--
First step in reorganizing Finite_Set
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@15392
   127
  have "finite {y. y < nat n}"
paulson@13871
   128
    by (rule bdd_nat_set_l_finite)
nipkow@15392
   129
  moreover have "inj_on (%y. int y) {y. y < nat n}"
paulson@13871
   130
    by (auto simp add: inj_on_def)
nipkow@15392
   131
  ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}"
paulson@13871
   132
    by (rule card_image)
nipkow@15392
   133
  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
paulson@13871
   134
    apply (auto simp add: zless_nat_eq_int_zless image_def)
paulson@13871
   135
    apply (rule_tac x = "nat x" in exI)
paulson@13871
   136
    by (auto simp add: nat_0_le)
nipkow@15392
   137
  also have "card {y. y < nat n} = nat n" 
paulson@13871
   138
    by (rule card_bdd_nat_set_l)
nipkow@15392
   139
  finally show "card {y. 0 \<le> y & y < n} = nat n" .
nipkow@15392
   140
qed
paulson@13871
   141
paulson@13871
   142
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
nipkow@15392
   143
  nat n + 1"
paulson@13871
   144
apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
paulson@13871
   145
apply (insert card_bdd_int_set_l [of "n+1"])
paulson@13871
   146
by (auto simp add: nat_add_distrib)
paulson@13871
   147
paulson@13871
   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
  fix n::int
nipkow@15392
   152
  assume "0 \<le> n"
nipkow@15392
   153
  have "finite {x. 0 \<le> x & x < n}"
paulson@13871
   154
    by (rule bdd_int_set_l_finite)
nipkow@15392
   155
  moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
paulson@13871
   156
    by (auto simp add: inj_on_def)
paulson@13871
   157
  ultimately have "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
nipkow@15392
   158
     card {x. 0 \<le> x & x < n}"
paulson@13871
   159
    by (rule card_image)
nipkow@15392
   160
  also from prems have "... = nat n"
paulson@13871
   161
    by (rule card_bdd_int_set_l)
nipkow@15392
   162
  also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
paulson@13871
   163
    apply (auto simp add: image_def)
paulson@13871
   164
    apply (rule_tac x = "x - 1" in exI)
paulson@13871
   165
    by arith
nipkow@15392
   166
  finally show "card {x. 0 < x & x \<le> n} = nat n".
nipkow@15392
   167
qed
paulson@13871
   168
paulson@13871
   169
lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
nipkow@15392
   170
    card {x. 0 < x & x < n} = nat n - 1"
paulson@13871
   171
  apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
paulson@13871
   172
  apply (insert card_bdd_int_set_l_le [of "n - 1"])
paulson@13871
   173
  by (auto simp add: nat_diff_distrib)
paulson@13871
   174
paulson@13871
   175
lemma int_card_bdd_int_set_l_l: "0 < n ==> 
nipkow@15392
   176
    int(card {x. 0 < x & x < n}) = n - 1"
paulson@13871
   177
  apply (auto simp add: card_bdd_int_set_l_l)
paulson@13871
   178
  apply (subgoal_tac "Suc 0 \<le> nat n")
paulson@13871
   179
  apply (auto simp add: zdiff_int [THEN sym])
paulson@13871
   180
  apply (subgoal_tac "0 < nat n", arith)
paulson@13871
   181
  by (simp add: zero_less_nat_eq)
paulson@13871
   182
paulson@13871
   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
(*                                                                *)
paulson@13871
   189
(* Cartesian products of finite sets                              *)
paulson@13871
   190
(*                                                                *)
paulson@13871
   191
(******************************************************************)
paulson@13871
   192
paulson@13871
   193
subsection {* Cardinality of finite cartesian products *}
paulson@13871
   194
paulson@13871
   195
lemma insert_Sigma [simp]: "~(A = {}) ==>
nipkow@15392
   196
  (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
paulson@13871
   197
  by blast
paulson@13871
   198
paulson@13871
   199
lemma cartesian_product_finite: "[| finite A; finite B |] ==> 
nipkow@15392
   200
    finite (A <*> B)"
paulson@13871
   201
  apply (rule_tac F = A in finite_induct)
paulson@13871
   202
  by auto
paulson@13871
   203
paulson@13871
   204
lemma cartesian_product_card_a [simp]: "finite A ==> 
nipkow@15392
   205
    card({x} <*> A) = card(A)" 
nipkow@15392
   206
  apply (subgoal_tac "inj_on (%y .(x,y)) A")
paulson@13871
   207
  apply (frule card_image, assumption)
nipkow@15392
   208
  apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
paulson@13871
   209
  by (auto simp add: inj_on_def)
paulson@13871
   210
paulson@13871
   211
lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
nipkow@15392
   212
  card (A <*> B) = card(A) * card(B)"
paulson@13871
   213
  apply (rule_tac F = A in finite_induct, auto)
paulson@14430
   214
  done
paulson@13871
   215
paulson@13871
   216
(******************************************************************)
paulson@13871
   217
(*                                                                *)
paulson@13871
   218
(* Sums and products over finite sets                             *)
paulson@13871
   219
(*                                                                *)
paulson@13871
   220
(******************************************************************)
paulson@13871
   221
paulson@13871
   222
subsection {* Lemmas for counting arguments *}
paulson@13871
   223
paulson@13871
   224
lemma finite_union_finite_subsets: "[| finite A; \<forall>X \<in> A. finite X |] ==> 
nipkow@15392
   225
    finite (Union A)"
paulson@13871
   226
apply (induct set: Finites)
paulson@13871
   227
by auto
paulson@13871
   228
paulson@13871
   229
lemma finite_index_UNION_finite_sets: "finite A ==> 
nipkow@15392
   230
    (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)"
paulson@13871
   231
by (induct_tac rule: finite_induct, auto)
paulson@13871
   232
paulson@13871
   233
lemma card_union_disjoint_sets: "finite A ==> 
paulson@13871
   234
    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) ==> 
nipkow@15392
   235
    card (Union A) = setsum card A"
paulson@13871
   236
  apply auto
paulson@13871
   237
  apply (induct set: Finites, auto)
paulson@13871
   238
  apply (frule_tac B = "Union F" and A = x in card_Un_Int)
paulson@13871
   239
by (auto simp add: finite_union_finite_subsets)
paulson@13871
   240
paulson@13871
   241
lemma int_card_eq_setsum [rule_format]: "finite A ==> 
nipkow@15392
   242
    int (card A) = setsum (%x. 1) A"
paulson@13871
   243
  by (erule finite_induct, auto)
paulson@13871
   244
paulson@13871
   245
lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
paulson@13871
   246
    ((\<forall>x \<in> A. finite (g x)) & 
paulson@13871
   247
    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
nipkow@15392
   248
      card (UNION A g) = setsum (%x. card (g x)) A"
paulson@13871
   249
apply clarify
paulson@13871
   250
apply (frule_tac f = "%x.(1::nat)" and A = g in 
nipkow@15392
   251
    setsum_UN_disjoint)
nipkow@15392
   252
apply assumption+
nipkow@15392
   253
apply (subgoal_tac "finite (UNION A g)")
nipkow@15392
   254
apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)")
paulson@13871
   255
apply (auto simp only: card_eq_setsum)
nipkow@15392
   256
apply (rule setsum_cong)
nipkow@15392
   257
by auto
paulson@13871
   258
paulson@13871
   259
lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
paulson@13871
   260
    ((\<forall>x \<in> A. finite (g x)) & 
paulson@13871
   261
    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
nipkow@15392
   262
       int(card (UNION A g)) = setsum (%x. int( card (g x))) A"
paulson@13871
   263
apply clarify
paulson@13871
   264
apply (frule_tac f = "%x.(1::int)" and A = g in 
nipkow@15392
   265
    setsum_UN_disjoint)
nipkow@15392
   266
apply assumption+
nipkow@15392
   267
apply (subgoal_tac "finite (UNION A g)")
nipkow@15392
   268
apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)")
paulson@13871
   269
apply (auto simp only: int_card_eq_setsum)
nipkow@15392
   270
apply (rule setsum_cong)
paulson@13871
   271
by (auto simp add: int_card_eq_setsum)
paulson@13871
   272
paulson@13871
   273
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
nipkow@15392
   274
    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
nipkow@15392
   275
apply (frule_tac h = g and f = f in setsum_reindex)
nipkow@15392
   276
apply (subgoal_tac "setsum g B = setsum g (f ` A)")
paulson@13871
   277
apply (simp add: inj_on_def)
paulson@13871
   278
apply (subgoal_tac "card A = card B")
paulson@13871
   279
apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   280
apply (auto simp add: card_image)
paulson@13871
   281
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
paulson@13871
   282
apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
paulson@13871
   283
by auto
paulson@13871
   284
nipkow@15392
   285
lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
nipkow@15392
   286
    g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
nipkow@15392
   287
  apply (frule_tac h = g and f = f in setprod_reindex)
nipkow@15392
   288
  apply (subgoal_tac "setprod g B = setprod g (f ` A)") 
paulson@13871
   289
  apply (simp add: inj_on_def)
paulson@13871
   290
  apply (subgoal_tac "card A = card B")
paulson@13871
   291
  apply (drule_tac A = "f ` A" and B = B in card_seteq)
paulson@13871
   292
  apply (auto simp add: card_image)
paulson@13871
   293
  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
paulson@13871
   294
by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
paulson@13871
   295
nipkow@15392
   296
end