src/HOL/Number_Theory/Binomial.thy
author kuncar
Fri, 27 Sep 2013 14:43:26 +0200
changeset 53952 b2781a3ce958
parent 53374 a14d2a854c02
child 55130 70db8d380d62
permissions -rw-r--r--
new parametricity rules and useful lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41541
diff changeset
     1
(*  Title:      HOL/Number_Theory/Binomial.thy
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     2
    Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     3
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
     4
Defines the "choose" function, and establishes basic properties.
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     5
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     6
The original theory "Binomial" was by Lawrence C. Paulson, based on
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     7
the work of Andy Gordon and Florian Kammueller. The approach here,
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     8
which derives the definition of binomial coefficients in terms of the
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     9
factorial function, is due to Jeremy Avigad. The binomial theorem was
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    10
formalized by Tobias Nipkow.
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    11
*)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    12
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    13
header {* Binomial *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    14
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    15
theory Binomial
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    16
imports Cong Fact
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    17
begin
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    18
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    19
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    20
subsection {* Main definitions *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    21
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    22
class binomial =
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    23
  fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    24
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    25
(* definitions for the natural numbers *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    26
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    27
instantiation nat :: binomial
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    28
begin 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    29
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    30
fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    31
where
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    32
  "binomial_nat n k =
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    33
   (if k = 0 then 1 else
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    34
    if n = 0 then 0 else
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    35
      (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    36
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    37
instance ..
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    38
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    39
end
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    40
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    41
(* definitions for the integers *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    42
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    43
instantiation int :: binomial
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    44
begin 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    45
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    46
definition binomial_int :: "int => int \<Rightarrow> int" where
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    47
  "binomial_int n k =
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    48
   (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    49
    else 0)"
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    50
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    51
instance ..
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    52
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    53
end
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    54
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    55
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    56
subsection {* Set up Transfer *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    57
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    58
lemma transfer_nat_int_binomial:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    59
  "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) = 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    60
      nat (binomial n k)"
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    61
  unfolding binomial_int_def 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    62
  by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    63
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    64
lemma transfer_nat_int_binomial_closure:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    65
  "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    66
  by (auto simp add: binomial_int_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    67
35644
d20cf282342e transfer: avoid camel case
haftmann
parents: 32479
diff changeset
    68
declare transfer_morphism_nat_int[transfer add return: 
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    69
    transfer_nat_int_binomial transfer_nat_int_binomial_closure]
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    70
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    71
lemma transfer_int_nat_binomial:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    72
  "binomial (int n) (int k) = int (binomial n k)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    73
  unfolding fact_int_def binomial_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    74
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    75
lemma transfer_int_nat_binomial_closure:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    76
  "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    77
  by (auto simp add: binomial_int_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    78
35644
d20cf282342e transfer: avoid camel case
haftmann
parents: 32479
diff changeset
    79
declare transfer_morphism_int_nat[transfer add return: 
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    80
    transfer_int_nat_binomial transfer_int_nat_binomial_closure]
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    81
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    82
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    83
subsection {* Binomial coefficients *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    84
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
    85
lemma choose_zero_nat [simp]: "(n::nat) choose 0 = 1"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    86
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    87
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
    88
lemma choose_zero_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    89
  by (simp add: binomial_int_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    90
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
    91
lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
    92
  by (induct n rule: induct'_nat, auto)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    93
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
    94
lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    95
  unfolding binomial_int_def
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    96
  apply (cases "n < 0")
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    97
  apply force
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    98
  apply (simp del: binomial_nat.simps)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    99
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   100
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   101
lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   102
    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   103
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   104
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   105
lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   106
    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   107
  unfolding binomial_int_def
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   108
  apply (subst choose_reduce_nat)
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   109
    apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib)
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   110
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   111
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   112
lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) = 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   113
    (n choose (k + 1)) + (n choose k)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   114
  by (simp add: choose_reduce_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   115
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   116
lemma choose_Suc_nat: "(Suc n) choose (Suc k) = 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   117
    (n choose (Suc k)) + (n choose k)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   118
  by (simp add: choose_reduce_nat One_nat_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   119
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   120
lemma choose_plus_one_int: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) = 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   121
    (n choose (k + 1)) + (n choose k)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   122
  by (simp add: binomial_int_def choose_plus_one_nat nat_add_distrib del: binomial_nat.simps)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   123
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   124
declare binomial_nat.simps [simp del]
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   125
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   126
lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   127
  by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   128
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   129
lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   130
  by (auto simp add: binomial_int_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   131
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   132
lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   133
  by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   134
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   135
lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   136
  by (auto simp add: binomial_int_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   137
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   138
lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   139
  apply (induct n rule: induct'_nat, force)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   140
  apply (case_tac "n = 0")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   141
  apply auto
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   142
  apply (subst choose_reduce_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   143
  apply (auto simp add: One_nat_def)  
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   144
  (* natdiff_cancel_numerals introduces Suc *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   145
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   146
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   147
lemma Suc_choose_self_nat [simp]: "(Suc n) choose n = Suc n"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   148
  using plus_one_choose_self_nat by (simp add: One_nat_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   149
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   150
lemma plus_one_choose_self_int [rule_format, simp]: 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   151
    "(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   152
   by (auto simp add: binomial_int_def nat_add_distrib)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   153
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   154
(* bounded quantification doesn't work with the unicode characters? *)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   155
lemma choose_pos_nat [rule_format]: "ALL k <= (n::nat). 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   156
    ((n::nat) choose k) > 0"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   157
  apply (induct n rule: induct'_nat) 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   158
  apply force
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   159
  apply clarify
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   160
  apply (case_tac "k = 0")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   161
  apply force
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   162
  apply (subst choose_reduce_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   163
  apply auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   164
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   165
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   166
lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   167
    ((n::int) choose k) > 0"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   168
  by (auto simp add: binomial_int_def choose_pos_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   169
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   170
lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow> 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   171
    (ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   172
    P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   173
  apply (induct n rule: induct'_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   174
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   175
  apply (case_tac "k = 0")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   176
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   177
  apply (case_tac "k = n + 1")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   178
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   179
  apply (drule_tac x = n in spec) back back 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   180
  apply (drule_tac x = "k - 1" in spec) back back back
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   181
  apply auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   182
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   183
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   184
lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow> 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   185
    fact k * fact (n - k) * (n choose k) = fact n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   186
  apply (rule binomial_induct [of _ k n])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   187
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   188
proof -
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   189
  fix k :: nat and n
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   190
  assume less: "k < n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   191
  assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   192
  then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   193
    by (subst fact_plus_one_nat, auto)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   194
  assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =  fact n"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   195
  with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   196
      (n choose (k + 1)) = (n - k) * fact n"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   197
    by (subst (2) fact_plus_one_nat, auto)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   198
  with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) = 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   199
      (n - k) * fact n" by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   200
  have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   201
      fact (k + 1) * fact (n - k) * (n choose (k + 1)) + 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   202
      fact (k + 1) * fact (n - k) * (n choose k)" 
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 35731
diff changeset
   203
    by (subst choose_reduce_nat, auto simp add: field_simps)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   204
  also note one
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   205
  also note two
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 51292
diff changeset
   206
  also from less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   207
    apply (subst fact_plus_one_nat)
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 45933
diff changeset
   208
    apply (subst distrib_right [symmetric])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   209
    apply simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   210
    done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   211
  finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   212
    fact (n + 1)" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   213
qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   214
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   215
lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   216
    n choose k = fact n div (fact k * fact (n - k))"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   217
  apply (frule choose_altdef_aux_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   218
  apply (erule subst)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   219
  apply (simp add: mult_ac)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   220
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   221
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   222
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   223
lemma choose_altdef_int: 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   224
  assumes "(0::int) <= k" and "k <= n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   225
  shows "n choose k = fact n div (fact k * fact (n - k))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   226
  apply (subst tsub_eq [symmetric], rule assms)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   227
  apply (rule choose_altdef_nat [transferred])
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   228
  using assms apply auto
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   229
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   230
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   231
lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   232
  unfolding dvd_def apply (frule choose_altdef_aux_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   233
  (* why don't blast and auto get this??? *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   234
  apply (rule exI)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   235
  apply (erule sym)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   236
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   237
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   238
lemma choose_dvd_int: 
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   239
  assumes "(0::int) <= k" and "k <= n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   240
  shows "fact k * fact (n - k) dvd fact n"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   241
  apply (subst tsub_eq [symmetric], rule assms)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   242
  apply (rule choose_dvd_nat [transferred])
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   243
  using assms apply auto
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   244
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   245
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   246
(* generalizes Tobias Nipkow's proof to any commutative semiring *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   247
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   248
  (SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   249
proof (induct n rule: induct'_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   250
  show "?P 0" by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   251
next
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   252
  fix n
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   253
  assume ih: "?P n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   254
  have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   255
    by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   256
  have decomp2: "{0..n} = {0} Un {1..n}"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   257
    by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   258
  have decomp3: "{1..n+1} = {n+1} Un {1..n}"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   259
    by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   260
  have "(a+b)^(n+1) = 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   261
      (a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   262
    using ih by simp
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   263
  also have "... =  a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   264
                   b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   265
    by (rule distrib)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   266
  also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   267
                  (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   268
    by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   269
  also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   270
                  (SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   271
    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   272
      field_simps One_nat_def del:setsum_cl_ivl_Suc)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   273
  also have "... = a^(n+1) + b^(n+1) +
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   274
                  (SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   275
                  (SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   276
    by (simp add: decomp2 decomp3)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   277
  also have
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   278
      "... = a^(n+1) + b^(n+1) + 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   279
         (SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 35731
diff changeset
   280
    by (auto simp add: field_simps setsum_addf [symmetric]
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31719
diff changeset
   281
      choose_reduce_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   282
  also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 35731
diff changeset
   283
    using decomp by (simp add: field_simps)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   284
  finally show "?P (n + 1)" by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   285
qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   286
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   287
lemma card_subsets_nat:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   288
  fixes S :: "'a set"
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   289
  shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   290
proof (induct arbitrary: k set: finite)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   291
  case empty
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   292
  show ?case by (auto simp add: Collect_conv_if)
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   293
next
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   294
  case (insert x F)
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   295
  note iassms = insert(1,2)
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   296
  note ih = insert(3)
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   297
  show ?case
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   298
  proof (induct k rule: induct'_nat)
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   299
    case zero
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   300
    from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   301
      by (auto simp: finite_subset)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   302
    then show ?case by auto
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   303
  next
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   304
    case (plus1 k)
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   305
    from iassms have fin: "finite (insert x F)" by auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   306
    then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   307
      {T. T \<le> F & card T = k + 1} Un 
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   308
      {T. T \<le> insert x F & x : T & card T = k + 1}"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   309
      by auto
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   310
    with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   311
      card ({T. T \<subseteq> F \<and> card T = k + 1}) + 
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   312
      card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   313
      apply (subst card_Un_disjoint [symmetric])
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   314
      apply auto
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   315
        (* note: nice! Didn't have to say anything here *)
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   316
      done
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   317
    also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) = 
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   318
      card F choose (k+1)" by auto
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   319
    also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   320
      card ({T. T <= F & card T = k})"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   321
    proof -
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   322
      let ?f = "%T. T Un {x}"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   323
      from iassms have "inj_on ?f {T. T <= F & card T = k}"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 41340
diff changeset
   324
        unfolding inj_on_def by auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   325
      then have "card ({T. T <= F & card T = k}) = 
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   326
        card(?f ` {T. T <= F & card T = k})"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   327
        by (rule card_image [symmetric])
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   328
      also have "?f ` {T. T <= F & card T = k} = 
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   329
        {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R")
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   330
      proof-
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   331
        { fix S assume "S \<subseteq> F"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   332
          then have "card(insert x S) = card S +1"
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   333
            using iassms by (auto simp: finite_subset) }
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   334
        moreover
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   335
        { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   336
          let ?S = "T - {x}"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   337
          have "?S <= F & card ?S = k \<and> T = insert x ?S"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   338
            using 1 fin by (auto simp: finite_subset) }
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   339
        ultimately show ?thesis by(auto simp: image_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   340
      qed
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   341
      finally show ?thesis by (rule sym)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   342
    qed
41340
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   343
    also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   344
      by auto
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   345
    finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   346
      card F choose (k + 1) + (card F choose k)".
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   347
    with iassms choose_plus_one_nat show ?case
9b3f25c934c8 tuned proof
nipkow
parents: 36350
diff changeset
   348
      by (auto simp del: card.insert)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   349
  qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   350
qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   351
45933
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   352
lemma choose_le_pow:
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   353
  assumes "r \<le> n" shows "n choose r \<le> n ^ r"
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   354
proof -
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   355
  have X: "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   356
    by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   357
  have "n choose r \<le> fact n div fact (n - r)"
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   358
    using `r \<le> n` by (simp add: choose_altdef_nat div_le_mono2)
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   359
  also have "\<dots> \<le> n ^ r" using `r \<le> n`
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   360
    by (induct r rule: nat.induct)
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   361
     (auto simp add: fact_div_fact Suc_diff_Suc X One_nat_def mult_le_mono)
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   362
 finally show ?thesis .
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   363
qed
ee70da42e08a add lemmas
noschinl
parents: 44872
diff changeset
   364
51291
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   365
lemma card_UNION:
51292
8a635bf2c86c use lemma from Big_Operators
Andreas Lochbihler
parents: 51291
diff changeset
   366
  assumes "finite A" and "\<forall>k \<in> A. finite k"
51291
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   367
  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   368
  (is "?lhs = ?rhs")
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   369
proof -
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   370
  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   371
  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs")
51292
8a635bf2c86c use lemma from Big_Operators
Andreas Lochbihler
parents: 51291
diff changeset
   372
    by(subst setsum_right_distrib) simp
51291
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   373
  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   374
    using assms by(subst setsum_Sigma)(auto)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   375
  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   376
    by(rule setsum_reindex_cong[where f="\<lambda>(x, y). (y, x)"])(auto intro: inj_onI simp add: split_beta)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   377
  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   378
    using assms by(auto intro!: setsum_mono_zero_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   379
  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. -1 ^ (card I + 1)))" 
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   380
    using assms by(subst setsum_Sigma) auto
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   381
  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   382
  proof(rule setsum_cong[OF refl])
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   383
    fix x
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   384
    assume x: "x \<in> \<Union>A"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   385
    def K \<equiv> "{X \<in> A. x \<in> X}"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   386
    with `finite A` have K: "finite K" by auto
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   387
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   388
    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   389
    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   390
      using assms by(auto intro!: inj_onI)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   391
    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   392
      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)", standard] simp add: card_gt_0_iff[folded Suc_le_eq] One_nat_def dest: finite_subset intro: card_mono)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   393
    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   394
      by(rule setsum_reindex_cong[where f=snd]) fastforce
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   395
    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   396
      using assms by(subst setsum_Sigma) auto
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   397
    also have "\<dots> = (\<Sum>i=1..card A. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
51292
8a635bf2c86c use lemma from Big_Operators
Andreas Lochbihler
parents: 51291
diff changeset
   398
      by(subst setsum_right_distrib) simp
51291
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   399
    also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   400
    proof(rule setsum_mono_zero_cong_right[rule_format])
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   401
      show "{1..card K} \<subseteq> {1..card A}" using `finite A`
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   402
        by(auto simp add: K_def intro: card_mono)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   403
    next
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   404
      fix i
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   405
      assume "i \<in> {1..card A} - {1..card K}"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   406
      hence i: "i \<le> card A" "card K < i" by auto
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   407
      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}" 
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   408
        by(auto simp add: K_def)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   409
      also have "\<dots> = {}" using `finite A` i
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   410
        by(auto simp add: K_def dest: card_mono[rotated 1])
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   411
      finally show "-1 ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   412
        by(simp only:) simp
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   413
    next
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   414
      fix i
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   415
      have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   416
        (is "?lhs = ?rhs")
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   417
        by(rule setsum_cong)(auto simp add: K_def)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   418
      thus "-1 ^ (i + 1) * ?lhs = -1 ^ (i + 1) * ?rhs" by simp
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   419
    qed simp
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   420
    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   421
      by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   422
    hence "?rhs = (\<Sum>i = 0..card K. -1 ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   423
      by(subst (2) setsum_head_Suc)(simp_all add: One_nat_def)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   424
    also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   425
      using K by(subst card_subsets_nat[symmetric]) simp_all
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   426
    also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
51292
8a635bf2c86c use lemma from Big_Operators
Andreas Lochbihler
parents: 51291
diff changeset
   427
      by(subst setsum_right_distrib[symmetric]) simp
51291
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   428
    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   429
      by(subst binomial)(simp add: mult_ac)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   430
    also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   431
    finally show "?lhs x = 1" .
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   432
  qed
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   433
  also have "nat \<dots> = card (\<Union>A)" by simp
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   434
  finally show ?thesis ..
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   435
qed
c2b452628afa add inclusion/exclusion lemma
Andreas Lochbihler
parents: 49962
diff changeset
   436
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   437
end