one uniform type class for parity structures
authorhaftmann
Sun Oct 08 22:28:22 2017 +0200 (19 months ago)
changeset 6681593c6632ddf44
parent 66814 a24cde9588bb
child 66816 212a3334e7da
one uniform type class for parity structures
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/NthRoot.thy
src/HOL/Parity.thy
src/HOL/ex/Word_Type.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -282,6 +282,9 @@
     1.4    "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
     1.5    by (simp add: integer_eq_iff)
     1.6  
     1.7 +instance integer :: ring_parity
     1.8 +  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
     1.9 +
    1.10  instantiation integer :: unique_euclidean_semiring_numeral
    1.11  begin
    1.12  
    1.13 @@ -927,6 +930,9 @@
    1.14    "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
    1.15    by (simp add: fun_eq_iff)
    1.16  
    1.17 +instance natural :: semiring_parity
    1.18 +  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
    1.19 +
    1.20  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
    1.21    is "nat :: int \<Rightarrow> nat"
    1.22    .
     2.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     2.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  section \<open>More on quotient and remainder\<close>
     2.5  
     2.6  theory Divides
     2.7 -imports Parity
     2.8 +imports Parity Nat_Transfer
     2.9  begin
    2.10  
    2.11  subsection \<open>Numeral division with a pragmatic type class\<close>
    2.12 @@ -19,7 +19,7 @@
    2.13    and less technical class hierarchy.
    2.14  \<close>
    2.15  
    2.16 -class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
    2.17 +class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
    2.18    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    2.19      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    2.20      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
    2.21 @@ -40,29 +40,6 @@
    2.22      yields a significant speedup.\<close>
    2.23  begin
    2.24  
    2.25 -subclass unique_euclidean_semiring_parity
    2.26 -proof
    2.27 -  fix a
    2.28 -  show "a mod 2 = 0 \<or> a mod 2 = 1"
    2.29 -  proof (rule ccontr)
    2.30 -    assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
    2.31 -    then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
    2.32 -    have "0 < 2" by simp
    2.33 -    with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
    2.34 -    with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
    2.35 -    with discrete have "1 \<le> a mod 2" by simp
    2.36 -    with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
    2.37 -    with discrete have "2 \<le> a mod 2" by simp
    2.38 -    with \<open>a mod 2 < 2\<close> show False by simp
    2.39 -  qed
    2.40 -next
    2.41 -  show "1 mod 2 = 1"
    2.42 -    by (rule mod_less) simp_all
    2.43 -next
    2.44 -  show "0 \<noteq> 2"
    2.45 -    by simp
    2.46 -qed
    2.47 -
    2.48  lemma divmod_digit_1:
    2.49    assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
    2.50    shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
    2.51 @@ -74,7 +51,7 @@
    2.52    then have [simp]: "1 \<le> a div b" by (simp add: discrete)
    2.53    with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
    2.54    define w where "w = a div b mod 2"
    2.55 -  with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
    2.56 +  then have w_exhaust: "w = 0 \<or> w = 1" by auto
    2.57    have mod_w: "a mod (2 * b) = a mod b + b * w"
    2.58      by (simp add: w_def mod_mult2_eq ac_simps)
    2.59    from assms w_exhaust have "w = 1"
    2.60 @@ -93,7 +70,7 @@
    2.61      and "a mod (2 * b) = a mod b" (is "?Q")
    2.62  proof -
    2.63    define w where "w = a div b mod 2"
    2.64 -  with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
    2.65 +  then have w_exhaust: "w = 0 \<or> w = 1" by auto
    2.66    have mod_w: "a mod (2 * b) = a mod b + b * w"
    2.67      by (simp add: w_def mod_mult2_eq ac_simps)
    2.68    moreover have "b \<le> a mod b + b"
    2.69 @@ -318,60 +295,6 @@
    2.70  
    2.71  declare divmod_algorithm_code [where ?'a = nat, code]
    2.72  
    2.73 -lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
    2.74 -  by (auto elim: oddE)
    2.75 -
    2.76 -lemma even_Suc_div_two [simp]:
    2.77 -  "even n \<Longrightarrow> Suc n div 2 = n div 2"
    2.78 -  using even_succ_div_two [of n] by simp
    2.79 -
    2.80 -lemma odd_Suc_div_two [simp]:
    2.81 -  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
    2.82 -  using odd_succ_div_two [of n] by simp
    2.83 -
    2.84 -lemma odd_two_times_div_two_nat [simp]:
    2.85 -  assumes "odd n"
    2.86 -  shows "2 * (n div 2) = n - (1 :: nat)"
    2.87 -proof -
    2.88 -  from assms have "2 * (n div 2) + 1 = n"
    2.89 -    by (rule odd_two_times_div_two_succ)
    2.90 -  then have "Suc (2 * (n div 2)) - 1 = n - 1"
    2.91 -    by simp
    2.92 -  then show ?thesis
    2.93 -    by simp
    2.94 -qed
    2.95 -
    2.96 -lemma parity_induct [case_names zero even odd]:
    2.97 -  assumes zero: "P 0"
    2.98 -  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
    2.99 -  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
   2.100 -  shows "P n"
   2.101 -proof (induct n rule: less_induct)
   2.102 -  case (less n)
   2.103 -  show "P n"
   2.104 -  proof (cases "n = 0")
   2.105 -    case True with zero show ?thesis by simp
   2.106 -  next
   2.107 -    case False
   2.108 -    with less have hyp: "P (n div 2)" by simp
   2.109 -    show ?thesis
   2.110 -    proof (cases "even n")
   2.111 -      case True
   2.112 -      with hyp even [of "n div 2"] show ?thesis
   2.113 -        by simp
   2.114 -    next
   2.115 -      case False
   2.116 -      with hyp odd [of "n div 2"] show ?thesis
   2.117 -        by simp
   2.118 -    qed
   2.119 -  qed
   2.120 -qed
   2.121 -
   2.122 -lemma mod_2_not_eq_zero_eq_one_nat:
   2.123 -  fixes n :: nat
   2.124 -  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   2.125 -  by (fact not_mod_2_eq_0_eq_1)
   2.126 -
   2.127  lemma Suc_0_div_numeral [simp]:
   2.128    fixes k l :: num
   2.129    shows "Suc 0 div numeral k = fst (divmod Num.One k)"
   2.130 @@ -708,6 +631,39 @@
   2.131  
   2.132  text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
   2.133  
   2.134 +instance int :: ring_parity
   2.135 +proof
   2.136 +  fix k l :: int
   2.137 +  show "k mod 2 = 1" if "\<not> 2 dvd k"
   2.138 +  proof (rule order_antisym)
   2.139 +    have "0 \<le> k mod 2" and "k mod 2 < 2"
   2.140 +      by auto
   2.141 +    moreover have "k mod 2 \<noteq> 0"
   2.142 +      using that by (simp add: dvd_eq_mod_eq_0)
   2.143 +    ultimately have "0 < k mod 2"
   2.144 +      by (simp only: less_le) simp
   2.145 +    then show "1 \<le> k mod 2"
   2.146 +      by simp
   2.147 +    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
   2.148 +      by (simp only: less_le) simp
   2.149 +  qed
   2.150 +qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
   2.151 +
   2.152 +lemma even_diff_iff [simp]:
   2.153 +  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
   2.154 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   2.155 +
   2.156 +lemma even_abs_add_iff [simp]:
   2.157 +  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
   2.158 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
   2.159 +
   2.160 +lemma even_add_abs_iff [simp]:
   2.161 +  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
   2.162 +  using even_abs_add_iff [of l k] by (simp add: ac_simps)
   2.163 +
   2.164 +lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   2.165 +  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
   2.166 +
   2.167  
   2.168  subsubsection \<open>Laws for div and mod with Unary Minus\<close>
   2.169  
   2.170 @@ -1495,4 +1451,18 @@
   2.171    then show ?thesis ..
   2.172  qed
   2.173  
   2.174 +lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
   2.175 +
   2.176 +lemma mod_2_not_eq_zero_eq_one_nat:
   2.177 +  fixes n :: nat
   2.178 +  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   2.179 +  by (fact not_mod_2_eq_0_eq_1)
   2.180 +
   2.181 +lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
   2.182 +  by (fact even_of_nat)
   2.183 +
   2.184 +text \<open>Tool setup\<close>
   2.185 +
   2.186 +declare transfer_morphism_int_nat [transfer add return: even_int_iff]
   2.187 +
   2.188  end
     3.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:22 2017 +0200
     3.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:22 2017 +0200
     3.3 @@ -834,6 +834,10 @@
     3.4  
     3.5  end
     3.6  
     3.7 +instance star :: (semidom_modulo) semidom_modulo
     3.8 +  by standard (transfer; simp)
     3.9 +
    3.10 +
    3.11  
    3.12  subsection \<open>Power\<close>
    3.13  
    3.14 @@ -917,14 +921,6 @@
    3.15  
    3.16  instance star :: (ring_char_0) ring_char_0 ..
    3.17  
    3.18 -instance star :: (semiring_parity) semiring_parity
    3.19 -  apply intro_classes
    3.20 -     apply (transfer, rule odd_one)
    3.21 -    apply (transfer, erule (1) odd_even_add)
    3.22 -   apply (transfer, erule even_multD)
    3.23 -  apply (transfer, erule odd_ex_decrement)
    3.24 -  done
    3.25 -
    3.26  
    3.27  subsection \<open>Finite class\<close>
    3.28  
     4.1 --- a/src/HOL/NthRoot.thy	Sun Oct 08 22:28:22 2017 +0200
     4.2 +++ b/src/HOL/NthRoot.thy	Sun Oct 08 22:28:22 2017 +0200
     4.3 @@ -218,7 +218,7 @@
     4.4  
     4.5  lemma real_root_inverse: "root n (inverse x) = inverse (root n x)"
     4.6    by (auto split: split_root elim!: sgn_power_injE
     4.7 -      simp: inverse_sgn power_inverse)
     4.8 +      simp: power_inverse)
     4.9  
    4.10  lemma real_root_divide: "root n (x / y) = root n x / root n y"
    4.11    by (simp add: divide_inverse real_root_mult real_root_inverse)
    4.12 @@ -715,7 +715,7 @@
    4.13      have "x n \<le> sqrt (2 / real n)" if "2 < n" for n :: nat
    4.14      proof -
    4.15        have "1 + (real (n - 1) * n) / 2 * (x n)\<^sup>2 = 1 + of_nat (n choose 2) * (x n)\<^sup>2"
    4.16 -        by (auto simp add: choose_two of_nat_div mod_eq_0_iff_dvd)
    4.17 +        by (auto simp add: choose_two field_char_0_class.of_nat_div mod_eq_0_iff_dvd)
    4.18        also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
    4.19          by (simp add: x_def)
    4.20        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
     5.1 --- a/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
     5.2 +++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
     5.3 @@ -6,19 +6,73 @@
     5.4  section \<open>Parity in rings and semirings\<close>
     5.5  
     5.6  theory Parity
     5.7 -  imports Nat_Transfer Euclidean_Division
     5.8 +  imports Euclidean_Division
     5.9  begin
    5.10  
    5.11  subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
    5.12  
    5.13 -class semiring_parity = comm_semiring_1_cancel + numeral +
    5.14 -  assumes odd_one [simp]: "\<not> 2 dvd 1"
    5.15 -  assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
    5.16 -  assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
    5.17 -  assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
    5.18 +class semiring_parity = linordered_semidom + unique_euclidean_semiring +
    5.19 +  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
    5.20 +    and odd_imp_mod_2_eq_1: "\<not> 2 dvd a \<Longrightarrow> a mod 2 = 1"
    5.21 +
    5.22 +context semiring_parity
    5.23  begin
    5.24  
    5.25 -subclass semiring_numeral ..
    5.26 +lemma of_nat_dvd_iff:
    5.27 +  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
    5.28 +proof (cases "m = 0")
    5.29 +  case True
    5.30 +  then show ?thesis
    5.31 +    by simp
    5.32 +next
    5.33 +  case False
    5.34 +  show ?thesis
    5.35 +  proof
    5.36 +    assume ?Q
    5.37 +    then show ?P
    5.38 +      by (auto elim: dvd_class.dvdE)
    5.39 +  next
    5.40 +    assume ?P
    5.41 +    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
    5.42 +      by simp
    5.43 +    then have "of_nat n = of_nat (n div m * m)"
    5.44 +      by (simp add: of_nat_div)
    5.45 +    then have "n = n div m * m"
    5.46 +      by (simp only: of_nat_eq_iff)
    5.47 +    then have "n = m * (n div m)"
    5.48 +      by (simp add: ac_simps)
    5.49 +    then show ?Q ..
    5.50 +  qed
    5.51 +qed
    5.52 +
    5.53 +lemma of_nat_mod:
    5.54 +  "of_nat (m mod n) = of_nat m mod of_nat n"
    5.55 +proof -
    5.56 +  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
    5.57 +    by (simp add: div_mult_mod_eq)
    5.58 +  also have "of_nat m = of_nat (m div n * n + m mod n)"
    5.59 +    by simp
    5.60 +  finally show ?thesis
    5.61 +    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
    5.62 +qed
    5.63 +
    5.64 +lemma one_div_two_eq_zero [simp]:
    5.65 +  "1 div 2 = 0"
    5.66 +proof -
    5.67 +  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
    5.68 +    by (simp only:) simp
    5.69 +  then show ?thesis
    5.70 +    by simp
    5.71 +qed
    5.72 +
    5.73 +lemma one_mod_two_eq_one [simp]:
    5.74 +  "1 mod 2 = 1"
    5.75 +proof -
    5.76 +  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
    5.77 +    by (simp only:) simp
    5.78 +  then show ?thesis
    5.79 +    by simp
    5.80 +qed
    5.81  
    5.82  abbreviation even :: "'a \<Rightarrow> bool"
    5.83    where "even a \<equiv> 2 dvd a"
    5.84 @@ -26,11 +80,27 @@
    5.85  abbreviation odd :: "'a \<Rightarrow> bool"
    5.86    where "odd a \<equiv> \<not> 2 dvd a"
    5.87  
    5.88 -lemma even_zero [simp]: "even 0"
    5.89 -  by (fact dvd_0_right)
    5.90 +lemma even_iff_mod_2_eq_zero:
    5.91 +  "even a \<longleftrightarrow> a mod 2 = 0"
    5.92 +  by (fact dvd_eq_mod_eq_0)
    5.93 +
    5.94 +lemma odd_iff_mod_2_eq_one:
    5.95 +  "odd a \<longleftrightarrow> a mod 2 = 1"
    5.96 +  by (auto dest: odd_imp_mod_2_eq_1)
    5.97  
    5.98 -lemma even_plus_one_iff [simp]: "even (a + 1) \<longleftrightarrow> odd a"
    5.99 -  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
   5.100 +lemma parity_cases [case_names even odd]:
   5.101 +  assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
   5.102 +  assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
   5.103 +  shows P
   5.104 +  using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
   5.105 +
   5.106 +lemma not_mod_2_eq_1_eq_0 [simp]:
   5.107 +  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
   5.108 +  by (cases a rule: parity_cases) simp_all
   5.109 +
   5.110 +lemma not_mod_2_eq_0_eq_1 [simp]:
   5.111 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
   5.112 +  by (cases a rule: parity_cases) simp_all
   5.113  
   5.114  lemma evenE [elim?]:
   5.115    assumes "even a"
   5.116 @@ -41,22 +111,107 @@
   5.117    assumes "odd a"
   5.118    obtains b where "a = 2 * b + 1"
   5.119  proof -
   5.120 -  from assms obtain b where *: "a = b + 1"
   5.121 -    by (blast dest: odd_ex_decrement)
   5.122 -  with assms have "even (b + 2)" by simp
   5.123 -  then have "even b" by simp
   5.124 -  then obtain c where "b = 2 * c" ..
   5.125 -  with * have "a = 2 * c + 1" by simp
   5.126 -  with that show thesis .
   5.127 +  have "a = 2 * (a div 2) + a mod 2"
   5.128 +    by (simp add: mult_div_mod_eq)
   5.129 +  with assms have "a = 2 * (a div 2) + 1"
   5.130 +    by (simp add: odd_iff_mod_2_eq_one)
   5.131 +  then show ?thesis ..
   5.132 +qed
   5.133 +
   5.134 +lemma mod_2_eq_odd:
   5.135 +  "a mod 2 = of_bool (odd a)"
   5.136 +  by (auto elim: oddE)
   5.137 +
   5.138 +lemma one_mod_2_pow_eq [simp]:
   5.139 +  "1 mod (2 ^ n) = of_bool (n > 0)"
   5.140 +proof -
   5.141 +  have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
   5.142 +    by (induct n) (simp_all add: mod_mult2_eq)
   5.143 +  then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
   5.144 +    by simp
   5.145 +  then show ?thesis
   5.146 +    by (simp add: of_nat_mod)
   5.147 +qed
   5.148 +
   5.149 +lemma even_of_nat [simp]:
   5.150 +  "even (of_nat a) \<longleftrightarrow> even a"
   5.151 +proof -
   5.152 +  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
   5.153 +    by simp
   5.154 +  also have "\<dots> \<longleftrightarrow> even a"
   5.155 +    by (simp only: of_nat_dvd_iff)
   5.156 +  finally show ?thesis .
   5.157 +qed
   5.158 +
   5.159 +lemma even_zero [simp]:
   5.160 +  "even 0"
   5.161 +  by (fact dvd_0_right)
   5.162 +
   5.163 +lemma odd_one [simp]:
   5.164 +  "odd 1"
   5.165 +proof -
   5.166 +  have "\<not> (2 :: nat) dvd 1"
   5.167 +    by simp
   5.168 +  then have "\<not> of_nat 2 dvd of_nat 1"
   5.169 +    unfolding of_nat_dvd_iff by simp
   5.170 +  then show ?thesis
   5.171 +    by simp
   5.172  qed
   5.173  
   5.174 -lemma even_times_iff [simp]: "even (a * b) \<longleftrightarrow> even a \<or> even b"
   5.175 -  by (auto dest: even_multD)
   5.176 +lemma odd_even_add:
   5.177 +  "even (a + b)" if "odd a" and "odd b"
   5.178 +proof -
   5.179 +  from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
   5.180 +    by (blast elim: oddE)
   5.181 +  then have "a + b = 2 * c + 2 * d + (1 + 1)"
   5.182 +    by (simp only: ac_simps)
   5.183 +  also have "\<dots> = 2 * (c + d + 1)"
   5.184 +    by (simp add: algebra_simps)
   5.185 +  finally show ?thesis ..
   5.186 +qed
   5.187 +
   5.188 +lemma even_add [simp]:
   5.189 +  "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
   5.190 +  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
   5.191 +
   5.192 +lemma odd_add [simp]:
   5.193 +  "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
   5.194 +  by simp
   5.195 +
   5.196 +lemma even_plus_one_iff [simp]:
   5.197 +  "even (a + 1) \<longleftrightarrow> odd a"
   5.198 +  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
   5.199 +
   5.200 +lemma even_mult_iff [simp]:
   5.201 +  "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
   5.202 +proof
   5.203 +  assume ?Q
   5.204 +  then show ?P
   5.205 +    by auto
   5.206 +next
   5.207 +  assume ?P
   5.208 +  show ?Q
   5.209 +  proof (rule ccontr)
   5.210 +    assume "\<not> (even a \<or> even b)"
   5.211 +    then have "odd a" and "odd b"
   5.212 +      by auto
   5.213 +    then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
   5.214 +      by (blast elim: oddE)
   5.215 +    then have "a * b = (2 * r + 1) * (2 * s + 1)"
   5.216 +      by simp
   5.217 +    also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
   5.218 +      by (simp add: algebra_simps)
   5.219 +    finally have "odd (a * b)"
   5.220 +      by simp
   5.221 +    with \<open>?P\<close> show False
   5.222 +      by auto
   5.223 +  qed
   5.224 +qed
   5.225  
   5.226  lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
   5.227  proof -
   5.228    have "even (2 * numeral n)"
   5.229 -    unfolding even_times_iff by simp
   5.230 +    unfolding even_mult_iff by simp
   5.231    then have "even (numeral n + numeral n)"
   5.232      unfolding mult_2 .
   5.233    then show ?thesis
   5.234 @@ -77,15 +232,26 @@
   5.235    then show False by simp
   5.236  qed
   5.237  
   5.238 -lemma even_add [simp]: "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
   5.239 -  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
   5.240 -
   5.241 -lemma odd_add [simp]: "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
   5.242 -  by simp
   5.243 -
   5.244  lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   5.245    by (induct n) auto
   5.246  
   5.247 +lemma even_succ_div_two [simp]:
   5.248 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
   5.249 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
   5.250 +
   5.251 +lemma odd_succ_div_two [simp]:
   5.252 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
   5.253 +  by (auto elim!: oddE simp add: add.assoc)
   5.254 +
   5.255 +lemma even_two_times_div_two:
   5.256 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
   5.257 +  by (fact dvd_mult_div_cancel)
   5.258 +
   5.259 +lemma odd_two_times_div_two_succ [simp]:
   5.260 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   5.261 +  using mult_div_mod_eq [of 2 a]
   5.262 +  by (simp add: even_iff_mod_2_eq_zero)
   5.263 +
   5.264  end
   5.265  
   5.266  class ring_parity = ring + semiring_parity
   5.267 @@ -93,166 +259,48 @@
   5.268  
   5.269  subclass comm_ring_1 ..
   5.270  
   5.271 -lemma even_minus [simp]: "even (- a) \<longleftrightarrow> even a"
   5.272 +lemma even_minus [simp]:
   5.273 +  "even (- a) \<longleftrightarrow> even a"
   5.274    by (fact dvd_minus_iff)
   5.275  
   5.276 -lemma even_diff [simp]: "even (a - b) \<longleftrightarrow> even (a + b)"
   5.277 +lemma even_diff [simp]:
   5.278 +  "even (a - b) \<longleftrightarrow> even (a + b)"
   5.279    using even_add [of a "- b"] by simp
   5.280  
   5.281  end
   5.282  
   5.283 -class unique_euclidean_semiring_parity = unique_euclidean_semiring +
   5.284 -  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   5.285 -  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   5.286 -  assumes zero_not_eq_two: "0 \<noteq> 2"
   5.287 -begin
   5.288  
   5.289 -lemma parity_cases [case_names even odd]:
   5.290 -  assumes "a mod 2 = 0 \<Longrightarrow> P"
   5.291 -  assumes "a mod 2 = 1 \<Longrightarrow> P"
   5.292 -  shows P
   5.293 -  using assms parity by blast
   5.294 -
   5.295 -lemma one_div_two_eq_zero [simp]:
   5.296 -  "1 div 2 = 0"
   5.297 -proof (cases "2 = 0")
   5.298 -  case True then show ?thesis by simp
   5.299 -next
   5.300 -  case False
   5.301 -  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
   5.302 -  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
   5.303 -  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
   5.304 -  then have "1 div 2 = 0 \<or> 2 = 0" by simp
   5.305 -  with False show ?thesis by auto
   5.306 -qed
   5.307 -
   5.308 -lemma not_mod_2_eq_0_eq_1 [simp]:
   5.309 -  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
   5.310 -  by (cases a rule: parity_cases) simp_all
   5.311 -
   5.312 -lemma not_mod_2_eq_1_eq_0 [simp]:
   5.313 -  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
   5.314 -  by (cases a rule: parity_cases) simp_all
   5.315 +subsection \<open>Instance for @{typ nat}\<close>
   5.316  
   5.317 -subclass semiring_parity
   5.318 -proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
   5.319 -  show "1 mod 2 = 1"
   5.320 -    by (fact one_mod_two_eq_one)
   5.321 -next
   5.322 -  fix a b
   5.323 -  assume "a mod 2 = 1"
   5.324 -  moreover assume "b mod 2 = 1"
   5.325 -  ultimately show "(a + b) mod 2 = 0"
   5.326 -    using mod_add_eq [of a 2 b] by simp
   5.327 -next
   5.328 -  fix a b
   5.329 -  assume "(a * b) mod 2 = 0"
   5.330 -  then have "(a mod 2) * (b mod 2) mod 2 = 0"
   5.331 -    by (simp add: mod_mult_eq)
   5.332 -  then have "(a mod 2) * (b mod 2) = 0"
   5.333 -    by (cases "a mod 2 = 0") simp_all
   5.334 -  then show "a mod 2 = 0 \<or> b mod 2 = 0"
   5.335 -    by (rule divisors_zero)
   5.336 -next
   5.337 -  fix a
   5.338 -  assume "a mod 2 = 1"
   5.339 -  then have "a = a div 2 * 2 + 1"
   5.340 -    using div_mult_mod_eq [of a 2] by simp
   5.341 -  then show "\<exists>b. a = b + 1" ..
   5.342 -qed
   5.343 +instance nat :: semiring_parity
   5.344 +  by standard (simp_all add: dvd_eq_mod_eq_0)
   5.345  
   5.346 -lemma even_iff_mod_2_eq_zero:
   5.347 -  "even a \<longleftrightarrow> a mod 2 = 0"
   5.348 -  by (fact dvd_eq_mod_eq_0)
   5.349 -
   5.350 -lemma odd_iff_mod_2_eq_one:
   5.351 -  "odd a \<longleftrightarrow> a mod 2 = 1"
   5.352 -  by (simp add: even_iff_mod_2_eq_zero)
   5.353 -
   5.354 -lemma even_succ_div_two [simp]:
   5.355 -  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
   5.356 -  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
   5.357 -
   5.358 -lemma odd_succ_div_two [simp]:
   5.359 -  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
   5.360 -  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
   5.361 -
   5.362 -lemma even_two_times_div_two:
   5.363 -  "even a \<Longrightarrow> 2 * (a div 2) = a"
   5.364 -  by (fact dvd_mult_div_cancel)
   5.365 -
   5.366 -lemma odd_two_times_div_two_succ [simp]:
   5.367 -  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   5.368 -  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
   5.369 - 
   5.370 -end
   5.371 -
   5.372 -
   5.373 -subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
   5.374 -
   5.375 -lemma even_Suc_Suc_iff [simp]: "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
   5.376 +lemma even_Suc_Suc_iff [simp]:
   5.377 +  "even (Suc (Suc n)) \<longleftrightarrow> even n"
   5.378    using dvd_add_triv_right_iff [of 2 n] by simp
   5.379  
   5.380 -lemma even_Suc [simp]: "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
   5.381 -  by (induct n) auto
   5.382 +lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
   5.383 +  using even_plus_one_iff [of n] by simp
   5.384  
   5.385 -lemma even_diff_nat [simp]: "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
   5.386 -  for m n :: nat
   5.387 +lemma even_diff_nat [simp]:
   5.388 +  "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
   5.389  proof (cases "n \<le> m")
   5.390    case True
   5.391    then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
   5.392 -  moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
   5.393 -  ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
   5.394 +  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
   5.395 +  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
   5.396    then show ?thesis by auto
   5.397  next
   5.398    case False
   5.399    then show ?thesis by simp
   5.400  qed
   5.401  
   5.402 -instance nat :: semiring_parity
   5.403 -proof
   5.404 -  show "\<not> 2 dvd (1 :: nat)"
   5.405 -    by (rule notI, erule dvdE) simp
   5.406 -next
   5.407 -  fix m n :: nat
   5.408 -  assume "\<not> 2 dvd m"
   5.409 -  moreover assume "\<not> 2 dvd n"
   5.410 -  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
   5.411 -    by simp
   5.412 -  then have "2 dvd (Suc m + Suc n)"
   5.413 -    by (blast intro: dvd_add)
   5.414 -  also have "Suc m + Suc n = m + n + 2"
   5.415 -    by simp
   5.416 -  finally show "2 dvd (m + n)"
   5.417 -    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
   5.418 -next
   5.419 -  fix m n :: nat
   5.420 -  assume *: "2 dvd (m * n)"
   5.421 -  show "2 dvd m \<or> 2 dvd n"
   5.422 -  proof (rule disjCI)
   5.423 -    assume "\<not> 2 dvd n"
   5.424 -    then have "2 dvd (Suc n)" by simp
   5.425 -    then obtain r where "Suc n = 2 * r" ..
   5.426 -    moreover from * obtain s where "m * n = 2 * s" ..
   5.427 -    then have "2 * s + m = m * Suc n" by simp
   5.428 -    ultimately have " 2 * s + m = 2 * (m * r)"
   5.429 -      by (simp add: algebra_simps)
   5.430 -    then have "m = 2 * (m * r - s)" by simp
   5.431 -    then show "2 dvd m" ..
   5.432 -  qed
   5.433 -next
   5.434 -  fix n :: nat
   5.435 -  assume "\<not> 2 dvd n"
   5.436 -  then show "\<exists>m. n = m + 1"
   5.437 -    by (cases n) simp_all
   5.438 -qed
   5.439 -
   5.440 -lemma odd_pos: "odd n \<Longrightarrow> 0 < n"
   5.441 -  for n :: nat
   5.442 +lemma odd_pos:
   5.443 +  "odd n \<Longrightarrow> 0 < n" for n :: nat
   5.444    by (auto elim: oddE)
   5.445  
   5.446 -lemma Suc_double_not_eq_double: "Suc (2 * m) \<noteq> 2 * n"
   5.447 -  for m n :: nat
   5.448 +lemma Suc_double_not_eq_double:
   5.449 +  "Suc (2 * m) \<noteq> 2 * n"
   5.450  proof
   5.451    assume "Suc (2 * m) = 2 * n"
   5.452    moreover have "odd (Suc (2 * m))" and "even (2 * n)"
   5.453 @@ -260,52 +308,58 @@
   5.454    ultimately show False by simp
   5.455  qed
   5.456  
   5.457 -lemma double_not_eq_Suc_double: "2 * m \<noteq> Suc (2 * n)"
   5.458 -  for m n :: nat
   5.459 +lemma double_not_eq_Suc_double:
   5.460 +  "2 * m \<noteq> Suc (2 * n)"
   5.461    using Suc_double_not_eq_double [of n m] by simp
   5.462  
   5.463 -lemma even_diff_iff [simp]: "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
   5.464 -  for k l :: int
   5.465 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   5.466 +lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   5.467 +  by (auto elim: oddE)
   5.468  
   5.469 -lemma even_abs_add_iff [simp]: "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
   5.470 -  for k l :: int
   5.471 -  by (cases "k \<ge> 0") (simp_all add: ac_simps)
   5.472 +lemma even_Suc_div_two [simp]:
   5.473 +  "even n \<Longrightarrow> Suc n div 2 = n div 2"
   5.474 +  using even_succ_div_two [of n] by simp
   5.475  
   5.476 -lemma even_add_abs_iff [simp]: "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
   5.477 -  for k l :: int
   5.478 -  using even_abs_add_iff [of l k] by (simp add: ac_simps)
   5.479 +lemma odd_Suc_div_two [simp]:
   5.480 +  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   5.481 +  using odd_succ_div_two [of n] by simp
   5.482  
   5.483 -instance int :: ring_parity
   5.484 -proof
   5.485 -  show "\<not> 2 dvd (1 :: int)"
   5.486 -    by (simp add: dvd_int_unfold_dvd_nat)
   5.487 -next
   5.488 -  fix k l :: int
   5.489 -  assume "\<not> 2 dvd k"
   5.490 -  moreover assume "\<not> 2 dvd l"
   5.491 -  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
   5.492 -    by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
   5.493 -  then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
   5.494 -    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
   5.495 -  then show "2 dvd (k + l)"
   5.496 +lemma odd_two_times_div_two_nat [simp]:
   5.497 +  assumes "odd n"
   5.498 +  shows "2 * (n div 2) = n - (1 :: nat)"
   5.499 +proof -
   5.500 +  from assms have "2 * (n div 2) + 1 = n"
   5.501 +    by (rule odd_two_times_div_two_succ)
   5.502 +  then have "Suc (2 * (n div 2)) - 1 = n - 1"
   5.503      by simp
   5.504 -next
   5.505 -  fix k l :: int
   5.506 -  assume "2 dvd (k * l)"
   5.507 -  then show "2 dvd k \<or> 2 dvd l"
   5.508 -    by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
   5.509 -next
   5.510 -  fix k :: int
   5.511 -  have "k = (k - 1) + 1" by simp
   5.512 -  then show "\<exists>l. k = l + 1" ..
   5.513 +  then show ?thesis
   5.514 +    by simp
   5.515  qed
   5.516  
   5.517 -lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
   5.518 -  by (simp add: dvd_int_iff)
   5.519 -
   5.520 -lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   5.521 -  by (simp add: even_int_iff [symmetric])
   5.522 +lemma parity_induct [case_names zero even odd]:
   5.523 +  assumes zero: "P 0"
   5.524 +  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
   5.525 +  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
   5.526 +  shows "P n"
   5.527 +proof (induct n rule: less_induct)
   5.528 +  case (less n)
   5.529 +  show "P n"
   5.530 +  proof (cases "n = 0")
   5.531 +    case True with zero show ?thesis by simp
   5.532 +  next
   5.533 +    case False
   5.534 +    with less have hyp: "P (n div 2)" by simp
   5.535 +    show ?thesis
   5.536 +    proof (cases "even n")
   5.537 +      case True
   5.538 +      with hyp even [of "n div 2"] show ?thesis
   5.539 +        by simp
   5.540 +    next
   5.541 +      case False
   5.542 +      with hyp odd [of "n div 2"] show ?thesis
   5.543 +        by simp
   5.544 +    qed
   5.545 +  qed
   5.546 +qed
   5.547  
   5.548  
   5.549  subsection \<open>Parity and powers\<close>
   5.550 @@ -319,6 +373,10 @@
   5.551  lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
   5.552    by (auto elim: oddE)
   5.553  
   5.554 +lemma uminus_power_if:
   5.555 +  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
   5.556 +  by auto
   5.557 +
   5.558  lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
   5.559    by simp
   5.560  
   5.561 @@ -396,9 +454,6 @@
   5.562    qed
   5.563  qed
   5.564  
   5.565 -lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))"
   5.566 -  by auto
   5.567 -
   5.568  text \<open>Simplify, when the exponent is a numeral\<close>
   5.569  
   5.570  lemma zero_le_power_eq_numeral [simp]:
   5.571 @@ -428,9 +483,4 @@
   5.572  
   5.573  end
   5.574  
   5.575 -
   5.576 -subsubsection \<open>Tool setup\<close>
   5.577 -
   5.578 -declare transfer_morphism_int_nat [transfer add return: even_int_iff]
   5.579 -
   5.580  end
     6.1 --- a/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:22 2017 +0200
     6.2 +++ b/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:22 2017 +0200
     6.3 @@ -11,7 +11,7 @@
     6.4  
     6.5  subsection \<open>Truncating bit representations of numeric types\<close>
     6.6  
     6.7 -class semiring_bits = unique_euclidean_semiring_parity +
     6.8 +class semiring_bits = semiring_parity +
     6.9    assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
    6.10  begin
    6.11  
    6.12 @@ -27,28 +27,16 @@
    6.13    by (simp add: bitrunc_eq_mod)
    6.14  
    6.15  lemma bitrunc_Suc [simp]:
    6.16 -  "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + a mod 2"
    6.17 +  "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + of_bool (odd a)"
    6.18  proof -
    6.19 -  define b and c
    6.20 -    where "b = a div 2" and "c = a mod 2"
    6.21 -  then have a: "a = b * 2 + c" 
    6.22 -    and "c = 0 \<or> c = 1"
    6.23 -    by (simp_all add: div_mult_mod_eq parity)
    6.24 -  from \<open>c = 0 \<or> c = 1\<close>
    6.25 -  have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
    6.26 -  proof
    6.27 -    assume "c = 0"
    6.28 -    moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)"
    6.29 -      by (simp add: mod_mult_mult1)
    6.30 -    ultimately show ?thesis
    6.31 -      by (simp add: bitrunc_eq_mod ac_simps)
    6.32 -  next
    6.33 -    assume "c = 1"
    6.34 -    with semiring_bits [of b "2 ^ n"] show ?thesis
    6.35 -      by (simp add: bitrunc_eq_mod ac_simps)
    6.36 -  qed
    6.37 -  with a show ?thesis
    6.38 -    by (simp add: b_def c_def)
    6.39 +  have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
    6.40 +    if "odd a"
    6.41 +    using that semiring_bits [of "a div 2" "2 ^ n"]
    6.42 +      by (simp add: algebra_simps odd_iff_mod_2_eq_one mult_mod_right)
    6.43 +  also have "\<dots> = a mod (2 * 2 ^ n)"
    6.44 +    by (simp only: div_mult_mod_eq)
    6.45 +  finally show ?thesis
    6.46 +    by (simp add: bitrunc_eq_mod algebra_simps mult_mod_right)
    6.47  qed
    6.48  
    6.49  lemma bitrunc_of_0 [simp]:
    6.50 @@ -57,11 +45,11 @@
    6.51  
    6.52  lemma bitrunc_plus:
    6.53    "bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
    6.54 -  by (simp add: bitrunc_eq_mod mod_add_eq)
    6.55 +  by (simp add: bitrunc_eq_mod mod_simps)
    6.56  
    6.57  lemma bitrunc_of_1_eq_0_iff [simp]:
    6.58    "bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
    6.59 -  by (induct n) simp_all
    6.60 +  by (simp add: bitrunc_eq_mod)
    6.61  
    6.62  end
    6.63  
    6.64 @@ -113,7 +101,7 @@
    6.65  
    6.66  lemma signed_bitrunc_Suc [simp]:
    6.67    "signed_bitrunc (Suc n) k = signed_bitrunc n (k div 2) * 2 + k mod 2"
    6.68 -  using zero_not_eq_two by (simp add: signed_bitrunc_eq_bitrunc algebra_simps)
    6.69 +  by (simp add: odd_iff_mod_2_eq_one signed_bitrunc_eq_bitrunc algebra_simps)
    6.70  
    6.71  lemma signed_bitrunc_of_0 [simp]:
    6.72    "signed_bitrunc n 0 = 0"