--- a/src/HOL/Power.ML Thu Nov 15 15:07:16 2001 +0100
+++ b/src/HOL/Power.ML Thu Nov 15 16:12:49 2001 +0100
@@ -81,8 +81,28 @@
qed "power_dvd_imp_le";
+(*** Logical equivalences for inequalities ***)
-(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
+Goal "(x^n = 0) = (x = (0::nat) & 0<n)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "power_eq_0_iff";
+Addsimps [power_eq_0_iff];
+
+Goal "(0 < x^n) = (x ~= (0::nat) | n=0)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "zero_less_power_iff";
+Addsimps [zero_less_power_iff];
+
+Goal "(0::nat) <= x^n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "zero_le_power";
+Addsimps [zero_le_power];
+
+
+(**** Binomial Coefficients, following Andy Gordon and Florian Kammueller ****)
Goal "(n choose 0) = 1";
by (case_tac "n" 1);