src/HOL/Power.thy
 changeset 62347 2230b7047376 parent 62083 7582b39f51ed child 62366 95c6cf433c91
```     1.1 --- a/src/HOL/Power.thy	Wed Feb 17 21:51:56 2016 +0100
1.2 +++ b/src/HOL/Power.thy	Wed Feb 17 21:51:57 2016 +0100
1.3 @@ -9,19 +9,6 @@
1.4  imports Num Equiv_Relations
1.5  begin
1.6
1.7 -context linordered_ring (* TODO: move *)
1.8 -begin
1.9 -
1.10 -lemma sum_squares_ge_zero:
1.11 -  "0 \<le> x * x + y * y"
1.12 -  by (intro add_nonneg_nonneg zero_le_square)
1.13 -
1.14 -lemma not_sum_squares_lt_zero:
1.15 -  "\<not> x * x + y * y < 0"
1.16 -  by (simp add: not_less sum_squares_ge_zero)
1.17 -
1.18 -end
1.19 -
1.20  subsection \<open>Powers for Arbitrary Monoids\<close>
1.21
1.22  class power = one + times
1.23 @@ -123,6 +110,10 @@
1.24    finally show ?case .
1.25  qed simp
1.26
1.27 +lemma power_minus_mult:
1.28 +  "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
1.29 +  by (simp add: power_commutes split add: nat_diff_split)
1.30 +
1.31  end
1.32
1.33  context comm_monoid_mult
1.34 @@ -584,6 +575,10 @@
1.35    "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
1.36    by (cases n) (simp_all del: power_Suc, rule power_inject_base)
1.37
1.38 +lemma power_eq_iff_eq_base:
1.39 +  "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
1.40 +  using power_eq_imp_eq_base [of a n b] by auto
1.41 +
1.42  lemma power2_le_imp_le:
1.43    "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
1.44    unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
1.45 @@ -596,6 +591,10 @@
1.46    "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
1.47    unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
1.48
1.49 +lemma power_Suc_le_self:
1.50 +  shows "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
1.51 +  using power_decreasing [of 1 "Suc n" a] by simp
1.52 +
1.53  end
1.54
1.55  context linordered_ring_strict
```