proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
--- 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"
+ by (simp add: xor_def)
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
-
-context ab_group_add
+ Bit_Operations
begin
-lemma minus_diff_commute:
- "- b - a = - a - b"
- by (simp only: diff_conv_add_uminus add.commute)
-
-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 @@
simp_all add: algebra_simps)
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 @@
by (auto simp add: of_bits_int_def)
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)"
+ by (simp add: of_bits_int_def)
-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)"
+ by (simp add: n_bits_of_eq_iff)
-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
- by (simp add: ac_simps)
- next
- case (even m)
- with rec [of "2 * m" n] rec [of n "2 * m"] show ?case
- by (simp add: ac_simps)
- next
- case (odd m)
- with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case
- by (simp add: ac_simps)
- 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
- by (simp add: and_nat.self)
-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
- by (simp add: or_nat.self)
-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
- by (simp_all add: not_eq)
-
-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
- by (simp add: ac_simps)
- next
- case (odd k)
- with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case
- by (simp add: ac_simps)
- 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
- by (simp add: and_int.self)
-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
- by (simp add: or_int.self)
-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
- by (simp add: not_int_def)
-
-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
- by (simp add: not_int_def)
- 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"
- by (simp add: bit_int.xor_def)
- 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
+ by (simp add: ac_simps)
+ next
+ case (odd k)
+ with rec [of k True] show ?case
+ by (simp add: ac_simps)
+ 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 (no_types, hide_lams) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus)
+ 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
+ by (simp add: shift_bit_nat_def)
+ show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat
+ by (simp add: drop_bit_nat_def)
+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
+ by (simp add: shift_bit_int_def)
+ show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int
+ by (simp add: drop_bit_int_def)
+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
+ (simp add: Parity.take_bit_eq_mod take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq)
+ 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
+ by (simp add: ac_simps)
+ next
+ case (even m)
+ with rec [of "2 * m" n] rec [of n "2 * m"] show ?case
+ by (simp add: ac_simps)
+ next
+ case (odd m)
+ with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case
+ by (simp add: ac_simps)
+ 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
+ by (simp add: and_nat.self)
+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
+ by (simp add: or_nat.self)
+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
+ by (simp add: ac_simps)
+ next
+ case (odd k)
+ with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case
+ by (simp add: ac_simps)
+ 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
+ by (simp add: and_int.self)
+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
+ by (simp add: or_int.self)
+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
+ by (simp add: not_int_def)
+
+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,
+ simp_all add: and_int.commute or_int.commute)
+ 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
+ by (simp add: not_int_def)
+ 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"
+ by (simp add: bit_int.xor_def)
+ 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
+ by (simp add: take_bit_not_iff)
+
+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"
+ by (simp add: bit_word.xor_def)
+ 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>
+
+context ab_group_add
+begin
+
+lemma minus_diff_commute:
+ "- b - a = - a - b"
+ by (simp only: diff_conv_add_uminus add.commute)
+
+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
+ by (simp add: take_bit_eq_mod)
+
+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"
+ by (simp add: even_iff_mod_2_eq_zero)
+ with True show ?thesis
+ by (simp add: signed_take_bit_eq_take_bit)
+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))"
+ by (simp only: take_bit_add)
+ 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)"
+ by (simp only: take_bit_add)
+ 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
+ by (metis mod_add_eq)
+ then have "k mod 2 ^ n = l mod 2 ^ n"
+ by (metis add_diff_cancel_right' uminus_add_conv_diff)
+ then show ?Q
+ by (simp add: take_bit_eq_mod)
+ 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
+ by (subst take_bit_add [symmetric]) (simp add: take_bit_add)
+
+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
+ by (simp add: take_bit_eq_mod)
+ have "k mod r = ((k mod r) div (l mod r) * (l mod r)
+ + (k mod r) mod (l mod r)) mod r"
+ by (simp add: div_mult_mod_eq)
+ also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
+ + (k mod r) mod (l mod r)) mod r"
+ by (simp add: mod_add_left_eq)
+ also have "... = (((k mod r) div (l mod r) * l) mod r
+ + (k mod r) mod (l mod r)) mod r"
+ by (simp add: mod_mult_right_eq)
+ finally have "k mod r = ((k mod r) div (l mod r) * l
+ + (k mod r) mod (l mod r)) mod r"
+ by (simp add: mod_simps)
+ 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>
+ by (simp add: unsigned_nat_less)
+ then have \<open>n < 2 * 2 ^ m\<close>
+ by (simp add: l)
+ 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
+ by (simp add: n_def)
+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>
+ by (simp add: take_bit_eq_mod)
+ 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>
+ by (simp add: take_bit_eq_mod)
+ 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
- by (simp add: take_bit_eq_mod)
-
-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"
- by (simp add: even_iff_mod_2_eq_zero)
- with True show ?thesis
- by (simp add: signed_take_bit_eq_take_bit)
-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))"
- by (simp only: take_bit_add)
- 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)"
- by (simp only: take_bit_add)
- 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
- by (metis mod_add_eq)
- then have "k mod 2 ^ n = l mod 2 ^ n"
- by (metis add_diff_cancel_right' uminus_add_conv_diff)
- then show ?Q
- by (simp add: take_bit_eq_mod)
- 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
- by (subst take_bit_add [symmetric]) (simp add: take_bit_add)
-
-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
- by (simp add: take_bit_eq_mod)
- have "k mod r = ((k mod r) div (l mod r) * (l mod r)
- + (k mod r) mod (l mod r)) mod r"
- by (simp add: div_mult_mod_eq)
- also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
- + (k mod r) mod (l mod r)) mod r"
- by (simp add: mod_add_left_eq)
- also have "... = (((k mod r) div (l mod r) * l) mod r
- + (k mod r) mod (l mod r)) mod r"
- by (simp add: mod_mult_right_eq)
- finally have "k mod r = ((k mod r) div (l mod r) * l
- + (k mod r) mod (l mod r)) mod r"
- by (simp add: mod_simps)
- 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)"
- by (simp add: of_bits_int_def)
-
-
-instantiation word :: (len) bit_representation
-begin
-
-lift_definition bits_of_word :: "'a word \<Rightarrow> bool list"
- is "n_bits_of LENGTH('a)"
- by (simp add: n_bits_of_eq_iff)
-
-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
- by (simp add: take_bit_not_iff)
-
-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>
- by (simp add: unsigned_nat_less)
- then have \<open>n < 2 * 2 ^ m\<close>
- by (simp add: l)
- 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
- by (simp add: n_def)
-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"
- by (simp add: bit_word.xor_def)
- qed
-qed
-
-end