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
```