--- a/src/HOL/Power.thy Mon Jul 19 18:21:26 2004 +0200
+++ b/src/HOL/Power.thy Tue Jul 20 14:22:49 2004 +0200
@@ -9,7 +9,7 @@
theory Power = Divides:
-subsection{*Powers for Arbitrary (Semi)Rings*}
+subsection{*Powers for Arbitrary Semirings*}
axclass recpower \<subseteq> comm_semiring_1_cancel, power
power_0 [simp]: "a ^ 0 = 1"
@@ -270,6 +270,14 @@
order_less_imp_le)
done
+lemma power_increasing_iff [simp]:
+ "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
+ by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le)
+
+lemma power_strict_increasing_iff [simp]:
+ "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
+ by (blast intro: power_less_imp_less_exp power_strict_increasing)
+
lemma power_le_imp_le_base:
assumes le: "a ^ Suc n \<le> b ^ Suc n"
and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"