src/HOL/Power.thy
changeset 15066 d2f2b908e0a4
parent 15004 44ac09ba7213
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Power.thy	Mon Jul 19 18:21:26 2004 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Jul 20 14:22:49 2004 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  theory Power = Divides:
     1.6  
     1.7 -subsection{*Powers for Arbitrary (Semi)Rings*}
     1.8 +subsection{*Powers for Arbitrary Semirings*}
     1.9  
    1.10  axclass recpower \<subseteq> comm_semiring_1_cancel, power
    1.11    power_0 [simp]: "a ^ 0       = 1"
    1.12 @@ -270,6 +270,14 @@
    1.13                   order_less_imp_le)
    1.14  done
    1.15  
    1.16 +lemma power_increasing_iff [simp]: 
    1.17 +     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
    1.18 +  by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) 
    1.19 +
    1.20 +lemma power_strict_increasing_iff [simp]:
    1.21 +     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
    1.22 +  by (blast intro: power_less_imp_less_exp power_strict_increasing) 
    1.23 +
    1.24  lemma power_le_imp_le_base:
    1.25    assumes le: "a ^ Suc n \<le> b ^ Suc n"
    1.26        and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"