equal
deleted
inserted
replaced
267 lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]] |
267 lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]] |
268 |
268 |
269 lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)" |
269 lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)" |
270 by (auto intro!: bin_nth_lem del: equalityI) |
270 by (auto intro!: bin_nth_lem del: equalityI) |
271 |
271 |
|
272 lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n" |
|
273 by (induct n) auto |
|
274 |
272 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" |
275 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" |
273 by (induct n) auto |
276 by (induct n) auto |
274 |
277 |
275 lemma bin_nth_Min [simp]: "bin_nth Int.Min n" |
278 lemma bin_nth_Min [simp]: "bin_nth Int.Min n" |
276 by (induct n) auto |
279 by (induct n) auto |