tuned
authorhaftmann
Tue Apr 16 19:50:07 2019 +0000 (7 days ago)
changeset 701713173d7878274
parent 70170 56727602d0a5
child 70172 c247bf924d25
tuned
src/HOL/ex/Word_Type.thy
     1.1 --- a/src/HOL/ex/Word_Type.thy	Tue Apr 16 19:50:05 2019 +0000
     1.2 +++ b/src/HOL/ex/Word_Type.thy	Tue Apr 16 19:50:07 2019 +0000
     1.3 @@ -10,18 +10,15 @@
     1.4  begin
     1.5  
     1.6  lemma take_bit_uminus:
     1.7 -  fixes k :: int
     1.8 -  shows "take_bit n (- (take_bit n k)) = take_bit n (- k)"
     1.9 +  "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int
    1.10    by (simp add: take_bit_eq_mod mod_minus_eq)
    1.11  
    1.12  lemma take_bit_minus:
    1.13 -  fixes k l :: int
    1.14 -  shows "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
    1.15 +  "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" for k l :: int
    1.16    by (simp add: take_bit_eq_mod mod_diff_eq)
    1.17  
    1.18  lemma take_bit_nonnegative [simp]:
    1.19 -  fixes k :: int
    1.20 -  shows "take_bit n k \<ge> 0"
    1.21 +  "take_bit n k \<ge> 0" for k :: int
    1.22    by (simp add: take_bit_eq_mod)
    1.23  
    1.24  definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
    1.25 @@ -29,9 +26,8 @@
    1.26      "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
    1.27  
    1.28  lemma signed_take_bit_eq_take_bit':
    1.29 -  assumes "n > 0"
    1.30 -  shows "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
    1.31 -  using assms by (simp add: signed_take_bit_eq_take_bit)
    1.32 +  "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)" if "n > 0"
    1.33 +  using that by (simp add: signed_take_bit_eq_take_bit)
    1.34    
    1.35  lemma signed_take_bit_0 [simp]:
    1.36    "signed_take_bit 0 k = - (k mod 2)"
    1.37 @@ -62,10 +58,10 @@
    1.38    by (induct n) simp_all
    1.39  
    1.40  lemma signed_take_bit_eq_iff_take_bit_eq:
    1.41 -  assumes "n > 0"
    1.42 -  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")
    1.43 +  "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")
    1.44 +  if "n > 0"
    1.45  proof -
    1.46 -  from assms obtain m where m: "n = Suc m"
    1.47 +  from that obtain m where m: "n = Suc m"
    1.48      by (cases n) auto
    1.49    show ?thesis
    1.50    proof 
    1.51 @@ -82,7 +78,7 @@
    1.52        by (simp only: signed_take_bit_eq_take_bit m) simp
    1.53    next
    1.54      assume ?P
    1.55 -    with assms have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
    1.56 +    with that have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
    1.57        by (simp add: signed_take_bit_eq_take_bit' take_bit_eq_mod)
    1.58      then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
    1.59        by (metis mod_add_eq)