dedicated symbols for code generation, to pave way for generic conversions from and to word
--- a/src/HOL/Library/Bit_Operations.thy Mon Aug 10 08:27:24 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy Mon Aug 10 15:34:55 2020 +0000
@@ -9,6 +9,27 @@
Main
begin
+lemma nat_take_bit_eq:
+ \<open>nat (take_bit n k) = take_bit n (nat k)\<close>
+ if \<open>k \<ge> 0\<close>
+ using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
+
+lemma take_bit_eq_self:
+ \<open>take_bit m n = n\<close> if \<open>n < 2 ^ m\<close> for n :: nat
+ using that by (simp add: take_bit_eq_mod)
+
+lemma horner_sum_of_bool_2_less:
+ \<open>(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\<close>
+proof -
+ have \<open>(\<Sum>n = 0..<length bs. of_bool (bs ! n) * (2::int) ^ n) \<le> (\<Sum>n = 0..<length bs. 2 ^ n)\<close>
+ by (rule sum_mono) simp
+ also have \<open>\<dots> = 2 ^ length bs - 1\<close>
+ by (induction bs) simp_all
+ finally show ?thesis
+ by (simp add: horner_sum_eq_sum)
+qed
+
+
subsection \<open>Bit operations\<close>
class semiring_bit_operations = semiring_bit_shifts +
--- a/src/HOL/Word/More_Word.thy Mon Aug 10 08:27:24 2020 +0200
+++ b/src/HOL/Word/More_Word.thy Mon Aug 10 15:34:55 2020 +0000
@@ -40,6 +40,6 @@
lemma shiftl_transfer [transfer_rule]:
includes lifting_syntax
shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)"
- by (auto intro!: rel_funI word_eqI simp add: word.pcr_cr_eq cr_word_def word_size nth_shiftl)
+ by (unfold shiftl_eq_push_bit) transfer_prover
end
--- a/src/HOL/Word/Reversed_Bit_Lists.thy Mon Aug 10 08:27:24 2020 +0200
+++ b/src/HOL/Word/Reversed_Bit_Lists.thy Mon Aug 10 15:34:55 2020 +0000
@@ -8,6 +8,41 @@
imports Word
begin
+context comm_semiring_1
+begin
+
+lemma horner_sum_append:
+ \<open>horner_sum f a (xs @ ys) = horner_sum f a xs + a ^ length xs * horner_sum f a ys\<close>
+ using sum.atLeastLessThan_shift_bounds [of _ 0 \<open>length xs\<close> \<open>length ys\<close>]
+ atLeastLessThan_add_Un [of 0 \<open>length xs\<close> \<open>length ys\<close>]
+ by (simp add: horner_sum_eq_sum sum_distrib_left sum.union_disjoint ac_simps nth_append power_add)
+
+end
+
+lemma horner_sum_of_bool_2_concat:
+ \<open>horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws\<close>
+ for ws :: \<open>'a::len word list\<close>
+proof (induction ws)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons w ws)
+ moreover have \<open>horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w\<close>
+ proof transfer
+ fix k :: int
+ have \<open>map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]
+ = map (bit k) [0..<LENGTH('a)]\<close>
+ by simp
+ then show \<open>horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)])
+ = take_bit LENGTH('a) k\<close>
+ by (simp only: horner_sum_bit_eq_take_bit)
+ qed
+ ultimately show ?case
+ by (simp add: horner_sum_append)
+qed
+
+
subsection \<open>Implicit augmentation of list prefixes\<close>
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
@@ -971,7 +1006,7 @@
lemma bit_of_bl_iff:
\<open>bit (of_bl bs :: 'a word) n \<longleftrightarrow> rev bs ! n \<and> n < LENGTH('a::len) \<and> n < length bs\<close>
- by (auto simp add: of_bl_def bit_word_of_int_iff bin_nth_of_bl)
+ by transfer (simp add: bin_nth_of_bl ac_simps)
lemma rev_to_bl_eq:
\<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close>
@@ -981,6 +1016,14 @@
apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq)
done
+lemma to_bl_eq_rev:
+ \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a)])\<close>
+ for w :: \<open>'a::len word\<close>
+ using rev_to_bl_eq [of w]
+ apply (subst rev_is_rev_conv [symmetric])
+ apply (simp add: rev_map)
+ done
+
lemma of_bl_rev_eq:
\<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close>
apply (rule bit_word_eqI)
@@ -989,6 +1032,10 @@
apply (simp add: bit_horner_sum_bit_iff ac_simps)
done
+lemma of_bl_eq:
+ \<open>of_bl bs = horner_sum of_bool 2 (rev bs)\<close>
+ using of_bl_rev_eq [of \<open>rev bs\<close>] by simp
+
lemma bshiftr1_eq:
\<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close>
apply transfer
@@ -1037,11 +1084,8 @@
(to_bl :: 'a::len word \<Rightarrow> bool list)
of_bl
{bl. length bl = LENGTH('a)}"
- apply (unfold type_definition_def of_bl.abs_eq to_bl_eq)
- apply (simp add: word_ubin.eq_norm)
- apply safe
- apply (drule sym)
- apply simp
+ apply (standard; transfer)
+ apply (auto dest: sym)
done
interpretation word_bl:
@@ -1081,15 +1125,14 @@
lemma of_bl_drop':
"lend = length bl - LENGTH('a::len) \<Longrightarrow>
of_bl (drop lend bl) = (of_bl bl :: 'a word)"
- by (auto simp: of_bl_def trunc_bl2bin [symmetric])
+ by transfer (simp flip: trunc_bl2bin)
lemma test_bit_of_bl:
"(of_bl bl::'a::len word) !! n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)"
- by (auto simp add: of_bl_def word_test_bit_def word_size
- word_ubin.eq_norm nth_bintr bin_nth_of_bl)
+ by transfer (simp add: bin_nth_of_bl ac_simps)
lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))"
- by (simp add: of_bl_def)
+ by transfer simp
lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
by transfer simp
@@ -1142,7 +1185,7 @@
lemma word_rev_tf:
"to_bl (of_bl bl::'a::len word) =
rev (takefill False (LENGTH('a)) (rev bl))"
- by (auto simp: of_bl_def uint_bl bl_bin_bl_rtf word_ubin.eq_norm word_size)
+ by transfer (simp add: bl_bin_bl_rtf)
lemma word_rep_drop:
"to_bl (of_bl bl::'a::len word) =
@@ -1184,13 +1227,13 @@
done
lemma word_0_bl [simp]: "of_bl [] = 0"
- by (simp add: of_bl_def)
+ by transfer simp
lemma word_1_bl: "of_bl [True] = 1"
- by (simp add: of_bl_def bl_to_bin_def)
+ by transfer (simp add: bl_to_bin_def)
lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
- by (simp add: of_bl_def bl_to_bin_rep_False)
+ by transfer (simp add: bl_to_bin_rep_False)
lemma to_bl_0 [simp]: "to_bl (0::'a::len word) = replicate (LENGTH('a)) False"
by (simp add: uint_bl word_size bin_to_bl_zero)
@@ -1228,19 +1271,21 @@
by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl)
lemma of_bl_length_less:
- "length x = k \<Longrightarrow> k < LENGTH('a) \<Longrightarrow> (of_bl x :: 'a::len word) < 2 ^ k"
- apply (unfold of_bl_def word_less_alt word_numeral_alt)
- apply safe
- apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
- del: word_of_int_numeral)
- apply simp
- apply (subst mod_pos_pos_trivial)
- apply (rule bl_to_bin_ge0)
- apply (rule order_less_trans)
- apply (rule bl_to_bin_lt2p)
- apply simp
- apply (rule bl_to_bin_lt2p)
- done
+ \<open>(of_bl x :: 'a::len word) < 2 ^ k\<close>
+ if \<open>length x = k\<close> \<open>k < LENGTH('a)\<close>
+proof -
+ from that have \<open>length x < LENGTH('a)\<close>
+ by simp
+ then have \<open>(of_bl x :: 'a::len word) < 2 ^ length x\<close>
+ apply (simp add: of_bl_eq)
+ apply transfer
+ apply (simp add: take_bit_horner_sum_bit_eq)
+ apply (subst length_rev [symmetric])
+ apply (simp only: horner_sum_of_bool_2_less)
+ done
+ with that show ?thesis
+ by simp
+qed
lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
by simp
@@ -1305,10 +1350,6 @@
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
by (auto simp: of_bl_def bl_to_bin_rep_F)
-lemma of_bl_eq:
- \<open>of_bl bs = horner_sum of_bool 2 (rev bs)\<close>
- by (rule bit_word_eqI) (simp add: bit_of_bl_iff bit_horner_sum_bit_word_iff ac_simps)
-
lemma [code abstract]:
\<open>uint (of_bl bs :: 'a word) = horner_sum of_bool 2 (take LENGTH('a::len) (rev bs))\<close>
apply (simp add: of_bl_eq flip: take_bit_horner_sum_bit_eq)
@@ -1360,7 +1401,7 @@
unfolding bshiftr1_eq by (rule word_bl.Abs_inverse) simp
lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
- by (simp add: of_bl_def bl_to_bin_append)
+ by transfer (simp add: bl_to_bin_append)
lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
for w :: "'a::len word"
@@ -1495,7 +1536,7 @@
lemma shiftr1_bl_of:
"length bl \<le> LENGTH('a) \<Longrightarrow>
shiftr1 (of_bl bl::'a::len word) = of_bl (butlast bl)"
- by (clarsimp simp: shiftr1_eq of_bl_def butlast_rest_bl2bin word_ubin.eq_norm trunc_bl2bin)
+ by transfer (simp add: butlast_rest_bl2bin trunc_bl2bin)
lemma shiftr_bl_of:
"length bl \<le> LENGTH('a) \<Longrightarrow>
@@ -1576,17 +1617,20 @@
lemma slice1_down_alt':
"sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
to_bl sl = takefill False fs (drop k (to_bl w))"
- by (auto simp: slice1_eq_of_bl word_size of_bl_def uint_bl
- word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
+ apply (simp add: slice1_eq_of_bl)
+ apply transfer
+ apply (simp add: bl_bin_bl_rep_drop)
+ using drop_takefill
+ apply force
+ done
lemma slice1_up_alt':
"sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
- apply (unfold slice1_eq_of_bl word_size of_bl_def uint_bl)
- apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
- apply (rule_tac f = "\<lambda>k. takefill False (LENGTH('a))
- (replicate k False @ bin_to_bl (LENGTH('b)) (uint w))" in arg_cong)
- apply arith
+ apply (simp add: slice1_eq_of_bl)
+ apply transfer
+ apply (simp add: bl_bin_bl_rep_drop flip: takefill_append)
+ apply (metis diff_add_inverse)
done
lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
@@ -1626,8 +1670,8 @@
lemma of_bl_append:
"(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
- apply (simp add: of_bl_def bl_to_bin_app_cat bin_cat_num)
- apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
+ apply transfer
+ apply (simp add: bl_to_bin_app_cat bin_cat_num)
done
lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
@@ -1642,24 +1686,10 @@
lemma word_split_bl':
"std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
(a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))"
- apply (unfold word_split_bin')
- apply safe
- defer
- apply (clarsimp split: prod.splits)
- apply (metis of_bl.abs_eq size_word.rep_eq to_bl_to_bin trunc_bl2bin word_size_bl word_ubin.eq_norm word_uint.Rep_inverse)
- apply hypsubst_thin
- apply (drule word_ubin.norm_Rep [THEN ssubst])
- apply (simp add: of_bl_def bl2bin_drop word_size
- word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep)
- apply (clarsimp split: prod.splits)
- apply (cases "LENGTH('a) \<ge> LENGTH('b)")
- apply (simp_all add: not_le)
- defer
- apply (simp add: drop_bit_eq_div lt2p_lem)
- apply (simp add: to_bl_eq)
- apply (subst bin_to_bl_drop_bit [symmetric])
- apply (subst diff_add)
- apply (simp_all add: take_bit_drop_bit)
+ apply (simp add: word_split_def)
+ apply transfer
+ apply (cases \<open>LENGTH('b) \<le> LENGTH('a)\<close>)
+ apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>])
done
lemma word_split_bl: "std = size c - size b \<Longrightarrow>
@@ -1684,8 +1714,18 @@
apply (rule refl conjI)+
done
-lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
- by (auto simp: word_rcat_eq to_bl_def' of_bl_def bin_rcat_bl)
+lemma word_rcat_bl:
+ \<open>word_rcat wl = of_bl (concat (map to_bl wl))\<close>
+proof -
+ define ws where \<open>ws = rev wl\<close>
+ moreover have \<open>word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))\<close>
+ apply (simp add: word_rcat_def of_bl_eq rev_concat rev_map comp_def rev_to_bl_eq flip: horner_sum_of_bool_2_concat)
+ apply transfer
+ apply simp
+ done
+ ultimately show ?thesis
+ by simp
+qed
lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
by (induct wl) (auto simp: word_size)
--- a/src/HOL/Word/Word.thy Mon Aug 10 08:27:24 2020 +0200
+++ b/src/HOL/Word/Word.thy Mon Aug 10 15:34:55 2020 +0000
@@ -18,7 +18,12 @@
subsection \<open>Type definition\<close>
quotient_type (overloaded) 'a word = int / \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l\<close>
- morphisms rep_word word_of_int by (auto intro!: equivpI reflpI sympI transpI)
+ morphisms rep_word Word by (auto intro!: equivpI reflpI sympI transpI)
+
+hide_const (open) Word \<comment> \<open>only for code generation\<close>
+
+lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
+ is \<open>\<lambda>k. k\<close> .
lift_definition uint :: \<open>'a::len word \<Rightarrow> int\<close>
is \<open>take_bit LENGTH('a)\<close> .
@@ -161,20 +166,17 @@
subsection \<open>Basic code generation setup\<close>
-lift_definition Word :: \<open>int \<Rightarrow> 'a::len word\<close>
- is id .
-
lemma Word_eq_word_of_int [code_post]:
- \<open>Word = word_of_int\<close>
- by (simp add: fun_eq_iff Word.abs_eq)
+ \<open>Word.Word = word_of_int\<close>
+ by rule (transfer, rule)
lemma [code abstype]:
- \<open>Word (uint w) = w\<close>
+ \<open>Word.Word (uint w) = w\<close>
by transfer simp
lemma [code abstract]:
\<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close>
- by (fact uint.abs_eq)
+ by transfer rule
instantiation word :: (len) equal
begin
@@ -356,23 +358,42 @@
text \<open>Legacy theorems:\<close>
-lemma word_arith_wis:
- shows word_add_def [code]: "a + b = word_of_int (uint a + uint b)"
- and word_sub_wi [code]: "a - b = word_of_int (uint a - uint b)"
- and word_mult_def [code]: "a * b = word_of_int (uint a * uint b)"
- and word_minus_def [code]: "- a = word_of_int (- uint a)"
- and word_succ_alt [code]: "word_succ a = word_of_int (uint a + 1)"
- and word_pred_alt [code]: "word_pred a = word_of_int (uint a - 1)"
- and word_0_wi: "0 = word_of_int 0"
- and word_1_wi: "1 = word_of_int 1"
- apply (simp_all flip: plus_word.abs_eq minus_word.abs_eq
- times_word.abs_eq uminus_word.abs_eq
- zero_word.abs_eq one_word.abs_eq)
- apply transfer
- apply simp
- apply transfer
- apply simp
- done
+lemma word_add_def [code]:
+ "a + b = word_of_int (uint a + uint b)"
+ by transfer (simp add: take_bit_add)
+
+lemma word_sub_wi [code]:
+ "a - b = word_of_int (uint a - uint b)"
+ by transfer (simp add: take_bit_diff)
+
+lemma word_mult_def [code]:
+ "a * b = word_of_int (uint a * uint b)"
+ by transfer (simp add: take_bit_eq_mod mod_simps)
+
+lemma word_minus_def [code]:
+ "- a = word_of_int (- uint a)"
+ by transfer (simp add: take_bit_minus)
+
+lemma word_succ_alt [code]:
+ "word_succ a = word_of_int (uint a + 1)"
+ by transfer (simp add: take_bit_eq_mod mod_simps)
+
+lemma word_pred_alt [code]:
+ "word_pred a = word_of_int (uint a - 1)"
+ by transfer (simp add: take_bit_eq_mod mod_simps)
+
+lemma word_0_wi:
+ "0 = word_of_int 0"
+ by transfer simp
+
+lemma word_1_wi:
+ "1 = word_of_int 1"
+ by transfer simp
+
+lemmas word_arith_wis =
+ word_add_def word_sub_wi word_mult_def
+ word_minus_def word_succ_alt word_pred_alt
+ word_0_wi word_1_wi
lemma wi_homs:
shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)"
@@ -2049,7 +2070,9 @@
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)"
- by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
+ apply (simp_all only: word_arith_wis)
+ apply (simp_all add: word_uint.eq_norm)
+ done
lemma uint_word_arith_bintrs:
fixes a b :: "'a::len word"
@@ -2879,7 +2902,10 @@
subsection \<open>Cardinality, finiteness of set of words\<close>
lemma inj_on_word_of_int: \<open>inj_on (word_of_int :: int \<Rightarrow> 'a word) {0..<2 ^ LENGTH('a::len)}\<close>
- by (rule inj_onI) (simp add: word.abs_eq_iff take_bit_eq_mod)
+ apply (rule inj_onI)
+ apply transfer
+ apply (simp add: take_bit_eq_mod)
+ done
lemma inj_uint: \<open>inj uint\<close>
by (rule injI) simp
@@ -2890,7 +2916,7 @@
lemma UNIV_eq: \<open>(UNIV :: 'a word set) = word_of_int ` {0..<2 ^ LENGTH('a::len)}\<close>
proof -
have \<open>uint ` (UNIV :: 'a word set) = uint ` (word_of_int :: int \<Rightarrow> 'a word) ` {0..<2 ^ LENGTH('a::len)}\<close>
- by (simp add: range_uint image_image uint.abs_eq take_bit_eq_mod)
+ by transfer (simp add: range_bintrunc, auto simp add: take_bit_eq_mod)
then show ?thesis
using inj_image_eq_iff [of \<open>uint :: 'a word \<Rightarrow> int\<close> \<open>UNIV :: 'a word set\<close> \<open>word_of_int ` {0..<2 ^ LENGTH('a)} :: 'a word set\<close>, OF inj_uint]
by simp
@@ -2993,8 +3019,8 @@
lemma word_test_bit_transfer [transfer_rule]:
"(rel_fun pcr_word (rel_fun (=) (=)))
- (\<lambda>x n. n < LENGTH('a) \<and> bin_nth x n) (test_bit :: 'a::len word \<Rightarrow> _)"
- unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
+ (\<lambda>x n. n < LENGTH('a) \<and> bit x n) (test_bit :: 'a::len word \<Rightarrow> _)"
+ by (simp only: test_bit_eq_bit) transfer_prover
lemma word_ops_nth_size:
"n < size x \<Longrightarrow>
@@ -3259,7 +3285,7 @@
subsection \<open>Shifting, Rotating, and Splitting Words\<close>
lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (2 * w)"
- by (fact shiftl1.abs_eq)
+ by transfer simp
lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
unfolding word_numeral_alt shiftl1_wi by simp
@@ -3546,8 +3572,17 @@
lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
by (simp only: and_mask_bintr take_bit_eq_mod)
+lemma uint_mask_eq:
+ \<open>uint (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close>
+ by transfer simp
+
lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
- by (simp add: and_mask_bintr uint.abs_eq min_def not_le lt2p_lem bintr_lt2p)
+ apply (simp add: uint_and uint_mask_eq)
+ apply (rule AND_upper2'')
+ apply simp
+ apply (auto simp add: mask_eq_exp_minus_1 min_def power_add algebra_simps dest!: le_Suc_ex)
+ apply (metis add_minus_cancel le_add2 one_le_numeral power_add power_increasing uminus_add_conv_diff zle_diff1_eq)
+ done
lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
for b n :: int
@@ -4358,11 +4393,21 @@
else uint x - uint y + 2^size x)"
by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size)
-lemma unat_sub: "b \<le> a \<Longrightarrow> unat (a - b) = unat a - unat b"
- apply transfer
- apply (simp flip: nat_diff_distrib)
- apply (metis minus_word.abs_eq uint_sub_lem word_ubin.eq_norm)
- done
+lemma unat_sub:
+ \<open>unat (a - b) = unat a - unat b\<close>
+ if \<open>b \<le> a\<close>
+proof -
+ from that have \<open>unat b \<le> unat a\<close>
+ by transfer simp
+ with that show ?thesis
+ apply transfer
+ apply simp
+ 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)
+ done
+qed
lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
@@ -4578,6 +4623,4 @@
ML_file \<open>Tools/word_lib.ML\<close>
ML_file \<open>Tools/smt_word.ML\<close>
-hide_const (open) Word
-
end