equal
deleted
inserted
replaced
99 lemma twos_complement: "- x = word_succ (NOT x)" |
99 lemma twos_complement: "- x = word_succ (NOT x)" |
100 using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"] |
100 using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"] |
101 by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not) |
101 by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not) |
102 |
102 |
103 lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))" |
103 lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))" |
|
104 for x :: \<open>'a::len word\<close> |
104 by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def) |
105 by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def) |
105 |
106 |
106 lemma rbl_word_cat: |
107 lemma rbl_word_cat: |
107 "rev (to_bl (word_cat x y :: 'a::len word)) = |
108 "rev (to_bl (word_cat x y :: 'a::len word)) = |
108 takefill False (LENGTH('a)) (rev (to_bl y) @ rev (to_bl x))" |
109 takefill False (LENGTH('a)) (rev (to_bl y) @ rev (to_bl x))" |