1755 for w :: \<open>'a::len word\<close> |
1755 for w :: \<open>'a::len word\<close> |
1756 proof - |
1756 proof - |
1757 have \<open>?P \<longleftrightarrow> bit (uint w) (LENGTH('a) - Suc 0)\<close> |
1757 have \<open>?P \<longleftrightarrow> bit (uint w) (LENGTH('a) - Suc 0)\<close> |
1758 by (simp add: bit_uint_iff) |
1758 by (simp add: bit_uint_iff) |
1759 also have \<open>\<dots> \<longleftrightarrow> ?Q\<close> |
1759 also have \<open>\<dots> \<longleftrightarrow> ?Q\<close> |
1760 by (simp add: sint_uint bin_sign_def flip: bin_sign_lem) |
1760 by (simp add: sint_uint) |
1761 finally show ?thesis . |
1761 finally show ?thesis . |
1762 qed |
1762 qed |
1763 |
1763 |
1764 lemma drop_bit_eq_zero_iff_not_bit_last: |
1764 lemma drop_bit_eq_zero_iff_not_bit_last: |
1765 \<open>drop_bit (LENGTH('a) - Suc 0) w = 0 \<longleftrightarrow> \<not> bit w (LENGTH('a) - Suc 0)\<close> |
1765 \<open>drop_bit (LENGTH('a) - Suc 0) w = 0 \<longleftrightarrow> \<not> bit w (LENGTH('a) - Suc 0)\<close> |
4097 (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\<close> |
4097 (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\<close> |
4098 for x y :: \<open>'a::len word\<close> |
4098 for x y :: \<open>'a::len word\<close> |
4099 proof - |
4099 proof - |
4100 obtain n where n: \<open>LENGTH('a) = Suc n\<close> |
4100 obtain n where n: \<open>LENGTH('a) = Suc n\<close> |
4101 by (cases \<open>LENGTH('a)\<close>) simp_all |
4101 by (cases \<open>LENGTH('a)\<close>) simp_all |
|
4102 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> |
|
4103 \<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close> |
|
4104 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>] |
|
4105 by (auto intro: ccontr) |
4102 have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow> |
4106 have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow> |
4103 (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or> |
4107 (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or> |
4104 (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close> |
4108 (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close> |
4105 apply safe |
4109 using sint_range' [of x] sint_range' [of y] |
4106 apply simp_all |
4110 apply (auto simp add: not_less) |
4107 apply (unfold sint_word_ariths) |
4111 apply (unfold sint_word_ariths word_sbin.set_iff_norm [symmetric] sints_num) |
4108 apply (unfold word_sbin.set_iff_norm [symmetric] sints_num) |
4112 apply (auto simp add: signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *) |
4109 apply safe |
|
4110 apply (insert sint_range' [where x=x]) |
|
4111 apply (insert sint_range' [where x=y]) |
|
4112 defer |
|
4113 apply (simp (no_asm), arith) |
|
4114 apply (simp (no_asm), arith) |
|
4115 defer |
|
4116 defer |
|
4117 apply (simp (no_asm), arith) |
|
4118 apply (simp (no_asm), arith) |
|
4119 apply (simp_all add: n not_less) |
|
4120 apply (rule notI [THEN notnotD], |
|
4121 drule leI not_le_imp_less, |
|
4122 drule sbintrunc_inc sbintrunc_dec, |
|
4123 simp)+ |
|
4124 done |
4113 done |
4125 then show ?thesis |
4114 then show ?thesis |
4126 apply (simp add: word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff) |
4115 apply (simp add: word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff) |
4127 apply (simp add: bit_last_iff) |
4116 apply (simp add: bit_last_iff) |
4128 done |
4117 done |
4129 qed |
4118 qed |
4130 |
4119 |
4131 lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0" |
4120 lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0" |