src/HOL/Power.thy
 changeset 25874 14819a95cf75 parent 25836 f7771e4f7064 child 28131 3130d7b3149d
```     1.1 --- a/src/HOL/Power.thy	Wed Jan 09 10:56:35 2008 +0100
1.2 +++ b/src/HOL/Power.thy	Wed Jan 09 19:23:36 2008 +0100
1.3 @@ -45,20 +45,20 @@
1.4  lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)"
1.5    by (induct n) (simp_all add: power_Suc mult_ac)
1.6
1.7 -lemma zero_less_power:
1.8 +lemma zero_less_power[simp]:
1.9       "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
1.10  apply (induct "n")
1.11  apply (simp_all add: power_Suc zero_less_one mult_pos_pos)
1.12  done
1.13
1.14 -lemma zero_le_power:
1.15 +lemma zero_le_power[simp]:
1.16       "0 \<le> (a::'a::{ordered_semidom,recpower}) ==> 0 \<le> a^n"
1.18  apply (erule disjE)
1.19 -apply (simp_all add: zero_less_power zero_less_one power_0_left)
1.20 +apply (simp_all add: zero_less_one power_0_left)
1.21  done
1.22
1.23 -lemma one_le_power:
1.24 +lemma one_le_power[simp]:
1.25       "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
1.26  apply (induct "n")
1.28 @@ -80,7 +80,7 @@
1.29    finally show ?thesis by simp
1.30  qed
1.31
1.32 -lemma one_less_power:
1.33 +lemma one_less_power[simp]:
1.34    "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n"
1.35  by (cases n, simp_all add: power_gt1_lemma power_Suc)
1.36
1.37 @@ -128,14 +128,14 @@
1.38       "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
1.39  apply (induct "n")
1.41 -apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
1.42 +apply (auto intro: mult_mono order_trans [of 0 a b])
1.43  done
1.44
1.45  lemma power_strict_mono [rule_format]:
1.46       "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
1.47        ==> 0 < n --> a^n < b^n"
1.48  apply (induct "n")
1.49 -apply (auto simp add: mult_strict_mono zero_le_power power_Suc
1.50 +apply (auto simp add: mult_strict_mono power_Suc
1.51                        order_le_less_trans [of 0 a b])
1.52  done
1.53
1.54 @@ -225,7 +225,7 @@
1.55  apply (rename_tac m)
1.56  apply (subgoal_tac "a * a^m < 1 * a^n", simp)
1.57  apply (rule mult_strict_mono)
1.58 -apply (auto simp add: zero_le_power zero_less_one order_less_imp_le)
1.59 +apply (auto simp add: zero_less_one order_less_imp_le)
1.60  done
1.61
1.62  text{*Proof resembles that of @{text power_strict_decreasing}*}
1.63 @@ -238,7 +238,7 @@
1.64  apply (rename_tac m)
1.65  apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
1.66  apply (rule mult_mono)
1.67 -apply (auto simp add: zero_le_power zero_le_one)
1.68 +apply (auto simp add: zero_le_one)
1.69  done
1.70
1.71  lemma power_Suc_less_one:
1.72 @@ -255,7 +255,7 @@
1.73  apply (rename_tac m)
1.74  apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
1.75  apply (rule mult_mono)
1.76 -apply (auto simp add: order_trans [OF zero_le_one] zero_le_power)
1.77 +apply (auto simp add: order_trans [OF zero_le_one])
1.78  done
1.79
1.80  text{*Lemma for @{text power_strict_increasing}*}
1.81 @@ -273,8 +273,7 @@
1.82  apply (rename_tac m)
1.83  apply (subgoal_tac "1 * a^n < a * a^m", simp)
1.84  apply (rule mult_strict_mono)
1.85 -apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power
1.86 -                 order_less_imp_le)
1.87 +apply (auto simp add: order_less_trans [OF zero_less_one] order_less_imp_le)
1.88  done
1.89
1.90  lemma power_increasing_iff [simp]:
```