added simp attributes
authornipkow
Wed Jan 09 19:23:36 2008 +0100 (2008-01-09)
changeset 2587414819a95cf75
parent 25873 b213fd2924be
child 25875 536dfdc25e0a
added simp attributes
src/HOL/Power.thy
     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.17  apply (simp add: order_le_less)
    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.27  apply (simp_all add: power_Suc)
    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.40  apply (simp_all add: power_Suc)
    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]: