new lemmas concerning powers and #mmm
authorpaulson
Thu, 04 May 2000 15:16:18 +0200
changeset 8792 59a4b5e6a591
parent 8791 50b650d19641
child 8793 a735b1e74f3a
new lemmas concerning powers and #mmm
src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Thu May 04 15:15:37 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Thu May 04 15:16:18 2000 +0200
@@ -373,7 +373,15 @@
 Goal "(p::nat) ^ #0 = #1";
 by (simp_tac numeral_ss 1);
 qed "power_zero";
-Addsimps [power_zero];
+
+Goal "(p::nat) ^ #1 = p";
+by (simp_tac numeral_ss 1);
+qed "power_one";
+Addsimps [power_zero, power_one];
+
+Goal "(p::nat) ^ #2 = p*p";
+by (simp_tac numeral_ss 1);
+qed "power_two";
 
 val binomial_zero = rename_numerals thy binomial_0;
 val binomial_Suc' = rename_numerals thy binomial_Suc;
@@ -383,6 +391,7 @@
 Addsimps (map (rename_numerals thy) 
 	  [binomial_n_0, binomial_zero, binomial_1]);
 
+Addsimps [rename_numerals thy card_Pow];
 
 (*** Comparisons involving 0 ***)