# HG changeset patch
# User paulson
# Date 1090326169 -7200
# Node ID d2f2b908e0a4d8e4e1854b741747b083de18d7bf
# Parent  9feac0b7f935006673314c818c6ee913a7dedecd
two new results

diff -r 9feac0b7f935 -r d2f2b908e0a4 src/HOL/Power.thy
--- 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"