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
     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 (*** Simple laws about Power ***)
    11 
    12 Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
    13 by (induct_tac "k" 1);
    14 by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
    15 qed "power_add";
    16 
    17 Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k";
    18 by (induct_tac "k" 1);
    19 by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
    20 qed "power_mult";
    21 
    22 Goal "!!i::nat. 0 < i ==> 0 < i^n";
    23 by (induct_tac "n" 1);
    24 by (ALLGOALS Asm_simp_tac);
    25 qed "zero_less_power";
    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];
    33 
    34 Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
    35 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    36 by (asm_simp_tac (simpset() addsimps [power_add]) 1);
    37 qed "le_imp_power_dvd";
    38 
    39 Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
    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);
    43 by (contr_tac 1);
    44 qed "power_less_imp_less";
    45 
    46 Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
    47 by (induct_tac "j" 1);
    48 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    49 by (stac mult_commute 1);
    50 by (blast_tac (claset() addSDs [dvd_mult_left]) 1);
    51 qed_spec_mp "power_less_dvd";
    52 
    53 
    54 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
    55 
    56 Goal "(n choose 0) = 1";
    57 by (case_tac "n" 1);
    58 by (ALLGOALS Asm_simp_tac);
    59 qed "binomial_n_0";
    60 
    61 Goal "(0 choose Suc k) = 0";
    62 by (Simp_tac 1);
    63 qed "binomial_0_Suc";
    64 
    65 Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
    66 by (Simp_tac 1);
    67 qed "binomial_Suc_Suc";
    68 
    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 
    77 Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
    78 Delsimps [binomial_0, binomial_Suc];
    79 
    80 Goal "(n choose n) = 1";
    81 by (induct_tac "n" 1);
    82 by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
    83 qed "binomial_n_n";
    84 Addsimps [binomial_n_n];
    85 
    86 Goal "(Suc n choose n) = Suc n";
    87 by (induct_tac "n" 1);
    88 by (ALLGOALS Asm_simp_tac);
    89 qed "binomial_Suc_n";
    90 Addsimps [binomial_Suc_n];
    91 
    92 Goal "(n choose 1) = n";
    93 by (induct_tac "n" 1);
    94 by (ALLGOALS Asm_simp_tac);
    95 qed "binomial_1";
    96 Addsimps [binomial_1];
    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 re-oriented*)
   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);
   108 by (case_tac "k" 1);
   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
   116     (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
   117 				  div_mult_self_is_m]) 1);
   118 qed "binomial_Suc_Suc_eq_times";
   119