src/HOL/Word/Word.thy
changeset 55818 d8b2f50705d0
parent 55817 0bc0217387a5
child 55833 6fe16c8a6474
equal deleted inserted replaced
55817:0bc0217387a5 55818:d8b2f50705d0
  1190 
  1190 
  1191 
  1191 
  1192 subsection {* Word Arithmetic *}
  1192 subsection {* Word Arithmetic *}
  1193 
  1193 
  1194 lemma word_less_alt: "(a < b) = (uint a < uint b)"
  1194 lemma word_less_alt: "(a < b) = (uint a < uint b)"
  1195   unfolding word_less_def word_le_def by (simp add: less_le)
  1195   by (fact word_less_def)
  1196 
  1196 
  1197 lemma signed_linorder: "class.linorder word_sle word_sless"
  1197 lemma signed_linorder: "class.linorder word_sle word_sless"
  1198   by default (unfold word_sle_def word_sless_def, auto)
  1198   by default (unfold word_sle_def word_sless_def, auto)
  1199 
  1199 
  1200 interpretation signed: linorder "word_sle" "word_sless"
  1200 interpretation signed: linorder "word_sle" "word_sless"
  1234 lemma to_bl_0 [simp]:
  1234 lemma to_bl_0 [simp]:
  1235   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
  1235   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
  1236   unfolding uint_bl
  1236   unfolding uint_bl
  1237   by (simp add: word_size bin_to_bl_zero)
  1237   by (simp add: word_size bin_to_bl_zero)
  1238 
  1238 
  1239 lemma uint_0_iff: "(uint x = 0) = (x = 0)"
  1239 lemma uint_0_iff:
  1240   by (auto intro!: word_uint.Rep_eqD)
  1240   "uint x = 0 \<longleftrightarrow> x = 0"
  1241 
  1241   by (simp add: word_uint_eq_iff)
  1242 lemma unat_0_iff: "(unat x = 0) = (x = 0)"
  1242 
       
  1243 lemma unat_0_iff:
       
  1244   "unat x = 0 \<longleftrightarrow> x = 0"
  1243   unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
  1245   unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
  1244 
  1246 
  1245 lemma unat_0 [simp]: "unat 0 = 0"
  1247 lemma unat_0 [simp]:
       
  1248   "unat 0 = 0"
  1246   unfolding unat_def by auto
  1249   unfolding unat_def by auto
  1247 
  1250 
  1248 lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
  1251 lemma size_0_same':
       
  1252   "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
  1249   apply (unfold word_size)
  1253   apply (unfold word_size)
  1250   apply (rule box_equals)
  1254   apply (rule box_equals)
  1251     defer
  1255     defer
  1252     apply (rule word_uint.Rep_inverse)+
  1256     apply (rule word_uint.Rep_inverse)+
  1253   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
  1257   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
  1276 
  1280 
  1277 lemma scast_n1 [simp]: "scast (- 1) = - 1"
  1281 lemma scast_n1 [simp]: "scast (- 1) = - 1"
  1278   unfolding scast_def by simp
  1282   unfolding scast_def by simp
  1279 
  1283 
  1280 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
  1284 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
  1281   unfolding word_1_wi
  1285   by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))
  1282   by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
       
  1283 
  1286 
  1284 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
  1287 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
  1285   unfolding unat_def by simp
  1288   unfolding unat_def by simp
  1286 
  1289 
  1287 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
  1290 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
  1288   unfolding ucast_def by simp
  1291   unfolding ucast_def by simp
  1289 
  1292 
  1290 (* now, to get the weaker results analogous to word_div/mod_def *)
  1293 (* now, to get the weaker results analogous to word_div/mod_def *)
  1291 
       
  1292 lemmas word_arith_alts = 
       
  1293   word_sub_wi
       
  1294   word_arith_wis (* FIXME: duplicate *)
       
  1295 
  1294 
  1296 
  1295 
  1297 subsection {* Transferring goals from words to ints *}
  1296 subsection {* Transferring goals from words to ints *}
  1298 
  1297 
  1299 lemma word_ths:  
  1298 lemma word_ths:  
  1306   by (transfer, simp add: algebra_simps)+
  1305   by (transfer, simp add: algebra_simps)+
  1307 
  1306 
  1308 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
  1307 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
  1309   by simp
  1308   by simp
  1310 
  1309 
  1311 lemmas uint_word_ariths = 
  1310 lemma uint_word_ariths:
  1312   word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
  1311   fixes a b :: "'a::len0 word"
  1313 
  1312   shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"
  1314 lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
  1313     and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"
  1315 
  1314     and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"
  1316 (* similar expressions for sint (arith operations) *)
  1315     and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"
  1317 lemmas sint_word_ariths = uint_word_arith_bintrs
  1316     and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"
  1318   [THEN uint_sint [symmetric, THEN trans],
  1317     and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"
  1319   unfolded uint_sint bintr_arith1s bintr_ariths 
  1318     and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"
  1320     len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]
  1319     and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"
       
  1320   by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
       
  1321 
       
  1322 lemma uint_word_arith_bintrs:
       
  1323   fixes a b :: "'a::len0 word"
       
  1324   shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"
       
  1325     and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"
       
  1326     and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"
       
  1327     and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"
       
  1328     and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"
       
  1329     and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"
       
  1330     and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"
       
  1331     and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"
       
  1332   by (simp_all add: uint_word_ariths bintrunc_mod2p)
       
  1333 
       
  1334 lemma sint_word_ariths:
       
  1335   fixes a b :: "'a::len word"
       
  1336   shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"
       
  1337     and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"
       
  1338     and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"
       
  1339     and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"
       
  1340     and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"
       
  1341     and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
       
  1342     and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
       
  1343     and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
       
  1344   by (simp_all add: uint_word_arith_bintrs
       
  1345     [THEN uint_sint [symmetric, THEN trans],
       
  1346     unfolded uint_sint bintr_arith1s bintr_ariths 
       
  1347       len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
  1321 
  1348 
  1322 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]]
  1323 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]]
  1324 
  1351 
  1325 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"
  1415   with `1 \<le> uint w` have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
  1442   with `1 \<le> uint w` have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
  1416     by (auto intro: mod_pos_pos_trivial)
  1443     by (auto intro: mod_pos_pos_trivial)
  1417   with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
  1444   with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
  1418     by auto
  1445     by auto
  1419   then show ?thesis
  1446   then show ?thesis
  1420     by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric])
  1447     by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
  1421 qed
  1448 qed
  1422 
  1449 
  1423 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
  1450 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
  1424   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
  1451   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
  1425   
  1452   
  3928   apply (rule trans)
  3955   apply (rule trans)
  3929    apply (rule test_bit_rsplit_alt)
  3956    apply (rule test_bit_rsplit_alt)
  3930      apply (clarsimp simp: word_size)+
  3957      apply (clarsimp simp: word_size)+
  3931   apply (rule trans)
  3958   apply (rule trans)
  3932   apply (rule test_bit_rcat [OF refl refl])
  3959   apply (rule test_bit_rcat [OF refl refl])
  3933   apply (simp add: word_size msrevs)
  3960   apply (simp add: word_size)
  3934   apply (subst nth_rev)
  3961   apply (subst nth_rev)
  3935    apply arith
  3962    apply arith
  3936   apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
  3963   apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
  3937   apply safe
  3964   apply safe
  3938   apply (simp add: diff_mult_distrib)
  3965   apply (simp add: diff_mult_distrib)
  4478   "uint (x + y) = 
  4505   "uint (x + y) = 
  4479   (if uint x + uint y < 2^size x then 
  4506   (if uint x + uint y < 2^size x then 
  4480       uint x + uint y 
  4507       uint x + uint y 
  4481    else 
  4508    else 
  4482       uint x + uint y - 2^size x)" 
  4509       uint x + uint y - 2^size x)" 
  4483   by (simp add: word_arith_alts int_word_uint mod_add_if_z 
  4510   by (simp add: word_arith_wis int_word_uint mod_add_if_z 
  4484                 word_size)
  4511                 word_size)
  4485 
  4512 
  4486 lemma unat_plus_if_size:
  4513 lemma unat_plus_if_size:
  4487   "unat (x + (y::'a::len word)) = 
  4514   "unat (x + (y::'a::len word)) = 
  4488   (if unat x + unat y < 2^size x then 
  4515   (if unat x + unat y < 2^size x then 
  4499   shows "(w \<noteq> 0) = (0 < w)"
  4526   shows "(w \<noteq> 0) = (0 < w)"
  4500   unfolding word_gt_0 by simp
  4527   unfolding word_gt_0 by simp
  4501 
  4528 
  4502 lemma max_lt:
  4529 lemma max_lt:
  4503   "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
  4530   "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
  4504   apply (subst word_arith_nat_defs)
  4531   by (fact unat_div)
  4505   apply (subst word_unat.eq_norm)
       
  4506   apply (subst mod_if)
       
  4507   apply clarsimp
       
  4508   apply (erule notE)
       
  4509   apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
       
  4510   apply (erule order_le_less_trans)
       
  4511   apply (insert unat_lt2p [of "max a b"])
       
  4512   apply simp
       
  4513   done
       
  4514 
  4532 
  4515 lemma uint_sub_if_size:
  4533 lemma uint_sub_if_size:
  4516   "uint (x - y) = 
  4534   "uint (x - y) = 
  4517   (if uint y \<le> uint x then 
  4535   (if uint y \<le> uint x then 
  4518       uint x - uint y 
  4536       uint x - uint y 
  4519    else 
  4537    else 
  4520       uint x - uint y + 2^size x)"
  4538       uint x - uint y + 2^size x)"
  4521   by (simp add: word_arith_alts int_word_uint mod_sub_if_z 
  4539   by (simp add: word_arith_wis int_word_uint mod_sub_if_z 
  4522                 word_size)
  4540                 word_size)
  4523 
  4541 
  4524 lemma unat_sub:
  4542 lemma unat_sub:
  4525   "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4543   "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4526   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4544   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4723 
  4741 
  4724 hide_const (open) Word
  4742 hide_const (open) Word
  4725 
  4743 
  4726 end
  4744 end
  4727 
  4745 
  4728 
       
  4729