src/HOL/Power.thy
changeset 21413 0951647209f2
parent 21199 2d83f93c3580
child 21456 1c2b9df41e98
     1.1 --- a/src/HOL/Power.thy	Sat Nov 18 00:20:19 2006 +0100
     1.2 +++ b/src/HOL/Power.thy	Sat Nov 18 00:20:20 2006 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header{*Exponentiation*}
     1.5  
     1.6  theory Power
     1.7 -imports Divides
     1.8 +imports Nat
     1.9  begin
    1.10  
    1.11  subsection{*Powers for Arbitrary Monoids*}
    1.12 @@ -325,34 +325,22 @@
    1.13  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    1.14  by (insert one_le_power [of i n], simp)
    1.15  
    1.16 -lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
    1.17 -apply (unfold dvd_def)
    1.18 -apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    1.19 -apply (simp add: power_add)
    1.20 -done
    1.21 +lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
    1.22 +by (induct "n", auto)
    1.23  
    1.24  text{*Valid for the naturals, but what if @{text"0<i<1"}?
    1.25  Premises cannot be weakened: consider the case where @{term "i=0"},
    1.26  @{term "m=1"} and @{term "n=0"}.*}
    1.27 -lemma nat_power_less_imp_less: "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"
    1.28 -apply (rule ccontr)
    1.29 -apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD])
    1.30 -apply (erule zero_less_power, auto)
    1.31 -done
    1.32 -
    1.33 -lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
    1.34 -by (induct "n", auto)
    1.35 -
    1.36 -lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
    1.37 -apply (induct "j")
    1.38 -apply (simp_all add: le_Suc_eq)
    1.39 -apply (blast dest!: dvd_mult_right)
    1.40 -done
    1.41 -
    1.42 -lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
    1.43 -apply (rule power_le_imp_le_exp, assumption)
    1.44 -apply (erule dvd_imp_le, simp)
    1.45 -done
    1.46 +lemma nat_power_less_imp_less:
    1.47 +  assumes nonneg: "0 < (i\<Colon>nat)"
    1.48 +  assumes less: "i^m < i^n"
    1.49 +  shows "m < n"
    1.50 +proof (cases "i = 1")
    1.51 +  case True with less power_one [where 'a = nat] show ?thesis by simp
    1.52 +next
    1.53 +  case False with nonneg have "1 < i" by auto
    1.54 +  from power_strict_increasing_iff [OF this] less show ?thesis ..
    1.55 +qed
    1.56  
    1.57  lemma power_diff:
    1.58    assumes nz: "a ~= 0"
    1.59 @@ -408,11 +396,8 @@
    1.60  ML
    1.61  {*
    1.62  val nat_one_le_power = thm"nat_one_le_power";
    1.63 -val le_imp_power_dvd = thm"le_imp_power_dvd";
    1.64  val nat_power_less_imp_less = thm"nat_power_less_imp_less";
    1.65  val nat_zero_less_power_iff = thm"nat_zero_less_power_iff";
    1.66 -val power_le_dvd = thm"power_le_dvd";
    1.67 -val power_dvd_imp_le = thm"power_dvd_imp_le";
    1.68  *}
    1.69  
    1.70  end