--- a/CONTRIBUTORS Thu Sep 17 18:48:06 2020 +0100
+++ b/CONTRIBUTORS Thu Sep 17 18:48:37 2020 +0100
@@ -25,6 +25,10 @@
* May 2020: Florian Haftmann
Generic algebraically founded bit operations NOT, AND, OR, XOR.
+* Sept. 2020: Florian Haftmann
+ Substantial reworking and modularization of Word library, with
+ generic type conversions.
+
* June 2020: Florian Haftmann
Simproc defined_all for more aggressive substitution with variables
from assumptions.
--- a/NEWS Thu Sep 17 18:48:06 2020 +0100
+++ b/NEWS Thu Sep 17 18:48:37 2020 +0100
@@ -93,6 +93,10 @@
* Session HOL-Word: Most operations on type word are set up
for transfer and lifting. INCOMPATIBILITY.
+* Session HOL-Word: Generic type conversions. INCOMPATIBILITY,
+sometimes additional rewrite rules must be added to applications to
+get a confluent system again.
+
* Session HOL-Word: Theory "Word_Bitwise" has been moved to AFP entry
Word_Lib as theory "Bitwise". INCOMPATIBILITY.
@@ -107,7 +111,7 @@
into its components "drop_bit" and "take_bit". INCOMPATIBILITY.
* Session HOL-Word: Uniform polymorphic "mask" operation for both
-types int and word. INCOMPATIBILITY
+types int and word. INCOMPATIBILITY.
* Session HOL-Word: Operations lsb, msb and set_bit are separated
into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Thu Sep 17 18:48:37 2020 +0100
@@ -422,7 +422,7 @@
lemma field_poly_irreducible_imp_prime:
"prime_elem p" if "irreducible p" for p :: "'a :: field poly"
using that by (fact field_poly.irreducible_imp_prime_elem)
-find_theorems name:prod_mset_prime_factorization
+
lemma field_poly_prod_mset_prime_factorization:
"prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p"
if "p \<noteq> 0" for p :: "'a :: field poly"
--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy Thu Sep 17 18:48:37 2020 +0100
@@ -80,10 +80,6 @@
by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split)
qed
-lemma bheight_baliR:
- "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
-by (cases "(l,a,r)" rule: baliR.cases) auto
-
lemma bheight_joinR:
"\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l"
proof (induct l x r rule: joinR.induct)
@@ -99,10 +95,27 @@
split!: tree.split color.split)
qed
+text \<open>All invariants in one:\<close>
+
+lemma inv_joinL: "\<lbrakk> invc l; invc r; invh l; invh r; bheight l \<le> bheight r \<rbrakk>
+ \<Longrightarrow> invc2 (joinL l x r) \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc (joinL l x r))
+ \<and> invh (joinL l x r) \<and> bheight (joinL l x r) = bheight r"
+proof (induct l x r rule: joinL.induct)
+ case (1 l x r) thus ?case
+ by(auto simp: inv_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits)
+qed
+
+lemma inv_joinR: "\<lbrakk> invc l; invc r; invh l; invh r; bheight l \<ge> bheight r \<rbrakk>
+ \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
+ \<and> invh (joinR l x r) \<and> bheight (joinR l x r) = bheight l"
+proof (induct l x r rule: joinR.induct)
+ case (1 l x r) thus ?case
+ by(auto simp: inv_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
+qed
+
(* unused *)
lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
-by(simp add: invc2_joinL invc2_joinR invh_joinL invh_joinR invh_paint rbt_def
- color_paint_Black join_def)
+by(simp add: inv_joinL inv_joinR invh_paint rbt_def color_paint_Black join_def)
text \<open>To make sure the the black height is not increased unnecessarily:\<close>
--- a/src/HOL/Divides.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Divides.thy Thu Sep 17 18:48:37 2020 +0100
@@ -693,32 +693,6 @@
thus ?lhs by simp
qed
-lemma take_bit_greater_eq:
- \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
-proof -
- have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
- proof (cases \<open>k > - (2 ^ n)\<close>)
- case False
- then have \<open>k + 2 ^ n \<le> 0\<close>
- by simp
- also note take_bit_nonnegative
- finally show ?thesis .
- next
- case True
- with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
- by simp_all
- then show ?thesis
- by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
- qed
- then show ?thesis
- by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_less_eq:
- \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
- using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
- by (simp add: take_bit_eq_mod)
-
subsection \<open>Numeral division with a pragmatic type class\<close>
@@ -1251,6 +1225,113 @@
code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+subsection \<open>More on bit operations\<close>
+
+lemma take_bit_incr_eq:
+ \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close>
+ for k :: int
+proof -
+ from that have \<open>2 ^ n \<noteq> k mod 2 ^ n + 1\<close>
+ by (simp add: take_bit_eq_mod)
+ moreover have \<open>k mod 2 ^ n < 2 ^ n\<close>
+ by simp
+ ultimately have *: \<open>k mod 2 ^ n + 1 < 2 ^ n\<close>
+ by linarith
+ have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
+ by (simp add: mod_simps)
+ also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
+ using * by (simp add: zmod_trival_iff)
+ finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_decr_eq:
+ \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close>
+ for k :: int
+proof -
+ from that have \<open>k mod 2 ^ n \<noteq> 0\<close>
+ by (simp add: take_bit_eq_mod)
+ moreover have \<open>k mod 2 ^ n \<ge> 0\<close> \<open>k mod 2 ^ n < 2 ^ n\<close>
+ by simp_all
+ ultimately have *: \<open>k mod 2 ^ n > 0\<close>
+ by linarith
+ have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
+ by (simp add: mod_simps)
+ also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
+ by (simp add: zmod_trival_iff)
+ (use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
+ finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_greater_eq:
+ \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
+proof -
+ have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
+ proof (cases \<open>k > - (2 ^ n)\<close>)
+ case False
+ then have \<open>k + 2 ^ n \<le> 0\<close>
+ by simp
+ also note take_bit_nonnegative
+ finally show ?thesis .
+ next
+ case True
+ with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
+ by simp_all
+ then show ?thesis
+ by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
+ qed
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_less_eq:
+ \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
+ using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_int_less_eq_self_iff:
+ \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for k :: int
+proof
+ assume ?P
+ show ?Q
+ proof (rule ccontr)
+ assume \<open>\<not> 0 \<le> k\<close>
+ then have \<open>k < 0\<close>
+ by simp
+ with \<open>?P\<close>
+ have \<open>take_bit n k < 0\<close>
+ by (rule le_less_trans)
+ then show False
+ by simp
+ qed
+next
+ assume ?Q
+ then show ?P
+ by (simp add: take_bit_eq_mod zmod_le_nonneg_dividend)
+qed
+
+lemma take_bit_int_less_self_iff:
+ \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+ for k :: int
+ by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
+ intro: order_trans [of 0 \<open>2 ^ n\<close> k])
+
+lemma take_bit_int_greater_self_iff:
+ \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close>
+ for k :: int
+ using take_bit_int_less_eq_self_iff [of n k] by auto
+
+lemma take_bit_int_greater_eq_self_iff:
+ \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+ for k :: int
+ by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
+ dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
+
+
subsection \<open>Lemmas of doubtful value\<close>
lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
@@ -1275,6 +1356,4 @@
lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
using that by auto
-find_theorems \<open>(?k::int) mod _ = ?k\<close>
-
end
--- a/src/HOL/Library/Bit_Operations.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy Thu Sep 17 18:48:37 2020 +0100
@@ -275,6 +275,20 @@
apply (use exp_eq_0_imp_not_bit in blast)
done
+lemma take_bit_not_eq_mask_diff:
+ \<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
+proof -
+ have \<open>take_bit n (NOT a) = take_bit n (NOT (take_bit n a))\<close>
+ by (simp add: take_bit_not_take_bit)
+ also have \<open>\<dots> = mask n AND NOT (take_bit n a)\<close>
+ by (simp add: take_bit_eq_mask ac_simps)
+ also have \<open>\<dots> = mask n - take_bit n a\<close>
+ by (subst disjunctive_diff)
+ (auto simp add: bit_take_bit_iff bit_mask_iff exp_eq_0_imp_not_bit)
+ finally show ?thesis
+ by simp
+qed
+
lemma mask_eq_take_bit_minus_one:
\<open>mask n = take_bit n (- 1)\<close>
by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)
@@ -1106,23 +1120,50 @@
for k :: int
by (simp add: signed_take_bit_def not_less concat_bit_def)
-lemma signed_take_bit_greater_eq:
+lemma signed_take_bit_int_eq_self_iff:
+ \<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
+ for k :: int
+ by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_eq_self:
+ \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
+ for k :: int
+ using that by (simp add: signed_take_bit_int_eq_self_iff)
+
+lemma signed_take_bit_int_less_eq_self_iff:
+ \<open>signed_take_bit n k \<le> k \<longleftrightarrow> - (2 ^ n) \<le> k\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_eq_self_iff algebra_simps)
+ linarith
+
+lemma signed_take_bit_int_less_self_iff:
+ \<open>signed_take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_self_iff algebra_simps)
+
+lemma signed_take_bit_int_greater_self_iff:
+ \<open>k < signed_take_bit n k \<longleftrightarrow> k < - (2 ^ n)\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_self_iff algebra_simps)
+ linarith
+
+lemma signed_take_bit_int_greater_eq_self_iff:
+ \<open>k \<le> signed_take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_greater_eq:
\<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k < - (2 ^ n)\<close>
for k :: int
- using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
+ using that take_bit_int_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
by (simp add: signed_take_bit_eq_take_bit_shift)
-lemma signed_take_bit_less_eq:
+lemma signed_take_bit_int_less_eq:
\<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close>
for k :: int
- using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
+ using that take_bit_int_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
by (simp add: signed_take_bit_eq_take_bit_shift)
-lemma signed_take_bit_eq_self:
- \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
- for k :: int
- using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self)
-
lemma signed_take_bit_Suc_bit0 [simp]:
\<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\<close>
by (simp add: signed_take_bit_Suc)
--- a/src/HOL/Parity.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Parity.thy Thu Sep 17 18:48:37 2020 +0100
@@ -1024,6 +1024,37 @@
qed
qed
+lemma
+ exp_add_not_zero_imp_left: \<open>2 ^ m \<noteq> 0\<close>
+ and exp_add_not_zero_imp_right: \<open>2 ^ n \<noteq> 0\<close>
+ if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+ have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+ proof (rule notI)
+ assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+ then have \<open>2 ^ (m + n) = 0\<close>
+ by (rule disjE) (simp_all add: power_add)
+ with that show False ..
+ qed
+ then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+ by simp_all
+qed
+
+lemma exp_not_zero_imp_exp_diff_not_zero:
+ \<open>2 ^ (n - m) \<noteq> 0\<close> if \<open>2 ^ n \<noteq> 0\<close>
+proof (cases \<open>m \<le> n\<close>)
+ case True
+ moreover define q where \<open>q = n - m\<close>
+ ultimately have \<open>n = m + q\<close>
+ by simp
+ with that show ?thesis
+ by (simp add: exp_add_not_zero_imp_right)
+next
+ case False
+ with that show ?thesis
+ by simp
+qed
+
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -1147,7 +1178,7 @@
also have "\<dots> = - int (2 * n) - 1"
by (simp add: algebra_simps)
finally show ?case
- using even by simp
+ using even.prems by simp
next
case (odd n)
have "P (- int (Suc n) * 2)"
@@ -1155,7 +1186,7 @@
also have "\<dots> = - int (Suc (2 * n)) - 1"
by (simp add: algebra_simps)
finally show ?case
- using odd by simp
+ using odd.prems by simp
qed
qed
@@ -1584,6 +1615,78 @@
\<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
by (auto simp add: bit_push_bit_iff)
+lemma take_bit_nat_less_exp [simp]:
+ \<open>take_bit n m < 2 ^ n\<close> for n m ::nat
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nonnegative [simp]:
+ \<open>take_bit n k \<ge> 0\<close> for k :: int
+ by (simp add: take_bit_eq_mod)
+
+lemma not_take_bit_negative [simp]:
+ \<open>\<not> take_bit n k < 0\<close> for k :: int
+ by (simp add: not_less)
+
+lemma take_bit_int_less_exp [simp]:
+ \<open>take_bit n k < 2 ^ n\<close> for k :: int
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nat_eq_self_iff:
+ \<open>take_bit n m = m \<longleftrightarrow> m < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for n m :: nat
+proof
+ assume ?P
+ moreover note take_bit_nat_less_exp [of n m]
+ ultimately show ?Q
+ by simp
+next
+ assume ?Q
+ then show ?P
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_nat_eq_self:
+ \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for m n :: nat
+ using that by (simp add: take_bit_nat_eq_self_iff)
+
+lemma take_bit_int_eq_self_iff:
+ \<open>take_bit n k = k \<longleftrightarrow> 0 \<le> k \<and> k < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for k :: int
+proof
+ assume ?P
+ moreover note take_bit_int_less_exp [of n k] take_bit_nonnegative [of n k]
+ ultimately show ?Q
+ by simp
+next
+ assume ?Q
+ then show ?P
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_eq_self:
+ \<open>take_bit n k = k\<close> if \<open>0 \<le> k\<close> \<open>k < 2 ^ n\<close> for k :: int
+ using that by (simp add: take_bit_int_eq_self_iff)
+
+lemma take_bit_nat_less_eq_self [simp]:
+ \<open>take_bit n m \<le> m\<close> for n m :: nat
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nat_less_self_iff:
+ \<open>take_bit n m < m \<longleftrightarrow> 2 ^ n \<le> m\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for m n :: nat
+proof
+ assume ?P
+ then have \<open>take_bit n m \<noteq> m\<close>
+ by simp
+ then show \<open>?Q\<close>
+ by (simp add: take_bit_nat_eq_self_iff)
+next
+ have \<open>take_bit n m < 2 ^ n\<close>
+ by (fact take_bit_nat_less_exp)
+ also assume ?Q
+ finally show ?P .
+qed
+
class unique_euclidean_semiring_with_bit_shifts =
unique_euclidean_semiring_with_nat + semiring_bit_shifts
begin
@@ -1752,10 +1855,6 @@
"drop_bit n (Suc 0) = of_bool (n = 0)"
using drop_bit_of_1 [where ?'a = nat] by simp
-lemma take_bit_eq_self:
- \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for n m :: nat
- using that by (simp add: take_bit_eq_mod)
-
lemma push_bit_minus_one:
"push_bit n (- 1 :: int) = - (2 ^ n)"
by (simp add: push_bit_eq_mult)
@@ -1782,24 +1881,6 @@
for k l :: int
by (simp add: take_bit_eq_mod mod_diff_eq)
-lemma take_bit_nonnegative [simp]:
- \<open>take_bit n k \<ge> 0\<close>
- for k :: int
- by (simp add: take_bit_eq_mod)
-
-lemma not_take_bit_negative [simp]:
- \<open>\<not> take_bit n k < 0\<close>
- for k :: int
- by (simp add: not_less)
-
-lemma take_bit_int_less_exp:
- \<open>take_bit n k < 2 ^ n\<close> for k :: int
- by (simp add: take_bit_eq_mod)
-
-lemma take_bit_int_eq_self:
- \<open>take_bit n k = k\<close> if \<open>0 \<le> k\<close> \<open>k < 2 ^ n\<close> for k :: int
- using that by (simp add: take_bit_eq_mod)
-
lemma bit_imp_take_bit_positive:
\<open>0 < take_bit m k\<close> if \<open>n < m\<close> and \<open>bit k n\<close> for k :: int
proof (rule ccontr)
--- a/src/HOL/ROOT Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/ROOT Thu Sep 17 18:48:37 2020 +0100
@@ -898,7 +898,6 @@
Word
More_Word
Word_Examples
- Conversions
document_files "root.bib" "root.tex"
session "HOL-Statespace" in Statespace = HOL +
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Thu Sep 17 18:48:37 2020 +0100
@@ -5147,7 +5147,6 @@
lemma filterlim_of_int_at_bot:
"filterlim f F at_bot \<Longrightarrow> filterlim (\<lambda>x. f (of_int x :: real)) F at_bot"
by (erule filterlim_compose[OF _ filterlim_real_of_int_at_bot])
-find_theorems of_int at_bot
lemma asymp_equiv_real_int_transfer_at_top:
"f \<sim>[at_top] g \<Longrightarrow> (\<lambda>x. f (of_int x :: real)) \<sim>[at_top] (\<lambda>x. g (of_int x))"
--- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Thu Sep 17 18:48:37 2020 +0100
@@ -26,7 +26,7 @@
proof -
from H8 have "nat j <= 15" by simp
with assms show ?thesis
- by (simp add: f_def bwsimps int_word_uint)
+ by (simp add: f_def bwsimps int_word_uint take_bit_int_eq_self)
qed
spark_vc function_f_7
@@ -34,7 +34,8 @@
from H7 have "16 <= nat j" by simp
moreover from H8 have "nat j <= 31" by simp
ultimately show ?thesis using assms
- by (simp add: f_def bwsimps int_word_uint)
+ by (simp only: f_def bwsimps int_word_uint)
+ (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
spark_vc function_f_8
@@ -42,7 +43,7 @@
from H7 have "32 <= nat j" by simp
moreover from H8 have "nat j <= 47" by simp
ultimately show ?thesis using assms
- by (simp add: f_def bwsimps int_word_uint)
+ by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
spark_vc function_f_9
@@ -50,7 +51,7 @@
from H7 have "48 <= nat j" by simp
moreover from H8 have "nat j <= 63" by simp
ultimately show ?thesis using assms
- by (simp add: f_def bwsimps int_word_uint)
+ by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
spark_vc function_f_10
@@ -58,7 +59,7 @@
from H2 have "nat j <= 79" by simp
moreover from H12 have "64 <= nat j" by simp
ultimately show ?thesis using assms
- by (simp add: f_def bwsimps int_word_uint)
+ by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
spark_end
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Thu Sep 17 18:48:37 2020 +0100
@@ -63,7 +63,7 @@
proof (cases C)
fix a b c d e f::word32
assume "C = (a, b, c, d, e)"
- thus ?thesis by (cases a) simp
+ thus ?thesis by (cases a) (simp add: take_bit_nat_eq_self)
qed
lemma steps_to_steps':
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Thu Sep 17 18:48:37 2020 +0100
@@ -253,7 +253,8 @@
show ?thesis
unfolding steps'_step[OF \<open>0 <= j\<close>] step_hyp[symmetric]
step_both_def step_r_def step_l_def
- by (simp add: AL BL CL DL EL AR BR CR DR ER)
+ using AL CL EL AR CR ER
+ by (simp add: BL DL BR DR take_bit_int_eq_self_iff take_bit_int_eq_self)
qed
spark_vc procedure_round_61
@@ -275,12 +276,13 @@
h3 = cd, h4 = ce\<rparr>\<rparr>)
0 x"
unfolding steps_def
- by (simp add:
+ using
uint_word_of_int_id[OF \<open>0 <= ca\<close> \<open>ca <= ?M\<close>]
uint_word_of_int_id[OF \<open>0 <= cb\<close> \<open>cb <= ?M\<close>]
uint_word_of_int_id[OF \<open>0 <= cc\<close> \<open>cc <= ?M\<close>]
uint_word_of_int_id[OF \<open>0 <= cd\<close> \<open>cd <= ?M\<close>]
- uint_word_of_int_id[OF \<open>0 <= ce\<close> \<open>ce <= ?M\<close>])
+ uint_word_of_int_id[OF \<open>0 <= ce\<close> \<open>ce <= ?M\<close>]
+ by (simp add: take_bit_int_eq_self_iff take_bit_int_eq_self)
let ?rotate_arg_l =
"((((ca + f 0 cb cc cd) mod 4294967296 +
x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)"
@@ -458,7 +460,7 @@
unfolding steps_to_steps'
unfolding H1[symmetric]
by (simp add: uint_word_ariths(1) mod_simps
- uint_word_of_int_id)
+ uint_word_of_int_id take_bit_int_eq_self)
qed
spark_end
--- a/src/HOL/Word/Bits_Int.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Word/Bits_Int.thy Thu Sep 17 18:48:37 2020 +0100
@@ -372,11 +372,11 @@
lemma sbintrunc_inc:
\<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close>
- using that by (fact signed_take_bit_greater_eq)
+ using that by (fact signed_take_bit_int_greater_eq)
lemma sbintrunc_dec:
\<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
- using that by (fact signed_take_bit_less_eq)
+ using that by (fact signed_take_bit_int_less_eq)
lemma bintr_ge0: "0 \<le> bintrunc n w"
by (simp add: bintrunc_mod2p)
--- a/src/HOL/Word/Conversions.thy Thu Sep 17 18:48:06 2020 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,556 +0,0 @@
-(* Author: Florian Haftmann, TUM
-*)
-
-section \<open>Proof of concept for conversions for algebraically founded bit word types\<close>
-
-theory Conversions
- imports
- Main
- "HOL-Library.Type_Length"
- "HOL-Library.Bit_Operations"
- "HOL-Word.Word"
-begin
-
-hide_const (open) unat uint sint word_of_int ucast scast
-
-context semiring_bits
-begin
-
-lemma
- exp_add_not_zero_imp_left: \<open>2 ^ m \<noteq> 0\<close>
- and exp_add_not_zero_imp_right: \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
-proof -
- have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
- proof (rule notI)
- assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
- then have \<open>2 ^ (m + n) = 0\<close>
- by (rule disjE) (simp_all add: power_add)
- with that show False ..
- qed
- then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
- by simp_all
-qed
-
-lemma exp_not_zero_imp_exp_diff_not_zero:
- \<open>2 ^ (n - m) \<noteq> 0\<close> if \<open>2 ^ n \<noteq> 0\<close>
-proof (cases \<open>m \<le> n\<close>)
- case True
- moreover define q where \<open>q = n - m\<close>
- ultimately have \<open>n = m + q\<close>
- by simp
- with that show ?thesis
- by (simp add: exp_add_not_zero_imp_right)
-next
- case False
- with that show ?thesis
- by simp
-qed
-
-end
-
-
-subsection \<open>Conversions to word\<close>
-
-abbreviation word_of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close>
- where \<open>word_of_nat \<equiv> of_nat\<close>
-
-abbreviation word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
- where \<open>word_of_int \<equiv> of_int\<close>
-
-lemma Word_eq_word_of_int [simp]:
- \<open>Word.Word = word_of_int\<close>
- by (rule ext; transfer) simp
-
-lemma word_of_nat_eq_iff:
- \<open>word_of_nat m = (word_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 word_of_int_eq_iff:
- \<open>word_of_int k = (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
- by transfer rule
-
-lemma word_of_nat_less_eq_iff:
- \<open>word_of_nat m \<le> (word_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 word_of_int_less_eq_iff:
- \<open>word_of_int k \<le> (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
- by transfer rule
-
-lemma word_of_nat_less_iff:
- \<open>word_of_nat m < (word_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 word_of_int_less_iff:
- \<open>word_of_int k < (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
- by transfer rule
-
-lemma word_of_nat_eq_0_iff [simp]:
- \<open>word_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 word_of_int_eq_0_iff [simp]:
- \<open>word_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>Conversion from word\<close>
-
-subsubsection \<open>Generic unsigned conversion\<close>
-
-context semiring_1
-begin
-
-lift_definition unsigned :: \<open>'b::len word \<Rightarrow> 'a\<close>
- is \<open>of_nat \<circ> nat \<circ> take_bit LENGTH('b)\<close>
- by simp
-
-lemma unsigned_0 [simp]:
- \<open>unsigned 0 = 0\<close>
- by transfer simp
-
-lemma unsigned_1 [simp]:
- \<open>unsigned 1 = 1\<close>
- by transfer simp
-
-end
-
-context semiring_char_0
-begin
-
-lemma unsigned_word_eqI:
- \<open>v = w\<close> if \<open>unsigned v = unsigned w\<close>
- using that by transfer (simp add: eq_nat_nat_iff)
-
-lemma word_eq_iff_unsigned:
- \<open>v = w \<longleftrightarrow> unsigned v = unsigned w\<close>
- by (auto intro: unsigned_word_eqI)
-
-end
-
-context semiring_bits
-begin
-
-lemma bit_unsigned_iff:
- \<open>bit (unsigned w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w n\<close>
- for w :: \<open>'b::len word\<close>
- by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)
-
-end
-
-context semiring_bit_shifts
-begin
-
-lemma unsigned_push_bit_eq:
- \<open>unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\<close>
- for w :: \<open>'b::len word\<close>
-proof (rule bit_eqI)
- fix m
- assume \<open>2 ^ m \<noteq> 0\<close>
- show \<open>bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\<close>
- proof (cases \<open>n \<le> m\<close>)
- case True
- with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
- by (metis (full_types) diff_add exp_add_not_zero_imp)
- with True show ?thesis
- by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff ac_simps exp_eq_zero_iff not_le)
- next
- case False
- then show ?thesis
- by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff)
- qed
-qed
-
-lemma unsigned_take_bit_eq:
- \<open>unsigned (take_bit n w) = take_bit n (unsigned w)\<close>
- for w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff)
-
-end
-
-context semiring_bit_operations
-begin
-
-lemma unsigned_and_eq:
- \<open>unsigned (v AND w) = unsigned v AND unsigned w\<close>
- for v w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff)
-
-lemma unsigned_or_eq:
- \<open>unsigned (v OR w) = unsigned v OR unsigned w\<close>
- for v w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_unsigned_iff bit_or_iff Bit_Operations.bit_or_iff)
-
-lemma unsigned_xor_eq:
- \<open>unsigned (v XOR w) = unsigned v XOR unsigned w\<close>
- for v w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_unsigned_iff bit_xor_iff Bit_Operations.bit_xor_iff)
-
-end
-
-context ring_bit_operations
-begin
-
-lemma unsigned_not_eq:
- \<open>unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\<close>
- for w :: \<open>'b::len word\<close>
- by (rule bit_eqI)
- (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le)
-
-end
-
-lemma unsigned_of_nat [simp]:
- \<open>unsigned (word_of_nat n :: 'a::len word) = of_nat (take_bit LENGTH('a) n)\<close>
- by transfer (simp add: nat_eq_iff take_bit_of_nat)
-
-lemma unsigned_of_int [simp]:
- \<open>unsigned (word_of_int n :: 'a::len word) = of_int (take_bit LENGTH('a) n)\<close>
- by transfer (simp add: nat_eq_iff take_bit_of_nat)
-
-context unique_euclidean_semiring_numeral
-begin
-
-lemma unsigned_greater_eq:
- \<open>0 \<le> unsigned w\<close> for w :: \<open>'b::len word\<close>
- by (transfer fixing: less_eq) simp
-
-lemma unsigned_less:
- \<open>unsigned w < 2 ^ LENGTH('b)\<close> for w :: \<open>'b::len word\<close>
- by (transfer fixing: less) (simp add: take_bit_int_less_exp)
-
-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
-
-
-subsubsection \<open>Generic signed conversion\<close>
-
-context ring_1
-begin
-
-lift_definition signed :: \<open>'b::len word \<Rightarrow> 'a\<close>
- is \<open>of_int \<circ> signed_take_bit (LENGTH('b) - Suc 0)\<close>
- by (simp flip: signed_take_bit_decr_length_iff)
-
-lemma signed_0 [simp]:
- \<open>signed 0 = 0\<close>
- by transfer simp
-
-lemma signed_1 [simp]:
- \<open>signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\<close>
- by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>)
- (simp_all add: sbintrunc_minus_simps)
-
-lemma signed_minus_1 [simp]:
- \<open>signed (- 1 :: 'b::len word) = - 1\<close>
- by (transfer fixing: uminus) simp
-
-end
-
-context ring_char_0
-begin
-
-lemma signed_word_eqI:
- \<open>v = w\<close> if \<open>signed v = signed w\<close>
- using that by transfer (simp flip: signed_take_bit_decr_length_iff)
-
-lemma word_eq_iff_signed:
- \<open>v = w \<longleftrightarrow> signed v = signed w\<close>
- by (auto intro: signed_word_eqI)
-
-end
-
-context ring_bit_operations
-begin
-
-lemma bit_signed_iff:
- \<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
- for w :: \<open>'b::len word\<close>
- by (transfer fixing: bit)
- (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
-
-lemma signed_push_bit_eq:
- \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))\<close>
- for w :: \<open>'b::len word\<close>
-proof (rule bit_eqI)
- fix m
- assume \<open>2 ^ m \<noteq> 0\<close>
- define q where \<open>q = LENGTH('b) - Suc 0\<close>
- then have *: \<open>LENGTH('b) = Suc q\<close>
- by simp
- show \<open>bit (signed (push_bit n w)) m \<longleftrightarrow>
- bit (signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))) m\<close>
- proof (cases \<open>q \<le> m\<close>)
- case True
- moreover define r where \<open>r = m - q\<close>
- ultimately have \<open>m = q + r\<close>
- by simp
- moreover from \<open>m = q + r\<close> \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ r \<noteq> 0\<close>
- using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r]
- by simp_all
- moreover from \<open>2 ^ q \<noteq> 0\<close> have \<open>2 ^ (q - n) \<noteq> 0\<close>
- by (rule exp_not_zero_imp_exp_diff_not_zero)
- ultimately show ?thesis
- by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
- min_def * exp_eq_zero_iff le_diff_conv2)
- next
- case False
- then show ?thesis
- using exp_not_zero_imp_exp_diff_not_zero [of m n]
- by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
- min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit
- exp_eq_zero_iff)
- qed
-qed
-
-lemma signed_take_bit_eq:
- \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
- for w :: \<open>'b::len word\<close>
- by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
- (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
-
-lemma signed_not_eq:
- \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
- for w :: \<open>'b::len word\<close>
-proof (rule bit_eqI)
- fix n
- assume \<open>2 ^ n \<noteq> 0\<close>
- define q where \<open>q = LENGTH('b) - Suc 0\<close>
- then have *: \<open>LENGTH('b) = Suc q\<close>
- by simp
- show \<open>bit (signed (NOT w)) n \<longleftrightarrow>
- bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\<close>
- proof (cases \<open>q < n\<close>)
- case True
- moreover define r where \<open>r = n - Suc q\<close>
- ultimately have \<open>n = r + Suc q\<close>
- by simp
- moreover from \<open>2 ^ n \<noteq> 0\<close> \<open>n = r + Suc q\<close>
- have \<open>2 ^ Suc q \<noteq> 0\<close>
- using exp_add_not_zero_imp_right by blast
- ultimately show ?thesis
- by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
- exp_eq_zero_iff)
- next
- case False
- then show ?thesis
- by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
- exp_eq_zero_iff)
- qed
-qed
-
-lemma signed_and_eq:
- \<open>signed (v AND w) = signed v AND signed w\<close>
- for v w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff)
-
-lemma signed_or_eq:
- \<open>signed (v OR w) = signed v OR signed w\<close>
- for v w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff)
-
-lemma signed_xor_eq:
- \<open>signed (v XOR w) = signed v XOR signed w\<close>
- for v w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff)
-
-end
-
-lemma signed_of_nat [simp]:
- \<open>signed (word_of_nat n :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - Suc 0) (int n))\<close>
- by transfer simp
-
-lemma signed_of_int [simp]:
- \<open>signed (word_of_int n :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - Suc 0) n)\<close>
- by transfer simp
-
-
-subsubsection \<open>Important special cases\<close>
-
-abbreviation unat :: \<open>'a::len word \<Rightarrow> nat\<close>
- where \<open>unat \<equiv> unsigned\<close>
-
-abbreviation uint :: \<open>'a::len word \<Rightarrow> int\<close>
- where \<open>uint \<equiv> unsigned\<close>
-
-abbreviation sint :: \<open>'a::len word \<Rightarrow> int\<close>
- where \<open>sint \<equiv> signed\<close>
-
-abbreviation ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
- where \<open>ucast \<equiv> unsigned\<close>
-
-abbreviation scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
- where \<open>scast \<equiv> signed\<close>
-
-context
- includes lifting_syntax
-begin
-
-lemma [transfer_rule]:
- \<open>(pcr_word ===> (=)) (nat \<circ> take_bit LENGTH('a)) (unat :: 'a::len word \<Rightarrow> nat)\<close>
- using unsigned.transfer [where ?'a = nat] by simp
-
-lemma [transfer_rule]:
- \<open>(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \<Rightarrow> int)\<close>
- using unsigned.transfer [where ?'a = int] by (simp add: comp_def)
-
-lemma [transfer_rule]:
- \<open>(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word \<Rightarrow> int)\<close>
- using signed.transfer [where ?'a = int] by simp
-
-lemma [transfer_rule]:
- \<open>(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
-proof (rule rel_funI)
- fix k :: int and w :: \<open>'a word\<close>
- assume \<open>pcr_word k w\<close>
- then have \<open>w = word_of_int k\<close>
- by (simp add: pcr_word_def cr_word_def relcompp_apply)
- moreover have \<open>pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\<close>
- by transfer (simp add: pcr_word_def cr_word_def relcompp_apply)
- ultimately show \<open>pcr_word (take_bit LENGTH('a) k) (ucast w)\<close>
- by simp
-qed
-
-lemma [transfer_rule]:
- \<open>(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
-proof (rule rel_funI)
- fix k :: int and w :: \<open>'a word\<close>
- assume \<open>pcr_word k w\<close>
- then have \<open>w = word_of_int k\<close>
- by (simp add: pcr_word_def cr_word_def relcompp_apply)
- moreover have \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))\<close>
- by transfer (simp add: pcr_word_def cr_word_def relcompp_apply)
- ultimately show \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)\<close>
- by simp
-qed
-
-end
-
-lemma of_nat_unat [simp]:
- \<open>of_nat (unat w) = unsigned w\<close>
- by transfer simp
-
-lemma of_int_uint [simp]:
- \<open>of_int (uint w) = unsigned w\<close>
- by transfer simp
-
-lemma unat_div_distrib:
- \<open>unat (v div w) = unat v div unat w\<close>
-proof transfer
- fix k l
- have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
- by (rule div_le_dividend)
- also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
- by (simp add: nat_less_iff take_bit_int_less_exp)
- finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
- (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_eq_self)
-qed
-
-lemma unat_mod_distrib:
- \<open>unat (v mod w) = unat v mod unat w\<close>
-proof transfer
- fix k l
- have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
- by (rule mod_less_eq_dividend)
- also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
- by (simp add: nat_less_iff take_bit_int_less_exp)
- finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
- (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_eq_self)
-qed
-
-lemma uint_div_distrib:
- \<open>uint (v div w) = uint v div uint w\<close>
-proof -
- have \<open>int (unat (v div w)) = int (unat v div unat w)\<close>
- by (simp add: unat_div_distrib)
- then show ?thesis
- by (simp add: of_nat_div)
-qed
-
-lemma uint_mod_distrib:
- \<open>uint (v mod w) = uint v mod uint w\<close>
-proof -
- have \<open>int (unat (v mod w)) = int (unat v mod unat w)\<close>
- by (simp add: unat_mod_distrib)
- then show ?thesis
- by (simp add: of_nat_mod)
-qed
-
-lemma of_int_sint [simp]:
- \<open>of_int (sint a) = signed a\<close>
- by transfer (simp_all add: take_bit_signed_take_bit)
-
-lemma sint_greater_eq:
- \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
-proof (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>)
- case True
- then show ?thesis
- by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps)
-next
- have *: \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> (0::int)\<close>
- by simp
- case False
- then show ?thesis
- by transfer (auto simp add: signed_take_bit_eq intro: order_trans *)
-qed
-
-lemma sint_less:
- \<open>sint w < 2 ^ (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
- by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
- (simp_all add: signed_take_bit_eq signed_take_bit_def take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
-
-context semiring_bit_shifts
-begin
-
-lemma unsigned_ucast_eq:
- \<open>unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\<close>
- for w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (simp add: bit_unsigned_iff Conversions.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le)
-
-end
-
-context ring_bit_operations
-begin
-
-lemma signed_ucast_eq:
- \<open>signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\<close>
- for w :: \<open>'b::len word\<close>
-proof (rule bit_eqI)
- fix n
- assume \<open>2 ^ n \<noteq> 0\<close>
- then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
- by (simp add: min_def)
- (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero)
- then show \<open>bit (signed (ucast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\<close>
- by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
-qed
-
-lemma signed_scast_eq:
- \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
- for w :: \<open>'b::len word\<close>
-proof (rule bit_eqI)
- fix n
- assume \<open>2 ^ n \<noteq> 0\<close>
- then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
- by (simp add: min_def)
- (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero)
- then show \<open>bit (signed (scast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\<close>
- by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
-qed
-
-end
-
-end
--- a/src/HOL/Word/More_Word.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Word/More_Word.thy Thu Sep 17 18:48:37 2020 +0100
@@ -42,6 +42,11 @@
lemmas uint_mod_same = uint_idem
lemmas of_nth_def = word_set_bits_def
+lemmas of_nat_word_eq_iff = word_of_nat_eq_iff
+lemmas of_nat_word_eq_0_iff = word_of_nat_eq_0_iff
+lemmas of_int_word_eq_iff = word_of_int_eq_iff
+lemmas of_int_word_eq_0_iff = word_of_int_eq_0_iff
+
lemma shiftl_transfer [transfer_rule]:
includes lifting_syntax
shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)"
--- a/src/HOL/Word/Word.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/Word/Word.thy Thu Sep 17 18:48:37 2020 +0100
@@ -129,16 +129,29 @@
\<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
by transfer simp
+lemma exp_eq_zero_iff:
+ \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
+ by transfer simp
+
subsubsection \<open>Basic code generation setup\<close>
-lift_definition uint :: \<open>'a::len word \<Rightarrow> int\<close>
+context
+begin
+
+qualified lift_definition the_int :: \<open>'a::len word \<Rightarrow> int\<close>
is \<open>take_bit LENGTH('a)\<close> .
+end
+
lemma [code abstype]:
- \<open>Word.Word (uint w) = w\<close>
+ \<open>Word.Word (Word.the_int w) = w\<close>
by transfer simp
+lemma Word_eq_word_of_int [code_post, simp]:
+ \<open>Word.Word = of_int\<close>
+ by (rule; transfer) simp
+
quickcheck_generator word
constructors:
\<open>0 :: 'a::len word\<close>,
@@ -157,71 +170,326 @@
end
lemma [code]:
- \<open>HOL.equal v w \<longleftrightarrow> HOL.equal (uint v) (uint w)\<close>
+ \<open>HOL.equal v w \<longleftrightarrow> HOL.equal (Word.the_int v) (Word.the_int w)\<close>
by transfer (simp add: equal)
lemma [code]:
- \<open>uint 0 = 0\<close>
+ \<open>Word.the_int 0 = 0\<close>
by transfer simp
lemma [code]:
- \<open>uint 1 = 1\<close>
+ \<open>Word.the_int 1 = 1\<close>
by transfer simp
lemma [code]:
- \<open>uint (v + w) = take_bit LENGTH('a) (uint v + uint w)\<close>
+ \<open>Word.the_int (v + w) = take_bit LENGTH('a) (Word.the_int v + Word.the_int w)\<close>
for v w :: \<open>'a::len word\<close>
by transfer (simp add: take_bit_add)
lemma [code]:
- \<open>uint (- w) = (let k = uint w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\<close>
+ \<open>Word.the_int (- w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\<close>
for w :: \<open>'a::len word\<close>
by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if)
lemma [code]:
- \<open>uint (v - w) = take_bit LENGTH('a) (uint v - uint w)\<close>
+ \<open>Word.the_int (v - w) = take_bit LENGTH('a) (Word.the_int v - Word.the_int w)\<close>
for v w :: \<open>'a::len word\<close>
by transfer (simp add: take_bit_diff)
lemma [code]:
- \<open>uint (v * w) = take_bit LENGTH('a) (uint v * uint w)\<close>
+ \<open>Word.the_int (v * w) = take_bit LENGTH('a) (Word.the_int v * Word.the_int w)\<close>
for v w :: \<open>'a::len word\<close>
by transfer (simp add: take_bit_mult)
subsubsection \<open>Basic conversions\<close>
-lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
- is \<open>\<lambda>k. k\<close> .
-
-lift_definition unat :: \<open>'a::len word \<Rightarrow> nat\<close>
- is \<open>nat \<circ> take_bit LENGTH('a)\<close>
+abbreviation word_of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close>
+ where \<open>word_of_nat \<equiv> of_nat\<close>
+
+abbreviation word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
+ where \<open>word_of_int \<equiv> of_int\<close>
+
+lemma word_of_nat_eq_iff:
+ \<open>word_of_nat m = (word_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 word_of_int_eq_iff:
+ \<open>word_of_int k = (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+ by transfer rule
+
+lemma word_of_nat_eq_0_iff [simp]:
+ \<open>word_of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
+ using word_of_nat_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
+
+lemma word_of_int_eq_0_iff [simp]:
+ \<open>word_of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
+ using word_of_int_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
+
+context semiring_1
+begin
+
+lift_definition unsigned :: \<open>'b::len word \<Rightarrow> 'a\<close>
+ is \<open>of_nat \<circ> nat \<circ> take_bit LENGTH('b)\<close>
by simp
-lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close>
- \<comment> \<open>treats the most-significant bit as a sign bit\<close>
- is \<open>signed_take_bit (LENGTH('a) - 1)\<close>
- by (simp add: signed_take_bit_decr_length_iff)
+lemma unsigned_0 [simp]:
+ \<open>unsigned 0 = 0\<close>
+ by transfer simp
+
+lemma unsigned_1 [simp]:
+ \<open>unsigned 1 = 1\<close>
+ by transfer simp
+
+lemma unsigned_numeral [simp]:
+ \<open>unsigned (numeral n :: 'b::len word) = of_nat (take_bit LENGTH('b) (numeral n))\<close>
+ by transfer (simp add: nat_take_bit_eq)
+
+lemma unsigned_neg_numeral [simp]:
+ \<open>unsigned (- numeral n :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) (- numeral n)))\<close>
+ by transfer simp
+
+end
+
+context semiring_1
+begin
+
+lemma unsigned_of_nat [simp]:
+ \<open>unsigned (word_of_nat n :: 'b::len word) = of_nat (take_bit LENGTH('b) n)\<close>
+ by transfer (simp add: nat_eq_iff take_bit_of_nat)
+
+lemma unsigned_of_int [simp]:
+ \<open>unsigned (word_of_int k :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) k))\<close>
+ by transfer simp
+
+end
+
+context semiring_char_0
+begin
+
+lemma unsigned_word_eqI:
+ \<open>v = w\<close> if \<open>unsigned v = unsigned w\<close>
+ using that by transfer (simp add: eq_nat_nat_iff)
+
+lemma word_eq_iff_unsigned:
+ \<open>v = w \<longleftrightarrow> unsigned v = unsigned w\<close>
+ by (auto intro: unsigned_word_eqI)
+
+end
+
+context ring_1
+begin
+
+lift_definition signed :: \<open>'b::len word \<Rightarrow> 'a\<close>
+ is \<open>of_int \<circ> signed_take_bit (LENGTH('b) - Suc 0)\<close>
+ by (simp flip: signed_take_bit_decr_length_iff)
+
+lemma signed_0 [simp]:
+ \<open>signed 0 = 0\<close>
+ by transfer simp
+
+lemma signed_1 [simp]:
+ \<open>signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\<close>
+ by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>)
+ (simp_all add: sbintrunc_minus_simps)
+
+lemma signed_minus_1 [simp]:
+ \<open>signed (- 1 :: 'b::len word) = - 1\<close>
+ by (transfer fixing: uminus) simp
+
+lemma signed_numeral [simp]:
+ \<open>signed (numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (numeral n))\<close>
+ by transfer simp
+
+lemma signed_neg_numeral [simp]:
+ \<open>signed (- numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (- numeral n))\<close>
+ by transfer simp
+
+lemma signed_of_nat [simp]:
+ \<open>signed (word_of_nat n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) (int n))\<close>
+ by transfer simp
+
+lemma signed_of_int [simp]:
+ \<open>signed (word_of_int n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) n)\<close>
+ by transfer simp
+
+end
+
+context ring_char_0
+begin
+
+lemma signed_word_eqI:
+ \<open>v = w\<close> if \<open>signed v = signed w\<close>
+ using that by transfer (simp flip: signed_take_bit_decr_length_iff)
+
+lemma word_eq_iff_signed:
+ \<open>v = w \<longleftrightarrow> signed v = signed w\<close>
+ by (auto intro: signed_word_eqI)
+
+end
+
+abbreviation unat :: \<open>'a::len word \<Rightarrow> nat\<close>
+ where \<open>unat \<equiv> unsigned\<close>
+
+abbreviation uint :: \<open>'a::len word \<Rightarrow> int\<close>
+ where \<open>uint \<equiv> unsigned\<close>
+
+abbreviation sint :: \<open>'a::len word \<Rightarrow> int\<close>
+ where \<open>sint \<equiv> signed\<close>
+
+abbreviation ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+ where \<open>ucast \<equiv> unsigned\<close>
+
+abbreviation scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+ where \<open>scast \<equiv> signed\<close>
+
+context
+ includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+ \<open>(pcr_word ===> (=)) (nat \<circ> take_bit LENGTH('a)) (unat :: 'a::len word \<Rightarrow> nat)\<close>
+ using unsigned.transfer [where ?'a = nat] by simp
+
+lemma [transfer_rule]:
+ \<open>(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \<Rightarrow> int)\<close>
+ using unsigned.transfer [where ?'a = int] by (simp add: comp_def)
+
+lemma [transfer_rule]:
+ \<open>(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word \<Rightarrow> int)\<close>
+ using signed.transfer [where ?'a = int] by simp
+
+lemma [transfer_rule]:
+ \<open>(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
+proof (rule rel_funI)
+ fix k :: int and w :: \<open>'a word\<close>
+ assume \<open>pcr_word k w\<close>
+ then have \<open>w = word_of_int k\<close>
+ by (simp add: pcr_word_def cr_word_def relcompp_apply)
+ moreover have \<open>pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\<close>
+ by transfer (simp add: pcr_word_def cr_word_def relcompp_apply)
+ ultimately show \<open>pcr_word (take_bit LENGTH('a) k) (ucast w)\<close>
+ by simp
+qed
+
+lemma [transfer_rule]:
+ \<open>(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
+proof (rule rel_funI)
+ fix k :: int and w :: \<open>'a word\<close>
+ assume \<open>pcr_word k w\<close>
+ then have \<open>w = word_of_int k\<close>
+ by (simp add: pcr_word_def cr_word_def relcompp_apply)
+ moreover have \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))\<close>
+ by transfer (simp add: pcr_word_def cr_word_def relcompp_apply)
+ ultimately show \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)\<close>
+ by simp
+qed
+
+end
+
+lemma of_nat_unat [simp]:
+ \<open>of_nat (unat w) = unsigned w\<close>
+ by transfer simp
+
+lemma of_int_uint [simp]:
+ \<open>of_int (uint w) = unsigned w\<close>
+ by transfer simp
+
+lemma of_int_sint [simp]:
+ \<open>of_int (sint a) = signed a\<close>
+ by transfer (simp_all add: take_bit_signed_take_bit)
lemma nat_uint_eq [simp]:
\<open>nat (uint w) = unat w\<close>
by transfer simp
-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>
+text \<open>Aliasses only for code generation\<close>
+
+context
+begin
+
+qualified lift_definition of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
+ is \<open>take_bit LENGTH('a)\<close> .
+
+qualified lift_definition of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close>
+ is \<open>int \<circ> take_bit LENGTH('a)\<close> .
+
+qualified lift_definition the_nat :: \<open>'a::len word \<Rightarrow> nat\<close>
+ is \<open>nat \<circ> take_bit LENGTH('a)\<close> by simp
+
+qualified lift_definition the_signed_int :: \<open>'a::len word \<Rightarrow> int\<close>
+ is \<open>signed_take_bit (LENGTH('a) - Suc 0)\<close> by (simp add: signed_take_bit_decr_length_iff)
+
+qualified lift_definition cast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+ is \<open>take_bit LENGTH('a)\<close> by simp
+
+qualified lift_definition signed_cast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+ is \<open>signed_take_bit (LENGTH('a) - Suc 0)\<close> by (metis signed_take_bit_decr_length_iff)
+
+end
+
+lemma [code_abbrev, simp]:
+ \<open>Word.the_int = uint\<close>
+ by transfer rule
+
+lemma [code]:
+ \<open>Word.the_int (Word.of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close>
+ by transfer simp
+
+lemma [code_abbrev, simp]:
+ \<open>Word.of_int = word_of_int\<close>
+ by (rule; transfer) simp
+
+lemma [code]:
+ \<open>Word.the_int (Word.of_nat n :: 'a::len word) = take_bit LENGTH('a) (int 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_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)
+lemma [code_abbrev, simp]:
+ \<open>Word.of_nat = word_of_nat\<close>
+ by (rule; transfer) (simp add: take_bit_of_nat)
+
+lemma [code]:
+ \<open>Word.the_nat w = nat (Word.the_int w)\<close>
+ by transfer simp
+
+lemma [code_abbrev, simp]:
+ \<open>Word.the_nat = unat\<close>
+ by (rule; transfer) simp
+
+lemma [code]:
+ \<open>Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer simp
+
+lemma [code_abbrev, simp]:
+ \<open>Word.the_signed_int = sint\<close>
+ by (rule; transfer) simp
+
+lemma [code]:
+ \<open>Word.the_int (Word.cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_int w)\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer simp
+
+lemma [code_abbrev, simp]:
+ \<open>Word.cast = ucast\<close>
+ by (rule; transfer) simp
+
+lemma [code]:
+ \<open>Word.the_int (Word.signed_cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_signed_int w)\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer simp
+
+lemma [code_abbrev, simp]:
+ \<open>Word.signed_cast = scast\<close>
+ by (rule; transfer) simp
+
+lemma [code]:
+ \<open>unsigned w = of_nat (nat (Word.the_int w))\<close>
+ by transfer simp
+
+lemma [code]:
+ \<open>signed w = of_int (Word.the_signed_int w)\<close>
+ by transfer simp
subsubsection \<open>Basic ordering\<close>
@@ -248,6 +516,22 @@
interpretation word_coorder: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0 :: 'a::len word\<close>
by (standard; transfer) simp
+lemma word_of_nat_less_eq_iff:
+ \<open>word_of_nat m \<le> (word_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 word_of_int_less_eq_iff:
+ \<open>word_of_int k \<le> (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
+ by transfer rule
+
+lemma word_of_nat_less_iff:
+ \<open>word_of_nat m < (word_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 word_of_int_less_iff:
+ \<open>word_of_int k < (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
+ by transfer rule
+
lemma word_le_def [code]:
"a \<le> b \<longleftrightarrow> uint a \<le> uint b"
by transfer rule
@@ -331,16 +615,16 @@
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>
+ and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> P (2 * a)\<close>
+ and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - Suc 0) \<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>
+ define m :: nat where \<open>m = LENGTH('a) - Suc 0\<close>
then have l: \<open>LENGTH('a) = Suc m\<close>
by simp
define n :: nat where \<open>n = unat a\<close>
then have \<open>n < 2 ^ LENGTH('a)\<close>
- by (unfold unat_def) (transfer, simp add: take_bit_eq_mod)
+ by transfer (simp add: take_bit_eq_mod)
then have \<open>n < 2 * 2 ^ m\<close>
by (simp add: l)
then have \<open>P (of_nat n)\<close>
@@ -355,10 +639,10 @@
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>
+ by (auto simp add: word_greater_zero_iff l)
+ moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\<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)
+ by (simp add: l take_bit_eq_mod)
ultimately have \<open>P (2 * of_nat n)\<close>
by (rule word_even)
then show ?case
@@ -369,9 +653,9 @@
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>
+ moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\<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)
+ by (simp add: l take_bit_eq_mod)
ultimately have \<open>P (1 + 2 * of_nat n)\<close>
by (rule word_odd)
then show ?case
@@ -556,6 +840,20 @@
end
+lemma bit_word_eqI:
+ \<open>a = b\<close> if \<open>\<And>n. n < LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
+ for a b :: \<open>'a::len word\<close>
+ using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff)
+
+lemma bit_imp_le_length:
+ \<open>n < LENGTH('a)\<close> if \<open>bit w n\<close>
+ for w :: \<open>'a::len word\<close>
+ using that by transfer simp
+
+lemma not_bit_length [simp]:
+ \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
+ by transfer simp
+
instantiation word :: (len) semiring_bit_shifts
begin
@@ -595,45 +893,426 @@
end
-lemma bit_word_eqI:
- \<open>a = b\<close> if \<open>\<And>n. n < LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
- for a b :: \<open>'a::len word\<close>
- using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff)
-
-lemma bit_imp_le_length:
- \<open>n < LENGTH('a)\<close> if \<open>bit w n\<close>
- for w :: \<open>'a::len word\<close>
- using that by transfer simp
-
-lemma not_bit_length [simp]:
- \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
+lemma [code]:
+ \<open>Word.the_int (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (Word.the_int w) else Word.the_int w)\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer (simp add: not_le not_less ac_simps min_absorb2)
+
+
+instantiation word :: (len) ring_bit_operations
+begin
+
+lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close>
+ is not
+ by (simp add: take_bit_not_iff)
+
+lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is \<open>and\<close>
+ by simp
+
+lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is or
+ by simp
+
+lift_definition xor_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is xor
+ by simp
+
+lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
+ is mask
+ .
+
+instance by (standard; transfer)
+ (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+ bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
+
+end
+
+lemma [code_abbrev]:
+ \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
+ by (fact push_bit_of_1)
+
+lemma [code]:
+ \<open>NOT w = Word.of_int (NOT (Word.the_int w))\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer (simp add: take_bit_not_take_bit)
+
+lemma [code]:
+ \<open>Word.the_int (v AND w) = Word.the_int v AND Word.the_int w\<close>
by transfer simp
+lemma [code]:
+ \<open>Word.the_int (v OR w) = Word.the_int v OR Word.the_int w\<close>
+ by transfer simp
+
+lemma [code]:
+ \<open>Word.the_int (v XOR w) = Word.the_int v XOR Word.the_int w\<close>
+ by transfer simp
+
+lemma [code]:
+ \<open>Word.the_int (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close>
+ by transfer simp
+
+context
+ includes lifting_syntax
+begin
+
+lemma set_bit_word_transfer [transfer_rule]:
+ \<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close>
+ by (unfold set_bit_def) transfer_prover
+
+lemma unset_bit_word_transfer [transfer_rule]:
+ \<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close>
+ by (unfold unset_bit_def) transfer_prover
+
+lemma flip_bit_word_transfer [transfer_rule]:
+ \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close>
+ by (unfold flip_bit_def) transfer_prover
+
+lemma signed_take_bit_word_transfer [transfer_rule]:
+ \<open>((=) ===> pcr_word ===> pcr_word)
+ (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))
+ (signed_take_bit :: nat \<Rightarrow> 'a word \<Rightarrow> 'a word)\<close>
+proof -
+ let ?K = \<open>\<lambda>n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \<and> bit k n) * NOT (mask n)\<close>
+ let ?W = \<open>\<lambda>n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\<close>
+ have \<open>((=) ===> pcr_word ===> pcr_word) ?K ?W\<close>
+ by transfer_prover
+ also have \<open>?K = (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))\<close>
+ by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps)
+ also have \<open>?W = signed_take_bit\<close>
+ by (simp add: fun_eq_iff signed_take_bit_def)
+ finally show ?thesis .
+qed
+
+end
+
subsection \<open>Conversions including casts\<close>
+subsubsection \<open>Generic unsigned conversion\<close>
+
+context semiring_bits
+begin
+
+lemma bit_unsigned_iff:
+ \<open>bit (unsigned w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w n\<close>
+ for w :: \<open>'b::len word\<close>
+ by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)
+
+end
+
+context semiring_bit_shifts
+begin
+
+lemma unsigned_push_bit_eq:
+ \<open>unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix m
+ assume \<open>2 ^ m \<noteq> 0\<close>
+ show \<open>bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\<close>
+ proof (cases \<open>n \<le> m\<close>)
+ case True
+ with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
+ by (metis (full_types) diff_add exp_add_not_zero_imp)
+ with True show ?thesis
+ by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff not_le exp_eq_zero_iff ac_simps)
+ next
+ case False
+ then show ?thesis
+ by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff)
+ qed
+qed
+
+lemma unsigned_take_bit_eq:
+ \<open>unsigned (take_bit n w) = take_bit n (unsigned w)\<close>
+ for w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff)
+
+end
+
+context semiring_bit_operations
+begin
+
+lemma unsigned_and_eq:
+ \<open>unsigned (v AND w) = unsigned v AND unsigned w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma unsigned_or_eq:
+ \<open>unsigned (v OR w) = unsigned v OR unsigned w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma unsigned_xor_eq:
+ \<open>unsigned (v XOR w) = unsigned v XOR unsigned w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma unsigned_not_eq:
+ \<open>unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\<close>
+ for w :: \<open>'b::len word\<close>
+ by (rule bit_eqI)
+ (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le)
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma unsigned_greater_eq:
+ \<open>0 \<le> unsigned w\<close> for w :: \<open>'b::len word\<close>
+ by (transfer fixing: less_eq) simp
+
+lemma unsigned_less:
+ \<open>unsigned w < 2 ^ LENGTH('b)\<close> for w :: \<open>'b::len word\<close>
+ by (transfer fixing: less) simp
+
+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
+
+
+subsubsection \<open>Generic signed conversion\<close>
+
+context ring_bit_operations
+begin
+
+lemma bit_signed_iff:
+ \<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
+ for w :: \<open>'b::len word\<close>
+ by (transfer fixing: bit)
+ (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
+
+lemma signed_push_bit_eq:
+ \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix m
+ assume \<open>2 ^ m \<noteq> 0\<close>
+ define q where \<open>q = LENGTH('b) - Suc 0\<close>
+ then have *: \<open>LENGTH('b) = Suc q\<close>
+ by simp
+ show \<open>bit (signed (push_bit n w)) m \<longleftrightarrow>
+ bit (signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))) m\<close>
+ proof (cases \<open>q \<le> m\<close>)
+ case True
+ moreover define r where \<open>r = m - q\<close>
+ ultimately have \<open>m = q + r\<close>
+ by simp
+ moreover from \<open>m = q + r\<close> \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ r \<noteq> 0\<close>
+ using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r]
+ by simp_all
+ moreover from \<open>2 ^ q \<noteq> 0\<close> have \<open>2 ^ (q - n) \<noteq> 0\<close>
+ by (rule exp_not_zero_imp_exp_diff_not_zero)
+ ultimately show ?thesis
+ by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
+ min_def * exp_eq_zero_iff le_diff_conv2)
+ next
+ case False
+ then show ?thesis
+ using exp_not_zero_imp_exp_diff_not_zero [of m n]
+ by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
+ min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit
+ exp_eq_zero_iff)
+ qed
+qed
+
+lemma signed_take_bit_eq:
+ \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
+ for w :: \<open>'b::len word\<close>
+ by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
+ (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
+
+lemma signed_not_eq:
+ \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix n
+ assume \<open>2 ^ n \<noteq> 0\<close>
+ define q where \<open>q = LENGTH('b) - Suc 0\<close>
+ then have *: \<open>LENGTH('b) = Suc q\<close>
+ by simp
+ show \<open>bit (signed (NOT w)) n \<longleftrightarrow>
+ bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\<close>
+ proof (cases \<open>q < n\<close>)
+ case True
+ moreover define r where \<open>r = n - Suc q\<close>
+ ultimately have \<open>n = r + Suc q\<close>
+ by simp
+ moreover from \<open>2 ^ n \<noteq> 0\<close> \<open>n = r + Suc q\<close>
+ have \<open>2 ^ Suc q \<noteq> 0\<close>
+ using exp_add_not_zero_imp_right by blast
+ ultimately show ?thesis
+ by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
+ exp_eq_zero_iff)
+ next
+ case False
+ then show ?thesis
+ by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
+ exp_eq_zero_iff)
+ qed
+qed
+
+lemma signed_and_eq:
+ \<open>signed (v AND w) = signed v AND signed w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma signed_or_eq:
+ \<open>signed (v OR w) = signed v OR signed w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma signed_xor_eq:
+ \<open>signed (v XOR w) = signed v XOR signed w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+end
+
+
+subsubsection \<open>More\<close>
+
+lemma sint_greater_eq:
+ \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
+proof (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>)
+ case True
+ then show ?thesis
+ by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps)
+next
+ have *: \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> (0::int)\<close>
+ by simp
+ case False
+ then show ?thesis
+ by transfer (auto simp add: signed_take_bit_eq intro: order_trans *)
+qed
+
+lemma sint_less:
+ \<open>sint w < 2 ^ (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
+ by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
+ (simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper)
+
+lemma unat_div_distrib:
+ \<open>unat (v div w) = unat v div unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule div_le_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
+qed
+
+lemma unat_mod_distrib:
+ \<open>unat (v mod w) = unat v mod unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule mod_less_eq_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
+qed
+
+lemma uint_div_distrib:
+ \<open>uint (v div w) = uint v div uint w\<close>
+proof -
+ have \<open>int (unat (v div w)) = int (unat v div unat w)\<close>
+ by (simp add: unat_div_distrib)
+ then show ?thesis
+ by (simp add: of_nat_div)
+qed
+
+lemma uint_mod_distrib:
+ \<open>uint (v mod w) = uint v mod uint w\<close>
+proof -
+ have \<open>int (unat (v mod w)) = int (unat v mod unat w)\<close>
+ by (simp add: unat_mod_distrib)
+ then show ?thesis
+ by (simp add: of_nat_mod)
+qed
+
+context semiring_bit_shifts
+begin
+
+lemma unsigned_ucast_eq:
+ \<open>unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\<close>
+ for w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma signed_ucast_eq:
+ \<open>signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix n
+ assume \<open>2 ^ n \<noteq> 0\<close>
+ then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
+ by (simp add: min_def)
+ (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero)
+ then show \<open>bit (signed (ucast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\<close>
+ by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+qed
+
+lemma signed_scast_eq:
+ \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix n
+ assume \<open>2 ^ n \<noteq> 0\<close>
+ then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
+ by (simp add: min_def)
+ (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero)
+ then show \<open>bit (signed (scast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\<close>
+ by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+qed
+
+end
+
lemma uint_nonnegative: "0 \<le> uint w"
- by transfer simp
+ by (fact unsigned_greater_eq)
lemma uint_bounded: "uint w < 2 ^ LENGTH('a)"
for w :: "'a::len word"
- by transfer (simp add: take_bit_eq_mod)
+ by (fact unsigned_less)
lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w"
for w :: "'a::len word"
- using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
+ by transfer (simp add: take_bit_eq_mod)
lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b"
- by transfer simp
+ by (fact unsigned_word_eqI)
lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
- using word_uint_eqI by auto
-
-lemma Word_eq_word_of_int [code_post]:
- \<open>Word.Word = word_of_int\<close>
- by rule (transfer, rule)
-
-lemma uint_word_of_int_eq [code]:
+ by (fact word_eq_iff_unsigned)
+
+lemma uint_word_of_int_eq:
\<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close>
by transfer rule
@@ -656,80 +1335,73 @@
fix x :: "'a word"
assume "\<And>x. PROP P (word_of_int x)"
then have "PROP P (word_of_int (uint x))" .
- then show "PROP P x" by (simp add: word_of_int_uint)
+ then show "PROP P x"
+ by (simp only: word_of_int_uint)
qed
-lemma sint_uint [code]:
- \<open>sint w = signed_take_bit (LENGTH('a) - 1) (uint w)\<close>
+lemma sint_uint:
+ \<open>sint w = signed_take_bit (LENGTH('a) - Suc 0) (uint w)\<close>
for w :: \<open>'a::len word\<close>
by (cases \<open>LENGTH('a)\<close>; transfer) (simp_all add: signed_take_bit_take_bit)
-lemma unat_eq_nat_uint [code]:
+lemma unat_eq_nat_uint:
\<open>unat w = nat (uint w)\<close>
by simp
-lift_definition ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
- is \<open>take_bit LENGTH('a)\<close>
- by simp
-
-lemma ucast_eq [code]:
+lemma ucast_eq:
\<open>ucast w = word_of_int (uint w)\<close>
by transfer simp
-lift_definition scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
- is \<open>signed_take_bit (LENGTH('a) - 1)\<close>
- by (simp flip: signed_take_bit_decr_length_iff)
-
-lemma scast_eq [code]:
+lemma scast_eq:
\<open>scast w = word_of_int (sint w)\<close>
by transfer simp
-lemma uint_0_eq [simp]:
+lemma uint_0_eq:
\<open>uint 0 = 0\<close>
- by transfer simp
-
-lemma uint_1_eq [simp]:
+ by (fact unsigned_0)
+
+lemma uint_1_eq:
\<open>uint 1 = 1\<close>
- by transfer simp
+ by (fact unsigned_1)
lemma word_m1_wi: "- 1 = word_of_int (- 1)"
- by transfer rule
+ by simp
lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
- by (simp add: word_uint_eq_iff)
+ by (auto simp add: unsigned_word_eqI)
lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0"
- by transfer (auto intro: antisym)
-
-lemma unat_0 [simp]: "unat 0 = 0"
- by transfer simp
+ by (auto simp add: unsigned_word_eqI)
+
+lemma unat_0: "unat 0 = 0"
+ by (fact unsigned_0)
lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0"
by (auto simp: unat_0_iff [symmetric])
-lemma ucast_0 [simp]: "ucast 0 = 0"
- by transfer simp
-
-lemma sint_0 [simp]: "sint 0 = 0"
- by (simp add: sint_uint)
-
-lemma scast_0 [simp]: "scast 0 = 0"
- by transfer simp
-
-lemma sint_n1 [simp] : "sint (- 1) = - 1"
- by transfer simp
-
-lemma scast_n1 [simp]: "scast (- 1) = - 1"
- by transfer simp
+lemma ucast_0: "ucast 0 = 0"
+ by (fact unsigned_0)
+
+lemma sint_0: "sint 0 = 0"
+ by (fact signed_0)
+
+lemma scast_0: "scast 0 = 0"
+ by (fact signed_0)
+
+lemma sint_n1: "sint (- 1) = - 1"
+ by (fact signed_minus_1)
+
+lemma scast_n1: "scast (- 1) = - 1"
+ by (fact signed_minus_1)
lemma uint_1: "uint (1::'a::len word) = 1"
by (fact uint_1_eq)
-lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
- by transfer simp
-
-lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
- by transfer simp
+lemma unat_1: "unat (1::'a::len word) = 1"
+ by (fact unsigned_1)
+
+lemma ucast_1: "ucast (1::'a::len word) = 1"
+ by (fact unsigned_1)
instantiation word :: (len) size
begin
@@ -851,26 +1523,6 @@
lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
-lemma word_of_nat: "of_nat n = word_of_int (int n)"
- by (induct n) (auto simp add : word_of_int_hom_syms)
-
-lemma word_of_int: "of_int = word_of_int"
- apply (rule ext)
- apply (case_tac x rule: int_diff_cases)
- apply (simp add: word_of_nat wi_hom_sub)
- done
-
-lemma word_of_int_eq:
- "word_of_int = of_int"
- by (rule ext) (transfer, rule)
-
-definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50)
- where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)"
-
-lemma exp_eq_zero_iff:
- \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
- by transfer simp
-
lemma double_eq_zero_iff:
\<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a) - Suc 0)\<close>
for a :: \<open>'a::len word\<close>
@@ -978,8 +1630,7 @@
subsection \<open>Bit-wise operations\<close>
-
-lemma uint_take_bit_eq [code]:
+lemma uint_take_bit_eq:
\<open>uint (take_bit n w) = take_bit n (uint w)\<close>
by transfer (simp add: ac_simps)
@@ -1049,69 +1700,6 @@
\<open>shiftr1 w = word_of_int (uint w div 2)\<close>
by transfer simp
-instantiation word :: (len) ring_bit_operations
-begin
-
-lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close>
- is not
- by (simp add: take_bit_not_iff)
-
-lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
- is \<open>and\<close>
- by simp
-
-lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
- is or
- by simp
-
-lift_definition xor_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
- is xor
- by simp
-
-lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
- is mask
- .
-
-instance by (standard; transfer)
- (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
- bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
-
-end
-
-context
- includes lifting_syntax
-begin
-
-lemma set_bit_word_transfer [transfer_rule]:
- \<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close>
- by (unfold set_bit_def) transfer_prover
-
-lemma unset_bit_word_transfer [transfer_rule]:
- \<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close>
- by (unfold unset_bit_def) transfer_prover
-
-lemma flip_bit_word_transfer [transfer_rule]:
- \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close>
- by (unfold flip_bit_def) transfer_prover
-
-lemma signed_take_bit_word_transfer [transfer_rule]:
- \<open>((=) ===> pcr_word ===> pcr_word)
- (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))
- (signed_take_bit :: nat \<Rightarrow> 'a word \<Rightarrow> 'a word)\<close>
-proof -
- let ?K = \<open>\<lambda>n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \<and> bit k n) * NOT (mask n)\<close>
- let ?W = \<open>\<lambda>n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\<close>
- have \<open>((=) ===> pcr_word ===> pcr_word) ?K ?W\<close>
- by transfer_prover
- also have \<open>?K = (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))\<close>
- by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps)
- also have \<open>?W = signed_take_bit\<close>
- by (simp add: fun_eq_iff signed_take_bit_def)
- finally show ?thesis .
-qed
-
-end
-
instantiation word :: (len) semiring_bit_syntax
begin
@@ -1188,11 +1776,14 @@
\<open>shiftl1 w = w << 1\<close>
by transfer (simp add: push_bit_eq_mult ac_simps)
-lemma uint_shiftr_eq [code]:
+lemma uint_shiftr_eq:
\<open>uint (w >> n) = uint w div 2 ^ n\<close>
- for w :: \<open>'a::len word\<close>
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv)
+lemma [code]:
+ \<open>Word.the_int (w >> n) = drop_bit n (Word.the_int w)\<close>
+ by transfer (simp add: drop_bit_take_bit min_def le_less less_diff_conv)
+
lemma shiftr1_code [code]:
\<open>shiftr1 w = w >> 1\<close>
by transfer (simp add: drop_bit_Suc)
@@ -1232,47 +1823,22 @@
\<open>push_bit n w = w << n\<close> for w :: \<open>'a::len word\<close>
by (simp add: shiftl_word_eq)
+lemma [code]:
+ \<open>drop_bit n w = w >> n\<close> for w :: \<open>'a::len word\<close>
+ by (simp add: shiftr_word_eq)
+
lemma bit_shiftr_word_iff:
\<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close>
for w :: \<open>'a::len word\<close>
by (simp add: shiftr_word_eq bit_drop_bit_eq)
-lemma [code]:
- \<open>drop_bit n w = w >> n\<close> for w :: \<open>'a::len word\<close>
- by (simp add: shiftr_word_eq)
-
-lemma [code]:
- \<open>uint (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (uint w) else uint w)\<close>
- for w :: \<open>'a::len word\<close>
- by transfer (simp add: min_def)
-
-lemma [code]:
- \<open>uint (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close>
- by transfer simp
-
-lemma [code_abbrev]:
- \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
- by (fact push_bit_of_1)
-
lemma
- word_not_def [code]: "NOT (a::'a::len word) = word_of_int (NOT (uint a))"
+ word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))"
and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)"
and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
by (transfer, simp add: take_bit_not_take_bit)+
-lemma [code abstract]:
- \<open>uint (v AND w) = uint v AND uint w\<close>
- by transfer simp
-
-lemma [code abstract]:
- \<open>uint (v OR w) = uint v OR uint w\<close>
- by transfer simp
-
-lemma [code abstract]:
- \<open>uint (v XOR w) = uint v XOR uint w\<close>
- by transfer simp
-
lift_definition setBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
is \<open>\<lambda>k n. set_bit n k\<close>
by (simp add: take_bit_set_bit_eq)
@@ -1327,6 +1893,45 @@
by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp
qed
+lemma
+ take_bit_word_Bit0_eq [simp]: \<open>take_bit (numeral n) (numeral (num.Bit0 m) :: 'a::len word)
+ = 2 * take_bit (pred_numeral n) (numeral m)\<close> (is ?P)
+ and take_bit_word_Bit1_eq [simp]: \<open>take_bit (numeral n) (numeral (num.Bit1 m) :: 'a::len word)
+ = 1 + 2 * take_bit (pred_numeral n) (numeral m)\<close> (is ?Q)
+ and take_bit_word_minus_Bit0_eq [simp]: \<open>take_bit (numeral n) (- numeral (num.Bit0 m) :: 'a::len word)
+ = 2 * take_bit (pred_numeral n) (- numeral m)\<close> (is ?R)
+ and take_bit_word_minus_Bit1_eq [simp]: \<open>take_bit (numeral n) (- numeral (num.Bit1 m) :: 'a::len word)
+ = 1 + 2 * take_bit (pred_numeral n) (- numeral (Num.inc m))\<close> (is ?S)
+proof -
+ define w :: \<open>'a::len word\<close>
+ where \<open>w = numeral m\<close>
+ moreover define q :: nat
+ where \<open>q = pred_numeral n\<close>
+ ultimately have num:
+ \<open>numeral m = w\<close>
+ \<open>numeral (num.Bit0 m) = 2 * w\<close>
+ \<open>numeral (num.Bit1 m) = 1 + 2 * w\<close>
+ \<open>numeral (Num.inc m) = 1 + w\<close>
+ \<open>pred_numeral n = q\<close>
+ \<open>numeral n = Suc q\<close>
+ by (simp_all only: w_def q_def numeral_Bit0 [of m] numeral_Bit1 [of m] ac_simps
+ numeral_inc numeral_eq_Suc flip: mult_2)
+ have even: \<open>take_bit (Suc q) (2 * w) = 2 * take_bit q w\<close> for w :: \<open>'a::len word\<close>
+ by (rule bit_word_eqI)
+ (auto simp add: bit_take_bit_iff bit_double_iff)
+ have odd: \<open>take_bit (Suc q) (1 + 2 * w) = 1 + 2 * take_bit q w\<close> for w :: \<open>'a::len word\<close>
+ by (rule bit_eqI)
+ (auto simp add: bit_take_bit_iff bit_double_iff even_bit_succ_iff)
+ show ?P
+ using even [of w] by (simp add: num)
+ show ?Q
+ using odd [of w] by (simp add: num)
+ show ?R
+ using even [of \<open>- w\<close>] by (simp add: num)
+ show ?S
+ using odd [of \<open>- (1 + w)\<close>] by (simp add: num)
+qed
+
subsection \<open>Type-definition locale instantiations\<close>
@@ -1396,8 +2001,8 @@
"n = LENGTH('a::len) \<Longrightarrow>
td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
apply (standard; transfer)
- apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self)
- apply (simp add: take_bit_eq_mod)
+ apply (simp_all add: unats_def take_bit_of_nat take_bit_nat_eq_self_iff
+ flip: take_bit_eq_mod)
done
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
@@ -1424,16 +2029,7 @@
lemma td_ext_sbin:
"td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
(signed_take_bit (LENGTH('a) - 1))"
- apply (unfold td_ext_def' sint_uint)
- apply (simp add : word_ubin.eq_norm)
- apply (cases "LENGTH('a)")
- apply (auto simp add : sints_def)
- apply (rule sym [THEN trans])
- apply (rule word_ubin.Abs_norm)
- apply (simp only: bintrunc_sbintrunc)
- apply (drule sym)
- apply simp
- done
+ by (standard; transfer) (auto simp add: sints_def)
lemma td_ext_sint:
"td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
@@ -1512,11 +2108,16 @@
\<open>mask n = (1 << n) - (1 :: 'a::len word)\<close>
by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1)
-lemma uint_sshiftr_eq [code]:
+lemma uint_sshiftr_eq:
\<open>uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\<close>
for w :: \<open>'a::len word\<close>
by transfer (simp flip: drop_bit_eq_div)
+lemma [code]:
+ \<open>Word.the_int (w >>> n) = take_bit LENGTH('a) (drop_bit n (Word.the_signed_int w))\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer simp
+
lemma sshift1_code [code]:
\<open>sshiftr1 w = w >>> 1\<close>
by transfer (simp add: drop_bit_Suc)
@@ -1653,7 +2254,7 @@
by simp
qed
-lemma uint_word_rotr_eq [code]:
+lemma uint_word_rotr_eq:
\<open>uint (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a))
(drop_bit (n mod LENGTH('a)) (uint w))
(uint (take_bit (n mod LENGTH('a)) w))\<close>
@@ -1663,6 +2264,13 @@
using mod_less_divisor not_less apply blast
done
+lemma [code]:
+ \<open>Word.the_int (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a))
+ (drop_bit (n mod LENGTH('a)) (Word.the_int w))
+ (Word.the_int (take_bit (n mod LENGTH('a)) w))\<close>
+ for w :: \<open>'a::len word\<close>
+ using uint_word_rotr_eq [of n w] by simp
+
subsection \<open>Split and cat operations\<close>
@@ -1895,33 +2503,7 @@
lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)" (is \<open>?P \<longleftrightarrow> ?Q\<close>)
for x y :: "'a::len word"
-proof
- assume ?P
- then show ?Q
- by simp
-next
- assume ?Q
- then have *: \<open>bit (uint x) n \<longleftrightarrow> bit (uint y) n\<close> if \<open>n < LENGTH('a)\<close> for n
- using that by (simp add: word_test_bit_def)
- show ?P
- proof (rule word_uint_eqI, rule bit_eqI, rule iffI)
- fix n
- assume \<open>bit (uint x) n\<close>
- then have \<open>n < LENGTH('a)\<close>
- by (simp add: bit_take_bit_iff uint.rep_eq)
- with * \<open>bit (uint x) n\<close>
- show \<open>bit (uint y) n\<close>
- by simp
- next
- fix n
- assume \<open>bit (uint y) n\<close>
- then have \<open>n < LENGTH('a)\<close>
- by (simp add: bit_take_bit_iff uint.rep_eq)
- with * \<open>bit (uint y) n\<close>
- show \<open>bit (uint x) n\<close>
- by simp
- qed
-qed
+ by transfer (auto simp add: bit_eq_iff bit_take_bit_iff)
lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v"
for u :: "'a::len word"
@@ -2139,9 +2721,6 @@
subsection \<open>Word Arithmetic\<close>
-lemma udvdI: "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
- by (auto simp: udvd_def)
-
lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b
lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b
lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b
@@ -2182,9 +2761,7 @@
and "uint (word_pred a) = (uint a - 1) mod 2 ^ LENGTH('a)"
and "uint (0 :: 'a word) = 0 mod 2 ^ LENGTH('a)"
and "uint (1 :: 'a word) = 1 mod 2 ^ LENGTH('a)"
- apply (simp_all only: word_arith_wis)
- apply (simp_all add: word_uint.eq_norm)
- done
+ by (simp_all only: word_arith_wis uint_word_of_int_eq flip: take_bit_eq_mod)
lemma uint_word_arith_bintrs:
fixes a b :: "'a::len word"
@@ -2238,23 +2815,89 @@
subsection \<open>Order on fixed-length words\<close>
-lemma udvd_nat_alt: "a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. unat b = n * unat a)"
- supply nat_uint_eq [simp del]
- apply (unfold udvd_def)
- apply safe
- apply (simp add: unat_eq_nat_uint nat_mult_distrib)
- apply (simp add: uint_nat)
- apply (rule exI)
- apply safe
- prefer 2
- apply (erule notE)
- apply (rule refl)
- apply force
+lift_definition udvd :: \<open>'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool\<close> (infixl \<open>udvd\<close> 50)
+ is \<open>\<lambda>k l. take_bit LENGTH('a) k dvd take_bit LENGTH('a) l\<close> by simp
+
+lemma udvd_iff_dvd:
+ \<open>x udvd y \<longleftrightarrow> unat x dvd unat y\<close>
+ by transfer (simp add: nat_dvd_iff)
+
+lemma udvd_iff_dvd_int:
+ \<open>v udvd w \<longleftrightarrow> uint v dvd uint w\<close>
+ by transfer rule
+
+lemma udvdI [intro]:
+ \<open>v udvd w\<close> if \<open>unat w = unat v * unat u\<close>
+proof -
+ from that have \<open>unat v dvd unat w\<close> ..
+ then show ?thesis
+ by (simp add: udvd_iff_dvd)
+qed
+
+lemma udvdE [elim]:
+ fixes v w :: \<open>'a::len word\<close>
+ assumes \<open>v udvd w\<close>
+ obtains u :: \<open>'a word\<close> where \<open>unat w = unat v * unat u\<close>
+proof (cases \<open>v = 0\<close>)
+ case True
+ moreover from True \<open>v udvd w\<close> have \<open>w = 0\<close>
+ by transfer simp
+ ultimately show thesis
+ using that by simp
+next
+ case False
+ then have \<open>unat v > 0\<close>
+ by (simp add: unat_gt_0)
+ from \<open>v udvd w\<close> have \<open>unat v dvd unat w\<close>
+ by (simp add: udvd_iff_dvd)
+ then obtain n where \<open>unat w = unat v * n\<close> ..
+ moreover have \<open>n < 2 ^ LENGTH('a)\<close>
+ proof (rule ccontr)
+ assume \<open>\<not> n < 2 ^ LENGTH('a)\<close>
+ then have \<open>n \<ge> 2 ^ LENGTH('a)\<close>
+ by (simp add: not_le)
+ then have \<open>unat v * n \<ge> 2 ^ LENGTH('a)\<close>
+ using \<open>unat v > 0\<close> mult_le_mono [of 1 \<open>unat v\<close> \<open>2 ^ LENGTH('a)\<close> n]
+ by simp
+ with \<open>unat w = unat v * n\<close> unat_lt2p [of w]
+ show False
+ by simp
+ qed
+ ultimately have \<open>unat w = unat v * unat (word_of_nat n :: 'a word)\<close>
+ by (auto simp add: take_bit_nat_eq_self_iff intro: sym)
+ with that show thesis .
+qed
+
+lemma udvd_imp_mod_eq_0:
+ \<open>w mod v = 0\<close> if \<open>v udvd w\<close>
+ using that by transfer simp
+
+lemma mod_eq_0_imp_udvd [intro?]:
+ \<open>v udvd w\<close> if \<open>w mod v = 0\<close>
+proof -
+ from that have \<open>unat (w mod v) = unat 0\<close>
+ by simp
+ then have \<open>unat w mod unat v = 0\<close>
+ by (simp add: unat_mod_distrib)
+ then have \<open>unat v dvd unat w\<close> ..
+ then show ?thesis
+ by (simp add: udvd_iff_dvd)
+qed
+
+lemma udvd_nat_alt:
+ \<open>a udvd b \<longleftrightarrow> (\<exists>n. unat b = n * unat a)\<close>
+ by (auto simp add: udvd_iff_dvd)
+
+lemma udvd_unfold_int:
+ \<open>a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. uint b = n * uint a)\<close>
+ apply (auto elim!: dvdE simp add: udvd_iff_dvd)
+ apply (simp only: uint_nat)
+ apply auto
+ using of_nat_0_le_iff apply blast
+ apply (simp only: unat_eq_nat_uint)
+ apply (simp add: nat_mult_distrib)
done
-lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y"
- unfolding dvd_def udvd_nat_alt by force
-
lemma unat_minus_one:
\<open>unat (w - 1) = unat w - 1\<close> if \<open>w \<noteq> 0\<close>
proof -
@@ -2299,7 +2942,7 @@
by (metis mod_pos_pos_trivial uint_lt2p uint_mult_ge0 uint_word_ariths(3))
lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
- by (metis (mono_tags, hide_lams) diff_ge_0_iff_ge mod_pos_pos_trivial of_nat_0_le_iff take_bit_eq_mod uint_nat uint_sub_lt2p word_sub_wi word_ubin.eq_norm) find_theorems uint \<open>- _\<close>
+ by (metis (mono_tags, hide_lams) diff_ge_0_iff_ge mod_pos_pos_trivial of_nat_0_le_iff take_bit_eq_mod uint_nat uint_sub_lt2p word_sub_wi word_ubin.eq_norm)
lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend)
@@ -2358,14 +3001,12 @@
lemma uint_split:
"P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)"
for x :: "'a::len word"
- by transfer (auto simp add: take_bit_eq_mod take_bit_int_less_exp)
+ by transfer (auto simp add: take_bit_eq_mod)
lemma uint_split_asm:
"P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<and> \<not> P i)"
for x :: "'a::len word"
- by (auto dest!: word_of_int_inverse
- simp: int_word_uint
- split: uint_split)
+ by auto (metis take_bit_int_eq_self_iff)
lemmas uint_splits = uint_split uint_split_asm
@@ -2569,7 +3210,7 @@
lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
lemma udvd_minus_le': "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy \<le> k - z"
- apply (unfold udvd_def)
+ apply (unfold udvd_unfold_int)
apply clarify
apply (erule (2) udvd_decr0)
done
@@ -2578,7 +3219,7 @@
"p < a + s \<Longrightarrow> a \<le> a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a \<le> p \<Longrightarrow>
0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s"
supply [[simproc del: linordered_ring_less_cancel_factor]]
- apply (unfold udvd_def)
+ apply (unfold udvd_unfold_int)
apply clarify
apply (simp add: uint_arith_simps split: if_split_asm)
prefer 2
@@ -2603,7 +3244,7 @@
word_zero_le [THEN leD, THEN antisym_conv1]
lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
- by (simp add: word_of_int)
+ by simp
text \<open>
note that \<open>iszero_def\<close> is only for class \<open>comm_semiring_1_cancel\<close>,
@@ -2654,10 +3295,10 @@
by simp
lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)"
- by (simp add: word_of_nat wi_hom_mult)
+ by (simp add: wi_hom_mult)
lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)"
- by (simp add: word_of_nat wi_hom_succ ac_simps)
+ by transfer (simp add: ac_simps)
lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
by simp
@@ -2679,10 +3320,10 @@
by (subst Abs_fnat_hom_Suc [symmetric]) simp
lemma word_arith_nat_div: "a div b = of_nat (unat a div unat b)"
- by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
-
+ by (metis of_int_of_nat_eq of_nat_unat of_nat_div word_div_def)
+
lemma word_arith_nat_mod: "a mod b = of_nat (unat a mod unat b)"
- by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
+ by (metis of_int_of_nat_eq of_nat_mod of_nat_unat word_mod_def)
lemmas word_arith_nat_defs =
word_arith_nat_add word_arith_nat_mult
@@ -2758,30 +3399,30 @@
lemma uint_div:
\<open>uint (x div y) = uint x div uint y\<close>
- by (metis div_le_dividend le_less_trans mod_less uint_nat unat_lt2p unat_word_ariths(6) zdiv_int)
+ by (fact uint_div_distrib)
lemma unat_div:
\<open>unat (x div y) = unat x div unat y\<close>
- by (simp add: uint_div nat_div_distrib flip: nat_uint_eq)
+ by (fact unat_div_distrib)
lemma uint_mod:
\<open>uint (x mod y) = uint x mod uint y\<close>
- by (metis (no_types, lifting) le_less_trans mod_by_0 mod_le_divisor mod_less neq0_conv uint_nat unat_lt2p unat_word_ariths(7) zmod_int)
+ by (fact uint_mod_distrib)
lemma unat_mod:
\<open>unat (x mod y) = unat x mod unat y\<close>
- by (simp add: uint_mod nat_mod_distrib flip: nat_uint_eq)
+ by (fact unat_mod_distrib)
text \<open>Definition of \<open>unat_arith\<close> tactic\<close>
lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)"
for x :: "'a::len word"
- by (auto simp: unat_of_nat)
+ by auto (metis take_bit_nat_eq_self_iff)
lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)"
for x :: "'a::len word"
- by (auto simp: unat_of_nat)
+ by auto (metis take_bit_nat_eq_self_iff)
lemmas of_nat_inverse =
word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
@@ -3236,29 +3877,14 @@
by transfer (simp add: bin_sc_eq)
lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
- by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin)
+ by transfer (auto simp add: bit_exp_iff)
lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a::len)"
- by (simp add: test_bit_2p [symmetric] word_of_int [symmetric])
+ by transfer (auto simp add: bit_exp_iff)
lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
- apply (unfold word_arith_power_alt)
- apply (case_tac "LENGTH('a)")
- apply clarsimp
- apply (case_tac "nat")
- apply clarsimp
- apply (case_tac "n")
- apply clarsimp
- apply clarsimp
- apply (drule word_gt_0 [THEN iffD1])
- apply (safe intro!: word_eqI)
- apply (auto simp add: nth_2p_bin)
- apply (erule notE)
- apply (simp (no_asm_use) add: uint_word_of_int word_size)
- apply (subst mod_pos_pos_trivial)
- apply simp
- apply (rule power_strict_increasing)
- apply simp_all
+ apply (cases \<open>n < LENGTH('a)\<close>; transfer)
+ apply auto
done
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
@@ -3487,7 +4113,7 @@
lemma shiftr1_bintr [simp]:
"(shiftr1 (numeral w) :: 'a::len word) =
word_of_int (bin_rest (take_bit (LENGTH('a)) (numeral w)))"
- unfolding shiftr1_eq word_numeral_alt by (simp add: word_ubin.eq_norm)
+ by transfer simp
lemma sshiftr1_sbintr [simp]:
"(sshiftr1 (numeral w) :: 'a::len word) =
@@ -3624,26 +4250,14 @@
done
lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0"
- apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
- apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs del: word_of_int_0)
- apply (subst word_uint.norm_Rep [symmetric])
- apply (simp only: bintrunc_bintrunc_min take_bit_eq_mod [symmetric] min_def)
- apply auto
- done
+ by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 uint_0_iff)
lemma and_mask_dvd_nat: "2 ^ n dvd unat w \<longleftrightarrow> w AND mask n = 0"
- apply (simp flip: and_mask_dvd)
- apply transfer
- using dvd_nat_abs_iff [of _ \<open>take_bit LENGTH('a) k\<close> for k]
- apply simp
- done
+ by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 unat_0_iff uint_0_iff)
lemma word_2p_lem: "n < size w \<Longrightarrow> w < 2 ^ n = (uint w < 2 ^ n)"
for w :: "'a::len word"
- apply (unfold word_size word_less_alt word_numeral_alt)
- apply (auto simp add: word_of_int_power_hom word_uint.eq_norm
- simp del: word_of_int_numeral)
- done
+ by transfer simp
lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
for x :: "'a::len word"
@@ -3680,12 +4294,40 @@
"word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
"word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
- by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff take_bit_eq_mod mod_simps)
+ apply (auto simp flip: take_bit_eq_mask)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ done
lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
for x :: \<open>'a::len word\<close>
using word_of_int_Ex [where x=x]
- by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff take_bit_eq_mod mod_simps)
+ apply (auto simp flip: take_bit_eq_mask)
+ apply transfer
+ apply (simp add: take_bit_eq_mod mod_simps)
+ done
lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)"
by transfer (simp add: take_bit_minus_one_eq_mask)
@@ -3882,7 +4524,7 @@
by (cases \<open>LENGTH('a)\<close>) simp_all
have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close>
\<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close>
- using signed_take_bit_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_less_eq [of n \<open>sint x + sint y\<close>]
+ using signed_take_bit_int_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_int_less_eq [of n \<open>sint x + sint y\<close>]
by (auto intro: ccontr)
have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
(sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
@@ -3912,7 +4554,7 @@
"(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) =
map word_of_int (bin_rsplit (LENGTH('a::len))
(LENGTH('b), take_bit (LENGTH('b)) (numeral bin)))"
- by (simp add: word_rsplit_def word_ubin.eq_norm)
+ by (simp add: word_rsplit_def of_nat_take_bit)
lemmas word_rsplit_no_cl [simp] = word_rsplit_no
[unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
@@ -3943,7 +4585,7 @@
apply (unfold word_split_bin' test_bit_bin)
apply (clarify)
apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
- apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq ac_simps bin_nth_uint_imp)
+ apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_unsigned_iff ac_simps exp_eq_zero_iff dest: bit_imp_le_length)
done
lemma test_bit_split:
@@ -4392,7 +5034,10 @@
(if uint x + uint y < 2^size x
then uint x + uint y
else uint x + uint y - 2^size x)"
- by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
+ apply (simp only: word_arith_wis word_size uint_word_of_int_eq)
+ apply (auto simp add: not_less take_bit_int_eq_self_iff)
+ apply (metis not_less uint_plus_if' word_add_def word_ubin.eq_norm)
+ done
lemma unat_plus_if_size:
"unat (x + y) =
@@ -4408,7 +5053,7 @@
lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
for w :: "'a::len word"
- by (simp add: word_gt_0)
+ by (fact word_coorder.not_eq_extremum)
lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c"
for c :: "'a::len word"
@@ -4419,7 +5064,10 @@
(if uint y \<le> uint x
then uint x - uint y
else uint x - uint y + 2^size x)"
- by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size)
+ apply (simp only: word_arith_wis word_size uint_word_of_int_eq)
+ apply (auto simp add: take_bit_int_eq_self_iff not_le)
+ apply (metis not_le uint_sub_if' word_sub_wi word_ubin.eq_norm)
+ done
lemma unat_sub:
\<open>unat (a - b) = unat a - unat b\<close>
@@ -4433,7 +5081,7 @@
apply (subst take_bit_diff [symmetric])
apply (subst nat_take_bit_eq)
apply (simp add: nat_le_eq_zle)
- apply (simp add: nat_diff_distrib take_bit_eq_self less_imp_diff_less bintr_lt2p)
+ apply (simp add: nat_diff_distrib take_bit_nat_eq_self_iff less_imp_diff_less bintr_lt2p)
done
qed
@@ -4483,38 +5131,57 @@
shows "(x - y) mod b = z' mod b'"
using assms [symmetric] by (auto intro: mod_diff_cong)
-lemma word_induct_less: "P 0 \<Longrightarrow> (\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
- for P :: "'a::len word \<Rightarrow> bool"
- apply (cases m)
- apply atomize
- apply (erule rev_mp)+
- apply (rule_tac x=m in spec)
- apply (induct_tac n)
- apply simp
- apply clarsimp
- apply (erule impE)
- apply clarsimp
- apply (erule_tac x=n in allE)
- apply (erule impE)
- apply (simp add: unat_arith_simps)
- apply (clarsimp simp: unat_of_nat)
- apply simp
- apply (erule_tac x="of_nat na" in allE)
- apply (erule impE)
- apply (simp add: unat_arith_simps)
- apply (clarsimp simp: unat_of_nat)
- apply simp
- done
+lemma word_induct_less:
+ \<open>P m\<close> if zero: \<open>P 0\<close> and less: \<open>\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)\<close>
+ for m :: \<open>'a::len word\<close>
+proof -
+ define q where \<open>q = unat m\<close>
+ with less have \<open>\<And>n. n < word_of_nat q \<Longrightarrow> P n \<Longrightarrow> P (1 + n)\<close>
+ by simp
+ then have \<open>P (word_of_nat q :: 'a word)\<close>
+ proof (induction q)
+ case 0
+ show ?case
+ by (simp add: zero)
+ next
+ case (Suc q)
+ show ?case
+ proof (cases \<open>1 + word_of_nat q = (0 :: 'a word)\<close>)
+ case True
+ then show ?thesis
+ by (simp add: zero)
+ next
+ case False
+ then have *: \<open>word_of_nat q < (word_of_nat (Suc q) :: 'a word)\<close>
+ by (simp add: unatSuc word_less_nat_alt)
+ then have **: \<open>n < (1 + word_of_nat q :: 'a word) \<longleftrightarrow> n \<le> (word_of_nat q :: 'a word)\<close> for n
+ by (metis (no_types, lifting) add.commute inc_le le_less_trans not_less of_nat_Suc)
+ have \<open>P (word_of_nat q)\<close>
+ apply (rule Suc.IH)
+ apply (rule Suc.prems)
+ apply (erule less_trans)
+ apply (rule *)
+ apply assumption
+ done
+ with * have \<open>P (1 + word_of_nat q)\<close>
+ by (rule Suc.prems)
+ then show ?thesis
+ by simp
+ qed
+ qed
+ with \<open>q = unat m\<close> show ?thesis
+ by simp
+qed
lemma word_induct: "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
for P :: "'a::len word \<Rightarrow> bool"
- by (erule word_induct_less) simp
+ by (rule word_induct_less)
lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
for P :: "'b::len word \<Rightarrow> bool"
- apply (rule word_induct)
- apply simp
- apply (case_tac "1 + n = 0")
+ apply (rule word_induct_less)
+ apply simp_all
+ apply (case_tac "1 + na = 0")
apply auto
done
--- a/src/HOL/ex/Bit_Lists.thy Thu Sep 17 18:48:06 2020 +0100
+++ b/src/HOL/ex/Bit_Lists.thy Thu Sep 17 18:48:37 2020 +0100
@@ -5,7 +5,7 @@
theory Bit_Lists
imports
- "HOL-Word.Conversions" "HOL-Library.More_List"
+ "HOL-Word.Word" "HOL-Library.More_List"
begin
subsection \<open>Fragments of algebraic bit representations\<close>