author  haftmann 
Thu, 16 Oct 2014 19:26:26 +0200  
changeset 58689  ee5bf401cfa7 
parent 58688  ddd124805260 
child 58690  5c5c14844738 
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 

58687  22 
lemma two_dvd_diff_nat_iff: 
23 
fixes m n :: nat 

24 
shows "2 dvd m  n \<longleftrightarrow> m < n \<or> 2 dvd m + n" 

25 
proof (cases "n \<le> m") 

26 
case True 

27 
then have "m  n + n * 2 = m + n" by simp 

28 
moreover have "2 dvd m  n \<longleftrightarrow> 2 dvd m  n + n * 2" by simp 

29 
ultimately have "2 dvd m  n \<longleftrightarrow> 2 dvd m + n" by (simp only:) 

30 
then show ?thesis by auto 

31 
next 

32 
case False 

33 
then show ?thesis by simp 

34 
qed 

35 

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

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

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

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

39 
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

40 

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

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

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

43 
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

44 
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

45 

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

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

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

48 
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

49 
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

50 

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

51 

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

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

53 

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

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

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

56 
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

57 
assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b" 
58680  58 
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

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

60 

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

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

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

63 
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

64 

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

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

68 
proof  

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

70 
by (blast dest: not_dvd_ex_decrement) 

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

72 
then have "2 dvd b" by simp 

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

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

75 
with that show thesis . 

76 
qed 

77 

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

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

79 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

95 
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

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

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

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

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

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

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

102 
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

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

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

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

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

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

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

109 
qed 
58680  110 
next 
111 
fix n :: nat 

112 
assume "\<not> 2 dvd n" 

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

114 
by (cases n) simp_all 

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

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

116 

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

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

118 

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

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

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

121 
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

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

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

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

125 
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

126 
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

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

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

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

130 
by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff) 
58680  131 
next 
132 
fix k l :: int 

133 
assume "2 dvd k * l" 

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

135 
by (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib) 

136 
next 

137 
fix k :: int 

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

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

140 
qed 

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

141 

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

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

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

144 

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

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

146 
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

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

148 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

172 
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

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

174 
by (rule divisors_zero) 
58680  175 
next 
176 
fix a 

177 
assume "a mod 2 = 1" 

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

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

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

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

181 

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

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

183 

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

184 

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

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

186 

58680  187 
subsubsection {* Properties *} 
188 

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

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

190 
begin 
21256  191 

54228  192 
definition even :: "'a \<Rightarrow> bool" 
193 
where 

58645  194 
[algebra]: "even a \<longleftrightarrow> 2 dvd a" 
54228  195 

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

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

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

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

199 

58681  200 
lemma oddE [elim?]: 
58680  201 
assumes "odd a" 
202 
obtains b where "a = 2 * b + 1" 

203 
proof  

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

205 
then show thesis using that by (rule not_two_dvdE) 

206 
qed 

207 

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

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

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

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

211 

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

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

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

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

215 

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

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

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

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

219 

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

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

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

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

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

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

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

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

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

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

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

230 

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

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

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

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

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

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

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

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

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

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

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

241 
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

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

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

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

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

246 

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

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

250 

251 
lemma odd_add [simp]: 

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

253 
by simp 

254 

255 
lemma even_power [simp, presburger]: 

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

257 
by (induct n) auto 

258 

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

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

260 

58679  261 
context ring_parity 
262 
begin 

263 

264 
lemma even_minus [simp, presburger, algebra]: 

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

266 
by (simp add: even_def) 

267 

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

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

271 

58679  272 
end 
273 

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

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

275 
begin 
58645  276 

277 
lemma even_iff_mod_2_eq_zero [presburger]: 

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

54228  279 
by (simp add: even_def dvd_eq_mod_eq_0) 
280 

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

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

282 

58680  283 

58687  284 
subsubsection {* Particularities for @{typ nat} and @{typ int} *} 
285 

286 
lemma even_Suc [simp, presburger, algebra]: 

287 
"even (Suc n) = odd n" 

288 
by (simp add: even_def two_dvd_Suc_iff) 

289 

58689  290 
lemma odd_pos: 
291 
"odd (n :: nat) \<Longrightarrow> 0 < n" 

292 
by (auto simp add: even_def intro: classical) 

293 

58687  294 
lemma even_diff_nat [simp]: 
295 
fixes m n :: nat 

296 
shows "even (m  n) \<longleftrightarrow> m < n \<or> even (m + n)" 

297 
by (simp add: even_def two_dvd_diff_nat_iff) 

58680  298 

58679  299 
lemma even_int_iff: 
300 
"even (int n) \<longleftrightarrow> even n" 

301 
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

302 

58687  303 
lemma even_nat_iff: 
304 
"0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k" 

305 
by (simp add: even_int_iff [symmetric]) 

306 

307 

58689  308 
subsubsection {* Parity and powers *} 
309 

310 
context comm_ring_1 

311 
begin 

312 

313 
lemma neg_power_if: 

314 
"( a) ^ n = (if even n then a ^ n else  (a ^ n))" 

315 
by (induct n) simp_all 

316 

317 
lemma power_minus_even [simp]: 

318 
"even n \<Longrightarrow> ( a) ^ n = a ^ n" 

319 
by (simp add: neg_power_if) 

320 

321 
lemma power_minus_odd [simp]: 

322 
"odd n \<Longrightarrow> ( a) ^ n =  (a ^ n)" 

323 
by (simp add: neg_power_if) 

324 

325 
lemma neg_one_even_power [simp]: 

326 
"even n \<Longrightarrow> ( 1) ^ n = 1" 

327 
by (simp add: neg_power_if) 

328 

329 
lemma neg_one_odd_power [simp]: 

330 
"odd n \<Longrightarrow> ( 1) ^ n =  1" 

331 
by (simp_all add: neg_power_if) 

332 

333 
end 

334 

335 
lemma zero_less_power_nat_eq_numeral [simp]:  \<open>FIXME move\<close> 

336 
"0 < (n :: nat) ^ numeral w \<longleftrightarrow> 0 < n \<or> numeral w = (0 :: nat)" 

337 
by (fact nat_zero_less_power_iff) 

338 

339 
context linordered_idom 

340 
begin 

341 

342 
lemma power_eq_0_iff' [simp]:  \<open>FIXME move\<close> 

343 
"a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0" 

344 
by (induct n) auto 

345 

346 
lemma power2_less_eq_zero_iff [simp]:  \<open>FIXME move\<close> 

347 
"a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0" 

348 
proof (cases "a = 0") 

349 
case True then show ?thesis by simp 

350 
next 

351 
case False then have "a < 0 \<or> a > 0" by auto 

352 
then have "a\<^sup>2 > 0" by auto 

353 
then have "\<not> a\<^sup>2 \<le> 0" by (simp add: not_le) 

354 
with False show ?thesis by simp 

355 
qed 

356 

357 
lemma zero_le_even_power: 

358 
"even n \<Longrightarrow> 0 \<le> a ^ n" 

359 
by (auto simp add: even_def elim: dvd_class.dvdE) 

360 

361 
lemma zero_le_odd_power: 

362 
"odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a" 

363 
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) 

364 

365 
lemma zero_le_power_iff [presburger]: 

366 
"0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n" 

367 
proof (cases "even n") 

368 
case True 

369 
then have "2 dvd n" by (simp add: even_def) 

370 
then obtain k where "n = 2 * k" .. 

371 
thus ?thesis by (simp add: zero_le_even_power True) 

372 
next 

373 
case False 

374 
then obtain k where "n = 2 * k + 1" .. 

375 
moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0" 

376 
by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) 

377 
ultimately show ?thesis 

378 
by (auto simp add: zero_le_mult_iff zero_le_even_power) 

379 
qed 

380 

381 
lemma zero_le_power_eq [presburger]:  \<open>FIXME weaker version of @{text zero_le_power_iff}\<close> 

382 
"0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a" 

383 
using zero_le_power_iff [of a n] by auto 

384 

385 
lemma zero_less_power_eq [presburger]: 

386 
"0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a" 

387 
proof  

388 
have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0" 

389 
unfolding power_eq_0_iff' [of a n, symmetric] by blast 

390 
show ?thesis 

391 
unfolding less_le zero_le_power_iff by auto 

392 
qed 

393 

394 
lemma power_less_zero_eq [presburger]: 

395 
"a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0" 

396 
unfolding not_le [symmetric] zero_le_power_eq by auto 

397 

398 
lemma power_le_zero_eq [presburger]: 

399 
"a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)" 

400 
unfolding not_less [symmetric] zero_less_power_eq by auto 

401 

402 
lemma power_even_abs: 

403 
"even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n" 

404 
using power_abs [of a n] by (simp add: zero_le_even_power) 

405 

406 
lemma power_mono_even: 

407 
assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>" 

408 
shows "a ^ n \<le> b ^ n" 

409 
proof  

410 
have "0 \<le> \<bar>a\<bar>" by auto 

411 
with `\<bar>a\<bar> \<le> \<bar>b\<bar>` 

412 
have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" by (rule power_mono) 

413 
with `even n` show ?thesis by (simp add: power_even_abs) 

414 
qed 

415 

416 
lemma power_mono_odd: 

417 
assumes "odd n" and "a \<le> b" 

418 
shows "a ^ n \<le> b ^ n" 

419 
proof (cases "b < 0") 

420 
case True with `a \<le> b` have " b \<le>  a" and "0 \<le>  b" by auto 

421 
hence "( b) ^ n \<le> ( a) ^ n" by (rule power_mono) 

422 
with `odd n` show ?thesis by simp 

423 
next 

424 
case False then have "0 \<le> b" by auto 

425 
show ?thesis 

426 
proof (cases "a < 0") 

427 
case True then have "n \<noteq> 0" and "a \<le> 0" using `odd n` [THEN odd_pos] by auto 

428 
then have "a ^ n \<le> 0" unfolding power_le_zero_eq using `odd n` by auto 

429 
moreover 

430 
from `0 \<le> b` have "0 \<le> b ^ n" by auto 

431 
ultimately show ?thesis by auto 

432 
next 

433 
case False then have "0 \<le> a" by auto 

434 
with `a \<le> b` show ?thesis using power_mono by auto 

435 
qed 

436 
qed 

437 

438 
text {* Simplify, when the exponent is a numeral *} 

439 

440 
lemma zero_le_power_eq_numeral [simp]: 

441 
"0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" 

442 
by (fact zero_le_power_eq) 

443 

444 
lemma zero_less_power_eq_numeral [simp]: 

445 
"0 < a ^ numeral w \<longleftrightarrow> numeral w = (0 :: nat) 

446 
\<or> even (numeral w :: nat) \<and> a \<noteq> 0 \<or> odd (numeral w :: nat) \<and> 0 < a" 

447 
by (fact zero_less_power_eq) 

448 

449 
lemma power_le_zero_eq_numeral [simp]: 

450 
"a ^ numeral w \<le> 0 \<longleftrightarrow> (0 :: nat) < numeral w 

451 
\<and> (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)" 

452 
by (fact power_le_zero_eq) 

453 

454 
lemma power_less_zero_eq_numeral [simp]: 

455 
"a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0" 

456 
by (fact power_less_zero_eq) 

457 

458 
lemma power_eq_0_iff_numeral [simp]: 

459 
"a ^ numeral w = (0 :: nat) \<longleftrightarrow> a = 0 \<and> numeral w \<noteq> (0 :: nat)" 

460 
by (fact power_eq_0_iff) 

461 

462 
lemma power_even_abs_numeral [simp]: 

463 
"even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w" 

464 
by (fact power_even_abs) 

465 

466 
end 

467 

468 

58687  469 
subsubsection {* Tools setup *} 
470 

58679  471 
declare transfer_morphism_int_nat [transfer add return: 
472 
even_int_iff 

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

473 
] 
21256  474 

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

477 
using even_int_iff [of n] by simp 

25600  478 

58687  479 
lemma (in semiring_parity) [presburger]: 
58680  480 
"even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b" 
481 
by auto 

21256  482 

58687  483 
lemma [presburger, algebra]: 
484 
fixes m n :: nat 

485 
shows "even (m  n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n" 

486 
by auto 

487 

488 
lemma [presburger, algebra]: 

489 
fixes m n :: nat 

490 
shows "even (m ^ n) \<longleftrightarrow> even m \<and> 0 < n" 

491 
by simp 

492 

493 
lemma [presburger]: 

494 
fixes k :: int 

495 
shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k" 

496 
by presburger 

497 

498 
lemma [presburger]: 

499 
fixes k :: int 

500 
shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k" 

501 
by presburger 

502 

503 
lemma [presburger]: 

504 
"Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n" 

505 
by presburger 

506 

21256  507 

58688  508 
subsubsection {* Miscellaneous *} 
58680  509 

58688  510 
lemma even_nat_plus_one_div_two: 
511 
"even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" 

512 
by presburger 

58680  513 

58688  514 
lemma odd_nat_plus_one_div_two: 
515 
"odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" 

516 
by presburger 

58680  517 

58687  518 
lemma even_nat_mod_two_eq_zero: 
519 
"even (x::nat) ==> x mod Suc (Suc 0) = 0" 

58680  520 
by presburger 
21256  521 

58687  522 
lemma odd_nat_mod_two_eq_one: 
523 
"odd (x::nat) ==> x mod Suc (Suc 0) = Suc 0" 

58680  524 
by presburger 
21256  525 

58687  526 
lemma even_nat_equiv_def: 
527 
"even (x::nat) = (x mod Suc (Suc 0) = 0)" 

58680  528 
by presburger 
21256  529 

58687  530 
lemma odd_nat_equiv_def: 
531 
"odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" 

532 
by presburger 

21256  533 

58687  534 
lemma even_nat_div_two_times_two: 
535 
"even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x" 

536 
by presburger 

21256  537 

58687  538 
lemma odd_nat_div_two_times_two_plus_one: 
539 
"odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x" 

540 
by presburger 

21256  541 

58688  542 
lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger 
543 
lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger 

544 

545 
lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" 

546 
by presburger 

547 

548 
lemma lemma_odd_div2 [simp]: "odd n ==> (n + 1) div 2 = Suc (n div 2)" 

549 
by presburger 

550 

551 
lemma even_num_iff: "0 < n ==> even n = (odd (n  1 :: nat))" by presburger 

552 
lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger 

553 

554 
lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n  1) div 2)" by presburger 

555 

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

557 
by presburger 

558 

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

560 