629 |
629 |
630 lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b + |
630 lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b + |
631 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) - |
631 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) - |
632 2 ^ (len_of TYPE('a) - 1)" |
632 2 ^ (len_of TYPE('a) - 1)" |
633 unfolding word_number_of_alt by (rule int_word_sint) |
633 unfolding word_number_of_alt by (rule int_word_sint) |
|
634 |
|
635 lemma word_of_int_0: "word_of_int 0 = 0" |
|
636 unfolding word_0_wi .. |
|
637 |
|
638 lemma word_of_int_1: "word_of_int 1 = 1" |
|
639 unfolding word_1_wi .. |
634 |
640 |
635 lemma word_of_int_bin [simp] : |
641 lemma word_of_int_bin [simp] : |
636 "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)" |
642 "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)" |
637 unfolding word_number_of_alt by auto |
643 unfolding word_number_of_alt by auto |
638 |
644 |
1094 note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1 |
1100 note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1 |
1095 are in the default simpset, so to use the automatic simplifications for |
1101 are in the default simpset, so to use the automatic simplifications for |
1096 (eg) sint (number_of bin) on sint 1, must do |
1102 (eg) sint (number_of bin) on sint 1, must do |
1097 (simp add: word_1_no del: numeral_1_eq_1) |
1103 (simp add: word_1_no del: numeral_1_eq_1) |
1098 *) |
1104 *) |
1099 lemmas word_0_wi_Pls = word_0_wi [folded Pls_def] |
1105 lemma word_0_wi_Pls: "0 = word_of_int Int.Pls" |
1100 lemmas word_0_no = word_0_wi_Pls [folded word_no_wi] |
1106 by (simp only: Pls_def word_0_wi) |
|
1107 |
|
1108 lemma word_0_no: "(0::'a::len0 word) = Numeral0" |
|
1109 by (simp add: word_number_of_alt word_0_wi) |
1101 |
1110 |
1102 lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)" |
1111 lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)" |
1103 unfolding Pls_def Bit_def by auto |
1112 unfolding Pls_def Bit_def by auto |
1104 |
1113 |
1105 lemma word_1_no: |
1114 lemma word_1_no: |
1155 lemmas unat_eq_zero = unat_0_iff |
1164 lemmas unat_eq_zero = unat_0_iff |
1156 |
1165 |
1157 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)" |
1166 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)" |
1158 by (auto simp: unat_0_iff [symmetric]) |
1167 by (auto simp: unat_0_iff [symmetric]) |
1159 |
1168 |
1160 lemma ucast_0 [simp] : "ucast 0 = 0" |
1169 lemma ucast_0 [simp]: "ucast 0 = 0" |
1161 unfolding ucast_def |
1170 unfolding ucast_def by (simp add: word_of_int_0) |
1162 by simp (simp add: word_0_wi) |
1171 |
1163 |
1172 lemma sint_0 [simp]: "sint 0 = 0" |
1164 lemma sint_0 [simp] : "sint 0 = 0" |
1173 unfolding sint_uint by simp |
1165 unfolding sint_uint |
1174 |
1166 by (simp add: Pls_def [symmetric]) |
1175 lemma scast_0 [simp]: "scast 0 = 0" |
1167 |
1176 unfolding scast_def by (simp add: word_of_int_0) |
1168 lemma scast_0 [simp] : "scast 0 = 0" |
|
1169 apply (unfold scast_def) |
|
1170 apply simp |
|
1171 apply (simp add: word_0_wi) |
|
1172 done |
|
1173 |
1177 |
1174 lemma sint_n1 [simp] : "sint -1 = -1" |
1178 lemma sint_n1 [simp] : "sint -1 = -1" |
1175 apply (unfold word_m1_wi_Min) |
1179 unfolding word_m1_wi by (simp add: word_sbin.eq_norm) |
1176 apply (simp add: word_sbin.eq_norm) |
1180 |
1177 apply (unfold Min_def number_of_eq) |
1181 lemma scast_n1 [simp]: "scast -1 = -1" |
1178 apply simp |
1182 unfolding scast_def by simp |
1179 done |
1183 |
1180 |
1184 lemma uint_1 [simp]: "uint (1::'a::len word) = 1" |
1181 lemma scast_n1 [simp] : "scast -1 = -1" |
|
1182 apply (unfold scast_def sint_n1) |
|
1183 apply (unfold word_number_of_alt) |
|
1184 apply (rule refl) |
|
1185 done |
|
1186 |
|
1187 lemma uint_1 [simp] : "uint (1 :: 'a :: len word) = 1" |
|
1188 unfolding word_1_wi |
1185 unfolding word_1_wi |
1189 by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) |
1186 by (simp add: word_ubin.eq_norm bintrunc_minus_simps) |
1190 |
1187 |
1191 lemma unat_1 [simp] : "unat (1 :: 'a :: len word) = 1" |
1188 lemma unat_1 [simp]: "unat (1::'a::len word) = 1" |
1192 by (unfold unat_def uint_1) auto |
1189 unfolding unat_def by simp |
1193 |
1190 |
1194 lemma ucast_1 [simp] : "ucast (1 :: 'a :: len word) = 1" |
1191 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" |
1195 unfolding ucast_def word_1_wi |
1192 unfolding ucast_def by (simp add: word_of_int_1) |
1196 by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) |
|
1197 |
1193 |
1198 (* now, to get the weaker results analogous to word_div/mod_def *) |
1194 (* now, to get the weaker results analogous to word_div/mod_def *) |
1199 |
1195 |
1200 lemmas word_arith_alts = |
1196 lemmas word_arith_alts = |
1201 word_sub_wi [unfolded succ_def pred_def] |
1197 word_sub_wi [unfolded succ_def pred_def] |