src/HOL/Power.thy
 changeset 15066 d2f2b908e0a4 parent 15004 44ac09ba7213 child 15131 c69542757a4d
```--- 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"```