author haftmann Sat Nov 18 00:20:20 2006 +0100 (2006-11-18) changeset 21413 0951647209f2 parent 21412 a259061ad0b0 child 21414 4cb808163adc
moved dvd stuff to theory Divides
 src/HOL/Power.thy file | annotate | diff | revisions
```     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.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.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.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
```