src/HOL/Power.ML
author paulson
Mon Jun 23 10:42:03 1997 +0200 (1997-06-23)
changeset 3457 a8ab7c64817c
parent 3396 aa74c71c3982
child 4089 96fba19bcbe2
permissions -rw-r--r--
Ran expandshort
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
paulson@3390
    11
open Power;
paulson@3390
    12
paulson@3390
    13
(*** Simple laws about Power ***)
paulson@3390
    14
paulson@3390
    15
goal thy "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
paulson@3390
    16
by (induct_tac "k" 1);
paulson@3390
    17
by (ALLGOALS (asm_simp_tac (!simpset addsimps mult_ac)));
paulson@3390
    18
qed "power_add";
paulson@3390
    19
paulson@3390
    20
goal thy "!!i::nat. i ^ (j*k) = (i^j) ^ k";
paulson@3390
    21
by (induct_tac "k" 1);
paulson@3390
    22
by (ALLGOALS (asm_simp_tac (!simpset addsimps [power_add])));
paulson@3390
    23
qed "power_mult";
paulson@3390
    24
paulson@3390
    25
goal thy "!! i. 0 < i ==> 0 < i^n";
paulson@3390
    26
by (induct_tac "n" 1);
paulson@3390
    27
by (ALLGOALS (asm_simp_tac (!simpset addsimps [zero_less_mult_iff])));
paulson@3390
    28
qed "zero_less_power";
paulson@3390
    29
paulson@3390
    30
goalw thy [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
paulson@3457
    31
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
paulson@3390
    32
by (asm_simp_tac (!simpset addsimps [power_add]) 1);
paulson@3390
    33
by (Blast_tac 1);
paulson@3390
    34
qed "le_imp_power_dvd";
paulson@3390
    35
paulson@3390
    36
goal thy "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
paulson@3457
    37
by (rtac ccontr 1);
paulson@3457
    38
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
paulson@3457
    39
by (etac zero_less_power 1);
paulson@3390
    40
by (contr_tac 1);
paulson@3390
    41
qed "power_less_imp_less";
paulson@3390
    42
paulson@3390
    43
goal thy "!!n. k^j dvd n --> i<j --> k^i dvd n";
paulson@3390
    44
by (induct_tac "j" 1);
paulson@3390
    45
by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq])));
paulson@3390
    46
by (stac mult_commute 1);
paulson@3390
    47
by (blast_tac (!claset addSDs [dvd_mult_left]) 1);
paulson@3390
    48
qed_spec_mp "power_less_dvd";
paulson@3390
    49
paulson@3390
    50
wenzelm@3396
    51
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
paulson@3390
    52
paulson@3390
    53
goal thy "(n choose 0) = 1";
paulson@3390
    54
by (exhaust_tac "n" 1);
paulson@3390
    55
by (ALLGOALS Asm_simp_tac);
paulson@3390
    56
qed "binomial_n_0";
paulson@3390
    57
paulson@3390
    58
goal thy "(0 choose Suc k) = 0";
paulson@3390
    59
by (Simp_tac 1);
paulson@3390
    60
qed "binomial_0_Suc";
paulson@3390
    61
paulson@3390
    62
goal thy "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
paulson@3390
    63
by (Simp_tac 1);
paulson@3390
    64
qed "binomial_Suc_Suc";
paulson@3390
    65
paulson@3390
    66
Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
paulson@3390
    67
Delsimps [binomial_0, binomial_Suc];
paulson@3390
    68
paulson@3390
    69
paulson@3390
    70
goal thy "!k. n<k --> (n choose k) = 0";
paulson@3390
    71
by (induct_tac "n" 1);
paulson@3390
    72
by (ALLGOALS (rtac allI THEN' exhaust_tac "k"));
paulson@3390
    73
by (ALLGOALS Asm_simp_tac);
paulson@3390
    74
qed_spec_mp "less_imp_binomial_eq_0";
paulson@3390
    75
paulson@3390
    76
goal thy "(n choose n) = 1";
paulson@3390
    77
by (induct_tac "n" 1);
paulson@3390
    78
by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_imp_binomial_eq_0])));
paulson@3390
    79
qed "binomial_n_n";
paulson@3390
    80
Addsimps [binomial_n_n];
paulson@3390
    81
paulson@3390
    82
goal thy "(Suc n choose n) = Suc n";
paulson@3390
    83
by (induct_tac "n" 1);
paulson@3390
    84
by (ALLGOALS Asm_simp_tac);
paulson@3390
    85
qed "binomial_Suc_n";
paulson@3390
    86
Addsimps [binomial_Suc_n];
paulson@3390
    87
paulson@3390
    88
goal thy "(n choose 1) = n";
paulson@3390
    89
by (induct_tac "n" 1);
paulson@3390
    90
by (ALLGOALS Asm_simp_tac);
paulson@3390
    91
qed "binomial_1";
paulson@3390
    92
Addsimps [binomial_1];