author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 32149  ef59550a55d3 
child 37117  59cee8807c29 
permissions  rwrr 
24333  1 
(* 
2 
Author: Jeremy Dawson and Gerwin Klein, NICTA 

3 

4 
contains arithmetic theorems for word, instantiations to 

5 
arithmetic type classes and tactics for reducing word arithmetic 

6 
to linear arithmetic on int or nat 

7 
*) 

8 

24350  9 
header {* Word Arithmetic *} 
10 

26560  11 
theory WordArith 
12 
imports WordDefinition 

13 
begin 

24465  14 

15 
lemma word_less_alt: "(a < b) = (uint a < uint b)" 

16 
unfolding word_less_def word_le_def 

17 
by (auto simp del: word_uint.Rep_inject 

18 
simp: word_uint.Rep_inject [symmetric]) 

19 

36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
32149
diff
changeset

20 
lemma signed_linorder: "class.linorder word_sle word_sless" 
28823  21 
proof 
22 
qed (unfold word_sle_def word_sless_def, auto) 

24465  23 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30686
diff
changeset

24 
interpretation signed: linorder "word_sle" "word_sless" 
24465  25 
by (rule signed_linorder) 
26 

25762  27 
lemmas word_arith_wis = 
24333  28 
word_add_def word_mult_def word_minus_def 
29 
word_succ_def word_pred_def word_0_wi word_1_wi 

30 

24465  31 
lemma udvdI: 
32 
"0 \<le> n ==> uint b = n * uint a ==> a udvd b" 

33 
by (auto simp: udvd_def) 

34 

35 
lemmas word_div_no [simp] = 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

36 
word_div_def [of "number_of a" "number_of b", standard] 
24465  37 

38 
lemmas word_mod_no [simp] = 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

39 
word_mod_def [of "number_of a" "number_of b", standard] 
24465  40 

41 
lemmas word_less_no [simp] = 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

42 
word_less_def [of "number_of a" "number_of b", standard] 
24465  43 

44 
lemmas word_le_no [simp] = 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

45 
word_le_def [of "number_of a" "number_of b", standard] 
24465  46 

47 
lemmas word_sless_no [simp] = 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

48 
word_sless_def [of "number_of a" "number_of b", standard] 
24465  49 

50 
lemmas word_sle_no [simp] = 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

51 
word_sle_def [of "number_of a" "number_of b", standard] 
24465  52 

24333  53 
(* following two are available in class number_ring, 
54 
but convenient to have them here here; 

55 
note  the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1 

56 
are in the default simpset, so to use the automatic simplifications for 

57 
(eg) sint (number_of bin) on sint 1, must do 

58 
(simp add: word_1_no del: numeral_1_eq_1) 

59 
*) 

60 
lemmas word_0_wi_Pls = word_0_wi [folded Pls_def] 

61 
lemmas word_0_no = word_0_wi_Pls [folded word_no_wi] 

62 

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

63 
lemma int_one_bin: "(1 :: int) == (Int.Pls BIT bit.B1)" 
24333  64 
unfolding Pls_def Bit_def by auto 
65 

66 
lemma word_1_no: 

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

67 
"(1 :: 'a :: len0 word) == number_of (Int.Pls BIT bit.B1)" 
24333  68 
unfolding word_1_wi word_number_of_def int_one_bin by auto 
69 

70 
lemma word_m1_wi: "1 == word_of_int 1" 

71 
by (rule word_number_of_alt) 

72 

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

73 
lemma word_m1_wi_Min: "1 = word_of_int Int.Min" 
24333  74 
by (simp add: word_m1_wi number_of_eq) 
75 

24465  76 
lemma word_0_bl: "of_bl [] = 0" 
77 
unfolding word_0_wi of_bl_def by (simp add : Pls_def) 

78 

79 
lemma word_1_bl: "of_bl [True] = 1" 

80 
unfolding word_1_wi of_bl_def 

81 
by (simp add : bl_to_bin_def Bit_def Pls_def) 

82 

24333  83 
lemma uint_0 [simp] : "(uint 0 = 0)" 
84 
unfolding word_0_wi 

85 
by (simp add: word_ubin.eq_norm Pls_def [symmetric]) 

86 

24465  87 
lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0" 
88 
by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def) 

89 

90 
lemma to_bl_0: 

91 
"to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False" 

92 
unfolding uint_bl 

93 
by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric]) 

94 

24333  95 
lemma uint_0_iff: "(uint x = 0) = (x = 0)" 
96 
by (auto intro!: word_uint.Rep_eqD) 

97 

98 
lemma unat_0_iff: "(unat x = 0) = (x = 0)" 

99 
unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff) 

100 

101 
lemma unat_0 [simp]: "unat 0 = 0" 

102 
unfolding unat_def by auto 

103 

24465  104 
lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)" 
24333  105 
apply (unfold word_size) 
106 
apply (rule box_equals) 

107 
defer 

108 
apply (rule word_uint.Rep_inverse)+ 

109 
apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 

110 
apply simp 

111 
done 

112 

113 
lemmas size_0_same = size_0_same' [folded word_size] 

114 

115 
lemmas unat_eq_0 = unat_0_iff 

116 
lemmas unat_eq_zero = unat_0_iff 

117 

118 
lemma unat_gt_0: "(0 < unat x) = (x ~= 0)" 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

119 
by (auto simp: unat_0_iff [symmetric]) 
24333  120 

121 
lemma ucast_0 [simp] : "ucast 0 = 0" 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

122 
unfolding ucast_def 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

123 
by simp (simp add: word_0_wi) 
24333  124 

125 
lemma sint_0 [simp] : "sint 0 = 0" 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

126 
unfolding sint_uint 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

127 
by (simp add: Pls_def [symmetric]) 
24333  128 

129 
lemma scast_0 [simp] : "scast 0 = 0" 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

130 
apply (unfold scast_def) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

131 
apply simp 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

132 
apply (simp add: word_0_wi) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

133 
done 
24333  134 

135 
lemma sint_n1 [simp] : "sint 1 = 1" 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

136 
apply (unfold word_m1_wi_Min) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

137 
apply (simp add: word_sbin.eq_norm) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

138 
apply (unfold Min_def number_of_eq) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

139 
apply simp 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

140 
done 
24333  141 

142 
lemma scast_n1 [simp] : "scast 1 = 1" 

143 
apply (unfold scast_def sint_n1) 

144 
apply (unfold word_number_of_alt) 

145 
apply (rule refl) 

146 
done 

147 

24465  148 
lemma uint_1 [simp] : "uint (1 :: 'a :: len word) = 1" 
24333  149 
unfolding word_1_wi 
150 
by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) 

151 

24465  152 
lemma unat_1 [simp] : "unat (1 :: 'a :: len word) = 1" 
24333  153 
by (unfold unat_def uint_1) auto 
154 

24465  155 
lemma ucast_1 [simp] : "ucast (1 :: 'a :: len word) = 1" 
24333  156 
unfolding ucast_def word_1_wi 
157 
by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) 

158 

159 
(* abstraction preserves the operations 

160 
(the definitions tell this for bins in range uint) *) 

161 

162 
lemmas arths = 

163 
bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], 

164 
folded word_ubin.eq_norm, standard] 

165 

166 
lemma wi_homs: 

167 
shows 

168 
wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and 

169 
wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and 

170 
wi_hom_neg: " word_of_int a = word_of_int ( a)" and 

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

171 
wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

172 
wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)" 
24333  173 
by (auto simp: word_arith_wis arths) 
174 

175 
lemmas wi_hom_syms = wi_homs [symmetric] 

176 

24465  177 
lemma word_sub_def: "a  b == a +  (b :: 'a :: len0 word)" 
178 
unfolding word_sub_wi diff_def 

179 
by (simp only : word_uint.Rep_inverse wi_hom_syms) 

24333  180 

181 
lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard] 

182 

183 
lemma word_of_int_sub_hom: 

184 
"(word_of_int a)  word_of_int b = word_of_int (a  b)" 

185 
unfolding word_sub_def diff_def by (simp only : wi_homs) 

186 

187 
lemmas new_word_of_int_homs = 

188 
word_of_int_sub_hom wi_homs word_0_wi word_1_wi 

189 

190 
lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard] 

191 

192 
lemmas word_of_int_hom_syms = 

193 
new_word_of_int_hom_syms [unfolded succ_def pred_def] 

194 

195 
lemmas word_of_int_homs = 

196 
new_word_of_int_homs [unfolded succ_def pred_def] 

197 

198 
lemmas word_of_int_add_hom = word_of_int_homs (2) 

199 
lemmas word_of_int_mult_hom = word_of_int_homs (3) 

200 
lemmas word_of_int_minus_hom = word_of_int_homs (4) 

201 
lemmas word_of_int_succ_hom = word_of_int_homs (5) 

202 
lemmas word_of_int_pred_hom = word_of_int_homs (6) 

203 
lemmas word_of_int_0_hom = word_of_int_homs (7) 

204 
lemmas word_of_int_1_hom = word_of_int_homs (8) 

205 

206 
(* now, to get the weaker results analogous to word_div/mod_def *) 

207 

208 
lemmas word_arith_alts = 

25762  209 
word_sub_wi [unfolded succ_def pred_def, standard] 
24333  210 
word_arith_wis [unfolded succ_def pred_def, standard] 
211 

212 
lemmas word_sub_alt = word_arith_alts (1) 

213 
lemmas word_add_alt = word_arith_alts (2) 

214 
lemmas word_mult_alt = word_arith_alts (3) 

215 
lemmas word_minus_alt = word_arith_alts (4) 

216 
lemmas word_succ_alt = word_arith_alts (5) 

217 
lemmas word_pred_alt = word_arith_alts (6) 

218 
lemmas word_0_alt = word_arith_alts (7) 

219 
lemmas word_1_alt = word_arith_alts (8) 

220 

24350  221 
subsection "Transferring goals from words to ints" 
24333  222 

223 
lemma word_ths: 

224 
shows 

225 
word_succ_p1: "word_succ a = a + 1" and 

226 
word_pred_m1: "word_pred a = a  1" and 

227 
word_pred_succ: "word_pred (word_succ a) = a" and 

228 
word_succ_pred: "word_succ (word_pred a) = a" and 

229 
word_mult_succ: "word_succ a * b = b + a * b" 

230 
by (rule word_uint.Abs_cases [of b], 

231 
rule word_uint.Abs_cases [of a], 

232 
simp add: pred_def succ_def add_commute mult_commute 

233 
ring_distribs new_word_of_int_homs)+ 

234 

235 
lemmas uint_cong = arg_cong [where f = uint] 

236 

237 
lemmas uint_word_ariths = 

238 
word_arith_alts [THEN trans [OF uint_cong int_word_uint], standard] 

239 

240 
lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p] 

241 

242 
(* similar expressions for sint (arith operations) *) 

243 
lemmas sint_word_ariths = uint_word_arith_bintrs 

244 
[THEN uint_sint [symmetric, THEN trans], 

245 
unfolded uint_sint bintr_arith1s bintr_ariths 

24465  246 
len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard] 
247 

248 
lemmas uint_div_alt = word_div_def 

25762  249 
[THEN trans [OF uint_cong int_word_uint], standard] 
24465  250 
lemmas uint_mod_alt = word_mod_def 
25762  251 
[THEN trans [OF uint_cong int_word_uint], standard] 
24333  252 

253 
lemma word_pred_0_n1: "word_pred 0 = word_of_int 1" 

254 
unfolding word_pred_def number_of_eq 

255 
by (simp add : pred_def word_no_wi) 

256 

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

257 
lemma word_pred_0_Min: "word_pred 0 = word_of_int Int.Min" 
24333  258 
by (simp add: word_pred_0_n1 number_of_eq) 
259 

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

260 
lemma word_m1_Min: " 1 = word_of_int Int.Min" 
24333  261 
unfolding Min_def by (simp only: word_of_int_hom_syms) 
262 

263 
lemma succ_pred_no [simp]: 

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

264 
"word_succ (number_of bin) = number_of (Int.succ bin) & 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

265 
word_pred (number_of bin) = number_of (Int.pred bin)" 
24333  266 
unfolding word_number_of_def by (simp add : new_word_of_int_homs) 
267 

268 
lemma word_sp_01 [simp] : 

269 
"word_succ 1 = 0 & word_succ 0 = 1 & word_pred 0 = 1 & word_pred 1 = 0" 

270 
by (unfold word_0_no word_1_no) auto 

271 

272 
(* alternative approach to lifting arithmetic equalities *) 

273 
lemma word_of_int_Ex: 

274 
"\<exists>y. x = word_of_int y" 

275 
by (rule_tac x="uint x" in exI) simp 

276 

24465  277 
lemma word_arith_eqs: 
278 
fixes a :: "'a::len0 word" 

279 
fixes b :: "'a::len0 word" 

280 
shows 

281 
word_add_0: "0 + a = a" and 

282 
word_add_0_right: "a + 0 = a" and 

283 
word_mult_1: "1 * a = a" and 

284 
word_mult_1_right: "a * 1 = a" and 

285 
word_add_commute: "a + b = b + a" and 

286 
word_add_assoc: "a + b + c = a + (b + c)" and 

287 
word_add_left_commute: "a + (b + c) = b + (a + c)" and 

288 
word_mult_commute: "a * b = b * a" and 

289 
word_mult_assoc: "a * b * c = a * (b * c)" and 

290 
word_mult_left_commute: "a * (b * c) = b * (a * c)" and 

291 
word_left_distrib: "(a + b) * c = a * c + b * c" and 

292 
word_right_distrib: "a * (b + c) = a * b + a * c" and 

293 
word_left_minus: " a + a = 0" and 

294 
word_diff_0_right: "a  0 = a" and 

295 
word_diff_self: "a  a = 0" 

296 
using word_of_int_Ex [of a] 

297 
word_of_int_Ex [of b] 

298 
word_of_int_Ex [of c] 

299 
by (auto simp: word_of_int_hom_syms [symmetric] 

300 
zadd_0_right add_commute add_assoc add_left_commute 

301 
mult_commute mult_assoc mult_left_commute 

28059  302 
left_distrib right_distrib) 
24465  303 

304 
lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute 

305 
lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute 

306 

307 
lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac 

308 
lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac 

309 

310 

24350  311 
subsection "Order on fixedlength words" 
24333  312 

24465  313 
lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)" 
24333  314 
unfolding word_le_def by auto 
315 

24465  316 
lemma word_order_refl: "z <= (z :: 'a :: len0 word)" 
24333  317 
unfolding word_le_def by auto 
318 

24465  319 
lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)" 
24333  320 
unfolding word_le_def by (auto intro!: word_uint.Rep_eqD) 
321 

322 
lemma word_order_linear: 

24465  323 
"y <= x  x <= (y :: 'a :: len0 word)" 
24333  324 
unfolding word_le_def by auto 
325 

326 
lemma word_zero_le [simp] : 

24465  327 
"0 <= (y :: 'a :: len0 word)" 
24333  328 
unfolding word_le_def by auto 
24465  329 

330 
instance word :: (len0) semigroup_add 

331 
by intro_classes (simp add: word_add_assoc) 

24333  332 

24465  333 
instance word :: (len0) linorder 
24333  334 
by intro_classes (auto simp: word_less_def word_le_def) 
335 

24465  336 
instance word :: (len0) ring 
337 
by intro_classes 

338 
(auto simp: word_arith_eqs word_diff_minus 

339 
word_diff_self [unfolded word_diff_minus]) 

340 

24333  341 
lemma word_m1_ge [simp] : "word_pred 0 >= y" 
342 
unfolding word_le_def 

343 
by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto 

344 

345 
lemmas word_n1_ge [simp] = word_m1_ge [simplified word_sp_01] 

346 

347 
lemmas word_not_simps [simp] = 

348 
word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] 

349 

24465  350 
lemma word_gt_0: "0 < y = (0 ~= (y :: 'a :: len0 word))" 
24333  351 
unfolding word_less_def by auto 
352 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

353 
lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of y", standard] 
24333  354 

355 
lemma word_sless_alt: "(a <s b) == (sint a < sint b)" 

356 
unfolding word_sle_def word_sless_def 

27682  357 
by (auto simp add: less_le) 
24333  358 

359 
lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)" 

360 
unfolding unat_def word_le_def 

361 
by (rule nat_le_eq_zle [symmetric]) simp 

362 

363 
lemma word_less_nat_alt: "(a < b) = (unat a < unat b)" 

364 
unfolding unat_def word_less_alt 

365 
by (rule nat_less_eq_zless [symmetric]) simp 

366 

367 
lemma wi_less: 

24465  368 
"(word_of_int n < (word_of_int m :: 'a :: len0 word)) = 
369 
(n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))" 

24333  370 
unfolding word_less_alt by (simp add: word_uint.eq_norm) 
371 

372 
lemma wi_le: 

24465  373 
"(word_of_int n <= (word_of_int m :: 'a :: len0 word)) = 
374 
(n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))" 

24333  375 
unfolding word_le_def by (simp add: word_uint.eq_norm) 
376 

377 
lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)" 

378 
apply (unfold udvd_def) 

379 
apply safe 

380 
apply (simp add: unat_def nat_mult_distrib) 

381 
apply (simp add: uint_nat int_mult) 

382 
apply (rule exI) 

383 
apply safe 

384 
prefer 2 

385 
apply (erule notE) 

386 
apply (rule refl) 

387 
apply force 

388 
done 

389 

390 
lemma udvd_iff_dvd: "x udvd y <> unat x dvd unat y" 

391 
unfolding dvd_def udvd_nat_alt by force 

392 

24465  393 
lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard] 
24378
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset

394 

24465  395 
lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1"; 
24333  396 
unfolding word_arith_wis 
28959  397 
by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc) 
24333  398 

24465  399 
lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one] 
24333  400 

401 
lemma no_no [simp] : "number_of (number_of b) = number_of b" 

402 
by (simp add: number_of_eq) 

403 

404 
lemma unat_minus_one: "x ~= 0 ==> unat (x  1) = unat x  1" 

405 
apply (unfold unat_def) 

406 
apply (simp only: int_word_uint word_arith_alts rdmods) 

407 
apply (subgoal_tac "uint x >= 1") 

408 
prefer 2 

409 
apply (drule contrapos_nn) 

410 
apply (erule word_uint.Rep_inverse' [symmetric]) 

411 
apply (insert uint_ge_0 [of x])[1] 

412 
apply arith 

413 
apply (rule box_equals) 

414 
apply (rule nat_diff_distrib) 

415 
prefer 2 

416 
apply assumption 

417 
apply simp 

418 
apply (subst mod_pos_pos_trivial) 

419 
apply arith 

420 
apply (insert uint_lt2p [of x])[1] 

421 
apply arith 

422 
apply (rule refl) 

423 
apply simp 

424 
done 

425 

426 
lemma measure_unat: "p ~= 0 ==> unat (p  1) < unat p" 

427 
by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric]) 

428 

429 
lemmas uint_add_ge0 [simp] = 

430 
add_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard] 

431 
lemmas uint_mult_ge0 [simp] = 

432 
mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard] 

433 

434 
lemma uint_sub_lt2p [simp]: 

24465  435 
"uint (x :: 'a :: len0 word)  uint (y :: 'b :: len0 word) < 
436 
2 ^ len_of TYPE('a)" 

24333  437 
using uint_ge_0 [of y] uint_lt2p [of x] by arith 
438 

439 

24350  440 
subsection "Conditions for the addition (etc) of two words to overflow" 
24333  441 

442 
lemma uint_add_lem: 

24465  443 
"(uint x + uint y < 2 ^ len_of TYPE('a)) = 
444 
(uint (x + y :: 'a :: len0 word) = uint x + uint y)" 

24333  445 
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) 
446 

447 
lemma uint_mult_lem: 

24465  448 
"(uint x * uint y < 2 ^ len_of TYPE('a)) = 
449 
(uint (x * y :: 'a :: len0 word) = uint x * uint y)" 

24333  450 
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) 
451 

452 
lemma uint_sub_lem: 

453 
"(uint x >= uint y) = (uint (x  y) = uint x  uint y)" 

454 
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) 

455 

456 
lemma uint_add_le: "uint (x + y) <= uint x + uint y" 

457 
unfolding uint_word_ariths by (auto simp: mod_add_if_z) 

458 

459 
lemma uint_sub_ge: "uint (x  y) >= uint x  uint y" 

460 
unfolding uint_word_ariths by (auto simp: mod_sub_if_z) 

461 

462 
lemmas uint_sub_if' = 

463 
trans [OF uint_word_ariths(1) mod_sub_if_z, simplified, standard] 

464 
lemmas uint_plus_if' = 

465 
trans [OF uint_word_ariths(2) mod_add_if_z, simplified, standard] 

466 

467 

24350  468 
subsection {* Definition of uint\_arith *} 
24333  469 

470 
lemma word_of_int_inverse: 

24465  471 
"word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==> 
472 
uint (a::'a::len0 word) = r" 

24333  473 
apply (erule word_uint.Abs_inverse' [rotated]) 
474 
apply (simp add: uints_num) 

475 
done 

476 

477 
lemma uint_split: 

24465  478 
fixes x::"'a::len0 word" 
24333  479 
shows "P (uint x) = 
24465  480 
(ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) > P i)" 
24333  481 
apply (fold word_int_case_def) 
482 
apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq' 

483 
split: word_int_split) 

484 
done 

485 

486 
lemma uint_split_asm: 

24465  487 
fixes x::"'a::len0 word" 
24333  488 
shows "P (uint x) = 
24465  489 
(~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))" 
24333  490 
by (auto dest!: word_of_int_inverse 
491 
simp: int_word_uint int_mod_eq' 

492 
split: uint_split) 

493 

494 
lemmas uint_splits = uint_split uint_split_asm 

495 

496 
lemmas uint_arith_simps = 

497 
word_le_def word_less_alt 

498 
word_uint.Rep_inject [symmetric] 

499 
uint_sub_if' uint_plus_if' 

500 

24465  501 
(* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *) 
24333  502 
lemma power_False_cong: "False ==> a ^ b = c ^ d" 
503 
by auto 

504 

505 
(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *) 

506 
ML {* 

507 
fun uint_arith_ss_of ss = 

508 
ss addsimps @{thms uint_arith_simps} 

509 
delsimps @{thms word_uint.Rep_inject} 

510 
addsplits @{thms split_if_asm} 

511 
addcongs @{thms power_False_cong} 

512 

513 
fun uint_arith_tacs ctxt = 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

514 
let 
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30649
diff
changeset

515 
fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31072
diff
changeset

516 
val cs = claset_of ctxt; 
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31072
diff
changeset

517 
val ss = simpset_of ctxt; 
24333  518 
in 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

519 
[ clarify_tac cs 1, 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

520 
full_simp_tac (uint_arith_ss_of ss) 1, 
24333  521 
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} 
522 
addcongs @{thms power_False_cong})), 

523 
rewrite_goals_tac @{thms word_size}, 

524 
ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN 

525 
REPEAT (etac conjE n) THEN 

526 
REPEAT (dtac @{thm word_of_int_inverse} n 

527 
THEN atac n 

528 
THEN atac n)), 

529 
TRYALL arith_tac' ] 

530 
end 

531 

532 
fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt)) 

533 
*} 

534 

535 
method_setup uint_arith = 

30549  536 
{* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *} 
24333  537 
"solving word arithmetic via integers and arith" 
538 

539 

24350  540 
subsection "More on overflows and monotonicity" 
24333  541 

542 
lemma no_plus_overflow_uint_size: 

24465  543 
"((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)" 
24333  544 
unfolding word_size by uint_arith 
545 

546 
lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size] 

547 

24465  548 
lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x  y) = (uint y <= uint x)" 
24333  549 
by uint_arith 
550 

551 
lemma no_olen_add': 

24465  552 
fixes x :: "'a::len0 word" 
553 
shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))" 

554 
by (simp add: word_add_ac add_ac no_olen_add) 

24333  555 

556 
lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard] 

557 

558 
lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem, standard] 

559 
lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1, standard] 

560 
lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem, standard] 

561 
lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def] 

562 
lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def] 

563 
lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard] 

564 

565 
lemma word_less_sub1: 

24465  566 
"(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x  1)" 
24333  567 
by uint_arith 
568 

569 
lemma word_le_sub1: 

24465  570 
"(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x  1)" 
24333  571 
by uint_arith 
572 

573 
lemma sub_wrap_lt: 

24465  574 
"((x :: 'a :: len0 word) < x  z) = (x < z)" 
24333  575 
by uint_arith 
576 

577 
lemma sub_wrap: 

24465  578 
"((x :: 'a :: len0 word) <= x  z) = (z = 0  x < z)" 
24333  579 
by uint_arith 
580 

581 
lemma plus_minus_not_NULL_ab: 

24465  582 
"(x :: 'a :: len0 word) <= ab  c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0" 
24333  583 
by uint_arith 
584 

585 
lemma plus_minus_no_overflow_ab: 

24465  586 
"(x :: 'a :: len0 word) <= ab  c ==> c <= ab ==> x <= x + c" 
24333  587 
by uint_arith 
588 

589 
lemma le_minus': 

24465  590 
"(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b  a" 
24333  591 
by uint_arith 
592 

593 
lemma le_plus': 

24465  594 
"(a :: 'a :: len0 word) <= b ==> c <= b  a ==> a + c <= b" 
24333  595 
by uint_arith 
596 

597 
lemmas le_plus = le_plus' [rotated] 

598 

599 
lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard] 

600 

601 
lemma word_plus_mono_right: 

24465  602 
"(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z" 
24333  603 
by uint_arith 
604 

605 
lemma word_less_minus_cancel: 

24465  606 
"y  x < z  x ==> x <= z ==> (y :: 'a :: len0 word) < z" 
24333  607 
by uint_arith 
608 

609 
lemma word_less_minus_mono_left: 

24465  610 
"(y :: 'a :: len0 word) < z ==> x <= y ==> y  x < z  x" 
24333  611 
by uint_arith 
612 

613 
lemma word_less_minus_mono: 

614 
"a < c ==> d < b ==> a  b < a ==> c  d < c 

24465  615 
==> a  b < c  (d::'a::len word)" 
24333  616 
by uint_arith 
617 

618 
lemma word_le_minus_cancel: 

24465  619 
"y  x <= z  x ==> x <= z ==> (y :: 'a :: len0 word) <= z" 
24333  620 
by uint_arith 
621 

622 
lemma word_le_minus_mono_left: 

24465  623 
"(y :: 'a :: len0 word) <= z ==> x <= y ==> y  x <= z  x" 
24333  624 
by uint_arith 
625 

626 
lemma word_le_minus_mono: 

627 
"a <= c ==> d <= b ==> a  b <= a ==> c  d <= c 

24465  628 
==> a  b <= c  (d::'a::len word)" 
24333  629 
by uint_arith 
630 

631 
lemma plus_le_left_cancel_wrap: 

24465  632 
"(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)" 
24333  633 
by uint_arith 
634 

635 
lemma plus_le_left_cancel_nowrap: 

24465  636 
"(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==> 
24333  637 
(x + y' < x + y) = (y' < y)" 
638 
by uint_arith 

639 

640 
lemma word_plus_mono_right2: 

24465  641 
"(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c" 
24333  642 
by uint_arith 
643 

644 
lemma word_less_add_right: 

24465  645 
"(x :: 'a :: len0 word) < y  z ==> z <= y ==> x + z < y" 
24333  646 
by uint_arith 
647 

648 
lemma word_less_sub_right: 

24465  649 
"(x :: 'a :: len0 word) < y + z ==> y <= x ==> x  y < z" 
24333  650 
by uint_arith 
651 

652 
lemma word_le_plus_either: 

24465  653 
"(x :: 'a :: len0 word) <= y  x <= z ==> y <= y + z ==> x <= y + z" 
24333  654 
by uint_arith 
655 

656 
lemma word_less_nowrapI: 

24465  657 
"(x :: 'a :: len0 word) < z  k ==> k <= z ==> 0 < k ==> x < x + k" 
24333  658 
by uint_arith 
659 

24465  660 
lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m" 
24333  661 
by uint_arith 
662 

663 
lemma inc_i: 

24465  664 
"(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m" 
24333  665 
by uint_arith 
666 

667 
lemma udvd_incr_lem: 

668 
"up < uq ==> up = ua + n * uint K ==> 

669 
uq = ua + n' * uint K ==> up + uint K <= uq" 

670 
apply clarsimp 

671 
apply (drule less_le_mult) 

672 
apply safe 

673 
done 

674 

675 
lemma udvd_incr': 

676 
"p < q ==> uint p = ua + n * uint K ==> 

677 
uint q = ua + n' * uint K ==> p + K <= q" 

678 
apply (unfold word_less_alt word_le_def) 

679 
apply (drule (2) udvd_incr_lem) 

680 
apply (erule uint_add_le [THEN order_trans]) 

681 
done 

682 

683 
lemma udvd_decr': 

684 
"p < q ==> uint p = ua + n * uint K ==> 

685 
uint q = ua + n' * uint K ==> p <= q  K" 

686 
apply (unfold word_less_alt word_le_def) 

687 
apply (drule (2) udvd_incr_lem) 

688 
apply (drule le_diff_eq [THEN iffD2]) 

689 
apply (erule order_trans) 

690 
apply (rule uint_sub_ge) 

691 
done 

692 

693 
lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, simplified] 

694 
lemmas udvd_incr0 = udvd_incr' [where ua=0, simplified] 

695 
lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified] 

696 

697 
lemma udvd_minus_le': 

698 
"xy < k ==> z udvd xy ==> z udvd k ==> xy <= k  z" 

699 
apply (unfold udvd_def) 

700 
apply clarify 

701 
apply (erule (2) udvd_decr0) 

702 
done 

703 

31072  704 
ML {* Delsimprocs Numeral_Simprocs.cancel_factors *} 
705 

24333  706 
lemma udvd_incr2_K: 
707 
"p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p  a ==> a <= p ==> 

708 
0 < K ==> p <= p + K & p + K <= a + s" 

709 
apply (unfold udvd_def) 

710 
apply clarify 

711 
apply (simp add: uint_arith_simps split: split_if_asm) 

712 
prefer 2 

713 
apply (insert uint_range' [of s])[1] 

714 
apply arith 

715 
apply (drule add_commute [THEN xtr1]) 

716 
apply (simp add: diff_less_eq [symmetric]) 

717 
apply (drule less_le_mult) 

718 
apply arith 

719 
apply simp 

720 
done 

31072  721 

722 
ML {* Addsimprocs Numeral_Simprocs.cancel_factors *} 

24333  723 

24465  724 
(* links with rbl operations *) 
725 
lemma word_succ_rbl: 

726 
"to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))" 

727 
apply (unfold word_succ_def) 

728 
apply clarify 

729 
apply (simp add: to_bl_of_bin) 

730 
apply (simp add: to_bl_def rbl_succ) 

731 
done 

732 

733 
lemma word_pred_rbl: 

734 
"to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))" 

735 
apply (unfold word_pred_def) 

736 
apply clarify 

737 
apply (simp add: to_bl_of_bin) 

738 
apply (simp add: to_bl_def rbl_pred) 

739 
done 

740 

741 
lemma word_add_rbl: 

742 
"to_bl v = vbl ==> to_bl w = wbl ==> 

743 
to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))" 

744 
apply (unfold word_add_def) 

745 
apply clarify 

746 
apply (simp add: to_bl_of_bin) 

747 
apply (simp add: to_bl_def rbl_add) 

748 
done 

749 

750 
lemma word_mult_rbl: 

751 
"to_bl v = vbl ==> to_bl w = wbl ==> 

752 
to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))" 

753 
apply (unfold word_mult_def) 

754 
apply clarify 

755 
apply (simp add: to_bl_of_bin) 

756 
apply (simp add: to_bl_def rbl_mult) 

757 
done 

758 

759 
lemma rtb_rbl_ariths: 

760 
"rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys" 

761 

762 
"rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys" 

763 

764 
"[ rev (to_bl v) = ys; rev (to_bl w) = xs ] 

765 
==> rev (to_bl (v * w)) = rbl_mult ys xs" 

766 

767 
"[ rev (to_bl v) = ys; rev (to_bl w) = xs ] 

768 
==> rev (to_bl (v + w)) = rbl_add ys xs" 

769 
by (auto simp: rev_swap [symmetric] word_succ_rbl 

770 
word_pred_rbl word_mult_rbl word_add_rbl) 

771 

772 

24350  773 
subsection "Arithmetic type class instantiations" 
24333  774 

24465  775 
instance word :: (len0) comm_monoid_add .. 
776 

777 
instance word :: (len0) comm_monoid_mult 

778 
apply (intro_classes) 

779 
apply (simp add: word_mult_commute) 

780 
apply (simp add: word_mult_1) 

781 
done 

782 

783 
instance word :: (len0) comm_semiring 

784 
by (intro_classes) (simp add : word_left_distrib) 

785 

786 
instance word :: (len0) ab_group_add .. 

787 

788 
instance word :: (len0) comm_ring .. 

789 

790 
instance word :: (len) comm_semiring_1 

791 
by (intro_classes) (simp add: lenw1_zero_neq_one) 

792 

793 
instance word :: (len) comm_ring_1 .. 

794 

795 
instance word :: (len0) comm_semiring_0 .. 

796 

797 
instance word :: (len0) order .. 

798 

24333  799 
(* note that iszero_def is only for class comm_semiring_1_cancel, 
24465  800 
which requires word length >= 1, ie 'a :: len word *) 
24333  801 
lemma zero_bintrunc: 
24465  802 
"iszero (number_of x :: 'a :: len word) = 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

803 
(bintrunc (len_of TYPE('a)) x = Int.Pls)" 
24333  804 
apply (unfold iszero_def word_0_wi word_no_wi) 
805 
apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans]) 

806 
apply (simp add : Pls_def [symmetric]) 

807 
done 

808 

809 
lemmas word_le_0_iff [simp] = 

810 
word_zero_le [THEN leD, THEN linorder_antisym_conv1] 

811 

812 
lemma word_of_nat: "of_nat n = word_of_int (int n)" 

813 
by (induct n) (auto simp add : word_of_int_hom_syms) 

814 

815 
lemma word_of_int: "of_int = word_of_int" 

816 
apply (rule ext) 

24465  817 
apply (unfold of_int_def) 
818 
apply (rule contentsI) 

819 
apply safe 

820 
apply (simp_all add: word_of_nat word_of_int_homs) 

821 
defer 

822 
apply (rule Rep_Integ_ne [THEN nonemptyE]) 

823 
apply (rule bexI) 

824 
prefer 2 

825 
apply assumption 

826 
apply (auto simp add: RI_eq_diff) 

24333  827 
done 
828 

829 
lemma word_of_int_nat: 

830 
"0 <= x ==> word_of_int x = of_nat (nat x)" 

831 
by (simp add: of_nat_nat word_of_int) 

832 

833 
lemma word_number_of_eq: 

24465  834 
"number_of w = (of_int w :: 'a :: len word)" 
24333  835 
unfolding word_number_of_def word_of_int by auto 
836 

24465  837 
instance word :: (len) number_ring 
24333  838 
by (intro_classes) (simp add : word_number_of_eq) 
839 

840 
lemma iszero_word_no [simp] : 

24465  841 
"iszero (number_of bin :: 'a :: len word) = 
842 
iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)" 

24368  843 
apply (simp add: zero_bintrunc number_of_is_id) 
24333  844 
apply (unfold iszero_def Pls_def) 
845 
apply (rule refl) 

846 
done 

847 

848 

24350  849 
subsection "Word and nat" 
24333  850 

851 
lemma td_ext_unat': 

24465  852 
"n = len_of TYPE ('a :: len) ==> 
24333  853 
td_ext (unat :: 'a word => nat) of_nat 
854 
(unats n) (%i. i mod 2 ^ n)" 

855 
apply (unfold td_ext_def' unat_def word_of_nat unats_uints) 

856 
apply (auto intro!: imageI simp add : word_of_int_hom_syms) 

857 
apply (erule word_uint.Abs_inverse [THEN arg_cong]) 

858 
apply (simp add: int_word_uint nat_mod_distrib nat_power_eq) 

859 
done 

860 

861 
lemmas td_ext_unat = refl [THEN td_ext_unat'] 

862 
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard] 

863 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30686
diff
changeset

864 
interpretation word_unat: 
29235  865 
td_ext "unat::'a::len word => nat" 
866 
of_nat 

867 
"unats (len_of TYPE('a::len))" 

868 
"%i. i mod 2 ^ len_of TYPE('a::len)" 

24333  869 
by (rule td_ext_unat) 
870 

871 
lemmas td_unat = word_unat.td_thm 

872 

873 
lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] 

874 

24465  875 
lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))" 
24333  876 
apply (unfold unats_def) 
877 
apply clarsimp 

878 
apply (rule xtrans, rule unat_lt2p, assumption) 

879 
done 

880 

881 
lemma word_nchotomy: 

24465  882 
"ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)" 
24333  883 
apply (rule allI) 
884 
apply (rule word_unat.Abs_cases) 

885 
apply (unfold unats_def) 

886 
apply auto 

887 
done 

888 

889 
lemma of_nat_eq: 

24465  890 
fixes w :: "'a::len word" 
891 
shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))" 

24333  892 
apply (rule trans) 
893 
apply (rule word_unat.inverse_norm) 

894 
apply (rule iffI) 

895 
apply (rule mod_eqD) 

896 
apply simp 

897 
apply clarsimp 

898 
done 

899 

900 
lemma of_nat_eq_size: 

901 
"(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)" 

902 
unfolding word_size by (rule of_nat_eq) 

903 

904 
lemma of_nat_0: 

24465  905 
"(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))" 
24333  906 
by (simp add: of_nat_eq) 
907 

908 
lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]] 

909 

910 
lemma of_nat_gt_0: "of_nat k ~= 0 ==> 0 < k" 

911 
by (cases k) auto 

912 

913 
lemma of_nat_neq_0: 

24465  914 
"0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)" 
24333  915 
by (clarsimp simp add : of_nat_0) 
916 

917 
lemma Abs_fnat_hom_add: 

918 
"of_nat a + of_nat b = of_nat (a + b)" 

919 
by simp 

920 

921 
lemma Abs_fnat_hom_mult: 

24465  922 
"of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)" 
24333  923 
by (simp add: word_of_nat word_of_int_mult_hom zmult_int) 
924 

925 
lemma Abs_fnat_hom_Suc: 

926 
"word_succ (of_nat a) = of_nat (Suc a)" 

927 
by (simp add: word_of_nat word_of_int_succ_hom add_ac) 

928 

24465  929 
lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0" 
24333  930 
by (simp add: word_of_nat word_0_wi) 
931 

24465  932 
lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)" 
24333  933 
by (simp add: word_of_nat word_1_wi) 
934 

935 
lemmas Abs_fnat_homs = 

936 
Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 

937 
Abs_fnat_hom_0 Abs_fnat_hom_1 

938 

939 
lemma word_arith_nat_add: 

940 
"a + b = of_nat (unat a + unat b)" 

941 
by simp 

942 

943 
lemma word_arith_nat_mult: 

944 
"a * b = of_nat (unat a * unat b)" 

945 
by (simp add: Abs_fnat_hom_mult [symmetric]) 

946 

947 
lemma word_arith_nat_Suc: 

948 
"word_succ a = of_nat (Suc (unat a))" 

949 
by (subst Abs_fnat_hom_Suc [symmetric]) simp 

950 

951 
lemma word_arith_nat_div: 

952 
"a div b = of_nat (unat a div unat b)" 

953 
by (simp add: word_div_def word_of_nat zdiv_int uint_nat) 

954 

955 
lemma word_arith_nat_mod: 

956 
"a mod b = of_nat (unat a mod unat b)" 

957 
by (simp add: word_mod_def word_of_nat zmod_int uint_nat) 

958 

959 
lemmas word_arith_nat_defs = 

960 
word_arith_nat_add word_arith_nat_mult 

961 
word_arith_nat_Suc Abs_fnat_hom_0 

962 
Abs_fnat_hom_1 word_arith_nat_div 

963 
word_arith_nat_mod 

964 

965 
lemmas unat_cong = arg_cong [where f = "unat"] 

966 

967 
lemmas unat_word_ariths = word_arith_nat_defs 

968 
[THEN trans [OF unat_cong unat_of_nat], standard] 

969 

970 
lemmas word_sub_less_iff = word_sub_le_iff 

971 
[simplified linorder_not_less [symmetric], simplified] 

972 

973 
lemma unat_add_lem: 

24465  974 
"(unat x + unat y < 2 ^ len_of TYPE('a)) = 
975 
(unat (x + y :: 'a :: len word) = unat x + unat y)" 

24333  976 
unfolding unat_word_ariths 
977 
by (auto intro!: trans [OF _ nat_mod_lem]) 

978 

979 
lemma unat_mult_lem: 

24465  980 
"(unat x * unat y < 2 ^ len_of TYPE('a)) = 
981 
(unat (x * y :: 'a :: len word) = unat x * unat y)" 

24333  982 
unfolding unat_word_ariths 
983 
by (auto intro!: trans [OF _ nat_mod_lem]) 

984 

985 
lemmas unat_plus_if' = 

986 
trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard] 

987 

988 
lemma le_no_overflow: 

24465  989 
"x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)" 
24333  990 
apply (erule order_trans) 
991 
apply (erule olen_add_eqv [THEN iffD1]) 

992 
done 

993 

994 
lemmas un_ui_le = trans 

995 
[OF word_le_nat_alt [symmetric] 

25762  996 
word_le_def, 
24333  997 
standard] 
998 

999 
lemma unat_sub_if_size: 

1000 
"unat (x  y) = (if unat y <= unat x 

1001 
then unat x  unat y 

1002 
else unat x + 2 ^ size x  unat y)" 

1003 
apply (unfold word_size) 

1004 
apply (simp add: un_ui_le) 

1005 
apply (auto simp add: unat_def uint_sub_if') 

1006 
apply (rule nat_diff_distrib) 

1007 
prefer 3 

29667  1008 
apply (simp add: algebra_simps) 
24333  1009 
apply (rule nat_diff_distrib [THEN trans]) 
1010 
prefer 3 

1011 
apply (subst nat_add_distrib) 

1012 
prefer 3 

1013 
apply (simp add: nat_power_eq) 

1014 
apply auto 

1015 
apply uint_arith 

1016 
done 

1017 

1018 
lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size] 

1019 

24465  1020 
lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y" 
24333  1021 
apply (simp add : unat_word_ariths) 
1022 
apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq']) 

1023 
apply (rule div_le_dividend) 

1024 
done 

1025 

24465  1026 
lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y" 
24333  1027 
apply (clarsimp simp add : unat_word_ariths) 
1028 
apply (cases "unat y") 

1029 
prefer 2 

1030 
apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq']) 

1031 
apply (rule mod_le_divisor) 

1032 
apply auto 

1033 
done 

1034 

24465  1035 
lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y" 
24333  1036 
unfolding uint_nat by (simp add : unat_div zdiv_int) 
1037 

24465  1038 
lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y" 
24333  1039 
unfolding uint_nat by (simp add : unat_mod zmod_int) 
1040 

1041 

24350  1042 
subsection {* Definition of unat\_arith tactic *} 
24333  1043 

1044 
lemma unat_split: 

24465  1045 
fixes x::"'a::len word" 
24333  1046 
shows "P (unat x) = 
24465  1047 
(ALL n. of_nat n = x & n < 2^len_of TYPE('a) > P n)" 
24333  1048 
by (auto simp: unat_of_nat) 
1049 

1050 
lemma unat_split_asm: 

24465  1051 
fixes x::"'a::len word" 
24333  1052 
shows "P (unat x) = 
24465  1053 
(~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))" 
24333  1054 
by (auto simp: unat_of_nat) 
1055 

1056 
lemmas of_nat_inverse = 

1057 
word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified] 

1058 

1059 
lemmas unat_splits = unat_split unat_split_asm 

1060 

1061 
lemmas unat_arith_simps = 

1062 
word_le_nat_alt word_less_nat_alt 

1063 
word_unat.Rep_inject [symmetric] 

1064 
unat_sub_if' unat_plus_if' unat_div unat_mod 

1065 

1066 
(* unat_arith_tac: tactic to reduce word arithmetic to nat, 

1067 
try to solve via arith *) 

1068 
ML {* 

1069 
fun unat_arith_ss_of ss = 

1070 
ss addsimps @{thms unat_arith_simps} 

1071 
delsimps @{thms word_unat.Rep_inject} 

1072 
addsplits @{thms split_if_asm} 

1073 
addcongs @{thms power_False_cong} 

1074 

1075 
fun unat_arith_tacs ctxt = 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

1076 
let 
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30649
diff
changeset

1077 
fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31072
diff
changeset

1078 
val cs = claset_of ctxt; 
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31072
diff
changeset

1079 
val ss = simpset_of ctxt; 
24333  1080 
in 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

1081 
[ clarify_tac cs 1, 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

1082 
full_simp_tac (unat_arith_ss_of ss) 1, 
24333  1083 
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} 
1084 
addcongs @{thms power_False_cong})), 

1085 
rewrite_goals_tac @{thms word_size}, 

1086 
ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN 

1087 
REPEAT (etac conjE n) THEN 

1088 
REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)), 

1089 
TRYALL arith_tac' ] 

1090 
end 

1091 

1092 
fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt)) 

1093 
*} 

1094 

1095 
method_setup unat_arith = 

30549  1096 
{* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *} 
24333  1097 
"solving word arithmetic via natural numbers and arith" 
1098 

1099 
lemma no_plus_overflow_unat_size: 

24465  1100 
"((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" 
24333  1101 
unfolding word_size by unat_arith 
1102 

24465  1103 
lemma unat_sub: "b <= a ==> unat (a  b) = unat a  unat (b :: 'a :: len word)" 
24333  1104 
by unat_arith 
1105 

1106 
lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size] 

1107 

1108 
lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard] 

1109 

1110 
lemma word_div_mult: 

24465  1111 
"(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==> 
24333  1112 
x * y div y = x" 
1113 
apply unat_arith 

1114 
apply clarsimp 

1115 
apply (subst unat_mult_lem [THEN iffD1]) 

1116 
apply auto 

1117 
done 

1118 

24465  1119 
lemma div_lt': "(i :: 'a :: len word) <= k div x ==> 
1120 
unat i * unat x < 2 ^ len_of TYPE('a)" 

24333  1121 
apply unat_arith 
1122 
apply clarsimp 

1123 
apply (drule mult_le_mono1) 

1124 
apply (erule order_le_less_trans) 

1125 
apply (rule xtr7 [OF unat_lt2p div_mult_le]) 

1126 
done 

1127 

1128 
lemmas div_lt'' = order_less_imp_le [THEN div_lt'] 

1129 

24465  1130 
lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k" 
24333  1131 
apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]]) 
1132 
apply (simp add: unat_arith_simps) 

1133 
apply (drule (1) mult_less_mono1) 

1134 
apply (erule order_less_le_trans) 

1135 
apply (rule div_mult_le) 

1136 
done 

1137 

1138 
lemma div_le_mult: 

24465  1139 
"(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k" 
24333  1140 
apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]]) 
1141 
apply (simp add: unat_arith_simps) 

1142 
apply (drule mult_le_mono1) 

1143 
apply (erule order_trans) 

1144 
apply (rule div_mult_le) 

1145 
done 

1146 

1147 
lemma div_lt_uint': 

24465  1148 
"(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)" 
24333  1149 
apply (unfold uint_nat) 
1150 
apply (drule div_lt') 

1151 
apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 

1152 
nat_power_eq) 

1153 
done 

1154 

1155 
lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint'] 

1156 

1157 
lemma word_le_exists': 

24465  1158 
"(x :: 'a :: len0 word) <= y ==> 
1159 
(EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))" 

24333  1160 
apply (rule exI) 
1161 
apply (rule conjI) 

1162 
apply (rule zadd_diff_inverse) 

1163 
apply uint_arith 

1164 
done 

1165 

1166 
lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab] 

1167 

1168 
lemmas plus_minus_no_overflow = 

1169 
order_less_imp_le [THEN plus_minus_no_overflow_ab] 

1170 

1171 
lemmas mcs = word_less_minus_cancel word_less_minus_mono_left 

1172 
word_le_minus_cancel word_le_minus_mono_left 

1173 

25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

1174 
lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel, standard] 
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

1175 
lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel, standard] 
24333  1176 
lemmas word_plus_mcs = word_diff_ls 
25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

1177 
[where y = "v + x", unfolded add_diff_cancel, standard] 
24333  1178 

1179 
lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse] 

1180 

1181 
lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1] 

1182 

1183 
lemma thd1: 

1184 
"a div b * b \<le> (a::nat)" 

1185 
using gt_or_eq_0 [of b] 

1186 
apply (rule disjE) 

1187 
apply (erule xtr4 [OF thd mult_commute]) 

1188 
apply clarsimp 

1189 
done 

1190 

1191 
lemmas uno_simps [THEN le_unat_uoi, standard] = 

1192 
mod_le_divisor div_le_dividend thd1 

1193 

1194 
lemma word_mod_div_equality: 

24465  1195 
"(n div b) * b + (n mod b) = (n :: 'a :: len word)" 
24333  1196 
apply (unfold word_less_nat_alt word_arith_nat_defs) 
1197 
apply (cut_tac y="unat b" in gt_or_eq_0) 

1198 
apply (erule disjE) 

1199 
apply (simp add: mod_div_equality uno_simps) 

1200 
apply simp 

1201 
done 

1202 

24465  1203 
lemma word_div_mult_le: "a div b * b <= (a::'a::len word)" 
24333  1204 
apply (unfold word_le_nat_alt word_arith_nat_defs) 
1205 
apply (cut_tac y="unat b" in gt_or_eq_0) 

1206 
apply (erule disjE) 

1207 
apply (simp add: div_mult_le uno_simps) 

1208 
apply simp 

1209 
done 

1210 

24465  1211 
lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)" 
24333  1212 
apply (simp only: word_less_nat_alt word_arith_nat_defs) 
1213 
apply (clarsimp simp add : uno_simps) 

1214 
done 

1215 

1216 
lemma word_of_int_power_hom: 

24465  1217 
"word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)" 
24333  1218 
by (induct n) (simp_all add : word_of_int_hom_syms power_Suc) 
1219 

1220 
lemma word_arith_power_alt: 

24465  1221 
"a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)" 
24333  1222 
by (simp add : word_of_int_power_hom [symmetric]) 
1223 

24465  1224 
lemma of_bl_length_less: 
1225 
"length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k" 

1226 
apply (unfold of_bl_no [unfolded word_number_of_def] 

1227 
word_less_alt word_number_of_alt) 

1228 
apply safe 

1229 
apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 

1230 
del: word_of_int_bin) 

1231 
apply (simp add: mod_pos_pos_trivial) 

1232 
apply (subst mod_pos_pos_trivial) 

1233 
apply (rule bl_to_bin_ge0) 

1234 
apply (rule order_less_trans) 

1235 
apply (rule bl_to_bin_lt2p) 

1236 
apply simp 

1237 
apply (rule bl_to_bin_lt2p) 

1238 
done 

1239 

24333  1240 

24350  1241 
subsection "Cardinality, finiteness of set of words" 
24333  1242 

1243 
lemmas card_lessThan' = card_lessThan [unfolded lessThan_def] 

1244 

1245 
lemmas card_eq = word_unat.Abs_inj_on [THEN card_image, 

1246 
unfolded word_unat.image, unfolded unats_def, standard] 

1247 

1248 
lemmas card_word = trans [OF card_eq card_lessThan', standard] 

1249 

24465  1250 
lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1251 
apply (rule contrapos_np) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1252 
prefer 2 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1253 
apply (erule card_infinite) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1254 
apply (simp add: card_word) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1255 
done 
24333  1256 

1257 
lemma card_word_size: 

24465  1258 
"card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1259 
unfolding word_size by (rule card_word) 
24333  1260 

1261 
end 