--- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Sat Jul 04 20:45:24 2020 +0000
@@ -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 int_mod_eq')
+ by (simp add: f_def bwsimps int_word_uint)
qed
spark_vc function_f_7
@@ -34,7 +34,7 @@
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 int_mod_eq')
+ by (simp add: f_def bwsimps int_word_uint)
qed
spark_vc function_f_8
@@ -42,7 +42,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 int_mod_eq')
+ by (simp add: f_def bwsimps int_word_uint)
qed
spark_vc function_f_9
@@ -50,7 +50,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 int_mod_eq')
+ by (simp add: f_def bwsimps int_word_uint)
qed
spark_vc function_f_10
@@ -58,7 +58,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 int_mod_eq')
+ by (simp add: f_def bwsimps int_word_uint)
qed
spark_end
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Jul 04 20:45:24 2020 +0000
@@ -56,7 +56,7 @@
shows"uint(word_of_int x::word32) = x"
unfolding int_word_uint
using assms
- by (simp add:int_mod_eq')
+ by simp
lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i"
unfolding steps_def
@@ -186,11 +186,11 @@
(is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
proof -
have "a mod ?MM = a" using \<open>0 <= a\<close> \<open>a <= ?M\<close>
- by (simp add: int_mod_eq')
+ by simp
have "?X mod ?MM = ?X" using \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>
- by (simp add: int_mod_eq')
+ by simp
have "e mod ?MM = e" using \<open>0 <= e\<close> \<open>e <= ?M\<close>
- by (simp add: int_mod_eq')
+ by simp
have "(?MM::int) = 2 ^ LENGTH(32)" by simp
show ?thesis
unfolding
@@ -226,11 +226,11 @@
(is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
proof -
have "a' mod ?MM = a'" using \<open>0 <= a'\<close> \<open>a' <= ?M\<close>
- by (simp add: int_mod_eq')
+ by simp
have "?X mod ?MM = ?X" using \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>
- by (simp add: int_mod_eq')
+ by simp
have "e' mod ?MM = e'" using \<open>0 <= e'\<close> \<open>e' <= ?M\<close>
- by (simp add: int_mod_eq')
+ by simp
have "(?MM::int) = 2 ^ LENGTH(32)" by simp
have nat_transfer: "79 - nat j = nat (79 - j)"
using nat_diff_distrib \<open>0 <= j\<close> \<open>j <= 79\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bit_Lists.thy Sat Jul 04 20:45:24 2020 +0000
@@ -0,0 +1,137 @@
+(* Title: HOL/Word/Bit_Lists.thy
+ Author: Jeremy Dawson, NICTA
+*)
+
+section \<open>Bit values as reversed lists of bools\<close>
+
+theory Bit_Lists
+ imports Bits_Int
+begin
+
+subsection \<open>Implicit augmentation of list prefixes\<close>
+
+primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+ Z: "takefill fill 0 xs = []"
+ | Suc: "takefill fill (Suc n) xs =
+ (case xs of
+ [] \<Rightarrow> fill # takefill fill n xs
+ | y # ys \<Rightarrow> y # takefill fill n ys)"
+
+lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
+ apply (induct n arbitrary: m l)
+ apply clarsimp
+ apply clarsimp
+ apply (case_tac m)
+ apply (simp split: list.split)
+ apply (simp split: list.split)
+ done
+
+lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
+ by (induct n arbitrary: l) (auto split: list.split)
+
+lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
+ by (simp add: takefill_alt replicate_add [symmetric])
+
+lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+ by (induct m arbitrary: l n) (auto split: list.split)
+
+lemma length_takefill [simp]: "length (takefill fill n l) = n"
+ by (simp add: takefill_alt)
+
+lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
+ by (induct k arbitrary: w n) (auto split: list.split)
+
+lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
+ by (induct k arbitrary: w) (auto split: list.split)
+
+lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+ by (auto simp: le_iff_add takefill_le')
+
+lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
+ by (auto simp: le_iff_add take_takefill')
+
+lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
+ by (induct xs) auto
+
+lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
+ by (induct xs arbitrary: l) auto
+
+lemmas takefill_same [simp] = takefill_same' [OF refl]
+
+lemma tf_rev:
+ "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
+ rev (takefill y m (rev (takefill x k (rev bl))))"
+ apply (rule nth_equalityI)
+ apply (auto simp add: nth_takefill rev_nth)
+ apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
+ apply arith
+ done
+
+lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
+ by auto
+
+lemmas takefill_Suc_cases =
+ list.cases [THEN takefill.Suc [THEN trans]]
+
+lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
+lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
+
+lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
+ takefill_minus [symmetric, THEN trans]]
+
+lemma takefill_numeral_Nil [simp]:
+ "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
+ by (simp add: numeral_eq_Suc)
+
+lemma takefill_numeral_Cons [simp]:
+ "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
+ by (simp add: numeral_eq_Suc)
+
+
+subsection \<open>Range projection\<close>
+
+definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
+ where "bl_of_nth n f = map f (rev [0..<n])"
+
+lemma bl_of_nth_simps [simp, code]:
+ "bl_of_nth 0 f = []"
+ "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+ by (simp_all add: bl_of_nth_def)
+
+lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
+ by (simp add: bl_of_nth_def)
+
+lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
+ by (simp add: bl_of_nth_def rev_map)
+
+lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
+ by (simp add: bl_of_nth_def)
+
+lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
+ apply (induct n arbitrary: xs)
+ apply clarsimp
+ apply clarsimp
+ apply (rule trans [OF _ hd_Cons_tl])
+ apply (frule Suc_le_lessD)
+ apply (simp add: rev_nth trans [OF drop_Suc drop_tl, symmetric])
+ apply (subst hd_drop_conv_nth)
+ apply force
+ apply simp_all
+ apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
+ apply simp
+ done
+
+lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
+ by (simp add: bl_of_nth_nth_le)
+
+lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
+ apply (rule nth_equalityI)
+ apply simp
+ apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
+ done
+
+lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
+ by (simp add: takefill_bintrunc)
+
+end
--- a/src/HOL/Word/Bits_Int.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy Sat Jul 04 20:45:24 2020 +0000
@@ -9,9 +9,16 @@
section \<open>Bitwise Operations on integers\<close>
theory Bits_Int
- imports Misc_Auxiliary Bits
+ imports Bits
begin
+subsection \<open>Generic auxiliary\<close>
+
+lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
+ for a n :: int
+ by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
+
+
subsection \<open>Implicit bit representation of \<^typ>\<open>int\<close>\<close>
abbreviation (input) bin_last :: "int \<Rightarrow> bool"
@@ -256,6 +263,10 @@
by (auto elim!: evenE oddE simp add: mult_mod_right ac_simps)
qed
+lemma sbintrunc_eq_take_bit:
+ \<open>sbintrunc n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
+ by (simp add: sbintrunc_mod2p take_bit_eq_mod)
+
lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
by (simp add: bintrunc_mod2p bin_sign_def)
@@ -464,47 +475,59 @@
by (rule ext) (rule bintrunc_mod2p)
lemma range_bintrunc: "range (bintrunc n) = {i. 0 \<le> i \<and> i < 2 ^ n}"
- apply (unfold no_bintr_alt1)
- apply (auto simp add: image_iff)
- apply (rule exI)
- apply (rule sym)
- using int_mod_lem [symmetric, of "2 ^ n"]
- apply auto
- done
+ by (auto simp add: take_bit_eq_mod image_iff) (metis mod_pos_pos_trivial)
lemma no_sbintr_alt2: "sbintrunc n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
by (rule ext) (simp add : sbintrunc_mod2p)
lemma range_sbintrunc: "range (sbintrunc n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}"
- apply (unfold no_sbintr_alt2)
- apply (auto simp add: image_iff eq_diff_eq)
-
- apply (rule exI)
- apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
- done
-
-lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
- for a :: int
- using int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"]
- by simp
-
-lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
- for a :: int
- by (rule sb_inc_lem) simp
-
-lemma sbintrunc_inc: "x < - (2^n) \<Longrightarrow> x + 2^(Suc n) \<le> sbintrunc n x"
- unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
-
-lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
- for a :: int
- using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
-
-lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
- for a :: int
- by (rule sb_dec_lem) simp
-
-lemma sbintrunc_dec: "x \<ge> (2 ^ n) \<Longrightarrow> x - 2 ^ (Suc n) >= sbintrunc n x"
- unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
+proof -
+ have \<open>surj (\<lambda>k::int. k + 2 ^ n)\<close>
+ by (rule surjI [of _ \<open>(\<lambda>k. k - 2 ^ n)\<close>]) simp
+ moreover have \<open>sbintrunc n = ((\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n))\<close>
+ by (simp add: sbintrunc_eq_take_bit fun_eq_iff)
+ ultimately show ?thesis
+ apply (simp only: fun.set_map range_bintrunc)
+ apply (auto simp add: image_iff)
+ apply presburger
+ done
+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)
+
+lemma sbintrunc_inc:
+ \<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close>
+ using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
+ by (simp add: sbintrunc_eq_take_bit)
+
+lemma sbintrunc_dec:
+ \<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
+ using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
+ by (simp add: sbintrunc_eq_take_bit)
lemma bintr_ge0: "0 \<le> bintrunc n w"
by (simp add: bintrunc_mod2p)
@@ -513,8 +536,8 @@
by (simp add: bintrunc_mod2p)
lemma bintr_Min: "bintrunc n (- 1) = 2 ^ n - 1"
- by (simp add: bintrunc_mod2p m1mod2k)
-
+ by (simp add: stable_imp_take_bit_eq)
+
lemma sbintr_ge: "- (2 ^ n) \<le> sbintrunc n w"
by (simp add: sbintrunc_mod2p)
@@ -540,7 +563,7 @@
by (auto simp add: take_bit_Suc)
lemma bin_rest_strunc: "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
- by (induct n arbitrary: bin) auto
+ by simp
lemma bintrunc_rest [simp]: "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
by (induct n arbitrary: bin) (simp_all add: take_bit_Suc)
@@ -609,8 +632,12 @@
proof -
have \<open>0 \<le> x\<close> if \<open>0 \<le> x * 2 ^ n + y mod 2 ^ n\<close>
proof -
- from that have \<open>x \<noteq> - 1\<close>
- using int_mod_le' [of \<open>y mod 2 ^ n\<close> \<open>2 ^ n\<close>] by auto
+ have \<open>y mod 2 ^ n < 2 ^ n\<close>
+ using pos_mod_bound [of \<open>2 ^ n\<close> y] by simp
+ then have \<open>\<not> y mod 2 ^ n \<ge> 2 ^ n\<close>
+ by (simp add: less_le)
+ with that have \<open>x \<noteq> - 1\<close>
+ by auto
have *: \<open>- 1 \<le> (- (y mod 2 ^ n)) div 2 ^ n\<close>
by (simp add: zdiv_zminus1_eq_if)
from that have \<open>- (y mod 2 ^ n) \<le> x * 2 ^ n\<close>
@@ -1858,11 +1885,14 @@
lemma nth_bin_to_bl_aux:
"n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
- (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
+ (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
apply (induction bl arbitrary: w)
apply simp_all
- apply (metis add.right_neutral bin_nth_bl bin_to_bl_def diff_Suc_less less_Suc_eq_0_disj less_imp_Suc_add list.size(3) nth_rev_alt size_bin_to_bl_aux)
- apply (metis One_nat_def Suc_pred add_diff_cancel_left' add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def cancel_comm_monoid_add_class.diff_cancel diff_Suc_Suc diff_is_0_eq diff_zero le_add_diff_inverse le_eq_less_or_eq less_Suc_eq_0_disj less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append order_refl size_bin_to_bl_aux)
+ apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
+ apply (metis One_nat_def Suc_pred add_diff_cancel_left'
+ add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
+ diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
+ less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
done
lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
@@ -2030,19 +2060,10 @@
"k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
using bin_split_take by simp
-lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
- apply (rule nth_equalityI)
- apply simp
- apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
- done
-
-lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
- by (simp add: takefill_bintrunc)
-
lemma bl_bin_bl_rep_drop:
"bin_to_bl n (bl_to_bin bl) =
replicate (n - length bl) False @ drop (length bl - n) bl"
- by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
+ by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
lemma bl_to_bin_aux_cat:
"bl_to_bin_aux bs (bin_cat w nv v) =
--- a/src/HOL/Word/Misc_Arithmetic.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Misc_Arithmetic.thy Sat Jul 04 20:45:24 2020 +0000
@@ -3,9 +3,49 @@
section \<open>Miscellaneous lemmas, mostly for arithmetic\<close>
theory Misc_Arithmetic
- imports Misc_Auxiliary
+ imports Main Bits_Int
begin
+lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
+ for b n :: int
+ apply safe
+ apply (erule (1) mod_pos_pos_trivial)
+ apply (erule_tac [!] subst)
+ apply auto
+ done
+
+lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
+ for b n :: int
+ by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
+
+lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
+ for b n :: int
+ by (metis minus_mod_self2 zmod_le_nonneg_dividend)
+
+lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
+ for n d :: int
+ by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
+
+lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
+ by (rule zmod_minus1) simp
+
+lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+ for a :: int
+ using int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"]
+ by simp
+
+lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+ for a :: int
+ by (rule sb_inc_lem) simp
+
+lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+ for a :: int
+ using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
+
+lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+ for a :: int
+ by (rule sb_dec_lem) simp
+
lemma one_mod_exp_eq_one [simp]:
"1 mod (2 * 2 ^ n) = (1::int)"
using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)
--- a/src/HOL/Word/Misc_Auxiliary.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Misc_Auxiliary.thy Sat Jul 04 20:45:24 2020 +0000
@@ -8,42 +8,6 @@
imports Main
begin
-subsection \<open>Arithmetic lemmas\<close>
-
-lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
- for b n :: int
- apply safe
- apply (erule (1) mod_pos_pos_trivial)
- apply (erule_tac [!] subst)
- apply auto
- done
-
-lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
- for a n :: int
- by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
-
-lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
- for b n :: int
- by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
-
-lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
- for b n :: int
- by (metis minus_mod_self2 zmod_le_nonneg_dividend)
-
-lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
- for n d :: int
- by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
-
-lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
- by (rule zmod_minus1) simp
-
-lemma sub_inc_One: "Num.sub (Num.inc n) num.One = numeral n"
- by (metis add_diff_cancel add_neg_numeral_special(3) add_uminus_conv_diff numeral_inc)
-
-lemma inc_BitM: "Num.inc (Num.BitM n) = num.Bit0 n"
- by (simp add: BitM_plus_one[symmetric] add_One)
-
-
subsection \<open>Lemmas on list operations\<close>
lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl"
@@ -58,122 +22,4 @@
lemma hd_butlast: "length xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs"
by (cases xs) auto
-
-subsection \<open>Implicit augmentation of list prefixes\<close>
-
-primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- Z: "takefill fill 0 xs = []"
- | Suc: "takefill fill (Suc n) xs =
- (case xs of
- [] \<Rightarrow> fill # takefill fill n xs
- | y # ys \<Rightarrow> y # takefill fill n ys)"
-
-lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
- apply (induct n arbitrary: m l)
- apply clarsimp
- apply clarsimp
- apply (case_tac m)
- apply (simp split: list.split)
- apply (simp split: list.split)
- done
-
-lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
- by (induct n arbitrary: l) (auto split: list.split)
-
-lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
- by (simp add: takefill_alt replicate_add [symmetric])
-
-lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
- by (induct m arbitrary: l n) (auto split: list.split)
-
-lemma length_takefill [simp]: "length (takefill fill n l) = n"
- by (simp add: takefill_alt)
-
-lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
- by (induct k arbitrary: w n) (auto split: list.split)
-
-lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
- by (induct k arbitrary: w) (auto split: list.split)
-
-lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
- by (auto simp: le_iff_add takefill_le')
-
-lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
- by (auto simp: le_iff_add take_takefill')
-
-lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
- by (induct xs) auto
-
-lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
- by (induct xs arbitrary: l) auto
-
-lemmas takefill_same [simp] = takefill_same' [OF refl]
-
-lemma tf_rev:
- "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
- rev (takefill y m (rev (takefill x k (rev bl))))"
- apply (rule nth_equalityI)
- apply (auto simp add: nth_takefill nth_rev)
- apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
- apply arith
- done
-
-lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
- by auto
-
-lemmas takefill_Suc_cases =
- list.cases [THEN takefill.Suc [THEN trans]]
-
-lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
-lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
-
-lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
- takefill_minus [symmetric, THEN trans]]
-
-lemma takefill_numeral_Nil [simp]:
- "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
- by (simp add: numeral_eq_Suc)
-
-lemma takefill_numeral_Cons [simp]:
- "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
- by (simp add: numeral_eq_Suc)
-
-
-subsection \<open>Auxiliary: Range projection\<close>
-
-definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
- where "bl_of_nth n f = map f (rev [0..<n])"
-
-lemma bl_of_nth_simps [simp, code]:
- "bl_of_nth 0 f = []"
- "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
- by (simp_all add: bl_of_nth_def)
-
-lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
- by (simp add: bl_of_nth_def)
-
-lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
- by (simp add: bl_of_nth_def rev_map)
-
-lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
- by (simp add: bl_of_nth_def)
-
-lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
- apply (induct n arbitrary: xs)
- apply clarsimp
- apply clarsimp
- apply (rule trans [OF _ hd_Cons_tl])
- apply (frule Suc_le_lessD)
- apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
- apply (subst hd_drop_conv_nth)
- apply force
- apply simp_all
- apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
- apply simp
- done
-
-lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
- by (simp add: bl_of_nth_nth_le)
-
end
--- a/src/HOL/Word/More_Word.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/More_Word.thy Sat Jul 04 20:45:24 2020 +0000
@@ -7,6 +7,8 @@
imports
Word
Ancient_Numeral
+ Misc_Auxiliary
+ Misc_Arithmetic
begin
end
--- a/src/HOL/Word/Word.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Word.thy Sat Jul 04 20:45:24 2020 +0000
@@ -11,8 +11,8 @@
"HOL-Library.Bit_Operations"
Bits_Int
Bit_Comprehension
+ Bit_Lists
Misc_Typedef
- Misc_Arithmetic
begin
subsection \<open>Type definition\<close>
@@ -1290,7 +1290,7 @@
lemma lt2p_lem: "LENGTH('a) \<le> n \<Longrightarrow> uint w < 2 ^ n"
for w :: "'a::len word"
- by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
+ by (metis bintr_lt2p bintr_uint)
lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
by (fact uint_ge_0 [THEN leD, THEN antisym_conv1])
@@ -1953,7 +1953,7 @@
unfolding word_le_def by auto
lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
- by (simp only: word_le_def word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
+ by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p)
lemma word_n1_ge [simp]: "y \<le> -1"
for y :: "'a::len word"
@@ -2056,28 +2056,34 @@
"(uint x + uint y < 2 ^ LENGTH('a)) =
(uint (x + y) = uint x + uint y)"
for x y :: "'a::len word"
- by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
+ by (metis add.right_neutral add_mono_thms_linordered_semiring(1) mod_pos_pos_trivial of_nat_0_le_iff uint_lt2p uint_nat uint_word_ariths(1))
lemma uint_mult_lem:
"(uint x * uint y < 2 ^ LENGTH('a)) =
(uint (x * y) = uint x * uint y)"
for x y :: "'a::len word"
- by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
+ 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 (auto simp: uint_word_ariths intro!: trans [OF _ int_mod_lem])
+ 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>
lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
- unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)
+ unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend)
lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
- unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
-
+ unfolding uint_word_ariths by (simp add: int_mod_ge)
+
lemma mod_add_if_z:
"x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
(x + y) mod z = (if x + y < z then x + y else x + y - z)"
for x y z :: int
- by (auto intro: int_mod_eq)
+ apply (auto simp add: not_less)
+ apply (rule antisym)
+ apply (metis diff_ge_0_iff_ge minus_mod_self2 zmod_le_nonneg_dividend)
+ apply (simp only: flip: minus_mod_self2 [of \<open>x + y\<close> z])
+ apply (rule int_mod_ge)
+ apply simp_all
+ done
lemma uint_plus_if':
"uint (a + b) =
@@ -2090,7 +2096,13 @@
"x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
(x - y) mod z = (if y \<le> x then x - y else x - y + z)"
for x y z :: int
- by (auto intro: int_mod_eq)
+ apply (auto simp add: not_le)
+ apply (rule antisym)
+ apply (simp only: flip: mod_add_self2 [of \<open>x - y\<close> z])
+ apply (rule zmod_le_nonneg_dividend)
+ apply simp
+ apply (metis add.commute add.right_neutral add_le_cancel_left diff_ge_0_iff_ge int_mod_ge le_less le_less_trans mod_add_self1 not_le not_less)
+ done
lemma uint_sub_if':
"uint (a - b) =
@@ -2301,10 +2313,7 @@
lemma udvd_incr_lem:
"up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
uq = ua + n' * uint K \<Longrightarrow> up + uint K \<le> uq"
- apply clarsimp
- apply (drule less_le_mult)
- apply safe
- done
+ by auto (metis int_distrib(1) linorder_not_less mult.left_neutral mult_right_mono uint_nonnegative zless_imp_add1_zle)
lemma udvd_incr':
"p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
@@ -2344,11 +2353,16 @@
prefer 2
apply (insert uint_range' [of s])[1]
apply arith
- apply (drule add.commute [THEN xtr1])
- apply (simp add: diff_less_eq [symmetric])
- apply (drule less_le_mult)
- apply arith
+ apply (drule add.commute [THEN xtrans(1)])
+ apply (simp flip: diff_less_eq)
+ apply (subst (asm) mult_less_cancel_right)
apply simp
+ apply (simp add: diff_eq_eq not_less)
+ apply (subst (asm) (3) zless_iff_Suc_zadd)
+ apply auto
+ apply (auto simp add: algebra_simps)
+ apply (drule less_le_trans [of _ \<open>2 ^ LENGTH('a)\<close>]) apply assumption
+ apply (simp add: mult_less_0_iff)
done
\<comment> \<open>links with \<open>rbl\<close> operations\<close>
@@ -2527,15 +2541,27 @@
lemma unat_add_lem:
"unat x + unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x + y) = unat x + unat y"
for x y :: "'a::len word"
- by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
+ apply (auto simp: unat_word_ariths)
+ apply (metis unat_lt2p word_unat.eq_norm)
+ done
lemma unat_mult_lem:
"unat x * unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
for x y :: "'a::len word"
- by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
-
-lemmas unat_plus_if' =
- trans [OF unat_word_ariths(1) mod_nat_add, simplified]
+ apply (auto simp: unat_word_ariths)
+ apply (metis unat_lt2p word_unat.eq_norm)
+ done
+
+lemma unat_plus_if':
+ \<open>unat (a + b) =
+ (if unat a + unat b < 2 ^ LENGTH('a)
+ then unat a + unat b
+ else unat a + unat b - 2 ^ LENGTH('a))\<close> for a b :: \<open>'a::len word\<close>
+ apply (auto simp: unat_word_ariths not_less)
+ apply (subst (asm) le_iff_add)
+ apply auto
+ apply (metis add_less_cancel_left add_less_cancel_right le_less_trans less_imp_le mod_less unat_lt2p)
+ done
lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
for a b x :: "'a::len word"
@@ -2568,30 +2594,22 @@
lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
-lemma unat_div: "unat (x div y) = unat x div unat y"
- for x y :: " 'a::len word"
- apply (simp add : unat_word_ariths)
- apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
- apply (rule div_le_dividend)
- done
-
+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)
+
+lemma unat_div:
+ \<open>unat (x div y) = unat x div unat y\<close>
+ by (simp add: unat_def uint_div add: nat_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)
+
lemma unat_mod: "unat (x mod y) = unat x mod unat y"
for x y :: "'a::len word"
- apply (clarsimp simp add : unat_word_ariths)
- apply (cases "unat y")
- prefer 2
- apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
- apply (rule mod_le_divisor)
- apply auto
- done
-
-lemma uint_div: "uint (x div y) = uint x div uint y"
- for x y :: "'a::len word"
- by (simp add: uint_nat unat_div zdiv_int)
-
-lemma uint_mod: "uint (x mod y) = uint x mod uint y"
- for x y :: "'a::len word"
- by (simp add: uint_nat unat_mod zmod_int)
+ by (simp add: unat_def uint_mod add: nat_mod_distrib)
+
text \<open>Definition of \<open>unat_arith\<close> tactic\<close>
@@ -2671,7 +2689,7 @@
apply clarsimp
apply (drule mult_le_mono1)
apply (erule order_le_less_trans)
- apply (rule xtr7 [OF unat_lt2p div_mult_le])
+ apply (metis add_lessD1 div_mult_mod_eq unat_lt2p)
done
lemmas div_lt'' = order_less_imp_le [THEN div_lt']
@@ -2682,7 +2700,7 @@
apply (simp add: unat_arith_simps)
apply (drule (1) mult_less_mono1)
apply (erule order_less_le_trans)
- apply (rule div_mult_le)
+ apply auto
done
lemma div_le_mult: "i \<le> k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x \<le> k"
@@ -2691,7 +2709,7 @@
apply (simp add: unat_arith_simps)
apply (drule mult_le_mono1)
apply (erule order_trans)
- apply (rule div_mult_le)
+ apply auto
done
lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ LENGTH('a)"
@@ -2705,12 +2723,8 @@
lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ LENGTH('a)"
for x y z :: "'a::len word"
- apply (rule exI)
- apply (rule conjI)
- apply (rule zadd_diff_inverse)
- apply uint_arith
- done
-
+ by (metis add_diff_cancel_left' add_diff_eq uint_add_lem uint_plus_simple)
+
lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
lemmas plus_minus_no_overflow =
@@ -2727,32 +2741,20 @@
lemmas thd = times_div_less_eq_dividend
-lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
+lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend
lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n"
for n b :: "'a::len word"
- apply (unfold word_less_nat_alt word_arith_nat_defs)
- apply (cut_tac y="unat b" in gt_or_eq_0)
- apply (erule disjE)
- apply (simp only: div_mult_mod_eq uno_simps Word.word_unat.Rep_inverse)
- apply simp
- done
+ by (fact div_mult_mod_eq)
lemma word_div_mult_le: "a div b * b \<le> a"
for a b :: "'a::len word"
- apply (unfold word_le_nat_alt word_arith_nat_defs)
- apply (cut_tac y="unat b" in gt_or_eq_0)
- apply (erule disjE)
- apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse)
- apply simp
- done
+ by (metis div_le_mult mult_not_zero order.not_eq_order_implies_strict order_refl word_zero_le)
lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < n"
for m n :: "'a::len word"
- apply (simp only: word_less_nat_alt word_arith_nat_defs)
- apply (auto simp: uno_simps)
- done
-
+ by (simp add: unat_arith_simps)
+
lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
by (induct n) (simp_all add: wi_hom_mult [symmetric])
@@ -3039,9 +3041,9 @@
for x y :: "'a::len word"
by (auto simp: word_le_def uint_or intro: le_int_or)
-lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
-lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
-lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
+lemmas le_word_or1 = xtrans(3) [OF word_bw_comms (2) le_word_or2]
+lemmas word_and_le1 = xtrans(3) [OF word_ao_absorbs (4) [symmetric] le_word_or2]
+lemmas word_and_le2 = xtrans(3) [OF word_ao_absorbs (8) [symmetric] le_word_or2]
lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
unfolding to_bl_def word_log_defs bl_not_bin
@@ -3129,12 +3131,7 @@
unfolding to_bl_def word_test_bit_def word_size by (rule bin_nth_uint)
lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
- apply (unfold test_bit_bl)
- apply clarsimp
- apply (rule trans)
- apply (rule nth_rev_alt)
- apply (auto simp add: word_size)
- done
+ by (simp add: word_size rev_nth test_bit_bl)
lemma map_bit_interval_eq:
\<open>map (bit w) [0..<n] = takefill False n (rev (to_bl w))\<close> for w :: \<open>'a::len word\<close>
@@ -3325,7 +3322,7 @@
lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
for x :: "'a::len word"
- apply (rule xtr3)
+ apply (rule xtrans(3))
apply (rule_tac [2] y = "x" in le_word_or2)
apply (rule word_eqI)
apply (auto simp add: word_ao_nth nth_w2p word_size)
@@ -3433,7 +3430,7 @@
by (simp add: shiftl1_def)
lemma shiftl1_def_u: "shiftl1 w = word_of_int (2 * uint w)"
- by (simp only: shiftl1_def) (* FIXME: duplicate *)
+ by (fact shiftl1_def)
lemma shiftl1_def_s: "shiftl1 w = word_of_int (2 * sint w)"
by (simp add: shiftl1_def wi_hom_syms)
@@ -3555,10 +3552,7 @@
apply (unfold shiftr1_def)
apply (rule word_uint.Abs_inverse)
apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
- apply (rule xtr7)
- prefer 2
- apply (rule zdiv_le_dividend)
- apply auto
+ apply (metis uint_lt2p uint_shiftr1)
done
lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
@@ -3599,8 +3593,9 @@
subsubsection \<open>shift functions in terms of lists of bools\<close>
-lemmas bshiftr1_numeral [simp] =
- bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
+lemma bshiftr1_numeral [simp]:
+ \<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close>
+ by (simp add: bshiftr1_def)
lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
@@ -3742,7 +3737,9 @@
finally show ?thesis .
qed
-lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
+lemma shiftl_numeral [simp]:
+ \<open>numeral k << numeral l = (push_bit (numeral l) (numeral k) :: 'a::len word)\<close>
+ by (fact shiftl_word_eq)
lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
by (simp add: shiftl_bl word_rep_drop word_size)
@@ -3778,19 +3775,23 @@
word_of_int (bin_rest (sbintrunc (LENGTH('a) - 1) (numeral w)))"
unfolding sshiftr1_def word_numeral_alt by (simp add: word_sbin.eq_norm)
-lemma shiftr_no [simp]:
- (* FIXME: neg_numeral *)
- "(numeral w::'a::len word) >> n = word_of_int
- ((bin_rest ^^ n) (bintrunc (LENGTH('a)) (numeral w)))"
- by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
-
-lemma sshiftr_no [simp]:
- (* FIXME: neg_numeral *)
- "(numeral w::'a::len word) >>> n = word_of_int
- ((bin_rest ^^ n) (sbintrunc (LENGTH('a) - 1) (numeral w)))"
+text \<open>TODO: rules for \<^term>\<open>- (numeral n)\<close>\<close>
+
+lemma drop_bit_word_numeral [simp]:
+ \<open>drop_bit (numeral n) (numeral k) =
+ (word_of_int (drop_bit (numeral n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
+ by transfer simp
+
+lemma shiftr_numeral [simp]:
+ \<open>(numeral k >> numeral n :: 'a::len word) = drop_bit (numeral n) (numeral k)\<close>
+ by (fact shiftr_word_eq)
+
+lemma sshiftr_numeral [simp]:
+ \<open>(numeral k >>> numeral n :: 'a::len word) =
+ word_of_int (drop_bit (numeral n) (sbintrunc (LENGTH('a) - 1) (numeral k)))\<close>
apply (rule word_eqI)
- apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
- apply (subgoal_tac "na + n = LENGTH('a) - Suc 0", simp, simp)+
+ apply (cases \<open>LENGTH('a)\<close>)
+ apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr nth_sbintr not_le not_less less_Suc_eq_le ac_simps)
done
lemma shiftr1_bl_of:
@@ -3938,24 +3939,18 @@
apply simp
apply (clarsimp simp add: to_bl_nth word_size)
apply (simp add: word_size word_ops_nth_size)
- apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
+ apply (auto simp add: word_size test_bit_bl nth_append rev_nth)
done
lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
by (simp only: and_mask_bintr bintrunc_mod2p)
lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
- apply (simp add: and_mask_bintr word_ubin.eq_norm)
- apply (simp add: bintrunc_mod2p)
- apply (rule xtr8)
- prefer 2
- apply (rule pos_mod_bound)
- apply auto
- done
+ by (simp add: and_mask_bintr uint.abs_eq min_def not_le lt2p_lem bintr_lt2p)
lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
for b n :: int
- by (simp add: int_mod_lem eq_sym_conv)
+ by auto (metis pos_mod_conj)+
lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
apply (simp add: and_mask_bintr)
@@ -3991,12 +3986,11 @@
lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
for x :: "'a::len word"
- apply (unfold word_less_alt word_numeral_alt)
- apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm
- simp del: word_of_int_numeral)
- apply (drule xtr8 [rotated])
- apply (rule int_mod_le)
- apply simp_all
+ apply (simp add: and_mask_bintr)
+ apply transfer
+ apply (simp add: ac_simps)
+ apply (auto simp add: min_def)
+ apply (metis bintrunc_bintrunc_ge mod_pos_pos_trivial mult.commute mult.left_neutral mult_zero_left not_le of_bool_def take_bit_eq_mod take_bit_nonnegative)
done
lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
@@ -4521,8 +4515,6 @@
lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
-lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
-
lemma nth_rcat_lem:
"n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow>
rev (concat (map to_bl wl)) ! n =
@@ -4530,9 +4522,8 @@
apply (induct wl)
apply clarsimp
apply (clarsimp simp add : nth_append size_rcat_lem)
- apply (simp (no_asm_use) only: mult_Suc [symmetric]
- td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
- apply clarsimp
+ apply (simp flip: mult_Suc minus_div_mult_eq_mod add: less_Suc_eq_le not_less)
+ apply (metis (no_types, lifting) diff_is_0_eq div_le_mono len_not_eq_0 less_Suc_eq less_mult_imp_div_less nonzero_mult_div_cancel_right not_le nth_Cons_0)
done
lemma test_bit_rcat:
@@ -4540,9 +4531,8 @@
(n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
for wl :: "'a::len word list"
apply (unfold word_rcat_bl word_size)
- apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
- apply safe
- apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
+ apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size)
+ apply (metis div_le_mono len_gt_0 len_not_eq_0 less_mult_imp_div_less mod_less_divisor nonzero_mult_div_cancel_right not_le nth_rcat_lem test_bit_bl word_size)
done
lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0"
@@ -4558,8 +4548,10 @@
for w :: \<open>'a::len word\<close>
apply (rule trans)
apply (rule test_bit_cong)
- apply (rule nth_rev_alt)
+ apply (rule rev_nth [of _ \<open>rev (word_rsplit w)\<close>, simplified rev_rev_ident])
+ apply simp
apply (rule that(1))
+ apply simp
apply (rule test_bit_rsplit)
apply (rule refl)
apply (rule asm_rl)
@@ -4589,13 +4581,13 @@
lemma length_word_rsplit_even_size:
"n = LENGTH('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
length (word_rsplit w :: 'a word list) = m"
- by (auto simp: length_word_rsplit_exp_size given_quot_alt)
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)
lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
lemmas tdle = times_div_less_eq_dividend
-lemmas dtle = xtr4 [OF tdle mult.commute]
+lemmas dtle = xtrans(4) [OF tdle mult.commute]
lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
apply (rule word_eqI)
@@ -4604,16 +4596,14 @@
apply (simp_all add: word_size
refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
apply safe
- apply (erule xtr7, rule dtle)+
+ apply (erule xtrans(7), rule dtle)+
done
lemma size_word_rsplit_rcat_size:
"word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * LENGTH('a)
\<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
for ws :: "'a::len word list" and frcw :: "'b::len word"
- apply (clarsimp simp: word_size length_word_rsplit_exp_size')
- apply (fast intro: given_quot_alt)
- done
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
lemma msrevs:
"0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
@@ -4636,12 +4626,11 @@
apply (rule trans)
apply (rule test_bit_rcat [OF refl refl])
apply (simp add: word_size)
- apply (subst nth_rev)
+ apply (subst rev_nth)
apply arith
- apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
+ apply (simp add: le0 [THEN [2] xtrans(7), THEN diff_Suc_less])
apply safe
apply (simp add: diff_mult_distrib)
- apply (rule mpl_lem)
apply (cases "size ws")
apply simp_all
done
@@ -5234,7 +5223,8 @@
for x y :: "'a::len word"
apply (subst word_arith_nat_defs)
apply (subst unat_of_nat)
- apply (simp add: mod_nat_add word_size)
+ apply (auto simp add: not_less word_size)
+ apply (metis not_le unat_plus_if' unat_word_ariths(1))
done
lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
@@ -5347,10 +5337,8 @@
lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
for n :: "'a::len word"
- apply (simp add: word_rec_def unat_word_ariths)
- apply (subst nat_mod_eq')
- apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
- apply simp
+ apply (auto simp add: word_rec_def unat_word_ariths)
+ apply (metis (mono_tags, lifting) old.nat.simps(7) unatSuc word_unat.Rep_inverse word_unat.eq_norm word_unat.td_th)
done
lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
--- a/src/HOL/Word/Word_Examples.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Word_Examples.thy Sat Jul 04 20:45:24 2020 +0000
@@ -81,7 +81,8 @@
lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
text "this is not exactly fast, but bearable"
-lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
+lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
+ by (simp add: numeral_eq_Suc)
text "this works only for replicate n True"
lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"