New theory "Power" of exponentiation (and binomial coefficients)
authorpaulson
Tue Jun 03 10:56:04 1997 +0200 (1997-06-03)
changeset 33900c7625196d95
parent 3389 3150eba724a1
child 3391 5e45dd3b64e9
New theory "Power" of exponentiation (and binomial coefficients)
src/HOL/IsaMakefile
src/HOL/Power.ML
src/HOL/Power.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Jun 03 10:53:58 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 03 10:56:04 1997 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
     1.6  	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
     1.7 -	Divides Sexp Univ List RelPow Option
     1.8 +	Divides Power Sexp Univ List RelPow Option
     1.9  
    1.10  PROVERS = hypsubst.ML classical.ML blast.ML \
    1.11  	simplifier.ML splitter.ML nat_transitive.ML 
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Power.ML	Tue Jun 03 10:56:04 1997 +0200
     2.3 @@ -0,0 +1,92 @@
     2.4 +(*  Title:      HOL/Power.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1997  University of Cambridge
     2.8 +
     2.9 +The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
    2.10 +Also binomial coefficents
    2.11 +*)
    2.12 +
    2.13 +
    2.14 +open Power;
    2.15 +
    2.16 +(*** Simple laws about Power ***)
    2.17 +
    2.18 +goal thy "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
    2.19 +by (induct_tac "k" 1);
    2.20 +by (ALLGOALS (asm_simp_tac (!simpset addsimps mult_ac)));
    2.21 +qed "power_add";
    2.22 +
    2.23 +goal thy "!!i::nat. i ^ (j*k) = (i^j) ^ k";
    2.24 +by (induct_tac "k" 1);
    2.25 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [power_add])));
    2.26 +qed "power_mult";
    2.27 +
    2.28 +goal thy "!! i. 0 < i ==> 0 < i^n";
    2.29 +by (induct_tac "n" 1);
    2.30 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [zero_less_mult_iff])));
    2.31 +qed "zero_less_power";
    2.32 +
    2.33 +goalw thy [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
    2.34 +be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
    2.35 +by (asm_simp_tac (!simpset addsimps [power_add]) 1);
    2.36 +by (Blast_tac 1);
    2.37 +qed "le_imp_power_dvd";
    2.38 +
    2.39 +goal thy "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
    2.40 +br ccontr 1;
    2.41 +bd (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1;
    2.42 +be zero_less_power 1;
    2.43 +by (contr_tac 1);
    2.44 +qed "power_less_imp_less";
    2.45 +
    2.46 +goal thy "!!n. k^j dvd n --> i<j --> k^i dvd n";
    2.47 +by (induct_tac "j" 1);
    2.48 +by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq])));
    2.49 +by (stac mult_commute 1);
    2.50 +by (blast_tac (!claset addSDs [dvd_mult_left]) 1);
    2.51 +qed_spec_mp "power_less_dvd";
    2.52 +
    2.53 +
    2.54 +(*** Binomial Coefficients, following Andy Gordon and Florian Kammüller ***)
    2.55 +
    2.56 +goal thy "(n choose 0) = 1";
    2.57 +by (exhaust_tac "n" 1);
    2.58 +by (ALLGOALS Asm_simp_tac);
    2.59 +qed "binomial_n_0";
    2.60 +
    2.61 +goal thy "(0 choose Suc k) = 0";
    2.62 +by (Simp_tac 1);
    2.63 +qed "binomial_0_Suc";
    2.64 +
    2.65 +goal thy "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
    2.66 +by (Simp_tac 1);
    2.67 +qed "binomial_Suc_Suc";
    2.68 +
    2.69 +Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
    2.70 +Delsimps [binomial_0, binomial_Suc];
    2.71 +
    2.72 +
    2.73 +goal thy "!k. n<k --> (n choose k) = 0";
    2.74 +by (induct_tac "n" 1);
    2.75 +by (ALLGOALS (rtac allI THEN' exhaust_tac "k"));
    2.76 +by (ALLGOALS Asm_simp_tac);
    2.77 +qed_spec_mp "less_imp_binomial_eq_0";
    2.78 +
    2.79 +goal thy "(n choose n) = 1";
    2.80 +by (induct_tac "n" 1);
    2.81 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_imp_binomial_eq_0])));
    2.82 +qed "binomial_n_n";
    2.83 +Addsimps [binomial_n_n];
    2.84 +
    2.85 +goal thy "(Suc n choose n) = Suc n";
    2.86 +by (induct_tac "n" 1);
    2.87 +by (ALLGOALS Asm_simp_tac);
    2.88 +qed "binomial_Suc_n";
    2.89 +Addsimps [binomial_Suc_n];
    2.90 +
    2.91 +goal thy "(n choose 1) = n";
    2.92 +by (induct_tac "n" 1);
    2.93 +by (ALLGOALS Asm_simp_tac);
    2.94 +qed "binomial_1";
    2.95 +Addsimps [binomial_1];
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Power.thy	Tue Jun 03 10:56:04 1997 +0200
     3.3 @@ -0,0 +1,25 @@
     3.4 +(*  Title:      HOL/Power.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1997  University of Cambridge
     3.8 +
     3.9 +The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
    3.10 +Also binomial coefficents
    3.11 +*)
    3.12 +
    3.13 +Power = Divides + 
    3.14 +consts
    3.15 +  binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
    3.16 +
    3.17 +primrec "op ^" nat
    3.18 +  "p ^ 0 = 1"
    3.19 +  "p ^ (Suc n) = (p::nat) * (p ^ n)"
    3.20 +  
    3.21 +primrec "binomial" nat
    3.22 +  binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
    3.23 +
    3.24 +  binomial_Suc "(Suc n choose k) =
    3.25 +                (if k = 0 then 1 else (n choose pred k) + (n choose k))"
    3.26 +
    3.27 +end
    3.28 +