src/HOL/Power.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9637 47d39a31eb2f
child 11311 5a659c406465
permissions -rw-r--r--
improved theory reference in comment
paulson@3390
     1
(*  Title:      HOL/Power.ML
paulson@3390
     2
    ID:         $Id$
paulson@3390
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3390
     4
    Copyright   1997  University of Cambridge
paulson@3390
     5
paulson@3390
     6
The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
paulson@3390
     7
Also binomial coefficents
paulson@3390
     8
*)
paulson@3390
     9
paulson@3390
    10
(*** Simple laws about Power ***)
paulson@3390
    11
wenzelm@5069
    12
Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
paulson@3390
    13
by (induct_tac "k" 1);
wenzelm@4089
    14
by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
paulson@3390
    15
qed "power_add";
paulson@3390
    16
wenzelm@5069
    17
Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k";
paulson@3390
    18
by (induct_tac "k" 1);
wenzelm@4089
    19
by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
paulson@3390
    20
qed "power_mult";
paulson@3390
    21
paulson@8935
    22
Goal "!!i::nat. 0 < i ==> 0 < i^n";
paulson@3390
    23
by (induct_tac "n" 1);
paulson@8935
    24
by (ALLGOALS Asm_simp_tac);
paulson@3390
    25
qed "zero_less_power";
paulson@8861
    26
Addsimps [zero_less_power];
paulson@8861
    27
paulson@8861
    28
Goal "!!i::nat. 1 <= i ==> 1 <= i^n";
paulson@8861
    29
by (induct_tac "n" 1);
paulson@8861
    30
by Auto_tac;
paulson@8861
    31
qed "one_le_power";
paulson@8861
    32
Addsimps [one_le_power];
paulson@3390
    33
paulson@8935
    34
Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
paulson@3457
    35
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
wenzelm@4089
    36
by (asm_simp_tac (simpset() addsimps [power_add]) 1);
paulson@3390
    37
qed "le_imp_power_dvd";
paulson@3390
    38
paulson@8935
    39
Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
paulson@3457
    40
by (rtac ccontr 1);
paulson@3457
    41
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
paulson@3457
    42
by (etac zero_less_power 1);
paulson@3390
    43
by (contr_tac 1);
paulson@3390
    44
qed "power_less_imp_less";
paulson@3390
    45
paulson@6865
    46
Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
paulson@3390
    47
by (induct_tac "j" 1);
wenzelm@4089
    48
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
paulson@3390
    49
by (stac mult_commute 1);
wenzelm@4089
    50
by (blast_tac (claset() addSDs [dvd_mult_left]) 1);
paulson@3390
    51
qed_spec_mp "power_less_dvd";
paulson@3390
    52
paulson@3390
    53
wenzelm@3396
    54
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
paulson@3390
    55
wenzelm@5069
    56
Goal "(n choose 0) = 1";
wenzelm@8442
    57
by (case_tac "n" 1);
paulson@3390
    58
by (ALLGOALS Asm_simp_tac);
paulson@3390
    59
qed "binomial_n_0";
paulson@3390
    60
wenzelm@5069
    61
Goal "(0 choose Suc k) = 0";
paulson@3390
    62
by (Simp_tac 1);
paulson@3390
    63
qed "binomial_0_Suc";
paulson@3390
    64
wenzelm@5069
    65
Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
paulson@3390
    66
by (Simp_tac 1);
paulson@3390
    67
qed "binomial_Suc_Suc";
paulson@3390
    68
paulson@7084
    69
Goal "ALL k. n < k --> (n choose k) = 0";
paulson@7084
    70
by (induct_tac "n" 1);
paulson@7084
    71
by Auto_tac;
paulson@7084
    72
by (etac allE 1);
paulson@7084
    73
by (etac mp 1);
paulson@7084
    74
by (arith_tac 1);
paulson@7084
    75
qed_spec_mp "binomial_eq_0";
paulson@7084
    76
paulson@3390
    77
Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
paulson@3390
    78
Delsimps [binomial_0, binomial_Suc];
paulson@3390
    79
wenzelm@5069
    80
Goal "(n choose n) = 1";
paulson@3390
    81
by (induct_tac "n" 1);
paulson@7844
    82
by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
paulson@3390
    83
qed "binomial_n_n";
paulson@3390
    84
Addsimps [binomial_n_n];
paulson@3390
    85
wenzelm@5069
    86
Goal "(Suc n choose n) = Suc n";
paulson@3390
    87
by (induct_tac "n" 1);
paulson@3390
    88
by (ALLGOALS Asm_simp_tac);
paulson@3390
    89
qed "binomial_Suc_n";
paulson@3390
    90
Addsimps [binomial_Suc_n];
paulson@3390
    91
wenzelm@5069
    92
Goal "(n choose 1) = n";
paulson@3390
    93
by (induct_tac "n" 1);
paulson@3390
    94
by (ALLGOALS Asm_simp_tac);
paulson@3390
    95
qed "binomial_1";
paulson@3390
    96
Addsimps [binomial_1];
paulson@7084
    97
paulson@7084
    98
Goal "k <= n --> 0 < (n choose k)";
paulson@7084
    99
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
paulson@7084
   100
by (ALLGOALS Asm_simp_tac);
paulson@7084
   101
qed_spec_mp "zero_less_binomial";
paulson@7084
   102
paulson@7084
   103
(*Might be more useful if re-oriented*)
paulson@7084
   104
Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k";
paulson@7084
   105
by (induct_tac "n" 1);
paulson@7084
   106
by (simp_tac (simpset() addsimps [binomial_0]) 1);
paulson@7084
   107
by (Clarify_tac 1);
wenzelm@8442
   108
by (case_tac "k" 1);
paulson@7084
   109
by (auto_tac (claset(),
paulson@7084
   110
	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
paulson@7084
   111
				  le_Suc_eq, binomial_eq_0]));
paulson@7084
   112
qed_spec_mp "Suc_times_binomial_eq";
paulson@7084
   113
paulson@7084
   114
Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
paulson@7084
   115
by (asm_simp_tac
wenzelm@9424
   116
    (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
paulson@7084
   117
				  div_mult_self_is_m]) 1);
paulson@7084
   118
qed "binomial_Suc_Suc_eq_times";
paulson@7084
   119