src/HOL/Old_Number_Theory/Finite2.thy
author wenzelm
Sat Oct 10 16:26:23 2015 +0200 (2015-10-10)
changeset 61382 efac889fccbc
parent 61286 dcf7be51bf5d
child 64267 b9a1486e79be
permissions -rw-r--r--
isabelle update_cartouches;
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
wenzelm@61382
     5
section \<open>Finite Sets and Finite Sums\<close>
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@61382
    11
text\<open>
wenzelm@19670
    12
  These are useful for combinatorial and number-theoretic counting
wenzelm@19670
    13
  arguments.
wenzelm@61382
    14
\<close>
paulson@13871
    15
paulson@13871
    16
wenzelm@61382
    17
subsection \<open>Useful properties of sums and products\<close>
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
haftmann@51489
    26
  assume "infinite S" thus ?thesis by simp
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
haftmann@51489
    36
  assume "infinite S" thus ?thesis by simp
nipkow@15392
    37
qed
paulson@13871
    38
nipkow@15392
    39
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
lp15@61286
    40
by (simp add: of_nat_mult)
paulson@13871
    41
wenzelm@18369
    42
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
nipkow@15392
    43
    int(c) * int(card X)"
lp15@61286
    44
by (simp add: of_nat_mult)
paulson@13871
    45
wenzelm@18369
    46
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
nipkow@15392
    47
    c * setsum f A"
webertj@49962
    48
  by (induct set: finite) (auto simp add: distrib_left)
wenzelm@18369
    49
paulson@13871
    50
wenzelm@61382
    51
subsection \<open>Cardinality of explicit finite sets\<close>
paulson@13871
    52
nipkow@15392
    53
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
nipkow@40786
    54
by (simp add: finite_subset)
paulson@13871
    55
wenzelm@18369
    56
lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
wenzelm@18369
    57
  by (rule bounded_nat_set_is_finite) blast
paulson@13871
    58
wenzelm@18369
    59
lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}"
wenzelm@18369
    60
proof -
wenzelm@18369
    61
  have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto
wenzelm@18369
    62
  then show ?thesis by (auto simp add: bdd_nat_set_l_finite)
wenzelm@18369
    63
qed
paulson@13871
    64
wenzelm@18369
    65
lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
wenzelm@19670
    66
  apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
wenzelm@19670
    67
      int ` {(x :: nat). x < nat n}")
wenzelm@19670
    68
   apply (erule finite_surjI)
wenzelm@19670
    69
   apply (auto simp add: bdd_nat_set_l_finite image_def)
wenzelm@19670
    70
  apply (rule_tac x = "nat x" in exI, simp)
wenzelm@19670
    71
  done
paulson@13871
    72
nipkow@15392
    73
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
wenzelm@19670
    74
  apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
wenzelm@19670
    75
   apply (erule ssubst)
wenzelm@19670
    76
   apply (rule bdd_int_set_l_finite)
wenzelm@19670
    77
  apply auto
wenzelm@19670
    78
  done
paulson@13871
    79
nipkow@15392
    80
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
wenzelm@18369
    81
proof -
wenzelm@18369
    82
  have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}"
wenzelm@18369
    83
    by auto
wenzelm@18369
    84
  then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset)
wenzelm@18369
    85
qed
paulson@13871
    86
nipkow@15392
    87
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
wenzelm@18369
    88
proof -
wenzelm@18369
    89
  have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}"
wenzelm@18369
    90
    by auto
wenzelm@18369
    91
  then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset)
wenzelm@18369
    92
qed
paulson@13871
    93
nipkow@15392
    94
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
wenzelm@18369
    95
proof (induct x)
wenzelm@20369
    96
  case 0
wenzelm@18369
    97
  show "card {y::nat . y < 0} = 0" by simp
wenzelm@18369
    98
next
wenzelm@20369
    99
  case (Suc n)
nipkow@15392
   100
  have "{y. y < Suc n} = insert n {y. y < n}"
paulson@13871
   101
    by auto
nipkow@15392
   102
  then have "card {y. y < Suc n} = card (insert n {y. y < n})"
paulson@13871
   103
    by auto
nipkow@15392
   104
  also have "... = Suc (card {y. y < n})"
wenzelm@18369
   105
    by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
wenzelm@18369
   106
  finally show "card {y. y < Suc n} = Suc n"
wenzelm@61382
   107
    using \<open>card {y. y < n} = n\<close> by simp
nipkow@15392
   108
qed
paulson@13871
   109
nipkow@15392
   110
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
wenzelm@18369
   111
proof -
wenzelm@18369
   112
  have "{y::nat. y \<le> x} = { y::nat. y < Suc x}"
wenzelm@18369
   113
    by auto
wenzelm@18369
   114
  then show ?thesis by (auto simp add: card_bdd_nat_set_l)
wenzelm@18369
   115
qed
paulson@13871
   116
nipkow@15392
   117
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
nipkow@15392
   118
proof -
nipkow@15392
   119
  assume "0 \<le> n"
nipkow@15402
   120
  have "inj_on (%y. int y) {y. y < nat n}"
paulson@13871
   121
    by (auto simp add: inj_on_def)
nipkow@15402
   122
  hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
paulson@13871
   123
    by (rule card_image)
wenzelm@61382
   124
  also from \<open>0 \<le> n\<close> have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
paulson@13871
   125
    apply (auto simp add: zless_nat_eq_int_zless image_def)
paulson@13871
   126
    apply (rule_tac x = "nat x" in exI)
wenzelm@18369
   127
    apply (auto simp add: nat_0_le)
wenzelm@18369
   128
    done
wenzelm@18369
   129
  also have "card {y. y < nat n} = nat n"
paulson@13871
   130
    by (rule card_bdd_nat_set_l)
nipkow@15392
   131
  finally show "card {y. 0 \<le> y & y < n} = nat n" .
nipkow@15392
   132
qed
paulson@13871
   133
wenzelm@18369
   134
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
nipkow@15392
   135
  nat n + 1"
wenzelm@18369
   136
proof -
wenzelm@18369
   137
  assume "0 \<le> n"
wenzelm@18369
   138
  moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto
wenzelm@18369
   139
  ultimately show ?thesis
wenzelm@18369
   140
    using card_bdd_int_set_l [of "n + 1"]
wenzelm@18369
   141
    by (auto simp add: nat_add_distrib)
wenzelm@18369
   142
qed
paulson@13871
   143
wenzelm@18369
   144
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
nipkow@15392
   145
    card {x. 0 < x & x \<le> n} = nat n"
nipkow@15392
   146
proof -
nipkow@15392
   147
  assume "0 \<le> n"
nipkow@15402
   148
  have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
paulson@13871
   149
    by (auto simp add: inj_on_def)
wenzelm@18369
   150
  hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
nipkow@15392
   151
     card {x. 0 \<le> x & x < n}"
paulson@13871
   152
    by (rule card_image)
wenzelm@61382
   153
  also from \<open>0 \<le> n\<close> have "... = nat n"
paulson@13871
   154
    by (rule card_bdd_int_set_l)
nipkow@15392
   155
  also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
paulson@13871
   156
    apply (auto simp add: image_def)
paulson@13871
   157
    apply (rule_tac x = "x - 1" in exI)
wenzelm@18369
   158
    apply arith
wenzelm@18369
   159
    done
wenzelm@18369
   160
  finally show "card {x. 0 < x & x \<le> n} = nat n" .
nipkow@15392
   161
qed
paulson@13871
   162
wenzelm@18369
   163
lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
wenzelm@18369
   164
  card {x. 0 < x & x < n} = nat n - 1"
wenzelm@18369
   165
proof -
wenzelm@18369
   166
  assume "0 < n"
wenzelm@18369
   167
  moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}"
wenzelm@18369
   168
    by simp
wenzelm@18369
   169
  ultimately show ?thesis
wenzelm@18369
   170
    using insert card_bdd_int_set_l_le [of "n - 1"]
wenzelm@18369
   171
    by (auto simp add: nat_diff_distrib)
wenzelm@18369
   172
qed
paulson@13871
   173
wenzelm@18369
   174
lemma int_card_bdd_int_set_l_l: "0 < n ==>
nipkow@15392
   175
    int(card {x. 0 < x & x < n}) = n - 1"
paulson@13871
   176
  apply (auto simp add: card_bdd_int_set_l_l)
wenzelm@18369
   177
  done
paulson@13871
   178
wenzelm@18369
   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
wenzelm@18369
   184
end