src/HOL/Parity.thy
changeset 35028 108662d50512
parent 33358 3495dbba0da2
child 35043 07dbdf60d5ad
     1.1 --- a/src/HOL/Parity.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Parity.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -218,7 +218,7 @@
     1.4    done
     1.5  
     1.6  lemma zero_le_even_power: "even n ==>
     1.7 -    0 <= (x::'a::{ordered_ring_strict,monoid_mult}) ^ n"
     1.8 +    0 <= (x::'a::{linlinordered_ring_strict,monoid_mult}) ^ n"
     1.9    apply (simp add: even_nat_equiv_def2)
    1.10    apply (erule exE)
    1.11    apply (erule ssubst)
    1.12 @@ -227,12 +227,12 @@
    1.13    done
    1.14  
    1.15  lemma zero_le_odd_power: "odd n ==>
    1.16 -    (0 <= (x::'a::{ordered_idom}) ^ n) = (0 <= x)"
    1.17 +    (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
    1.18  apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
    1.19  apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
    1.20  done
    1.21  
    1.22 -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{ordered_idom}) ^ n) =
    1.23 +lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
    1.24      (even n | (odd n & 0 <= x))"
    1.25    apply auto
    1.26    apply (subst zero_le_odd_power [symmetric])
    1.27 @@ -240,19 +240,19 @@
    1.28    apply (erule zero_le_even_power)
    1.29    done
    1.30  
    1.31 -lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{ordered_idom}) ^ n) =
    1.32 +lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{linordered_idom}) ^ n) =
    1.33      (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
    1.34  
    1.35    unfolding order_less_le zero_le_power_eq by auto
    1.36  
    1.37 -lemma power_less_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n < 0) =
    1.38 +lemma power_less_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n < 0) =
    1.39      (odd n & x < 0)"
    1.40    apply (subst linorder_not_le [symmetric])+
    1.41    apply (subst zero_le_power_eq)
    1.42    apply auto
    1.43    done
    1.44  
    1.45 -lemma power_le_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n <= 0) =
    1.46 +lemma power_le_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n <= 0) =
    1.47      (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
    1.48    apply (subst linorder_not_less [symmetric])+
    1.49    apply (subst zero_less_power_eq)
    1.50 @@ -260,7 +260,7 @@
    1.51    done
    1.52  
    1.53  lemma power_even_abs: "even n ==>
    1.54 -    (abs (x::'a::{ordered_idom}))^n = x^n"
    1.55 +    (abs (x::'a::{linordered_idom}))^n = x^n"
    1.56    apply (subst power_abs [symmetric])
    1.57    apply (simp add: zero_le_even_power)
    1.58    done
    1.59 @@ -280,7 +280,7 @@
    1.60    apply simp
    1.61    done
    1.62  
    1.63 -lemma power_mono_even: fixes x y :: "'a :: {ordered_idom}"
    1.64 +lemma power_mono_even: fixes x y :: "'a :: {linordered_idom}"
    1.65    assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>"
    1.66    shows "x^n \<le> y^n"
    1.67  proof -
    1.68 @@ -292,7 +292,7 @@
    1.69  
    1.70  lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
    1.71  
    1.72 -lemma power_mono_odd: fixes x y :: "'a :: {ordered_idom}"
    1.73 +lemma power_mono_odd: fixes x y :: "'a :: {linordered_idom}"
    1.74    assumes "odd n" and "x \<le> y"
    1.75    shows "x^n \<le> y^n"
    1.76  proof (cases "y < 0")
    1.77 @@ -372,11 +372,11 @@
    1.78  subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
    1.79  
    1.80  lemma even_power_le_0_imp_0:
    1.81 -    "a ^ (2*k) \<le> (0::'a::{ordered_idom}) ==> a=0"
    1.82 +    "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
    1.83    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
    1.84  
    1.85  lemma zero_le_power_iff[presburger]:
    1.86 -  "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom}) | even n)"
    1.87 +  "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
    1.88  proof cases
    1.89    assume even: "even n"
    1.90    then obtain k where "n = 2*k"