# HG changeset patch
# User haftmann
# Date 1256907590 -3600
# Node ID 2ca60fc13c5a550cb62638b6e558662b53cf284a
# Parent  9157d0f9f00ec6dd2bba1200a5f03474dfc82d03
tuned proof

diff -r 9157d0f9f00e -r 2ca60fc13c5a src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Oct 30 13:59:49 2009 +0100
+++ b/src/HOL/Library/Word.thy	Fri Oct 30 13:59:50 2009 +0100
@@ -5,7 +5,7 @@
 header {* Binary Words *}
 
 theory Word
-imports "~~/src/HOL/Main"
+imports Main
 begin
 
 subsection {* Auxilary Lemmas *}
@@ -561,35 +561,17 @@
   shows        "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])"
 proof (cases x)
   assume [simp]: "x = \<one>"
-  show ?thesis
-    apply (simp add: nat_to_bv_non0)
-    apply safe
-  proof -
-    fix q
-    assume "Suc (2 * bv_to_nat w) = 2 * q"
-    hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs")
-      by simp
-    have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
-      by (simp add: add_commute)
-    also have "... = 1"
-      by (subst mod_add_eq) simp
-    finally have eq1: "?lhs = 1" .
-    have "?rhs  = 0" by simp
-    with orig and eq1
-    show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
-      by simp
-  next
-    have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] =
-        nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
-      by (simp add: add_commute)
-    also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
-      by (subst div_add1_eq) simp
-    also have "... = norm_unsigned w @ [\<one>]"
-      by (subst ass) (rule refl)
-    also have "... = norm_unsigned (w @ [\<one>])"
-      by (cases "norm_unsigned w") simp_all
-    finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" .
-  qed
+  have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] =
+      nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
+    by (simp add: add_commute)
+  also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
+    by (subst div_add1_eq) simp
+  also have "... = norm_unsigned w @ [\<one>]"
+    by (subst ass) (rule refl)
+  also have "... = norm_unsigned (w @ [\<one>])"
+    by (cases "norm_unsigned w") simp_all
+  finally have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" .
+  then show ?thesis by (simp add: nat_to_bv_non0)
 next
   assume [simp]: "x = \<zero>"
   show ?thesis