src/HOL/Parity.thy
changeset 29803 c56a5571f60a
parent 29654 24e73987bfe2
child 30056 0a35bee25c20
     1.1 --- a/src/HOL/Parity.thy	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/Parity.thy	Thu Feb 05 11:34:42 2009 +0100
     1.3 @@ -291,6 +291,40 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 +lemma power_mono_even: fixes x y :: "'a :: {recpower, ordered_idom}"
     1.8 +  assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>"
     1.9 +  shows "x^n \<le> y^n"
    1.10 +proof -
    1.11 +  have "0 \<le> \<bar>x\<bar>" by auto
    1.12 +  with `\<bar>x\<bar> \<le> \<bar>y\<bar>`
    1.13 +  have "\<bar>x\<bar>^n \<le> \<bar>y\<bar>^n" by (rule power_mono)
    1.14 +  thus ?thesis unfolding power_even_abs[OF `even n`] .
    1.15 +qed
    1.16 +
    1.17 +lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
    1.18 +
    1.19 +lemma power_mono_odd: fixes x y :: "'a :: {recpower, ordered_idom}"
    1.20 +  assumes "odd n" and "x \<le> y"
    1.21 +  shows "x^n \<le> y^n"
    1.22 +proof (cases "y < 0")
    1.23 +  case True with `x \<le> y` have "-y \<le> -x" and "0 \<le> -y" by auto
    1.24 +  hence "(-y)^n \<le> (-x)^n" by (rule power_mono)
    1.25 +  thus ?thesis unfolding power_minus_odd[OF `odd n`] by auto
    1.26 +next
    1.27 +  case False
    1.28 +  show ?thesis
    1.29 +  proof (cases "x < 0")
    1.30 +    case True hence "n \<noteq> 0" and "x \<le> 0" using `odd n`[THEN odd_pos] by auto
    1.31 +    hence "x^n \<le> 0" unfolding power_le_zero_eq using `odd n` by auto
    1.32 +    moreover
    1.33 +    from `\<not> y < 0` have "0 \<le> y" by auto
    1.34 +    hence "0 \<le> y^n" by auto
    1.35 +    ultimately show ?thesis by auto
    1.36 +  next
    1.37 +    case False hence "0 \<le> x" by auto
    1.38 +    with `x \<le> y` show ?thesis using power_mono by auto
    1.39 +  qed
    1.40 +qed
    1.41  
    1.42  subsection {* General Lemmas About Division *}
    1.43  
    1.44 @@ -405,8 +439,6 @@
    1.45  
    1.46  subsection {* Miscellaneous *}
    1.47  
    1.48 -lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
    1.49 -
    1.50  lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger
    1.51  lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger
    1.52  lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"  by presburger