# HG changeset patch # User huffman # Date 1323781322 -3600 # Node ID cbb6f2243b52c05a6c5555debdce2213b356ea43 # Parent 24f563d9449775e69423029a1f98def79a4bdaf6 add lemma bin_nth_zero diff -r 24f563d94497 -r cbb6f2243b52 src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Tue Dec 13 19:21:36 2011 +0100 +++ b/src/HOL/Word/Bit_Representation.thy Tue Dec 13 14:02:02 2011 +0100 @@ -269,6 +269,9 @@ lemma bin_eq_iff: "x = y \ (\n. bin_nth x n = bin_nth y n)" by (auto intro!: bin_nth_lem del: equalityI) +lemma bin_nth_zero [simp]: "\ bin_nth 0 n" + by (induct n) auto + lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" by (induct n) auto