author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47300  2284a40e0f57 
child 48891  c0eafbd55de3 
permissions  rwrr 
47108  1 
(* Title: HOL/Num.thy 
2 
Author: Florian Haftmann 

3 
Author: Brian Huffman 

4 
*) 

5 

6 
header {* Binary Numerals *} 

7 

8 
theory Num 

47191  9 
imports Datatype 
47228  10 
uses 
11 
("Tools/numeral.ML") 

47108  12 
begin 
13 

14 
subsection {* The @{text num} type *} 

15 

16 
datatype num = One  Bit0 num  Bit1 num 

17 

18 
text {* Increment function for type @{typ num} *} 

19 

20 
primrec inc :: "num \<Rightarrow> num" where 

21 
"inc One = Bit0 One"  

22 
"inc (Bit0 x) = Bit1 x"  

23 
"inc (Bit1 x) = Bit0 (inc x)" 

24 

25 
text {* Converting between type @{typ num} and type @{typ nat} *} 

26 

27 
primrec nat_of_num :: "num \<Rightarrow> nat" where 

28 
"nat_of_num One = Suc 0"  

29 
"nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x"  

30 
"nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)" 

31 

32 
primrec num_of_nat :: "nat \<Rightarrow> num" where 

33 
"num_of_nat 0 = One"  

34 
"num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)" 

35 

36 
lemma nat_of_num_pos: "0 < nat_of_num x" 

37 
by (induct x) simp_all 

38 

39 
lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0" 

40 
by (induct x) simp_all 

41 

42 
lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)" 

43 
by (induct x) simp_all 

44 

45 
lemma num_of_nat_double: 

46 
"0 < n \<Longrightarrow> num_of_nat (n + n) = Bit0 (num_of_nat n)" 

47 
by (induct n) simp_all 

48 

49 
text {* 

50 
Type @{typ num} is isomorphic to the strictly positive 

51 
natural numbers. 

52 
*} 

53 

54 
lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x" 

55 
by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos) 

56 

57 
lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" 

58 
by (induct n) (simp_all add: nat_of_num_inc) 

59 

60 
lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" 

61 
apply safe 

62 
apply (drule arg_cong [where f=num_of_nat]) 

63 
apply (simp add: nat_of_num_inverse) 

64 
done 

65 

66 
lemma num_induct [case_names One inc]: 

67 
fixes P :: "num \<Rightarrow> bool" 

68 
assumes One: "P One" 

69 
and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" 

70 
shows "P x" 

71 
proof  

72 
obtain n where n: "Suc n = nat_of_num x" 

73 
by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0) 

74 
have "P (num_of_nat (Suc n))" 

75 
proof (induct n) 

76 
case 0 show ?case using One by simp 

77 
next 

78 
case (Suc n) 

79 
then have "P (inc (num_of_nat (Suc n)))" by (rule inc) 

80 
then show "P (num_of_nat (Suc (Suc n)))" by simp 

81 
qed 

82 
with n show "P x" 

83 
by (simp add: nat_of_num_inverse) 

84 
qed 

85 

86 
text {* 

87 
From now on, there are two possible models for @{typ num}: 

88 
as positive naturals (rule @{text "num_induct"}) 

89 
and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}). 

90 
*} 

91 

92 

93 
subsection {* Numeral operations *} 

94 

95 
instantiation num :: "{plus,times,linorder}" 

96 
begin 

97 

98 
definition [code del]: 

99 
"m + n = num_of_nat (nat_of_num m + nat_of_num n)" 

100 

101 
definition [code del]: 

102 
"m * n = num_of_nat (nat_of_num m * nat_of_num n)" 

103 

104 
definition [code del]: 

105 
"m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n" 

106 

107 
definition [code del]: 

108 
"m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" 

109 

110 
instance 

111 
by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff) 

112 

113 
end 

114 

115 
lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" 

116 
unfolding plus_num_def 

117 
by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos) 

118 

119 
lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y" 

120 
unfolding times_num_def 

121 
by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos) 

122 

123 
lemma add_num_simps [simp, code]: 

124 
"One + One = Bit0 One" 

125 
"One + Bit0 n = Bit1 n" 

126 
"One + Bit1 n = Bit0 (n + One)" 

127 
"Bit0 m + One = Bit1 m" 

128 
"Bit0 m + Bit0 n = Bit0 (m + n)" 

129 
"Bit0 m + Bit1 n = Bit1 (m + n)" 

130 
"Bit1 m + One = Bit0 (m + One)" 

131 
"Bit1 m + Bit0 n = Bit1 (m + n)" 

132 
"Bit1 m + Bit1 n = Bit0 (m + n + One)" 

133 
by (simp_all add: num_eq_iff nat_of_num_add) 

134 

135 
lemma mult_num_simps [simp, code]: 

136 
"m * One = m" 

137 
"One * n = n" 

138 
"Bit0 m * Bit0 n = Bit0 (Bit0 (m * n))" 

139 
"Bit0 m * Bit1 n = Bit0 (m * Bit1 n)" 

140 
"Bit1 m * Bit0 n = Bit0 (Bit1 m * n)" 

141 
"Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))" 

142 
by (simp_all add: num_eq_iff nat_of_num_add 

143 
nat_of_num_mult left_distrib right_distrib) 

144 

145 
lemma eq_num_simps: 

146 
"One = One \<longleftrightarrow> True" 

147 
"One = Bit0 n \<longleftrightarrow> False" 

148 
"One = Bit1 n \<longleftrightarrow> False" 

149 
"Bit0 m = One \<longleftrightarrow> False" 

150 
"Bit1 m = One \<longleftrightarrow> False" 

151 
"Bit0 m = Bit0 n \<longleftrightarrow> m = n" 

152 
"Bit0 m = Bit1 n \<longleftrightarrow> False" 

153 
"Bit1 m = Bit0 n \<longleftrightarrow> False" 

154 
"Bit1 m = Bit1 n \<longleftrightarrow> m = n" 

155 
by simp_all 

156 

157 
lemma le_num_simps [simp, code]: 

158 
"One \<le> n \<longleftrightarrow> True" 

159 
"Bit0 m \<le> One \<longleftrightarrow> False" 

160 
"Bit1 m \<le> One \<longleftrightarrow> False" 

161 
"Bit0 m \<le> Bit0 n \<longleftrightarrow> m \<le> n" 

162 
"Bit0 m \<le> Bit1 n \<longleftrightarrow> m \<le> n" 

163 
"Bit1 m \<le> Bit1 n \<longleftrightarrow> m \<le> n" 

164 
"Bit1 m \<le> Bit0 n \<longleftrightarrow> m < n" 

165 
using nat_of_num_pos [of n] nat_of_num_pos [of m] 

166 
by (auto simp add: less_eq_num_def less_num_def) 

167 

168 
lemma less_num_simps [simp, code]: 

169 
"m < One \<longleftrightarrow> False" 

170 
"One < Bit0 n \<longleftrightarrow> True" 

171 
"One < Bit1 n \<longleftrightarrow> True" 

172 
"Bit0 m < Bit0 n \<longleftrightarrow> m < n" 

173 
"Bit0 m < Bit1 n \<longleftrightarrow> m \<le> n" 

174 
"Bit1 m < Bit1 n \<longleftrightarrow> m < n" 

175 
"Bit1 m < Bit0 n \<longleftrightarrow> m < n" 

176 
using nat_of_num_pos [of n] nat_of_num_pos [of m] 

177 
by (auto simp add: less_eq_num_def less_num_def) 

178 

179 
text {* Rules using @{text One} and @{text inc} as constructors *} 

180 

181 
lemma add_One: "x + One = inc x" 

182 
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) 

183 

184 
lemma add_One_commute: "One + n = n + One" 

185 
by (induct n) simp_all 

186 

187 
lemma add_inc: "x + inc y = inc (x + y)" 

188 
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) 

189 

190 
lemma mult_inc: "x * inc y = x * y + x" 

191 
by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) 

192 

193 
text {* The @{const num_of_nat} conversion *} 

194 

195 
lemma num_of_nat_One: 

47300  196 
"n \<le> 1 \<Longrightarrow> num_of_nat n = One" 
47108  197 
by (cases n) simp_all 
198 

199 
lemma num_of_nat_plus_distrib: 

200 
"0 < m \<Longrightarrow> 0 < n \<Longrightarrow> num_of_nat (m + n) = num_of_nat m + num_of_nat n" 

201 
by (induct n) (auto simp add: add_One add_One_commute add_inc) 

202 

203 
text {* A doubleanddecrement function *} 

204 

205 
primrec BitM :: "num \<Rightarrow> num" where 

206 
"BitM One = One"  

207 
"BitM (Bit0 n) = Bit1 (BitM n)"  

208 
"BitM (Bit1 n) = Bit1 (Bit0 n)" 

209 

210 
lemma BitM_plus_one: "BitM n + One = Bit0 n" 

211 
by (induct n) simp_all 

212 

213 
lemma one_plus_BitM: "One + BitM n = Bit0 n" 

214 
unfolding add_One_commute BitM_plus_one .. 

215 

216 
text {* Squaring and exponentiation *} 

217 

218 
primrec sqr :: "num \<Rightarrow> num" where 

219 
"sqr One = One"  

220 
"sqr (Bit0 n) = Bit0 (Bit0 (sqr n))"  

221 
"sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))" 

222 

223 
primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where 

224 
"pow x One = x"  

225 
"pow x (Bit0 y) = sqr (pow x y)"  

47191  226 
"pow x (Bit1 y) = sqr (pow x y) * x" 
47108  227 

228 
lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x" 

229 
by (induct x, simp_all add: algebra_simps nat_of_num_add) 

230 

231 
lemma sqr_conv_mult: "sqr x = x * x" 

232 
by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult) 

233 

234 

47211  235 
subsection {* Binary numerals *} 
47108  236 

237 
text {* 

47211  238 
We embed binary representations into a generic algebraic 
47108  239 
structure using @{text numeral}. 
240 
*} 

241 

242 
class numeral = one + semigroup_add 

243 
begin 

244 

245 
primrec numeral :: "num \<Rightarrow> 'a" where 

246 
numeral_One: "numeral One = 1"  

247 
numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n"  

248 
numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1" 

249 

250 
lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1" 

251 
apply (induct x) 

252 
apply simp 

253 
apply (simp add: add_assoc [symmetric], simp add: add_assoc) 

254 
apply (simp add: add_assoc [symmetric], simp add: add_assoc) 

255 
done 

256 

257 
lemma numeral_inc: "numeral (inc x) = numeral x + 1" 

258 
proof (induct x) 

259 
case (Bit1 x) 

260 
have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1" 

261 
by (simp only: one_plus_numeral_commute) 

262 
with Bit1 show ?case 

263 
by (simp add: add_assoc) 

264 
qed simp_all 

265 

266 
declare numeral.simps [simp del] 

267 

268 
abbreviation "Numeral1 \<equiv> numeral One" 

269 

270 
declare numeral_One [code_post] 

271 

272 
end 

273 

274 
text {* Negative numerals. *} 

275 

276 
class neg_numeral = numeral + group_add 

277 
begin 

278 

279 
definition neg_numeral :: "num \<Rightarrow> 'a" where 

280 
"neg_numeral k =  numeral k" 

281 

282 
end 

283 

284 
text {* Numeral syntax. *} 

285 

286 
syntax 

287 
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_") 

288 

289 
parse_translation {* 

290 
let 

291 
fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2) 

292 
of (0, 1) => Syntax.const @{const_name One} 

293 
 (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n 

294 
 (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n 

295 
else raise Match; 

296 
val pos = Syntax.const @{const_name numeral} 

297 
val neg = Syntax.const @{const_name neg_numeral} 

298 
val one = Syntax.const @{const_name Groups.one} 

299 
val zero = Syntax.const @{const_name Groups.zero} 

300 
fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = 

301 
c $ numeral_tr [t] $ u 

302 
 numeral_tr [Const (num, _)] = 

303 
let 

304 
val {value, ...} = Lexicon.read_xnum num; 

305 
in 

306 
if value = 0 then zero else 

307 
if value > 0 

308 
then pos $ num_of_int value 

309 
else neg $ num_of_int (~value) 

310 
end 

311 
 numeral_tr ts = raise TERM ("numeral_tr", ts); 

312 
in [("_Numeral", numeral_tr)] end 

313 
*} 

314 

315 
typed_print_translation (advanced) {* 

316 
let 

317 
fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n 

318 
 dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1 

319 
 dest_num (Const (@{const_syntax One}, _)) = 1; 

320 
fun num_tr' sign ctxt T [n] = 

321 
let 

322 
val k = dest_num n; 

323 
val t' = Syntax.const @{syntax_const "_Numeral"} $ 

324 
Syntax.free (sign ^ string_of_int k); 

325 
in 

326 
case T of 

327 
Type (@{type_name fun}, [_, T']) => 

328 
if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t' 

329 
else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T' 

330 
 T' => if T' = dummyT then t' else raise Match 

331 
end; 

332 
in [(@{const_syntax numeral}, num_tr' ""), 

333 
(@{const_syntax neg_numeral}, num_tr' "")] end 

334 
*} 

335 

47228  336 
use "Tools/numeral.ML" 
337 

338 

47108  339 
subsection {* Classspecific numeral rules *} 
340 

341 
text {* 

342 
@{const numeral} is a morphism. 

343 
*} 

344 

345 
subsubsection {* Structures with addition: class @{text numeral} *} 

346 

347 
context numeral 

348 
begin 

349 

350 
lemma numeral_add: "numeral (m + n) = numeral m + numeral n" 

351 
by (induct n rule: num_induct) 

352 
(simp_all only: numeral_One add_One add_inc numeral_inc add_assoc) 

353 

354 
lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)" 

355 
by (rule numeral_add [symmetric]) 

356 

357 
lemma numeral_plus_one: "numeral n + 1 = numeral (n + One)" 

358 
using numeral_add [of n One] by (simp add: numeral_One) 

359 

360 
lemma one_plus_numeral: "1 + numeral n = numeral (One + n)" 

361 
using numeral_add [of One n] by (simp add: numeral_One) 

362 

363 
lemma one_add_one: "1 + 1 = 2" 

364 
using numeral_add [of One One] by (simp add: numeral_One) 

365 

366 
lemmas add_numeral_special = 

367 
numeral_plus_one one_plus_numeral one_add_one 

368 

369 
end 

370 

371 
subsubsection {* 

372 
Structures with negation: class @{text neg_numeral} 

373 
*} 

374 

375 
context neg_numeral 

376 
begin 

377 

378 
text {* Numerals form an abelian subgroup. *} 

379 

380 
inductive is_num :: "'a \<Rightarrow> bool" where 

381 
"is_num 1"  

382 
"is_num x \<Longrightarrow> is_num ( x)"  

383 
"\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> is_num (x + y)" 

384 

385 
lemma is_num_numeral: "is_num (numeral k)" 

386 
by (induct k, simp_all add: numeral.simps is_num.intros) 

387 

388 
lemma is_num_add_commute: 

389 
"\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + y = y + x" 

390 
apply (induct x rule: is_num.induct) 

391 
apply (induct y rule: is_num.induct) 

392 
apply simp 

393 
apply (rule_tac a=x in add_left_imp_eq) 

394 
apply (rule_tac a=x in add_right_imp_eq) 

395 
apply (simp add: add_assoc minus_add_cancel) 

396 
apply (simp add: add_assoc [symmetric], simp add: add_assoc) 

397 
apply (rule_tac a=x in add_left_imp_eq) 

398 
apply (rule_tac a=x in add_right_imp_eq) 

399 
apply (simp add: add_assoc minus_add_cancel add_minus_cancel) 

400 
apply (simp add: add_assoc, simp add: add_assoc [symmetric]) 

401 
done 

402 

403 
lemma is_num_add_left_commute: 

404 
"\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + (y + z) = y + (x + z)" 

405 
by (simp only: add_assoc [symmetric] is_num_add_commute) 

406 

407 
lemmas is_num_normalize = 

408 
add_assoc is_num_add_commute is_num_add_left_commute 

409 
is_num.intros is_num_numeral 

410 
diff_minus minus_add add_minus_cancel minus_add_cancel 

411 

412 
definition dbl :: "'a \<Rightarrow> 'a" where "dbl x = x + x" 

413 
definition dbl_inc :: "'a \<Rightarrow> 'a" where "dbl_inc x = x + x + 1" 

414 
definition dbl_dec :: "'a \<Rightarrow> 'a" where "dbl_dec x = x + x  1" 

415 

416 
definition sub :: "num \<Rightarrow> num \<Rightarrow> 'a" where 

417 
"sub k l = numeral k  numeral l" 

418 

419 
lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n)  1" 

420 
by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq) 

421 

422 
lemma dbl_simps [simp]: 

423 
"dbl (neg_numeral k) = neg_numeral (Bit0 k)" 

424 
"dbl 0 = 0" 

425 
"dbl 1 = 2" 

426 
"dbl (numeral k) = numeral (Bit0 k)" 

427 
unfolding dbl_def neg_numeral_def numeral.simps 

428 
by (simp_all add: minus_add) 

429 

430 
lemma dbl_inc_simps [simp]: 

431 
"dbl_inc (neg_numeral k) = neg_numeral (BitM k)" 

432 
"dbl_inc 0 = 1" 

433 
"dbl_inc 1 = 3" 

434 
"dbl_inc (numeral k) = numeral (Bit1 k)" 

435 
unfolding dbl_inc_def neg_numeral_def numeral.simps numeral_BitM 

436 
by (simp_all add: is_num_normalize) 

437 

438 
lemma dbl_dec_simps [simp]: 

439 
"dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)" 

440 
"dbl_dec 0 = 1" 

441 
"dbl_dec 1 = 1" 

442 
"dbl_dec (numeral k) = numeral (BitM k)" 

443 
unfolding dbl_dec_def neg_numeral_def numeral.simps numeral_BitM 

444 
by (simp_all add: is_num_normalize) 

445 

446 
lemma sub_num_simps [simp]: 

447 
"sub One One = 0" 

448 
"sub One (Bit0 l) = neg_numeral (BitM l)" 

449 
"sub One (Bit1 l) = neg_numeral (Bit0 l)" 

450 
"sub (Bit0 k) One = numeral (BitM k)" 

451 
"sub (Bit1 k) One = numeral (Bit0 k)" 

452 
"sub (Bit0 k) (Bit0 l) = dbl (sub k l)" 

453 
"sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)" 

454 
"sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)" 

455 
"sub (Bit1 k) (Bit1 l) = dbl (sub k l)" 

456 
unfolding dbl_def dbl_dec_def dbl_inc_def sub_def 

457 
unfolding neg_numeral_def numeral.simps numeral_BitM 

458 
by (simp_all add: is_num_normalize) 

459 

460 
lemma add_neg_numeral_simps: 

461 
"numeral m + neg_numeral n = sub m n" 

462 
"neg_numeral m + numeral n = sub n m" 

463 
"neg_numeral m + neg_numeral n = neg_numeral (m + n)" 

464 
unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps 

465 
by (simp_all add: is_num_normalize) 

466 

467 
lemma add_neg_numeral_special: 

468 
"1 + neg_numeral m = sub One m" 

469 
"neg_numeral m + 1 = sub One m" 

470 
unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps 

471 
by (simp_all add: is_num_normalize) 

472 

473 
lemma diff_numeral_simps: 

474 
"numeral m  numeral n = sub m n" 

475 
"numeral m  neg_numeral n = numeral (m + n)" 

476 
"neg_numeral m  numeral n = neg_numeral (m + n)" 

477 
"neg_numeral m  neg_numeral n = sub n m" 

478 
unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps 

479 
by (simp_all add: is_num_normalize) 

480 

481 
lemma diff_numeral_special: 

482 
"1  numeral n = sub One n" 

483 
"1  neg_numeral n = numeral (One + n)" 

484 
"numeral m  1 = sub m One" 

485 
"neg_numeral m  1 = neg_numeral (m + One)" 

486 
unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps 

487 
by (simp_all add: is_num_normalize) 

488 

489 
lemma minus_one: " 1 = 1" 

490 
unfolding neg_numeral_def numeral.simps .. 

491 

492 
lemma minus_numeral: " numeral n = neg_numeral n" 

493 
unfolding neg_numeral_def .. 

494 

495 
lemma minus_neg_numeral: " neg_numeral n = numeral n" 

496 
unfolding neg_numeral_def by simp 

497 

498 
lemmas minus_numeral_simps [simp] = 

499 
minus_one minus_numeral minus_neg_numeral 

500 

501 
end 

502 

503 
subsubsection {* 

504 
Structures with multiplication: class @{text semiring_numeral} 

505 
*} 

506 

507 
class semiring_numeral = semiring + monoid_mult 

508 
begin 

509 

510 
subclass numeral .. 

511 

512 
lemma numeral_mult: "numeral (m * n) = numeral m * numeral n" 

513 
apply (induct n rule: num_induct) 

514 
apply (simp add: numeral_One) 

47227  515 
apply (simp add: mult_inc numeral_inc numeral_add right_distrib) 
47108  516 
done 
517 

518 
lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)" 

519 
by (rule numeral_mult [symmetric]) 

520 

521 
end 

522 

523 
subsubsection {* 

524 
Structures with a zero: class @{text semiring_1} 

525 
*} 

526 

527 
context semiring_1 

528 
begin 

529 

530 
subclass semiring_numeral .. 

531 

532 
lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" 

533 
by (induct n, 

534 
simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) 

535 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

536 
lemma mult_2: "2 * z = z + z" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

537 
unfolding one_add_one [symmetric] left_distrib by simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

538 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

539 
lemma mult_2_right: "z * 2 = z + z" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

540 
unfolding one_add_one [symmetric] right_distrib by simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

541 

47108  542 
end 
543 

544 
lemma nat_of_num_numeral: "nat_of_num = numeral" 

545 
proof 

546 
fix n 

547 
have "numeral n = nat_of_num n" 

548 
by (induct n) (simp_all add: numeral.simps) 

549 
then show "nat_of_num n = numeral n" by simp 

550 
qed 

551 

552 
subsubsection {* 

553 
Equality: class @{text semiring_char_0} 

554 
*} 

555 

556 
context semiring_char_0 

557 
begin 

558 

559 
lemma numeral_eq_iff: "numeral m = numeral n \<longleftrightarrow> m = n" 

560 
unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] 

561 
of_nat_eq_iff num_eq_iff .. 

562 

563 
lemma numeral_eq_one_iff: "numeral n = 1 \<longleftrightarrow> n = One" 

564 
by (rule numeral_eq_iff [of n One, unfolded numeral_One]) 

565 

566 
lemma one_eq_numeral_iff: "1 = numeral n \<longleftrightarrow> One = n" 

567 
by (rule numeral_eq_iff [of One n, unfolded numeral_One]) 

568 

569 
lemma numeral_neq_zero: "numeral n \<noteq> 0" 

570 
unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] 

571 
by (simp add: nat_of_num_pos) 

572 

573 
lemma zero_neq_numeral: "0 \<noteq> numeral n" 

574 
unfolding eq_commute [of 0] by (rule numeral_neq_zero) 

575 

576 
lemmas eq_numeral_simps [simp] = 

577 
numeral_eq_iff 

578 
numeral_eq_one_iff 

579 
one_eq_numeral_iff 

580 
numeral_neq_zero 

581 
zero_neq_numeral 

582 

583 
end 

584 

585 
subsubsection {* 

586 
Comparisons: class @{text linordered_semidom} 

587 
*} 

588 

589 
text {* Could be perhaps more general than here. *} 

590 

591 
context linordered_semidom 

592 
begin 

593 

594 
lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n" 

595 
proof  

596 
have "of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n" 

597 
unfolding less_eq_num_def nat_of_num_numeral of_nat_le_iff .. 

598 
then show ?thesis by simp 

599 
qed 

600 

601 
lemma one_le_numeral: "1 \<le> numeral n" 

602 
using numeral_le_iff [of One n] by (simp add: numeral_One) 

603 

604 
lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One" 

605 
using numeral_le_iff [of n One] by (simp add: numeral_One) 

606 

607 
lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n" 

608 
proof  

609 
have "of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n" 

610 
unfolding less_num_def nat_of_num_numeral of_nat_less_iff .. 

611 
then show ?thesis by simp 

612 
qed 

613 

614 
lemma not_numeral_less_one: "\<not> numeral n < 1" 

615 
using numeral_less_iff [of n One] by (simp add: numeral_One) 

616 

617 
lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n" 

618 
using numeral_less_iff [of One n] by (simp add: numeral_One) 

619 

620 
lemma zero_le_numeral: "0 \<le> numeral n" 

621 
by (induct n) (simp_all add: numeral.simps) 

622 

623 
lemma zero_less_numeral: "0 < numeral n" 

624 
by (induct n) (simp_all add: numeral.simps add_pos_pos) 

625 

626 
lemma not_numeral_le_zero: "\<not> numeral n \<le> 0" 

627 
by (simp add: not_le zero_less_numeral) 

628 

629 
lemma not_numeral_less_zero: "\<not> numeral n < 0" 

630 
by (simp add: not_less zero_le_numeral) 

631 

632 
lemmas le_numeral_extra = 

633 
zero_le_one not_one_le_zero 

634 
order_refl [of 0] order_refl [of 1] 

635 

636 
lemmas less_numeral_extra = 

637 
zero_less_one not_one_less_zero 

638 
less_irrefl [of 0] less_irrefl [of 1] 

639 

640 
lemmas le_numeral_simps [simp] = 

641 
numeral_le_iff 

642 
one_le_numeral 

643 
numeral_le_one_iff 

644 
zero_le_numeral 

645 
not_numeral_le_zero 

646 

647 
lemmas less_numeral_simps [simp] = 

648 
numeral_less_iff 

649 
one_less_numeral_iff 

650 
not_numeral_less_one 

651 
zero_less_numeral 

652 
not_numeral_less_zero 

653 

654 
end 

655 

656 
subsubsection {* 

657 
Multiplication and negation: class @{text ring_1} 

658 
*} 

659 

660 
context ring_1 

661 
begin 

662 

663 
subclass neg_numeral .. 

664 

665 
lemma mult_neg_numeral_simps: 

666 
"neg_numeral m * neg_numeral n = numeral (m * n)" 

667 
"neg_numeral m * numeral n = neg_numeral (m * n)" 

668 
"numeral m * neg_numeral n = neg_numeral (m * n)" 

669 
unfolding neg_numeral_def mult_minus_left mult_minus_right 

670 
by (simp_all only: minus_minus numeral_mult) 

671 

672 
lemma mult_minus1 [simp]: "1 * z =  z" 

673 
unfolding neg_numeral_def numeral.simps mult_minus_left by simp 

674 

675 
lemma mult_minus1_right [simp]: "z * 1 =  z" 

676 
unfolding neg_numeral_def numeral.simps mult_minus_right by simp 

677 

678 
end 

679 

680 
subsubsection {* 

681 
Equality using @{text iszero} for rings with nonzero characteristic 

682 
*} 

683 

684 
context ring_1 

685 
begin 

686 

687 
definition iszero :: "'a \<Rightarrow> bool" 

688 
where "iszero z \<longleftrightarrow> z = 0" 

689 

690 
lemma iszero_0 [simp]: "iszero 0" 

691 
by (simp add: iszero_def) 

692 

693 
lemma not_iszero_1 [simp]: "\<not> iszero 1" 

694 
by (simp add: iszero_def) 

695 

696 
lemma not_iszero_Numeral1: "\<not> iszero Numeral1" 

697 
by (simp add: numeral_One) 

698 

699 
lemma iszero_neg_numeral [simp]: 

700 
"iszero (neg_numeral w) \<longleftrightarrow> iszero (numeral w)" 

701 
unfolding iszero_def neg_numeral_def 

702 
by (rule neg_equal_0_iff_equal) 

703 

704 
lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x  y)" 

705 
unfolding iszero_def by (rule eq_iff_diff_eq_0) 

706 

707 
text {* The @{text "eq_numeral_iff_iszero"} lemmas are not declared 

708 
@{text "[simp]"} by default, because for rings of characteristic zero, 

709 
better simp rules are possible. For a type like integers mod @{text 

710 
"n"}, typeinstantiated versions of these rules should be added to the 

711 
simplifier, along with a typespecific rule for deciding propositions 

712 
of the form @{text "iszero (numeral w)"}. 

713 

714 
bh: Maybe it would not be so bad to just declare these as simp 

715 
rules anyway? I should test whether these rules take precedence over 

716 
the @{text "ring_char_0"} rules in the simplifier. 

717 
*} 

718 

719 
lemma eq_numeral_iff_iszero: 

720 
"numeral x = numeral y \<longleftrightarrow> iszero (sub x y)" 

721 
"numeral x = neg_numeral y \<longleftrightarrow> iszero (numeral (x + y))" 

722 
"neg_numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))" 

723 
"neg_numeral x = neg_numeral y \<longleftrightarrow> iszero (sub y x)" 

724 
"numeral x = 1 \<longleftrightarrow> iszero (sub x One)" 

725 
"1 = numeral y \<longleftrightarrow> iszero (sub One y)" 

726 
"neg_numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))" 

727 
"1 = neg_numeral y \<longleftrightarrow> iszero (numeral (One + y))" 

728 
"numeral x = 0 \<longleftrightarrow> iszero (numeral x)" 

729 
"0 = numeral y \<longleftrightarrow> iszero (numeral y)" 

730 
"neg_numeral x = 0 \<longleftrightarrow> iszero (numeral x)" 

731 
"0 = neg_numeral y \<longleftrightarrow> iszero (numeral y)" 

732 
unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special 

733 
by simp_all 

734 

735 
end 

736 

737 
subsubsection {* 

738 
Equality and negation: class @{text ring_char_0} 

739 
*} 

740 

741 
class ring_char_0 = ring_1 + semiring_char_0 

742 
begin 

743 

744 
lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)" 

745 
by (simp add: iszero_def) 

746 

747 
lemma neg_numeral_eq_iff: "neg_numeral m = neg_numeral n \<longleftrightarrow> m = n" 

748 
by (simp only: neg_numeral_def neg_equal_iff_equal numeral_eq_iff) 

749 

750 
lemma numeral_neq_neg_numeral: "numeral m \<noteq> neg_numeral n" 

751 
unfolding neg_numeral_def eq_neg_iff_add_eq_0 

752 
by (simp add: numeral_plus_numeral) 

753 

754 
lemma neg_numeral_neq_numeral: "neg_numeral m \<noteq> numeral n" 

755 
by (rule numeral_neq_neg_numeral [symmetric]) 

756 

757 
lemma zero_neq_neg_numeral: "0 \<noteq> neg_numeral n" 

758 
unfolding neg_numeral_def neg_0_equal_iff_equal by simp 

759 

760 
lemma neg_numeral_neq_zero: "neg_numeral n \<noteq> 0" 

761 
unfolding neg_numeral_def neg_equal_0_iff_equal by simp 

762 

763 
lemma one_neq_neg_numeral: "1 \<noteq> neg_numeral n" 

764 
using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One) 

765 

766 
lemma neg_numeral_neq_one: "neg_numeral n \<noteq> 1" 

767 
using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One) 

768 

769 
lemmas eq_neg_numeral_simps [simp] = 

770 
neg_numeral_eq_iff 

771 
numeral_neq_neg_numeral neg_numeral_neq_numeral 

772 
one_neq_neg_numeral neg_numeral_neq_one 

773 
zero_neq_neg_numeral neg_numeral_neq_zero 

774 

775 
end 

776 

777 
subsubsection {* 

778 
Structures with negation and order: class @{text linordered_idom} 

779 
*} 

780 

781 
context linordered_idom 

782 
begin 

783 

784 
subclass ring_char_0 .. 

785 

786 
lemma neg_numeral_le_iff: "neg_numeral m \<le> neg_numeral n \<longleftrightarrow> n \<le> m" 

787 
by (simp only: neg_numeral_def neg_le_iff_le numeral_le_iff) 

788 

789 
lemma neg_numeral_less_iff: "neg_numeral m < neg_numeral n \<longleftrightarrow> n < m" 

790 
by (simp only: neg_numeral_def neg_less_iff_less numeral_less_iff) 

791 

792 
lemma neg_numeral_less_zero: "neg_numeral n < 0" 

793 
by (simp only: neg_numeral_def neg_less_0_iff_less zero_less_numeral) 

794 

795 
lemma neg_numeral_le_zero: "neg_numeral n \<le> 0" 

796 
by (simp only: neg_numeral_def neg_le_0_iff_le zero_le_numeral) 

797 

798 
lemma not_zero_less_neg_numeral: "\<not> 0 < neg_numeral n" 

799 
by (simp only: not_less neg_numeral_le_zero) 

800 

801 
lemma not_zero_le_neg_numeral: "\<not> 0 \<le> neg_numeral n" 

802 
by (simp only: not_le neg_numeral_less_zero) 

803 

804 
lemma neg_numeral_less_numeral: "neg_numeral m < numeral n" 

805 
using neg_numeral_less_zero zero_less_numeral by (rule less_trans) 

806 

807 
lemma neg_numeral_le_numeral: "neg_numeral m \<le> numeral n" 

808 
by (simp only: less_imp_le neg_numeral_less_numeral) 

809 

810 
lemma not_numeral_less_neg_numeral: "\<not> numeral m < neg_numeral n" 

811 
by (simp only: not_less neg_numeral_le_numeral) 

812 

813 
lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> neg_numeral n" 

814 
by (simp only: not_le neg_numeral_less_numeral) 

815 

816 
lemma neg_numeral_less_one: "neg_numeral m < 1" 

817 
by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One]) 

818 

819 
lemma neg_numeral_le_one: "neg_numeral m \<le> 1" 

820 
by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One]) 

821 

822 
lemma not_one_less_neg_numeral: "\<not> 1 < neg_numeral m" 

823 
by (simp only: not_less neg_numeral_le_one) 

824 

825 
lemma not_one_le_neg_numeral: "\<not> 1 \<le> neg_numeral m" 

826 
by (simp only: not_le neg_numeral_less_one) 

827 

828 
lemma sub_non_negative: 

829 
"sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m" 

830 
by (simp only: sub_def le_diff_eq) simp 

831 

832 
lemma sub_positive: 

833 
"sub n m > 0 \<longleftrightarrow> n > m" 

834 
by (simp only: sub_def less_diff_eq) simp 

835 

836 
lemma sub_non_positive: 

837 
"sub n m \<le> 0 \<longleftrightarrow> n \<le> m" 

838 
by (simp only: sub_def diff_le_eq) simp 

839 

840 
lemma sub_negative: 

841 
"sub n m < 0 \<longleftrightarrow> n < m" 

842 
by (simp only: sub_def diff_less_eq) simp 

843 

844 
lemmas le_neg_numeral_simps [simp] = 

845 
neg_numeral_le_iff 

846 
neg_numeral_le_numeral not_numeral_le_neg_numeral 

847 
neg_numeral_le_zero not_zero_le_neg_numeral 

848 
neg_numeral_le_one not_one_le_neg_numeral 

849 

850 
lemmas less_neg_numeral_simps [simp] = 

851 
neg_numeral_less_iff 

852 
neg_numeral_less_numeral not_numeral_less_neg_numeral 

853 
neg_numeral_less_zero not_zero_less_neg_numeral 

854 
neg_numeral_less_one not_one_less_neg_numeral 

855 

856 
lemma abs_numeral [simp]: "abs (numeral n) = numeral n" 

857 
by simp 

858 

859 
lemma abs_neg_numeral [simp]: "abs (neg_numeral n) = numeral n" 

860 
by (simp only: neg_numeral_def abs_minus_cancel abs_numeral) 

861 

862 
end 

863 

864 
subsubsection {* 

865 
Natural numbers 

866 
*} 

867 

47299  868 
lemma Suc_1 [simp]: "Suc 1 = 2" 
869 
unfolding Suc_eq_plus1 by (rule one_add_one) 

870 

47108  871 
lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)" 
47299  872 
unfolding Suc_eq_plus1 by (rule numeral_plus_one) 
47108  873 

47209
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

874 
definition pred_numeral :: "num \<Rightarrow> nat" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

875 
where [code del]: "pred_numeral k = numeral k  1" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

876 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

877 
lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

878 
unfolding pred_numeral_def by simp 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

879 

47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47218
diff
changeset

880 
lemma eval_nat_numeral: 
47108  881 
"numeral One = Suc 0" 
882 
"numeral (Bit0 n) = Suc (numeral (BitM n))" 

883 
"numeral (Bit1 n) = Suc (numeral (Bit0 n))" 

884 
by (simp_all add: numeral.simps BitM_plus_one) 

885 

47209
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

886 
lemma pred_numeral_simps [simp]: 
47300  887 
"pred_numeral One = 0" 
888 
"pred_numeral (Bit0 k) = numeral (BitM k)" 

889 
"pred_numeral (Bit1 k) = numeral (Bit0 k)" 

47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47218
diff
changeset

890 
unfolding pred_numeral_def eval_nat_numeral 
47209
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

891 
by (simp_all only: diff_Suc_Suc diff_0) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

892 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

893 
lemma numeral_2_eq_2: "2 = Suc (Suc 0)" 
47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47218
diff
changeset

894 
by (simp add: eval_nat_numeral) 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

895 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

896 
lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))" 
47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47218
diff
changeset

897 
by (simp add: eval_nat_numeral) 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

898 

47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

899 
lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

900 
by (simp only: numeral_One One_nat_def) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

901 

9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

902 
lemma Suc_nat_number_of_add: 
47300  903 
"Suc (numeral v + n) = numeral (v + One) + n" 
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

904 
by simp 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

905 

9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

906 
(*Maps #n to n for n = 1, 2*) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

907 
lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

908 

47209
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

909 
text {* Comparisons involving @{term Suc}. *} 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

910 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

911 
lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

912 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

913 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

914 
lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

915 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

916 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

917 
lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

918 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

919 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

920 
lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

921 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

922 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

923 
lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

924 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

925 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

926 
lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

927 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

928 

47218
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset

929 
lemma diff_Suc_numeral [simp]: "Suc n  numeral k = n  pred_numeral k" 
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset

930 
by (simp add: numeral_eq_Suc) 
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset

931 

2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset

932 
lemma diff_numeral_Suc [simp]: "numeral k  Suc n = pred_numeral k  n" 
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset

933 
by (simp add: numeral_eq_Suc) 
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset

934 

47209
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

935 
lemma max_Suc_numeral [simp]: 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

936 
"max (Suc n) (numeral k) = Suc (max n (pred_numeral k))" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

937 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

938 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

939 
lemma max_numeral_Suc [simp]: 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

940 
"max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

941 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

942 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

943 
lemma min_Suc_numeral [simp]: 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

944 
"min (Suc n) (numeral k) = Suc (min n (pred_numeral k))" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

945 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

946 

4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

947 
lemma min_numeral_Suc [simp]: 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

948 
"min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)" 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

949 
by (simp add: numeral_eq_Suc) 
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47207
diff
changeset

950 

47216
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

951 
text {* For @{term nat_case} and @{term nat_rec}. *} 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

952 

4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

953 
lemma nat_case_numeral [simp]: 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

954 
"nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)" 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

955 
by (simp add: numeral_eq_Suc) 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

956 

4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

957 
lemma nat_case_add_eq_if [simp]: 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

958 
"nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))" 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

959 
by (simp add: numeral_eq_Suc) 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

960 

4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

961 
lemma nat_rec_numeral [simp]: 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

962 
"nat_rec a f (numeral v) = 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

963 
(let pv = pred_numeral v in f pv (nat_rec a f pv))" 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

964 
by (simp add: numeral_eq_Suc Let_def) 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

965 

4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

966 
lemma nat_rec_add_eq_if [simp]: 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

967 
"nat_rec a f (numeral v + n) = 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

968 
(let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))" 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

969 
by (simp add: numeral_eq_Suc Let_def) 
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset

970 

47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

971 
text {* Case analysis on @{term "n < 2"} *} 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

972 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

973 
lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

974 
by (auto simp add: numeral_2_eq_2) 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

975 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

976 
text {* Removal of Small Numerals: 0, 1 and (in additive positions) 2 *} 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

977 
text {* bh: Are these rules really a good idea? *} 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

978 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

979 
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

980 
by simp 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

981 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

982 
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

983 
by simp 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

984 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

985 
text {* Can be used to eliminate long strings of Sucs, but not by default. *} 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

986 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

987 
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

988 
by simp 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

989 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

990 
lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *) 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

991 

47108  992 

993 
subsection {* Numeral equations as default simplification rules *} 

994 

995 
declare (in numeral) numeral_One [simp] 

996 
declare (in numeral) numeral_plus_numeral [simp] 

997 
declare (in numeral) add_numeral_special [simp] 

998 
declare (in neg_numeral) add_neg_numeral_simps [simp] 

999 
declare (in neg_numeral) add_neg_numeral_special [simp] 

1000 
declare (in neg_numeral) diff_numeral_simps [simp] 

1001 
declare (in neg_numeral) diff_numeral_special [simp] 

1002 
declare (in semiring_numeral) numeral_times_numeral [simp] 

1003 
declare (in ring_1) mult_neg_numeral_simps [simp] 

1004 

1005 
subsection {* Setting up simprocs *} 

1006 

1007 
lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)" 

1008 
by simp 

1009 

1010 
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::semiring_numeral)" 

1011 
by simp 

1012 

1013 
lemma divide_numeral_1: "a / Numeral1 = (a::'a::field)" 

1014 
by simp 

1015 

1016 
lemma inverse_numeral_1: 

1017 
"inverse Numeral1 = (Numeral1::'a::division_ring)" 

1018 
by simp 

1019 

47211  1020 
text{*Theorem lists for the cancellation simprocs. The use of a binary 
47108  1021 
numeral for 1 reduces the number of special cases.*} 
1022 

1023 
lemmas mult_1s = 

1024 
mult_numeral_1 mult_numeral_1_right 

1025 
mult_minus1 mult_minus1_right 

1026 

47226  1027 
setup {* 
1028 
Reorient_Proc.add 

1029 
(fn Const (@{const_name numeral}, _) $ _ => true 

1030 
 Const (@{const_name neg_numeral}, _) $ _ => true 

1031 
 _ => false) 

1032 
*} 

1033 

1034 
simproc_setup reorient_numeral 

1035 
("numeral w = x"  "neg_numeral w = y") = Reorient_Proc.proc 

1036 

47108  1037 

1038 
subsubsection {* Simplification of arithmetic operations on integer constants. *} 

1039 

1040 
lemmas arith_special = (* already declared simp above *) 

1041 
add_numeral_special add_neg_numeral_special 

1042 
diff_numeral_special minus_one 

1043 

1044 
(* rules already in simpset *) 

1045 
lemmas arith_extra_simps = 

1046 
numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right 

1047 
minus_numeral minus_neg_numeral minus_zero minus_one 

1048 
diff_numeral_simps diff_0 diff_0_right 

1049 
numeral_times_numeral mult_neg_numeral_simps 

1050 
mult_zero_left mult_zero_right 

1051 
abs_numeral abs_neg_numeral 

1052 

1053 
text {* 

1054 
For making a minimal simpset, one must include these default simprules. 

1055 
Also include @{text simp_thms}. 

1056 
*} 

1057 

1058 
lemmas arith_simps = 

1059 
add_num_simps mult_num_simps sub_num_simps 

1060 
BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps 

1061 
abs_zero abs_one arith_extra_simps 

1062 

1063 
text {* Simplification of relational operations *} 

1064 

1065 
lemmas eq_numeral_extra = 

1066 
zero_neq_one one_neq_zero 

1067 

1068 
lemmas rel_simps = 

1069 
le_num_simps less_num_simps eq_num_simps 

1070 
le_numeral_simps le_neg_numeral_simps le_numeral_extra 

1071 
less_numeral_simps less_neg_numeral_simps less_numeral_extra 

1072 
eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra 

1073 

1074 

1075 
subsubsection {* Simplification of arithmetic when nested to the right. *} 

1076 

1077 
lemma add_numeral_left [simp]: 

1078 
"numeral v + (numeral w + z) = (numeral(v + w) + z)" 

1079 
by (simp_all add: add_assoc [symmetric]) 

1080 

1081 
lemma add_neg_numeral_left [simp]: 

1082 
"numeral v + (neg_numeral w + y) = (sub v w + y)" 

1083 
"neg_numeral v + (numeral w + y) = (sub w v + y)" 

1084 
"neg_numeral v + (neg_numeral w + y) = (neg_numeral(v + w) + y)" 

1085 
by (simp_all add: add_assoc [symmetric]) 

1086 

1087 
lemma mult_numeral_left [simp]: 

1088 
"numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)" 

1089 
"neg_numeral v * (numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)" 

1090 
"numeral v * (neg_numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)" 

1091 
"neg_numeral v * (neg_numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)" 

1092 
by (simp_all add: mult_assoc [symmetric]) 

1093 

1094 
hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec 

1095 

1096 
subsection {* code module namespace *} 

1097 

1098 
code_modulename SML 

47126  1099 
Num Arith 
47108  1100 

1101 
code_modulename OCaml 

47126  1102 
Num Arith 
47108  1103 

1104 
code_modulename Haskell 

47126  1105 
Num Arith 
47108  1106 

1107 
end 