equal
deleted
inserted
replaced
43 unfolding bin_last_def Bit_def |
43 unfolding bin_last_def Bit_def |
44 by (cases b, simp_all add: z1pmod2) |
44 by (cases b, simp_all add: z1pmod2) |
45 |
45 |
46 lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c" |
46 lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c" |
47 by (metis bin_rest_BIT bin_last_BIT) |
47 by (metis bin_rest_BIT bin_last_BIT) |
|
48 |
|
49 lemma BIT_bin_simps [simp]: |
|
50 "number_of w BIT 0 = number_of (Int.Bit0 w)" |
|
51 "number_of w BIT 1 = number_of (Int.Bit1 w)" |
|
52 unfolding Bit_def number_of_is_id numeral_simps by simp_all |
|
53 |
|
54 lemma BIT_special_simps [simp]: |
|
55 shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3" |
|
56 unfolding Bit_def by simp_all |
48 |
57 |
49 lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w" |
58 lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w" |
50 unfolding Bit_def Bit0_def by simp |
59 unfolding Bit_def Bit0_def by simp |
51 |
60 |
52 lemma BIT_B1_eq_Bit1: "w BIT 1 = Int.Bit1 w" |
61 lemma BIT_B1_eq_Bit1: "w BIT 1 = Int.Bit1 w" |