author haftmann Mon, 04 Nov 2019 20:38:15 +0000 changeset 71042 400e9512f1d3 parent 71041 fdb6c5034c24 child 71045 9858f391ed2d
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
 src/HOL/Library/Boolean_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/ROOT file | annotate | diff | comparison | revisions src/HOL/ex/Bit_Lists.thy file | annotate | diff | comparison | revisions src/HOL/ex/Bit_Operations.thy file | annotate | diff | comparison | revisions src/HOL/ex/Word.thy file | annotate | diff | comparison | revisions src/HOL/ex/Word_Type.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Library/Boolean_Algebra.thy	Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 04 20:38:15 2019 +0000
@@ -211,7 +211,7 @@
definition xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<oplus>" 65)
where "x \<oplus> y = (x \<^bold>\<sqinter> \<sim> y) \<^bold>\<squnion> (\<sim> x \<^bold>\<sqinter> y)"

-sublocale xor: abel_semigroup xor
+sublocale xor: comm_monoid xor \<zero>
proof
fix x y z :: 'a
let ?t = "(x \<^bold>\<sqinter> y \<^bold>\<sqinter> z) \<^bold>\<squnion> (x \<^bold>\<sqinter> \<sim> y \<^bold>\<sqinter> \<sim> z) \<^bold>\<squnion> (\<sim> x \<^bold>\<sqinter> y \<^bold>\<sqinter> \<sim> z) \<^bold>\<squnion> (\<sim> x \<^bold>\<sqinter> \<sim> y \<^bold>\<sqinter> z)"
@@ -222,6 +222,8 @@
(simp only: conj_disj_distribs conj_ac disj_ac)
show "x \<oplus> y = y \<oplus> x"
by (simp only: xor_def conj_commute disj_commute)
+  show "x \<oplus> \<zero> = x"
qed

lemmas xor_assoc = xor.assoc```
```--- a/src/HOL/ROOT	Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/ROOT	Mon Nov 04 20:38:15 2019 +0000
@@ -650,7 +650,7 @@
Triangular_Numbers
Unification
While_Combinator_Example
-    Word_Type
+    Word
veriT_Preprocessing
theories [skip_proofs = false]
SAT_Examples```
```--- a/src/HOL/ex/Bit_Lists.thy	Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/ex/Bit_Lists.thy	Mon Nov 04 20:38:15 2019 +0000
@@ -5,31 +5,10 @@

theory Bit_Lists
imports
-    Main
-    "HOL-Library.Boolean_Algebra"
-begin
-
+    Bit_Operations
begin

-lemma minus_diff_commute:
-  "- b - a = - a - b"
-
-end
-
-
-subsection \<open>Bit representations\<close>
-
-subsubsection \<open>Mere syntactic bit representation\<close>
-
-class bit_representation =
-  fixes bits_of :: "'a \<Rightarrow> bool list"
-    and of_bits :: "bool list \<Rightarrow> 'a"
-  assumes of_bits_of [simp]: "of_bits (bits_of a) = a"
-
-
-subsubsection \<open>Algebraic bit representation\<close>
+subsection \<open>Fragments of algebraic bit representations\<close>

context comm_semiring_1
begin
@@ -57,7 +36,7 @@

lemma unsigned_of_bits_take [simp]:
-  "unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)"
+  "unsigned_of_bits (take n bs) = Parity.take_bit n (unsigned_of_bits bs)"
proof (induction bs arbitrary: n)
case Nil
then show ?case
@@ -69,7 +48,7 @@
qed

lemma unsigned_of_bits_drop [simp]:
-  "unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)"
+  "unsigned_of_bits (drop n bs) = Parity.drop_bit n (unsigned_of_bits bs)"
proof (induction bs arbitrary: n)
case Nil
then show ?case
@@ -80,10 +59,44 @@
by (cases n) simp_all
qed

+primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
+  where
+    "n_bits_of 0 a = []"
+  | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)"
+
+lemma n_bits_of_eq_iff:
+  "n_bits_of n a = n_bits_of n b \<longleftrightarrow> Parity.take_bit n a = Parity.take_bit n b"
+  apply (induction n arbitrary: a b)
+   apply (auto elim!: evenE oddE)
+   apply (metis dvd_triv_right even_plus_one_iff)
+  apply (metis dvd_triv_right even_plus_one_iff)
+  done
+
+lemma take_n_bits_of [simp]:
+  "take m (n_bits_of n a) = n_bits_of (min m n) a"
+proof -
+  define q and v and w where "q = min m n" and "v = m - q" and "w = n - q"
+  then have "v = 0 \<or> w = 0"
+    by auto
+  then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a"
+    by (induction q arbitrary: a) auto
+  with q_def v_def w_def show ?thesis
+    by simp
+qed
+
+lemma unsigned_of_bits_n_bits_of [simp]:
+  "unsigned_of_bits (n_bits_of n a) = Parity.take_bit n a"
+  by (induction n arbitrary: a) (simp_all add: ac_simps)
+
end

-subsubsection \<open>Instances\<close>
+subsection \<open>Syntactic bit representation\<close>
+
+class bit_representation =
+  fixes bits_of :: "'a \<Rightarrow> bool list"
+    and of_bits :: "bool list \<Rightarrow> 'a"
+  assumes of_bits_of [simp]: "of_bits (bits_of a) = a"

text \<open>Unclear whether a \<^typ>\<open>bool\<close> instantiation is needed or not\<close>

@@ -216,7 +229,7 @@

lemma of_bits_drop [simp]:
-  "of_bits (drop n bs) = drop_bit n (of_bits bs :: int)"
+  "of_bits (drop n bs) = Parity.drop_bit n (of_bits bs :: int)"
if "n < length bs"
using that proof (induction bs arbitrary: n)
case Nil
@@ -240,140 +253,47 @@

end

-
-subsection \<open>Syntactic bit operations\<close>
+lemma unsigned_of_bits_eq_of_bits:
+  "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"

-class bit_operations = bit_representation +
-  fixes not :: "'a \<Rightarrow> 'a"  ("NOT")
-    and "and" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
-    and or :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
-    and xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
-    and shift_left :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
-    and shift_right :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
-  assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of"
-    and and_eq: "length bs = length cs \<Longrightarrow>
-      of_bits bs AND of_bits cs = of_bits (map2 (\<and>) bs cs)"
-    and semilattice_and: "semilattice (AND)"
-    and or_eq: "length bs = length cs \<Longrightarrow>
-      of_bits bs OR of_bits cs = of_bits (map2 (\<or>) bs cs)"
-    and semilattice_or: "semilattice (OR)"
-    and xor_eq: "length bs = length cs \<Longrightarrow>
-      of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)"
-    and abel_semigroup_xor: "abel_semigroup (XOR)"
-    and shift_right_eq: "a << n = of_bits (replicate n False @ bits_of a)"
-    and shift_left_eq: "n < length (bits_of a) \<Longrightarrow> a >> n = of_bits (drop n (bits_of a))"
+instantiation word :: (len) bit_representation
begin

-text \<open>
-  We want the bitwise operations to bind slightly weaker
-  than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
-  bind slightly stronger than \<open>*\<close>.
-\<close>
+lift_definition bits_of_word :: "'a word \<Rightarrow> bool list"
+  is "n_bits_of LENGTH('a)"

-sublocale "and": semilattice "(AND)"
-  by (fact semilattice_and)
+lift_definition of_bits_word :: "bool list \<Rightarrow> 'a word"
+  is unsigned_of_bits .

-sublocale or: semilattice "(OR)"
-  by (fact semilattice_or)
-
-sublocale xor: abel_semigroup "(XOR)"
-  by (fact abel_semigroup_xor)
+instance proof
+  fix a :: "'a word"
+  show "of_bits (bits_of a) = a"
+    by transfer simp
+qed

end

-subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
-
-locale zip_nat = single: abel_semigroup f
-    for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70) +
-  assumes end_of_bits: "\<not> False \<^bold>* False"
-begin
-
-lemma False_P_imp:
-  "False \<^bold>* True \<and> P" if "False \<^bold>* P"
-  using that end_of_bits by (cases P) simp_all
-
-function F :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infixl "\<^bold>\<times>" 70)
-  where "m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
-    else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2)"
-  by auto
-
-termination
-  by (relation "measure (case_prod (+))") auto
-
-lemma zero_left_eq:
-  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
-  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma zero_right_eq:
-  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
-  by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma simps [simp]:
-  "0 \<^bold>\<times> 0 = 0"
-  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
-  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
-  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
-  by (simp_all only: zero_left_eq zero_right_eq) simp
-
-lemma rec:
-  "m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
-  by (cases "m = 0 \<and> n = 0") (auto simp add: end_of_bits)
-
-declare F.simps [simp del]
+subsection \<open>Bit representations with bit operations\<close>

-sublocale abel_semigroup F
-proof
-  show "m \<^bold>\<times> n \<^bold>\<times> q = m \<^bold>\<times> (n \<^bold>\<times> q)" for m n q :: nat
-  proof (induction m arbitrary: n q rule: nat_bit_induct)
-    case zero
-    show ?case
-      by simp
-  next
-    case (even m)
-    with rec [of "2 * m"] rec [of _ q] show ?case
-      by (cases "even n") (auto dest: False_P_imp)
-  next
-    case (odd m)
-    with rec [of "Suc (2 * m)"] rec [of _ q] show ?case
-      by (cases "even n"; cases "even q")
-        (auto dest: False_P_imp simp add: ac_simps)
-  qed
-  show "m \<^bold>\<times> n = n \<^bold>\<times> m" for m n :: nat
-  proof (induction m arbitrary: n rule: nat_bit_induct)
-    case zero
-    show ?case
-  next
-    case (even m)
-    with rec [of "2 * m" n] rec [of n "2 * m"] show ?case
-  next
-    case (odd m)
-    with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case
-  qed
-qed
+class semiring_bit_representation = semiring_bit_operations + bit_representation +
+  assumes and_eq: "length bs = length cs \<Longrightarrow>
+      of_bits bs AND of_bits cs = of_bits (map2 (\<and>) bs cs)"
+    and or_eq: "length bs = length cs \<Longrightarrow>
+      of_bits bs OR of_bits cs = of_bits (map2 (\<or>) bs cs)"
+    and xor_eq: "length bs = length cs \<Longrightarrow>
+      of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)"
+    and shift_bit_eq: "shift_bit n a = of_bits (replicate n False @ bits_of a)"
+    and drop_bit_eq: "n < length (bits_of a) \<Longrightarrow> drop_bit n a = of_bits (drop n (bits_of a))"

-lemma self [simp]:
-  "n \<^bold>\<times> n = of_bool (True \<^bold>* True) * n"
-  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
+class ring_bit_representation = ring_bit_operations + semiring_bit_representation +
+  assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of"

-lemma even_iff [simp]:
-  "even (m \<^bold>\<times> n) \<longleftrightarrow> \<not> (odd m \<^bold>* odd n)"
-proof (induction m arbitrary: n rule: nat_bit_induct)
-  case zero
-  show ?case
-    by (cases "even n") (simp_all add: end_of_bits)
-next
-  case (even m)
-  then show ?case
-    by (simp add: rec [of "2 * m"])
-next
-  case (odd m)
-  then show ?case
-    by (simp add: rec [of "Suc (2 * m)"])
-qed
+
+context zip_nat
+begin

lemma of_bits:
"of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: nat)"
@@ -391,366 +311,15 @@

end

-instantiation nat :: bit_operations
-begin
-
-definition not_nat :: "nat \<Rightarrow> nat"
-  where "not_nat = of_bits \<circ> map Not \<circ> bits_of"
-
-global_interpretation and_nat: zip_nat "(\<and>)"
-  defines and_nat = and_nat.F
-  by standard auto
-
-global_interpretation and_nat: semilattice "(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat"
-proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard)
-  show "n AND n = n" for n :: nat
-qed
-
-declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-lemma zero_nat_and_eq [simp]:
-  "0 AND n = 0" for n :: nat
-  by simp
-
-lemma and_zero_nat_eq [simp]:
-  "n AND 0 = 0" for n :: nat
-  by simp
-
-global_interpretation or_nat: zip_nat "(\<or>)"
-  defines or_nat = or_nat.F
-  by standard auto
-
-global_interpretation or_nat: semilattice "(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat"
-proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard)
-  show "n OR n = n" for n :: nat
-qed
-
-declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-lemma zero_nat_or_eq [simp]:
-  "0 OR n = n" for n :: nat
-  by simp
-
-lemma or_zero_nat_eq [simp]:
-  "n OR 0 = n" for n :: nat
-  by simp
-
-global_interpretation xor_nat: zip_nat "(\<noteq>)"
-  defines xor_nat = xor_nat.F
-  by standard auto
-
-declare xor_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-lemma zero_nat_xor_eq [simp]:
-  "0 XOR n = n" for n :: nat
-  by simp
-
-lemma xor_zero_nat_eq [simp]:
-  "n XOR 0 = n" for n :: nat
-  by simp
-
-definition shift_left_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where [simp]: "m << n = push_bit n m" for m :: nat
-
-definition shift_right_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where [simp]: "m >> n = drop_bit n m" for m :: nat
+instance nat :: semiring_bit_representation
+  apply standard
+      apply (simp_all only: and_nat.of_bits or_nat.of_bits xor_nat.of_bits)
+   apply (simp_all add: drop_bit_eq_div Parity.drop_bit_eq_div shift_bit_eq_mult push_bit_eq_mult)
+  done

-instance proof
-  show "semilattice ((AND) :: nat \<Rightarrow> _)"
-    by (fact and_nat.semilattice_axioms)
-  show "semilattice ((OR):: nat \<Rightarrow> _)"
-    by (fact or_nat.semilattice_axioms)
-  show "abel_semigroup ((XOR):: nat \<Rightarrow> _)"
-    by (fact xor_nat.abel_semigroup_axioms)
-  show "(not :: nat \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of"
-    by (fact not_nat_def)
-  show "of_bits bs AND of_bits cs = (of_bits (map2 (\<and>) bs cs) :: nat)"
-    if "length bs = length cs" for bs cs
-    using that by (fact and_nat.of_bits)
-  show "of_bits bs OR of_bits cs = (of_bits (map2 (\<or>) bs cs) :: nat)"
-    if "length bs = length cs" for bs cs
-    using that by (fact or_nat.of_bits)
-  show "of_bits bs XOR of_bits cs = (of_bits (map2 (\<noteq>) bs cs) :: nat)"
-    if "length bs = length cs" for bs cs
-    using that by (fact xor_nat.of_bits)
-  show "m << n = of_bits (replicate n False @ bits_of m)"
-    for m n :: nat
-    by simp
-  show "m >> n = of_bits (drop n (bits_of m))"
-    for m n :: nat
-    by simp
-qed
-
-end
-
-global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat"
-  by standard simp
-
-global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat"
-  by standard simp
-
-lemma not_nat_simps [simp]:
-  "NOT 0 = (0::nat)"
-  "n > 0 \<Longrightarrow> NOT n = of_bool (even n) + 2 * NOT (n div 2)" for n :: nat
-
-lemma not_1_nat [simp]:
-  "NOT 1 = (0::nat)"
-  by simp
-
-lemma not_Suc_0 [simp]:
-  "NOT (Suc 0) = (0::nat)"
-  by simp
-
-lemma Suc_0_and_eq [simp]:
-  "Suc 0 AND n = n mod 2"
-  by (cases n) auto
-
-lemma and_Suc_0_eq [simp]:
-  "n AND Suc 0 = n mod 2"
-  using Suc_0_and_eq [of n] by (simp add: ac_simps)
-
-lemma Suc_0_or_eq [simp]:
-  "Suc 0 OR n = n + of_bool (even n)"
-  by (cases n) (simp_all add: ac_simps)
-
-lemma or_Suc_0_eq [simp]:
-  "n OR Suc 0 = n + of_bool (even n)"
-  using Suc_0_or_eq [of n] by (simp add: ac_simps)
-
-lemma Suc_0_xor_eq [simp]:
-  "Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)"
-  by (cases n) (simp_all add: ac_simps)
-
-lemma xor_Suc_0_eq [simp]:
-  "n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)"
-  using Suc_0_xor_eq [of n] by (simp add: ac_simps)
-
-
-subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
-
-abbreviation (input) complement :: "int \<Rightarrow> int"
-  where "complement k \<equiv> - k - 1"
-
-lemma complement_half:
-  "complement (k * 2) div 2 = complement k"
-  by simp
-
-lemma complement_div_2:
-  "complement (k div 2) = complement k div 2"
-  by linarith
-
-locale zip_int = single: abel_semigroup f
-  for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70)
+context zip_int
begin

-lemma False_False_imp_True_True:
-  "True \<^bold>* True" if "False \<^bold>* False"
-proof (rule ccontr)
-  assume "\<not> True \<^bold>* True"
-  with that show False
-    using single.assoc [of False True True]
-    by (cases "False \<^bold>* True") simp_all
-qed
-
-function F :: "int \<Rightarrow> int \<Rightarrow> int"  (infixl "\<^bold>\<times>" 70)
-  where "k \<^bold>\<times> l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
-    then - of_bool (odd k \<^bold>* odd l)
-    else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2)"
-  by auto
-
-termination
-  by (relation "measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))") auto
-
-lemma zero_left_eq:
-  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction l rule: int_bit_induct)
-   (simp_all split: bool.split)
-
-lemma minus_left_eq:
-  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction l rule: int_bit_induct)
-   (simp_all split: bool.split)
-
-lemma zero_right_eq:
-  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct)
-    (simp_all add: ac_simps split: bool.split)
-
-lemma minus_right_eq:
-  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct)
-    (simp_all add: ac_simps split: bool.split)
-
-lemma simps [simp]:
-  "0 \<^bold>\<times> 0 = - of_bool (False \<^bold>* False)"
-  "- 1 \<^bold>\<times> 0 = - of_bool (True \<^bold>* False)"
-  "0 \<^bold>\<times> - 1 = - of_bool (False \<^bold>* True)"
-  "- 1 \<^bold>\<times> - 1 = - of_bool (True \<^bold>* True)"
-  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> l \<noteq> - 1
-    \<Longrightarrow> k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
-  by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp)
-
-declare F.simps [simp del]
-
-lemma rec:
-  "k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
-  by (cases "k \<in> {0, - 1} \<and> l \<in> {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split)
-
-sublocale abel_semigroup F
-proof
-  show "k \<^bold>\<times> l \<^bold>\<times> r = k \<^bold>\<times> (l \<^bold>\<times> r)" for k l r :: int
-  proof (induction k arbitrary: l r rule: int_bit_induct)
-    case zero
-    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "False \<^bold>* False" "\<not> False \<^bold>* True"
-    proof (induction l arbitrary: r rule: int_bit_induct)
-      case zero
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case minus
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (even l)
-      with that rec [of _ r] show ?case
-        by (cases "even r")
-          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (odd l)
-      moreover have "- l - 1 = - 1 - l"
-        by simp
-      ultimately show ?case
-        using that rec [of _ r]
-        by (cases "even r")
-          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    qed
-    then show ?case
-      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-  next
-    case minus
-    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "\<not> True \<^bold>* True" "False \<^bold>* True"
-    proof (induction l arbitrary: r rule: int_bit_induct)
-      case zero
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case minus
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (even l)
-      with that rec [of _ r] show ?case
-        by (cases "even r")
-          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (odd l)
-      moreover have "- l - 1 = - 1 - l"
-        by simp
-      ultimately show ?case
-        using that rec [of _ r]
-        by (cases "even r")
-          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    qed
-    then show ?case
-      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-  next
-    case (even k)
-    with rec [of "k * 2"] rec [of _ r] show ?case
-      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
-  next
-    case (odd k)
-    with rec [of "1 + k * 2"] rec [of _ r] show ?case
-      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
-  qed
-  show "k \<^bold>\<times> l = l \<^bold>\<times> k" for k l :: int
-  proof (induction k arbitrary: l rule: int_bit_induct)
-    case zero
-    show ?case
-      by simp
-  next
-    case minus
-    show ?case
-      by simp
-  next
-    case (even k)
-    with rec [of "k * 2" l] rec [of l "k * 2"] show ?case
-  next
-    case (odd k)
-    with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case
-  qed
-qed
-
-lemma self [simp]:
-  "k \<^bold>\<times> k = (case (False \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split)
-
-lemma even_iff [simp]:
-  "even (k \<^bold>\<times> l) \<longleftrightarrow> \<not> (odd k \<^bold>* odd l)"
-proof (induction k arbitrary: l rule: int_bit_induct)
-  case zero
-  show ?case
-    by (cases "even l") (simp_all split: bool.splits)
-next
-  case minus
-  show ?case
-    by (cases "even l") (simp_all split: bool.splits)
-next
-  case (even k)
-  then show ?case
-    by (simp add: rec [of "k * 2"])
-next
-  case (odd k)
-  then show ?case
-    by (simp add: rec [of "1 + k * 2"])
-qed
-
lemma of_bits:
"of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)"
if "length bs = length cs" and "\<not> False \<^bold>* False" for bs cs
@@ -782,265 +351,18 @@

end

-instantiation int :: bit_operations
-begin
-
-definition not_int :: "int \<Rightarrow> int"
-  where "not_int = complement"
-
-global_interpretation and_int: zip_int "(\<and>)"
-  defines and_int = and_int.F
-  by standard
-
-declare and_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation and_int: semilattice "(AND) :: int \<Rightarrow> int \<Rightarrow> int"
-proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard)
-  show "k AND k = k" for k :: int
-qed
-
-lemma zero_int_and_eq [simp]:
-  "0 AND k = 0" for k :: int
-  by simp
-
-lemma and_zero_int_eq [simp]:
-  "k AND 0 = 0" for k :: int
-  by simp
-
-lemma minus_int_and_eq [simp]:
-  "- 1 AND k = k" for k :: int
-  by simp
-
-lemma and_minus_int_eq [simp]:
-  "k AND - 1 = k" for k :: int
-  by simp
-
-global_interpretation or_int: zip_int "(\<or>)"
-  defines or_int = or_int.F
-  by standard
-
-declare or_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation or_int: semilattice "(OR) :: int \<Rightarrow> int \<Rightarrow> int"
-proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard)
-  show "k OR k = k" for k :: int
-qed
-
-lemma zero_int_or_eq [simp]:
-  "0 OR k = k" for k :: int
-  by simp
-
-lemma and_zero_or_eq [simp]:
-  "k OR 0 = k" for k :: int
-  by simp
-
-lemma minus_int_or_eq [simp]:
-  "- 1 OR k = - 1" for k :: int
-  by simp
-
-lemma or_minus_int_eq [simp]:
-  "k OR - 1 = - 1" for k :: int
-  by simp
-
-global_interpretation xor_int: zip_int "(\<noteq>)"
-  defines xor_int = xor_int.F
-  by standard
-
-declare xor_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-lemma zero_int_xor_eq [simp]:
-  "0 XOR k = k" for k :: int
-  by simp
-
-lemma and_zero_xor_eq [simp]:
-  "k XOR 0 = k" for k :: int
-  by simp
-
-lemma minus_int_xor_eq [simp]:
-  "- 1 XOR k = complement k" for k :: int
-  by simp
-
-lemma xor_minus_int_eq [simp]:
-  "k XOR - 1 = complement k" for k :: int
-  by simp
-
-definition shift_left_int :: "int \<Rightarrow> nat \<Rightarrow> int"
-  where [simp]: "k << n = push_bit n k" for k :: int
-
-definition shift_right_int :: "int \<Rightarrow> nat \<Rightarrow> int"
-  where [simp]: "k >> n = drop_bit n k" for k :: int
-
-instance proof
-  show "semilattice ((AND) :: int \<Rightarrow> _)"
-    by (fact and_int.semilattice_axioms)
-  show "semilattice ((OR) :: int \<Rightarrow> _)"
-    by (fact or_int.semilattice_axioms)
-  show "abel_semigroup ((XOR) :: int \<Rightarrow> _)"
-    by (fact xor_int.abel_semigroup_axioms)
+instance int :: ring_bit_representation
+proof
show "(not :: int \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of"
proof (rule sym, rule ext)
fix k :: int
show "(of_bits \<circ> map Not \<circ> bits_of) k = NOT k"
by (induction k rule: int_bit_induct) (simp_all add: not_int_def)
qed
-  show "of_bits bs AND of_bits cs = (of_bits (map2 (\<and>) bs cs) :: int)"
-    if "length bs = length cs" for bs cs
-    using that by (rule and_int.of_bits) simp
-  show "of_bits bs OR of_bits cs = (of_bits (map2 (\<or>) bs cs) :: int)"
-    if "length bs = length cs" for bs cs
-    using that by (rule or_int.of_bits) simp
-  show "of_bits bs XOR of_bits cs = (of_bits (map2 (\<noteq>) bs cs) :: int)"
-    if "length bs = length cs" for bs cs
-    using that by (rule xor_int.of_bits) simp
-  show "k << n = of_bits (replicate n False @ bits_of k)"
+  show "shift_bit n k = of_bits (replicate n False @ bits_of k)"
for k :: int and n :: nat
-    by (cases "n = 0") simp_all
-  show "k >> n = of_bits (drop n (bits_of k))"
-    if "n < length (bits_of k)"
-    for k :: int and n :: nat
-    using that by simp
-qed
+    by (cases "n = 0") (simp_all add: shift_bit_eq_push_bit)
+qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits
+  drop_bit_eq_drop_bit)

end
-
-global_interpretation and_int: semilattice_neutr "(AND)" "- 1 :: int"
-  by standard simp
-
-global_interpretation or_int: semilattice_neutr "(OR)" "0 :: int"
-  by standard simp
-
-global_interpretation xor_int: comm_monoid "(XOR)" "0 :: int"
-  by standard simp
-
-lemma not_int_simps [simp]:
-  "NOT 0 = (- 1 :: int)"
-  "NOT (- 1) = (0 :: int)"
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
-  by (auto simp add: not_int_def elim: oddE)
-
-lemma not_one_int [simp]:
-  "NOT 1 = (- 2 :: int)"
-  by simp
-
-lemma even_not_iff [simp]:
-  "even (NOT k) \<longleftrightarrow> odd k"
-  for k :: int
-
-lemma not_div_2:
-  "NOT k div 2 = NOT (k div 2)"
-  for k :: int
-  by (simp add: complement_div_2 not_int_def)
-
-lemma one_and_int_eq [simp]:
-  "1 AND k = k mod 2" for k :: int
-  using and_int.rec [of 1] by (simp add: mod2_eq_if)
-
-lemma and_one_int_eq [simp]:
-  "k AND 1 = k mod 2" for k :: int
-  using one_and_int_eq [of 1] by (simp add: ac_simps)
-
-lemma one_or_int_eq [simp]:
-  "1 OR k = k + of_bool (even k)" for k :: int
-  using or_int.rec [of 1] by (auto elim: oddE)
-
-lemma or_one_int_eq [simp]:
-  "k OR 1 = k + of_bool (even k)" for k :: int
-  using one_or_int_eq [of k] by (simp add: ac_simps)
-
-lemma one_xor_int_eq [simp]:
-  "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int
-  using xor_int.rec [of 1] by (auto elim: oddE)
-
-lemma xor_one_int_eq [simp]:
-  "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int
-  using one_xor_int_eq [of k] by (simp add: ac_simps)
-
-global_interpretation bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int"
-  rewrites "bit_int.xor = ((XOR) :: int \<Rightarrow> _)"
-proof -
-  interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int"
-  proof
-    show "k AND (l OR r) = k AND l OR k AND r"
-      for k l r :: int
-    proof (induction k arbitrary: l r rule: int_bit_induct)
-      case zero
-      show ?case
-        by simp
-    next
-      case minus
-      show ?case
-        by simp
-    next
-      case (even k)
-      then show ?case by (simp add: and_int.rec [of "k * 2"]
-        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l])
-    next
-      case (odd k)
-      then show ?case by (simp add: and_int.rec [of "1 + k * 2"]
-        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l])
-    qed
-    show "k OR l AND r = (k OR l) AND (k OR r)"
-      for k l r :: int
-    proof (induction k arbitrary: l r rule: int_bit_induct)
-      case zero
-      then show ?case
-        by simp
-    next
-      case minus
-      then show ?case
-        by simp
-    next
-      case (even k)
-      then show ?case by (simp add: or_int.rec [of "k * 2"]
-        and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
-    next
-      case (odd k)
-      then show ?case by (simp add: or_int.rec [of "1 + k * 2"]
-        and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
-    qed
-    show "k AND NOT k = 0" for k :: int
-      by (induction k rule: int_bit_induct)
-        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
-    show "k OR NOT k = - 1" for k :: int
-      by (induction k rule: int_bit_induct)
-        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
-  qed simp_all
-  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)"
-    by (fact bit_int.boolean_algebra_axioms)
-  show "bit_int.xor = ((XOR) :: int \<Rightarrow> _)"
-  proof (rule ext)+
-    fix k l :: int
-    have "k XOR l = k AND NOT l OR NOT k AND l"
-    proof (induction k arbitrary: l rule: int_bit_induct)
-      case zero
-      show ?case
-        by simp
-    next
-      case minus
-      show ?case
-    next
-      case (even k)
-      then show ?case
-        by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"]
-          or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2)
-          (simp add: and_int.rec [of _ l])
-    next
-      case (odd k)
-      then show ?case
-        by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"]
-          or_int.rec [of _ "2 * NOT k AND l"] not_div_2)
-          (simp add: and_int.rec [of _ l])
-    qed
-    then show "bit_int.xor k l = k XOR l"
-  qed
-qed
-
-end```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Mon Nov 04 20:38:15 2019 +0000
@@ -0,0 +1,1033 @@
+(*  Author:  Florian Haftmann, TUM
+*)
+
+section \<open>Proof of concept for purely algebraically founded lists of bits\<close>
+
+theory Bit_Operations
+  imports
+    "HOL-Library.Boolean_Algebra"
+    Word
+begin
+
+hide_const (open) drop_bit take_bit
+
+subsection \<open>Algebraic structures with bits\<close>
+
+class semiring_bits = semiring_parity +
+  assumes bit_split_eq: \<open>\<And>a. of_bool (odd a) + 2 * (a div 2) = a\<close>
+    and bit_eq_rec: \<open>\<And>a b. a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close>
+    and bit_induct [case_names stable rec]:
+    \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
+     \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
+        \<Longrightarrow> P a\<close>
+
+
+subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
+
+instance nat :: semiring_bits
+proof
+  show \<open>of_bool (odd n) + 2 * (n div 2) = n\<close>
+    for n :: nat
+    by simp
+  show \<open>m = n \<longleftrightarrow> (even m \<longleftrightarrow> even n) \<and> m div 2 = n div 2\<close>
+    for m n :: nat
+    by (auto dest: odd_two_times_div_two_succ)
+  show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close>
+    and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close>
+    for P and n :: nat
+  proof (induction n rule: nat_bit_induct)
+    case zero
+    from stable [of 0] show ?case
+      by simp
+  next
+    case (even n)
+    with rec [of n False] show ?case
+      by simp
+  next
+    case (odd n)
+    with rec [of n True] show ?case
+      by simp
+  qed
+qed
+
+
+subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
+
+instance int :: semiring_bits
+proof
+  show \<open>of_bool (odd k) + 2 * (k div 2) = k\<close>
+    for k :: int
+    by (auto elim: oddE)
+  show \<open>k = l \<longleftrightarrow> (even k \<longleftrightarrow> even l) \<and> k div 2 = l div 2\<close>
+    for k l :: int
+    by (auto dest: odd_two_times_div_two_succ)
+  show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close>
+    and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close>
+    for P and k :: int
+  proof (induction k rule: int_bit_induct)
+    case zero
+    from stable [of 0] show ?case
+      by simp
+  next
+    case minus
+    from stable [of \<open>- 1\<close>] show ?case
+      by simp
+  next
+    case (even k)
+    with rec [of k False] show ?case
+  next
+    case (odd k)
+    with rec [of k True] show ?case
+  qed
+qed
+
+
+subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
+
+instance word :: (len) semiring_bits
+proof
+  show \<open>of_bool (odd a) + 2 * (a div 2) = a\<close>
+    for a :: \<open>'a word\<close>
+    apply (cases \<open>even a\<close>; simp, transfer; cases rule: length_cases [where ?'a = 'a])
+      apply auto
+    apply (auto simp add: take_bit_eq_mod)
+    apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod)
+    done
+  show \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
+    for a b :: \<open>'a word\<close>
+    apply transfer
+    apply (cases rule: length_cases [where ?'a = 'a])
+     apply auto
+       apply (metis even_take_bit_eq len_not_eq_0)
+      apply (metis even_take_bit_eq len_not_eq_0)
+    apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod)
+    done
+  show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
+    and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
+  for P and a :: \<open>'a word\<close>
+  proof (induction a rule: word_bit_induct)
+    case zero
+    from stable [of 0] show ?case
+      by simp
+  next
+    case (even a)
+    with rec [of a False] show ?case
+      using bit_word_half_eq [of a False] by (simp add: ac_simps)
+  next
+    case (odd a)
+    with rec [of a True] show ?case
+      using bit_word_half_eq [of a True] by (simp add: ac_simps)
+  qed
+qed
+
+
+subsection \<open>Bit shifts in suitable algebraic structures\<close>
+
+class semiring_bit_shifts = semiring_bits +
+  fixes shift_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  assumes shift_bit_eq_mult: \<open>shift_bit n a = a * 2 ^ n\<close>
+  fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
+begin
+
+definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
+
+text \<open>
+  Logically, \<^const>\<open>shift_bit\<close>,
+  \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
+  as separate operations makes proofs easier, otherwise proof automation
+  would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
+  algebraic relationships between those operations; having
+  \<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations
+  takes into account that specific instances of these can be implemented
+  differently wrt. code generation.
+\<close>
+
+end
+
+subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
+
+instantiation nat :: semiring_bit_shifts
+begin
+
+definition shift_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>shift_bit_nat n m = m * 2 ^ n\<close>
+
+definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
+
+instance proof
+  show \<open>shift_bit n m = m * 2 ^ n\<close> for n m :: nat
+  show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat
+qed
+
+end
+
+
+subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
+
+instantiation int :: semiring_bit_shifts
+begin
+
+definition shift_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>shift_bit_int n k = k * 2 ^ n\<close>
+
+definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>drop_bit_int n k = k div 2 ^ n\<close>
+
+instance proof
+  show \<open>shift_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int
+  show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int
+qed
+
+end
+
+lemma shift_bit_eq_push_bit:
+  \<open>shift_bit = (push_bit :: nat \<Rightarrow> int \<Rightarrow> int)\<close>
+  by (simp add: fun_eq_iff push_bit_eq_mult shift_bit_eq_mult)
+
+lemma drop_bit_eq_drop_bit:
+  \<open>drop_bit = (Parity.drop_bit :: nat \<Rightarrow> int \<Rightarrow> int)\<close>
+  by (simp add: fun_eq_iff drop_bit_eq_div Parity.drop_bit_eq_div)
+
+lemma take_bit_eq_take_bit:
+  \<open>take_bit = (Parity.take_bit :: nat \<Rightarrow> int \<Rightarrow> int)\<close>
+  by (simp add: fun_eq_iff take_bit_eq_mod Parity.take_bit_eq_mod)
+
+
+subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
+
+instantiation word :: (len) semiring_bit_shifts
+begin
+
+lift_definition shift_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is shift_bit
+proof -
+  show \<open>Parity.take_bit LENGTH('a) (shift_bit n k) = Parity.take_bit LENGTH('a) (shift_bit n l)\<close>
+    if \<open>Parity.take_bit LENGTH('a) k = Parity.take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
+  proof -
+    from that
+    have \<open>Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) k)
+      = Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) l)\<close>
+      by simp
+    moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
+      by simp
+    ultimately show ?thesis
+      by (simp add: shift_bit_eq_push_bit take_bit_push_bit)
+  qed
+qed
+
+lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
+  by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod)
+
+instance proof
+  show \<open>shift_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
+    by transfer (simp add: shift_bit_eq_mult)
+  show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
+  proof (cases \<open>n < LENGTH('a)\<close>)
+    case True
+    then show ?thesis
+      by transfer
+        (simp add: Parity.take_bit_eq_mod take_bit_eq_mod drop_bit_eq_div)
+  next
+    case False
+    then obtain m where n: \<open>n = LENGTH('a) + m\<close>
+      by (auto simp add: not_less dest: le_Suc_ex)
+    then show ?thesis
+      by transfer
+  qed
+qed
+
+end
+
+
+subsection \<open>Bit operations in suitable algebraic structures\<close>
+
+class semiring_bit_operations = semiring_bit_shifts +
+  fixes "and" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
+    and or :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
+    and xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
+begin
+
+text \<open>
+  We want the bitwise operations to bind slightly weaker
+  than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
+  bind slightly stronger than \<open>*\<close>.
+  For the sake of code generation
+  the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close>
+  are specified as definitional class operations.
+
+\<close>
+
+definition bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
+  where \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
+
+definition map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>map_bit n f a = take_bit n a + shift_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\<close>
+
+definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>set_bit n = map_bit n top\<close>
+
+definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>unset_bit n = map_bit n bot\<close>
+
+definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>flip_bit n = map_bit n Not\<close>
+
+text \<open>
+  The logical core are \<^const>\<open>bit\<close> and \<^const>\<open>map_bit\<close>; having
+  <^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
+  operations allows to implement them using bit masks later.
+\<close>
+
+end
+
+class ring_bit_operations = semiring_bit_operations + ring_parity +
+  fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
+  assumes boolean_algebra: \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
+    and boolean_algebra_xor_eq: \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
+begin
+
+sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
+  rewrites \<open>bit.xor = (XOR)\<close>
+proof -
+  interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
+    by (fact boolean_algebra)
+  show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
+    by standard
+  show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
+    by (fact boolean_algebra_xor_eq)
+qed
+
+text \<open>
+  For the sake of code generation \<^const>\<open>not\<close> is specified as
+  definitional class operation.  Note that \<^const>\<open>not\<close> has no
+  sensible definition for unlimited but only positive bit strings
+  (type \<^typ>\<open>nat\<close>).
+\<close>
+
+end
+
+
+subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
+
+locale zip_nat = single: abel_semigroup f
+    for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70) +
+  assumes end_of_bits: "\<not> False \<^bold>* False"
+begin
+
+lemma False_P_imp:
+  "False \<^bold>* True \<and> P" if "False \<^bold>* P"
+  using that end_of_bits by (cases P) simp_all
+
+function F :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infixl "\<^bold>\<times>" 70)
+  where "m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
+    else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2)"
+  by auto
+
+termination
+  by (relation "measure (case_prod (+))") auto
+
+lemma zero_left_eq:
+  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
+  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
+
+lemma zero_right_eq:
+  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
+  by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits)
+
+lemma simps [simp]:
+  "0 \<^bold>\<times> 0 = 0"
+  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
+  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
+  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
+  by (simp_all only: zero_left_eq zero_right_eq) simp
+
+lemma rec:
+  "m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
+  by (cases "m = 0 \<and> n = 0") (auto simp add: end_of_bits)
+
+declare F.simps [simp del]
+
+sublocale abel_semigroup F
+proof
+  show "m \<^bold>\<times> n \<^bold>\<times> q = m \<^bold>\<times> (n \<^bold>\<times> q)" for m n q :: nat
+  proof (induction m arbitrary: n q rule: nat_bit_induct)
+    case zero
+    show ?case
+      by simp
+  next
+    case (even m)
+    with rec [of "2 * m"] rec [of _ q] show ?case
+      by (cases "even n") (auto dest: False_P_imp)
+  next
+    case (odd m)
+    with rec [of "Suc (2 * m)"] rec [of _ q] show ?case
+      by (cases "even n"; cases "even q")
+        (auto dest: False_P_imp simp add: ac_simps)
+  qed
+  show "m \<^bold>\<times> n = n \<^bold>\<times> m" for m n :: nat
+  proof (induction m arbitrary: n rule: nat_bit_induct)
+    case zero
+    show ?case
+  next
+    case (even m)
+    with rec [of "2 * m" n] rec [of n "2 * m"] show ?case
+  next
+    case (odd m)
+    with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case
+  qed
+qed
+
+lemma self [simp]:
+  "n \<^bold>\<times> n = of_bool (True \<^bold>* True) * n"
+  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
+
+lemma even_iff [simp]:
+  "even (m \<^bold>\<times> n) \<longleftrightarrow> \<not> (odd m \<^bold>* odd n)"
+proof (induction m arbitrary: n rule: nat_bit_induct)
+  case zero
+  show ?case
+    by (cases "even n") (simp_all add: end_of_bits)
+next
+  case (even m)
+  then show ?case
+    by (simp add: rec [of "2 * m"])
+next
+  case (odd m)
+  then show ?case
+    by (simp add: rec [of "Suc (2 * m)"])
+qed
+
+end
+
+instantiation nat :: semiring_bit_operations
+begin
+
+global_interpretation and_nat: zip_nat "(\<and>)"
+  defines and_nat = and_nat.F
+  by standard auto
+
+global_interpretation and_nat: semilattice "(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard)
+  show "n AND n = n" for n :: nat
+qed
+
+declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
+  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+
+lemma zero_nat_and_eq [simp]:
+  "0 AND n = 0" for n :: nat
+  by simp
+
+lemma and_zero_nat_eq [simp]:
+  "n AND 0 = 0" for n :: nat
+  by simp
+
+global_interpretation or_nat: zip_nat "(\<or>)"
+  defines or_nat = or_nat.F
+  by standard auto
+
+global_interpretation or_nat: semilattice "(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard)
+  show "n OR n = n" for n :: nat
+qed
+
+declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
+  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+
+lemma zero_nat_or_eq [simp]:
+  "0 OR n = n" for n :: nat
+  by simp
+
+lemma or_zero_nat_eq [simp]:
+  "n OR 0 = n" for n :: nat
+  by simp
+
+global_interpretation xor_nat: zip_nat "(\<noteq>)"
+  defines xor_nat = xor_nat.F
+  by standard auto
+
+declare xor_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
+  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+
+lemma zero_nat_xor_eq [simp]:
+  "0 XOR n = n" for n :: nat
+  by simp
+
+lemma xor_zero_nat_eq [simp]:
+  "n XOR 0 = n" for n :: nat
+  by simp
+
+instance ..
+
+end
+
+global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat"
+  by standard simp
+
+global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat"
+  by standard simp
+
+lemma Suc_0_and_eq [simp]:
+  "Suc 0 AND n = n mod 2"
+  by (cases n) auto
+
+lemma and_Suc_0_eq [simp]:
+  "n AND Suc 0 = n mod 2"
+  using Suc_0_and_eq [of n] by (simp add: ac_simps)
+
+lemma Suc_0_or_eq [simp]:
+  "Suc 0 OR n = n + of_bool (even n)"
+  by (cases n) (simp_all add: ac_simps)
+
+lemma or_Suc_0_eq [simp]:
+  "n OR Suc 0 = n + of_bool (even n)"
+  using Suc_0_or_eq [of n] by (simp add: ac_simps)
+
+lemma Suc_0_xor_eq [simp]:
+  "Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)"
+  by (cases n) (simp_all add: ac_simps)
+
+lemma xor_Suc_0_eq [simp]:
+  "n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)"
+  using Suc_0_xor_eq [of n] by (simp add: ac_simps)
+
+
+subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
+
+abbreviation (input) complement :: "int \<Rightarrow> int"
+  where "complement k \<equiv> - k - 1"
+
+lemma complement_half:
+  "complement (k * 2) div 2 = complement k"
+  by simp
+
+lemma complement_div_2:
+  "complement (k div 2) = complement k div 2"
+  by linarith
+
+locale zip_int = single: abel_semigroup f
+  for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70)
+begin
+
+lemma False_False_imp_True_True:
+  "True \<^bold>* True" if "False \<^bold>* False"
+proof (rule ccontr)
+  assume "\<not> True \<^bold>* True"
+  with that show False
+    using single.assoc [of False True True]
+    by (cases "False \<^bold>* True") simp_all
+qed
+
+function F :: "int \<Rightarrow> int \<Rightarrow> int"  (infixl "\<^bold>\<times>" 70)
+  where "k \<^bold>\<times> l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
+    then - of_bool (odd k \<^bold>* odd l)
+    else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2)"
+  by auto
+
+termination
+  by (relation "measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))") auto
+
+lemma zero_left_eq:
+  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> l
+     | (True, False) \<Rightarrow> complement l
+     | (True, True) \<Rightarrow> - 1)"
+  by (induction l rule: int_bit_induct)
+   (simp_all split: bool.split)
+
+lemma minus_left_eq:
+  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> l
+     | (True, False) \<Rightarrow> complement l
+     | (True, True) \<Rightarrow> - 1)"
+  by (induction l rule: int_bit_induct)
+   (simp_all split: bool.split)
+
+lemma zero_right_eq:
+  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> k
+     | (True, False) \<Rightarrow> complement k
+     | (True, True) \<Rightarrow> - 1)"
+  by (induction k rule: int_bit_induct)
+    (simp_all add: ac_simps split: bool.split)
+
+lemma minus_right_eq:
+  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> k
+     | (True, False) \<Rightarrow> complement k
+     | (True, True) \<Rightarrow> - 1)"
+  by (induction k rule: int_bit_induct)
+    (simp_all add: ac_simps split: bool.split)
+
+lemma simps [simp]:
+  "0 \<^bold>\<times> 0 = - of_bool (False \<^bold>* False)"
+  "- 1 \<^bold>\<times> 0 = - of_bool (True \<^bold>* False)"
+  "0 \<^bold>\<times> - 1 = - of_bool (False \<^bold>* True)"
+  "- 1 \<^bold>\<times> - 1 = - of_bool (True \<^bold>* True)"
+  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> l
+     | (True, False) \<Rightarrow> complement l
+     | (True, True) \<Rightarrow> - 1)"
+  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> l
+     | (True, False) \<Rightarrow> complement l
+     | (True, True) \<Rightarrow> - 1)"
+  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> k
+     | (True, False) \<Rightarrow> complement k
+     | (True, True) \<Rightarrow> - 1)"
+  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> k
+     | (True, False) \<Rightarrow> complement k
+     | (True, True) \<Rightarrow> - 1)"
+  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> l \<noteq> - 1
+    \<Longrightarrow> k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
+  by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp)
+
+declare F.simps [simp del]
+
+lemma rec:
+  "k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
+  by (cases "k \<in> {0, - 1} \<and> l \<in> {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split)
+
+sublocale abel_semigroup F
+proof
+  show "k \<^bold>\<times> l \<^bold>\<times> r = k \<^bold>\<times> (l \<^bold>\<times> r)" for k l r :: int
+  proof (induction k arbitrary: l r rule: int_bit_induct)
+    case zero
+    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "False \<^bold>* False" "\<not> False \<^bold>* True"
+    proof (induction l arbitrary: r rule: int_bit_induct)
+      case zero
+      from that show ?case
+        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+    next
+      case minus
+      from that show ?case
+        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+    next
+      case (even l)
+      with that rec [of _ r] show ?case
+        by (cases "even r")
+          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
+    next
+      case (odd l)
+      moreover have "- l - 1 = - 1 - l"
+        by simp
+      ultimately show ?case
+        using that rec [of _ r]
+        by (cases "even r")
+          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+    qed
+    then show ?case
+      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+  next
+    case minus
+    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "\<not> True \<^bold>* True" "False \<^bold>* True"
+    proof (induction l arbitrary: r rule: int_bit_induct)
+      case zero
+      from that show ?case
+        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+    next
+      case minus
+      from that show ?case
+        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+    next
+      case (even l)
+      with that rec [of _ r] show ?case
+        by (cases "even r")
+          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
+    next
+      case (odd l)
+      moreover have "- l - 1 = - 1 - l"
+        by simp
+      ultimately show ?case
+        using that rec [of _ r]
+        by (cases "even r")
+          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+    qed
+    then show ?case
+      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
+  next
+    case (even k)
+    with rec [of "k * 2"] rec [of _ r] show ?case
+      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
+  next
+    case (odd k)
+    with rec [of "1 + k * 2"] rec [of _ r] show ?case
+      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
+  qed
+  show "k \<^bold>\<times> l = l \<^bold>\<times> k" for k l :: int
+  proof (induction k arbitrary: l rule: int_bit_induct)
+    case zero
+    show ?case
+      by simp
+  next
+    case minus
+    show ?case
+      by simp
+  next
+    case (even k)
+    with rec [of "k * 2" l] rec [of l "k * 2"] show ?case
+  next
+    case (odd k)
+    with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case
+  qed
+qed
+
+lemma self [simp]:
+  "k \<^bold>\<times> k = (case (False \<^bold>* False, True \<^bold>* True)
+    of (False, False) \<Rightarrow> 0
+     | (False, True) \<Rightarrow> k
+     | (True, True) \<Rightarrow> - 1)"
+  by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split)
+
+lemma even_iff [simp]:
+  "even (k \<^bold>\<times> l) \<longleftrightarrow> \<not> (odd k \<^bold>* odd l)"
+proof (induction k arbitrary: l rule: int_bit_induct)
+  case zero
+  show ?case
+    by (cases "even l") (simp_all split: bool.splits)
+next
+  case minus
+  show ?case
+    by (cases "even l") (simp_all split: bool.splits)
+next
+  case (even k)
+  then show ?case
+    by (simp add: rec [of "k * 2"])
+next
+  case (odd k)
+  then show ?case
+    by (simp add: rec [of "1 + k * 2"])
+qed
+
+end
+
+instantiation int :: ring_bit_operations
+begin
+
+definition not_int :: "int \<Rightarrow> int"
+  where "not_int = complement"
+
+global_interpretation and_int: zip_int "(\<and>)"
+  defines and_int = and_int.F
+  by standard
+
+declare and_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
+  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+
+global_interpretation and_int: semilattice "(AND) :: int \<Rightarrow> int \<Rightarrow> int"
+proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard)
+  show "k AND k = k" for k :: int
+qed
+
+lemma zero_int_and_eq [simp]:
+  "0 AND k = 0" for k :: int
+  by simp
+
+lemma and_zero_int_eq [simp]:
+  "k AND 0 = 0" for k :: int
+  by simp
+
+lemma minus_int_and_eq [simp]:
+  "- 1 AND k = k" for k :: int
+  by simp
+
+lemma and_minus_int_eq [simp]:
+  "k AND - 1 = k" for k :: int
+  by simp
+
+global_interpretation or_int: zip_int "(\<or>)"
+  defines or_int = or_int.F
+  by standard
+
+declare or_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
+  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+
+global_interpretation or_int: semilattice "(OR) :: int \<Rightarrow> int \<Rightarrow> int"
+proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard)
+  show "k OR k = k" for k :: int
+qed
+
+lemma zero_int_or_eq [simp]:
+  "0 OR k = k" for k :: int
+  by simp
+
+lemma and_zero_or_eq [simp]:
+  "k OR 0 = k" for k :: int
+  by simp
+
+lemma minus_int_or_eq [simp]:
+  "- 1 OR k = - 1" for k :: int
+  by simp
+
+lemma or_minus_int_eq [simp]:
+  "k OR - 1 = - 1" for k :: int
+  by simp
+
+global_interpretation xor_int: zip_int "(\<noteq>)"
+  defines xor_int = xor_int.F
+  by standard
+
+declare xor_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
+  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+
+lemma zero_int_xor_eq [simp]:
+  "0 XOR k = k" for k :: int
+  by simp
+
+lemma and_zero_xor_eq [simp]:
+  "k XOR 0 = k" for k :: int
+  by simp
+
+lemma minus_int_xor_eq [simp]:
+  "- 1 XOR k = complement k" for k :: int
+  by simp
+
+lemma xor_minus_int_eq [simp]:
+  "k XOR - 1 = complement k" for k :: int
+  by simp
+
+lemma not_div_2:
+  "NOT k div 2 = NOT (k div 2)"
+  for k :: int
+  by (simp add: complement_div_2 not_int_def)
+
+lemma not_int_simps [simp]:
+  "NOT 0 = (- 1 :: int)"
+  "NOT (- 1) = (0 :: int)"
+  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+  by (auto simp add: not_int_def elim: oddE)
+
+lemma not_one_int [simp]:
+  "NOT 1 = (- 2 :: int)"
+  by simp
+
+lemma even_not_iff [simp]:
+  "even (NOT k) \<longleftrightarrow> odd k"
+  for k :: int
+
+instance proof
+  interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int"
+  proof
+    show "k AND (l OR r) = k AND l OR k AND r"
+      for k l r :: int
+    proof (induction k arbitrary: l r rule: int_bit_induct)
+      case zero
+      show ?case
+        by simp
+    next
+      case minus
+      show ?case
+        by simp
+    next
+      case (even k)
+      then show ?case by (simp add: and_int.rec [of "k * 2"]
+        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l])
+    next
+      case (odd k)
+      then show ?case by (simp add: and_int.rec [of "1 + k * 2"]
+        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l])
+    qed
+    show "k OR l AND r = (k OR l) AND (k OR r)"
+      for k l r :: int
+    proof (induction k arbitrary: l r rule: int_bit_induct)
+      case zero
+      then show ?case
+        by simp
+    next
+      case minus
+      then show ?case
+        by simp
+    next
+      case (even k)
+      then show ?case by (simp add: or_int.rec [of "k * 2"]
+        and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
+    next
+      case (odd k)
+      then show ?case by (simp add: or_int.rec [of "1 + k * 2"]
+        and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
+    qed
+    show "k AND NOT k = 0" for k :: int
+      by (induction k rule: int_bit_induct)
+        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
+    show "k OR NOT k = - 1" for k :: int
+      by (induction k rule: int_bit_induct)
+        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
+  qed (simp_all add: and_int.assoc or_int.assoc,
+  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)"
+    by (fact bit_int.boolean_algebra_axioms)
+  show "bit_int.xor = ((XOR) :: int \<Rightarrow> _)"
+  proof (rule ext)+
+    fix k l :: int
+    have "k XOR l = k AND NOT l OR NOT k AND l"
+    proof (induction k arbitrary: l rule: int_bit_induct)
+      case zero
+      show ?case
+        by simp
+    next
+      case minus
+      show ?case
+    next
+      case (even k)
+      then show ?case
+        by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"]
+          or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2)
+          (simp add: and_int.rec [of _ l])
+    next
+      case (odd k)
+      then show ?case
+        by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"]
+          or_int.rec [of _ "2 * NOT k AND l"] not_div_2)
+          (simp add: and_int.rec [of _ l])
+    qed
+    then show "bit_int.xor k l = k XOR l"
+  qed
+qed
+
+end
+
+lemma one_and_int_eq [simp]:
+  "1 AND k = k mod 2" for k :: int
+  using and_int.rec [of 1] by (simp add: mod2_eq_if)
+
+lemma and_one_int_eq [simp]:
+  "k AND 1 = k mod 2" for k :: int
+  using one_and_int_eq [of 1] by (simp add: ac_simps)
+
+lemma one_or_int_eq [simp]:
+  "1 OR k = k + of_bool (even k)" for k :: int
+  using or_int.rec [of 1] by (auto elim: oddE)
+
+lemma or_one_int_eq [simp]:
+  "k OR 1 = k + of_bool (even k)" for k :: int
+  using one_or_int_eq [of k] by (simp add: ac_simps)
+
+lemma one_xor_int_eq [simp]:
+  "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int
+  using xor_int.rec [of 1] by (auto elim: oddE)
+
+lemma xor_one_int_eq [simp]:
+  "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int
+  using one_xor_int_eq [of k] by (simp add: ac_simps)
+
+lemma take_bit_complement_iff:
+  "Parity.take_bit n (complement k) = Parity.take_bit n (complement l) \<longleftrightarrow> Parity.take_bit n k = Parity.take_bit n l"
+  for k l :: int
+  by (simp add: Parity.take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute)
+
+lemma take_bit_not_iff:
+  "Parity.take_bit n (NOT k) = Parity.take_bit n (NOT l) \<longleftrightarrow> Parity.take_bit n k = Parity.take_bit n l"
+  for k l :: int
+  by (simp add: not_int_def take_bit_complement_iff)
+
+lemma take_bit_and [simp]:
+  "Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l"
+  for k l :: int
+  apply (induction n arbitrary: k l)
+   apply simp
+  apply (subst and_int.rec)
+  apply (subst (2) and_int.rec)
+  apply simp
+  done
+
+lemma take_bit_or [simp]:
+  "Parity.take_bit n (k OR l) = Parity.take_bit n k OR Parity.take_bit n l"
+  for k l :: int
+  apply (induction n arbitrary: k l)
+   apply simp
+  apply (subst or_int.rec)
+  apply (subst (2) or_int.rec)
+  apply simp
+  done
+
+lemma take_bit_xor [simp]:
+  "Parity.take_bit n (k XOR l) = Parity.take_bit n k XOR Parity.take_bit n l"
+  for k l :: int
+  apply (induction n arbitrary: k l)
+   apply simp
+  apply (subst xor_int.rec)
+  apply (subst (2) xor_int.rec)
+  apply simp
+  done
+
+
+subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
+
+instantiation word :: (len) ring_bit_operations
+begin
+
+lift_definition not_word :: "'a word \<Rightarrow> 'a word"
+  is not
+
+lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "and"
+  by simp
+
+lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is or
+  by simp
+
+lift_definition xor_word ::  "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is xor
+  by simp
+
+instance proof
+  interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word"
+  proof
+    show "a AND (b OR c) = a AND b OR a AND c"
+      for a b c :: "'a word"
+      by transfer (simp add: bit.conj_disj_distrib)
+    show "a OR b AND c = (a OR b) AND (a OR c)"
+      for a b c :: "'a word"
+      by transfer (simp add: bit.disj_conj_distrib)
+  qed (transfer; simp add: ac_simps)+
+  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)"
+    by (fact bit_word.boolean_algebra_axioms)
+  show "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
+  proof (rule ext)+
+    fix a b :: "'a word"
+    have "a XOR b = a AND NOT b OR NOT a AND b"
+      by transfer (simp add: bit.xor_def)
+    then show "bit_word.xor a b = a XOR b"
+  qed
+qed
+
+end
+
+end```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Word.thy	Mon Nov 04 20:38:15 2019 +0000
@@ -0,0 +1,574 @@
+(*  Author:  Florian Haftmann, TUM
+*)
+
+section \<open>Proof of concept for algebraically founded bit word types\<close>
+
+theory Word
+  imports
+    Main
+    "HOL-Library.Type_Length"
+begin
+
+subsection \<open>Preliminaries\<close>
+
+begin
+
+lemma minus_diff_commute:
+  "- b - a = - a - b"
+
+end
+
+lemma take_bit_uminus:
+  "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:
+  "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]:
+  "take_bit n k \<ge> 0" for k :: int
+
+definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
+  where signed_take_bit_eq_take_bit:
+    "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
+
+lemma 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)"
+proof (cases "even k")
+  case True
+  then have "odd (k + 1)"
+    by simp
+  then have "(k + 1) mod 2 = 1"
+  with True show ?thesis
+next
+  case False
+  then show ?thesis
+    by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one)
+qed
+
+lemma signed_take_bit_Suc [simp]:
+  "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
+  by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps)
+
+lemma signed_take_bit_of_0 [simp]:
+  "signed_take_bit n 0 = 0"
+  by (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod)
+
+lemma signed_take_bit_of_minus_1 [simp]:
+  "signed_take_bit n (- 1) = - 1"
+  by (induct n) simp_all
+
+lemma signed_take_bit_eq_iff_take_bit_eq:
+  "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 that obtain m where m: "n = Suc m"
+    by (cases n) auto
+  show ?thesis
+  proof
+    assume ?Q
+    have "take_bit (Suc m) (k + 2 ^ m) =
+      take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))"
+    also have "\<dots> =
+      take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))"
+      by (simp only: \<open>?Q\<close> m [symmetric])
+    also have "\<dots> = take_bit (Suc m) (l + 2 ^ m)"
+    finally show ?P
+      by (simp only: signed_take_bit_eq_take_bit m) simp
+  next
+    assume ?P
+    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
+    then have "k mod 2 ^ n = l mod 2 ^ n"
+    then show ?Q
+  qed
+qed
+
+
+subsection \<open>Bit strings as quotient type\<close>
+
+subsubsection \<open>Basic properties\<close>
+
+quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l"
+  by (auto intro!: equivpI reflpI sympI transpI)
+
+instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
+begin
+
+lift_definition zero_word :: "'a word"
+  is 0
+  .
+
+lift_definition one_word :: "'a word"
+  is 1
+  .
+
+lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is plus
+
+lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
+  is uminus
+  by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus)
+
+lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is minus
+  by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus)
+
+lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is times
+  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
+
+instance
+  by standard (transfer; simp add: algebra_simps)+
+
+end
+
+instance word :: (len) comm_ring_1
+  by standard (transfer; simp)+
+
+quickcheck_generator word
+  constructors:
+    "zero_class.zero :: ('a::len0) word",
+    "numeral :: num \<Rightarrow> ('a::len0) word",
+    "uminus :: ('a::len0) word \<Rightarrow> ('a::len0) word"
+
+context
+  includes lifting_syntax
+  notes power_transfer [transfer_rule]
+begin
+
+lemma power_transfer_word [transfer_rule]:
+  \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
+  by transfer_prover
+
+end
+
+
+subsubsection \<open>Conversions\<close>
+
+context
+  includes lifting_syntax
+  notes transfer_rule_numeral [transfer_rule]
+    transfer_rule_of_nat [transfer_rule]
+    transfer_rule_of_int [transfer_rule]
+begin
+
+lemma [transfer_rule]:
+  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
+  by transfer_prover
+
+lemma [transfer_rule]:
+  "((=) ===> pcr_word) int of_nat"
+  by transfer_prover
+
+lemma [transfer_rule]:
+  "((=) ===> pcr_word) (\<lambda>k. k) of_int"
+proof -
+  have "((=) ===> pcr_word) of_int of_int"
+    by transfer_prover
+  then show ?thesis by (simp add: id_def)
+qed
+
+end
+
+lemma abs_word_eq:
+  "abs_word = of_int"
+  by (rule ext) (transfer, rule)
+
+context semiring_1
+begin
+
+lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
+  is "of_nat \<circ> nat \<circ> take_bit LENGTH('b)"
+  by simp
+
+lemma unsigned_0 [simp]:
+  "unsigned 0 = 0"
+  by transfer simp
+
+end
+
+context semiring_char_0
+begin
+
+lemma word_eq_iff_unsigned:
+  "a = b \<longleftrightarrow> unsigned a = unsigned b"
+  by safe (transfer; simp add: eq_nat_nat_iff)
+
+end
+
+instantiation word :: (len0) equal
+begin
+
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+  where "equal_word a b \<longleftrightarrow> (unsigned a :: int) = unsigned b"
+
+instance proof
+  fix a b :: "'a word"
+  show "HOL.equal a b \<longleftrightarrow> a = b"
+    using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def)
+qed
+
+end
+
+context ring_1
+begin
+
+lift_definition signed :: "'b::len word \<Rightarrow> 'a"
+  is "of_int \<circ> signed_take_bit (LENGTH('b) - 1)"
+  by (simp add: signed_take_bit_eq_iff_take_bit_eq [symmetric])
+
+lemma signed_0 [simp]:
+  "signed 0 = 0"
+  by transfer simp
+
+end
+
+lemma unsigned_of_nat [simp]:
+  "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n"
+  by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int)
+
+lemma of_nat_unsigned [simp]:
+  "of_nat (unsigned a) = a"
+  by transfer simp
+
+lemma of_int_unsigned [simp]:
+  "of_int (unsigned a) = a"
+  by transfer simp
+
+lemma unsigned_nat_less:
+  \<open>unsigned a < (2 ^ LENGTH('a) :: nat)\<close> for a :: \<open>'a::len0 word\<close>
+  by transfer (simp add: take_bit_eq_mod)
+
+lemma unsigned_int_less:
+  \<open>unsigned a < (2 ^ LENGTH('a) :: int)\<close> for a :: \<open>'a::len0 word\<close>
+  by transfer (simp add: take_bit_eq_mod)
+
+context ring_char_0
+begin
+
+lemma word_eq_iff_signed:
+  "a = b \<longleftrightarrow> signed a = signed b"
+  by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq)
+
+end
+
+lemma signed_of_int [simp]:
+  "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k"
+  by transfer simp
+
+lemma of_int_signed [simp]:
+  "of_int (signed a) = a"
+  by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps)
+
+
+subsubsection \<open>Properties\<close>
+
+lemma length_cases:
+  obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)"
+    | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)"
+proof (cases "LENGTH('a) \<ge> 2")
+  case False
+  then have "LENGTH('a) = 1"
+    by (auto simp add: not_le dest: less_2_cases)
+  then have "take_bit LENGTH('a) 2 = (0 :: int)"
+    by simp
+  with \<open>LENGTH('a) = 1\<close> triv show ?thesis
+    by simp
+next
+  case True
+  then obtain n where "LENGTH('a) = Suc (Suc n)"
+    by (auto dest: le_Suc_ex)
+  then have "take_bit LENGTH('a) 2 = (2 :: int)"
+    by simp
+  with take_bit_2 show ?thesis
+    by simp
+qed
+
+
+subsubsection \<open>Division\<close>
+
+instantiation word :: (len0) modulo
+begin
+
+lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b"
+  by simp
+
+lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b"
+  by simp
+
+instance ..
+
+end
+
+lemma zero_word_div_eq [simp]:
+  \<open>0 div a = 0\<close> for a :: \<open>'a::len0 word\<close>
+  by transfer simp
+
+lemma div_zero_word_eq [simp]:
+  \<open>a div 0 = 0\<close> for a :: \<open>'a::len0 word\<close>
+  by transfer simp
+
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  "(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
+proof -
+  have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
+    for k :: int
+  proof
+    assume ?P
+    then show ?Q
+      by auto
+  next
+    assume ?Q
+    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
+    then have "even (take_bit LENGTH('a) k)"
+      by simp
+    then show ?P
+      by simp
+  qed
+  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
+    transfer_prover
+qed
+
+end
+
+instance word :: (len) semiring_modulo
+proof
+  show "a div b * b + a mod b = a" for a b :: "'a word"
+  proof transfer
+    fix k l :: int
+    define r :: int where "r = 2 ^ LENGTH('a)"
+    then have r: "take_bit LENGTH('a) k = k mod r" for k
+    have "k mod r = ((k mod r) div (l mod r) * (l mod r)
+      + (k mod r) mod (l mod r)) mod r"
+    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
+      + (k mod r) mod (l mod r)) mod r"
+    also have "... = (((k mod r) div (l mod r) * l) mod r
+      + (k mod r) mod (l mod r)) mod r"
+    finally have "k mod r = ((k mod r) div (l mod r) * l
+      + (k mod r) mod (l mod r)) mod r"
+    with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
+      + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
+      by simp
+  qed
+qed
+
+instance word :: (len) semiring_parity
+proof
+  show "\<not> 2 dvd (1::'a word)"
+    by transfer simp
+  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
+    for a :: "'a word"
+    by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
+  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
+    for a :: "'a word"
+    by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
+qed
+
+
+subsubsection \<open>Orderings\<close>
+
+instantiation word :: (len0) linorder
+begin
+
+lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+  is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b"
+  by simp
+
+lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+  is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b"
+  by simp
+
+instance
+  by standard (transfer; auto)+
+
+end
+
+context linordered_semidom
+begin
+
+lemma word_less_eq_iff_unsigned:
+  "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
+  by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
+
+lemma word_less_iff_unsigned:
+  "a < b \<longleftrightarrow> unsigned a < unsigned b"
+  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
+
+end
+
+lemma word_greater_zero_iff:
+  \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len0 word\<close>
+  by transfer (simp add: less_le)
+
+lemma of_nat_word_eq_iff:
+  \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
+  by transfer (simp add: take_bit_of_nat)
+
+lemma of_nat_word_less_eq_iff:
+  \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close>
+  by transfer (simp add: take_bit_of_nat)
+
+lemma of_nat_word_less_iff:
+  \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close>
+  by transfer (simp add: take_bit_of_nat)
+
+lemma of_nat_word_eq_0_iff:
+  \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
+  using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
+
+lemma of_int_word_eq_iff:
+  \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+  by transfer rule
+
+lemma of_int_word_less_eq_iff:
+  \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
+  by transfer rule
+
+lemma of_int_word_less_iff:
+  \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
+  by transfer rule
+
+lemma of_int_word_eq_0_iff:
+  \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
+  using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
+
+
+subsection \<open>Bit structure on \<^typ>\<open>'a word\<close>\<close>
+
+lemma word_bit_induct [case_names zero even odd]:
+  \<open>P a\<close> if word_zero: \<open>P 0\<close>
+    and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close>
+    and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (1 + 2 * a)\<close>
+  for P and a :: \<open>'a::len word\<close>
+proof -
+  define m :: nat where \<open>m = LENGTH('a) - 1\<close>
+  then have l: \<open>LENGTH('a) = Suc m\<close>
+    by simp
+  define n :: nat where \<open>n = unsigned a\<close>
+  then have \<open>n < 2 ^ LENGTH('a)\<close>
+  then have \<open>n < 2 * 2 ^ m\<close>
+  then have \<open>P (of_nat n)\<close>
+  proof (induction n rule: nat_bit_induct)
+    case zero
+    show ?case
+      by simp (rule word_zero)
+  next
+    case (even n)
+    then have \<open>n < 2 ^ m\<close>
+      by simp
+    with even.IH have \<open>P (of_nat n)\<close>
+      by simp
+    moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
+      by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l)
+    moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
+      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
+      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
+    ultimately have \<open>P (2 * of_nat n)\<close>
+      by (rule word_even)
+    then show ?case
+      by simp
+  next
+    case (odd n)
+    then have \<open>Suc n \<le> 2 ^ m\<close>
+      by simp
+    with odd.IH have \<open>P (of_nat n)\<close>
+      by simp
+    moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
+      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
+      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
+    ultimately have \<open>P (1 + 2 * of_nat n)\<close>
+      by (rule word_odd)
+    then show ?case
+      by simp
+  qed
+  then show ?thesis
+qed
+
+lemma bit_word_half_eq:
+  \<open>(of_bool b + a * 2) div 2 = a\<close>
+    if \<open>a < 2 ^ (LENGTH('a) - Suc 0)\<close>
+    for a :: \<open>'a::len word\<close>
+proof (cases rule: length_cases [where ?'a = 'a])
+  case triv
+  have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
+    by auto
+  with triv that show ?thesis
+    by (auto; transfer) simp_all
+next
+  case take_bit_2
+  obtain n where length: \<open>LENGTH('a) = Suc n\<close>
+    by (cases \<open>LENGTH('a)\<close>) simp_all
+  show ?thesis proof (cases b)
+    case False
+    moreover have \<open>a * 2 div 2 = a\<close>
+    using that proof transfer
+      fix k :: int
+      from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close>
+        by simp
+      moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
+      with \<open>LENGTH('a) = Suc n\<close>
+      have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
+        by (simp add: take_bit_eq_mod divmod_digit_0)
+      ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
+      with take_bit_2 show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
+        = take_bit LENGTH('a) k\<close>
+        by simp
+    qed
+    ultimately show ?thesis
+      by simp
+  next
+    case True
+    moreover have \<open>(1 + a * 2) div 2 = a\<close>
+    using that proof transfer
+      fix k :: int
+      from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close>
+        using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps)
+      moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
+      with \<open>LENGTH('a) = Suc n\<close>
+      have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
+        by (simp add: take_bit_eq_mod divmod_digit_0)
+      ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
+      with take_bit_2 show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
+        = take_bit LENGTH('a) k\<close>
+        by simp
+    qed
+    ultimately show ?thesis
+      by simp
+  qed
+qed
+
+end```
```--- a/src/HOL/ex/Word_Type.thy	Tue Nov 05 19:15:00 2019 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,730 +0,0 @@
-(*  Author:  Florian Haftmann, TUM
-*)
-
-section \<open>Proof of concept for algebraically founded bit word types\<close>
-
-theory Word_Type
-  imports
-    Main
-    "HOL-ex.Bit_Lists"
-    "HOL-Library.Type_Length"
-begin
-
-subsection \<open>Preliminaries\<close>
-
-lemma take_bit_uminus:
-  "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:
-  "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]:
-  "take_bit n k \<ge> 0" for k :: int
-
-definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
-  where signed_take_bit_eq_take_bit:
-    "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
-
-lemma 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)"
-proof (cases "even k")
-  case True
-  then have "odd (k + 1)"
-    by simp
-  then have "(k + 1) mod 2 = 1"
-  with True show ?thesis
-next
-  case False
-  then show ?thesis
-    by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one)
-qed
-
-lemma signed_take_bit_Suc [simp]:
-  "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
-  by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps)
-
-lemma signed_take_bit_of_0 [simp]:
-  "signed_take_bit n 0 = 0"
-  by (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod)
-
-lemma signed_take_bit_of_minus_1 [simp]:
-  "signed_take_bit n (- 1) = - 1"
-  by (induct n) simp_all
-
-lemma signed_take_bit_eq_iff_take_bit_eq:
-  "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 that obtain m where m: "n = Suc m"
-    by (cases n) auto
-  show ?thesis
-  proof
-    assume ?Q
-    have "take_bit (Suc m) (k + 2 ^ m) =
-      take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))"
-    also have "\<dots> =
-      take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))"
-      by (simp only: \<open>?Q\<close> m [symmetric])
-    also have "\<dots> = take_bit (Suc m) (l + 2 ^ m)"
-    finally show ?P
-      by (simp only: signed_take_bit_eq_take_bit m) simp
-  next
-    assume ?P
-    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
-    then have "k mod 2 ^ n = l mod 2 ^ n"
-    then show ?Q
-  qed
-qed
-
-
-subsection \<open>Bit strings as quotient type\<close>
-
-subsubsection \<open>Basic properties\<close>
-
-quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l"
-  by (auto intro!: equivpI reflpI sympI transpI)
-
-instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
-begin
-
-lift_definition zero_word :: "'a word"
-  is 0
-  .
-
-lift_definition one_word :: "'a word"
-  is 1
-  .
-
-lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is plus
-
-lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
-  is uminus
-  by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus)
-
-lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is minus
-  by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus)
-
-lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is times
-  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
-
-instance
-  by standard (transfer; simp add: algebra_simps)+
-
-end
-
-instance word :: (len) comm_ring_1
-  by standard (transfer; simp)+
-
-quickcheck_generator word
-  constructors:
-    "zero_class.zero :: ('a::len0) word",
-    "numeral :: num \<Rightarrow> ('a::len0) word",
-    "uminus :: ('a::len0) word \<Rightarrow> ('a::len0) word"
-
-context
-  includes lifting_syntax
-  notes power_transfer [transfer_rule]
-begin
-
-lemma power_transfer_word [transfer_rule]:
-  \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
-  by transfer_prover
-
-end
-
-
-subsubsection \<open>Conversions\<close>
-
-context
-  includes lifting_syntax
-  notes transfer_rule_numeral [transfer_rule]
-    transfer_rule_of_nat [transfer_rule]
-    transfer_rule_of_int [transfer_rule]
-begin
-
-lemma [transfer_rule]:
-  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
-  by transfer_prover
-
-lemma [transfer_rule]:
-  "((=) ===> pcr_word) int of_nat"
-  by transfer_prover
-
-lemma [transfer_rule]:
-  "((=) ===> pcr_word) (\<lambda>k. k) of_int"
-proof -
-  have "((=) ===> pcr_word) of_int of_int"
-    by transfer_prover
-  then show ?thesis by (simp add: id_def)
-qed
-
-end
-
-lemma abs_word_eq:
-  "abs_word = of_int"
-  by (rule ext) (transfer, rule)
-
-context semiring_1
-begin
-
-lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
-  is "of_nat \<circ> nat \<circ> take_bit LENGTH('b)"
-  by simp
-
-lemma unsigned_0 [simp]:
-  "unsigned 0 = 0"
-  by transfer simp
-
-end
-
-context semiring_char_0
-begin
-
-lemma word_eq_iff_unsigned:
-  "a = b \<longleftrightarrow> unsigned a = unsigned b"
-  by safe (transfer; simp add: eq_nat_nat_iff)
-
-end
-
-instantiation word :: (len0) equal
-begin
-
-definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
-  where "equal_word a b \<longleftrightarrow> (unsigned a :: int) = unsigned b"
-
-instance proof
-  fix a b :: "'a word"
-  show "HOL.equal a b \<longleftrightarrow> a = b"
-    using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def)
-qed
-
-end
-
-context ring_1
-begin
-
-lift_definition signed :: "'b::len word \<Rightarrow> 'a"
-  is "of_int \<circ> signed_take_bit (LENGTH('b) - 1)"
-  by (simp add: signed_take_bit_eq_iff_take_bit_eq [symmetric])
-
-lemma signed_0 [simp]:
-  "signed 0 = 0"
-  by transfer simp
-
-end
-
-lemma unsigned_of_nat [simp]:
-  "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n"
-  by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int)
-
-lemma of_nat_unsigned [simp]:
-  "of_nat (unsigned a) = a"
-  by transfer simp
-
-lemma of_int_unsigned [simp]:
-  "of_int (unsigned a) = a"
-  by transfer simp
-
-lemma unsigned_nat_less:
-  \<open>unsigned a < (2 ^ LENGTH('a) :: nat)\<close> for a :: \<open>'a::len0 word\<close>
-  by transfer (simp add: take_bit_eq_mod)
-
-lemma unsigned_int_less:
-  \<open>unsigned a < (2 ^ LENGTH('a) :: int)\<close> for a :: \<open>'a::len0 word\<close>
-  by transfer (simp add: take_bit_eq_mod)
-
-context ring_char_0
-begin
-
-lemma word_eq_iff_signed:
-  "a = b \<longleftrightarrow> signed a = signed b"
-  by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq)
-
-end
-
-lemma signed_of_int [simp]:
-  "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k"
-  by transfer simp
-
-lemma of_int_signed [simp]:
-  "of_int (signed a) = a"
-  by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps)
-
-
-subsubsection \<open>Properties\<close>
-
-lemma length_cases:
-  obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)"
-    | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)"
-proof (cases "LENGTH('a) \<ge> 2")
-  case False
-  then have "LENGTH('a) = 1"
-    by (auto simp add: not_le dest: less_2_cases)
-  then have "take_bit LENGTH('a) 2 = (0 :: int)"
-    by simp
-  with \<open>LENGTH('a) = 1\<close> triv show ?thesis
-    by simp
-next
-  case True
-  then obtain n where "LENGTH('a) = Suc (Suc n)"
-    by (auto dest: le_Suc_ex)
-  then have "take_bit LENGTH('a) 2 = (2 :: int)"
-    by simp
-  with take_bit_2 show ?thesis
-    by simp
-qed
-
-
-subsubsection \<open>Division\<close>
-
-instantiation word :: (len0) modulo
-begin
-
-lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b"
-  by simp
-
-lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b"
-  by simp
-
-instance ..
-
-end
-
-lemma zero_word_div_eq [simp]:
-  \<open>0 div a = 0\<close> for a :: \<open>'a::len0 word\<close>
-  by transfer simp
-
-lemma div_zero_word_eq [simp]:
-  \<open>a div 0 = 0\<close> for a :: \<open>'a::len0 word\<close>
-  by transfer simp
-
-context
-  includes lifting_syntax
-begin
-
-lemma [transfer_rule]:
-  "(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
-proof -
-  have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
-    for k :: int
-  proof
-    assume ?P
-    then show ?Q
-      by auto
-  next
-    assume ?Q
-    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
-    then have "even (take_bit LENGTH('a) k)"
-      by simp
-    then show ?P
-      by simp
-  qed
-  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
-    transfer_prover
-qed
-
-end
-
-instance word :: (len) semiring_modulo
-proof
-  show "a div b * b + a mod b = a" for a b :: "'a word"
-  proof transfer
-    fix k l :: int
-    define r :: int where "r = 2 ^ LENGTH('a)"
-    then have r: "take_bit LENGTH('a) k = k mod r" for k
-    have "k mod r = ((k mod r) div (l mod r) * (l mod r)
-      + (k mod r) mod (l mod r)) mod r"
-    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
-      + (k mod r) mod (l mod r)) mod r"
-    also have "... = (((k mod r) div (l mod r) * l) mod r
-      + (k mod r) mod (l mod r)) mod r"
-    finally have "k mod r = ((k mod r) div (l mod r) * l
-      + (k mod r) mod (l mod r)) mod r"
-    with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
-      + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
-      by simp
-  qed
-qed
-
-instance word :: (len) semiring_parity
-proof
-  show "\<not> 2 dvd (1::'a word)"
-    by transfer simp
-  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
-    for a :: "'a word"
-    by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
-  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
-    for a :: "'a word"
-    by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
-qed
-
-
-subsubsection \<open>Orderings\<close>
-
-instantiation word :: (len0) linorder
-begin
-
-lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
-  is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b"
-  by simp
-
-lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
-  is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b"
-  by simp
-
-instance
-  by standard (transfer; auto)+
-
-end
-
-context linordered_semidom
-begin
-
-lemma word_less_eq_iff_unsigned:
-  "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
-  by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
-
-lemma word_less_iff_unsigned:
-  "a < b \<longleftrightarrow> unsigned a < unsigned b"
-  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
-
-end
-
-lemma word_greater_zero_iff:
-  \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len0 word\<close>
-  by transfer (simp add: less_le)
-
-lemma of_nat_word_eq_iff:
-  \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
-  by transfer (simp add: take_bit_of_nat)
-
-lemma of_nat_word_less_eq_iff:
-  \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close>
-  by transfer (simp add: take_bit_of_nat)
-
-lemma of_nat_word_less_iff:
-  \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close>
-  by transfer (simp add: take_bit_of_nat)
-
-lemma of_nat_word_eq_0_iff:
-  \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
-  using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
-
-lemma of_int_word_eq_iff:
-  \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
-  by transfer rule
-
-lemma of_int_word_less_eq_iff:
-  \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
-  by transfer rule
-
-lemma of_int_word_less_iff:
-  \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
-  by transfer rule
-
-lemma of_int_word_eq_0_iff:
-  \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
-  using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
-
-
-subsection \<open>Bit operation on \<^typ>\<open>'a word\<close>\<close>
-
-context unique_euclidean_semiring_with_nat
-begin
-
-primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
-  where
-    "n_bits_of 0 a = []"
-  | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)"
-
-lemma n_bits_of_eq_iff:
-  "n_bits_of n a = n_bits_of n b \<longleftrightarrow> take_bit n a = take_bit n b"
-  apply (induction n arbitrary: a b)
-   apply (auto elim!: evenE oddE)
-   apply (metis dvd_triv_right even_plus_one_iff)
-  apply (metis dvd_triv_right even_plus_one_iff)
-  done
-
-lemma take_n_bits_of [simp]:
-  "take m (n_bits_of n a) = n_bits_of (min m n) a"
-proof -
-  define q and v and w where "q = min m n" and "v = m - q" and "w = n - q"
-  then have "v = 0 \<or> w = 0"
-    by auto
-  then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a"
-    by (induction q arbitrary: a) auto
-  with q_def v_def w_def show ?thesis
-    by simp
-qed
-
-lemma unsigned_of_bits_n_bits_of [simp]:
-  "unsigned_of_bits (n_bits_of n a) = take_bit n a"
-  by (induction n arbitrary: a) (simp_all add: ac_simps)
-
-end
-
-lemma unsigned_of_bits_eq_of_bits:
-  "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
-
-
-instantiation word :: (len) bit_representation
-begin
-
-lift_definition bits_of_word :: "'a word \<Rightarrow> bool list"
-  is "n_bits_of LENGTH('a)"
-
-lift_definition of_bits_word :: "bool list \<Rightarrow> 'a word"
-  is unsigned_of_bits .
-
-instance proof
-  fix a :: "'a word"
-  show "of_bits (bits_of a) = a"
-    by transfer simp
-qed
-
-end
-
-lemma take_bit_complement_iff:
-  "take_bit n (complement k) = take_bit n (complement l) \<longleftrightarrow> take_bit n k = take_bit n l"
-  for k l :: int
-  by (simp add: take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute)
-
-lemma take_bit_not_iff:
-  "take_bit n (NOT k) = take_bit n (NOT l) \<longleftrightarrow> take_bit n k = take_bit n l"
-  for k l :: int
-  by (simp add: not_int_def take_bit_complement_iff)
-
-lemma n_bits_of_not:
-  "n_bits_of n (NOT k) = map Not (n_bits_of n k)"
-  for k :: int
-  by (induction n arbitrary: k) (simp_all add: not_div_2)
-
-lemma take_bit_and [simp]:
-  "take_bit n (k AND l) = take_bit n k AND take_bit n l"
-  for k l :: int
-  apply (induction n arbitrary: k l)
-   apply simp
-  apply (subst and_int.rec)
-  apply (subst (2) and_int.rec)
-  apply simp
-  done
-
-lemma take_bit_or [simp]:
-  "take_bit n (k OR l) = take_bit n k OR take_bit n l"
-  for k l :: int
-  apply (induction n arbitrary: k l)
-   apply simp
-  apply (subst or_int.rec)
-  apply (subst (2) or_int.rec)
-  apply simp
-  done
-
-lemma take_bit_xor [simp]:
-  "take_bit n (k XOR l) = take_bit n k XOR take_bit n l"
-  for k l :: int
-  apply (induction n arbitrary: k l)
-   apply simp
-  apply (subst xor_int.rec)
-  apply (subst (2) xor_int.rec)
-  apply simp
-  done
-
-instantiation word :: (len) bit_operations
-begin
-
-lift_definition not_word :: "'a word \<Rightarrow> 'a word"
-  is not
-
-lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "and"
-  by simp
-
-lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is or
-  by simp
-
-lift_definition xor_word ::  "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is xor
-  by simp
-
-lift_definition shift_left_word :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word"
-  is shift_left
-proof -
-  show "take_bit LENGTH('a) (k << n) = take_bit LENGTH('a) (l << n)"
-    if "take_bit LENGTH('a) k = take_bit LENGTH('a) l" for k l :: int and n :: nat
-  proof -
-    from that
-    have "take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
-      = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)"
-      by simp
-    moreover have "min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n"
-      by simp
-    ultimately show ?thesis by (simp add: take_bit_push_bit)
-  qed
-qed
-
-lift_definition shift_right_word :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word"
-  is "\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)"
-  by simp
-
-instance proof
-  show "semilattice ((AND) :: 'a word \<Rightarrow> _)"
-    by standard (transfer; simp add: ac_simps)+
-  show "semilattice ((OR) :: 'a word \<Rightarrow> _)"
-    by standard (transfer; simp add: ac_simps)+
-  show "abel_semigroup ((XOR) :: 'a word \<Rightarrow> _)"
-    by standard (transfer; simp add: ac_simps)+
-  show "not = (of_bits \<circ> map Not \<circ> bits_of :: 'a word \<Rightarrow> 'a word)"
-  proof
-    fix a :: "'a word"
-    have "NOT a = of_bits (map Not (bits_of a))"
-      by transfer (simp flip: unsigned_of_bits_take n_bits_of_not add: take_map)
-    then show "NOT a = (of_bits \<circ> map Not \<circ> bits_of) a"
-      by simp
-  qed
-  show "of_bits bs AND of_bits cs = (of_bits (map2 (\<and>) bs cs) :: 'a word)"
-    if "length bs = length cs" for bs cs
-    using that apply transfer
-    apply (simp only: unsigned_of_bits_eq_of_bits)
-    apply (subst and_eq)
-    apply simp_all
-    done
-  show "of_bits bs OR of_bits cs = (of_bits (map2 (\<or>) bs cs) :: 'a word)"
-    if "length bs = length cs" for bs cs
-    using that apply transfer
-    apply (simp only: unsigned_of_bits_eq_of_bits)
-    apply (subst or_eq)
-    apply simp_all
-    done
-  show "of_bits bs XOR of_bits cs = (of_bits (map2 (\<noteq>) bs cs) :: 'a word)"
-    if "length bs = length cs" for bs cs
-    using that apply transfer
-    apply (simp only: unsigned_of_bits_eq_of_bits)
-    apply (subst xor_eq)
-    apply simp_all
-    done
-  show "a << n = of_bits (replicate n False @ bits_of a)"
-    for a :: "'a word" and n :: nat
-    by transfer (simp add: push_bit_take_bit)
-  show "a >> n = of_bits (drop n (bits_of a))"
-    if "n < length (bits_of a)"
-    for a :: "'a word" and n :: nat
-    using that by transfer simp
-qed
-
-
-subsection \<open>Bit structure on \<^typ>\<open>'a word\<close>\<close>
-
-lemma word_bit_induct [case_names zero even odd]:
-  \<open>P a\<close> if word_zero: \<open>P 0\<close>
-    and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close>
-    and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (1 + 2 * a)\<close>
-  for P and a :: \<open>'a::len word\<close>
-proof -
-  define m :: nat where \<open>m = LENGTH('a) - 1\<close>
-  then have l: \<open>LENGTH('a) = Suc m\<close>
-    by simp
-  define n :: nat where \<open>n = unsigned a\<close>
-  then have \<open>n < 2 ^ LENGTH('a)\<close>
-  then have \<open>n < 2 * 2 ^ m\<close>
-  then have \<open>P (of_nat n)\<close>
-  proof (induction n rule: nat_bit_induct)
-    case zero
-    show ?case
-      by simp (rule word_zero)
-  next
-    case (even n)
-    then have \<open>n < 2 ^ m\<close>
-      by simp
-    with even.IH have \<open>P (of_nat n)\<close>
-      by simp
-    moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
-      by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l)
-    moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
-      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
-      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
-    ultimately have \<open>P (2 * of_nat n)\<close>
-      by (rule word_even)
-    then show ?case
-      by simp
-  next
-    case (odd n)
-    then have \<open>Suc n \<le> 2 ^ m\<close>
-      by simp
-    with odd.IH have \<open>P (of_nat n)\<close>
-      by simp
-    moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
-      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
-      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
-    ultimately have \<open>P (1 + 2 * of_nat n)\<close>
-      by (rule word_odd)
-    then show ?case
-      by simp
-  qed
-  then show ?thesis
-qed
-
-end
-
-global_interpretation bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a::len word"
-  rewrites "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
-proof -
-  interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word"
-  proof
-    show "a AND (b OR c) = a AND b OR a AND c"
-      for a b c :: "'a word"
-      by transfer (simp add: bit_int.conj_disj_distrib)
-    show "a OR b AND c = (a OR b) AND (a OR c)"
-      for a b c :: "'a word"
-      by transfer (simp add: bit_int.disj_conj_distrib)
-    show "a AND NOT a = 0" for a :: "'a word"
-      by transfer simp
-    show "a OR NOT a = - 1" for a :: "'a word"
-      by transfer simp
-  qed (transfer; simp)+
-  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)"
-    by (fact bit_word.boolean_algebra_axioms)
-  show "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
-  proof (rule ext)+
-    fix a b :: "'a word"
-    have "a XOR b = a AND NOT b OR NOT a AND b"
-      by transfer (simp add: bit_int.xor_def)
-    then show "bit_word.xor a b = a XOR b"