src/HOL/Power.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5143 b94cd208f073
child 6865 5577ffe4c2f1
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (*  Title:      HOL/Power.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
     7 Also binomial coefficents
     8 *)
     9 
    10 
    11 open Power;
    12 
    13 (*** Simple laws about Power ***)
    14 
    15 Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
    16 by (induct_tac "k" 1);
    17 by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
    18 qed "power_add";
    19 
    20 Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k";
    21 by (induct_tac "k" 1);
    22 by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
    23 qed "power_mult";
    24 
    25 Goal "0 < i ==> 0 < i^n";
    26 by (induct_tac "n" 1);
    27 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
    28 qed "zero_less_power";
    29 
    30 Goalw [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
    31 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    32 by (asm_simp_tac (simpset() addsimps [power_add]) 1);
    33 by (Blast_tac 1);
    34 qed "le_imp_power_dvd";
    35 
    36 Goal "[| 0 < i; i^m < i^n |] ==> m<n";
    37 by (rtac ccontr 1);
    38 by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
    39 by (etac zero_less_power 1);
    40 by (contr_tac 1);
    41 qed "power_less_imp_less";
    42 
    43 Goal "k^j dvd n --> i<j --> k^i dvd n";
    44 by (induct_tac "j" 1);
    45 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    46 by (stac mult_commute 1);
    47 by (blast_tac (claset() addSDs [dvd_mult_left]) 1);
    48 qed_spec_mp "power_less_dvd";
    49 
    50 
    51 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
    52 
    53 Goal "(n choose 0) = 1";
    54 by (exhaust_tac "n" 1);
    55 by (ALLGOALS Asm_simp_tac);
    56 qed "binomial_n_0";
    57 
    58 Goal "(0 choose Suc k) = 0";
    59 by (Simp_tac 1);
    60 qed "binomial_0_Suc";
    61 
    62 Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
    63 by (Simp_tac 1);
    64 qed "binomial_Suc_Suc";
    65 
    66 Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
    67 Delsimps [binomial_0, binomial_Suc];
    68 
    69 
    70 Goal "!k. n<k --> (n choose k) = 0";
    71 by (induct_tac "n" 1);
    72 by (ALLGOALS (rtac allI THEN' exhaust_tac "k"));
    73 by (ALLGOALS Asm_simp_tac);
    74 qed_spec_mp "less_imp_binomial_eq_0";
    75 
    76 Goal "(n choose n) = 1";
    77 by (induct_tac "n" 1);
    78 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_imp_binomial_eq_0])));
    79 qed "binomial_n_n";
    80 Addsimps [binomial_n_n];
    81 
    82 Goal "(Suc n choose n) = Suc n";
    83 by (induct_tac "n" 1);
    84 by (ALLGOALS Asm_simp_tac);
    85 qed "binomial_Suc_n";
    86 Addsimps [binomial_Suc_n];
    87 
    88 Goal "(n choose 1) = n";
    89 by (induct_tac "n" 1);
    90 by (ALLGOALS Asm_simp_tac);
    91 qed "binomial_1";
    92 Addsimps [binomial_1];