src/HOL/Power.ML
 author berghofe Tue, 30 May 2000 18:02:49 +0200 changeset 9001 93af64f54bf2 parent 8935 548901d05a0e child 9424 234ef8652cae permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
```
(*  Title:      HOL/Power.ML
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
Also binomial coefficents
*)

(*** Simple laws about Power ***)

Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
by (induct_tac "k" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));

Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k";
by (induct_tac "k" 1);
qed "power_mult";

Goal "!!i::nat. 0 < i ==> 0 < i^n";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "zero_less_power";

Goal "!!i::nat. 1 <= i ==> 1 <= i^n";
by (induct_tac "n" 1);
by Auto_tac;
qed "one_le_power";

Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
by (Blast_tac 1);
qed "le_imp_power_dvd";

Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
by (rtac ccontr 1);
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
by (etac zero_less_power 1);
by (contr_tac 1);
qed "power_less_imp_less";

Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
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 Kammueller ***)

Goal "(n choose 0) = 1";
by (case_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "binomial_n_0";

Goal "(0 choose Suc k) = 0";
by (Simp_tac 1);
qed "binomial_0_Suc";

Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
by (Simp_tac 1);
qed "binomial_Suc_Suc";

Goal "ALL k. n < k --> (n choose k) = 0";
by (induct_tac "n" 1);
by Auto_tac;
by (etac allE 1);
by (etac mp 1);
by (arith_tac 1);
qed_spec_mp "binomial_eq_0";

Delsimps [binomial_0, binomial_Suc];

Goal "(n choose n) = 1";
by (induct_tac "n" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
qed "binomial_n_n";

Goal "(Suc n choose n) = Suc n";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "binomial_Suc_n";

Goal "(n choose 1) = n";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "binomial_1";

Goal "k <= n --> 0 < (n choose k)";
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "zero_less_binomial";

(*Might be more useful if re-oriented*)
Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k";
by (induct_tac "n" 1);
by (simp_tac (simpset() addsimps [binomial_0]) 1);
by (Clarify_tac 1);
by (case_tac "k" 1);
by (auto_tac (claset(),