55 qed |
55 qed |
56 |
56 |
57 |
57 |
58 subsection \<open>Type conversions and casting\<close> |
58 subsection \<open>Type conversions and casting\<close> |
59 |
59 |
60 definition sint :: "'a::len word \<Rightarrow> int" |
60 lemma signed_take_bit_decr_length_iff: |
61 \<comment> \<open>treats the most-significant-bit as a sign bit\<close> |
61 \<open>signed_take_bit (LENGTH('a::len) - Suc 0) k = signed_take_bit (LENGTH('a) - Suc 0) l |
62 where sint_uint: "sint w = sbintrunc (LENGTH('a) - 1) (uint w)" |
62 \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> |
63 |
63 by (cases \<open>LENGTH('a)\<close>) |
64 definition unat :: "'a::len word \<Rightarrow> nat" |
64 (simp_all add: signed_take_bit_eq_iff_take_bit_eq) |
65 where "unat w = nat (uint w)" |
65 |
66 |
66 lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close> |
67 definition scast :: "'a::len word \<Rightarrow> 'b::len word" |
67 \<comment> \<open>treats the most-significant bit as a sign bit\<close> |
68 \<comment> \<open>cast a word to a different length\<close> |
68 is \<open>signed_take_bit (LENGTH('a) - 1)\<close> |
69 where "scast w = word_of_int (sint w)" |
69 by (simp add: signed_take_bit_decr_length_iff) |
70 |
70 |
71 definition ucast :: "'a::len word \<Rightarrow> 'b::len word" |
71 lemma sint_uint [code]: |
72 where "ucast w = word_of_int (uint w)" |
72 \<open>sint w = signed_take_bit (LENGTH('a) - 1) (uint w)\<close> |
|
73 for w :: \<open>'a::len word\<close> |
|
74 by transfer simp |
|
75 |
|
76 lift_definition unat :: \<open>'a::len word \<Rightarrow> nat\<close> |
|
77 is \<open>nat \<circ> take_bit LENGTH('a)\<close> |
|
78 by transfer simp |
|
79 |
|
80 lemma nat_uint_eq [simp]: |
|
81 \<open>nat (uint w) = unat w\<close> |
|
82 by transfer simp |
|
83 |
|
84 lemma unat_eq_nat_uint [code]: |
|
85 \<open>unat w = nat (uint w)\<close> |
|
86 by simp |
|
87 |
|
88 lift_definition ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
89 is \<open>take_bit LENGTH('a)\<close> |
|
90 by simp |
|
91 |
|
92 lemma ucast_eq [code]: |
|
93 \<open>ucast w = word_of_int (uint w)\<close> |
|
94 by transfer simp |
|
95 |
|
96 lift_definition scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
|
97 is \<open>signed_take_bit (LENGTH('a) - 1)\<close> |
|
98 by (simp flip: signed_take_bit_decr_length_iff) |
|
99 |
|
100 lemma scast_eq [code]: |
|
101 \<open>scast w = word_of_int (sint w)\<close> |
|
102 by transfer simp |
73 |
103 |
74 instantiation word :: (len) size |
104 instantiation word :: (len) size |
75 begin |
105 begin |
76 |
106 |
77 definition word_size: "size (w :: 'a word) = LENGTH('a)" |
107 lift_definition size_word :: \<open>'a word \<Rightarrow> nat\<close> |
|
108 is \<open>\<lambda>_. LENGTH('a)\<close> .. |
78 |
109 |
79 instance .. |
110 instance .. |
80 |
111 |
81 end |
112 end |
|
113 |
|
114 lemma word_size [code]: |
|
115 \<open>size w = LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
|
116 by (fact size_word.rep_eq) |
82 |
117 |
83 lemma word_size_gt_0 [iff]: "0 < size w" |
118 lemma word_size_gt_0 [iff]: "0 < size w" |
84 for w :: "'a::len word" |
119 for w :: "'a::len word" |
85 by (simp add: word_size) |
120 by (simp add: word_size) |
86 |
121 |
88 |
123 |
89 lemma lens_not_0 [iff]: |
124 lemma lens_not_0 [iff]: |
90 \<open>size w \<noteq> 0\<close> for w :: \<open>'a::len word\<close> |
125 \<open>size w \<noteq> 0\<close> for w :: \<open>'a::len word\<close> |
91 by auto |
126 by auto |
92 |
127 |
93 definition source_size :: "('a::len word \<Rightarrow> 'b) \<Rightarrow> nat" |
128 lift_definition source_size :: \<open>('a::len word \<Rightarrow> 'b) \<Rightarrow> nat\<close> |
94 \<comment> \<open>whether a cast (or other) function is to a longer or shorter length\<close> |
129 is \<open>\<lambda>_. LENGTH('a)\<close> . |
95 where [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)" |
130 |
96 |
131 lift_definition target_size :: \<open>('a \<Rightarrow> 'b::len word) \<Rightarrow> nat\<close> |
97 definition target_size :: "('a \<Rightarrow> 'b::len word) \<Rightarrow> nat" |
132 is \<open>\<lambda>_. LENGTH('b)\<close> .. |
98 where [code del]: "target_size c = size (c undefined)" |
133 |
99 |
134 lift_definition is_up :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> |
100 definition is_up :: "('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool" |
135 is \<open>\<lambda>_. LENGTH('a) \<le> LENGTH('b)\<close> .. |
101 where "is_up c \<longleftrightarrow> source_size c \<le> target_size c" |
136 |
102 |
137 lift_definition is_down :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> |
103 definition is_down :: "('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool" |
138 is \<open>\<lambda>_. LENGTH('a) \<ge> LENGTH('b)\<close> .. |
104 where "is_down c \<longleftrightarrow> target_size c \<le> source_size c" |
139 |
105 |
140 lemma is_up_eq: |
106 definition of_bl :: "bool list \<Rightarrow> 'a::len word" |
141 \<open>is_up f \<longleftrightarrow> source_size f \<le> target_size f\<close> |
107 where "of_bl bl = word_of_int (bl_to_bin bl)" |
142 for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
108 |
143 by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq) |
109 definition to_bl :: "'a::len word \<Rightarrow> bool list" |
144 |
110 where "to_bl w = bin_to_bl (LENGTH('a)) (uint w)" |
145 lemma is_down_eq: |
111 |
146 \<open>is_down f \<longleftrightarrow> target_size f \<le> source_size f\<close> |
112 definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b" |
147 for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
113 where "word_int_case f w = f (uint w)" |
148 by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq) |
|
149 |
|
150 lift_definition of_bl :: \<open>bool list \<Rightarrow> 'a::len word\<close> |
|
151 is bl_to_bin . |
|
152 |
|
153 lift_definition to_bl :: \<open>'a::len word \<Rightarrow> bool list\<close> |
|
154 is \<open>bin_to_bl LENGTH('a)\<close> |
|
155 by (simp add: bl_to_bin_inj) |
|
156 |
|
157 lemma to_bl_eq: |
|
158 \<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close> |
|
159 for w :: \<open>'a::len word\<close> |
|
160 by transfer simp |
|
161 |
|
162 lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close> |
|
163 is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp |
|
164 |
|
165 lemma word_int_case_eq_uint [code]: |
|
166 \<open>word_int_case f w = f (uint w)\<close> |
|
167 by transfer simp |
114 |
168 |
115 translations |
169 translations |
116 "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x" |
170 "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x" |
117 "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x" |
171 "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x" |
118 |
172 |
119 |
173 |
120 subsection \<open>Basic code generation setup\<close> |
174 subsection \<open>Basic code generation setup\<close> |
121 |
175 |
122 definition Word :: "int \<Rightarrow> 'a::len word" |
176 lift_definition Word :: \<open>int \<Rightarrow> 'a::len word\<close> |
123 where [code_post]: "Word = word_of_int" |
177 is id . |
124 |
178 |
125 lemma [code abstype]: "Word (uint w) = w" |
179 lemma Word_eq_word_of_int [code_post]: |
126 by (simp add: Word_def word_of_int_uint) |
180 \<open>Word = word_of_int\<close> |
127 |
181 by (simp add: fun_eq_iff Word.abs_eq) |
128 declare uint_word_of_int [code abstract] |
182 |
|
183 lemma [code abstype]: |
|
184 \<open>Word (uint w) = w\<close> |
|
185 by transfer simp |
|
186 |
|
187 lemma [code abstract]: |
|
188 \<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close> |
|
189 by (fact uint.abs_eq) |
129 |
190 |
130 instantiation word :: (len) equal |
191 instantiation word :: (len) equal |
131 begin |
192 begin |
132 |
193 |
133 definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" |
194 lift_definition equal_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close> |
134 where "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)" |
195 is \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> |
|
196 by simp |
135 |
197 |
136 instance |
198 instance |
137 by standard (simp add: equal equal_word_def word_uint_eq_iff) |
199 by (standard; transfer) rule |
138 |
200 |
139 end |
201 end |
|
202 |
|
203 lemma [code]: |
|
204 \<open>HOL.equal k l \<longleftrightarrow> HOL.equal (uint k) (uint l)\<close> |
|
205 by transfer (simp add: equal) |
140 |
206 |
141 notation fcomp (infixl "\<circ>>" 60) |
207 notation fcomp (infixl "\<circ>>" 60) |
142 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
208 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
143 |
209 |
144 instantiation word :: ("{len, typerep}") random |
210 instantiation word :: ("{len, typerep}") random |
842 by transfer (simp add: bit_take_bit_iff) |
933 by transfer (simp add: bit_take_bit_iff) |
843 |
934 |
844 lemma bit_sint_iff: |
935 lemma bit_sint_iff: |
845 \<open>bit (sint w) n \<longleftrightarrow> n \<ge> LENGTH('a) \<and> bit w (LENGTH('a) - 1) \<or> bit w n\<close> |
936 \<open>bit (sint w) n \<longleftrightarrow> n \<ge> LENGTH('a) \<and> bit w (LENGTH('a) - 1) \<or> bit w n\<close> |
846 for w :: \<open>'a::len word\<close> |
937 for w :: \<open>'a::len word\<close> |
847 apply (cases \<open>LENGTH('a)\<close>) |
938 by transfer (auto simp add: bit_signed_take_bit_iff min_def le_less not_less) |
848 apply simp |
|
849 apply (simp add: sint_uint nth_sbintr not_less bit_uint_iff not_le Suc_le_eq) |
|
850 apply (auto simp add: le_less dest: bit_imp_le_length) |
|
851 done |
|
852 |
939 |
853 lemma bit_word_ucast_iff: |
940 lemma bit_word_ucast_iff: |
854 \<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close> |
941 \<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close> |
855 for w :: \<open>'a::len word\<close> |
942 for w :: \<open>'a::len word\<close> |
856 by (simp add: ucast_def bit_word_of_int_iff bit_uint_iff ac_simps) |
943 by transfer (simp add: bit_take_bit_iff ac_simps) |
857 |
944 |
858 lemma bit_word_scast_iff: |
945 lemma bit_word_scast_iff: |
859 \<open>bit (scast w :: 'b::len word) n \<longleftrightarrow> |
946 \<open>bit (scast w :: 'b::len word) n \<longleftrightarrow> |
860 n < LENGTH('b) \<and> (bit w n \<or> LENGTH('a) \<le> n \<and> bit w (LENGTH('a) - Suc 0))\<close> |
947 n < LENGTH('b) \<and> (bit w n \<or> LENGTH('a) \<le> n \<and> bit w (LENGTH('a) - Suc 0))\<close> |
861 for w :: \<open>'a::len word\<close> |
948 for w :: \<open>'a::len word\<close> |
862 by (simp add: scast_def bit_word_of_int_iff bit_sint_iff ac_simps) |
949 by transfer (auto simp add: bit_signed_take_bit_iff le_less min_def) |
863 |
950 |
864 definition shiftl1 :: "'a::len word \<Rightarrow> 'a word" |
951 lift_definition shiftl1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> |
865 where "shiftl1 w = word_of_int (2 * uint w)" |
952 is \<open>(*) 2\<close> |
|
953 by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) |
|
954 |
|
955 lemma shiftl1_eq: |
|
956 \<open>shiftl1 w = word_of_int (2 * uint w)\<close> |
|
957 by transfer (simp add: take_bit_eq_mod mod_simps) |
866 |
958 |
867 lemma shiftl1_eq_mult_2: |
959 lemma shiftl1_eq_mult_2: |
868 \<open>shiftl1 = (*) 2\<close> |
960 \<open>shiftl1 = (*) 2\<close> |
869 apply (simp add: fun_eq_iff shiftl1_def) |
961 by (rule ext, transfer) simp |
870 apply transfer |
|
871 apply (simp only: mult_2 take_bit_add) |
|
872 apply simp |
|
873 done |
|
874 |
962 |
875 lemma bit_shiftl1_iff: |
963 lemma bit_shiftl1_iff: |
876 \<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close> |
964 \<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close> |
877 for w :: \<open>'a::len word\<close> |
965 for w :: \<open>'a::len word\<close> |
878 by (simp add: shiftl1_eq_mult_2 bit_double_iff exp_eq_zero_iff not_le) (simp add: ac_simps) |
966 by (simp add: shiftl1_eq_mult_2 bit_double_iff exp_eq_zero_iff not_le) (simp add: ac_simps) |
879 |
967 |
880 definition shiftr1 :: "'a::len word \<Rightarrow> 'a word" |
968 lift_definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> |
881 \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close> |
969 \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close> |
882 where "shiftr1 w = word_of_int (bin_rest (uint w))" |
970 is \<open>\<lambda>k. take_bit LENGTH('a) k div 2\<close> by simp |
883 |
971 |
884 lemma shiftr1_eq_div_2: |
972 lemma shiftr1_eq_div_2: |
885 \<open>shiftr1 w = w div 2\<close> |
973 \<open>shiftr1 w = w div 2\<close> |
886 apply (simp add: fun_eq_iff shiftr1_def) |
974 by transfer simp |
887 apply transfer |
|
888 apply (auto simp add: not_le dest: less_2_cases) |
|
889 done |
|
890 |
975 |
891 lemma bit_shiftr1_iff: |
976 lemma bit_shiftr1_iff: |
892 \<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close> |
977 \<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close> |
893 for w :: \<open>'a::len word\<close> |
978 by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff) |
894 by (simp add: shiftr1_eq_div_2 bit_Suc) |
979 |
|
980 lemma shiftr1_eq: |
|
981 \<open>shiftr1 w = word_of_int (bin_rest (uint w))\<close> |
|
982 by transfer simp |
895 |
983 |
896 instantiation word :: (len) ring_bit_operations |
984 instantiation word :: (len) ring_bit_operations |
897 begin |
985 begin |
898 |
986 |
899 lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close> |
987 lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close> |
930 |
1018 |
931 context |
1019 context |
932 includes lifting_syntax |
1020 includes lifting_syntax |
933 begin |
1021 begin |
934 |
1022 |
935 lemma set_bit_word_transfer: |
1023 lemma set_bit_word_transfer [transfer_rule]: |
936 \<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close> |
1024 \<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close> |
937 by (unfold set_bit_def) transfer_prover |
1025 by (unfold set_bit_def) transfer_prover |
938 |
1026 |
939 lemma unset_bit_word_transfer: |
1027 lemma unset_bit_word_transfer [transfer_rule]: |
940 \<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close> |
1028 \<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close> |
941 by (unfold unset_bit_def) transfer_prover |
1029 by (unfold unset_bit_def) transfer_prover |
942 |
1030 |
943 lemma flip_bit_word_transfer: |
1031 lemma flip_bit_word_transfer [transfer_rule]: |
944 \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close> |
1032 \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close> |
945 by (unfold flip_bit_def) transfer_prover |
1033 by (unfold flip_bit_def) transfer_prover |
946 |
1034 |
947 end |
1035 end |
948 |
1036 |
949 instantiation word :: (len) semiring_bit_syntax |
1037 instantiation word :: (len) semiring_bit_syntax |
950 begin |
1038 begin |
951 |
1039 |
952 definition word_test_bit_def: "test_bit a = bin_nth (uint a)" |
1040 lift_definition test_bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close> |
953 |
1041 is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close> |
954 definition shiftl_def: "w << n = (shiftl1 ^^ n) w" |
1042 proof |
955 |
1043 fix k l :: int and n :: nat |
956 definition shiftr_def: "w >> n = (shiftr1 ^^ n) w" |
1044 assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> |
|
1045 show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close> |
|
1046 proof (cases \<open>n < LENGTH('a)\<close>) |
|
1047 case True |
|
1048 from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close> |
|
1049 by simp |
|
1050 then show ?thesis |
|
1051 by (simp add: bit_take_bit_iff) |
|
1052 next |
|
1053 case False |
|
1054 then show ?thesis |
|
1055 by simp |
|
1056 qed |
|
1057 qed |
957 |
1058 |
958 lemma test_bit_word_eq: |
1059 lemma test_bit_word_eq: |
959 \<open>test_bit w = bit w\<close> for w :: \<open>'a::len word\<close> |
1060 \<open>test_bit = (bit :: 'a word \<Rightarrow> _)\<close> |
960 apply (simp add: word_test_bit_def fun_eq_iff) |
1061 by transfer simp |
961 apply transfer |
1062 |
962 apply (simp add: bit_take_bit_iff) |
1063 lemma [code]: |
963 done |
1064 \<open>bit w n \<longleftrightarrow> w AND push_bit n 1 \<noteq> 0\<close> |
|
1065 for w :: \<open>'a::len word\<close> |
|
1066 apply (simp add: bit_eq_iff) |
|
1067 apply (auto simp add: bit_and_iff bit_push_bit_iff bit_1_iff exp_eq_0_imp_not_bit) |
|
1068 done |
|
1069 |
|
1070 lemma [code]: |
|
1071 \<open>test_bit w n \<longleftrightarrow> w AND push_bit n 1 \<noteq> 0\<close> |
|
1072 for w :: \<open>'a::len word\<close> |
|
1073 apply (simp add: test_bit_word_eq bit_eq_iff) |
|
1074 apply (auto simp add: bit_and_iff bit_push_bit_iff bit_1_iff exp_eq_0_imp_not_bit) |
|
1075 done |
|
1076 |
|
1077 lift_definition shiftl_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> |
|
1078 is \<open>\<lambda>k n. push_bit n k\<close> |
|
1079 proof - |
|
1080 show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close> |
|
1081 if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat |
|
1082 proof - |
|
1083 from that |
|
1084 have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k) |
|
1085 = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close> |
|
1086 by simp |
|
1087 moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close> |
|
1088 by simp |
|
1089 ultimately show ?thesis |
|
1090 by (simp add: take_bit_push_bit) |
|
1091 qed |
|
1092 qed |
964 |
1093 |
965 lemma shiftl_word_eq: |
1094 lemma shiftl_word_eq: |
966 \<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close> |
1095 \<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close> |
967 by (induction n) (simp_all add: shiftl_def shiftl1_eq_mult_2 push_bit_double) |
1096 by transfer rule |
968 |
1097 |
|
1098 lift_definition shiftr_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> |
|
1099 is \<open>\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)\<close> by simp |
|
1100 |
969 lemma shiftr_word_eq: |
1101 lemma shiftr_word_eq: |
970 \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close> |
1102 \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close> |
971 by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half) |
1103 by transfer simp |
972 |
1104 |
973 instance by standard |
1105 instance |
974 (simp_all add: fun_eq_iff test_bit_word_eq shiftl_word_eq shiftr_word_eq) |
1106 by (standard; transfer) simp_all |
975 |
1107 |
976 end |
1108 end |
|
1109 |
|
1110 lemma shiftl_code [code]: |
|
1111 \<open>w << n = w * 2 ^ n\<close> |
|
1112 for w :: \<open>'a::len word\<close> |
|
1113 by transfer (simp add: push_bit_eq_mult) |
|
1114 |
|
1115 lemma shiftl1_code [code]: |
|
1116 \<open>shiftl1 w = w << 1\<close> |
|
1117 by transfer (simp add: push_bit_eq_mult ac_simps) |
|
1118 |
|
1119 lemma uint_shiftr_eq [code]: |
|
1120 \<open>uint (w >> n) = uint w div 2 ^ n\<close> |
|
1121 for w :: \<open>'a::len word\<close> |
|
1122 by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv) |
|
1123 |
|
1124 lemma shiftr1_code [code]: |
|
1125 \<open>shiftr1 w = w >> 1\<close> |
|
1126 by transfer (simp add: drop_bit_Suc) |
|
1127 |
|
1128 lemma word_test_bit_def: |
|
1129 \<open>test_bit a = bin_nth (uint a)\<close> |
|
1130 by transfer (simp add: fun_eq_iff bit_take_bit_iff) |
|
1131 |
|
1132 lemma shiftl_def: |
|
1133 \<open>w << n = (shiftl1 ^^ n) w\<close> |
|
1134 proof - |
|
1135 have \<open>push_bit n = (((*) 2 ^^ n) :: int \<Rightarrow> int)\<close> for n |
|
1136 by (induction n) (simp_all add: fun_eq_iff funpow_swap1, simp add: ac_simps) |
|
1137 then show ?thesis |
|
1138 by transfer simp |
|
1139 qed |
|
1140 |
|
1141 lemma shiftr_def: |
|
1142 \<open>w >> n = (shiftr1 ^^ n) w\<close> |
|
1143 proof - |
|
1144 have \<open>drop_bit n = (((\<lambda>k::int. k div 2) ^^ n))\<close> for n |
|
1145 by (rule sym, induction n) |
|
1146 (simp_all add: fun_eq_iff drop_bit_Suc flip: drop_bit_half) |
|
1147 then show ?thesis |
|
1148 apply transfer |
|
1149 apply simp |
|
1150 apply (metis bintrunc_bintrunc rco_bintr) |
|
1151 done |
|
1152 qed |
977 |
1153 |
978 lemma bit_shiftl_word_iff: |
1154 lemma bit_shiftl_word_iff: |
979 \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close> |
1155 \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close> |
980 for w :: \<open>'a::len word\<close> |
1156 for w :: \<open>'a::len word\<close> |
981 by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le) |
1157 by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le) |
992 lemma [code]: |
1168 lemma [code]: |
993 \<open>drop_bit n w = w >> n\<close> for w :: \<open>'a::len word\<close> |
1169 \<open>drop_bit n w = w >> n\<close> for w :: \<open>'a::len word\<close> |
994 by (simp add: shiftr_word_eq) |
1170 by (simp add: shiftr_word_eq) |
995 |
1171 |
996 lemma [code]: |
1172 lemma [code]: |
997 \<open>take_bit n a = a AND Bit_Operations.mask n\<close> for a :: \<open>'a::len word\<close> |
1173 \<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close> |
998 by (fact take_bit_eq_mask) |
1174 by (fact take_bit_eq_mask) |
999 |
1175 |
1000 lemma [code_abbrev]: |
1176 lemma [code_abbrev]: |
1001 \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> |
1177 \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> |
1002 by (fact push_bit_of_1) |
1178 by (fact push_bit_of_1) |
1003 |
1179 |
1004 lemma [code]: |
1180 lemma |
1005 shows word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" |
1181 word_not_def [code]: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" |
1006 and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" |
1182 and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" |
1007 and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" |
1183 and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" |
1008 and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" |
1184 and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" |
1009 by (transfer, simp add: take_bit_not_take_bit)+ |
1185 by (transfer, simp add: take_bit_not_take_bit)+ |
1010 |
1186 |
1011 definition setBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" |
1187 lemma [code abstract]: |
1012 where \<open>setBit w n = Bit_Operations.set_bit n w\<close> |
1188 \<open>uint (v AND w) = uint v AND uint w\<close> |
|
1189 by transfer simp |
|
1190 |
|
1191 lemma [code abstract]: |
|
1192 \<open>uint (v OR w) = uint v OR uint w\<close> |
|
1193 by transfer simp |
|
1194 |
|
1195 lemma [code abstract]: |
|
1196 \<open>uint (v XOR w) = uint v XOR uint w\<close> |
|
1197 by transfer simp |
|
1198 |
|
1199 lift_definition setBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> |
|
1200 is \<open>\<lambda>k n. set_bit n k\<close> |
|
1201 by (simp add: take_bit_set_bit_eq) |
|
1202 |
|
1203 lemma set_Bit_eq: |
|
1204 \<open>setBit w n = set_bit n w\<close> |
|
1205 by transfer simp |
1013 |
1206 |
1014 lemma bit_setBit_iff: |
1207 lemma bit_setBit_iff: |
1015 \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close> |
1208 \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close> |
1016 for w :: \<open>'a::len word\<close> |
1209 for w :: \<open>'a::len word\<close> |
1017 by (simp add: setBit_def bit_set_bit_iff exp_eq_zero_iff not_le ac_simps) |
1210 by transfer (auto simp add: bit_set_bit_iff) |
1018 |
1211 |
1019 definition clearBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" |
1212 lift_definition clearBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> |
1020 where \<open>clearBit w n = unset_bit n w\<close> |
1213 is \<open>\<lambda>k n. unset_bit n k\<close> |
|
1214 by (simp add: take_bit_unset_bit_eq) |
|
1215 |
|
1216 lemma clear_Bit_eq: |
|
1217 \<open>clearBit w n = unset_bit n w\<close> |
|
1218 by transfer simp |
1021 |
1219 |
1022 lemma bit_clearBit_iff: |
1220 lemma bit_clearBit_iff: |
1023 \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close> |
1221 \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close> |
1024 for w :: \<open>'a::len word\<close> |
1222 for w :: \<open>'a::len word\<close> |
1025 by (simp add: clearBit_def bit_unset_bit_iff ac_simps) |
1223 by transfer (auto simp add: bit_unset_bit_iff) |
1026 |
1224 |
1027 definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> |
1225 definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> |
1028 where [code_abbrev]: \<open>even_word = even\<close> |
1226 where [code_abbrev]: \<open>even_word = even\<close> |
1029 |
1227 |
1030 lemma even_word_iff [code]: |
1228 lemma even_word_iff [code]: |
1033 |
1231 |
1034 lemma bit_word_iff_drop_bit_and [code]: |
1232 lemma bit_word_iff_drop_bit_and [code]: |
1035 \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close> |
1233 \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close> |
1036 by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq) |
1234 by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq) |
1037 |
1235 |
1038 |
1236 lemma map_bit_range_eq_if_take_bit_eq: |
1039 subsection \<open>Shift operations\<close> |
1237 \<open>map (bit k) [0..<n] = map (bit l) [0..<n]\<close> |
1040 |
1238 if \<open>take_bit n k = take_bit n l\<close> for k l :: int |
1041 definition sshiftr1 :: "'a::len word \<Rightarrow> 'a word" |
1239 using that proof (induction n arbitrary: k l) |
1042 where "sshiftr1 w = word_of_int (bin_rest (sint w))" |
1240 case 0 |
1043 |
1241 then show ?case |
1044 definition bshiftr1 :: "bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word" |
1242 by simp |
1045 where "bshiftr1 b w = of_bl (b # butlast (to_bl w))" |
1243 next |
1046 |
1244 case (Suc n) |
1047 definition sshiftr :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" (infixl ">>>" 55) |
1245 from Suc.prems have \<open>take_bit n (k div 2) = take_bit n (l div 2)\<close> |
1048 where "w >>> n = (sshiftr1 ^^ n) w" |
1246 by (simp add: take_bit_Suc) |
1049 |
1247 then have \<open>map (bit (k div 2)) [0..<n] = map (bit (l div 2)) [0..<n]\<close> |
1050 definition mask :: "nat \<Rightarrow> 'a::len word" |
1248 by (rule Suc.IH) |
1051 where "mask n = (1 << n) - 1" |
1249 moreover have \<open>bit (r div 2) = bit r \<circ> Suc\<close> for r :: int |
|
1250 by (simp add: fun_eq_iff bit_Suc) |
|
1251 moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close> |
|
1252 by (auto simp add: take_bit_Suc elim!: evenE oddE) arith+ |
|
1253 ultimately show ?case |
|
1254 by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp |
|
1255 qed |
|
1256 |
|
1257 lemma bit_of_bl_iff: |
|
1258 \<open>bit (of_bl bs :: 'a word) n \<longleftrightarrow> rev bs ! n \<and> n < LENGTH('a::len) \<and> n < length bs\<close> |
|
1259 by (auto simp add: of_bl_def bit_word_of_int_iff bin_nth_of_bl) |
|
1260 |
|
1261 lemma rev_to_bl_eq: |
|
1262 \<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close> |
|
1263 for w :: \<open>'a::len word\<close> |
|
1264 apply (rule nth_equalityI) |
|
1265 apply (simp add: to_bl.rep_eq) |
|
1266 apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq) |
|
1267 done |
|
1268 |
|
1269 lemma of_bl_rev_eq: |
|
1270 \<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close> |
|
1271 apply (rule bit_word_eqI) |
|
1272 apply (simp add: bit_of_bl_iff) |
|
1273 apply transfer |
|
1274 apply (simp add: bit_horner_sum_bit_iff ac_simps) |
|
1275 done |
|
1276 |
|
1277 |
|
1278 subsection \<open>More shift operations\<close> |
|
1279 |
|
1280 lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> |
|
1281 is \<open>\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - 1) k div 2)\<close> |
|
1282 by (simp flip: signed_take_bit_decr_length_iff) |
|
1283 |
|
1284 lift_definition sshiftr :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> (infixl \<open>>>>\<close> 55) |
|
1285 is \<open>\<lambda>k n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a) - 1) k))\<close> |
|
1286 by (simp flip: signed_take_bit_decr_length_iff) |
|
1287 |
|
1288 lift_definition bshiftr1 :: \<open>bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close> |
|
1289 is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\<close> |
|
1290 by (fact arg_cong) |
|
1291 |
|
1292 lift_definition mask :: \<open>nat \<Rightarrow> 'a::len word\<close> |
|
1293 is \<open>take_bit LENGTH('a) \<circ> Bit_Operations.mask\<close> . |
|
1294 |
|
1295 lemma sshiftr1_eq: |
|
1296 \<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close> |
|
1297 by transfer simp |
|
1298 |
|
1299 lemma bshiftr1_eq: |
|
1300 \<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close> |
|
1301 apply transfer |
|
1302 apply auto |
|
1303 apply (subst bl_to_bin_app_cat [of \<open>[True]\<close>, simplified]) |
|
1304 apply simp |
|
1305 apply (metis One_nat_def add.commute bin_bl_bin bin_last_bl_to_bin bin_rest_bl_to_bin butlast_bin_rest concat_bit_eq last.simps list.distinct(1) list.size(3) list.size(4) odd_iff_mod_2_eq_one plus_1_eq_Suc power_Suc0_right push_bit_of_1 size_bin_to_bl take_bit_eq_mod trunc_bl2bin_len) |
|
1306 apply (simp add: butlast_rest_bl2bin) |
|
1307 done |
|
1308 |
|
1309 lemma sshiftr_eq: |
|
1310 \<open>w >>> n = (sshiftr1 ^^ n) w\<close> |
|
1311 proof - |
|
1312 have *: \<open>(\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)) ^^ Suc n = |
|
1313 take_bit LENGTH('a) \<circ> drop_bit (Suc n) \<circ> signed_take_bit (LENGTH('a) - Suc 0)\<close> |
|
1314 for n |
|
1315 apply (induction n) |
|
1316 apply (auto simp add: fun_eq_iff drop_bit_Suc) |
|
1317 apply (metis (no_types, lifting) Suc_pred funpow_swap1 len_gt_0 sbintrunc_bintrunc sbintrunc_rest) |
|
1318 done |
|
1319 show ?thesis |
|
1320 apply transfer |
|
1321 apply simp |
|
1322 subgoal for k n |
|
1323 apply (cases n) |
|
1324 apply (simp_all only: *) |
|
1325 apply simp_all |
|
1326 done |
|
1327 done |
|
1328 qed |
|
1329 |
|
1330 lemma mask_eq: |
|
1331 \<open>mask n = (1 << n) - 1\<close> |
|
1332 by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) |
|
1333 |
|
1334 lemma uint_sshiftr_eq [code]: |
|
1335 \<open>uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\<close> |
|
1336 for w :: \<open>'a::len word\<close> |
|
1337 by transfer (simp flip: drop_bit_eq_div) |
|
1338 |
|
1339 lemma sshift1_code [code]: |
|
1340 \<open>sshiftr1 w = w >>> 1\<close> |
|
1341 by transfer (simp add: drop_bit_Suc) |
1052 |
1342 |
1053 |
1343 |
1054 subsection \<open>Rotation\<close> |
1344 subsection \<open>Rotation\<close> |
1055 |
1345 |
1056 definition rotater1 :: "'a list \<Rightarrow> 'a list" |
1346 lemma length_to_bl_eq: |
1057 where "rotater1 ys = |
1347 \<open>length (to_bl w) = LENGTH('a)\<close> |
1058 (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)" |
1348 for w :: \<open>'a::len word\<close> |
1059 |
1349 by transfer simp |
1060 definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
1350 |
1061 where "rotater n = rotater1 ^^ n" |
1351 lift_definition word_rotr :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close> |
1062 |
1352 is \<open>\<lambda>n k. concat_bit (LENGTH('a) - n mod LENGTH('a)) |
1063 definition word_rotr :: "nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word" |
1353 (drop_bit (n mod LENGTH('a)) (take_bit LENGTH('a) k)) |
1064 where "word_rotr n w = of_bl (rotater n (to_bl w))" |
1354 (take_bit (n mod LENGTH('a)) k)\<close> |
1065 |
1355 subgoal for n k l |
1066 definition word_rotl :: "nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word" |
1356 apply (simp add: concat_bit_def nat_le_iff less_imp_le |
1067 where "word_rotl n w = of_bl (rotate n (to_bl w))" |
1357 take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>n mod LENGTH('a::len)\<close>]) |
1068 |
1358 done |
1069 definition word_roti :: "int \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word" |
1359 done |
1070 where "word_roti i w = |
1360 |
1071 (if i \<ge> 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w)" |
1361 lift_definition word_rotl :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close> |
1072 |
1362 is \<open>\<lambda>n k. concat_bit (n mod LENGTH('a)) |
1073 |
1363 (drop_bit (LENGTH('a) - n mod LENGTH('a)) (take_bit LENGTH('a) k)) |
|
1364 (take_bit (LENGTH('a) - n mod LENGTH('a)) k)\<close> |
|
1365 subgoal for n k l |
|
1366 apply (simp add: concat_bit_def nat_le_iff less_imp_le |
|
1367 take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>LENGTH('a) - n mod LENGTH('a::len)\<close>]) |
|
1368 done |
|
1369 done |
|
1370 |
|
1371 lift_definition word_roti :: \<open>int \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close> |
|
1372 is \<open>\<lambda>r k. concat_bit (LENGTH('a) - nat (r mod int LENGTH('a))) |
|
1373 (drop_bit (nat (r mod int LENGTH('a))) (take_bit LENGTH('a) k)) |
|
1374 (take_bit (nat (r mod int LENGTH('a))) k)\<close> |
|
1375 subgoal for r k l |
|
1376 apply (simp add: concat_bit_def nat_le_iff less_imp_le |
|
1377 take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>nat (r mod int LENGTH('a::len))\<close>]) |
|
1378 done |
|
1379 done |
|
1380 |
|
1381 lemma word_rotl_eq_word_rotr [code]: |
|
1382 \<open>word_rotl n = (word_rotr (LENGTH('a) - n mod LENGTH('a)) :: 'a::len word \<Rightarrow> 'a word)\<close> |
|
1383 by (rule ext, cases \<open>n mod LENGTH('a) = 0\<close>; transfer) simp_all |
|
1384 |
|
1385 lemma word_roti_eq_word_rotr_word_rotl [code]: |
|
1386 \<open>word_roti i w = |
|
1387 (if i \<ge> 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w)\<close> |
|
1388 proof (cases \<open>i \<ge> 0\<close>) |
|
1389 case True |
|
1390 moreover define n where \<open>n = nat i\<close> |
|
1391 ultimately have \<open>i = int n\<close> |
|
1392 by simp |
|
1393 moreover have \<open>word_roti (int n) = (word_rotr n :: _ \<Rightarrow> 'a word)\<close> |
|
1394 by (rule ext, transfer) (simp add: nat_mod_distrib) |
|
1395 ultimately show ?thesis |
|
1396 by simp |
|
1397 next |
|
1398 case False |
|
1399 moreover define n where \<open>n = nat (- i)\<close> |
|
1400 ultimately have \<open>i = - int n\<close> \<open>n > 0\<close> |
|
1401 by simp_all |
|
1402 moreover have \<open>word_roti (- int n) = (word_rotl n :: _ \<Rightarrow> 'a word)\<close> |
|
1403 by (rule ext, transfer) |
|
1404 (simp add: zmod_zminus1_eq_if flip: of_nat_mod of_nat_diff) |
|
1405 ultimately show ?thesis |
|
1406 by simp |
|
1407 qed |
|
1408 |
|
1409 lemma bit_word_rotr_iff: |
|
1410 \<open>bit (word_rotr m w) n \<longleftrightarrow> |
|
1411 n < LENGTH('a) \<and> bit w ((n + m) mod LENGTH('a))\<close> |
|
1412 for w :: \<open>'a::len word\<close> |
|
1413 proof transfer |
|
1414 fix k :: int and m n :: nat |
|
1415 define q where \<open>q = m mod LENGTH('a)\<close> |
|
1416 have \<open>q < LENGTH('a)\<close> |
|
1417 by (simp add: q_def) |
|
1418 then have \<open>q \<le> LENGTH('a)\<close> |
|
1419 by simp |
|
1420 have \<open>m mod LENGTH('a) = q\<close> |
|
1421 by (simp add: q_def) |
|
1422 moreover have \<open>(n + m) mod LENGTH('a) = (n + q) mod LENGTH('a)\<close> |
|
1423 by (subst mod_add_right_eq [symmetric]) (simp add: \<open>m mod LENGTH('a) = q\<close>) |
|
1424 moreover have \<open>n < LENGTH('a) \<and> |
|
1425 bit (concat_bit (LENGTH('a) - q) (drop_bit q (take_bit LENGTH('a) k)) (take_bit q k)) n \<longleftrightarrow> |
|
1426 n < LENGTH('a) \<and> bit k ((n + q) mod LENGTH('a))\<close> |
|
1427 using \<open>q < LENGTH('a)\<close> |
|
1428 by (cases \<open>q + n \<ge> LENGTH('a)\<close>) |
|
1429 (auto simp add: bit_concat_bit_iff bit_drop_bit_eq |
|
1430 bit_take_bit_iff le_mod_geq ac_simps) |
|
1431 ultimately show \<open>n < LENGTH('a) \<and> |
|
1432 bit (concat_bit (LENGTH('a) - m mod LENGTH('a)) |
|
1433 (drop_bit (m mod LENGTH('a)) (take_bit LENGTH('a) k)) |
|
1434 (take_bit (m mod LENGTH('a)) k)) n |
|
1435 \<longleftrightarrow> n < LENGTH('a) \<and> |
|
1436 (n + m) mod LENGTH('a) < LENGTH('a) \<and> |
|
1437 bit k ((n + m) mod LENGTH('a))\<close> |
|
1438 by simp |
|
1439 qed |
|
1440 |
|
1441 lemma bit_word_rotl_iff: |
|
1442 \<open>bit (word_rotl m w) n \<longleftrightarrow> |
|
1443 n < LENGTH('a) \<and> bit w ((n + (LENGTH('a) - m mod LENGTH('a))) mod LENGTH('a))\<close> |
|
1444 for w :: \<open>'a::len word\<close> |
|
1445 by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff) |
|
1446 |
|
1447 lemma bit_word_roti_iff: |
|
1448 \<open>bit (word_roti k w) n \<longleftrightarrow> |
|
1449 n < LENGTH('a) \<and> bit w (nat ((int n + k) mod int LENGTH('a)))\<close> |
|
1450 for w :: \<open>'a::len word\<close> |
|
1451 proof transfer |
|
1452 fix k l :: int and n :: nat |
|
1453 define m where \<open>m = nat (k mod int LENGTH('a))\<close> |
|
1454 have \<open>m < LENGTH('a)\<close> |
|
1455 by (simp add: nat_less_iff m_def) |
|
1456 then have \<open>m \<le> LENGTH('a)\<close> |
|
1457 by simp |
|
1458 have \<open>k mod int LENGTH('a) = int m\<close> |
|
1459 by (simp add: nat_less_iff m_def) |
|
1460 moreover have \<open>(int n + k) mod int LENGTH('a) = int ((n + m) mod LENGTH('a))\<close> |
|
1461 by (subst mod_add_right_eq [symmetric]) (simp add: of_nat_mod \<open>k mod int LENGTH('a) = int m\<close>) |
|
1462 moreover have \<open>n < LENGTH('a) \<and> |
|
1463 bit (concat_bit (LENGTH('a) - m) (drop_bit m (take_bit LENGTH('a) l)) (take_bit m l)) n \<longleftrightarrow> |
|
1464 n < LENGTH('a) \<and> bit l ((n + m) mod LENGTH('a))\<close> |
|
1465 using \<open>m < LENGTH('a)\<close> |
|
1466 by (cases \<open>m + n \<ge> LENGTH('a)\<close>) |
|
1467 (auto simp add: bit_concat_bit_iff bit_drop_bit_eq |
|
1468 bit_take_bit_iff nat_less_iff not_le not_less ac_simps |
|
1469 le_diff_conv le_mod_geq) |
|
1470 ultimately show \<open>n < LENGTH('a) |
|
1471 \<and> bit (concat_bit (LENGTH('a) - nat (k mod int LENGTH('a))) |
|
1472 (drop_bit (nat (k mod int LENGTH('a))) (take_bit LENGTH('a) l)) |
|
1473 (take_bit (nat (k mod int LENGTH('a))) l)) n \<longleftrightarrow> |
|
1474 n < LENGTH('a) |
|
1475 \<and> nat ((int n + k) mod int LENGTH('a)) < LENGTH('a) |
|
1476 \<and> bit l (nat ((int n + k) mod int LENGTH('a)))\<close> |
|
1477 by simp |
|
1478 qed |
|
1479 |
|
1480 lemma uint_word_rotr_eq [code]: |
|
1481 \<open>uint (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a)) |
|
1482 (drop_bit (n mod LENGTH('a)) (uint w)) |
|
1483 (uint (take_bit (n mod LENGTH('a)) w))\<close> |
|
1484 for w :: \<open>'a::len word\<close> |
|
1485 apply transfer |
|
1486 apply (simp add: concat_bit_def take_bit_drop_bit push_bit_take_bit min_def) |
|
1487 using mod_less_divisor not_less apply blast |
|
1488 done |
|
1489 |
|
1490 lemma word_rotr_eq: |
|
1491 \<open>word_rotr n w = of_bl (rotater n (to_bl w))\<close> |
|
1492 apply (rule bit_word_eqI) |
|
1493 subgoal for n |
|
1494 apply (cases \<open>n < LENGTH('a)\<close>) |
|
1495 apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff rotater_rev length_to_bl_eq nth_rotate rev_to_bl_eq ac_simps) |
|
1496 done |
|
1497 done |
|
1498 |
|
1499 lemma word_rotl_eq: |
|
1500 \<open>word_rotl n w = of_bl (rotate n (to_bl w))\<close> |
|
1501 proof - |
|
1502 have \<open>rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))\<close> |
|
1503 by (simp add: rotater_rev') |
|
1504 then show ?thesis |
|
1505 apply (simp add: word_rotl_eq_word_rotr bit_of_bl_iff length_to_bl_eq rev_to_bl_eq) |
|
1506 apply (rule bit_word_eqI) |
|
1507 subgoal for n |
|
1508 apply (cases \<open>n < LENGTH('a)\<close>) |
|
1509 apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff nth_rotater) |
|
1510 done |
|
1511 done |
|
1512 qed |
|
1513 |
|
1514 |
1074 subsection \<open>Split and cat operations\<close> |
1515 subsection \<open>Split and cat operations\<close> |
1075 |
1516 |
1076 definition word_cat :: "'a::len word \<Rightarrow> 'b::len word \<Rightarrow> 'c::len word" |
1517 lift_definition word_cat :: \<open>'a::len word \<Rightarrow> 'b::len word \<Rightarrow> 'c::len word\<close> |
1077 where "word_cat a b = word_of_int (bin_cat (uint a) (LENGTH('b)) (uint b))" |
1518 is \<open>\<lambda>k l. concat_bit LENGTH('b) l (take_bit LENGTH('a) k)\<close> |
|
1519 by (simp add: bit_eq_iff bit_concat_bit_iff bit_take_bit_iff) |
1078 |
1520 |
1079 lemma word_cat_eq: |
1521 lemma word_cat_eq: |
1080 \<open>(word_cat v w :: 'c::len word) = push_bit LENGTH('b) (ucast v) + ucast w\<close> |
1522 \<open>(word_cat v w :: 'c::len word) = push_bit LENGTH('b) (ucast v) + ucast w\<close> |
1081 for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close> |
1523 for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close> |
1082 apply (simp add: word_cat_def bin_cat_eq_push_bit_add_take_bit ucast_def) |
1524 by transfer (simp add: bin_cat_eq_push_bit_add_take_bit) |
1083 apply transfer apply simp |
1525 |
1084 done |
1526 lemma word_cat_eq' [code]: |
|
1527 \<open>word_cat a b = word_of_int (concat_bit LENGTH('b) (uint b) (uint a))\<close> |
|
1528 for a :: \<open>'a::len word\<close> and b :: \<open>'b::len word\<close> |
|
1529 by transfer simp |
1085 |
1530 |
1086 lemma bit_word_cat_iff: |
1531 lemma bit_word_cat_iff: |
1087 \<open>bit (word_cat v w :: 'c::len word) n \<longleftrightarrow> n < LENGTH('c) \<and> (if n < LENGTH('b) then bit w n else bit v (n - LENGTH('b)))\<close> |
1532 \<open>bit (word_cat v w :: 'c::len word) n \<longleftrightarrow> n < LENGTH('c) \<and> (if n < LENGTH('b) then bit w n else bit v (n - LENGTH('b)))\<close> |
1088 for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close> |
1533 for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close> |
1089 by (auto simp add: word_cat_def bit_word_of_int_iff bin_nth_cat bit_uint_iff not_less bit_imp_le_length) |
1534 by transfer (simp add: bit_concat_bit_iff bit_take_bit_iff) |
1090 |
1535 |
1091 definition word_split :: "'a::len word \<Rightarrow> 'b::len word \<times> 'c::len word" |
1536 definition word_split :: "'a::len word \<Rightarrow> 'b::len word \<times> 'c::len word" |
1092 where "word_split a = |
1537 where "word_split a = |
1093 (case bin_split (LENGTH('c)) (uint a) of |
1538 (case bin_split (LENGTH('c)) (uint a) of |
1094 (u, v) \<Rightarrow> (word_of_int u, word_of_int v))" |
1539 (u, v) \<Rightarrow> (word_of_int u, word_of_int v))" |
1557 |
1993 |
1558 \<comment> \<open>literal u(s)cast\<close> |
1994 \<comment> \<open>literal u(s)cast\<close> |
1559 lemma ucast_bintr [simp]: |
1995 lemma ucast_bintr [simp]: |
1560 "ucast (numeral w :: 'a::len word) = |
1996 "ucast (numeral w :: 'a::len word) = |
1561 word_of_int (bintrunc (LENGTH('a)) (numeral w))" |
1997 word_of_int (bintrunc (LENGTH('a)) (numeral w))" |
1562 by (simp add: ucast_def) |
1998 by transfer simp |
1563 |
1999 |
1564 (* TODO: neg_numeral *) |
2000 (* TODO: neg_numeral *) |
1565 |
2001 |
1566 lemma scast_sbintr [simp]: |
2002 lemma scast_sbintr [simp]: |
1567 "scast (numeral w ::'a::len word) = |
2003 "scast (numeral w ::'a::len word) = |
1568 word_of_int (sbintrunc (LENGTH('a) - Suc 0) (numeral w))" |
2004 word_of_int (sbintrunc (LENGTH('a) - Suc 0) (numeral w))" |
1569 by (simp add: scast_def) |
2005 by transfer simp |
1570 |
2006 |
1571 lemma source_size: "source_size (c::'a::len word \<Rightarrow> _) = LENGTH('a)" |
2007 lemma source_size: "source_size (c::'a::len word \<Rightarrow> _) = LENGTH('a)" |
1572 unfolding source_size_def word_size Let_def .. |
2008 by transfer simp |
1573 |
2009 |
1574 lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len word) = LENGTH('b)" |
2010 lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len word) = LENGTH('b)" |
1575 unfolding target_size_def word_size Let_def .. |
2011 by transfer simp |
1576 |
2012 |
1577 lemma is_down: "is_down c \<longleftrightarrow> LENGTH('b) \<le> LENGTH('a)" |
2013 lemma is_down: "is_down c \<longleftrightarrow> LENGTH('b) \<le> LENGTH('a)" |
1578 for c :: "'a::len word \<Rightarrow> 'b::len word" |
2014 for c :: "'a::len word \<Rightarrow> 'b::len word" |
1579 by (simp only: is_down_def source_size target_size) |
2015 by transfer simp |
1580 |
2016 |
1581 lemma is_up: "is_up c \<longleftrightarrow> LENGTH('a) \<le> LENGTH('b)" |
2017 lemma is_up: "is_up c \<longleftrightarrow> LENGTH('a) \<le> LENGTH('b)" |
1582 for c :: "'a::len word \<Rightarrow> 'b::len word" |
2018 for c :: "'a::len word \<Rightarrow> 'b::len word" |
1583 by (simp only: is_up_def source_size target_size) |
2019 by transfer simp |
1584 |
2020 |
1585 lemmas is_up_down = trans [OF is_up is_down [symmetric]] |
2021 lemma is_up_down: |
1586 |
2022 \<open>is_up c \<longleftrightarrow> is_down d\<close> |
1587 lemma down_cast_same [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast" |
2023 for c :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
1588 apply (unfold is_down) |
2024 and d :: \<open>'b::len word \<Rightarrow> 'a::len word\<close> |
1589 apply safe |
2025 by transfer simp |
1590 apply (rule ext) |
2026 |
1591 apply (unfold ucast_def scast_def uint_sint) |
2027 context |
1592 apply (rule word_ubin.norm_eq_iff [THEN iffD1]) |
2028 fixes dummy_types :: \<open>'a::len \<times> 'b::len\<close> |
1593 apply simp |
2029 begin |
1594 done |
2030 |
1595 |
2031 private abbreviation (input) UCAST :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
1596 lemma word_rev_tf: |
2032 where \<open>UCAST == ucast\<close> |
1597 "to_bl (of_bl bl::'a::len word) = |
2033 |
1598 rev (takefill False (LENGTH('a)) (rev bl))" |
2034 private abbreviation (input) SCAST :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> |
1599 by (auto simp: of_bl_def uint_bl bl_bin_bl_rtf word_ubin.eq_norm word_size) |
2035 where \<open>SCAST == scast\<close> |
1600 |
2036 |
1601 lemma word_rep_drop: |
2037 lemma down_cast_same: |
1602 "to_bl (of_bl bl::'a::len word) = |
2038 \<open>UCAST = scast\<close> if \<open>is_down UCAST\<close> |
1603 replicate (LENGTH('a) - length bl) False @ |
2039 by (rule ext, use that in transfer) (simp add: take_bit_signed_take_bit) |
1604 drop (length bl - LENGTH('a)) bl" |
2040 |
1605 by (simp add: word_rev_tf takefill_alt rev_take) |
2041 lemma sint_up_scast: |
1606 |
2042 \<open>sint (SCAST w) = sint w\<close> if \<open>is_up SCAST\<close> |
1607 lemma to_bl_ucast: |
2043 using that by transfer (simp add: min_def Suc_leI le_diff_iff) |
1608 "to_bl (ucast (w::'b::len word) ::'a::len word) = |
2044 |
1609 replicate (LENGTH('a) - LENGTH('b)) False @ |
2045 lemma uint_up_ucast: |
1610 drop (LENGTH('b) - LENGTH('a)) (to_bl w)" |
2046 \<open>uint (UCAST w) = uint w\<close> if \<open>is_up UCAST\<close> |
1611 apply (unfold ucast_bl) |
2047 using that by transfer (simp add: min_def) |
1612 apply (rule trans) |
2048 |
1613 apply (rule word_rep_drop) |
2049 lemma ucast_up_ucast: |
1614 apply simp |
2050 \<open>ucast (UCAST w) = ucast w\<close> if \<open>is_up UCAST\<close> |
1615 done |
2051 using that by transfer (simp add: ac_simps) |
1616 |
2052 |
1617 lemma ucast_up_app [OF refl]: |
2053 lemma ucast_up_ucast_id: |
1618 "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow> |
2054 \<open>ucast (UCAST w) = w\<close> if \<open>is_up UCAST\<close> |
1619 to_bl (uc w) = replicate n False @ (to_bl w)" |
2055 using that by (simp add: ucast_up_ucast) |
1620 by (auto simp add : source_size target_size to_bl_ucast) |
2056 |
1621 |
2057 lemma scast_up_scast: |
1622 lemma ucast_down_drop [OF refl]: |
2058 \<open>scast (SCAST w) = scast w\<close> if \<open>is_up SCAST\<close> |
1623 "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> |
2059 using that by transfer (simp add: ac_simps) |
1624 to_bl (uc w) = drop n (to_bl w)" |
2060 |
1625 by (auto simp add : source_size target_size to_bl_ucast) |
2061 lemma scast_up_scast_id: |
1626 |
2062 \<open>scast (SCAST w) = w\<close> if \<open>is_up SCAST\<close> |
1627 lemma scast_down_drop [OF refl]: |
2063 using that by (simp add: scast_up_scast) |
1628 "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow> |
2064 |
1629 to_bl (sc w) = drop n (to_bl w)" |
2065 lemma isduu: |
1630 apply (subgoal_tac "sc = ucast") |
2066 \<open>is_up UCAST\<close> if \<open>is_down d\<close> |
1631 apply safe |
2067 for d :: \<open>'b word \<Rightarrow> 'a word\<close> |
1632 apply simp |
2068 using that is_up_down [of UCAST d] by simp |
1633 apply (erule ucast_down_drop) |
2069 |
1634 apply (rule down_cast_same [symmetric]) |
2070 lemma isdus: |
1635 apply (simp add : source_size target_size is_down) |
2071 \<open>is_up SCAST\<close> if \<open>is_down d\<close> |
1636 done |
2072 for d :: \<open>'b word \<Rightarrow> 'a word\<close> |
1637 |
2073 using that is_up_down [of SCAST d] by simp |
1638 lemma sint_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w" |
2074 |
1639 apply (unfold is_up) |
|
1640 apply safe |
|
1641 apply (simp add: scast_def word_sbin.eq_norm) |
|
1642 apply (rule box_equals) |
|
1643 prefer 3 |
|
1644 apply (rule word_sbin.norm_Rep) |
|
1645 apply (rule sbintrunc_sbintrunc_l) |
|
1646 defer |
|
1647 apply (subst word_sbin.norm_Rep) |
|
1648 apply (rule refl) |
|
1649 apply simp |
|
1650 done |
|
1651 |
|
1652 lemma uint_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w" |
|
1653 apply (unfold is_up) |
|
1654 apply safe |
|
1655 apply (rule bin_eqI) |
|
1656 apply (fold word_test_bit_def) |
|
1657 apply (auto simp add: nth_ucast) |
|
1658 apply (auto simp add: test_bit_bin) |
|
1659 done |
|
1660 |
|
1661 lemma ucast_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w" |
|
1662 apply (simp (no_asm) add: ucast_def) |
|
1663 apply (clarsimp simp add: uint_up_ucast) |
|
1664 done |
|
1665 |
|
1666 lemma scast_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w" |
|
1667 apply (simp (no_asm) add: scast_def) |
|
1668 apply (clarsimp simp add: sint_up_scast) |
|
1669 done |
|
1670 |
|
1671 lemma ucast_of_bl_up [OF refl]: "w = of_bl bl \<Longrightarrow> size bl \<le> size w \<Longrightarrow> ucast w = of_bl bl" |
|
1672 by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI) |
|
1673 |
|
1674 lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id] |
|
1675 lemmas scast_up_scast_id = trans [OF scast_up_scast scast_id] |
|
1676 |
|
1677 lemmas isduu = is_up_down [where c = "ucast", THEN iffD2] |
|
1678 lemmas isdus = is_up_down [where c = "scast", THEN iffD2] |
|
1679 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id] |
2075 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id] |
1680 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id] |
2076 lemmas scast_down_scast_id = isdus [THEN scast_up_scast_id] |
1681 |
2077 |
1682 lemma up_ucast_surj: |
2078 lemma up_ucast_surj: |
1683 "is_up (ucast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow> |
2079 \<open>surj (ucast :: 'b word \<Rightarrow> 'a word)\<close> if \<open>is_up UCAST\<close> |
1684 surj (ucast :: 'a word \<Rightarrow> 'b word)" |
2080 by (rule surjI) (use that in \<open>rule ucast_up_ucast_id\<close>) |
1685 by (rule surjI) (erule ucast_up_ucast_id) |
|
1686 |
2081 |
1687 lemma up_scast_surj: |
2082 lemma up_scast_surj: |
1688 "is_up (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow> |
2083 \<open>surj (scast :: 'b word \<Rightarrow> 'a word)\<close> if \<open>is_up SCAST\<close> |
1689 surj (scast :: 'a word \<Rightarrow> 'b word)" |
2084 by (rule surjI) (use that in \<open>rule scast_up_scast_id\<close>) |
1690 by (rule surjI) (erule scast_up_scast_id) |
2085 |
|
2086 lemma down_ucast_inj: |
|
2087 \<open>inj_on UCAST A\<close> if \<open>is_down (ucast :: 'b word \<Rightarrow> 'a word)\<close> |
|
2088 by (rule inj_on_inverseI) (use that in \<open>rule ucast_down_ucast_id\<close>) |
1691 |
2089 |
1692 lemma down_scast_inj: |
2090 lemma down_scast_inj: |
1693 "is_down (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow> |
2091 \<open>inj_on SCAST A\<close> if \<open>is_down (scast :: 'b word \<Rightarrow> 'a word)\<close> |
1694 inj_on (ucast :: 'a word \<Rightarrow> 'b word) A" |
2092 by (rule inj_on_inverseI) (use that in \<open>rule scast_down_scast_id\<close>) |
1695 by (rule inj_on_inverseI, erule scast_down_scast_id) |
2093 |
1696 |
2094 lemma ucast_down_wi: |
1697 lemma down_ucast_inj: |
2095 \<open>UCAST (word_of_int x) = word_of_int x\<close> if \<open>is_down UCAST\<close> |
1698 "is_down (ucast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow> |
2096 using that by transfer simp |
1699 inj_on (ucast :: 'a word \<Rightarrow> 'b word) A" |
2097 |
1700 by (rule inj_on_inverseI) (erule ucast_down_ucast_id) |
2098 lemma ucast_down_no: |
|
2099 \<open>UCAST (numeral bin) = numeral bin\<close> if \<open>is_down UCAST\<close> |
|
2100 using that by transfer simp |
|
2101 |
|
2102 lemma ucast_down_bl: |
|
2103 "UCAST (of_bl bl) = of_bl bl" if \<open>is_down UCAST\<close> |
|
2104 using that by transfer simp |
|
2105 |
|
2106 end |
1701 |
2107 |
1702 lemma of_bl_append_same: "of_bl (X @ to_bl w) = w" |
2108 lemma of_bl_append_same: "of_bl (X @ to_bl w) = w" |
1703 by (rule word_bl.Rep_eqD) (simp add: word_rep_drop) |
2109 by transfer (simp add: bl_to_bin_app_cat) |
1704 |
2110 |
1705 lemma ucast_down_wi [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x" |
2111 lemma ucast_of_bl_up: |
1706 apply (unfold is_down) |
2112 \<open>ucast (of_bl bl :: 'a::len word) = of_bl bl\<close> |
1707 apply (clarsimp simp add: ucast_def word_ubin.eq_norm) |
2113 if \<open>size bl \<le> size (of_bl bl :: 'a::len word)\<close> |
1708 apply (rule word_ubin.norm_eq_iff [THEN iffD1]) |
2114 using that |
1709 apply (erule bintrunc_bintrunc_ge) |
2115 apply transfer |
1710 done |
2116 apply (rule bit_eqI) |
1711 |
2117 apply (auto simp add: bit_take_bit_iff) |
1712 lemma ucast_down_no [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (numeral bin) = numeral bin" |
2118 apply (subst (asm) trunc_bl2bin_len [symmetric]) |
1713 unfolding word_numeral_alt by clarify (rule ucast_down_wi) |
2119 apply (auto simp only: bit_take_bit_iff) |
1714 |
2120 done |
1715 lemma ucast_down_bl [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl" |
|
1716 unfolding of_bl_def by clarify (erule ucast_down_wi) |
|
1717 |
2121 |
1718 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] |
2122 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] |
1719 |
2123 |
1720 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def |
2124 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def |
1721 |
2125 |
1741 apply (auto simp add: drop_bit_eq_div take_bit_eq_mod min_def) |
2145 apply (auto simp add: drop_bit_eq_div take_bit_eq_mod min_def) |
1742 apply (auto elim!: evenE) |
2146 apply (auto elim!: evenE) |
1743 apply (metis div_exp_eq mod_div_trivial mult.commute nonzero_mult_div_cancel_left power_Suc0_right power_add zero_neq_numeral) |
2147 apply (metis div_exp_eq mod_div_trivial mult.commute nonzero_mult_div_cancel_left power_Suc0_right power_add zero_neq_numeral) |
1744 done |
2148 done |
1745 |
2149 |
|
2150 lemma word_rev_tf: |
|
2151 "to_bl (of_bl bl::'a::len word) = |
|
2152 rev (takefill False (LENGTH('a)) (rev bl))" |
|
2153 by (auto simp: of_bl_def uint_bl bl_bin_bl_rtf word_ubin.eq_norm word_size) |
|
2154 |
|
2155 lemma word_rep_drop: |
|
2156 "to_bl (of_bl bl::'a::len word) = |
|
2157 replicate (LENGTH('a) - length bl) False @ |
|
2158 drop (length bl - LENGTH('a)) bl" |
|
2159 by (simp add: word_rev_tf takefill_alt rev_take) |
|
2160 |
|
2161 lemma to_bl_ucast: |
|
2162 "to_bl (ucast (w::'b::len word) ::'a::len word) = |
|
2163 replicate (LENGTH('a) - LENGTH('b)) False @ |
|
2164 drop (LENGTH('b) - LENGTH('a)) (to_bl w)" |
|
2165 apply (unfold ucast_bl) |
|
2166 apply (rule trans) |
|
2167 apply (rule word_rep_drop) |
|
2168 apply simp |
|
2169 done |
|
2170 |
|
2171 lemma ucast_up_app: |
|
2172 \<open>to_bl (ucast w :: 'b::len word) = replicate n False @ (to_bl w)\<close> |
|
2173 if \<open>source_size (ucast :: 'a word \<Rightarrow> 'b word) + n = target_size (ucast :: 'a word \<Rightarrow> 'b word)\<close> |
|
2174 for w :: \<open>'a::len word\<close> |
|
2175 using that |
|
2176 by (auto simp add : source_size target_size to_bl_ucast) |
|
2177 |
|
2178 lemma ucast_down_drop [OF refl]: |
|
2179 "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> |
|
2180 to_bl (uc w) = drop n (to_bl w)" |
|
2181 by (auto simp add : source_size target_size to_bl_ucast) |
|
2182 |
|
2183 lemma scast_down_drop [OF refl]: |
|
2184 "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow> |
|
2185 to_bl (sc w) = drop n (to_bl w)" |
|
2186 apply (subgoal_tac "sc = ucast") |
|
2187 apply safe |
|
2188 apply simp |
|
2189 apply (erule ucast_down_drop) |
|
2190 apply (rule down_cast_same [symmetric]) |
|
2191 apply (simp add : source_size target_size is_down) |
|
2192 done |
|
2193 |
1746 |
2194 |
1747 subsection \<open>Word Arithmetic\<close> |
2195 subsection \<open>Word Arithmetic\<close> |
1748 |
2196 |
1749 lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" |
2197 lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" |
1750 by (fact word_less_def) |
2198 by (fact word_less_def) |
1751 |
2199 |
1752 lemma signed_linorder: "class.linorder word_sle word_sless" |
2200 lemma signed_linorder: "class.linorder word_sle word_sless" |
1753 by standard (auto simp: word_sle_def word_sless_def) |
2201 by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff) |
1754 |
2202 |
1755 interpretation signed: linorder "word_sle" "word_sless" |
2203 interpretation signed: linorder "word_sle" "word_sless" |
1756 by (rule signed_linorder) |
2204 by (rule signed_linorder) |
1757 |
2205 |
1758 lemma udvdI: "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b" |
2206 lemma udvdI: "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b" |
1760 |
2208 |
1761 lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b |
2209 lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b |
1762 lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b |
2210 lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b |
1763 lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b |
2211 lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b |
1764 lemmas word_le_no [simp] = word_le_def [of "numeral a" "numeral b"] for a b |
2212 lemmas word_le_no [simp] = word_le_def [of "numeral a" "numeral b"] for a b |
1765 lemmas word_sless_no [simp] = word_sless_def [of "numeral a" "numeral b"] for a b |
2213 lemmas word_sless_no [simp] = word_sless_eq [of "numeral a" "numeral b"] for a b |
1766 lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b |
2214 lemmas word_sle_no [simp] = word_sle_eq [of "numeral a" "numeral b"] for a b |
1767 |
2215 |
1768 lemma word_m1_wi: "- 1 = word_of_int (- 1)" |
2216 lemma word_m1_wi: "- 1 = word_of_int (- 1)" |
1769 by (simp add: word_neg_numeral_alt [of Num.One]) |
2217 by (simp add: word_neg_numeral_alt [of Num.One]) |
1770 |
2218 |
1771 lemma word_0_bl [simp]: "of_bl [] = 0" |
2219 lemma word_0_bl [simp]: "of_bl [] = 0" |
1772 by (simp add: of_bl_def) |
2220 by (simp add: of_bl_def) |
1773 |
2221 |
1774 lemma word_1_bl: "of_bl [True] = 1" |
2222 lemma word_1_bl: "of_bl [True] = 1" |
1775 by (simp add: of_bl_def bl_to_bin_def) |
2223 by (simp add: of_bl_def bl_to_bin_def) |
1776 |
2224 |
1777 lemma uint_eq_0 [simp]: "uint 0 = 0" |
|
1778 unfolding word_0_wi word_ubin.eq_norm by simp |
|
1779 |
|
1780 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0" |
2225 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0" |
1781 by (simp add: of_bl_def bl_to_bin_rep_False) |
2226 by (simp add: of_bl_def bl_to_bin_rep_False) |
1782 |
2227 |
1783 lemma to_bl_0 [simp]: "to_bl (0::'a::len word) = replicate (LENGTH('a)) False" |
2228 lemma to_bl_0 [simp]: "to_bl (0::'a::len word) = replicate (LENGTH('a)) False" |
1784 by (simp add: uint_bl word_size bin_to_bl_zero) |
2229 by (simp add: uint_bl word_size bin_to_bl_zero) |
1785 |
2230 |
1786 lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0" |
2231 lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0" |
1787 by (simp add: word_uint_eq_iff) |
2232 by (simp add: word_uint_eq_iff) |
1788 |
2233 |
1789 lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0" |
2234 lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0" |
1790 by (auto simp: unat_def nat_eq_iff uint_0_iff) |
2235 by transfer (auto intro: antisym) |
1791 |
2236 |
1792 lemma unat_0 [simp]: "unat 0 = 0" |
2237 lemma unat_0 [simp]: "unat 0 = 0" |
1793 by (auto simp: unat_def) |
2238 by transfer simp |
1794 |
2239 |
1795 lemma size_0_same': "size w = 0 \<Longrightarrow> w = v" |
2240 lemma size_0_same': "size w = 0 \<Longrightarrow> w = v" |
1796 for v w :: "'a::len word" |
2241 for v w :: "'a::len word" |
1797 apply (unfold word_size) |
2242 by (unfold word_size) simp |
1798 apply (rule box_equals) |
|
1799 defer |
|
1800 apply (rule word_uint.Rep_inverse)+ |
|
1801 apply (rule word_ubin.norm_eq_iff [THEN iffD1]) |
|
1802 apply simp |
|
1803 done |
|
1804 |
2243 |
1805 lemmas size_0_same = size_0_same' [unfolded word_size] |
2244 lemmas size_0_same = size_0_same' [unfolded word_size] |
1806 |
2245 |
1807 lemmas unat_eq_0 = unat_0_iff |
2246 lemmas unat_eq_0 = unat_0_iff |
1808 lemmas unat_eq_zero = unat_0_iff |
2247 lemmas unat_eq_zero = unat_0_iff |
1809 |
2248 |
1810 lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0" |
2249 lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0" |
1811 by (auto simp: unat_0_iff [symmetric]) |
2250 by (auto simp: unat_0_iff [symmetric]) |
1812 |
2251 |
1813 lemma ucast_0 [simp]: "ucast 0 = 0" |
2252 lemma ucast_0 [simp]: "ucast 0 = 0" |
1814 by (simp add: ucast_def) |
2253 by transfer simp |
1815 |
2254 |
1816 lemma sint_0 [simp]: "sint 0 = 0" |
2255 lemma sint_0 [simp]: "sint 0 = 0" |
1817 by (simp add: sint_uint) |
2256 by (simp add: sint_uint) |
1818 |
2257 |
1819 lemma scast_0 [simp]: "scast 0 = 0" |
2258 lemma scast_0 [simp]: "scast 0 = 0" |
1820 by (simp add: scast_def) |
2259 by transfer simp |
1821 |
2260 |
1822 lemma sint_n1 [simp] : "sint (- 1) = - 1" |
2261 lemma sint_n1 [simp] : "sint (- 1) = - 1" |
1823 by (simp only: word_m1_wi word_sbin.eq_norm) simp |
2262 by transfer simp |
1824 |
2263 |
1825 lemma scast_n1 [simp]: "scast (- 1) = - 1" |
2264 lemma scast_n1 [simp]: "scast (- 1) = - 1" |
1826 by (simp add: scast_def) |
2265 by transfer simp |
1827 |
2266 |
1828 lemma uint_1 [simp]: "uint (1::'a::len word) = 1" |
2267 lemma uint_1 [simp]: "uint (1::'a::len word) = 1" |
1829 by (simp only: word_1_wi word_ubin.eq_norm) simp |
2268 by transfer simp |
1830 |
2269 |
1831 lemma unat_1 [simp]: "unat (1::'a::len word) = 1" |
2270 lemma unat_1 [simp]: "unat (1::'a::len word) = 1" |
1832 by (simp add: unat_def) |
2271 by transfer simp |
1833 |
2272 |
1834 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" |
2273 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" |
1835 by (simp add: ucast_def) |
2274 by transfer simp |
1836 |
2275 |
1837 \<comment> \<open>now, to get the weaker results analogous to \<open>word_div\<close>/\<open>mod_def\<close>\<close> |
2276 \<comment> \<open>now, to get the weaker results analogous to \<open>word_div\<close>/\<open>mod_def\<close>\<close> |
1838 |
2277 |
1839 |
2278 |
1840 subsection \<open>Transferring goals from words to ints\<close> |
2279 subsection \<open>Transferring goals from words to ints\<close> |
3236 |
3664 |
3237 |
3665 |
3238 subsection \<open>Shifting, Rotating, and Splitting Words\<close> |
3666 subsection \<open>Shifting, Rotating, and Splitting Words\<close> |
3239 |
3667 |
3240 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (2 * w)" |
3668 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (2 * w)" |
3241 unfolding shiftl1_def |
3669 by (fact shiftl1.abs_eq) |
3242 apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm) |
|
3243 apply (simp add: mod_mult_right_eq take_bit_eq_mod) |
|
3244 done |
|
3245 |
3670 |
3246 lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)" |
3671 lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)" |
3247 unfolding word_numeral_alt shiftl1_wi by simp |
3672 unfolding word_numeral_alt shiftl1_wi by simp |
3248 |
3673 |
3249 lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)" |
3674 lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)" |
3250 unfolding word_neg_numeral_alt shiftl1_wi by simp |
3675 unfolding word_neg_numeral_alt shiftl1_wi by simp |
3251 |
3676 |
3252 lemma shiftl1_0 [simp] : "shiftl1 0 = 0" |
3677 lemma shiftl1_0 [simp] : "shiftl1 0 = 0" |
3253 by (simp add: shiftl1_def) |
3678 by transfer simp |
3254 |
3679 |
3255 lemma shiftl1_def_u: "shiftl1 w = word_of_int (2 * uint w)" |
3680 lemma shiftl1_def_u: "shiftl1 w = word_of_int (2 * uint w)" |
3256 by (fact shiftl1_def) |
3681 by (fact shiftl1_eq) |
3257 |
3682 |
3258 lemma shiftl1_def_s: "shiftl1 w = word_of_int (2 * sint w)" |
3683 lemma shiftl1_def_s: "shiftl1 w = word_of_int (2 * sint w)" |
3259 by (simp add: shiftl1_def wi_hom_syms) |
3684 by (simp add: shiftl1_def_u wi_hom_syms) |
3260 |
3685 |
3261 lemma shiftr1_0 [simp]: "shiftr1 0 = 0" |
3686 lemma shiftr1_0 [simp]: "shiftr1 0 = 0" |
3262 by (simp add: shiftr1_def) |
3687 by transfer simp |
3263 |
3688 |
3264 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0" |
3689 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0" |
3265 by (simp add: sshiftr1_def) |
3690 by transfer simp |
3266 |
3691 |
3267 lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1" |
3692 lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1" |
3268 by (simp add: sshiftr1_def) |
3693 by transfer simp |
3269 |
3694 |
3270 lemma shiftl_0 [simp]: "(0::'a::len word) << n = 0" |
3695 lemma shiftl_0 [simp]: "(0::'a::len word) << n = 0" |
3271 by (induct n) (auto simp: shiftl_def) |
3696 by transfer simp |
3272 |
3697 |
3273 lemma shiftr_0 [simp]: "(0::'a::len word) >> n = 0" |
3698 lemma shiftr_0 [simp]: "(0::'a::len word) >> n = 0" |
3274 by (induct n) (auto simp: shiftr_def) |
3699 by transfer simp |
3275 |
3700 |
3276 lemma sshiftr_0 [simp]: "0 >>> n = 0" |
3701 lemma sshiftr_0 [simp]: "0 >>> n = 0" |
3277 by (induct n) (auto simp: sshiftr_def) |
3702 by transfer simp |
3278 |
3703 |
3279 lemma sshiftr_n1 [simp]: "-1 >>> n = -1" |
3704 lemma sshiftr_n1 [simp]: "-1 >>> n = -1" |
3280 by (induct n) (auto simp: sshiftr_def) |
3705 by transfer simp |
3281 |
3706 |
3282 lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)" |
3707 lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)" |
3283 apply (unfold shiftl1_def word_test_bit_def) |
3708 by transfer (auto simp add: bit_double_iff) |
3284 apply (simp add: nth_bintr word_ubin.eq_norm word_size) |
|
3285 apply (cases n) |
|
3286 apply (simp_all add: bit_Suc) |
|
3287 done |
|
3288 |
3709 |
3289 lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)" |
3710 lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)" |
3290 for w :: "'a::len word" |
3711 for w :: "'a::len word" |
3291 apply (unfold shiftl_def) |
3712 by transfer (auto simp add: bit_push_bit_iff) |
3292 apply (induct m arbitrary: n) |
|
3293 apply (force elim!: test_bit_size) |
|
3294 apply (clarsimp simp add : nth_shiftl1 word_size) |
|
3295 apply arith |
|
3296 done |
|
3297 |
3713 |
3298 lemmas nth_shiftl = nth_shiftl' [unfolded word_size] |
3714 lemmas nth_shiftl = nth_shiftl' [unfolded word_size] |
3299 |
3715 |
3300 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n" |
3716 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n" |
3301 apply (auto simp add: shiftr1_def word_test_bit_def word_ubin.eq_norm bit_take_bit_iff bit_Suc) |
3717 by transfer (auto simp add: bit_take_bit_iff simp flip: bit_Suc) |
3302 apply (metis (no_types, hide_lams) add_Suc_right add_diff_cancel_left' bit_Suc diff_is_0_eq' le_Suc_ex less_imp_le linorder_not_le test_bit_bin word_test_bit_def) |
|
3303 done |
|
3304 |
3718 |
3305 lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)" |
3719 lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)" |
3306 for w :: "'a::len word" |
3720 for w :: "'a::len word" |
3307 apply (unfold shiftr_def) |
3721 apply (unfold shiftr_def) |
3308 apply (induct "m" arbitrary: n) |
3722 apply (induct "m" arbitrary: n) |
3314 where \<open>f\<close> (ie \<open>bin_rest\<close>) takes normal arguments to normal results, |
3728 where \<open>f\<close> (ie \<open>bin_rest\<close>) takes normal arguments to normal results, |
3315 thus we get (2) from (1) |
3729 thus we get (2) from (1) |
3316 \<close> |
3730 \<close> |
3317 |
3731 |
3318 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" |
3732 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" |
3319 apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i) |
3733 by transfer simp |
3320 apply (subst bintr_uint [symmetric, OF order_refl]) |
|
3321 apply (simp only : bintrunc_bintrunc_l) |
|
3322 apply simp |
|
3323 done |
|
3324 |
3734 |
3325 lemma bit_sshiftr1_iff: |
3735 lemma bit_sshiftr1_iff: |
3326 \<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close> |
3736 \<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close> |
3327 for w :: \<open>'a::len word\<close> |
3737 for w :: \<open>'a::len word\<close> |
3328 apply (cases \<open>LENGTH('a)\<close>) |
3738 apply transfer |
3329 apply simp |
3739 apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc) |
3330 apply (simp add: sshiftr1_def bit_word_of_int_iff bit_sint_iff flip: bit_Suc) |
3740 using le_less_Suc_eq apply fastforce |
3331 apply transfer apply auto |
3741 using le_less_Suc_eq apply fastforce |
3332 done |
3742 done |
3333 |
3743 |
3334 lemma bit_sshiftr_word_iff: |
3744 lemma bit_sshiftr_word_iff: |
3335 \<open>bit (w >>> m) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else (m + n))\<close> |
3745 \<open>bit (w >>> m) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else (m + n))\<close> |
3336 for w :: \<open>'a::len word\<close> |
3746 for w :: \<open>'a::len word\<close> |
3337 apply (cases \<open>LENGTH('a)\<close>) |
3747 apply transfer |
3338 apply simp |
3748 apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le simp flip: bit_Suc) |
3339 apply (simp only:) |
3749 using le_less_Suc_eq apply fastforce |
3340 apply (induction m arbitrary: n) |
3750 using le_less_Suc_eq apply fastforce |
3341 apply (auto simp add: sshiftr_def bit_sshiftr1_iff not_le less_diff_conv) |
|
3342 done |
3751 done |
3343 |
3752 |
3344 lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)" |
3753 lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)" |
3345 apply (unfold sshiftr1_def word_test_bit_def) |
3754 apply transfer |
3346 apply (simp add: nth_bintr word_ubin.eq_norm bit_Suc [symmetric] word_size) |
3755 apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc) |
3347 apply (simp add: nth_bintr uint_sint) |
3756 using le_less_Suc_eq apply fastforce |
3348 apply (auto simp add: bin_nth_sint) |
3757 using le_less_Suc_eq apply fastforce |
3349 done |
3758 done |
3350 |
3759 |
3351 lemma nth_sshiftr [rule_format] : |
3760 lemma nth_sshiftr : |
3352 "\<forall>n. sshiftr w m !! n = |
3761 "sshiftr w m !! n = |
3353 (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))" |
3762 (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))" |
3354 apply (unfold sshiftr_def) |
3763 apply transfer |
3355 apply (induct_tac m) |
3764 apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le ac_simps) |
3356 apply (simp add: test_bit_bl) |
3765 using le_less_Suc_eq apply fastforce |
3357 apply (clarsimp simp add: nth_sshiftr1 word_size) |
3766 using le_less_Suc_eq apply fastforce |
3358 apply safe |
|
3359 apply arith |
|
3360 apply arith |
|
3361 apply (erule thin_rl) |
|
3362 apply (case_tac n) |
|
3363 apply safe |
|
3364 apply simp |
|
3365 apply simp |
|
3366 apply (erule thin_rl) |
|
3367 apply (case_tac n) |
|
3368 apply safe |
|
3369 apply simp |
|
3370 apply simp |
|
3371 apply arith+ |
|
3372 done |
3767 done |
3373 |
3768 |
3374 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2" |
3769 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2" |
3375 apply (unfold shiftr1_def) |
3770 by (fact uint_shiftr1) |
3376 apply (rule word_uint.Abs_inverse) |
|
3377 apply (simp add: uints_num pos_imp_zdiv_nonneg_iff) |
|
3378 apply (metis uint_lt2p uint_shiftr1) |
|
3379 done |
|
3380 |
3771 |
3381 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2" |
3772 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2" |
3382 apply (unfold sshiftr1_def) |
3773 by transfer simp |
3383 apply (simp add: word_sbin.eq_norm) |
|
3384 apply (rule trans) |
|
3385 defer |
|
3386 apply (subst word_sbin.norm_Rep [symmetric]) |
|
3387 apply (rule refl) |
|
3388 apply (subst word_sbin.norm_Rep [symmetric]) |
|
3389 apply (unfold One_nat_def) |
|
3390 apply (rule sbintrunc_rest) |
|
3391 done |
|
3392 |
3774 |
3393 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n" |
3775 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n" |
3394 apply (unfold shiftr_def) |
3776 apply (unfold shiftr_def) |
3395 apply (induct n) |
3777 apply (induct n) |
3396 apply simp |
3778 apply simp |
3397 apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric]) |
3779 apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric]) |
3398 done |
3780 done |
3399 |
3781 |
3400 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n" |
3782 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n" |
3401 apply (unfold sshiftr_def) |
3783 apply transfer |
3402 apply (induct n) |
3784 apply (auto simp add: bit_eq_iff bit_signed_take_bit_iff bit_drop_bit_eq min_def simp flip: drop_bit_eq_div) |
3403 apply simp |
|
3404 apply (simp add: sshiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric]) |
|
3405 done |
3785 done |
3406 |
3786 |
3407 lemma bit_bshiftr1_iff: |
3787 lemma bit_bshiftr1_iff: |
3408 \<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close> |
3788 \<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close> |
3409 for w :: \<open>'a::len word\<close> |
3789 for w :: \<open>'a::len word\<close> |
3410 apply (cases \<open>LENGTH('a)\<close>) |
3790 apply transfer |
3411 apply simp |
3791 apply (simp add: bit_take_bit_iff flip: bit_Suc) |
3412 apply (simp add: bshiftr1_def bit_of_bl_iff nth_append not_less rev_nth nth_butlast nth_to_bl) |
3792 apply (subst disjunctive_add) |
3413 apply (use bit_imp_le_length in fastforce) |
3793 apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff simp flip: bit_Suc) |
3414 done |
3794 done |
3415 |
3795 |
3416 |
3796 |
3417 subsubsection \<open>shift functions in terms of lists of bools\<close> |
3797 subsubsection \<open>shift functions in terms of lists of bools\<close> |
3418 |
3798 |
3419 lemma bshiftr1_numeral [simp]: |
3799 lemma bshiftr1_numeral [simp]: |
3420 \<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close> |
3800 \<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close> |
3421 by (simp add: bshiftr1_def) |
3801 by (simp add: bshiftr1_eq) |
3422 |
3802 |
3423 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)" |
3803 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)" |
3424 unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp |
3804 unfolding bshiftr1_eq by (rule word_bl.Abs_inverse) simp |
3425 |
3805 |
3426 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])" |
3806 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])" |
3427 by (simp add: of_bl_def bl_to_bin_append) |
3807 by (simp add: of_bl_def bl_to_bin_append) |
3428 |
3808 |
3429 lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])" |
3809 lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])" |
4493 done |
4869 done |
4494 |
4870 |
4495 |
4871 |
4496 subsection \<open>Rotation\<close> |
4872 subsection \<open>Rotation\<close> |
4497 |
4873 |
4498 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified] |
4874 lemmas word_rot_defs = word_roti_eq_word_rotr_word_rotl word_rotr_eq word_rotl_eq |
4499 |
|
4500 lemma bit_word_rotl_iff: |
|
4501 \<open>bit (word_rotl m w) n \<longleftrightarrow> |
|
4502 n < LENGTH('a) \<and> bit w ((n + (LENGTH('a) - m mod LENGTH('a))) mod LENGTH('a))\<close> |
|
4503 for w :: \<open>'a::len word\<close> |
|
4504 proof (cases \<open>n < LENGTH('a)\<close>) |
|
4505 case False |
|
4506 then show ?thesis |
|
4507 by (auto dest: bit_imp_le_length) |
|
4508 next |
|
4509 case True |
|
4510 define k where \<open>k = int n - int m\<close> |
|
4511 then have k: \<open>int n = k + int m\<close> |
|
4512 by simp |
|
4513 define l where \<open>l = int LENGTH('a)\<close> |
|
4514 then have l: \<open>int LENGTH('a) = l\<close> \<open>l > 0\<close> |
|
4515 by simp_all |
|
4516 have *: \<open>int (m - n) = int m - int n\<close> if \<open>n \<le> m\<close> for n m |
|
4517 using that by (simp add: int_minus) |
|
4518 from \<open>l > 0\<close> have \<open>l = 1 + (k mod l + ((- 1 - k) mod l))\<close> |
|
4519 using minus_mod_int_eq [of l \<open>k + 1\<close>] by (simp add: algebra_simps) |
|
4520 then have \<open>int (LENGTH('a) - Suc ((m + LENGTH('a) - Suc n) mod LENGTH('a))) = |
|
4521 int ((n + LENGTH('a) - m mod LENGTH('a)) mod LENGTH('a))\<close> |
|
4522 by (simp add: * k l zmod_int Suc_leI trans_le_add2 algebra_simps mod_simps \<open>n < LENGTH('a)\<close>) |
|
4523 then have \<open>LENGTH('a) - Suc ((m + LENGTH('a) - Suc n) mod LENGTH('a)) = |
|
4524 (n + LENGTH('a) - m mod LENGTH('a)) mod LENGTH('a)\<close> |
|
4525 by simp |
|
4526 with True show ?thesis |
|
4527 by (simp add: word_rotl_def bit_of_bl_iff rev_nth nth_rotate nth_to_bl) |
|
4528 qed |
|
4529 |
|
4530 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def |
|
4531 |
|
4532 lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs" |
|
4533 apply (rule box_equals) |
|
4534 defer |
|
4535 apply (rule rotate_conv_mod [symmetric])+ |
|
4536 apply simp |
|
4537 done |
|
4538 |
|
4539 lemmas rotate_eqs = |
|
4540 trans [OF rotate0 [THEN fun_cong] id_apply] |
|
4541 rotate_rotate [symmetric] |
|
4542 rotate_id |
|
4543 rotate_conv_mod |
|
4544 rotate_eq_mod |
|
4545 |
|
4546 |
|
4547 subsubsection \<open>Rotation of list to right\<close> |
|
4548 |
|
4549 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l" |
|
4550 by (cases l) (auto simp: rotater1_def) |
|
4551 |
|
4552 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l" |
|
4553 apply (unfold rotater1_def) |
|
4554 apply (cases "l") |
|
4555 apply (case_tac [2] "list") |
|
4556 apply auto |
|
4557 done |
|
4558 |
|
4559 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l" |
|
4560 by (cases l) (auto simp: rotater1_def) |
|
4561 |
|
4562 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)" |
|
4563 by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl') |
|
4564 |
|
4565 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)" |
|
4566 by (induct n) (auto simp: rotater_def intro: rotater1_rev') |
|
4567 |
|
4568 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))" |
|
4569 using rotater_rev' [where xs = "rev ys"] by simp |
|
4570 |
|
4571 lemma rotater_drop_take: |
|
4572 "rotater n xs = |
|
4573 drop (length xs - n mod length xs) xs @ |
|
4574 take (length xs - n mod length xs) xs" |
|
4575 by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop) |
|
4576 |
|
4577 lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)" |
|
4578 unfolding rotater_def by auto |
|
4579 |
|
4580 lemma nth_rotater: |
|
4581 \<open>rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)\<close> if \<open>n < length xs\<close> |
|
4582 using that by (simp add: rotater_drop_take nth_append not_less less_diff_conv ac_simps le_mod_geq) |
|
4583 |
|
4584 lemma nth_rotater1: |
|
4585 \<open>rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)\<close> if \<open>n < length xs\<close> |
|
4586 using that nth_rotater [of n xs 1] by simp |
|
4587 |
|
4588 lemma rotate_inv_plus [rule_format]: |
|
4589 "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and> |
|
4590 rotate k (rotater n xs) = rotate m xs \<and> |
|
4591 rotater n (rotate k xs) = rotate m xs \<and> |
|
4592 rotate n (rotater k xs) = rotater m xs" |
|
4593 by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans]) |
|
4594 |
|
4595 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus] |
|
4596 |
|
4597 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified] |
|
4598 |
|
4599 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1] |
|
4600 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1] |
|
4601 |
|
4602 lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs" |
|
4603 by auto |
|
4604 |
|
4605 lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys" |
|
4606 by auto |
|
4607 |
|
4608 lemma length_rotater [simp]: "length (rotater n xs) = length xs" |
|
4609 by (simp add : rotater_rev) |
|
4610 |
|
4611 lemma bit_word_rotr_iff: |
|
4612 \<open>bit (word_rotr m w) n \<longleftrightarrow> |
|
4613 n < LENGTH('a) \<and> bit w ((n + m) mod LENGTH('a))\<close> |
|
4614 for w :: \<open>'a::len word\<close> |
|
4615 proof (cases \<open>n < LENGTH('a)\<close>) |
|
4616 case False |
|
4617 then show ?thesis |
|
4618 by (auto dest: bit_imp_le_length) |
|
4619 next |
|
4620 case True |
|
4621 define k where \<open>k = int n + int m\<close> |
|
4622 then have k: \<open>int n = k - int m\<close> |
|
4623 by simp |
|
4624 define l where \<open>l = int LENGTH('a)\<close> |
|
4625 then have l: \<open>int LENGTH('a) = l\<close> \<open>l > 0\<close> |
|
4626 by simp_all |
|
4627 have *: \<open>int (m - n) = int m - int n\<close> if \<open>n \<le> m\<close> for n m |
|
4628 using that by (simp add: int_minus) |
|
4629 have \<open>int ((LENGTH('a) |
|
4630 - Suc ((LENGTH('a) + LENGTH('a) - Suc (n + m mod LENGTH('a))) mod LENGTH('a)))) = |
|
4631 int ((n + m) mod LENGTH('a))\<close> |
|
4632 using True |
|
4633 apply (simp add: l * zmod_int Suc_leI add_strict_mono) |
|
4634 apply (subst mod_diff_left_eq [symmetric]) |
|
4635 apply simp |
|
4636 using l minus_mod_int_eq [of l \<open>int n + int m mod l + 1\<close>] apply simp |
|
4637 apply (simp add: mod_simps) |
|
4638 done |
|
4639 then have \<open>(LENGTH('a) |
|
4640 - Suc ((LENGTH('a) + LENGTH('a) - Suc (n + m mod LENGTH('a))) mod LENGTH('a))) = |
|
4641 ((n + m) mod LENGTH('a))\<close> |
|
4642 by simp |
|
4643 with True show ?thesis |
|
4644 by (simp add: word_rotr_def bit_of_bl_iff rev_nth nth_rotater nth_to_bl) |
|
4645 qed |
|
4646 |
|
4647 lemma bit_word_roti_iff: |
|
4648 \<open>bit (word_roti k w) n \<longleftrightarrow> |
|
4649 n < LENGTH('a) \<and> bit w (nat ((int n + k) mod int LENGTH('a)))\<close> |
|
4650 for w :: \<open>'a::len word\<close> |
|
4651 proof (cases \<open>k \<ge> 0\<close>) |
|
4652 case True |
|
4653 moreover define m where \<open>m = nat k\<close> |
|
4654 ultimately have \<open>k = int m\<close> |
|
4655 by simp |
|
4656 then show ?thesis |
|
4657 by (simp add: word_roti_def bit_word_rotr_iff nat_mod_distrib nat_add_distrib) |
|
4658 next |
|
4659 have *: \<open>int (m - n) = int m - int n\<close> if \<open>n \<le> m\<close> for n m |
|
4660 using that by (simp add: int_minus) |
|
4661 case False |
|
4662 moreover define m where \<open>m = nat (- k)\<close> |
|
4663 ultimately have \<open>k = - int m\<close> \<open>k < 0\<close> |
|
4664 by simp_all |
|
4665 moreover have \<open>(int n - int m) mod int LENGTH('a) = |
|
4666 int ((n + LENGTH('a) - m mod LENGTH('a)) mod LENGTH('a))\<close> |
|
4667 apply (simp add: zmod_int * trans_le_add2 mod_simps) |
|
4668 apply (metis mod_add_self2 mod_diff_cong) |
|
4669 done |
|
4670 ultimately show ?thesis |
|
4671 by (simp add: word_roti_def bit_word_rotl_iff nat_mod_distrib) |
|
4672 qed |
|
4673 |
|
4674 lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z" |
|
4675 by simp |
|
4676 |
|
4677 lemmas rrs0 = rotate_eqs [THEN restrict_to_left, |
|
4678 simplified rotate_gal [symmetric] rotate_gal' [symmetric]] |
|
4679 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]] |
|
4680 lemmas rotater_eqs = rrs1 [simplified length_rotater] |
|
4681 lemmas rotater_0 = rotater_eqs (1) |
|
4682 lemmas rotater_add = rotater_eqs (2) |
|
4683 |
|
4684 |
|
4685 subsubsection \<open>map, map2, commuting with rotate(r)\<close> |
|
4686 |
|
4687 lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)" |
|
4688 by (induct xs) auto |
|
4689 |
|
4690 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" |
|
4691 by (cases xs) (auto simp: rotater1_def last_map butlast_map) |
|
4692 |
|
4693 lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)" |
|
4694 by (induct n) (auto simp: rotater_def rotater1_map) |
|
4695 |
|
4696 lemma but_last_zip [rule_format] : |
|
4697 "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> |
|
4698 last (zip xs ys) = (last xs, last ys) \<and> |
|
4699 butlast (zip xs ys) = zip (butlast xs) (butlast ys)" |
|
4700 apply (induct xs) |
|
4701 apply auto |
|
4702 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+ |
|
4703 done |
|
4704 |
|
4705 lemma but_last_map2 [rule_format] : |
|
4706 "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> |
|
4707 last (map2 f xs ys) = f (last xs) (last ys) \<and> |
|
4708 butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" |
|
4709 apply (induct xs) |
|
4710 apply auto |
|
4711 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+ |
|
4712 done |
|
4713 |
|
4714 lemma rotater1_zip: |
|
4715 "length xs = length ys \<Longrightarrow> |
|
4716 rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" |
|
4717 apply (unfold rotater1_def) |
|
4718 apply (cases xs) |
|
4719 apply auto |
|
4720 apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+ |
|
4721 done |
|
4722 |
|
4723 lemma rotater1_map2: |
|
4724 "length xs = length ys \<Longrightarrow> |
|
4725 rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" |
|
4726 by (simp add: rotater1_map rotater1_zip) |
|
4727 |
|
4728 lemmas lrth = |
|
4729 box_equals [OF asm_rl length_rotater [symmetric] |
|
4730 length_rotater [symmetric], |
|
4731 THEN rotater1_map2] |
|
4732 |
|
4733 lemma rotater_map2: |
|
4734 "length xs = length ys \<Longrightarrow> |
|
4735 rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" |
|
4736 by (induct n) (auto intro!: lrth) |
|
4737 |
|
4738 lemma rotate1_map2: |
|
4739 "length xs = length ys \<Longrightarrow> |
|
4740 rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" |
|
4741 by (cases xs; cases ys) auto |
|
4742 |
|
4743 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] |
|
4744 length_rotate [symmetric], THEN rotate1_map2] |
|
4745 |
|
4746 lemma rotate_map2: |
|
4747 "length xs = length ys \<Longrightarrow> |
|
4748 rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" |
|
4749 by (induct n) (auto intro!: lth) |
|
4750 |
|
4751 |
|
4752 \<comment> \<open>corresponding equalities for word rotation\<close> |
|
4753 |
4875 |
4754 lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)" |
4876 lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)" |
4755 by (simp add: word_bl.Abs_inverse' word_rotl_def) |
4877 by (simp add: word_rotl_eq to_bl_use_of_bl) |
4756 |
4878 |
4757 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]] |
4879 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]] |
4758 |
4880 |
4759 lemmas word_rotl_eqs = |
4881 lemmas word_rotl_eqs = |
4760 blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]] |
4882 blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]] |
4761 |
4883 |
4762 lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)" |
4884 lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)" |
4763 by (simp add: word_bl.Abs_inverse' word_rotr_def) |
4885 by (simp add: word_rotr_eq to_bl_use_of_bl) |
4764 |
4886 |
4765 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]] |
4887 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]] |
4766 |
4888 |
4767 lemmas word_rotr_eqs = |
4889 lemmas word_rotr_eqs = |
4768 brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]] |
4890 brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]] |