author  huffman 
Sat, 20 Aug 2011 09:59:28 0700  
changeset 44345  881c324470a2 
parent 43531  cc46a678faaf 
child 44766  d4d33a4d7548 
permissions  rwrr 
30925  1 
(* Title: HOL/Nat_Numeral.thy 
23164  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 1999 University of Cambridge 

4 
*) 

5 

30925  6 
header {* Binary numerals for the natural numbers *} 
23164  7 

30925  8 
theory Nat_Numeral 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

9 
imports Int 
23164  10 
begin 
11 

31014  12 
subsection {* Numerals for natural numbers *} 
13 

23164  14 
text {* 
15 
Arithmetic for naturals is reduced to that for the nonnegative integers. 

16 
*} 

17 

43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

18 
instantiation nat :: number_semiring 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25481
diff
changeset

19 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25481
diff
changeset

20 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25481
diff
changeset

21 
definition 
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

22 
nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25481
diff
changeset

23 

43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

24 
instance proof 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

25 
fix n show "number_of (int n) = (of_nat n :: nat)" 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

26 
unfolding nat_number_of_def number_of_eq by simp 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

27 
qed 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

28 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25481
diff
changeset

29 
end 
23164  30 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31790
diff
changeset

31 
lemma [code_post]: 
25965  32 
"nat (number_of v) = number_of v" 
33 
unfolding nat_number_of_def .. 

34 

31014  35 

36 
subsection {* Special case: squares and cubes *} 

37 

38 
lemma numeral_2_eq_2: "2 = Suc (Suc 0)" 

39 
by (simp add: nat_number_of_def) 

40 

41 
lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))" 

42 
by (simp add: nat_number_of_def) 

43 

44 
context power 

30960  45 
begin 
46 

23164  47 
abbreviation (xsymbols) 
30960  48 
power2 :: "'a \<Rightarrow> 'a" ("(_\<twosuperior>)" [1000] 999) where 
49 
"x\<twosuperior> \<equiv> x ^ 2" 

23164  50 

51 
notation (latex output) 

29401
94fd5dd918f5
rename abbreviation square > power2, to match theorem names
huffman
parents:
29045
diff
changeset

52 
power2 ("(_\<twosuperior>)" [1000] 999) 
23164  53 

54 
notation (HTML output) 

29401
94fd5dd918f5
rename abbreviation square > power2, to match theorem names
huffman
parents:
29045
diff
changeset

55 
power2 ("(_\<twosuperior>)" [1000] 999) 
23164  56 

30960  57 
end 
58 

31014  59 
context monoid_mult 
60 
begin 

61 

62 
lemma power2_eq_square: "a\<twosuperior> = a * a" 

63 
by (simp add: numeral_2_eq_2) 

64 

65 
lemma power3_eq_cube: "a ^ 3 = a * a * a" 

66 
by (simp add: numeral_3_eq_3 mult_assoc) 

67 

68 
lemma power_even_eq: 

69 
"a ^ (2*n) = (a ^ n) ^ 2" 

35047
1b2bae06c796
hide fact Nat.add_0_right; make add_0_right from Groups priority
haftmann
parents:
35043
diff
changeset

70 
by (subst mult_commute) (simp add: power_mult) 
31014  71 

72 
lemma power_odd_eq: 

73 
"a ^ Suc (2*n) = a * (a ^ n) ^ 2" 

74 
by (simp add: power_even_eq) 

75 

76 
end 

77 

78 
context semiring_1 

79 
begin 

80 

81 
lemma zero_power2 [simp]: "0\<twosuperior> = 0" 

82 
by (simp add: power2_eq_square) 

83 

84 
lemma one_power2 [simp]: "1\<twosuperior> = 1" 

85 
by (simp add: power2_eq_square) 

86 

87 
end 

88 

36823
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

89 
context ring_1 
31014  90 
begin 
91 

92 
lemma power2_minus [simp]: 

93 
"( a)\<twosuperior> = a\<twosuperior>" 

94 
by (simp add: power2_eq_square) 

95 

96 
text{* 

97 
We cannot prove general results about the numeral @{term "1"}, 

98 
so we have to use @{term " 1"} instead. 

99 
*} 

100 

101 
lemma power_minus1_even [simp]: 

102 
"( 1) ^ (2*n) = 1" 

103 
proof (induct n) 

104 
case 0 show ?case by simp 

105 
next 

106 
case (Suc n) then show ?case by (simp add: power_add) 

107 
qed 

108 

109 
lemma power_minus1_odd: 

110 
"( 1) ^ Suc (2*n) =  1" 

111 
by simp 

112 

113 
lemma power_minus_even [simp]: 

114 
"(a) ^ (2*n) = a ^ (2*n)" 

115 
by (simp add: power_minus [of a]) 

116 

117 
end 

118 

36823
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

119 
context ring_1_no_zero_divisors 
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

120 
begin 
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

121 

001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

122 
lemma zero_eq_power2 [simp]: 
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

123 
"a\<twosuperior> = 0 \<longleftrightarrow> a = 0" 
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

124 
unfolding power2_eq_square by simp 
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

125 

36964  126 
lemma power2_eq_1_iff: 
36823
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

127 
"a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a =  1" 
36964  128 
unfolding power2_eq_square by (rule square_eq_1_iff) 
36823
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

129 

001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

130 
end 
001d1aad99de
add lemma power2_eq_1_iff; generalize some other lemmas
huffman
parents:
36719
diff
changeset

131 

44345  132 
context idom 
133 
begin 

134 

135 
lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x =  y" 

136 
unfolding power2_eq_square by (rule square_eq_iff) 

137 

138 
end 

139 

35631
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

140 
context linordered_ring 
31014  141 
begin 
142 

143 
lemma sum_squares_ge_zero: 

144 
"0 \<le> x * x + y * y" 

145 
by (intro add_nonneg_nonneg zero_le_square) 

146 

147 
lemma not_sum_squares_lt_zero: 

148 
"\<not> x * x + y * y < 0" 

149 
by (simp add: not_less sum_squares_ge_zero) 

150 

35631
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

151 
end 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

152 

0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

153 
context linordered_ring_strict 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

154 
begin 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

155 

31014  156 
lemma sum_squares_eq_zero_iff: 
157 
"x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 

31034  158 
by (simp add: add_nonneg_eq_0_iff) 
31014  159 

160 
lemma sum_squares_le_zero_iff: 

161 
"x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" 

162 
by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) 

163 

164 
lemma sum_squares_gt_zero_iff: 

165 
"0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" 

35631
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35216
diff
changeset

166 
by (simp add: not_le [symmetric] sum_squares_le_zero_iff) 
31014  167 

168 
end 

169 

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

170 
context linordered_semidom 
31014  171 
begin 
172 

173 
lemma power2_le_imp_le: 

174 
"x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y" 

175 
unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) 

176 

177 
lemma power2_less_imp_less: 

178 
"x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y" 

179 
by (rule power_less_imp_less_base) 

180 

181 
lemma power2_eq_imp_eq: 

182 
"x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y" 

183 
unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp 

184 

185 
end 

186 

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

187 
context linordered_idom 
31014  188 
begin 
189 

190 
lemma zero_le_power2 [simp]: 

191 
"0 \<le> a\<twosuperior>" 

192 
by (simp add: power2_eq_square) 

193 

194 
lemma zero_less_power2 [simp]: 

195 
"0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0" 

196 
by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) 

197 

198 
lemma power2_less_0 [simp]: 

199 
"\<not> a\<twosuperior> < 0" 

200 
by (force simp add: power2_eq_square mult_less_0_iff) 

201 

202 
lemma abs_power2 [simp]: 

203 
"abs (a\<twosuperior>) = a\<twosuperior>" 

204 
by (simp add: power2_eq_square abs_mult abs_mult_self) 

205 

206 
lemma power2_abs [simp]: 

207 
"(abs a)\<twosuperior> = a\<twosuperior>" 

208 
by (simp add: power2_eq_square abs_mult_self) 

209 

210 
lemma odd_power_less_zero: 

211 
"a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0" 

212 
proof (induct n) 

213 
case 0 

214 
then show ?case by simp 

215 
next 

216 
case (Suc n) 

217 
have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 

218 
by (simp add: mult_ac power_add power2_eq_square) 

219 
thus ?case 

220 
by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg) 

221 
qed 

222 

223 
lemma odd_0_le_power_imp_0_le: 

224 
"0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a" 

225 
using odd_power_less_zero [of a n] 

226 
by (force simp add: linorder_not_less [symmetric]) 

227 

228 
lemma zero_le_even_power'[simp]: 

229 
"0 \<le> a ^ (2*n)" 

230 
proof (induct n) 

231 
case 0 

35216  232 
show ?case by simp 
31014  233 
next 
234 
case (Suc n) 

235 
have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 

236 
by (simp add: mult_ac power_add power2_eq_square) 

237 
thus ?case 

238 
by (simp add: Suc zero_le_mult_iff) 

239 
qed 

240 

241 
lemma sum_power2_ge_zero: 

242 
"0 \<le> x\<twosuperior> + y\<twosuperior>" 

243 
unfolding power2_eq_square by (rule sum_squares_ge_zero) 

244 

245 
lemma not_sum_power2_lt_zero: 

246 
"\<not> x\<twosuperior> + y\<twosuperior> < 0" 

247 
unfolding power2_eq_square by (rule not_sum_squares_lt_zero) 

248 

249 
lemma sum_power2_eq_zero_iff: 

250 
"x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 

251 
unfolding power2_eq_square by (rule sum_squares_eq_zero_iff) 

252 

253 
lemma sum_power2_le_zero_iff: 

254 
"x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" 

255 
unfolding power2_eq_square by (rule sum_squares_le_zero_iff) 

256 

257 
lemma sum_power2_gt_zero_iff: 

258 
"0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" 

259 
unfolding power2_eq_square by (rule sum_squares_gt_zero_iff) 

260 

261 
end 

262 

263 
lemma power2_sum: 

43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

264 
fixes x y :: "'a::number_semiring" 
31014  265 
shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y" 
43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

266 
by (simp add: algebra_simps power2_eq_square semiring_mult_2_right) 
31014  267 

268 
lemma power2_diff: 

269 
fixes x y :: "'a::number_ring" 

270 
shows "(x  y)\<twosuperior> = x\<twosuperior> + y\<twosuperior>  2 * x * y" 

33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

271 
by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute) 
31014  272 

23164  273 

29040
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

274 
subsection {* Predicate for negative binary numbers *} 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

275 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

276 
definition neg :: "int \<Rightarrow> bool" where 
29040
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

277 
"neg Z \<longleftrightarrow> Z < 0" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

278 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

279 
lemma not_neg_int [simp]: "~ neg (of_nat n)" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

280 
by (simp add: neg_def) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

281 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

282 
lemma neg_zminus_int [simp]: "neg ( (of_nat (Suc n)))" 
35216  283 
by (simp add: neg_def del: of_nat_Suc) 
29040
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

284 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

285 
lemmas neg_eq_less_0 = neg_def 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

286 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

287 
lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

288 
by (simp add: neg_def linorder_not_less) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

289 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

290 
text{*To simplify inequalities when Numeral1 can get simplified to 1*} 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

291 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

292 
lemma not_neg_0: "~ neg 0" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

293 
by (simp add: One_int_def neg_def) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

294 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

295 
lemma not_neg_1: "~ neg 1" 
35216  296 
by (simp add: neg_def linorder_not_less) 
29040
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

297 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

298 
lemma neg_nat: "neg z ==> nat z = 0" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

299 
by (simp add: neg_def order_less_imp_le) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

300 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

301 
lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

302 
by (simp add: linorder_not_less neg_def) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

303 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

304 
text {* 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

305 
If @{term Numeral0} is rewritten to 0 then this rule can't be applied: 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

306 
@{term Numeral0} IS @{term "number_of Pls"} 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

307 
*} 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

308 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

309 
lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

310 
by (simp add: neg_def) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

311 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

312 
lemma neg_number_of_Min: "neg (number_of Int.Min)" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

313 
by (simp add: neg_def) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

314 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

315 
lemma neg_number_of_Bit0: 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

316 
"neg (number_of (Int.Bit0 w)) = neg (number_of w)" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

317 
by (simp add: neg_def) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

318 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

319 
lemma neg_number_of_Bit1: 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

320 
"neg (number_of (Int.Bit1 w)) = neg (number_of w)" 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

321 
by (simp add: neg_def) 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

322 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

323 
lemmas neg_simps [simp] = 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

324 
not_neg_0 not_neg_1 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

325 
not_neg_number_of_Pls neg_number_of_Min 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

326 
neg_number_of_Bit0 neg_number_of_Bit1 
286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

327 

286c669d3a7a
move all negrelated lemmas to NatBin; make type of neg specific to int
huffman
parents:
29039
diff
changeset

328 

23164  329 
subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} 
330 

35216  331 
declare nat_1 [simp] 
23164  332 

333 
lemma nat_number_of [simp]: "nat (number_of w) = number_of w" 

334 
by (simp add: nat_number_of_def) 

335 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31790
diff
changeset

336 
lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)" 
23164  337 
by (simp add: nat_number_of_def) 
338 

339 
lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)" 

35216  340 
by (simp add: nat_number_of_def) 
23164  341 

36719  342 
lemma Numeral1_eq1_nat: 
343 
"(1::nat) = Numeral1" 

344 
by simp 

345 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31790
diff
changeset

346 
lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0" 
35216  347 
by (simp only: nat_numeral_1_eq_1 One_nat_def) 
23164  348 

349 

350 
subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*} 

351 

352 
lemma int_nat_number_of [simp]: 

23365  353 
"int (number_of v) = 
23307
2fe3345035c7
modify proofs to avoid referring to int::nat=>int
huffman
parents:
23294
diff
changeset

354 
(if neg (number_of v :: int) then 0 
2fe3345035c7
modify proofs to avoid referring to int::nat=>int
huffman
parents:
23294
diff
changeset

355 
else (number_of v :: int))" 
28984  356 
unfolding nat_number_of_def number_of_is_id neg_def 
357 
by simp 

23307
2fe3345035c7
modify proofs to avoid referring to int::nat=>int
huffman
parents:
23294
diff
changeset

358 

43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

359 
lemma nonneg_int_cases: 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

360 
fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n" 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

361 
using assms by (cases k, simp, simp) 
23164  362 

363 
subsubsection{*Successor *} 

364 

365 
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" 

366 
apply (rule sym) 

367 
apply (simp add: nat_eq_iff int_Suc) 

368 
done 

369 

370 
lemma Suc_nat_number_of_add: 

371 
"Suc (number_of v + n) = 

28984  372 
(if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)" 
373 
unfolding nat_number_of_def number_of_is_id neg_def numeral_simps 

374 
by (simp add: Suc_nat_eq_nat_zadd1 add_ac) 

23164  375 

376 
lemma Suc_nat_number_of [simp]: 

377 
"Suc (number_of v) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

378 
(if neg (number_of v :: int) then 1 else number_of (Int.succ v))" 
23164  379 
apply (cut_tac n = 0 in Suc_nat_number_of_add) 
380 
apply (simp cong del: if_weak_cong) 

381 
done 

382 

383 

384 
subsubsection{*Addition *} 

385 

386 
lemma add_nat_number_of [simp]: 

387 
"(number_of v :: nat) + number_of v' = 

29012  388 
(if v < Int.Pls then number_of v' 
389 
else if v' < Int.Pls then number_of v 

23164  390 
else number_of (v + v'))" 
29012  391 
unfolding nat_number_of_def number_of_is_id numeral_simps 
28984  392 
by (simp add: nat_add_distrib) 
23164  393 

30081  394 
lemma nat_number_of_add_1 [simp]: 
395 
"number_of v + (1::nat) = 

396 
(if v < Int.Pls then 1 else number_of (Int.succ v))" 

397 
unfolding nat_number_of_def number_of_is_id numeral_simps 

398 
by (simp add: nat_add_distrib) 

399 

400 
lemma nat_1_add_number_of [simp]: 

401 
"(1::nat) + number_of v = 

402 
(if v < Int.Pls then 1 else number_of (Int.succ v))" 

403 
unfolding nat_number_of_def number_of_is_id numeral_simps 

404 
by (simp add: nat_add_distrib) 

405 

406 
lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)" 

43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

407 
by (rule semiring_one_add_one_is_two) 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

408 

cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

409 
text {* TODO: replace simp rules above with these generic ones: *} 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

410 

cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

411 
lemma semiring_add_number_of: 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

412 
"\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow> 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

413 
(number_of v :: 'a::number_semiring) + number_of v' = number_of (v + v')" 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

414 
unfolding Int.Pls_def 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

415 
by (elim nonneg_int_cases, 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

416 
simp only: number_of_int of_nat_add [symmetric]) 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

417 

cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

418 
lemma semiring_number_of_add_1: 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

419 
"Int.Pls \<le> v \<Longrightarrow> 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

420 
number_of v + (1::'a::number_semiring) = number_of (Int.succ v)" 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

421 
unfolding Int.Pls_def Int.succ_def 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

422 
by (elim nonneg_int_cases, 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

423 
simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric]) 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

424 

cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

425 
lemma semiring_1_add_number_of: 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

426 
"Int.Pls \<le> v \<Longrightarrow> 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

427 
(1::'a::number_semiring) + number_of v = number_of (Int.succ v)" 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

428 
unfolding Int.Pls_def Int.succ_def 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

429 
by (elim nonneg_int_cases, 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

430 
simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric]) 
30081  431 

23164  432 

433 
subsubsection{*Subtraction *} 

434 

435 
lemma diff_nat_eq_if: 

436 
"nat z  nat z' = 

437 
(if neg z' then nat z 

438 
else let d = zz' in 

439 
if neg d then 0 else nat d)" 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26342
diff
changeset

440 
by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26342
diff
changeset

441 

23164  442 

443 
lemma diff_nat_number_of [simp]: 

444 
"(number_of v :: nat)  number_of v' = 

29012  445 
(if v' < Int.Pls then number_of v 
23164  446 
else let d = number_of (v + uminus v') in 
447 
if neg d then 0 else nat d)" 

29012  448 
unfolding nat_number_of_def number_of_is_id numeral_simps neg_def 
449 
by auto 

23164  450 

30081  451 
lemma nat_number_of_diff_1 [simp]: 
452 
"number_of v  (1::nat) = 

453 
(if v \<le> Int.Pls then 0 else number_of (Int.pred v))" 

454 
unfolding nat_number_of_def number_of_is_id numeral_simps 

455 
by auto 

456 

23164  457 

458 
subsubsection{*Multiplication *} 

459 

460 
lemma mult_nat_number_of [simp]: 

461 
"(number_of v :: nat) * number_of v' = 

29012  462 
(if v < Int.Pls then 0 else number_of (v * v'))" 
463 
unfolding nat_number_of_def number_of_is_id numeral_simps 

28984  464 
by (simp add: nat_mult_distrib) 
23164  465 

43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

466 
(* TODO: replace mult_nat_number_of with this next rule *) 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

467 
lemma semiring_mult_number_of: 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

468 
"\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow> 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

469 
(number_of v :: 'a::number_semiring) * number_of v' = number_of (v * v')" 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

470 
unfolding Int.Pls_def 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

471 
by (elim nonneg_int_cases, 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

472 
simp only: number_of_int of_nat_mult [symmetric]) 
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

473 

23164  474 

475 
subsection{*Comparisons*} 

476 

477 
subsubsection{*Equals (=) *} 

478 

479 
lemma eq_nat_number_of [simp]: 

480 
"((number_of v :: nat) = number_of v') = 

28969  481 
(if neg (number_of v :: int) then (number_of v' :: int) \<le> 0 
482 
else if neg (number_of v' :: int) then (number_of v :: int) = 0 

483 
else v = v')" 

484 
unfolding nat_number_of_def number_of_is_id neg_def 

485 
by auto 

23164  486 

487 

488 
subsubsection{*Lessthan (<) *} 

489 

490 
lemma less_nat_number_of [simp]: 

29011  491 
"(number_of v :: nat) < number_of v' \<longleftrightarrow> 
492 
(if v < v' then Int.Pls < v' else False)" 

493 
unfolding nat_number_of_def number_of_is_id numeral_simps 

28961  494 
by auto 
23164  495 

496 

29010  497 
subsubsection{*Lessthanorequal *} 
498 

499 
lemma le_nat_number_of [simp]: 

500 
"(number_of v :: nat) \<le> number_of v' \<longleftrightarrow> 

501 
(if v \<le> v' then True else v \<le> Int.Pls)" 

502 
unfolding nat_number_of_def number_of_is_id numeral_simps 

503 
by auto 

504 

23164  505 
(*Maps #n to n for n = 0, 1, 2*) 
506 
lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2 

507 

508 

509 
subsection{*Powers with Numeric Exponents*} 

510 

511 
text{*Squares of literal numerals will be evaluated.*} 

31014  512 
lemmas power2_eq_square_number_of [simp] = 
23164  513 
power2_eq_square [of "number_of w", standard] 
514 

515 

516 
text{*Simprules for comparisons where common factors can be cancelled.*} 

517 
lemmas zero_compare_simps = 

518 
add_strict_increasing add_strict_increasing2 add_increasing 

519 
zero_le_mult_iff zero_le_divide_iff 

520 
zero_less_mult_iff zero_less_divide_iff 

521 
mult_le_0_iff divide_le_0_iff 

522 
mult_less_0_iff divide_less_0_iff 

523 
zero_le_power2 power2_less_0 

524 

525 
subsubsection{*Nat *} 

526 

527 
lemma Suc_pred': "0 < n ==> n = Suc(n  1)" 

35216  528 
by simp 
23164  529 

530 
(*Expresses a natural number constant as the Suc of another one. 

531 
NOT suitable for rewriting because n recurs in the condition.*) 

532 
lemmas expand_Suc = Suc_pred' [of "number_of v", standard] 

533 

534 
subsubsection{*Arith *} 

535 

31790  536 
lemma Suc_eq_plus1: "Suc n = n + 1" 
35216  537 
unfolding One_nat_def by simp 
23164  538 

31790  539 
lemma Suc_eq_plus1_left: "Suc n = 1 + n" 
35216  540 
unfolding One_nat_def by simp 
23164  541 

542 
(* These two can be useful when m = number_of... *) 

543 

544 
lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m  1) + n))" 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29958
diff
changeset

545 
unfolding One_nat_def by (cases m) simp_all 
23164  546 

547 
lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m  1) * n))" 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29958
diff
changeset

548 
unfolding One_nat_def by (cases m) simp_all 
23164  549 

550 
lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m  1)))" 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29958
diff
changeset

551 
unfolding One_nat_def by (cases m) simp_all 
23164  552 

553 

554 
subsection{*Comparisons involving (0::nat) *} 

555 

556 
text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*} 

557 

558 
lemma eq_number_of_0 [simp]: 

29012  559 
"number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls" 
560 
unfolding nat_number_of_def number_of_is_id numeral_simps 

561 
by auto 

23164  562 

563 
lemma eq_0_number_of [simp]: 

29012  564 
"(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls" 
23164  565 
by (rule trans [OF eq_sym_conv eq_number_of_0]) 
566 

567 
lemma less_0_number_of [simp]: 

29012  568 
"(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v" 
569 
unfolding nat_number_of_def number_of_is_id numeral_simps 

570 
by simp 

23164  571 

572 
lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)" 

28969  573 
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric]) 
23164  574 

575 

576 

577 
subsection{*Comparisons involving @{term Suc} *} 

578 

579 
lemma eq_number_of_Suc [simp]: 

580 
"(number_of v = Suc n) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

581 
(let pv = number_of (Int.pred v) in 
23164  582 
if neg pv then False else nat pv = n)" 
583 
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 

584 
number_of_pred nat_number_of_def 

585 
split add: split_if) 

586 
apply (rule_tac x = "number_of v" in spec) 

587 
apply (auto simp add: nat_eq_iff) 

588 
done 

589 

590 
lemma Suc_eq_number_of [simp]: 

591 
"(Suc n = number_of v) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

592 
(let pv = number_of (Int.pred v) in 
23164  593 
if neg pv then False else nat pv = n)" 
594 
by (rule trans [OF eq_sym_conv eq_number_of_Suc]) 

595 

596 
lemma less_number_of_Suc [simp]: 

597 
"(number_of v < Suc n) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

598 
(let pv = number_of (Int.pred v) in 
23164  599 
if neg pv then True else nat pv < n)" 
600 
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 

601 
number_of_pred nat_number_of_def 

602 
split add: split_if) 

603 
apply (rule_tac x = "number_of v" in spec) 

604 
apply (auto simp add: nat_less_iff) 

605 
done 

606 

607 
lemma less_Suc_number_of [simp]: 

608 
"(Suc n < number_of v) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

609 
(let pv = number_of (Int.pred v) in 
23164  610 
if neg pv then False else n < nat pv)" 
611 
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 

612 
number_of_pred nat_number_of_def 

613 
split add: split_if) 

614 
apply (rule_tac x = "number_of v" in spec) 

615 
apply (auto simp add: zless_nat_eq_int_zless) 

616 
done 

617 

618 
lemma le_number_of_Suc [simp]: 

619 
"(number_of v <= Suc n) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

620 
(let pv = number_of (Int.pred v) in 
23164  621 
if neg pv then True else nat pv <= n)" 
35216  622 
by (simp add: Let_def linorder_not_less [symmetric]) 
23164  623 

624 
lemma le_Suc_number_of [simp]: 

625 
"(Suc n <= number_of v) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

626 
(let pv = number_of (Int.pred v) in 
23164  627 
if neg pv then False else n <= nat pv)" 
35216  628 
by (simp add: Let_def linorder_not_less [symmetric]) 
23164  629 

630 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

631 
lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min" 
23164  632 
by auto 
633 

634 

635 

636 
subsection{*Max and Min Combined with @{term Suc} *} 

637 

638 
lemma max_number_of_Suc [simp]: 

639 
"max (Suc n) (number_of v) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

640 
(let pv = number_of (Int.pred v) in 
23164  641 
if neg pv then Suc n else Suc(max n (nat pv)))" 
642 
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 

643 
split add: split_if nat.split) 

644 
apply (rule_tac x = "number_of v" in spec) 

645 
apply auto 

646 
done 

647 

648 
lemma max_Suc_number_of [simp]: 

649 
"max (number_of v) (Suc n) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

650 
(let pv = number_of (Int.pred v) in 
23164  651 
if neg pv then Suc n else Suc(max (nat pv) n))" 
652 
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 

653 
split add: split_if nat.split) 

654 
apply (rule_tac x = "number_of v" in spec) 

655 
apply auto 

656 
done 

657 

658 
lemma min_number_of_Suc [simp]: 

659 
"min (Suc n) (number_of v) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

660 
(let pv = number_of (Int.pred v) in 
23164  661 
if neg pv then 0 else Suc(min n (nat pv)))" 
662 
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 

663 
split add: split_if nat.split) 

664 
apply (rule_tac x = "number_of v" in spec) 

665 
apply auto 

666 
done 

667 

668 
lemma min_Suc_number_of [simp]: 

669 
"min (number_of v) (Suc n) = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25571
diff
changeset

670 
(let pv = number_of (Int.pred v) in 
23164  671 
if neg pv then 0 else Suc(min (nat pv) n))" 
672 
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 

673 
split add: split_if nat.split) 

674 
apply (rule_tac x = "number_of v" in spec) 

675 
apply auto 

676 
done 

677 

678 
subsection{*Literal arithmetic involving powers*} 

679 

680 
lemma power_nat_number_of: 

681 
"(number_of v :: nat) ^ n = 

682 
(if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))" 

683 
by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq 

684 
split add: split_if cong: imp_cong) 

685 

686 

687 
lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard] 

688 
declare power_nat_number_of_number_of [simp] 

689 

690 

691 

23294  692 
text{*For arbitrary rings*} 
23164  693 

23294  694 
lemma power_number_of_even: 
43526
2b92a6943915
generalize lemmas power_number_of_even and power_number_of_odd
huffman
parents:
40690
diff
changeset

695 
fixes z :: "'a::monoid_mult" 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset

696 
shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)" 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

697 
by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

698 
nat_add_distrib power_add simp del: nat_number_of) 
23164  699 

23294  700 
lemma power_number_of_odd: 
43526
2b92a6943915
generalize lemmas power_number_of_even and power_number_of_odd
huffman
parents:
40690
diff
changeset

701 
fixes z :: "'a::monoid_mult" 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset

702 
shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w 
23164  703 
then (let w = z ^ (number_of w) in z * w * w) else 1)" 
35815
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35631
diff
changeset

704 
unfolding Let_def Bit1_def nat_number_of_def number_of_is_id 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35631
diff
changeset

705 
apply (cases "0 <= w") 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35631
diff
changeset

706 
apply (simp only: mult_assoc nat_add_distrib power_add, simp) 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

707 
apply (simp add: not_le mult_2 [symmetric] add_assoc) 
23164  708 
done 
709 

23294  710 
lemmas zpower_number_of_even = power_number_of_even [where 'a=int] 
711 
lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int] 

23164  712 

23294  713 
lemmas power_number_of_even_number_of [simp] = 
714 
power_number_of_even [of "number_of v", standard] 

23164  715 

23294  716 
lemmas power_number_of_odd_number_of [simp] = 
717 
power_number_of_odd [of "number_of v", standard] 

23164  718 

719 
lemma nat_number_of_Pls: "Numeral0 = (0::nat)" 

35216  720 
by (simp add: nat_number_of_def) 
23164  721 

40690
3f472e57446a
added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
blanchet
parents:
40077
diff
changeset

722 
lemma nat_number_of_Min [no_atp]: "number_of Int.Min = (0::nat)" 
23164  723 
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int) 
724 
done 

725 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset

726 
lemma nat_number_of_Bit0: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset

727 
"number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)" 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

728 
by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

729 
nat_add_distrib simp del: nat_number_of) 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset

730 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset

731 
lemma nat_number_of_Bit1: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25965
diff
changeset

732 
"number_of (Int.Bit1 w) = 
23164  733 
(if neg (number_of w :: int) then 0 
734 
else let n = number_of w in Suc (n + n))" 

35815
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35631
diff
changeset

735 
unfolding Let_def Bit1_def nat_number_of_def number_of_is_id neg_def 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35631
diff
changeset

736 
apply (cases "w < 0") 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

737 
apply (simp add: mult_2 [symmetric] add_assoc) 
35815
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35631
diff
changeset

738 
apply (simp only: nat_add_distrib, simp) 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

739 
done 
23164  740 

40077  741 
lemmas eval_nat_numeral = 
35216  742 
nat_number_of_Bit0 nat_number_of_Bit1 
743 

36699
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset

744 
lemmas nat_arith = 
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset

745 
add_nat_number_of 
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset

746 
diff_nat_number_of 
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset

747 
mult_nat_number_of 
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset

748 
eq_nat_number_of 
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset

749 
less_nat_number_of 
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
35815
diff
changeset

750 

36716  751 
lemmas semiring_norm = 
752 
Let_def arith_simps nat_arith rel_simps neg_simps if_False 

753 
if_True add_0 add_Suc add_number_of_left mult_number_of_left 

754 
numeral_1_eq_1 [symmetric] Suc_eq_plus1 

755 
numeral_0_eq_0 [symmetric] numerals [symmetric] 

36841
02df88789641
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
huffman
parents:
36823
diff
changeset

756 
not_iszero_Numeral1 
36716  757 

23164  758 
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

759 
by (fact Let_def) 
23164  760 

31014  761 
lemma power_m1_even: "(1) ^ (2*n) = (1::'a::{number_ring})" 
762 
by (simp only: number_of_Min power_minus1_even) 

23164  763 

31014  764 
lemma power_m1_odd: "(1) ^ Suc(2*n) = (1::'a::{number_ring})" 
765 
by (simp only: number_of_Min power_minus1_odd) 

23164  766 

33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

767 
lemma nat_number_of_add_left: 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

768 
"number_of v + (number_of v' + (k::nat)) = 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

769 
(if neg (number_of v :: int) then number_of v' + k 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

770 
else if neg (number_of v' :: int) then number_of v + k 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

771 
else number_of (v + v') + k)" 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

772 
by (auto simp add: neg_def) 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

773 

a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

774 
lemma nat_number_of_mult_left: 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

775 
"number_of v * (number_of v' * (k::nat)) = 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

776 
(if v < Int.Pls then 0 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

777 
else number_of (v * v') * k)" 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

778 
by (auto simp add: not_less Pls_def nat_number_of_def number_of_is_id 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

779 
nat_mult_distrib simp del: nat_number_of) 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

780 

23164  781 

782 
subsection{*Literal arithmetic and @{term of_nat}*} 

783 

784 
lemma of_nat_double: 

785 
"0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)" 

786 
by (simp only: mult_2 nat_add_distrib of_nat_add) 

787 

788 
lemma nat_numeral_m1_eq_0: "1 = (0::nat)" 

789 
by (simp only: nat_number_of_def) 

790 

791 
lemma of_nat_number_of_lemma: 

792 
"of_nat (number_of v :: nat) = 

793 
(if 0 \<le> (number_of v :: int) 

794 
then (number_of v :: 'a :: number_ring) 

795 
else 0)" 

33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

796 
by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat) 
23164  797 

798 
lemma of_nat_number_of_eq [simp]: 

799 
"of_nat (number_of v :: nat) = 

800 
(if neg (number_of v :: int) then 0 

801 
else (number_of v :: 'a :: number_ring))" 

802 
by (simp only: of_nat_number_of_lemma neg_def, simp) 

803 

804 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

805 
subsubsection{*For simplifying @{term "Suc m  K"} and @{term "K  Suc m"}*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

806 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

807 
text{*Where K above is a literal*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

808 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

809 
lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m  n = m  (n  Numeral1)" 
35216  810 
by (simp split: nat_diff_split) 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

811 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

812 
text {*Now just instantiating @{text n} to @{text "number_of v"} does 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

813 
the right simplification, but with some redundant inequality 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

814 
tests.*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

815 
lemma neg_number_of_pred_iff_0: 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

816 
"neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

817 
apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ") 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

818 
apply (simp only: less_Suc_eq_le le_0_eq) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

819 
apply (subst less_number_of_Suc, simp) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

820 
done 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

821 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

822 
text{*No longer required as a simprule because of the @{text inverse_fold} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

823 
simproc*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

824 
lemma Suc_diff_number_of: 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

825 
"Int.Pls < v ==> 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

826 
Suc m  (number_of v) = m  (number_of (Int.pred v))" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

827 
apply (subst Suc_diff_eq_diff_pred) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

828 
apply simp 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

829 
apply (simp del: nat_numeral_1_eq_1) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

830 
apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

831 
neg_number_of_pred_iff_0) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

832 
done 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

833 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

834 
lemma diff_Suc_eq_diff_pred: "m  Suc n = (m  1)  n" 
35216  835 
by (simp split: nat_diff_split) 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

836 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

837 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

838 
subsubsection{*For @{term nat_case} and @{term nat_rec}*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

839 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

840 
lemma nat_case_number_of [simp]: 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

841 
"nat_case a f (number_of v) = 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

842 
(let pv = number_of (Int.pred v) in 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

843 
if neg pv then a else f (nat pv))" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

844 
by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

845 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

846 
lemma nat_case_add_eq_if [simp]: 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

847 
"nat_case a f ((number_of v) + n) = 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

848 
(let pv = number_of (Int.pred v) in 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

849 
if neg pv then nat_case a f n else f (nat pv + n))" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

850 
apply (subst add_eq_if) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

851 
apply (simp split add: nat.split 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

852 
del: nat_numeral_1_eq_1 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

853 
add: nat_numeral_1_eq_1 [symmetric] 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

854 
numeral_1_eq_Suc_0 [symmetric] 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

855 
neg_number_of_pred_iff_0) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

856 
done 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

857 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

858 
lemma nat_rec_number_of [simp]: 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

859 
"nat_rec a f (number_of v) = 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

860 
(let pv = number_of (Int.pred v) in 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

861 
if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

862 
apply (case_tac " (number_of v) ::nat") 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

863 
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

864 
apply (simp split add: split_if_asm) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

865 
done 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

866 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

867 
lemma nat_rec_add_eq_if [simp]: 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

868 
"nat_rec a f (number_of v + n) = 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

869 
(let pv = number_of (Int.pred v) in 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

870 
if neg pv then nat_rec a f n 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

871 
else f (nat pv + n) (nat_rec a f (nat pv + n)))" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

872 
apply (subst add_eq_if) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

873 
apply (simp split add: nat.split 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

874 
del: nat_numeral_1_eq_1 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

875 
add: nat_numeral_1_eq_1 [symmetric] 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

876 
numeral_1_eq_Suc_0 [symmetric] 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

877 
neg_number_of_pred_iff_0) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

878 
done 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

879 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

880 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

881 
subsubsection{*Various Other Lemmas*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

882 

31080  883 
lemma card_UNIV_bool[simp]: "card (UNIV :: bool set) = 2" 
884 
by(simp add: UNIV_bool) 

885 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

886 
text {*Evens and Odds, for Mutilated Chess Board*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

887 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

888 
text{*Lemmas for specialist use, NOT as default simprules*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

889 
lemma nat_mult_2: "2 * z = (z+z::nat)" 
43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

890 
by (rule semiring_mult_2) 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

891 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

892 
lemma nat_mult_2_right: "z * 2 = (z+z::nat)" 
43531
cc46a678faaf
added number_semiring class, plus a few new lemmas;
huffman
parents:
43526
diff
changeset

893 
by (rule semiring_mult_2_right) 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

894 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

895 
text{*Case analysis on @{term "n<2"}*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

896 
lemma less_2_cases: "(n::nat) < 2 ==> n = 0  n = Suc 0" 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
32069
diff
changeset

897 
by (auto simp add: nat_1_add_1 [symmetric]) 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

898 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

899 
text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

900 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

901 
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

902 
by simp 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

903 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

904 
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

905 
by simp 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

906 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

907 
text{*Can be used to eliminate long strings of Sucs, but not by default*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

908 
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

909 
by simp 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30497
diff
changeset

910 

31096  911 
end 