author  haftmann 
Wed, 14 Jul 2010 16:13:14 +0200  
changeset 37826  4c0a5e35931a 
parent 37765  26bdfb7b680b 
child 38054  acd48ef85bfc 
permissions  rwrr 
28021  1 
(* Title: HOL/ex/Numeral.thy 
2 
Author: Florian Haftmann 

29947  3 
*) 
28021  4 

29947  5 
header {* An experimental alternative numeral representation. *} 
28021  6 

7 
theory Numeral 

33346  8 
imports Main 
28021  9 
begin 
10 

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

12 

29943  13 
datatype num = One  Dig0 num  Dig1 num 
14 

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

16 

31021  17 
primrec inc :: "num \<Rightarrow> num" where 
29943  18 
"inc One = Dig0 One" 
19 
 "inc (Dig0 x) = Dig1 x" 

20 
 "inc (Dig1 x) = Dig0 (inc x)" 

21 

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

23 

31021  24 
primrec nat_of_num :: "num \<Rightarrow> nat" where 
29943  25 
"nat_of_num One = Suc 0" 
26 
 "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x" 

27 
 "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)" 

28 

31021  29 
primrec num_of_nat :: "nat \<Rightarrow> num" where 
29943  30 
"num_of_nat 0 = One" 
31 
 "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)" 

32 

29945  33 
lemma nat_of_num_pos: "0 < nat_of_num x" 
29943  34 
by (induct x) simp_all 
35 

31028  36 
lemma nat_of_num_neq_0: "nat_of_num x \<noteq> 0" 
29943  37 
by (induct x) simp_all 
38 

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

40 
by (induct x) simp_all 

41 

42 
lemma num_of_nat_double: 

43 
"0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)" 

44 
by (induct n) simp_all 

45 

28021  46 
text {* 
29943  47 
Type @{typ num} is isomorphic to the strictly positive 
28021  48 
natural numbers. 
49 
*} 

50 

29943  51 
lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x" 
29945  52 
by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos) 
28021  53 

29943  54 
lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" 
55 
by (induct n) (simp_all add: nat_of_num_inc) 

28021  56 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

57 
lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

58 
apply safe 
29943  59 
apply (drule arg_cong [where f=num_of_nat]) 
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

60 
apply (simp add: nat_of_num_inverse) 
28021  61 
done 
62 

29943  63 
lemma num_induct [case_names One inc]: 
64 
fixes P :: "num \<Rightarrow> bool" 

65 
assumes One: "P One" 

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

67 
shows "P x" 

68 
proof  

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

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

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

72 
proof (induct n) 

73 
case 0 show ?case using One by simp 

28021  74 
next 
29943  75 
case (Suc n) 
76 
then have "P (inc (num_of_nat (Suc n)))" by (rule inc) 

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

28021  78 
qed 
29943  79 
with n show "P x" 
80 
by (simp add: nat_of_num_inverse) 

28021  81 
qed 
82 

83 
text {* 

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

29943  85 
as positive naturals (rule @{text "num_induct"}) 
28021  86 
and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}). 
87 

88 
It is not entirely clear in which context it is better to use 

89 
the one or the other, or whether the construction should be reversed. 

90 
*} 

91 

92 

29945  93 
subsection {* Numeral operations *} 
28021  94 

95 
ML {* 

31902  96 
structure Dig_Simps = Named_Thms 
97 
( 

98 
val name = "numeral" 

99 
val description = "Simplification rules for numerals" 

100 
) 

28021  101 
*} 
102 

31902  103 
setup Dig_Simps.setup 
28021  104 

29945  105 
instantiation num :: "{plus,times,ord}" 
106 
begin 

28021  107 

108 
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where 

37765  109 
"m + n = num_of_nat (nat_of_num m + nat_of_num n)" 
28021  110 

111 
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where 

37765  112 
"m * n = num_of_nat (nat_of_num m * nat_of_num n)" 
28021  113 

29945  114 
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where 
37765  115 
"m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n" 
28021  116 

29945  117 
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where 
37765  118 
"m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" 
28021  119 

29945  120 
instance .. 
28021  121 

122 
end 

123 

29945  124 
lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" 
125 
unfolding plus_num_def 

126 
by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos) 

127 

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

129 
unfolding times_num_def 

130 
by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos) 

28021  131 

29945  132 
lemma Dig_plus [numeral, simp, code]: 
133 
"One + One = Dig0 One" 

134 
"One + Dig0 m = Dig1 m" 

135 
"One + Dig1 m = Dig0 (m + One)" 

136 
"Dig0 n + One = Dig1 n" 

137 
"Dig0 n + Dig0 m = Dig0 (n + m)" 

138 
"Dig0 n + Dig1 m = Dig1 (n + m)" 

139 
"Dig1 n + One = Dig0 (n + One)" 

140 
"Dig1 n + Dig0 m = Dig1 (n + m)" 

141 
"Dig1 n + Dig1 m = Dig0 (n + m + One)" 

142 
by (simp_all add: num_eq_iff nat_of_num_add) 

28021  143 

29945  144 
lemma Dig_times [numeral, simp, code]: 
145 
"One * One = One" 

146 
"One * Dig0 n = Dig0 n" 

147 
"One * Dig1 n = Dig1 n" 

148 
"Dig0 n * One = Dig0 n" 

149 
"Dig0 n * Dig0 m = Dig0 (n * Dig0 m)" 

150 
"Dig0 n * Dig1 m = Dig0 (n * Dig1 m)" 

151 
"Dig1 n * One = Dig1 n" 

152 
"Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)" 

153 
"Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)" 

154 
by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult 

155 
left_distrib right_distrib) 

28021  156 

29991  157 
lemma Dig_eq: 
158 
"One = One \<longleftrightarrow> True" 

159 
"One = Dig0 n \<longleftrightarrow> False" 

160 
"One = Dig1 n \<longleftrightarrow> False" 

161 
"Dig0 m = One \<longleftrightarrow> False" 

162 
"Dig1 m = One \<longleftrightarrow> False" 

163 
"Dig0 m = Dig0 n \<longleftrightarrow> m = n" 

164 
"Dig0 m = Dig1 n \<longleftrightarrow> False" 

165 
"Dig1 m = Dig0 n \<longleftrightarrow> False" 

166 
"Dig1 m = Dig1 n \<longleftrightarrow> m = n" 

167 
by simp_all 

168 

29945  169 
lemma less_eq_num_code [numeral, simp, code]: 
170 
"One \<le> n \<longleftrightarrow> True" 

171 
"Dig0 m \<le> One \<longleftrightarrow> False" 

172 
"Dig1 m \<le> One \<longleftrightarrow> False" 

173 
"Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n" 

174 
"Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n" 

175 
"Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n" 

176 
"Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n" 

177 
using nat_of_num_pos [of n] nat_of_num_pos [of m] 

178 
by (auto simp add: less_eq_num_def less_num_def) 

179 

180 
lemma less_num_code [numeral, simp, code]: 

181 
"m < One \<longleftrightarrow> False" 

182 
"One < One \<longleftrightarrow> False" 

183 
"One < Dig0 n \<longleftrightarrow> True" 

184 
"One < Dig1 n \<longleftrightarrow> True" 

185 
"Dig0 m < Dig0 n \<longleftrightarrow> m < n" 

186 
"Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n" 

187 
"Dig1 m < Dig1 n \<longleftrightarrow> m < n" 

188 
"Dig1 m < Dig0 n \<longleftrightarrow> m < n" 

189 
using nat_of_num_pos [of n] nat_of_num_pos [of m] 

190 
by (auto simp add: less_eq_num_def less_num_def) 

191 

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

28021  193 

29945  194 
lemma add_One: "x + One = inc x" 
195 
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) 

196 

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

198 
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) 

199 

200 
lemma mult_One: "x * One = x" 

201 
by (simp add: num_eq_iff nat_of_num_mult) 

202 

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

204 
by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) 

205 

206 
text {* A doubleanddecrement function *} 

28021  207 

29945  208 
primrec DigM :: "num \<Rightarrow> num" where 
209 
"DigM One = One" 

210 
 "DigM (Dig0 n) = Dig1 (DigM n)" 

211 
 "DigM (Dig1 n) = Dig1 (Dig0 n)" 

28021  212 

29945  213 
lemma DigM_plus_one: "DigM n + One = Dig0 n" 
214 
by (induct n) simp_all 

215 

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

217 
by (induct n) simp_all 

218 

219 
lemma one_plus_DigM: "One + DigM n = Dig0 n" 

220 
unfolding add_One_commute DigM_plus_one .. 

28021  221 

29954  222 
text {* Squaring and exponentiation *} 
29947  223 

224 
primrec square :: "num \<Rightarrow> num" where 

225 
"square One = One" 

226 
 "square (Dig0 n) = Dig0 (Dig0 (square n))" 

227 
 "square (Dig1 n) = Dig1 (Dig0 (square n + n))" 

228 

29954  229 
primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" 
230 
where 

231 
"pow x One = x" 

232 
 "pow x (Dig0 y) = square (pow x y)" 

233 
 "pow x (Dig1 y) = x * square (pow x y)" 

29947  234 

28021  235 

236 
subsection {* Binary numerals *} 

237 

238 
text {* 

239 
We embed binary representations into a generic algebraic 

29934  240 
structure using @{text of_num}. 
28021  241 
*} 
242 

243 
class semiring_numeral = semiring + monoid_mult 

244 
begin 

245 

246 
primrec of_num :: "num \<Rightarrow> 'a" where 

31028  247 
of_num_One [numeral]: "of_num One = 1" 
28021  248 
 "of_num (Dig0 n) = of_num n + of_num n" 
249 
 "of_num (Dig1 n) = of_num n + of_num n + 1" 

250 

29943  251 
lemma of_num_inc: "of_num (inc x) = of_num x + 1" 
252 
by (induct x) (simp_all add: add_ac) 

253 

31028  254 
lemma of_num_add: "of_num (m + n) = of_num m + of_num n" 
255 
apply (induct n rule: num_induct) 

256 
apply (simp_all add: add_One add_inc of_num_inc add_ac) 

257 
done 

258 

259 
lemma of_num_mult: "of_num (m * n) = of_num m * of_num n" 

260 
apply (induct n rule: num_induct) 

261 
apply (simp add: mult_One) 

262 
apply (simp add: mult_inc of_num_add of_num_inc right_distrib) 

263 
done 

264 

28021  265 
declare of_num.simps [simp del] 
266 

267 
end 

268 

269 
text {* 

270 
ML stuff and syntax. 

271 
*} 

272 

273 
ML {* 

31027  274 
fun mk_num k = 
275 
if k > 1 then 

276 
let 

277 
val (l, b) = Integer.div_mod k 2; 

278 
val bit = (if b = 0 then @{term Dig0} else @{term Dig1}); 

279 
in bit $ (mk_num l) end 

280 
else if k = 1 then @{term One} 

281 
else error ("mk_num " ^ string_of_int k); 

28021  282 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

283 
fun dest_num @{term One} = 1 
28021  284 
 dest_num (@{term Dig0} $ n) = 2 * dest_num n 
31027  285 
 dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1 
286 
 dest_num t = raise TERM ("dest_num", [t]); 

28021  287 

288 
(*FIXME these have to gain proper context via morphisms phi*) 

289 

290 
fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} > T) 

291 
$ mk_num k 

292 

293 
fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) = 

294 
(T, dest_num t) 

295 
*} 

296 

297 
syntax 

298 
"_Numerals" :: "xnum \<Rightarrow> 'a" ("_") 

299 

300 
parse_translation {* 

301 
let 

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

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

303 
of (0, 1) => Const (@{const_name One}, dummyT) 
28021  304 
 (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n 
305 
 (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n 

306 
else raise Match; 

307 
fun numeral_tr [Free (num, _)] = 

308 
let 

309 
val {leading_zeros, value, ...} = Syntax.read_xnum num; 

310 
val _ = leading_zeros = 0 andalso value > 0 

311 
orelse error ("Bad numeral: " ^ num); 

312 
in Const (@{const_name of_num}, @{typ num} > dummyT) $ num_of_int value end 

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

35113  314 
in [(@{syntax_const "_Numerals"}, numeral_tr)] end 
28021  315 
*} 
316 

317 
typed_print_translation {* 

318 
let 

319 
fun dig b n = b + 2 * n; 

320 
fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) = 

321 
dig 0 (int_of_num' n) 

322 
 int_of_num' (Const (@{const_syntax Dig1}, _) $ n) = 

323 
dig 1 (int_of_num' n) 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

324 
 int_of_num' (Const (@{const_syntax One}, _)) = 1; 
28021  325 
fun num_tr' show_sorts T [n] = 
326 
let 

327 
val k = int_of_num' n; 

35113  328 
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k); 
28021  329 
in case T 
35430
df2862dc23a8
adapted to authentic syntax  actual types are verbatim;
wenzelm
parents:
35363
diff
changeset

330 
of Type (@{type_name fun}, [_, T']) => 
28021  331 
if not (! show_types) andalso can Term.dest_Type T' then t' 
332 
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T' 

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

334 
end; 

335 
in [(@{const_syntax of_num}, num_tr')] end 

336 
*} 

337 

29945  338 
subsection {* Classspecific numeral rules *} 
28021  339 

340 
text {* 

341 
@{const of_num} is a morphism. 

342 
*} 

343 

29945  344 
subsubsection {* Class @{text semiring_numeral} *} 
345 

28021  346 
context semiring_numeral 
347 
begin 

348 

29943  349 
abbreviation "Num1 \<equiv> of_num One" 
28021  350 

351 
text {* 

352 
Alas, there is still the duplication of @{term 1}, 

353 
thought the duplicated @{term 0} has disappeared. 

354 
We could get rid of it by replacing the constructor 

355 
@{term 1} in @{typ num} by two constructors 

356 
@{text two} and @{text three}, resulting in a further 

357 
blowup. But it could be worth the effort. 

358 
*} 

359 

360 
lemma of_num_plus_one [numeral]: 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

361 
"of_num n + 1 = of_num (n + One)" 
31028  362 
by (simp only: of_num_add of_num_One) 
28021  363 

364 
lemma of_num_one_plus [numeral]: 

31028  365 
"1 + of_num n = of_num (One + n)" 
366 
by (simp only: of_num_add of_num_One) 

28021  367 

368 
lemma of_num_plus [numeral]: 

369 
"of_num m + of_num n = of_num (m + n)" 

31028  370 
unfolding of_num_add .. 
28021  371 

372 
lemma of_num_times_one [numeral]: 

373 
"of_num n * 1 = of_num n" 

374 
by simp 

375 

376 
lemma of_num_one_times [numeral]: 

377 
"1 * of_num n = of_num n" 

378 
by simp 

379 

380 
lemma of_num_times [numeral]: 

381 
"of_num m * of_num n = of_num (m * n)" 

31028  382 
unfolding of_num_mult .. 
28021  383 

384 
end 

385 

29945  386 
subsubsection {* 
29947  387 
Structures with a zero: class @{text semiring_1} 
28021  388 
*} 
389 

390 
context semiring_1 

391 
begin 

392 

393 
subclass semiring_numeral .. 

394 

395 
lemma of_nat_of_num [numeral]: "of_nat (of_num n) = of_num n" 

396 
by (induct n) 

397 
(simp_all add: semiring_numeral_class.of_num.simps of_num.simps add_ac) 

398 

399 
declare of_nat_1 [numeral] 

400 

401 
lemma Dig_plus_zero [numeral]: 

402 
"0 + 1 = 1" 

403 
"0 + of_num n = of_num n" 

404 
"1 + 0 = 1" 

405 
"of_num n + 0 = of_num n" 

406 
by simp_all 

407 

408 
lemma Dig_times_zero [numeral]: 

409 
"0 * 1 = 0" 

410 
"0 * of_num n = 0" 

411 
"1 * 0 = 0" 

412 
"of_num n * 0 = 0" 

413 
by simp_all 

414 

415 
end 

416 

417 
lemma nat_of_num_of_num: "nat_of_num = of_num" 

418 
proof 

419 
fix n 

29943  420 
have "of_num n = nat_of_num n" 
421 
by (induct n) (simp_all add: of_num.simps) 

28021  422 
then show "nat_of_num n = of_num n" by simp 
423 
qed 

424 

29945  425 
subsubsection {* 
426 
Equality: class @{text semiring_char_0} 

28021  427 
*} 
428 

429 
context semiring_char_0 

430 
begin 

431 

31028  432 
lemma of_num_eq_iff [numeral]: "of_num m = of_num n \<longleftrightarrow> m = n" 
28021  433 
unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric] 
29943  434 
of_nat_eq_iff num_eq_iff .. 
28021  435 

31028  436 
lemma of_num_eq_one_iff [numeral]: "of_num n = 1 \<longleftrightarrow> n = One" 
437 
using of_num_eq_iff [of n One] by (simp add: of_num_One) 

28021  438 

31028  439 
lemma one_eq_of_num_iff [numeral]: "1 = of_num n \<longleftrightarrow> One = n" 
440 
using of_num_eq_iff [of One n] by (simp add: of_num_One) 

28021  441 

442 
end 

443 

29945  444 
subsubsection {* 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

445 
Comparisons: class @{text linordered_semidom} 
28021  446 
*} 
447 

29945  448 
text {* Could be perhaps more general than here. *} 
449 

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

450 
context linordered_semidom 
28021  451 
begin 
452 

29991  453 
lemma of_num_pos [numeral]: "0 < of_num n" 
454 
by (induct n) (simp_all add: of_num.simps add_pos_pos) 

455 

28021  456 
lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n" 
457 
proof  

458 
have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n" 

459 
unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff .. 

460 
then show ?thesis by (simp add: of_nat_of_num) 

461 
qed 

462 

31028  463 
lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n \<le> One" 
464 
using of_num_less_eq_iff [of n One] by (simp add: of_num_One) 

28021  465 

466 
lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n" 

31028  467 
using of_num_less_eq_iff [of One n] by (simp add: of_num_One) 
28021  468 

469 
lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n" 

470 
proof  

471 
have "of_nat (of_num m) < of_nat (of_num n) \<longleftrightarrow> m < n" 

472 
unfolding less_num_def nat_of_num_of_num of_nat_less_iff .. 

473 
then show ?thesis by (simp add: of_nat_of_num) 

474 
qed 

475 

476 
lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1" 

31028  477 
using of_num_less_iff [of n One] by (simp add: of_num_One) 
28021  478 

31028  479 
lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> One < n" 
480 
using of_num_less_iff [of One n] by (simp add: of_num_One) 

28021  481 

29991  482 
lemma of_num_nonneg [numeral]: "0 \<le> of_num n" 
483 
by (induct n) (simp_all add: of_num.simps add_nonneg_nonneg) 

484 

485 
lemma of_num_less_zero_iff [numeral]: "\<not> of_num n < 0" 

486 
by (simp add: not_less of_num_nonneg) 

487 

488 
lemma of_num_le_zero_iff [numeral]: "\<not> of_num n \<le> 0" 

489 
by (simp add: not_le of_num_pos) 

490 

491 
end 

492 

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

493 
context linordered_idom 
29991  494 
begin 
495 

30792  496 
lemma minus_of_num_less_of_num_iff: " of_num m < of_num n" 
29991  497 
proof  
498 
have " of_num m < 0" by (simp add: of_num_pos) 

499 
also have "0 < of_num n" by (simp add: of_num_pos) 

500 
finally show ?thesis . 

501 
qed 

502 

30792  503 
lemma minus_of_num_less_one_iff: " of_num n < 1" 
31028  504 
using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One) 
29991  505 

30792  506 
lemma minus_one_less_of_num_iff: " 1 < of_num n" 
31028  507 
using minus_of_num_less_of_num_iff [of One n] by (simp add: of_num_One) 
29991  508 

30792  509 
lemma minus_one_less_one_iff: " 1 < 1" 
31028  510 
using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_One) 
30792  511 

512 
lemma minus_of_num_le_of_num_iff: " of_num m \<le> of_num n" 

29991  513 
by (simp add: less_imp_le minus_of_num_less_of_num_iff) 
514 

30792  515 
lemma minus_of_num_le_one_iff: " of_num n \<le> 1" 
29991  516 
by (simp add: less_imp_le minus_of_num_less_one_iff) 
517 

30792  518 
lemma minus_one_le_of_num_iff: " 1 \<le> of_num n" 
29991  519 
by (simp add: less_imp_le minus_one_less_of_num_iff) 
520 

30792  521 
lemma minus_one_le_one_iff: " 1 \<le> 1" 
522 
by (simp add: less_imp_le minus_one_less_one_iff) 

523 

524 
lemma of_num_le_minus_of_num_iff: "\<not> of_num m \<le>  of_num n" 

29991  525 
by (simp add: not_le minus_of_num_less_of_num_iff) 
526 

30792  527 
lemma one_le_minus_of_num_iff: "\<not> 1 \<le>  of_num n" 
29991  528 
by (simp add: not_le minus_of_num_less_one_iff) 
529 

30792  530 
lemma of_num_le_minus_one_iff: "\<not> of_num n \<le>  1" 
29991  531 
by (simp add: not_le minus_one_less_of_num_iff) 
532 

30792  533 
lemma one_le_minus_one_iff: "\<not> 1 \<le>  1" 
534 
by (simp add: not_le minus_one_less_one_iff) 

535 

536 
lemma of_num_less_minus_of_num_iff: "\<not> of_num m <  of_num n" 

29991  537 
by (simp add: not_less minus_of_num_le_of_num_iff) 
538 

30792  539 
lemma one_less_minus_of_num_iff: "\<not> 1 <  of_num n" 
29991  540 
by (simp add: not_less minus_of_num_le_one_iff) 
541 

30792  542 
lemma of_num_less_minus_one_iff: "\<not> of_num n <  1" 
29991  543 
by (simp add: not_less minus_one_le_of_num_iff) 
544 

30792  545 
lemma one_less_minus_one_iff: "\<not> 1 <  1" 
546 
by (simp add: not_less minus_one_le_one_iff) 

547 

548 
lemmas le_signed_numeral_special [numeral] = 

549 
minus_of_num_le_of_num_iff 

550 
minus_of_num_le_one_iff 

551 
minus_one_le_of_num_iff 

552 
minus_one_le_one_iff 

553 
of_num_le_minus_of_num_iff 

554 
one_le_minus_of_num_iff 

555 
of_num_le_minus_one_iff 

556 
one_le_minus_one_iff 

557 

558 
lemmas less_signed_numeral_special [numeral] = 

559 
minus_of_num_less_of_num_iff 

560 
minus_of_num_less_one_iff 

561 
minus_one_less_of_num_iff 

562 
minus_one_less_one_iff 

563 
of_num_less_minus_of_num_iff 

564 
one_less_minus_of_num_iff 

565 
of_num_less_minus_one_iff 

566 
one_less_minus_one_iff 

567 

28021  568 
end 
569 

29945  570 
subsubsection {* 
29947  571 
Structures with subtraction: class @{text semiring_1_minus} 
28021  572 
*} 
573 

574 
class semiring_minus = semiring + minus + zero + 

575 
assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c  b = a" 

576 
assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b  c = 0  a" 

577 
begin 

578 

579 
lemma minus_inverts_plus2: "a + b = c \<Longrightarrow> c  a = b" 

580 
by (simp add: add_ac minus_inverts_plus1 [of b a]) 

581 

582 
lemma minus_minus_zero_inverts_plus2: "a + b = c \<Longrightarrow> a  c = 0  b" 

583 
by (simp add: add_ac minus_minus_zero_inverts_plus1 [of b a]) 

584 

585 
end 

586 

587 
class semiring_1_minus = semiring_1 + semiring_minus 

588 
begin 

589 

590 
lemma Dig_of_num_pos: 

591 
assumes "k + n = m" 

592 
shows "of_num m  of_num n = of_num k" 

593 
using assms by (simp add: of_num_plus minus_inverts_plus1) 

594 

595 
lemma Dig_of_num_zero: 

596 
shows "of_num n  of_num n = 0" 

597 
by (rule minus_inverts_plus1) simp 

598 

599 
lemma Dig_of_num_neg: 

600 
assumes "k + m = n" 

601 
shows "of_num m  of_num n = 0  of_num k" 

602 
by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms) 

603 

604 
lemmas Dig_plus_eval = 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

605 
of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject 
28021  606 

607 
simproc_setup numeral_minus ("of_num m  of_num n") = {* 

608 
let 

609 
(*TODO proper implicit use of morphism via pattern antiquotations*) 

610 
fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct; 

611 
fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n); 

612 
fun attach_num ct = (dest_num (Thm.term_of ct), ct); 

613 
fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t; 

614 
val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval}); 

615 
fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"}, 

616 
[Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]]; 

617 
in fn phi => fn _ => fn ct => case try cdifference ct 

618 
of NONE => (NONE) 

619 
 SOME ((k, ck), (l, cl)) => SOME (let val j = k  l in if j = 0 

620 
then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct 

621 
else mk_meta_eq (let 

622 
val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j)); 

623 
in 

624 
(if j > 0 then (Morphism.thm phi @{thm Dig_of_num_pos}) OF [cert cj cl ck] 

625 
else (Morphism.thm phi @{thm Dig_of_num_neg}) OF [cert cj ck cl]) 

626 
end) end) 

627 
end 

628 
*} 

629 

630 
lemma Dig_of_num_minus_zero [numeral]: 

631 
"of_num n  0 = of_num n" 

632 
by (simp add: minus_inverts_plus1) 

633 

634 
lemma Dig_one_minus_zero [numeral]: 

635 
"1  0 = 1" 

636 
by (simp add: minus_inverts_plus1) 

637 

638 
lemma Dig_one_minus_one [numeral]: 

639 
"1  1 = 0" 

640 
by (simp add: minus_inverts_plus1) 

641 

642 
lemma Dig_of_num_minus_one [numeral]: 

29941  643 
"of_num (Dig0 n)  1 = of_num (DigM n)" 
28021  644 
"of_num (Dig1 n)  1 = of_num (Dig0 n)" 
29941  645 
by (auto intro: minus_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) 
28021  646 

647 
lemma Dig_one_minus_of_num [numeral]: 

29941  648 
"1  of_num (Dig0 n) = 0  of_num (DigM n)" 
28021  649 
"1  of_num (Dig1 n) = 0  of_num (Dig0 n)" 
29941  650 
by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) 
28021  651 

652 
end 

653 

29945  654 
subsubsection {* 
29947  655 
Structures with negation: class @{text ring_1} 
29945  656 
*} 
657 

28021  658 
context ring_1 
659 
begin 

660 

661 
subclass semiring_1_minus 

29667  662 
proof qed (simp_all add: algebra_simps) 
28021  663 

664 
lemma Dig_zero_minus_of_num [numeral]: 

665 
"0  of_num n =  of_num n" 

666 
by simp 

667 

668 
lemma Dig_zero_minus_one [numeral]: 

669 
"0  1 =  1" 

670 
by simp 

671 

672 
lemma Dig_uminus_uminus [numeral]: 

673 
" ( of_num n) = of_num n" 

674 
by simp 

675 

676 
lemma Dig_plus_uminus [numeral]: 

677 
"of_num m +  of_num n = of_num m  of_num n" 

678 
" of_num m + of_num n = of_num n  of_num m" 

679 
" of_num m +  of_num n =  (of_num m + of_num n)" 

680 
"of_num m   of_num n = of_num m + of_num n" 

681 
" of_num m  of_num n =  (of_num m + of_num n)" 

682 
" of_num m   of_num n = of_num n  of_num m" 

683 
by (simp_all add: diff_minus add_commute) 

684 

685 
lemma Dig_times_uminus [numeral]: 

686 
" of_num n * of_num m =  (of_num n * of_num m)" 

687 
"of_num n *  of_num m =  (of_num n * of_num m)" 

688 
" of_num n *  of_num m = of_num n * of_num m" 

31028  689 
by simp_all 
28021  690 

691 
lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n" 

692 
by (induct n) 

693 
(simp_all only: of_num.simps semiring_numeral_class.of_num.simps of_int_add, simp_all) 

694 

695 
declare of_int_1 [numeral] 

696 

697 
end 

698 

29945  699 
subsubsection {* 
29954  700 
Structures with exponentiation 
701 
*} 

702 

703 
lemma of_num_square: "of_num (square x) = of_num x * of_num x" 

704 
by (induct x) 

31028  705 
(simp_all add: of_num.simps of_num_add algebra_simps) 
29954  706 

31028  707 
lemma of_num_pow: "of_num (pow x y) = of_num x ^ of_num y" 
29954  708 
by (induct y) 
31028  709 
(simp_all add: of_num.simps of_num_square of_num_mult power_add) 
29954  710 

31028  711 
lemma power_of_num [numeral]: "of_num x ^ of_num y = of_num (pow x y)" 
712 
unfolding of_num_pow .. 

29954  713 

714 
lemma power_zero_of_num [numeral]: 

31029  715 
"0 ^ of_num n = (0::'a::semiring_1)" 
29954  716 
using of_num_pos [where n=n and ?'a=nat] 
717 
by (simp add: power_0_left) 

718 

719 
lemma power_minus_Dig0 [numeral]: 

31029  720 
fixes x :: "'a::ring_1" 
29954  721 
shows "( x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)" 
31028  722 
by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) 
29954  723 

724 
lemma power_minus_Dig1 [numeral]: 

31029  725 
fixes x :: "'a::ring_1" 
29954  726 
shows "( x) ^ of_num (Dig1 n) =  (x ^ of_num (Dig1 n))" 
31028  727 
by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) 
29954  728 

729 
declare power_one [numeral] 

730 

731 

732 
subsubsection {* 

28021  733 
Greetings to @{typ nat}. 
734 
*} 

735 

736 
instance nat :: semiring_1_minus proof qed simp_all 

737 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

738 
lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)" 
28021  739 
unfolding of_num_plus_one [symmetric] by simp 
740 

741 
lemma nat_number: 

742 
"1 = Suc 0" 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

743 
"of_num One = Suc 0" 
29941  744 
"of_num (Dig0 n) = Suc (of_num (DigM n))" 
28021  745 
"of_num (Dig1 n) = Suc (of_num (Dig0 n))" 
29941  746 
by (simp_all add: of_num.simps DigM_plus_one Suc_of_num) 
28021  747 

748 
declare diff_0_eq_0 [numeral] 

749 

750 

751 
subsection {* Code generator setup for @{typ int} *} 

752 

753 
definition Pls :: "num \<Rightarrow> int" where 

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

754 
[simp, code_post]: "Pls n = of_num n" 
28021  755 

756 
definition Mns :: "num \<Rightarrow> int" where 

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

757 
[simp, code_post]: "Mns n =  of_num n" 
28021  758 

759 
code_datatype "0::int" Pls Mns 

760 

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

761 
lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric] 
28021  762 

763 
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where 

37765  764 
[simp]: "sub m n = (of_num m  of_num n)" 
28021  765 

766 
definition dup :: "int \<Rightarrow> int" where 

37765  767 
"dup k = 2 * k" 
28021  768 

769 
lemma Dig_sub [code]: 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

770 
"sub One One = 0" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

771 
"sub (Dig0 m) One = of_num (DigM m)" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

772 
"sub (Dig1 m) One = of_num (Dig0 m)" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

773 
"sub One (Dig0 n) =  of_num (DigM n)" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

774 
"sub One (Dig1 n) =  of_num (Dig0 n)" 
28021  775 
"sub (Dig0 m) (Dig0 n) = dup (sub m n)" 
776 
"sub (Dig1 m) (Dig1 n) = dup (sub m n)" 

777 
"sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1" 

778 
"sub (Dig0 m) (Dig1 n) = dup (sub m n)  1" 

29667  779 
apply (simp_all add: dup_def algebra_simps) 
29941  780 
apply (simp_all add: of_num_plus one_plus_DigM)[4] 
28021  781 
apply (simp_all add: of_num.simps) 
782 
done 

783 

784 
lemma dup_code [code]: 

785 
"dup 0 = 0" 

786 
"dup (Pls n) = Pls (Dig0 n)" 

787 
"dup (Mns n) = Mns (Dig0 n)" 

788 
by (simp_all add: dup_def of_num.simps) 

789 

28562  790 
lemma [code, code del]: 
28021  791 
"(1 :: int) = 1" 
792 
"(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +" 

793 
"(uminus :: int \<Rightarrow> int) = uminus" 

794 
"(op  :: int \<Rightarrow> int \<Rightarrow> int) = op " 

795 
"(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *" 

28367  796 
"(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq" 
28021  797 
"(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>" 
798 
"(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <" 

799 
by rule+ 

800 

801 
lemma one_int_code [code]: 

29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

802 
"1 = Pls One" 
31028  803 
by (simp add: of_num_One) 
28021  804 

805 
lemma plus_int_code [code]: 

806 
"k + 0 = (k::int)" 

807 
"0 + l = (l::int)" 

808 
"Pls m + Pls n = Pls (m + n)" 

809 
"Pls m  Pls n = sub m n" 

810 
"Mns m + Mns n = Mns (m + n)" 

811 
"Mns m  Mns n = sub n m" 

31028  812 
by (simp_all add: of_num_add) 
28021  813 

814 
lemma uminus_int_code [code]: 

815 
"uminus 0 = (0::int)" 

816 
"uminus (Pls m) = Mns m" 

817 
"uminus (Mns m) = Pls m" 

818 
by simp_all 

819 

820 
lemma minus_int_code [code]: 

821 
"k  0 = (k::int)" 

822 
"0  l = uminus (l::int)" 

823 
"Pls m  Pls n = sub m n" 

824 
"Pls m  Mns n = Pls (m + n)" 

825 
"Mns m  Pls n = Mns (m + n)" 

826 
"Mns m  Mns n = sub n m" 

31028  827 
by (simp_all add: of_num_add) 
28021  828 

829 
lemma times_int_code [code]: 

830 
"k * 0 = (0::int)" 

831 
"0 * l = (0::int)" 

832 
"Pls m * Pls n = Pls (m * n)" 

833 
"Pls m * Mns n = Mns (m * n)" 

834 
"Mns m * Pls n = Mns (m * n)" 

835 
"Mns m * Mns n = Pls (m * n)" 

31028  836 
by (simp_all add: of_num_mult) 
28021  837 

838 
lemma eq_int_code [code]: 

28367  839 
"eq_class.eq 0 (0::int) \<longleftrightarrow> True" 
840 
"eq_class.eq 0 (Pls l) \<longleftrightarrow> False" 

841 
"eq_class.eq 0 (Mns l) \<longleftrightarrow> False" 

842 
"eq_class.eq (Pls k) 0 \<longleftrightarrow> False" 

843 
"eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l" 

844 
"eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False" 

845 
"eq_class.eq (Mns k) 0 \<longleftrightarrow> False" 

846 
"eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False" 

847 
"eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l" 

28021  848 
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] 
28367  849 
by (simp_all add: of_num_eq_iff eq) 
28021  850 

851 
lemma less_eq_int_code [code]: 

852 
"0 \<le> (0::int) \<longleftrightarrow> True" 

853 
"0 \<le> Pls l \<longleftrightarrow> True" 

854 
"0 \<le> Mns l \<longleftrightarrow> False" 

855 
"Pls k \<le> 0 \<longleftrightarrow> False" 

856 
"Pls k \<le> Pls l \<longleftrightarrow> k \<le> l" 

857 
"Pls k \<le> Mns l \<longleftrightarrow> False" 

858 
"Mns k \<le> 0 \<longleftrightarrow> True" 

859 
"Mns k \<le> Pls l \<longleftrightarrow> True" 

860 
"Mns k \<le> Mns l \<longleftrightarrow> l \<le> k" 

861 
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] 

862 
by (simp_all add: of_num_less_eq_iff) 

863 

864 
lemma less_int_code [code]: 

865 
"0 < (0::int) \<longleftrightarrow> False" 

866 
"0 < Pls l \<longleftrightarrow> True" 

867 
"0 < Mns l \<longleftrightarrow> False" 

868 
"Pls k < 0 \<longleftrightarrow> False" 

869 
"Pls k < Pls l \<longleftrightarrow> k < l" 

870 
"Pls k < Mns l \<longleftrightarrow> False" 

871 
"Mns k < 0 \<longleftrightarrow> True" 

872 
"Mns k < Pls l \<longleftrightarrow> True" 

873 
"Mns k < Mns l \<longleftrightarrow> l < k" 

874 
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] 

875 
by (simp_all add: of_num_less_iff) 

876 

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

877 
lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp 
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

878 
lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp 
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

879 
declare zero_is_num_zero [code_unfold del] 
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

880 
declare one_is_num_one [code_unfold del] 
28021  881 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35430
diff
changeset

882 
hide_const (open) sub dup 
28021  883 

884 

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

886 

31029  887 
declare (in semiring_numeral) of_num_One [simp] 
888 
declare (in semiring_numeral) of_num_plus_one [simp] 

889 
declare (in semiring_numeral) of_num_one_plus [simp] 

890 
declare (in semiring_numeral) of_num_plus [simp] 

891 
declare (in semiring_numeral) of_num_times [simp] 

892 

893 
declare (in semiring_1) of_nat_of_num [simp] 

894 

895 
declare (in semiring_char_0) of_num_eq_iff [simp] 

896 
declare (in semiring_char_0) of_num_eq_one_iff [simp] 

897 
declare (in semiring_char_0) one_eq_of_num_iff [simp] 

898 

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

899 
declare (in linordered_semidom) of_num_pos [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

900 
declare (in linordered_semidom) of_num_less_eq_iff [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

901 
declare (in linordered_semidom) of_num_less_eq_one_iff [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

902 
declare (in linordered_semidom) one_less_eq_of_num_iff [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

903 
declare (in linordered_semidom) of_num_less_iff [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

904 
declare (in linordered_semidom) of_num_less_one_iff [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

905 
declare (in linordered_semidom) one_less_of_num_iff [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

906 
declare (in linordered_semidom) of_num_nonneg [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

907 
declare (in linordered_semidom) of_num_less_zero_iff [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

908 
declare (in linordered_semidom) of_num_le_zero_iff [simp] 
31029  909 

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

910 
declare (in linordered_idom) le_signed_numeral_special [simp] 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33523
diff
changeset

911 
declare (in linordered_idom) less_signed_numeral_special [simp] 
31029  912 

913 
declare (in semiring_1_minus) Dig_of_num_minus_one [simp] 

914 
declare (in semiring_1_minus) Dig_one_minus_of_num [simp] 

915 

916 
declare (in ring_1) Dig_plus_uminus [simp] 

917 
declare (in ring_1) of_int_of_num [simp] 

918 

919 
declare power_of_num [simp] 

920 
declare power_zero_of_num [simp] 

921 
declare power_minus_Dig0 [simp] 

922 
declare power_minus_Dig1 [simp] 

923 

924 
declare Suc_of_num [simp] 

925 

28021  926 

31025  927 
subsection {* Simplification Procedures *} 
928 

31026
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

929 
subsubsection {* Reorientation of equalities *} 
31025  930 

931 
setup {* 

33523  932 
Reorient_Proc.add 
31025  933 
(fn Const(@{const_name of_num}, _) $ _ => true 
934 
 Const(@{const_name uminus}, _) $ 

935 
(Const(@{const_name of_num}, _) $ _) => true 

936 
 _ => false) 

937 
*} 

938 

33523  939 
simproc_setup reorient_num ("of_num n = x"  " of_num m = y") = Reorient_Proc.proc 
940 

31025  941 

31026
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

942 
subsubsection {* Constant folding for multiplication in semirings *} 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

943 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

944 
context semiring_numeral 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

945 
begin 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

946 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

947 
lemma mult_of_num_commute: "x * of_num n = of_num n * x" 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

948 
by (induct n) 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

949 
(simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right) 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

950 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

951 
definition 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

952 
"commutes_with a b \<longleftrightarrow> a * b = b * a" 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

953 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

954 
lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a" 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

955 
unfolding commutes_with_def . 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

956 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

957 
lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)" 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

958 
unfolding commutes_with_def by (simp only: mult_assoc [symmetric]) 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

959 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

960 
lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x" 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

961 
unfolding commutes_with_def by (simp_all add: mult_of_num_commute) 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

962 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

963 
lemmas mult_ac_numeral = 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

964 
mult_assoc 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

965 
commutes_with_commute 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

966 
commutes_with_left_commute 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

967 
commutes_with_numeral 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

968 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

969 
end 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

970 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

971 
ML {* 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

972 
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

973 
struct 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

974 
val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral} 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

975 
val eq_reflection = eq_reflection 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

976 
fun is_numeral (Const(@{const_name of_num}, _) $ _) = true 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

977 
 is_numeral _ = false; 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

978 
end; 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

979 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

980 
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

981 
*} 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

982 

020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

983 
simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") = 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

984 
{* fn phi => fn ss => fn ct => 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

985 
Semiring_Times_Assoc.proc ss (Thm.term_of ct) *} 
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset

986 

31025  987 

988 
subsection {* Toy examples *} 

28021  989 

990 
definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int)  #3" 

37826  991 

28021  992 
code_thms bar 
37826  993 

994 
export_code bar checking SML OCaml? Haskell? 

28021  995 

996 
end 