equal
deleted
inserted
replaced
356 by simp |
356 by simp |
357 moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close> |
357 moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close> |
358 by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) |
358 by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) |
359 moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close> |
359 moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close> |
360 using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] |
360 using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] |
361 by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l) |
361 by (simp add: l take_bit_eq_mod) |
362 ultimately have \<open>P (2 * of_nat n)\<close> |
362 ultimately have \<open>P (2 * of_nat n)\<close> |
363 by (rule word_even) |
363 by (rule word_even) |
364 then show ?case |
364 then show ?case |
365 by simp |
365 by simp |
366 next |
366 next |
369 by simp |
369 by simp |
370 with odd.IH have \<open>P (of_nat n)\<close> |
370 with odd.IH have \<open>P (of_nat n)\<close> |
371 by simp |
371 by simp |
372 moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close> |
372 moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close> |
373 using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] |
373 using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] |
374 by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l) |
374 by (simp add: l take_bit_eq_mod) |
375 ultimately have \<open>P (1 + 2 * of_nat n)\<close> |
375 ultimately have \<open>P (1 + 2 * of_nat n)\<close> |
376 by (rule word_odd) |
376 by (rule word_odd) |
377 then show ?case |
377 then show ?case |
378 by simp |
378 by simp |
379 qed |
379 qed |
1394 |
1394 |
1395 lemma td_ext_unat [OF refl]: |
1395 lemma td_ext_unat [OF refl]: |
1396 "n = LENGTH('a::len) \<Longrightarrow> |
1396 "n = LENGTH('a::len) \<Longrightarrow> |
1397 td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" |
1397 td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" |
1398 apply (standard; transfer) |
1398 apply (standard; transfer) |
1399 apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self) |
1399 apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_nat_eq_self_iff |
1400 apply (simp add: take_bit_eq_mod) |
1400 flip: take_bit_eq_mod) |
1401 done |
1401 done |
1402 |
1402 |
1403 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm] |
1403 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm] |
1404 |
1404 |
1405 interpretation word_unat: |
1405 interpretation word_unat: |
3880 proof - |
3880 proof - |
3881 obtain n where n: \<open>LENGTH('a) = Suc n\<close> |
3881 obtain n where n: \<open>LENGTH('a) = Suc n\<close> |
3882 by (cases \<open>LENGTH('a)\<close>) simp_all |
3882 by (cases \<open>LENGTH('a)\<close>) simp_all |
3883 have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close> |
3883 have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close> |
3884 \<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close> |
3884 \<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close> |
3885 using signed_take_bit_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_less_eq [of n \<open>sint x + sint y\<close>] |
3885 using signed_take_bit_int_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_int_less_eq [of n \<open>sint x + sint y\<close>] |
3886 by (auto intro: ccontr) |
3886 by (auto intro: ccontr) |
3887 have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow> |
3887 have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow> |
3888 (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or> |
3888 (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or> |
3889 (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close> |
3889 (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close> |
3890 using sint_range' [of x] sint_range' [of y] |
3890 using sint_range' [of x] sint_range' [of y] |
4431 apply transfer |
4431 apply transfer |
4432 apply simp |
4432 apply simp |
4433 apply (subst take_bit_diff [symmetric]) |
4433 apply (subst take_bit_diff [symmetric]) |
4434 apply (subst nat_take_bit_eq) |
4434 apply (subst nat_take_bit_eq) |
4435 apply (simp add: nat_le_eq_zle) |
4435 apply (simp add: nat_le_eq_zle) |
4436 apply (simp add: nat_diff_distrib take_bit_eq_self less_imp_diff_less bintr_lt2p) |
4436 apply (simp add: nat_diff_distrib take_bit_nat_eq_self_iff less_imp_diff_less bintr_lt2p) |
4437 done |
4437 done |
4438 qed |
4438 qed |
4439 |
4439 |
4440 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w |
4440 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w |
4441 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w |
4441 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w |