author  haftmann 
Tue, 14 Oct 2014 08:23:23 +0200  
changeset 58680  6b2fa479945f 
parent 58679  33c90658448a 
child 58681  a478a0742a8e 
permissions  rwrr 
41959  1 
(* Title: HOL/Parity.thy 
2 
Author: Jeremy Avigad 

3 
Author: Jacques D. Fleuriot 

21256  4 
*) 
5 

6 
header {* Even and Odd for int and nat *} 

7 

8 
theory Parity 

30738  9 
imports Main 
21256  10 
begin 
11 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

12 
subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *} 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

13 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

14 
lemma two_dvd_Suc_Suc_iff [simp]: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

15 
"2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

16 
using dvd_add_triv_right_iff [of 2 n] by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

17 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

18 
lemma two_dvd_Suc_iff: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

19 
"2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

20 
by (induct n) auto 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

21 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

22 
lemma two_dvd_diff_iff: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

23 
fixes k l :: int 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

24 
shows "2 dvd k  l \<longleftrightarrow> 2 dvd k + l" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

25 
using dvd_add_times_triv_right_iff [of 2 "k  l" l] by (simp add: ac_simps) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

26 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

27 
lemma two_dvd_abs_add_iff: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

28 
fixes k l :: int 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

29 
shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

30 
by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

31 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

32 
lemma two_dvd_add_abs_iff: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

33 
fixes k l :: int 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

34 
shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

35 
using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

36 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

37 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

38 
subsection {* Ring structures with parity *} 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

39 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

40 
class semiring_parity = semiring_dvd + semiring_numeral + 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

41 
assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

42 
assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

43 
assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b" 
58680  44 
assumes not_dvd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1" 
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

45 
begin 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

46 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

47 
lemma two_dvd_plus_one_iff [simp]: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

48 
"2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

49 
by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

50 

58680  51 
lemma not_two_dvdE [elim?]: 
52 
assumes "\<not> 2 dvd a" 

53 
obtains b where "a = 2 * b + 1" 

54 
proof  

55 
from assms obtain b where *: "a = b + 1" 

56 
by (blast dest: not_dvd_ex_decrement) 

57 
with assms have "2 dvd b + 2" by simp 

58 
then have "2 dvd b" by simp 

59 
then obtain c where "b = 2 * c" .. 

60 
with * have "a = 2 * c + 1" by simp 

61 
with that show thesis . 

62 
qed 

63 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

64 
end 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

65 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

66 
instance nat :: semiring_parity 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

67 
proof 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

68 
show "\<not> (2 :: nat) dvd 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

69 
by (rule notI, erule dvdE) simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

70 
next 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

71 
fix m n :: nat 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

72 
assume "\<not> 2 dvd m" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

73 
moreover assume "\<not> 2 dvd n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

74 
ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

75 
by (simp add: two_dvd_Suc_iff) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

76 
then have "2 dvd Suc m + Suc n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

77 
by (blast intro: dvd_add) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

78 
also have "Suc m + Suc n = m + n + 2" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

79 
by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

80 
finally show "2 dvd m + n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

81 
using dvd_add_triv_right_iff [of 2 "m + n"] by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

82 
next 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

83 
fix m n :: nat 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

84 
assume *: "2 dvd m * n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

85 
show "2 dvd m \<or> 2 dvd n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

86 
proof (rule disjCI) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

87 
assume "\<not> 2 dvd n" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

88 
then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

89 
then obtain r where "Suc n = 2 * r" .. 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

90 
moreover from * obtain s where "m * n = 2 * s" .. 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

91 
then have "2 * s + m = m * Suc n" by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

92 
ultimately have " 2 * s + m = 2 * (m * r)" by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

93 
then have "m = 2 * (m * r  s)" by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

94 
then show "2 dvd m" .. 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

95 
qed 
58680  96 
next 
97 
fix n :: nat 

98 
assume "\<not> 2 dvd n" 

99 
then show "\<exists>m. n = m + 1" 

100 
by (cases n) simp_all 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

101 
qed 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

102 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

103 
class ring_parity = comm_ring_1 + semiring_parity 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

104 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

105 
instance int :: ring_parity 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

106 
proof 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

107 
show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

108 
fix k l :: int 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

109 
assume "\<not> 2 dvd k" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

110 
moreover assume "\<not> 2 dvd l" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

111 
ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

112 
by (auto simp add: dvd_int_unfold_dvd_nat intro: not_dvd_not_dvd_dvd_add) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

113 
then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

114 
by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

115 
then show "2 dvd k + l" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

116 
by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff) 
58680  117 
next 
118 
fix k l :: int 

119 
assume "2 dvd k * l" 

120 
then show "2 dvd k \<or> 2 dvd l" 

121 
by (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib) 

122 
next 

123 
fix k :: int 

124 
have "k = (k  1) + 1" by simp 

125 
then show "\<exists>l. k = l + 1" .. 

126 
qed 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

127 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

128 
context semiring_div_parity 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

129 
begin 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

130 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

131 
subclass semiring_parity 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

132 
proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

133 
fix a b c 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

134 
show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

135 
by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

136 
next 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

137 
fix a b c 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

138 
assume "(b + c) mod a = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

139 
with mod_add_eq [of b c a] 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

140 
have "(b mod a + c mod a) mod a = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

141 
by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

142 
moreover assume "b mod a = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

143 
ultimately show "c mod a = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

144 
by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

145 
next 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

146 
show "1 mod 2 = 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

147 
by (fact one_mod_two_eq_one) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

148 
next 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

149 
fix a b 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

150 
assume "a mod 2 = 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

151 
moreover assume "b mod 2 = 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

152 
ultimately show "(a + b) mod 2 = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

153 
using mod_add_eq [of a b 2] by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

154 
next 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

155 
fix a b 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

156 
assume "(a * b) mod 2 = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

157 
then have "(a mod 2) * (b mod 2) = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

158 
by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2]) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

159 
then show "a mod 2 = 0 \<or> b mod 2 = 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

160 
by (rule divisors_zero) 
58680  161 
next 
162 
fix a 

163 
assume "a mod 2 = 1" 

164 
then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp 

165 
then show "\<exists>b. a = b + 1" .. 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

166 
qed 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

167 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

168 
end 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

169 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

170 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

171 
subsection {* Dedicated @{text even}/@{text odd} predicate *} 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

172 

58680  173 
subsubsection {* Properties *} 
174 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

175 
context semiring_parity 
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

176 
begin 
21256  177 

54228  178 
definition even :: "'a \<Rightarrow> bool" 
179 
where 

58645  180 
[algebra]: "even a \<longleftrightarrow> 2 dvd a" 
54228  181 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

182 
abbreviation odd :: "'a \<Rightarrow> bool" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

183 
where 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

184 
"odd a \<equiv> \<not> even a" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

185 

58680  186 
lemma odd_dvdE [elim?]: 
187 
assumes "odd a" 

188 
obtains b where "a = 2 * b + 1" 

189 
proof  

190 
from assms have "\<not> 2 dvd a" by (simp add: even_def) 

191 
then show thesis using that by (rule not_two_dvdE) 

192 
qed 

193 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

194 
lemma even_times_iff [simp, presburger, algebra]: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

195 
"even (a * b) \<longleftrightarrow> even a \<or> even b" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

196 
by (auto simp add: even_def dest: two_is_prime) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

197 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

198 
lemma even_zero [simp]: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

199 
"even 0" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

200 
by (simp add: even_def) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

201 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

202 
lemma odd_one [simp]: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

203 
"odd 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

204 
by (simp add: even_def) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

205 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

206 
lemma even_numeral [simp]: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

207 
"even (numeral (Num.Bit0 n))" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

208 
proof  
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

209 
have "even (2 * numeral n)" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

210 
unfolding even_times_iff by (simp add: even_def) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

211 
then have "even (numeral n + numeral n)" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

212 
unfolding mult_2 . 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

213 
then show ?thesis 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

214 
unfolding numeral.simps . 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

215 
qed 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

216 

398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

217 
lemma odd_numeral [simp]: 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

218 
"odd (numeral (Num.Bit1 n))" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

219 
proof 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

220 
assume "even (numeral (num.Bit1 n))" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

221 
then have "even (numeral n + numeral n + 1)" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

222 
unfolding numeral.simps . 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

223 
then have "even (2 * numeral n + 1)" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

224 
unfolding mult_2 . 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

225 
then have "2 dvd numeral n * 2 + 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

226 
unfolding even_def by (simp add: ac_simps) 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

227 
with dvd_add_times_triv_left_iff [of 2 "numeral n" 1] 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

228 
have "2 dvd 1" 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

229 
by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

230 
then show False by simp 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

231 
qed 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

232 

58680  233 
lemma even_add [simp]: 
234 
"even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)" 

235 
by (auto simp add: even_def dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add) 

236 

237 
lemma odd_add [simp]: 

238 
"odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))" 

239 
by simp 

240 

241 
lemma even_power [simp, presburger]: 

242 
"even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0" 

243 
by (induct n) auto 

244 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

245 
end 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

246 

58679  247 
context ring_parity 
248 
begin 

249 

250 
lemma even_minus [simp, presburger, algebra]: 

251 
"even ( a) \<longleftrightarrow> even a" 

252 
by (simp add: even_def) 

253 

58680  254 
lemma even_diff [simp]: 
255 
"even (a  b) \<longleftrightarrow> even (a + b)" 

256 
using even_add [of a " b"] by simp 

257 

58679  258 
end 
259 

58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

260 
context semiring_div_parity 
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

261 
begin 
58645  262 

263 
lemma even_iff_mod_2_eq_zero [presburger]: 

264 
"even a \<longleftrightarrow> a mod 2 = 0" 

54228  265 
by (simp add: even_def dvd_eq_mod_eq_0) 
266 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

267 
end 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

268 

58680  269 

270 
subsubsection {* Particularities for @{typ nat}/@{typ int} *} 

271 

58679  272 
lemma even_int_iff: 
273 
"even (int n) \<longleftrightarrow> even n" 

274 
by (simp add: even_def dvd_int_iff) 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
31718
diff
changeset

275 

58679  276 
declare transfer_morphism_int_nat [transfer add return: 
277 
even_int_iff 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
31718
diff
changeset

278 
] 
21256  279 

58680  280 

281 
subsubsection {* Tools setup *} 

282 

58679  283 
lemma [presburger]: 
284 
"even n \<longleftrightarrow> even (int n)" 

285 
using even_int_iff [of n] by simp 

25600  286 

58680  287 
lemma [presburger]: 
288 
"even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b" 

289 
by auto 

21256  290 

291 

58680  292 
subsubsection {* Legacy cruft *} 
293 

294 
lemma even_plus_even: 

295 
"even (x::int) ==> even y ==> even (x + y)" 

296 
by simp 

297 

298 
lemma odd_plus_odd: 

299 
"odd (x::int) ==> odd y ==> even (x + y)" 

300 
by simp 

301 

302 
lemma even_sum_nat: 

303 
"even ((x::nat) + y) = ((even x & even y)  (odd x & odd y))" 

304 
by auto 

21256  305 

58680  306 
lemma odd_pow: 
307 
"odd x ==> odd((x::int)^n)" 

308 
by simp 

309 

310 
lemma even_equiv_def: 

311 
"even (x::int) = (EX y. x = 2 * y)" 

312 
by presburger 

313 

314 

315 
subsubsection {* Equivalent definitions *} 

316 

317 
lemma two_times_even_div_two: 

318 
"even (x::int) ==> 2 * (x div 2) = x" 

319 
by presburger 

21256  320 

31148  321 
lemma two_times_odd_div_two_plus_one: 
322 
"odd (x::int) ==> 2 * (x div 2) + 1 = x" 

58680  323 
by presburger 
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset

324 

21256  325 

58680  326 
subsubsection {* even and odd for nats *} 
21256  327 

328 
lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)" 

58679  329 
by (simp add: even_int_iff [symmetric]) 
21256  330 

58680  331 
lemma even_difference_nat [simp,presburger,algebra]: 
332 
"even ((x::nat)  y) = (x < y  (even x & even y)  (odd x & odd y))" 

333 
by presburger 

21256  334 

58680  335 
lemma even_Suc [simp ,presburger, algebra]: 
336 
"even (Suc x) = odd x" 

337 
by presburger 

21256  338 

31148  339 
lemma even_power_nat[simp,presburger,algebra]: 
340 
"even ((x::nat)^y) = (even x & 0 < y)" 

58680  341 
by simp 
21256  342 

343 

58680  344 
subsubsection {* Equivalent definitions *} 
21256  345 

346 
lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" 

31148  347 
by presburger 
21256  348 

349 
lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" 

23522  350 
by presburger 
21256  351 

21263  352 
lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" 
31148  353 
by presburger 
21256  354 

355 
lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" 

31148  356 
by presburger 
21256  357 

21263  358 
lemma even_nat_div_two_times_two: "even (x::nat) ==> 
23522  359 
Suc (Suc 0) * (x div Suc (Suc 0)) = x" by presburger 
21256  360 

21263  361 
lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> 
23522  362 
Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger 
21256  363 

364 
lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))" 

58680  365 
by presburger 
21256  366 

25600  367 

58680  368 
subsubsection {* Parity and powers *} 
21256  369 

54228  370 
lemma (in comm_ring_1) neg_power_if: 
371 
"( a) ^ n = (if even n then (a ^ n) else  (a ^ n))" 

372 
by (induct n) simp_all 

21256  373 

54228  374 
lemma (in comm_ring_1) 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54228
diff
changeset

375 
shows neg_one_even_power [simp]: "even n \<Longrightarrow> ( 1) ^ n = 1" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54228
diff
changeset

376 
and neg_one_odd_power [simp]: "odd n \<Longrightarrow> ( 1) ^ n =  1" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54228
diff
changeset

377 
by (simp_all add: neg_power_if) 
21256  378 

21263  379 
lemma zero_le_even_power: "even n ==> 
35631
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

380 
0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n" 
58680  381 
apply (simp add: even_def) 
382 
apply (erule dvdE) 

21256  383 
apply (erule ssubst) 
58680  384 
unfolding mult.commute [of 2] 
385 
unfolding power_mult power2_eq_square 

21256  386 
apply (rule zero_le_square) 
387 
done 

388 

21263  389 
lemma zero_le_odd_power: "odd n ==> 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

390 
(0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" 
35216  391 
apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff) 
36722  392 
apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square) 
30056  393 
done 
21256  394 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

395 
lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = 
21256  396 
(even n  (odd n & 0 <= x))" 
397 
apply auto 

21263  398 
apply (subst zero_le_odd_power [symmetric]) 
21256  399 
apply assumption+ 
400 
apply (erule zero_le_even_power) 

21263  401 
done 
21256  402 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

403 
lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{linordered_idom}) ^ n) = 
21256  404 
(n = 0  (even n & x ~= 0)  (odd n & 0 < x))" 
27668  405 
unfolding order_less_le zero_le_power_eq by auto 
21256  406 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

407 
lemma power_less_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n < 0) = 
27668  408 
(odd n & x < 0)" 
21263  409 
apply (subst linorder_not_le [symmetric])+ 
21256  410 
apply (subst zero_le_power_eq) 
411 
apply auto 

21263  412 
done 
21256  413 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

414 
lemma power_le_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n <= 0) = 
21256  415 
(n ~= 0 & ((odd n & x <= 0)  (even n & x = 0)))" 
21263  416 
apply (subst linorder_not_less [symmetric])+ 
21256  417 
apply (subst zero_less_power_eq) 
418 
apply auto 

21263  419 
done 
21256  420 

21263  421 
lemma power_even_abs: "even n ==> 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

422 
(abs (x::'a::{linordered_idom}))^n = x^n" 
21263  423 
apply (subst power_abs [symmetric]) 
21256  424 
apply (simp add: zero_le_even_power) 
21263  425 
done 
21256  426 

21263  427 
lemma power_minus_even [simp]: "even n ==> 
31017  428 
( x)^n = (x^n::'a::{comm_ring_1})" 
21256  429 
apply (subst power_minus) 
430 
apply simp 

21263  431 
done 
21256  432 

21263  433 
lemma power_minus_odd [simp]: "odd n ==> 
31017  434 
( x)^n =  (x^n::'a::{comm_ring_1})" 
21256  435 
apply (subst power_minus) 
436 
apply simp 

21263  437 
done 
21256  438 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

439 
lemma power_mono_even: fixes x y :: "'a :: {linordered_idom}" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

440 
assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

441 
shows "x^n \<le> y^n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

442 
proof  
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

443 
have "0 \<le> \<bar>x\<bar>" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

444 
with `\<bar>x\<bar> \<le> \<bar>y\<bar>` 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

445 
have "\<bar>x\<bar>^n \<le> \<bar>y\<bar>^n" by (rule power_mono) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

446 
thus ?thesis unfolding power_even_abs[OF `even n`] . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

447 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

448 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

449 
lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

450 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

451 
lemma power_mono_odd: fixes x y :: "'a :: {linordered_idom}" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

452 
assumes "odd n" and "x \<le> y" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

453 
shows "x^n \<le> y^n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

454 
proof (cases "y < 0") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

455 
case True with `x \<le> y` have "y \<le> x" and "0 \<le> y" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

456 
hence "(y)^n \<le> (x)^n" by (rule power_mono) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

457 
thus ?thesis unfolding power_minus_odd[OF `odd n`] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

458 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

459 
case False 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

460 
show ?thesis 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

461 
proof (cases "x < 0") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

462 
case True hence "n \<noteq> 0" and "x \<le> 0" using `odd n`[THEN odd_pos] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

463 
hence "x^n \<le> 0" unfolding power_le_zero_eq using `odd n` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

464 
moreover 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

465 
from `\<not> y < 0` have "0 \<le> y" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

466 
hence "0 \<le> y^n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

467 
ultimately show ?thesis by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

468 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

469 
case False hence "0 \<le> x" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

470 
with `x \<le> y` show ?thesis using power_mono by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

471 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29654
diff
changeset

472 
qed 
21263  473 

25600  474 

58680  475 
subsubsection {* More Even/Odd Results *} 
25600  476 

27668  477 
lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger 
478 
lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger 

25600  479 

27668  480 
lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger 
25600  481 

482 
lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)" 

27668  483 
by presburger 
25600  484 

27668  485 
lemma even_num_iff: "0 < n ==> even n = (~ even(n  1 :: nat))" by presburger 
486 
lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger 

25600  487 

27668  488 
lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n  1) div 2)" by presburger 
25600  489 

490 
lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n  1) div 2)" 

27668  491 
by presburger 
25600  492 

21263  493 
text {* Simplify, when the exponent is a numeral *} 
21256  494 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45607
diff
changeset

495 
lemmas zero_le_power_eq_numeral [simp] = 
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

496 
zero_le_power_eq [of _ "numeral w"] for w 
21256  497 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45607
diff
changeset

498 
lemmas zero_less_power_eq_numeral [simp] = 
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

499 
zero_less_power_eq [of _ "numeral w"] for w 
21256  500 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45607
diff
changeset

501 
lemmas power_le_zero_eq_numeral [simp] = 
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

502 
power_le_zero_eq [of _ "numeral w"] for w 
21256  503 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45607
diff
changeset

504 
lemmas power_less_zero_eq_numeral [simp] = 
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

505 
power_less_zero_eq [of _ "numeral w"] for w 
21256  506 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45607
diff
changeset

507 
lemmas zero_less_power_nat_eq_numeral [simp] = 
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

508 
nat_zero_less_power_iff [of _ "numeral w"] for w 
21256  509 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

510 
lemmas power_eq_0_iff_numeral [simp] = 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

511 
power_eq_0_iff [of _ "numeral w"] for w 
21256  512 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

513 
lemmas power_even_abs_numeral [simp] = 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

514 
power_even_abs [of "numeral w" _] for w 
21256  515 

516 

58680  517 
subsubsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} 
21256  518 

23522  519 
lemma zero_le_power_iff[presburger]: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33358
diff
changeset

520 
"(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom})  even n)" 
21256  521 
proof cases 
522 
assume even: "even n" 

58680  523 
then have "2 dvd n" by (simp add: even_def) 
524 
then obtain k where "n = 2 * k" .. 

21263  525 
thus ?thesis by (simp add: zero_le_even_power even) 
21256  526 
next 
527 
assume odd: "odd n" 

528 
then obtain k where "n = Suc(2*k)" 

529 
by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

530 
moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0" 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

531 
by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

532 
ultimately show ?thesis 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

533 
by (auto simp add: zero_le_mult_iff zero_le_even_power) 
21263  534 
qed 
535 

21256  536 

58680  537 
subsubsection {* Miscellaneous *} 
21256  538 

23522  539 
lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger 
540 
lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger 

541 
lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" by presburger 

542 
lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger 

21256  543 

23522  544 
lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger 
21263  545 
lemma even_nat_plus_one_div_two: "even (x::nat) ==> 
23522  546 
(Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger 
21256  547 

21263  548 
lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> 
23522  549 
(Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger 
21256  550 

551 
end 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset

552 