New theory "Power" of exponentiation (and binomial coefficients)

--- a/src/HOL/IsaMakefile	Tue Jun 03 10:53:58 1997 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 03 10:56:04 1997 +0200
@@ -10,7 +10,7 @@
 
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
-	Divides Sexp Univ List RelPow Option
+	Divides Power Sexp Univ List RelPow Option
 
 PROVERS = hypsubst.ML classical.ML blast.ML \
 	simplifier.ML splitter.ML nat_transitive.ML 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Power.ML	Tue Jun 03 10:56:04 1997 +0200
@@ -0,0 +1,92 @@
+(*  Title:      HOL/Power.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
+Also binomial coefficents
+*)
+
+
+open Power;
+
+(*** Simple laws about Power ***)
+
+goal thy "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
+by (induct_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps mult_ac)));
+qed "power_add";
+
+goal thy "!!i::nat. i ^ (j*k) = (i^j) ^ k";
+by (induct_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [power_add])));
+qed "power_mult";
+
+goal thy "!! i. 0 < i ==> 0 < i^n";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [zero_less_mult_iff])));
+qed "zero_less_power";
+
+goalw thy [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
+be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
+by (asm_simp_tac (!simpset addsimps [power_add]) 1);
+by (Blast_tac 1);
+qed "le_imp_power_dvd";
+
+goal thy "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
+br ccontr 1;
+bd (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1;
+be zero_less_power 1;
+by (contr_tac 1);
+qed "power_less_imp_less";
+
+goal thy "!!n. k^j dvd n --> i<j --> k^i dvd n";
+by (induct_tac "j" 1);
+by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq])));
+by (stac mult_commute 1);
+by (blast_tac (!claset addSDs [dvd_mult_left]) 1);
+qed_spec_mp "power_less_dvd";
+
+
+(*** Binomial Coefficients, following Andy Gordon and Florian Kammüller ***)
+
+goal thy "(n choose 0) = 1";
+by (exhaust_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "binomial_n_0";
+
+goal thy "(0 choose Suc k) = 0";
+by (Simp_tac 1);
+qed "binomial_0_Suc";
+
+goal thy "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
+by (Simp_tac 1);
+qed "binomial_Suc_Suc";
+
+Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
+Delsimps [binomial_0, binomial_Suc];
+
+
+goal thy "!k. n<k --> (n choose k) = 0";
+by (induct_tac "n" 1);
+by (ALLGOALS (rtac allI THEN' exhaust_tac "k"));
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp "less_imp_binomial_eq_0";
+
+goal thy "(n choose n) = 1";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_imp_binomial_eq_0])));
+qed "binomial_n_n";
+Addsimps [binomial_n_n];
+
+goal thy "(Suc n choose n) = Suc n";
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "binomial_Suc_n";
+Addsimps [binomial_Suc_n];
+
+goal thy "(n choose 1) = n";
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "binomial_1";
+Addsimps [binomial_1];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Power.thy	Tue Jun 03 10:56:04 1997 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/Power.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
+Also binomial coefficents
+*)
+
+Power = Divides + 
+consts
+  binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
+
+primrec "op ^" nat
+  "p ^ 0 = 1"
+  "p ^ (Suc n) = (p::nat) * (p ^ n)"
+  
+primrec "binomial" nat
+  binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
+
+  binomial_Suc "(Suc n choose k) =
+                (if k = 0 then 1 else (n choose pred k) + (n choose k))"
+
+end
+