src/HOL/ex/Word_Type.thy
changeset 66815 93c6632ddf44
parent 66806 a4e82b58d833
child 67816 2249b27ab1dd
     1.1 --- a/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  subsection \<open>Truncating bit representations of numeric types\<close>
     1.6  
     1.7 -class semiring_bits = unique_euclidean_semiring_parity +
     1.8 +class semiring_bits = semiring_parity +
     1.9    assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
    1.10  begin
    1.11  
    1.12 @@ -27,28 +27,16 @@
    1.13    by (simp add: bitrunc_eq_mod)
    1.14  
    1.15  lemma bitrunc_Suc [simp]:
    1.16 -  "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + a mod 2"
    1.17 +  "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + of_bool (odd a)"
    1.18  proof -
    1.19 -  define b and c
    1.20 -    where "b = a div 2" and "c = a mod 2"
    1.21 -  then have a: "a = b * 2 + c" 
    1.22 -    and "c = 0 \<or> c = 1"
    1.23 -    by (simp_all add: div_mult_mod_eq parity)
    1.24 -  from \<open>c = 0 \<or> c = 1\<close>
    1.25 -  have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
    1.26 -  proof
    1.27 -    assume "c = 0"
    1.28 -    moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)"
    1.29 -      by (simp add: mod_mult_mult1)
    1.30 -    ultimately show ?thesis
    1.31 -      by (simp add: bitrunc_eq_mod ac_simps)
    1.32 -  next
    1.33 -    assume "c = 1"
    1.34 -    with semiring_bits [of b "2 ^ n"] show ?thesis
    1.35 -      by (simp add: bitrunc_eq_mod ac_simps)
    1.36 -  qed
    1.37 -  with a show ?thesis
    1.38 -    by (simp add: b_def c_def)
    1.39 +  have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
    1.40 +    if "odd a"
    1.41 +    using that semiring_bits [of "a div 2" "2 ^ n"]
    1.42 +      by (simp add: algebra_simps odd_iff_mod_2_eq_one mult_mod_right)
    1.43 +  also have "\<dots> = a mod (2 * 2 ^ n)"
    1.44 +    by (simp only: div_mult_mod_eq)
    1.45 +  finally show ?thesis
    1.46 +    by (simp add: bitrunc_eq_mod algebra_simps mult_mod_right)
    1.47  qed
    1.48  
    1.49  lemma bitrunc_of_0 [simp]:
    1.50 @@ -57,11 +45,11 @@
    1.51  
    1.52  lemma bitrunc_plus:
    1.53    "bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
    1.54 -  by (simp add: bitrunc_eq_mod mod_add_eq)
    1.55 +  by (simp add: bitrunc_eq_mod mod_simps)
    1.56  
    1.57  lemma bitrunc_of_1_eq_0_iff [simp]:
    1.58    "bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
    1.59 -  by (induct n) simp_all
    1.60 +  by (simp add: bitrunc_eq_mod)
    1.61  
    1.62  end
    1.63  
    1.64 @@ -113,7 +101,7 @@
    1.65  
    1.66  lemma signed_bitrunc_Suc [simp]:
    1.67    "signed_bitrunc (Suc n) k = signed_bitrunc n (k div 2) * 2 + k mod 2"
    1.68 -  using zero_not_eq_two by (simp add: signed_bitrunc_eq_bitrunc algebra_simps)
    1.69 +  by (simp add: odd_iff_mod_2_eq_one signed_bitrunc_eq_bitrunc algebra_simps)
    1.70  
    1.71  lemma signed_bitrunc_of_0 [simp]:
    1.72    "signed_bitrunc n 0 = 0"