author | paulson |
Mon, 26 Jul 1999 16:29:59 +0200 | |
changeset 7084 | 4af4f4d8035c |
parent 6865 | 5577ffe4c2f1 |
child 7844 | 6462cb4dfdc2 |
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 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
22 |
Goal "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); |
4089 | 24 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
25 |
qed "zero_less_power"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
26 |
|
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
5143
diff
changeset
|
27 |
Goalw [dvd_def] "!!(m::nat) (i::nat). m<=n ==> i^m dvd i^n"; |
3457 | 28 |
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
4089 | 29 |
by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
30 |
by (Blast_tac 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
31 |
qed "le_imp_power_dvd"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
32 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
33 |
Goal "[| 0 < i; i^m < i^n |] ==> m<n"; |
3457 | 34 |
by (rtac ccontr 1); |
35 |
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1); |
|
36 |
by (etac zero_less_power 1); |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
37 |
by (contr_tac 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
38 |
qed "power_less_imp_less"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
39 |
|
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
5143
diff
changeset
|
40 |
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
|
41 |
by (induct_tac "j" 1); |
4089 | 42 |
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq]))); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
43 |
by (stac mult_commute 1); |
4089 | 44 |
by (blast_tac (claset() addSDs [dvd_mult_left]) 1); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
45 |
qed_spec_mp "power_less_dvd"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
46 |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
47 |
|
3396 | 48 |
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***) |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
49 |
|
5069 | 50 |
Goal "(n choose 0) = 1"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
51 |
by (exhaust_tac "n" 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
52 |
by (ALLGOALS Asm_simp_tac); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
53 |
qed "binomial_n_0"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
54 |
|
5069 | 55 |
Goal "(0 choose Suc k) = 0"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
56 |
by (Simp_tac 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
57 |
qed "binomial_0_Suc"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
58 |
|
5069 | 59 |
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
|
60 |
by (Simp_tac 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
61 |
qed "binomial_Suc_Suc"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
62 |
|
7084 | 63 |
Goal "ALL k. n < k --> (n choose k) = 0"; |
64 |
by (induct_tac "n" 1); |
|
65 |
by Auto_tac; |
|
66 |
by (etac allE 1); |
|
67 |
by (etac mp 1); |
|
68 |
by (arith_tac 1); |
|
69 |
qed_spec_mp "binomial_eq_0"; |
|
70 |
||
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
71 |
Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
72 |
Delsimps [binomial_0, binomial_Suc]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
73 |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
74 |
|
5069 | 75 |
Goal "!k. n<k --> (n choose k) = 0"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
76 |
by (induct_tac "n" 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
77 |
by (ALLGOALS (rtac allI THEN' exhaust_tac "k")); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
78 |
by (ALLGOALS Asm_simp_tac); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
79 |
qed_spec_mp "less_imp_binomial_eq_0"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
80 |
|
5069 | 81 |
Goal "(n choose n) = 1"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
82 |
by (induct_tac "n" 1); |
4089 | 83 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_imp_binomial_eq_0]))); |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
84 |
qed "binomial_n_n"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
85 |
Addsimps [binomial_n_n]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
86 |
|
5069 | 87 |
Goal "(Suc n choose n) = Suc n"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
88 |
by (induct_tac "n" 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
89 |
by (ALLGOALS Asm_simp_tac); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
90 |
qed "binomial_Suc_n"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
91 |
Addsimps [binomial_Suc_n]; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
92 |
|
5069 | 93 |
Goal "(n choose 1) = n"; |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
94 |
by (induct_tac "n" 1); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
95 |
by (ALLGOALS Asm_simp_tac); |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
96 |
qed "binomial_1"; |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
97 |
Addsimps [binomial_1]; |
7084 | 98 |
|
99 |
Goal "k <= n --> 0 < (n choose k)"; |
|
100 |
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); |
|
101 |
by (ALLGOALS Asm_simp_tac); |
|
102 |
qed_spec_mp "zero_less_binomial"; |
|
103 |
||
104 |
(*Might be more useful if re-oriented*) |
|
105 |
Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"; |
|
106 |
by (induct_tac "n" 1); |
|
107 |
by (simp_tac (simpset() addsimps [binomial_0]) 1); |
|
108 |
by (Clarify_tac 1); |
|
109 |
by (exhaust_tac "k" 1); |
|
110 |
by (auto_tac (claset(), |
|
111 |
simpset() addsimps [add_mult_distrib, add_mult_distrib2, |
|
112 |
le_Suc_eq, binomial_eq_0])); |
|
113 |
qed_spec_mp "Suc_times_binomial_eq"; |
|
114 |
||
115 |
Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; |
|
116 |
by (asm_simp_tac |
|
117 |
(simpset_of Nat.thy addsimps [Suc_times_binomial_eq, |
|
118 |
div_mult_self_is_m]) 1); |
|
119 |
qed "binomial_Suc_Suc_eq_times"; |
|
120 |