author | skalberg |
Fri, 05 Dec 2003 19:39:39 +0100 | |
changeset 14278 | ae499452700a |
parent 13601 | fd3e3d6b37b2 |
permissions | -rw-r--r-- |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Power.ML |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
4 |
Copyright 1997 University of Cambridge |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
5 |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
6 |
The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
7 |
Also binomial coefficents |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
8 |
*) |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
9 |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
10 |
(*** Simple laws about Power ***) |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
11 |
|
5069 | 12 |
Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
13 |
by (induct_tac "k" 1); |
4089 | 14 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac))); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
15 |
qed "power_add"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
16 |
|
5069 | 17 |
Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
18 |
by (induct_tac "k" 1); |
4089 | 19 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add]))); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
20 |
qed "power_mult"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
21 |
|
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8861
diff
changeset
|
22 |
Goal "!!i::nat. 0 < i ==> 0 < i^n"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
23 |
by (induct_tac "n" 1); |
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8861
diff
changeset
|
24 |
by (ALLGOALS Asm_simp_tac); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
25 |
qed "zero_less_power"; |
8861 | 26 |
Addsimps [zero_less_power]; |
27 |
||
11365 | 28 |
Goal "i^n = 0 ==> i = (0::nat)"; |
29 |
by (etac contrapos_pp 1); |
|
30 |
by Auto_tac; |
|
31 |
qed "power_eq_0D"; |
|
32 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
33 |
Goal "!!i::nat. 1 <= i ==> Suc 0 <= i^n"; |
8861 | 34 |
by (induct_tac "n" 1); |
35 |
by Auto_tac; |
|
36 |
qed "one_le_power"; |
|
37 |
Addsimps [one_le_power]; |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
38 |
|
11331 | 39 |
Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)"; |
40 |
by (induct_tac "n" 1); |
|
41 |
by Auto_tac; |
|
42 |
by (ALLGOALS (case_tac "m")); |
|
13601 | 43 |
by (Simp_tac 1); |
11331 | 44 |
by Auto_tac; |
45 |
qed_spec_mp "power_inject"; |
|
46 |
Addsimps [power_inject]; |
|
47 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8861
diff
changeset
|
48 |
Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; |
3457 | 49 |
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
4089 | 50 |
by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
51 |
qed "le_imp_power_dvd"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
52 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
53 |
Goal "(1::nat) < i ==> \\<forall>n. i ^ m <= i ^ n --> m <= n"; |
11365 | 54 |
by (induct_tac "m" 1); |
55 |
by Auto_tac; |
|
56 |
by (case_tac "na" 1); |
|
57 |
by Auto_tac; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
58 |
by (subgoal_tac "Suc 1 * 1 <= i * i^n" 1); |
11365 | 59 |
by (Asm_full_simp_tac 1); |
60 |
by (rtac mult_le_mono 1); |
|
61 |
by Auto_tac; |
|
62 |
qed_spec_mp "power_le_imp_le"; |
|
63 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8861
diff
changeset
|
64 |
Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"; |
3457 | 65 |
by (rtac ccontr 1); |
66 |
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1); |
|
67 |
by (etac zero_less_power 1); |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
68 |
by (contr_tac 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
69 |
qed "power_less_imp_less"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
70 |
|
11311 | 71 |
Goal "k^j dvd n --> i<=j --> k^i dvd (n::nat)"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
72 |
by (induct_tac "j" 1); |
11311 | 73 |
by (ALLGOALS (simp_tac (simpset() addsimps [le_Suc_eq]))); |
74 |
by (blast_tac (claset() addSDs [dvd_mult_right]) 1); |
|
75 |
qed_spec_mp "power_le_dvd"; |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
76 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
77 |
Goal "[|i^m dvd i^n; (1::nat) < i|] ==> m <= n"; |
11365 | 78 |
by (rtac power_le_imp_le 1); |
79 |
by (assume_tac 1); |
|
80 |
by (etac dvd_imp_le 1); |
|
81 |
by (Asm_full_simp_tac 1); |
|
82 |
qed "power_dvd_imp_le"; |
|
83 |
||
84 |
||
12196 | 85 |
(*** Logical equivalences for inequalities ***) |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
86 |
|
12196 | 87 |
Goal "(x^n = 0) = (x = (0::nat) & 0<n)"; |
88 |
by (induct_tac "n" 1); |
|
89 |
by Auto_tac; |
|
90 |
qed "power_eq_0_iff"; |
|
91 |
Addsimps [power_eq_0_iff]; |
|
92 |
||
93 |
Goal "(0 < x^n) = (x ~= (0::nat) | n=0)"; |
|
94 |
by (induct_tac "n" 1); |
|
95 |
by Auto_tac; |
|
96 |
qed "zero_less_power_iff"; |
|
97 |
Addsimps [zero_less_power_iff]; |
|
98 |
||
99 |
Goal "(0::nat) <= x^n"; |
|
100 |
by (induct_tac "n" 1); |
|
101 |
by Auto_tac; |
|
102 |
qed "zero_le_power"; |
|
103 |
Addsimps [zero_le_power]; |
|
104 |
||
105 |
||
106 |
(**** Binomial Coefficients, following Andy Gordon and Florian Kammueller ****) |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
107 |
|
5069 | 108 |
Goal "(n choose 0) = 1"; |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
109 |
by (case_tac "n" 1); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
110 |
by (ALLGOALS Asm_simp_tac); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
111 |
qed "binomial_n_0"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
112 |
|
5069 | 113 |
Goal "(0 choose Suc k) = 0"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
114 |
by (Simp_tac 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
115 |
qed "binomial_0_Suc"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
116 |
|
5069 | 117 |
Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
118 |
by (Simp_tac 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
119 |
qed "binomial_Suc_Suc"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
120 |
|
7084 | 121 |
Goal "ALL k. n < k --> (n choose k) = 0"; |
122 |
by (induct_tac "n" 1); |
|
123 |
by Auto_tac; |
|
124 |
by (etac allE 1); |
|
125 |
by (etac mp 1); |
|
126 |
by (arith_tac 1); |
|
127 |
qed_spec_mp "binomial_eq_0"; |
|
128 |
||
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
129 |
Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
130 |
Delsimps [binomial_0, binomial_Suc]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
131 |
|
5069 | 132 |
Goal "(n choose n) = 1"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
133 |
by (induct_tac "n" 1); |
7844 | 134 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0]))); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
135 |
qed "binomial_n_n"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
136 |
Addsimps [binomial_n_n]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
137 |
|
5069 | 138 |
Goal "(Suc n choose n) = Suc n"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
139 |
by (induct_tac "n" 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
140 |
by (ALLGOALS Asm_simp_tac); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
141 |
qed "binomial_Suc_n"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
142 |
Addsimps [binomial_Suc_n]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
143 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
144 |
Goal "(n choose Suc 0) = n"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
145 |
by (induct_tac "n" 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
146 |
by (ALLGOALS Asm_simp_tac); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
147 |
qed "binomial_1"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
148 |
Addsimps [binomial_1]; |
7084 | 149 |
|
150 |
Goal "k <= n --> 0 < (n choose k)"; |
|
151 |
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); |
|
152 |
by (ALLGOALS Asm_simp_tac); |
|
153 |
qed_spec_mp "zero_less_binomial"; |
|
154 |
||
11365 | 155 |
Goal "(n choose k = 0) = (n<k)"; |
156 |
by (safe_tac (claset() addSIs [binomial_eq_0])); |
|
157 |
by (etac contrapos_pp 1); |
|
158 |
by (asm_full_simp_tac (simpset() addsimps [zero_less_binomial]) 1); |
|
159 |
qed "binomial_eq_0_iff"; |
|
160 |
||
161 |
Goal "(0 < n choose k) = (k<=n)"; |
|
162 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, |
|
163 |
binomial_eq_0_iff RS sym]) 1); |
|
164 |
qed "zero_less_binomial_iff"; |
|
165 |
||
7084 | 166 |
(*Might be more useful if re-oriented*) |
167 |
Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"; |
|
168 |
by (induct_tac "n" 1); |
|
169 |
by (simp_tac (simpset() addsimps [binomial_0]) 1); |
|
170 |
by (Clarify_tac 1); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
171 |
by (case_tac "k" 1); |
7084 | 172 |
by (auto_tac (claset(), |
173 |
simpset() addsimps [add_mult_distrib, add_mult_distrib2, |
|
174 |
le_Suc_eq, binomial_eq_0])); |
|
175 |
qed_spec_mp "Suc_times_binomial_eq"; |
|
176 |
||
11365 | 177 |
(*This is the well-known version, but it's harder to use because of the |
178 |
need to reason about division.*) |
|
7084 | 179 |
Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; |
13451 | 180 |
by (asm_simp_tac (simpset() |
181 |
addsimps [Suc_times_binomial_eq, div_mult_self_is_m, zero_less_Suc] |
|
182 |
delsimps [mult_Suc, mult_Suc_right]) 1); |
|
7084 | 183 |
qed "binomial_Suc_Suc_eq_times"; |
184 |
||
11365 | 185 |
(*Another version, with -1 instead of Suc.*) |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
186 |
Goal "[|k <= n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
187 |
by (cut_inst_tac [("n","n - 1"),("k","k - 1")] Suc_times_binomial_eq 1); |
11365 | 188 |
by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
189 |
by Auto_tac; |
|
190 |
qed "times_binomial_minus1_eq"; |
|
191 |