equal
deleted
inserted
replaced
297 \<^simproc>\<open>natle_cancel_numerals\<close>, |
297 \<^simproc>\<open>natle_cancel_numerals\<close>, |
298 \<^simproc>\<open>natdiff_cancel_numerals\<close>, |
298 \<^simproc>\<open>natdiff_cancel_numerals\<close>, |
299 Numeral_Simprocs.field_divide_cancel_numeral_factor]) |
299 Numeral_Simprocs.field_divide_cancel_numeral_factor]) |
300 \<close> |
300 \<close> |
301 |
301 |
|
302 lemma bit_numeral_int_simps [simp]: |
|
303 \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close> |
|
304 \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close> |
|
305 \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close> |
|
306 \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close> |
|
307 \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close> |
|
308 \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close> |
|
309 \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close> |
|
310 by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff) |
|
311 |
302 end |
312 end |