# 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 \ 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 \ b ^ y) = (x \ 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 \ b ^ Suc n" and xnonneg: "(0::'a::{ordered_semidom,recpower}) \ a"