1273 unfolding sint_uint by simp |
1273 unfolding sint_uint by simp |
1274 |
1274 |
1275 lemma scast_0 [simp]: "scast 0 = 0" |
1275 lemma scast_0 [simp]: "scast 0 = 0" |
1276 unfolding scast_def by simp |
1276 unfolding scast_def by simp |
1277 |
1277 |
1278 lemma sint_n1 [simp] : "sint -1 = -1" |
1278 lemma sint_n1 [simp] : "sint (- 1) = - 1" |
1279 unfolding word_m1_wi word_sbin.eq_norm by simp |
1279 unfolding word_m1_wi word_sbin.eq_norm by simp |
1280 |
1280 |
1281 lemma scast_n1 [simp]: "scast (- 1) = - 1" |
1281 lemma scast_n1 [simp]: "scast (- 1) = - 1" |
1282 unfolding scast_def by simp |
1282 unfolding scast_def by simp |
1283 |
1283 |
1347 len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]) |
1347 len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]) |
1348 |
1348 |
1349 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]] |
1349 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]] |
1350 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]] |
1350 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]] |
1351 |
1351 |
1352 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1" |
1352 lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)" |
1353 unfolding word_pred_m1 by simp |
1353 unfolding word_pred_m1 by simp |
1354 |
1354 |
1355 lemma succ_pred_no [simp]: |
1355 lemma succ_pred_no [simp]: |
1356 "word_succ (numeral w) = numeral w + 1" |
1356 "word_succ (numeral w) = numeral w + 1" |
1357 "word_pred (numeral w) = numeral w - 1" |
1357 "word_pred (numeral w) = numeral w - 1" |
1358 "word_succ (- numeral w) = - numeral w + 1" |
1358 "word_succ (- numeral w) = - numeral w + 1" |
1359 "word_pred (- numeral w) = - numeral w - 1" |
1359 "word_pred (- numeral w) = - numeral w - 1" |
1360 unfolding word_succ_p1 word_pred_m1 by simp_all |
1360 unfolding word_succ_p1 word_pred_m1 by simp_all |
1361 |
1361 |
1362 lemma word_sp_01 [simp] : |
1362 lemma word_sp_01 [simp] : |
1363 "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0" |
1363 "word_succ (- 1) = 0 & word_succ 0 = 1 & word_pred 0 = - 1 & word_pred 1 = 0" |
1364 unfolding word_succ_p1 word_pred_m1 by simp_all |
1364 unfolding word_succ_p1 word_pred_m1 by simp_all |
1365 |
1365 |
1366 (* alternative approach to lifting arithmetic equalities *) |
1366 (* alternative approach to lifting arithmetic equalities *) |
1367 lemma word_of_int_Ex: |
1367 lemma word_of_int_Ex: |
1368 "\<exists>y. x = word_of_int y" |
1368 "\<exists>y. x = word_of_int y" |
2801 unfolding shiftr1_def by simp |
2801 unfolding shiftr1_def by simp |
2802 |
2802 |
2803 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0" |
2803 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0" |
2804 unfolding sshiftr1_def by simp |
2804 unfolding sshiftr1_def by simp |
2805 |
2805 |
2806 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1" |
2806 lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1" |
2807 unfolding sshiftr1_def by simp |
2807 unfolding sshiftr1_def by simp |
2808 |
2808 |
2809 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0" |
2809 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0" |
2810 unfolding shiftl_def by (induct n) auto |
2810 unfolding shiftl_def by (induct n) auto |
2811 |
2811 |
3241 done |
3241 done |
3242 |
3242 |
3243 lemma mask_bl: "mask n = of_bl (replicate n True)" |
3243 lemma mask_bl: "mask n = of_bl (replicate n True)" |
3244 by (auto simp add : test_bit_of_bl word_size intro: word_eqI) |
3244 by (auto simp add : test_bit_of_bl word_size intro: word_eqI) |
3245 |
3245 |
3246 lemma mask_bin: "mask n = word_of_int (bintrunc n -1)" |
3246 lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))" |
3247 by (auto simp add: nth_bintr word_size intro: word_eqI) |
3247 by (auto simp add: nth_bintr word_size intro: word_eqI) |
3248 |
3248 |
3249 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))" |
3249 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))" |
3250 apply (rule word_eqI) |
3250 apply (rule word_eqI) |
3251 apply (simp add: nth_bintr word_size word_ops_nth_size) |
3251 apply (simp add: nth_bintr word_size word_ops_nth_size) |