src/HOL/Word/Bit_Representation.thy
changeset 45952 ed9cc0634aaf
parent 45856 caa99836aed8
child 45953 1d6fcb19aa50
equal deleted inserted replaced
45951:e49e45fee615 45952:ed9cc0634aaf
   273   by (induct n) auto
   273   by (induct n) auto
   274 
   274 
   275 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
   275 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
   276   by (induct n) auto
   276   by (induct n) auto
   277 
   277 
       
   278 lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
       
   279   by (induct n) auto
       
   280 
   278 lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
   281 lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
   279   by (induct n) auto
   282   by (induct n) auto
   280 
   283 
   281 lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))"
   284 lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))"
   282   by auto
   285   by auto