--- a/src/HOL/Code_Numeral.thy Mon Dec 02 13:57:32 2019 -0500
+++ b/src/HOL/Code_Numeral.thy Mon Dec 02 14:07:42 2019 -0500
@@ -297,8 +297,8 @@
is \<open>drop_bit\<close> .
instance by (standard; transfer)
- (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
- bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+ (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+ bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
@@ -993,8 +993,8 @@
is \<open>drop_bit\<close> .
instance by (standard; transfer)
- (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
- bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+ (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+ bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
--- a/src/HOL/Library/Type_Length.thy Mon Dec 02 13:57:32 2019 -0500
+++ b/src/HOL/Library/Type_Length.thy Mon Dec 02 14:07:42 2019 -0500
@@ -103,4 +103,8 @@
end
+lemma length_not_greater_eq_2_iff [simp]:
+ \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+ by (auto simp add: not_le dest: less_2_cases)
+
end
--- a/src/HOL/Parity.thy Mon Dec 02 13:57:32 2019 -0500
+++ b/src/HOL/Parity.thy Mon Dec 02 14:07:42 2019 -0500
@@ -569,13 +569,13 @@
subsection \<open>Abstract bit structures\<close>
class semiring_bits = semiring_parity +
- assumes bit_induct [case_names stable rec]:
+ assumes bits_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>
assumes bits_div_0 [simp]: \<open>0 div a = 0\<close>
and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
- and bit_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
+ and bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
@@ -584,6 +584,10 @@
and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
begin
+lemma bits_div_by_0 [simp]:
+ \<open>a div 0 = 0\<close>
+ by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)
+
lemma bits_1_div_2 [simp]:
\<open>1 div 2 = 0\<close>
using even_succ_div_2 [of 0] by simp
@@ -629,7 +633,7 @@
\<open>0 mod a = 0\<close>
using div_mult_mod_eq [of 0 a] by simp
-lemma one_mod_two_eq_one [simp]:
+lemma bits_one_mod_two_eq_one [simp]:
\<open>1 mod 2 = 1\<close>
by (simp add: mod2_eq_if)
@@ -644,12 +648,16 @@
\<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
using div_exp_eq [of a 1 n] by (simp add: bit_def)
+lemma bit_0_eq [simp]:
+ \<open>bit 0 = bot\<close>
+ by (simp add: fun_eq_iff bit_def)
+
context
fixes a
assumes stable: \<open>a div 2 = a\<close>
begin
-lemma stable_imp_add_self:
+lemma bits_stable_imp_add_self:
\<open>a + a mod 2 = 0\<close>
proof -
have \<open>a div 2 * 2 + a mod 2 = a\<close>
@@ -668,7 +676,7 @@
lemma bit_iff_idd_imp_stable:
\<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close>
-using that proof (induction a rule: bit_induct)
+using that proof (induction a rule: bits_induct)
case (stable a)
then show ?case
by simp
@@ -693,7 +701,7 @@
lemma bit_eqI:
\<open>a = b\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> bit b n\<close>
-using that proof (induction a arbitrary: b rule: bit_induct)
+using that proof (induction a arbitrary: b rule: bits_induct)
case (stable a)
from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
by simp
@@ -714,7 +722,7 @@
then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close>
by (simp add: ac_simps)
with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
- by (simp add: stable_imp_add_self)
+ by (simp add: bits_stable_imp_add_self)
next
case (rec a p)
from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
@@ -952,7 +960,7 @@
differently wrt. code generation.
\<close>
-lemma bit_ident:
+lemma bits_ident:
"push_bit n (drop_bit n a) + take_bit n a = a"
using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
@@ -1228,4 +1236,27 @@
"push_bit n (- 1 :: int) = - (2 ^ n)"
by (simp add: push_bit_eq_mult)
+lemma minus_1_div_exp_eq_int:
+ \<open>- 1 div (2 :: int) ^ n = - 1\<close>
+ by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
+
+lemma drop_bit_minus_one [simp]:
+ \<open>drop_bit n (- 1 :: int) = - 1\<close>
+ by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
+
+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)
+
end
--- a/src/HOL/ex/Bit_Operations.thy Mon Dec 02 13:57:32 2019 -0500
+++ b/src/HOL/ex/Bit_Operations.thy Mon Dec 02 14:07:42 2019 -0500
@@ -9,22 +9,9 @@
Main
begin
-lemma minus_1_div_exp_eq_int [simp]:
- \<open>- 1 div (2 :: int) ^ n = - 1\<close>
- for n :: nat
- by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
-
context semiring_bits
begin
-lemma bits_div_by_0 [simp]:
- \<open>a div 0 = 0\<close>
- by (metis local.add_cancel_right_right local.bit_mod_div_trivial local.mod_mult_div_eq local.mult_not_zero)
-
-lemma bit_0_eq [simp]:
- \<open>bit 0 = bot\<close>
- by (simp add: fun_eq_iff bit_def)
-
end
context semiring_bit_shifts
@@ -50,7 +37,6 @@
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 map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
@@ -712,7 +698,6 @@
by (induction n arbitrary: k)
(simp_all add: not_int_def flip: complement_div_2)
-
instance proof
fix k l :: int and n :: nat
show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
@@ -745,7 +730,7 @@
with xor_int.rec [of k l] show ?case
by simp
qed
-qed (simp_all add: bit_not_iff_int)
+qed (simp_all add: minus_1_div_exp_eq_int bit_not_iff_int)
end
@@ -774,27 +759,32 @@
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"
+ "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: Parity.take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute)
+ by (simp add: 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"
+ "take_bit n (NOT k) = take_bit n (NOT l) \<longleftrightarrow> take_bit n k = take_bit n l"
for k l :: int
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int)
+lemma take_bit_not_take_bit:
+ \<open>take_bit n (NOT (take_bit n k)) = take_bit n (NOT k)\<close>
+ for k :: int
+ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
+
lemma take_bit_and [simp]:
- "Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l"
+ "take_bit n (k AND l) = take_bit n k AND take_bit n l"
for k l :: int
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
lemma take_bit_or [simp]:
- "Parity.take_bit n (k OR l) = Parity.take_bit n k OR Parity.take_bit n l"
+ "take_bit n (k OR l) = take_bit n k OR take_bit n l"
for k l :: int
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff)
lemma take_bit_xor [simp]:
- "Parity.take_bit n (k XOR l) = Parity.take_bit n k XOR Parity.take_bit n l"
+ "take_bit n (k XOR l) = take_bit n k XOR take_bit n l"
for k l :: int
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
--- a/src/HOL/ex/Word.thy Mon Dec 02 13:57:32 2019 -0500
+++ b/src/HOL/ex/Word.thy Mon Dec 02 14:07:42 2019 -0500
@@ -10,37 +10,8 @@
"HOL-ex.Bit_Operations"
begin
-context
- includes lifting_syntax
-begin
-
-lemma transfer_rule_of_bool:
- \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
- if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
- for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close> (infix \<open>\<cong>\<close> 50)
- by (unfold of_bool_def [abs_def]) transfer_prover
-
-end
-
-
subsection \<open>Preliminaries\<close>
-lemma length_not_greater_eq_2_iff [simp]:
- \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
- by (auto simp add: not_le dest: less_2_cases)
-
-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"
@@ -296,26 +267,9 @@
subsubsection \<open>Properties\<close>
-lemma length_cases: \<comment> \<open>TODO get rid of\<close>
- 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
+lemma exp_eq_zero_iff:
+ \<open>(2 :: 'a::len word) ^ n = 0 \<longleftrightarrow> LENGTH('a) \<le> n\<close>
+ by transfer simp
subsubsection \<open>Division\<close>
@@ -343,10 +297,6 @@
\<open>a div 0 = 0\<close> for a :: \<open>'a::len0 word\<close>
by transfer simp
-(*lemma
- \<open>a div a = of_bool (a \<noteq> 0)\<close> for a :: \<open>'a::len word\<close>
- by transfer simp*)
-
context
includes lifting_syntax
begin
@@ -406,17 +356,12 @@
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)
+ by transfer (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)
+ by transfer (simp_all add: mod_2_eq_odd)
qed
-(*lemma
- \<open>2 ^ n = (0 :: 'a word) \<longleftrightarrow> LENGTH('a::len) \<le> n\<close>
- apply transfer*)
-
-
subsubsection \<open>Orderings\<close>
@@ -544,14 +489,14 @@
\<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
+proof (cases \<open>2 \<le> LENGTH('a::len)\<close>)
+ case False
have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
by auto
- with triv that show ?thesis
+ with False that show ?thesis
by (auto; transfer) simp_all
next
- case take_bit_2
+ case True
obtain n where length: \<open>LENGTH('a) = Suc n\<close>
by (cases \<open>LENGTH('a)\<close>) simp_all
show ?thesis proof (cases b)
@@ -567,7 +512,7 @@
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)
+ with True 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
@@ -586,9 +531,9 @@
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)
+ with True 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
+ by auto
qed
ultimately show ?thesis
by simp
@@ -651,10 +596,7 @@
done
show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n"
for a :: "'a word" and m n :: nat
- apply transfer
- apply (auto simp flip: take_bit_eq_mod)
- apply (simp add: ac_simps)
- done
+ by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps)
show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat
using that apply transfer
@@ -663,9 +605,7 @@
done
show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
for a :: "'a word" and m n :: nat
- apply transfer
- apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
- done
+ by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
qed
context
@@ -691,12 +631,12 @@
lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
is push_bit
proof -
- show \<open>Parity.take_bit LENGTH('a) (push_bit n k) = Parity.take_bit LENGTH('a) (push_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
+ show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
+ if \<open>take_bit LENGTH('a) k = 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>
+ have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
+ = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
by simp
moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
by simp
@@ -713,19 +653,7 @@
show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
by transfer (simp add: push_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: 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: take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq)
- qed
+ by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
qed
end
@@ -752,8 +680,7 @@
instance proof
fix a b :: \<open>'a word\<close> and n :: nat
show \<open>even (- 1 div (2 :: 'a word) ^ n) \<longleftrightarrow> (2 :: 'a word) ^ n = 0\<close>
- by transfer
- (simp flip: drop_bit_eq_div add: drop_bit_take_bit, simp add: drop_bit_eq_div)
+ by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
by transfer (simp add: bit_not_iff)
show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>