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.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.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"
```