src/HOL/Power.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7084 4af4f4d8035c
child 7844 6462cb4dfdc2
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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 "0 < i ==> 0 < i^n";
    23 by (induct_tac "n" 1);
    24 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
    25 qed "zero_less_power";
    26 
    27 Goalw [dvd_def] "!!(m::nat) (i::nat). m<=n ==> i^m dvd i^n";
    28 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    29 by (asm_simp_tac (simpset() addsimps [power_add]) 1);
    30 by (Blast_tac 1);
    31 qed "le_imp_power_dvd";
    32 
    33 Goal "[| 0 < i; i^m < i^n |] ==> m<n";
    34 by (rtac ccontr 1);
    35 by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
    36 by (etac zero_less_power 1);
    37 by (contr_tac 1);
    38 qed "power_less_imp_less";
    39 
    40 Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
    41 by (induct_tac "j" 1);
    42 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    43 by (stac mult_commute 1);
    44 by (blast_tac (claset() addSDs [dvd_mult_left]) 1);
    45 qed_spec_mp "power_less_dvd";
    46 
    47 
    48 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
    49 
    50 Goal "(n choose 0) = 1";
    51 by (exhaust_tac "n" 1);
    52 by (ALLGOALS Asm_simp_tac);
    53 qed "binomial_n_0";
    54 
    55 Goal "(0 choose Suc k) = 0";
    56 by (Simp_tac 1);
    57 qed "binomial_0_Suc";
    58 
    59 Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
    60 by (Simp_tac 1);
    61 qed "binomial_Suc_Suc";
    62 
    63 Goal "ALL k. n < k --> (n choose k) = 0";
    64 by (induct_tac "n" 1);
    65 by Auto_tac;
    66 by (etac allE 1);
    67 by (etac mp 1);
    68 by (arith_tac 1);
    69 qed_spec_mp "binomial_eq_0";
    70 
    71 Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
    72 Delsimps [binomial_0, binomial_Suc];
    73 
    74 
    75 Goal "!k. n<k --> (n choose k) = 0";
    76 by (induct_tac "n" 1);
    77 by (ALLGOALS (rtac allI THEN' exhaust_tac "k"));
    78 by (ALLGOALS Asm_simp_tac);
    79 qed_spec_mp "less_imp_binomial_eq_0";
    80 
    81 Goal "(n choose n) = 1";
    82 by (induct_tac "n" 1);
    83 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_imp_binomial_eq_0])));
    84 qed "binomial_n_n";
    85 Addsimps [binomial_n_n];
    86 
    87 Goal "(Suc n choose n) = Suc n";
    88 by (induct_tac "n" 1);
    89 by (ALLGOALS Asm_simp_tac);
    90 qed "binomial_Suc_n";
    91 Addsimps [binomial_Suc_n];
    92 
    93 Goal "(n choose 1) = n";
    94 by (induct_tac "n" 1);
    95 by (ALLGOALS Asm_simp_tac);
    96 qed "binomial_1";
    97 Addsimps [binomial_1];
    98 
    99 Goal "k <= n --> 0 < (n choose k)";
   100 by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
   101 by (ALLGOALS Asm_simp_tac);
   102 qed_spec_mp "zero_less_binomial";
   103 
   104 (*Might be more useful if re-oriented*)
   105 Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k";
   106 by (induct_tac "n" 1);
   107 by (simp_tac (simpset() addsimps [binomial_0]) 1);
   108 by (Clarify_tac 1);
   109 by (exhaust_tac "k" 1);
   110 by (auto_tac (claset(),
   111 	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
   112 				  le_Suc_eq, binomial_eq_0]));
   113 qed_spec_mp "Suc_times_binomial_eq";
   114 
   115 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
   116 by (asm_simp_tac
   117     (simpset_of Nat.thy addsimps [Suc_times_binomial_eq, 
   118 				  div_mult_self_is_m]) 1);
   119 qed "binomial_Suc_Suc_eq_times";
   120