src/HOL/Parity.thy
 changeset 54227 63b441f49645 parent 47225 650318981557 child 54228 229282d53781
```     1.1 --- a/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
1.2 +++ b/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
1.3 @@ -11,11 +11,14 @@
1.4
1.5  class even_odd =
1.6    fixes even :: "'a \<Rightarrow> bool"
1.7 +begin
1.8
1.9 -abbreviation
1.10 -  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
1.11 +abbreviation odd :: "'a \<Rightarrow> bool"
1.12 +where
1.13    "odd x \<equiv> \<not> even x"
1.14
1.15 +end
1.16 +
1.17  instantiation nat and int  :: even_odd
1.18  begin
1.19
1.20 @@ -52,7 +55,7 @@
1.21    unfolding even_def by simp
1.22
1.23  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
1.24 -declare even_def[of "neg_numeral v", simp] for v
1.25 +declare even_def [of "neg_numeral v", simp] for v
1.26
1.27  lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
1.28    unfolding even_nat_def by simp
1.29 @@ -62,13 +65,6 @@
1.30
1.31  subsection {* Even and odd are mutually exclusive *}
1.32
1.33 -lemma int_pos_lt_two_imp_zero_or_one:
1.34 -    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
1.35 -  by presburger
1.36 -
1.37 -lemma neq_one_mod_two [simp, presburger]:
1.38 -  "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger
1.39 -
1.40
1.41  subsection {* Behavior under integer arithmetic operations *}
1.42  declare dvd_def[algebra]
1.43 @@ -158,10 +154,6 @@
1.44
1.45  subsection {* Equivalent definitions *}
1.46
1.47 -lemma nat_lt_two_imp_zero_or_one:
1.48 -  "(x::nat) < Suc (Suc 0) ==> x = 0 | x = Suc 0"
1.49 -by presburger
1.50 -
1.51  lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
1.52  by presburger
1.53
1.54 @@ -244,7 +236,7 @@
1.55  apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
1.56  done
1.57
1.58 -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
1.59 +lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
1.60      (even n | (odd n & 0 <= x))"
1.61    apply auto
1.62    apply (subst zero_le_odd_power [symmetric])
1.63 @@ -277,9 +269,6 @@
1.65    done
1.66
1.67 -lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
1.68 -  by (induct n) auto
1.69 -
1.70  lemma power_minus_even [simp]: "even n ==>
1.71      (- x)^n = (x^n::'a::{comm_ring_1})"
1.72    apply (subst power_minus)
1.73 @@ -336,13 +325,6 @@
1.74
1.75  lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger
1.76
1.77 -lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +
1.78 -    (a mod c + Suc 0 mod c) div c"
1.79 -  apply (subgoal_tac "Suc a = a + Suc 0")
1.80 -  apply (erule ssubst)
1.81 -  apply (rule div_add1_eq, simp)
1.82 -  done
1.83 -
1.84  lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
1.85
1.86  lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
1.87 @@ -359,31 +341,29 @@
1.88  text {* Simplify, when the exponent is a numeral *}
1.89
1.90  lemmas zero_le_power_eq_numeral [simp] =
1.91 -    zero_le_power_eq [of _ "numeral w"] for w
1.92 +  zero_le_power_eq [of _ "numeral w"] for w
1.93
1.94  lemmas zero_less_power_eq_numeral [simp] =
1.95 -    zero_less_power_eq [of _ "numeral w"] for w
1.96 +  zero_less_power_eq [of _ "numeral w"] for w
1.97
1.98  lemmas power_le_zero_eq_numeral [simp] =
1.99 -    power_le_zero_eq [of _ "numeral w"] for w
1.100 +  power_le_zero_eq [of _ "numeral w"] for w
1.101
1.102  lemmas power_less_zero_eq_numeral [simp] =
1.103 -    power_less_zero_eq [of _ "numeral w"] for w
1.104 +  power_less_zero_eq [of _ "numeral w"] for w
1.105
1.106  lemmas zero_less_power_nat_eq_numeral [simp] =
1.107 -    zero_less_power_nat_eq [of _ "numeral w"] for w
1.108 +  nat_zero_less_power_iff [of _ "numeral w"] for w
1.109
1.110 -lemmas power_eq_0_iff_numeral [simp] = power_eq_0_iff [of _ "numeral w"] for w
1.111 +lemmas power_eq_0_iff_numeral [simp] =
1.112 +  power_eq_0_iff [of _ "numeral w"] for w
1.113
1.114 -lemmas power_even_abs_numeral [simp] = power_even_abs [of "numeral w" _] for w
1.115 +lemmas power_even_abs_numeral [simp] =
1.116 +  power_even_abs [of "numeral w" _] for w
1.117
1.118
1.119  subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
1.120
1.121 -lemma even_power_le_0_imp_0:
1.122 -    "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
1.123 -  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
1.124 -
1.125  lemma zero_le_power_iff[presburger]:
1.126    "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
1.127  proof cases
1.128 @@ -395,9 +375,10 @@
1.129    assume odd: "odd n"
1.130    then obtain k where "n = Suc(2*k)"
1.131      by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
1.132 -  thus ?thesis
1.133 -    by (auto simp add: zero_le_mult_iff zero_le_even_power
1.134 -             dest!: even_power_le_0_imp_0)
1.135 +  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
1.136 +    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
1.137 +  ultimately show ?thesis
1.138 +    by (auto simp add: zero_le_mult_iff zero_le_even_power)
1.139  qed
1.140
1.141
1.142 @@ -409,7 +390,6 @@
1.143  lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger
1.144
1.145  lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
1.146 -lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
1.147  lemma even_nat_plus_one_div_two: "even (x::nat) ==>
1.148      (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger
1.149
1.150 @@ -417,3 +397,4 @@
1.151      (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger
1.152
1.153  end
1.154 +
```