# HG changeset patch
# User haftmann
# Date 1555444207 0
# Node ID 3173d787827455bc6c1eed8b541743e7baec5e82
# Parent  56727602d0a5e7989066f37a80de69bc9975b7a0
tuned

diff -r 56727602d0a5 -r 3173d7878274 src/HOL/ex/Word_Type.thy
--- a/src/HOL/ex/Word_Type.thy	Tue Apr 16 19:50:05 2019 +0000
+++ b/src/HOL/ex/Word_Type.thy	Tue Apr 16 19:50:07 2019 +0000
@@ -10,18 +10,15 @@
 begin
 
 lemma take_bit_uminus:
-  fixes k :: int
-  shows "take_bit n (- (take_bit n k)) = take_bit n (- k)"
+  "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int
   by (simp add: take_bit_eq_mod mod_minus_eq)
 
 lemma take_bit_minus:
-  fixes k l :: int
-  shows "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
+  "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" for k l :: int
   by (simp add: take_bit_eq_mod mod_diff_eq)
 
 lemma take_bit_nonnegative [simp]:
-  fixes k :: int
-  shows "take_bit n k \<ge> 0"
+  "take_bit n k \<ge> 0" for k :: int
   by (simp add: take_bit_eq_mod)
 
 definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
@@ -29,9 +26,8 @@
     "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
 
 lemma signed_take_bit_eq_take_bit':
-  assumes "n > 0"
-  shows "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
-  using assms by (simp add: signed_take_bit_eq_take_bit)
+  "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)" if "n > 0"
+  using that by (simp add: signed_take_bit_eq_take_bit)
   
 lemma signed_take_bit_0 [simp]:
   "signed_take_bit 0 k = - (k mod 2)"
@@ -62,10 +58,10 @@
   by (induct n) simp_all
 
 lemma signed_take_bit_eq_iff_take_bit_eq:
-  assumes "n > 0"
-  shows "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \<longleftrightarrow> take_bit n k = take_bit n l" (is "?P \<longleftrightarrow> ?Q")
+  "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \<longleftrightarrow> take_bit n k = take_bit n l" (is "?P \<longleftrightarrow> ?Q")
+  if "n > 0"
 proof -
-  from assms obtain m where m: "n = Suc m"
+  from that obtain m where m: "n = Suc m"
     by (cases n) auto
   show ?thesis
   proof 
@@ -82,7 +78,7 @@
       by (simp only: signed_take_bit_eq_take_bit m) simp
   next
     assume ?P
-    with assms have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
+    with that have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
       by (simp add: signed_take_bit_eq_take_bit' take_bit_eq_mod)
     then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
       by (metis mod_add_eq)