author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9637  47d39a31eb2f 
child 11311  5a659c406465 
permissions  rwrr 
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 

28 
Goal "!!i::nat. 1 <= i ==> 1 <= i^n"; 

29 
by (induct_tac "n" 1); 

30 
by Auto_tac; 

31 
qed "one_le_power"; 

32 
Addsimps [one_le_power]; 

3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

33 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8861
diff
changeset

34 
Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; 
3457  35 
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); 
4089  36 
by (asm_simp_tac (simpset() addsimps [power_add]) 1); 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

37 
qed "le_imp_power_dvd"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

38 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8861
diff
changeset

39 
Goal "!!i::nat. [ 0 < i; i^m < i^n ] ==> m < n"; 
3457  40 
by (rtac ccontr 1); 
41 
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1); 

42 
by (etac zero_less_power 1); 

3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

43 
by (contr_tac 1); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

44 
qed "power_less_imp_less"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

45 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
5143
diff
changeset

46 
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

47 
by (induct_tac "j" 1); 
4089  48 
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq]))); 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

49 
by (stac mult_commute 1); 
4089  50 
by (blast_tac (claset() addSDs [dvd_mult_left]) 1); 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

51 
qed_spec_mp "power_less_dvd"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

52 

0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

53 

3396  54 
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***) 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

55 

5069  56 
Goal "(n choose 0) = 1"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

57 
by (case_tac "n" 1); 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

58 
by (ALLGOALS Asm_simp_tac); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

59 
qed "binomial_n_0"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

60 

5069  61 
Goal "(0 choose Suc k) = 0"; 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

62 
by (Simp_tac 1); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

63 
qed "binomial_0_Suc"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

64 

5069  65 
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

66 
by (Simp_tac 1); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

67 
qed "binomial_Suc_Suc"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

68 

7084  69 
Goal "ALL k. n < k > (n choose k) = 0"; 
70 
by (induct_tac "n" 1); 

71 
by Auto_tac; 

72 
by (etac allE 1); 

73 
by (etac mp 1); 

74 
by (arith_tac 1); 

75 
qed_spec_mp "binomial_eq_0"; 

76 

3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

77 
Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc]; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

78 
Delsimps [binomial_0, binomial_Suc]; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

79 

5069  80 
Goal "(n choose n) = 1"; 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

81 
by (induct_tac "n" 1); 
7844  82 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0]))); 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

83 
qed "binomial_n_n"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

84 
Addsimps [binomial_n_n]; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

85 

5069  86 
Goal "(Suc n choose n) = Suc n"; 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

87 
by (induct_tac "n" 1); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

88 
by (ALLGOALS Asm_simp_tac); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

89 
qed "binomial_Suc_n"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

90 
Addsimps [binomial_Suc_n]; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

91 

5069  92 
Goal "(n choose 1) = n"; 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

93 
by (induct_tac "n" 1); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

94 
by (ALLGOALS Asm_simp_tac); 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

95 
qed "binomial_1"; 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

96 
Addsimps [binomial_1]; 
7084  97 

98 
Goal "k <= n > 0 < (n choose k)"; 

99 
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); 

100 
by (ALLGOALS Asm_simp_tac); 

101 
qed_spec_mp "zero_less_binomial"; 

102 

103 
(*Might be more useful if reoriented*) 

104 
Goal "ALL k. k <= n > Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"; 

105 
by (induct_tac "n" 1); 

106 
by (simp_tac (simpset() addsimps [binomial_0]) 1); 

107 
by (Clarify_tac 1); 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

108 
by (case_tac "k" 1); 
7084  109 
by (auto_tac (claset(), 
110 
simpset() addsimps [add_mult_distrib, add_mult_distrib2, 

111 
le_Suc_eq, binomial_eq_0])); 

112 
qed_spec_mp "Suc_times_binomial_eq"; 

113 

114 
Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; 

115 
by (asm_simp_tac 

9424  116 
(simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
7084  117 
div_mult_self_is_m]) 1); 
118 
qed "binomial_Suc_Suc_eq_times"; 

119 