author  huffman 
Mon, 16 Feb 2009 12:53:59 0800  
changeset 29942  31069b8d39df 
parent 29941  b951d80774d5 
child 29943  922b931fd2eb 
permissions  rwrr 
28021  1 
(* Title: HOL/ex/Numeral.thy 
2 
ID: $Id$ 

3 
Author: Florian Haftmann 

4 

5 
An experimental alternative numeral representation. 

6 
*) 

7 

8 
theory Numeral 

9 
imports Int Inductive 

10 
begin 

11 

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

13 

14 
text {* 

15 
We construct @{text num} as a copy of strictly positive 

16 
natural numbers. 

17 
*} 

18 

19 
typedef (open) num = "\<lambda>n\<Colon>nat. n > 0" 

20 
morphisms nat_of_num num_of_nat_abs 

21 
by (auto simp add: mem_def) 

22 

23 
text {* 

24 
A totalized abstraction function. It is not entirely clear 

25 
whether this is really useful. 

26 
*} 

27 

28 
definition num_of_nat :: "nat \<Rightarrow> num" where 

29 
"num_of_nat n = (if n = 0 then num_of_nat_abs 1 else num_of_nat_abs n)" 

30 

31 
lemma num_cases [case_names nat, cases type: num]: 

32 
assumes "(\<And>n\<Colon>nat. m = num_of_nat n \<Longrightarrow> 0 < n \<Longrightarrow> P)" 

33 
shows P 

34 
apply (rule num_of_nat_abs_cases) 

35 
apply (unfold mem_def) 

36 
using assms unfolding num_of_nat_def 

37 
apply auto 

38 
done 

39 

40 
lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1" 

41 
by (simp add: num_of_nat_def) 

42 

43 
lemma num_of_nat_inverse: "nat_of_num (num_of_nat n) = (if n = 0 then 1 else n)" 

44 
apply (simp add: num_of_nat_def) 

45 
apply (subst num_of_nat_abs_inverse) 

46 
apply (auto simp add: mem_def num_of_nat_abs_inverse) 

47 
done 

48 

49 
lemma num_of_nat_inject: 

50 
"num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)" 

51 
by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def]) 

52 

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

53 
lemma nat_of_num_gt_0: "0 < nat_of_num x" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

54 
using nat_of_num [of x, unfolded mem_def] . 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

55 

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

56 
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

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

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

59 
apply (simp add: nat_of_num_inverse) 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

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

61 

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

62 

28021  63 
lemma split_num_all: 
64 
"(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))" 

65 
proof 

66 
fix n 

67 
assume "\<And>m\<Colon>num. PROP P m" 

68 
then show "PROP P (num_of_nat n)" . 

69 
next 

70 
fix m 

71 
have nat_of_num: "\<And>m. nat_of_num m \<noteq> 0" 

72 
using nat_of_num by (auto simp add: mem_def) 

73 
have nat_of_num_inverse: "\<And>m. num_of_nat (nat_of_num m) = m" 

74 
by (auto simp add: num_of_nat_def nat_of_num_inverse nat_of_num) 

75 
assume "\<And>n. PROP P (num_of_nat n)" 

76 
then have "PROP P (num_of_nat (nat_of_num m))" . 

77 
then show "PROP P m" unfolding nat_of_num_inverse . 

78 
qed 

79 

80 

81 
subsection {* Digit representation for @{typ num} *} 

82 

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

83 
instantiation num :: "semiring" 
28021  84 
begin 
85 

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

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

87 
one_num_def [code del]: "One = num_of_nat 1" 
28021  88 

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

28562  90 
[code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)" 
28021  91 

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

28562  93 
[code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)" 
28021  94 

95 
definition Dig0 :: "num \<Rightarrow> num" where 

28562  96 
[code del]: "Dig0 n = n + n" 
28021  97 

98 
definition Dig1 :: "num \<Rightarrow> num" where 

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

99 
[code del]: "Dig1 n = n + n + One" 
28021  100 

101 
instance proof 

102 
qed (simp_all add: one_num_def plus_num_def times_num_def 

103 
split_num_all num_of_nat_inverse num_of_nat_zero add_ac mult_ac nat_distrib) 

104 

105 
end 

106 

107 
text {* 

108 
The following proofs seem horribly complicated. 

109 
Any room for simplification!? 

110 
*} 

111 

112 
lemma nat_dig_cases [case_names 0 1 dig0 dig1]: 

113 
fixes n :: nat 

114 
assumes "n = 0 \<Longrightarrow> P" 

115 
and "n = 1 \<Longrightarrow> P" 

116 
and "\<And>m. m > 0 \<Longrightarrow> n = m + m \<Longrightarrow> P" 

117 
and "\<And>m. m > 0 \<Longrightarrow> n = Suc (m + m) \<Longrightarrow> P" 

118 
shows P 

119 
using assms proof (induct n) 

120 
case 0 then show ?case by simp 

121 
next 

122 
case (Suc n) 

123 
show P proof (rule Suc.hyps) 

124 
assume "n = 0" 

125 
then have "Suc n = 1" by simp 

126 
then show P by (rule Suc.prems(2)) 

127 
next 

128 
assume "n = 1" 

129 
have "1 > (0\<Colon>nat)" by simp 

130 
moreover from `n = 1` have "Suc n = 1 + 1" by simp 

131 
ultimately show P by (rule Suc.prems(3)) 

132 
next 

133 
fix m 

134 
assume "0 < m" and "n = m + m" 

135 
note `0 < m` 

136 
moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp 

137 
ultimately show P by (rule Suc.prems(4)) 

138 
next 

139 
fix m 

140 
assume "0 < m" and "n = Suc (m + m)" 

141 
have "0 < Suc m" by simp 

142 
moreover from `n = Suc (m + m)` have "Suc n = Suc m + Suc m" by simp 

143 
ultimately show P by (rule Suc.prems(3)) 

144 
qed 

145 
qed 

146 

147 
lemma num_induct_raw: 

148 
fixes n :: nat 

149 
assumes not0: "n > 0" 

150 
assumes "P 1" 

151 
and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (n + n)" 

152 
and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc (n + n))" 

153 
shows "P n" 

154 
using not0 proof (induct n rule: less_induct) 

155 
case (less n) 

156 
show "P n" proof (cases n rule: nat_dig_cases) 

157 
case 0 then show ?thesis using less by simp 

158 
next 

159 
case 1 then show ?thesis using assms by simp 

160 
next 

161 
case (dig0 m) 

162 
then show ?thesis apply simp 

163 
apply (rule assms(3)) apply assumption 

164 
apply (rule less) 

165 
apply simp_all 

166 
done 

167 
next 

168 
case (dig1 m) 

169 
then show ?thesis apply simp 

170 
apply (rule assms(4)) apply assumption 

171 
apply (rule less) 

172 
apply simp_all 

173 
done 

174 
qed 

175 
qed 

176 

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

177 
lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then One else num_of_nat n + One)" 
28021  178 
by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse) 
179 

180 
lemma num_induct [case_names 1 Suc, induct type: num]: 

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

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

182 
assumes 1: "P One" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

183 
and Suc: "\<And>n. P n \<Longrightarrow> P (n + One)" 
28021  184 
shows "P n" 
185 
proof (cases n) 

186 
case (nat m) then show ?thesis by (induct m arbitrary: n) 

187 
(auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm) 

188 
qed 

189 

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

190 
rep_datatype One Dig0 Dig1 proof  
28021  191 
fix P m 
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

192 
assume 1: "P One" 
28021  193 
and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)" 
194 
and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)" 

195 
obtain n where "0 < n" and m: "m = num_of_nat n" 

196 
by (cases m) auto 

197 
from `0 < n` have "P (num_of_nat n)" proof (induct n rule: num_induct_raw) 

198 
case 1 from `0 < n` show ?case . 

199 
next 

200 
case 2 with 1 show ?case by (simp add: one_num_def) 

201 
next 

202 
case (3 n) then have "P (num_of_nat n)" by auto 

203 
then have "P (Dig0 (num_of_nat n))" by (rule Dig0) 

204 
with 3 show ?case by (simp add: Dig0_def plus_num_def num_of_nat_inverse) 

205 
next 

206 
case (4 n) then have "P (num_of_nat n)" by auto 

207 
then have "P (Dig1 (num_of_nat n))" by (rule Dig1) 

208 
with 4 show ?case by (simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse) 

209 
qed 

210 
with m show "P m" by simp 

211 
next 

212 
fix m n 

213 
show "Dig0 m = Dig0 n \<longleftrightarrow> m = n" 

214 
apply (cases m) apply (cases n) 

215 
by (auto simp add: Dig0_def plus_num_def num_of_nat_inverse num_of_nat_inject) 

216 
next 

217 
fix m n 

218 
show "Dig1 m = Dig1 n \<longleftrightarrow> m = n" 

219 
apply (cases m) apply (cases n) 

220 
by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject) 

221 
next 

222 
fix n 

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

223 
show "One \<noteq> Dig0 n" 
28021  224 
apply (cases n) 
225 
by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject) 

226 
next 

227 
fix n 

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

228 
show "One \<noteq> Dig1 n" 
28021  229 
apply (cases n) 
230 
by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject) 

231 
next 

232 
fix m n 

233 
have "\<And>n m. n + n \<noteq> Suc (m + m)" 

234 
proof  

235 
fix n m 

236 
show "n + n \<noteq> Suc (m + m)" 

237 
proof (induct m arbitrary: n) 

238 
case 0 then show ?case by (cases n) simp_all 

239 
next 

240 
case (Suc m) then show ?case by (cases n) simp_all 

241 
qed 

242 
qed 

243 
then show "Dig0 n \<noteq> Dig1 m" 

244 
apply (cases n) apply (cases m) 

245 
by (auto simp add: Dig0_def Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject) 

246 
qed 

247 

248 
text {* 

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

250 
as positive naturals (rules @{text "num_induct"}, @{text "num_cases"}) 

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

252 

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

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

255 
*} 

256 

257 

258 
subsection {* Binary numerals *} 

259 

260 
text {* 

261 
We embed binary representations into a generic algebraic 

262 
structure using @{text of_num} 

263 
*} 

264 

265 
ML {* 

266 
structure DigSimps = 

267 
NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals") 

268 
*} 

269 

270 
setup DigSimps.setup 

271 

272 
class semiring_numeral = semiring + monoid_mult 

273 
begin 

274 

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

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

276 
of_num_one [numeral]: "of_num One = 1" 
28021  277 
 "of_num (Dig0 n) = of_num n + of_num n" 
278 
 "of_num (Dig1 n) = of_num n + of_num n + 1" 

279 

280 
declare of_num.simps [simp del] 

281 

282 
end 

283 

284 
text {* 

285 
ML stuff and syntax. 

286 
*} 

287 

288 
ML {* 

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

289 
fun mk_num 1 = @{term One} 
28021  290 
 mk_num k = 
291 
let 

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

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

294 
in bit $ (mk_num l) end; 

295 

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

296 
fun dest_num @{term One} = 1 
28021  297 
 dest_num (@{term Dig0} $ n) = 2 * dest_num n 
298 
 dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1; 

299 

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

301 

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

303 
$ mk_num k 

304 

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

306 
(T, dest_num t) 

307 
*} 

308 

309 
syntax 

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

311 

312 
parse_translation {* 

313 
let 

314 
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

315 
of (0, 1) => Const (@{const_name One}, dummyT) 
28021  316 
 (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n 
317 
 (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n 

318 
else raise Match; 

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

320 
let 

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

322 
val _ = leading_zeros = 0 andalso value > 0 

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

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

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

326 
in [("_Numerals", numeral_tr)] end 

327 
*} 

328 

329 
typed_print_translation {* 

330 
let 

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

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

333 
dig 0 (int_of_num' n) 

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

335 
dig 1 (int_of_num' n) 

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

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

339 
val k = int_of_num' n; 

340 
val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k); 

341 
in case T 

342 
of Type ("fun", [_, T']) => 

343 
if not (! show_types) andalso can Term.dest_Type T' then t' 

344 
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T' 

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

346 
end; 

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

348 
*} 

349 

350 

351 
subsection {* Numeral operations *} 

352 

353 
text {* 

354 
First, addition and multiplication on digits. 

355 
*} 

356 

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

357 
lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

358 
unfolding plus_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0) 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

359 

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

360 
lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

361 
unfolding times_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0) 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

362 

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

363 
lemma nat_of_num_One: "nat_of_num One = 1" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

364 
unfolding one_num_def by (simp add: num_of_nat_inverse) 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

365 

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

366 
lemma nat_of_num_Dig0: "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

367 
unfolding Dig0_def by (simp add: nat_of_num_add) 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

368 

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

369 
lemma nat_of_num_Dig1: "nat_of_num (Dig1 x) = nat_of_num x + nat_of_num x + 1" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

370 
unfolding Dig1_def by (simp add: nat_of_num_add nat_of_num_One) 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

371 

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

372 
lemmas nat_of_num_simps = 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

373 
nat_of_num_One nat_of_num_Dig0 nat_of_num_Dig1 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

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

375 

28021  376 
lemma Dig_plus [numeral, simp, code]: 
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

377 
"One + One = Dig0 One" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

378 
"One + Dig0 m = Dig1 m" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

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

380 
"Dig0 n + One = Dig1 n" 
28021  381 
"Dig0 n + Dig0 m = Dig0 (n + m)" 
382 
"Dig0 n + Dig1 m = Dig1 (n + m)" 

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

383 
"Dig1 n + One = Dig0 (n + One)" 
28021  384 
"Dig1 n + Dig0 m = Dig1 (n + m)" 
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

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

386 
by (simp_all add: num_eq_iff nat_of_num_simps) 
28021  387 

388 
lemma Dig_times [numeral, simp, code]: 

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

389 
"One * One = One" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

390 
"One * Dig0 n = Dig0 n" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

391 
"One * Dig1 n = Dig1 n" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

392 
"Dig0 n * One = Dig0 n" 
28021  393 
"Dig0 n * Dig0 m = Dig0 (n * Dig0 m)" 
394 
"Dig0 n * Dig1 m = Dig0 (n * Dig1 m)" 

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

395 
"Dig1 n * One = Dig1 n" 
28021  396 
"Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)" 
397 
"Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)" 

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

398 
by (simp_all add: num_eq_iff nat_of_num_simps left_distrib right_distrib) 
28021  399 

400 
text {* 

401 
@{const of_num} is a morphism. 

402 
*} 

403 

404 
context semiring_numeral 

405 
begin 

406 

407 
abbreviation "Num1 \<equiv> of_num 1" 

408 

409 
text {* 

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

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

412 
We could get rid of it by replacing the constructor 

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

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

415 
blowup. But it could be worth the effort. 

416 
*} 

417 

418 
lemma of_num_plus_one [numeral]: 

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

419 
"of_num n + 1 = of_num (n + One)" 
28021  420 
by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac) 
421 

422 
lemma of_num_one_plus [numeral]: 

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

423 
"1 + of_num n = of_num (n + One)" 
28021  424 
unfolding of_num_plus_one [symmetric] add_commute .. 
425 

426 
lemma of_num_plus [numeral]: 

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

428 
by (induct n rule: num_induct) 

28053  429 
(simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m] 
28021  430 
add_ac of_num_plus_one [symmetric]) 
431 

432 
lemma of_num_times_one [numeral]: 

433 
"of_num n * 1 = of_num n" 

434 
by simp 

435 

436 
lemma of_num_one_times [numeral]: 

437 
"1 * of_num n = of_num n" 

438 
by simp 

439 

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

440 
lemma times_One [simp]: "m * One = m" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

441 
by (simp add: num_eq_iff nat_of_num_simps) 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

442 

28021  443 
lemma of_num_times [numeral]: 
444 
"of_num m * of_num n = of_num (m * n)" 

445 
by (induct n rule: num_induct) 

446 
(simp_all add: of_num_plus [symmetric] 

28053  447 
semiring_class.right_distrib right_distrib of_num_one) 
28021  448 

449 
end 

450 

451 
text {* 

452 
Structures with a @{term 0}. 

453 
*} 

454 

455 
context semiring_1 

456 
begin 

457 

458 
subclass semiring_numeral .. 

459 

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

461 
by (induct n) 

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

463 

464 
declare of_nat_1 [numeral] 

465 

466 
lemma Dig_plus_zero [numeral]: 

467 
"0 + 1 = 1" 

468 
"0 + of_num n = of_num n" 

469 
"1 + 0 = 1" 

470 
"of_num n + 0 = of_num n" 

471 
by simp_all 

472 

473 
lemma Dig_times_zero [numeral]: 

474 
"0 * 1 = 0" 

475 
"0 * of_num n = 0" 

476 
"1 * 0 = 0" 

477 
"of_num n * 0 = 0" 

478 
by simp_all 

479 

480 
end 

481 

482 
lemma nat_of_num_of_num: "nat_of_num = of_num" 

483 
proof 

484 
fix n 

485 
have "of_num n = nat_of_num n" apply (induct n) 

486 
apply (simp_all add: of_num.simps) 

487 
using nat_of_num 

488 
apply (simp_all add: one_num_def plus_num_def Dig0_def Dig1_def num_of_nat_inverse mem_def) 

489 
done 

490 
then show "nat_of_num n = of_num n" by simp 

491 
qed 

492 

493 
text {* 

494 
Equality. 

495 
*} 

496 

497 
context semiring_char_0 

498 
begin 

499 

500 
lemma of_num_eq_iff [numeral]: 

501 
"of_num m = of_num n \<longleftrightarrow> m = n" 

502 
unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric] 

503 
of_nat_eq_iff nat_of_num_inject .. 

504 

505 
lemma of_num_eq_one_iff [numeral]: 

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

506 
"of_num n = 1 \<longleftrightarrow> n = One" 
28021  507 
proof  
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

508 
have "of_num n = of_num One \<longleftrightarrow> n = One" unfolding of_num_eq_iff .. 
28021  509 
then show ?thesis by (simp add: of_num_one) 
510 
qed 

511 

512 
lemma one_eq_of_num_iff [numeral]: 

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

513 
"1 = of_num n \<longleftrightarrow> n = One" 
28021  514 
unfolding of_num_eq_one_iff [symmetric] by auto 
515 

516 
end 

517 

518 
text {* 

519 
Comparisons. Could be perhaps more general than here. 

520 
*} 

521 

522 
lemma (in ordered_semidom) of_num_pos: "0 < of_num n" 

523 
proof  

524 
have "(0::nat) < of_num n" 

525 
by (induct n) (simp_all add: semiring_numeral_class.of_num.simps) 

526 
then have "of_nat 0 \<noteq> of_nat (of_num n)" 

527 
by (cases n) (simp_all only: semiring_numeral_class.of_num.simps of_nat_eq_iff) 

528 
then have "0 \<noteq> of_num n" 

529 
by (simp add: of_nat_of_num) 

530 
moreover have "0 \<le> of_nat (of_num n)" by simp 

531 
ultimately show ?thesis by (simp add: of_nat_of_num) 

532 
qed 

533 

534 
instantiation num :: linorder 

535 
begin 

536 

537 
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where 

28562  538 
[code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n" 
28021  539 

540 
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where 

28562  541 
[code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" 
28021  542 

543 
instance proof 

544 
qed (auto simp add: less_eq_num_def less_num_def 

545 
split_num_all num_of_nat_inverse num_of_nat_inject split: split_if_asm) 

546 

547 
end 

548 

549 
lemma less_eq_num_code [numeral, simp, code]: 

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

550 
"One \<le> n \<longleftrightarrow> True" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

551 
"Dig0 m \<le> One \<longleftrightarrow> False" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

552 
"Dig1 m \<le> One \<longleftrightarrow> False" 
28021  553 
"Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n" 
554 
"Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n" 

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

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

557 
using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat] 

558 
by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps) 

559 

560 
lemma less_num_code [numeral, simp, code]: 

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

561 
"m < One \<longleftrightarrow> False" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

562 
"One < One \<longleftrightarrow> False" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

563 
"One < Dig0 n \<longleftrightarrow> True" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

564 
"One < Dig1 n \<longleftrightarrow> True" 
28021  565 
"Dig0 m < Dig0 n \<longleftrightarrow> m < n" 
566 
"Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n" 

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

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

569 
using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat] 

570 
by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps) 

571 

572 
context ordered_semidom 

573 
begin 

574 

575 
lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n" 

576 
proof  

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

578 
unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff .. 

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

580 
qed 

581 

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

582 
lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = One" 
28021  583 
proof  
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

584 
have "of_num n \<le> of_num One \<longleftrightarrow> n = One" 
28021  585 
by (cases n) (simp_all add: of_num_less_eq_iff) 
586 
then show ?thesis by (simp add: of_num_one) 

587 
qed 

588 

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

590 
proof  

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

591 
have "of_num One \<le> of_num n" 
28021  592 
by (cases n) (simp_all add: of_num_less_eq_iff) 
593 
then show ?thesis by (simp add: of_num_one) 

594 
qed 

595 

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

597 
proof  

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

599 
unfolding less_num_def nat_of_num_of_num of_nat_less_iff .. 

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

601 
qed 

602 

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

604 
proof  

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

605 
have "\<not> of_num n < of_num One" 
28021  606 
by (cases n) (simp_all add: of_num_less_iff) 
607 
then show ?thesis by (simp add: of_num_one) 

608 
qed 

609 

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

610 
lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> One" 
28021  611 
proof  
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

612 
have "of_num One < of_num n \<longleftrightarrow> n \<noteq> One" 
28021  613 
by (cases n) (simp_all add: of_num_less_iff) 
614 
then show ?thesis by (simp add: of_num_one) 

615 
qed 

616 

617 
end 

618 

619 
text {* 

620 
Structures with subtraction @{term "op "}. 

621 
*} 

622 

29941  623 
text {* A doubleanddecrement function *} 
28021  624 

29941  625 
primrec DigM :: "num \<Rightarrow> num" where 
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

626 
"DigM One = One" 
29941  627 
 "DigM (Dig0 n) = Dig1 (DigM n)" 
628 
 "DigM (Dig1 n) = Dig1 (Dig0 n)" 

28021  629 

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

630 
lemma DigM_plus_one: "DigM n + One = Dig0 n" 
29941  631 
by (induct n) simp_all 
28021  632 

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

633 
lemma one_plus_DigM: "One + DigM n = Dig0 n" 
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset

634 
unfolding add_commute [of One] DigM_plus_one .. 
28021  635 

636 
class semiring_minus = semiring + minus + zero + 

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

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

639 
begin 

640 

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

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

643 

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

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

646 

647 
end 

648 

649 
class semiring_1_minus = semiring_1 + semiring_minus 

650 
begin 

651 

652 
lemma Dig_of_num_pos: 

653 
assumes "k + n = m" 

654 
shows "of_num m  of_num n = of_num k" 

655 
using assms by (simp add: of_num_plus minus_inverts_plus1) 

656 

657 
lemma Dig_of_num_zero: 

658 
shows "of_num n  of_num n = 0" 

659 
by (rule minus_inverts_plus1) simp 

660 

661 
lemma Dig_of_num_neg: 

662 
assumes "k + m = n" 

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

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

665 

666 
lemmas Dig_plus_eval = 

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

667 
of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject 
28021  668 

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

670 
let 

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

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

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

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

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

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

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

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

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

680 
of NONE => (NONE) 

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

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

683 
else mk_meta_eq (let 

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

685 
in 

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

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

688 
end) end) 

689 
end 

690 
*} 

691 

692 
lemma Dig_of_num_minus_zero [numeral]: 

693 
"of_num n  0 = of_num n" 

694 
by (simp add: minus_inverts_plus1) 

695 

696 
lemma Dig_one_minus_zero [numeral]: 

697 
"1  0 = 1" 

698 
by (simp add: minus_inverts_plus1) 

699 

700 
lemma Dig_one_minus_one [numeral]: 

701 
"1  1 = 0" 

702 
by (simp add: minus_inverts_plus1) 

703 

704 
lemma Dig_of_num_minus_one [numeral]: 

29941  705 
"of_num (Dig0 n)  1 = of_num (DigM n)" 
28021  706 
"of_num (Dig1 n)  1 = of_num (Dig0 n)" 
29941  707 
by (auto intro: minus_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) 
28021  708 

709 
lemma Dig_one_minus_of_num [numeral]: 

29941  710 
"1  of_num (Dig0 n) = 0  of_num (DigM n)" 
28021  711 
"1  of_num (Dig1 n) = 0  of_num (Dig0 n)" 
29941  712 
by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) 
28021  713 

714 
end 

715 

716 
context ring_1 

717 
begin 

718 

719 
subclass semiring_1_minus 

29667  720 
proof qed (simp_all add: algebra_simps) 
28021  721 

722 
lemma Dig_zero_minus_of_num [numeral]: 

723 
"0  of_num n =  of_num n" 

724 
by simp 

725 

726 
lemma Dig_zero_minus_one [numeral]: 

727 
"0  1 =  1" 

728 
by simp 

729 

730 
lemma Dig_uminus_uminus [numeral]: 

731 
" ( of_num n) = of_num n" 

732 
by simp 

733 

734 
lemma Dig_plus_uminus [numeral]: 

735 
"of_num m +  of_num n = of_num m  of_num n" 

736 
" of_num m + of_num n = of_num n  of_num m" 

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

738 
"of_num m   of_num n = of_num m + of_num n" 

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

740 
" of_num m   of_num n = of_num n  of_num m" 

741 
by (simp_all add: diff_minus add_commute) 

742 

743 
lemma Dig_times_uminus [numeral]: 

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

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

746 
" of_num n *  of_num m = of_num n * of_num m" 

747 
by (simp_all add: minus_mult_left [symmetric] minus_mult_right [symmetric]) 

748 

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

750 
by (induct n) 

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

752 

753 
declare of_int_1 [numeral] 

754 

755 
end 

756 

757 
text {* 

758 
Greetings to @{typ nat}. 

759 
*} 

760 

761 
instance nat :: semiring_1_minus proof qed simp_all 

762 

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

763 
lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)" 
28021  764 
unfolding of_num_plus_one [symmetric] by simp 
765 

766 
lemma nat_number: 

767 
"1 = Suc 0" 

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

768 
"of_num One = Suc 0" 
29941  769 
"of_num (Dig0 n) = Suc (of_num (DigM n))" 
28021  770 
"of_num (Dig1 n) = Suc (of_num (Dig0 n))" 
29941  771 
by (simp_all add: of_num.simps DigM_plus_one Suc_of_num) 
28021  772 

773 
declare diff_0_eq_0 [numeral] 

774 

775 

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

777 

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

779 
[simp, code post]: "Pls n = of_num n" 

780 

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

782 
[simp, code post]: "Mns n =  of_num n" 

783 

784 
code_datatype "0::int" Pls Mns 

785 

786 
lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric] 

787 

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

28562  789 
[simp, code del]: "sub m n = (of_num m  of_num n)" 
28021  790 

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

28562  792 
[code del]: "dup k = 2 * k" 
28021  793 

794 
lemma Dig_sub [code]: 

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

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

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

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

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

799 
"sub One (Dig1 n) =  of_num (Dig0 n)" 
28021  800 
"sub (Dig0 m) (Dig0 n) = dup (sub m n)" 
801 
"sub (Dig1 m) (Dig1 n) = dup (sub m n)" 

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

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

29667  804 
apply (simp_all add: dup_def algebra_simps) 
29941  805 
apply (simp_all add: of_num_plus one_plus_DigM)[4] 
28021  806 
apply (simp_all add: of_num.simps) 
807 
done 

808 

809 
lemma dup_code [code]: 

810 
"dup 0 = 0" 

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

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

813 
by (simp_all add: dup_def of_num.simps) 

814 

28562  815 
lemma [code, code del]: 
28021  816 
"(1 :: int) = 1" 
817 
"(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +" 

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

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

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

28367  821 
"(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq" 
28021  822 
"(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>" 
823 
"(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <" 

824 
by rule+ 

825 

826 
lemma one_int_code [code]: 

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

827 
"1 = Pls One" 
28021  828 
by (simp add: of_num_one) 
829 

830 
lemma plus_int_code [code]: 

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

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

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

834 
"Pls m  Pls n = sub m n" 

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

836 
"Mns m  Mns n = sub n m" 

837 
by (simp_all add: of_num_plus [symmetric]) 

838 

839 
lemma uminus_int_code [code]: 

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

841 
"uminus (Pls m) = Mns m" 

842 
"uminus (Mns m) = Pls m" 

843 
by simp_all 

844 

845 
lemma minus_int_code [code]: 

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

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

848 
"Pls m  Pls n = sub m n" 

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

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

851 
"Mns m  Mns n = sub n m" 

852 
by (simp_all add: of_num_plus [symmetric]) 

853 

854 
lemma times_int_code [code]: 

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

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

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

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

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

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

861 
by (simp_all add: of_num_times [symmetric]) 

862 

863 
lemma eq_int_code [code]: 

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

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

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

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

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

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

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

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

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

876 
lemma less_eq_int_code [code]: 

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

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

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

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

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

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

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

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

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

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

887 
by (simp_all add: of_num_less_eq_iff) 

888 

889 
lemma less_int_code [code]: 

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

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

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

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

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

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

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

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

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

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

900 
by (simp_all add: of_num_less_iff) 

901 

902 
lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp 

903 
lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp 

904 
declare zero_is_num_zero [code inline del] 

905 
declare one_is_num_one [code inline del] 

906 

907 
hide (open) const sub dup 

908 

909 

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

911 

912 
text {* TODO. Be more precise here with respect to subsumed facts. *} 

913 
declare (in semiring_numeral) numeral [simp] 

914 
declare (in semiring_1) numeral [simp] 

915 
declare (in semiring_char_0) numeral [simp] 

916 
declare (in ring_1) numeral [simp] 

917 
thm numeral 

918 

919 

920 
text {* Toy examples *} 

921 

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

923 
code_thms bar 

924 
export_code bar in Haskell file  

925 
export_code bar in OCaml module_name Foo file  

926 
ML {* @{code bar} *} 

927 

928 
end 