# HG changeset patch
# User huffman
# Date 1187907831 -7200
# Node ID 7e42e986b1a11a3086d7b60ee89365cfef884ee6
# Parent  5c3858b71f802c0831ccc85e4dbca9484662ea23
bin_sc_nth proof

diff -r 5c3858b71f80 -r 7e42e986b1a1 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Thu Aug 23 23:37:51 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy	Fri Aug 24 00:23:51 2007 +0200
@@ -361,10 +361,13 @@
 lemma bin_nth_sc_gen: 
   "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = bit.B1 else bin_nth w m)"
   by (induct n) (case_tac [!] m, auto)
+
+lemma bit_bool1: "(if s = bit.B1 then bit.B1 else bit.B0) = s"
+  by auto
   
 lemma bin_sc_nth [simp]:
   "!!w. (bin_sc n (If (bin_nth w n) bit.B1 bit.B0) w) = w"
-  by (induct n) auto
+  by (induct n) (auto simp add: bit_bool1)
 
 lemma bin_sign_sc [simp]:
   "!!w. bin_sign (bin_sc n b w) = bin_sign w"