--- a/src/HOL/Library/More_List.thy Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/Library/More_List.thy Wed Feb 05 20:17:00 2020 +0000
@@ -378,5 +378,18 @@
by simp
qed
+lemma nth_default_map2:
+ \<open>nth_default d (map2 f xs ys) n = f (nth_default d1 xs n) (nth_default d2 ys n)\<close>
+ if \<open>length xs = length ys\<close> and \<open>f d1 d2 = d\<close> for bs cs
+using that proof (induction xs ys arbitrary: n rule: list_induct2)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons x xs y ys)
+ then show ?case
+ by (cases n) simp_all
+qed
+
end
--- a/src/HOL/ex/Bit_Lists.thy Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/ex/Bit_Lists.thy Wed Feb 05 20:17:00 2020 +0000
@@ -5,9 +5,19 @@
theory Bit_Lists
imports
- Word
+ Word "HOL-Library.More_List"
begin
+lemma hd_zip:
+ \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+ using that by (cases xs; cases ys) simp_all
+
+lemma last_zip:
+ \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+ and \<open>length xs = length ys\<close>
+ using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all
+
+
subsection \<open>Fragments of algebraic bit representations\<close>
context comm_semiring_1
@@ -36,7 +46,7 @@
simp_all add: algebra_simps)
lemma unsigned_of_bits_take [simp]:
- "unsigned_of_bits (take n bs) = Parity.take_bit n (unsigned_of_bits bs)"
+ "unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)"
proof (induction bs arbitrary: n)
case Nil
then show ?case
@@ -59,6 +69,18 @@
by (cases n) simp_all
qed
+lemma bit_unsigned_of_bits_iff:
+ \<open>bit (unsigned_of_bits bs) n \<longleftrightarrow> nth_default False bs n\<close>
+proof (induction bs arbitrary: n)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ then show ?case
+ by (cases n) simp_all
+qed
+
primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
where
"n_bits_of 0 a = []"
@@ -125,6 +147,10 @@
end
+lemma bit_of_bits_nat_iff:
+ \<open>bit (of_bits bs :: nat) n \<longleftrightarrow> nth_default False bs n\<close>
+ by (simp add: bit_unsigned_of_bits_iff)
+
lemma bits_of_Suc_0 [simp]:
"bits_of (Suc 0) = [True]"
by simp
@@ -211,6 +237,18 @@
by (simp_all add: *)
qed
+lemma bit_of_bits_int_iff:
+ \<open>bit (of_bits bs :: int) n \<longleftrightarrow> nth_default (bs \<noteq> [] \<and> last bs) bs n\<close>
+proof (induction bs arbitrary: n)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ then show ?case
+ by (cases n; cases b; cases bs) simp_all
+qed
+
lemma of_bits_append [simp]:
"of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)"
if "bs \<noteq> []" "\<not> last bs"
@@ -291,24 +329,14 @@
class ring_bit_representation = ring_bit_operations + semiring_bit_representation +
assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of"
-
context zip_nat
begin
lemma of_bits:
"of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: nat)"
- if "length bs = length cs" for bs cs
-using that proof (induction bs cs rule: list_induct2)
- case Nil
- then show ?case
- by simp
-next
- case (Cons b bs c cs)
- then show ?case
- by (cases "of_bits bs = (0::nat) \<or> of_bits cs = (0::nat)")
- (auto simp add: ac_simps end_of_bits rec [of "Suc 0"])
-qed
-
+ if "length bs = length cs" for bs cs
+ by (simp add: Parity.bit_eq_iff bit_unsigned_of_bits_iff bit_eq_iff)
+ (simp add: that end_of_bits nth_default_map2 [of _ _ _ False False])
end
instance nat :: semiring_bit_representation
@@ -321,32 +349,22 @@
begin
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
-using \<open>length bs = length cs\<close> proof (induction bs cs rule: list_induct2)
- case Nil
- then show ?case
- using \<open>\<not> False \<^bold>* False\<close> by (auto simp add: False_False_imp_True_True split: bool.splits)
+ \<open>of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)\<close>
+ if \<open>length bs = length cs\<close> and \<open>\<not> False \<^bold>* False\<close> for bs cs
+proof (cases \<open>bs = []\<close>)
+ case True
+ moreover have \<open>cs = []\<close>
+ using True that by simp
+ ultimately show ?thesis
+ by (simp add: Parity.bit_eq_iff bit_eq_iff that)
next
- case (Cons b bs c cs)
- show ?case
- proof (cases "bs = []")
- case True
- with Cons show ?thesis
- using \<open>\<not> False \<^bold>* False\<close> by (cases b; cases c)
- (auto simp add: ac_simps split: bool.splits)
- next
- case False
- with Cons.hyps have "cs \<noteq> []"
- by auto
- with \<open>bs \<noteq> []\<close> have "map2 (\<^bold>*) bs cs \<noteq> []"
- by (simp add: zip_eq_Nil_iff)
- from \<open>bs \<noteq> []\<close> \<open>cs \<noteq> []\<close> \<open>map2 (\<^bold>*) bs cs \<noteq> []\<close> Cons show ?thesis
- by (cases b; cases c)
- (auto simp add: \<open>\<not> False \<^bold>* False\<close> ac_simps
- rec [of "of_bits bs * 2"] rec [of "of_bits cs * 2"]
- rec [of "1 + of_bits bs * 2"])
- qed
+ case False
+ moreover have \<open>cs \<noteq> []\<close>
+ using False that by auto
+ ultimately show ?thesis
+ apply (simp add: Parity.bit_eq_iff bit_of_bits_int_iff bit_eq_iff zip_eq_Nil_iff last_map last_zip that)
+ apply (simp add: that nth_default_map2 [of _ _ _ \<open>last bs\<close> \<open>last cs\<close>])
+ done
qed
end
--- a/src/HOL/ex/Bit_Operations.thy Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy Wed Feb 05 20:17:00 2020 +0000
@@ -248,176 +248,92 @@
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"
+ for f :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>\<^bold>*\<close> 70) +
+ assumes end_of_bits: \<open>\<not> False \<^bold>* False\<close>
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)"
+function F :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> (infixl \<open>\<^bold>\<times>\<close> 70)
+ where \<open>m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
+ else of_bool (odd m \<^bold>* odd n) + 2 * ((m div 2) \<^bold>\<times> (n div 2)))\<close>
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
+declare F.simps [simp del]
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)
+proof (cases \<open>m = 0 \<and> n = 0\<close>)
+ case True
+ then have \<open>m \<^bold>\<times> n = 0\<close>
+ using True by (simp add: F.simps [of 0 0])
+ moreover have \<open>(m div 2) \<^bold>\<times> (n div 2) = m \<^bold>\<times> n\<close>
+ using True by simp
+ ultimately show ?thesis
+ using True by (simp add: end_of_bits)
+next
+ case False
+ then show ?thesis
+ by (auto simp add: ac_simps F.simps [of m n])
+qed
-declare F.simps [simp del]
+lemma bit_eq_iff:
+ \<open>bit (m \<^bold>\<times> n) q \<longleftrightarrow> bit m q \<^bold>* bit n q\<close>
+proof (induction q arbitrary: m n)
+ case 0
+ then show ?case
+ by (simp add: rec [of m n])
+next
+ case (Suc n)
+ then show ?case
+ by (simp add: rec [of m n])
+qed
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 simp add: ac_simps 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
+ by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
end
instantiation nat :: semiring_bit_operations
begin
-global_interpretation and_nat: zip_nat "(\<and>)"
+global_interpretation and_nat: zip_nat \<open>(\<and>)\<close>
defines and_nat = and_nat.F
by standard auto
-global_interpretation and_nat: semilattice "(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+global_interpretation and_nat: semilattice \<open>(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat\<close>
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)
+ show \<open>n AND n = n\<close> for n :: nat
+ by (simp add: bit_eq_iff and_nat.bit_eq_iff)
qed
-declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
- \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation or_nat: zip_nat "(\<or>)"
+global_interpretation or_nat: zip_nat \<open>(\<or>)\<close>
defines or_nat = or_nat.F
by standard auto
-global_interpretation or_nat: semilattice "(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+global_interpretation or_nat: semilattice \<open>(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat\<close>
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)
+ show \<open>n OR n = n\<close> for n :: nat
+ by (simp add: bit_eq_iff or_nat.bit_eq_iff)
qed
-declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
- \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation xor_nat: zip_nat "(\<noteq>)"
+global_interpretation xor_nat: zip_nat \<open>(\<noteq>)\<close>
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>
-
instance proof
fix m n q :: nat
show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
- proof (rule sym, induction q arbitrary: m n)
- case 0
- then show ?case
- by (simp add: and_nat.even_iff)
- next
- case (Suc q)
- with and_nat.rec [of m n] show ?case
- by simp
- qed
+ by (fact and_nat.bit_eq_iff)
show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
- proof (rule sym, induction q arbitrary: m n)
- case 0
- then show ?case
- by (simp add: or_nat.even_iff)
- next
- case (Suc q)
- with or_nat.rec [of m n] show ?case
- by simp
- qed
+ by (fact or_nat.bit_eq_iff)
show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
- proof (rule sym, induction q arbitrary: m n)
- case 0
- then show ?case
- by (simp add: xor_nat.even_iff)
- next
- case (Suc q)
- with xor_nat.rec [of m n] show ?case
- by simp
- qed
+ by (fact xor_nat.bit_eq_iff)
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 Suc_0_and_eq [simp]:
\<open>Suc 0 AND n = of_bool (odd n)\<close>
using one_and_eq [of n] by simp
@@ -445,314 +361,112 @@
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)
+ for f :: \<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close> (infixl \<open>\<^bold>*\<close> 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}
+function F :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> (infixl \<open>\<^bold>\<times>\<close> 70)
+ where \<open>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)"
+ else of_bool (odd k \<^bold>* odd l) + 2 * ((k div 2) \<^bold>\<times> (l div 2)))\<close>
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)
+ \<open>k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + 2 * ((k div 2) \<^bold>\<times> (l div 2))\<close>
+proof (cases \<open>k \<in> {0, - 1} \<and> l \<in> {0, - 1}\<close>)
+ case True
+ then have \<open>(k div 2) \<^bold>\<times> (l div 2) = k \<^bold>\<times> l\<close>
+ by auto
+ moreover have \<open>of_bool (odd k \<^bold>* odd l) = - (k \<^bold>\<times> l)\<close>
+ using True by (simp add: F.simps [of k l])
+ ultimately show ?thesis by simp
+next
+ case False
+ then show ?thesis
+ by (auto simp add: ac_simps F.simps [of k l])
+qed
+
+lemma bit_eq_iff:
+ \<open>bit (k \<^bold>\<times> l) n \<longleftrightarrow> bit k n \<^bold>* bit l n\<close>
+proof (induction n arbitrary: k l)
+ case 0
+ then show ?case
+ by (simp add: rec [of k l])
+next
+ case (Suc n)
+ then show ?case
+ by (simp add: rec [of k l])
+qed
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
+ by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
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)
+ by (simp add: bit_eq_iff and_int.bit_eq_iff)
qed
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)
+ by (simp add: bit_eq_iff or_int.bit_eq_iff)
qed
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>
+definition not_int :: \<open>int \<Rightarrow> int\<close>
+ where \<open>not_int k = - k - 1\<close>
+
+lemma not_int_rec:
+ "NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+ by (auto simp add: not_int_def elim: oddE)
+
+lemma even_not_iff_int:
+ \<open>even (NOT k) \<longleftrightarrow> odd k\<close> for k :: int
+ by (simp add: not_int_def)
+
+lemma not_int_div_2:
+ \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
+ by (simp add: not_int_def)
lemma bit_not_iff_int:
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
for k :: int
- by (induction n arbitrary: k)
- (simp_all add: not_int_def flip: complement_div_2)
+ by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int)
instance proof
fix k l :: int and n :: nat
show \<open>- k = NOT (k - 1)\<close>
by (simp add: not_int_def)
show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
- proof (rule sym, induction n arbitrary: k l)
- case 0
- then show ?case
- by (simp add: and_int.even_iff)
- next
- case (Suc n)
- with and_int.rec [of k l] show ?case
- by simp
- qed
+ by (fact and_int.bit_eq_iff)
show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
- proof (rule sym, induction n arbitrary: k l)
- case 0
- then show ?case
- by (simp add: or_int.even_iff)
- next
- case (Suc n)
- with or_int.rec [of k l] show ?case
- by simp
- qed
+ by (fact or_int.bit_eq_iff)
show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
- proof (rule sym, induction n arbitrary: k l)
- case 0
- then show ?case
- by (simp add: xor_int.even_iff)
- next
- case (Suc n)
- with xor_int.rec [of k l] show ?case
- by simp
- qed
-qed (simp_all add: minus_1_div_exp_eq_int bit_not_iff_int)
+ by (fact xor_int.bit_eq_iff)
+qed (simp_all add: bit_not_iff_int)
end
-lemma not_int_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_rec [simp]:
- "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)
-
end