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