--- a/NEWS Wed Aug 05 17:19:35 2020 +0200
+++ b/NEWS Wed Aug 05 19:06:39 2020 +0200
@@ -63,6 +63,11 @@
* Session HOL-Word: Type word is restricted to bit strings consisting
of at least one bit. INCOMPATIBILITY.
+* Session HOL-Word: Various operations dealing with bit values
+represented as reversed lists of bools are separated into theory
+Reversed_Bit_Lists, included by theory More_Word rather than theory Word.
+INCOMPATIBILITY.
+
* Session HOL-Word: Bit operations NOT, AND, OR, XOR are based on
generic algebraic bit operations from HOL-Library.Bit_Operations.
INCOMPATIBILITY.
--- a/src/HOL/Word/Bit_Lists.thy Wed Aug 05 17:19:35 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,957 +0,0 @@
-(* 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)
-
-
-subsection \<open>More\<close>
-
-definition rotater1 :: "'a list \<Rightarrow> 'a list"
- where "rotater1 ys =
- (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)"
-
-definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
- where "rotater n = rotater1 ^^ n"
-
-lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
-
-lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
- by (cases l) (auto simp: rotater1_def)
-
-lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
- apply (unfold rotater1_def)
- apply (cases "l")
- apply (case_tac [2] "list")
- apply auto
- done
-
-lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
- by (cases l) (auto simp: rotater1_def)
-
-lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
- by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
-
-lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
- by (induct n) (auto simp: rotater_def intro: rotater1_rev')
-
-lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
- using rotater_rev' [where xs = "rev ys"] by simp
-
-lemma rotater_drop_take:
- "rotater n xs =
- drop (length xs - n mod length xs) xs @
- take (length xs - n mod length xs) xs"
- by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
-
-lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
- unfolding rotater_def by auto
-
-lemma nth_rotater:
- \<open>rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)\<close> if \<open>n < length xs\<close>
- using that by (simp add: rotater_drop_take nth_append not_less less_diff_conv ac_simps le_mod_geq)
-
-lemma nth_rotater1:
- \<open>rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)\<close> if \<open>n < length xs\<close>
- using that nth_rotater [of n xs 1] by simp
-
-lemma rotate_inv_plus [rule_format]:
- "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
- rotate k (rotater n xs) = rotate m xs \<and>
- rotater n (rotate k xs) = rotate m xs \<and>
- rotate n (rotater k xs) = rotater m xs"
- by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
-
-lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
-
-lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
-
-lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
-lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
-
-lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
- by auto
-
-lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
- by auto
-
-lemma length_rotater [simp]: "length (rotater n xs) = length xs"
- by (simp add : rotater_rev)
-
-lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
- apply (rule box_equals)
- defer
- apply (rule rotate_conv_mod [symmetric])+
- apply simp
- done
-
-lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
- by simp
-
-lemmas rotate_eqs =
- trans [OF rotate0 [THEN fun_cong] id_apply]
- rotate_rotate [symmetric]
- rotate_id
- rotate_conv_mod
- rotate_eq_mod
-
-lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
- simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
-lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
-lemmas rotater_eqs = rrs1 [simplified length_rotater]
-lemmas rotater_0 = rotater_eqs (1)
-lemmas rotater_add = rotater_eqs (2)
-
-lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
- by (induct xs) auto
-
-lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
- by (cases xs) (auto simp: rotater1_def last_map butlast_map)
-
-lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
- by (induct n) (auto simp: rotater_def rotater1_map)
-
-lemma but_last_zip [rule_format] :
- "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
- last (zip xs ys) = (last xs, last ys) \<and>
- butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
- apply (induct xs)
- apply auto
- apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
- done
-
-lemma but_last_map2 [rule_format] :
- "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
- last (map2 f xs ys) = f (last xs) (last ys) \<and>
- butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
- apply (induct xs)
- apply auto
- apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
- done
-
-lemma rotater1_zip:
- "length xs = length ys \<Longrightarrow>
- rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
- apply (unfold rotater1_def)
- apply (cases xs)
- apply auto
- apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
- done
-
-lemma rotater1_map2:
- "length xs = length ys \<Longrightarrow>
- rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
- by (simp add: rotater1_map rotater1_zip)
-
-lemmas lrth =
- box_equals [OF asm_rl length_rotater [symmetric]
- length_rotater [symmetric],
- THEN rotater1_map2]
-
-lemma rotater_map2:
- "length xs = length ys \<Longrightarrow>
- rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
- by (induct n) (auto intro!: lrth)
-
-lemma rotate1_map2:
- "length xs = length ys \<Longrightarrow>
- rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
- by (cases xs; cases ys) auto
-
-lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
- length_rotate [symmetric], THEN rotate1_map2]
-
-lemma rotate_map2:
- "length xs = length ys \<Longrightarrow>
- rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
- by (induct n) (auto intro!: lth)
-
-
-subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close>
-
-primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
- where
- Nil: "bl_to_bin_aux [] w = w"
- | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)"
-
-definition bl_to_bin :: "bool list \<Rightarrow> int"
- where "bl_to_bin bs = bl_to_bin_aux bs 0"
-
-primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
- where
- Z: "bin_to_bl_aux 0 w bl = bl"
- | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
-
-definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
- where "bin_to_bl n w = bin_to_bl_aux n w []"
-
-lemma bin_to_bl_aux_zero_minus_simp [simp]:
- "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
- by (cases n) auto
-
-lemma bin_to_bl_aux_minus1_minus_simp [simp]:
- "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
- by (cases n) auto
-
-lemma bin_to_bl_aux_one_minus_simp [simp]:
- "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
- by (cases n) auto
-
-lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
- "0 < n \<Longrightarrow>
- bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
- by (cases n) simp_all
-
-lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
- "0 < n \<Longrightarrow>
- bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
- by (cases n) simp_all
-
-lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
- by (induct bs arbitrary: w) auto
-
-lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
- by (induct n arbitrary: w bs) auto
-
-lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
- unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
-
-lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
- by (simp add: bin_to_bl_def bin_to_bl_aux_append)
-
-lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
- by (auto simp: bin_to_bl_def)
-
-lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
- by (induct n arbitrary: w bs) auto
-
-lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
- by (simp add: bin_to_bl_def size_bin_to_bl_aux)
-
-lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
- apply (induct bs arbitrary: w n)
- apply auto
- apply (simp_all only: add_Suc [symmetric])
- apply (auto simp add: bin_to_bl_def)
- done
-
-lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
- unfolding bl_to_bin_def
- apply (rule box_equals)
- apply (rule bl_bin_bl')
- prefer 2
- apply (rule bin_to_bl_aux.Z)
- apply simp
- done
-
-lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
- apply (rule_tac box_equals)
- defer
- apply (rule bl_bin_bl)
- apply (rule bl_bin_bl)
- apply simp
- done
-
-lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
- by (auto simp: bl_to_bin_def)
-
-lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
- by (auto simp: bl_to_bin_def)
-
-lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
- by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
-
-lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
- by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
-
-lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
- by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
-
-lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
- by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
-
-
-subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
-
-lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
- by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
-
-lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
- by (auto simp: bin_to_bl_def bin_bl_bin')
-
-lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
- by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
-
-lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
- by (auto intro: bl_to_bin_inj)
-
-lemma bin_to_bl_aux_bintr:
- "bin_to_bl_aux n (bintrunc m bin) bl =
- replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
- apply (induct n arbitrary: m bin bl)
- apply clarsimp
- apply clarsimp
- apply (case_tac "m")
- apply (clarsimp simp: bin_to_bl_zero_aux)
- apply (erule thin_rl)
- apply (induct_tac n)
- apply (auto simp add: take_bit_Suc)
- done
-
-lemma bin_to_bl_bintr:
- "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
- unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
-
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
- by (induct n) auto
-
-lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
- by (fact size_bin_to_bl_aux)
-
-lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
- by (fact size_bin_to_bl) (* FIXME: duplicate *)
-
-lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
- by (induction bs arbitrary: w) (simp_all add: bin_sign_def)
-
-lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
- by (simp add: bl_to_bin_def sign_bl_bin')
-
-lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
- by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
-
-lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
- unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
-
-lemma bin_nth_of_bl_aux:
- "bin_nth (bl_to_bin_aux bl w) n =
- (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
- apply (induction bl arbitrary: w)
- apply simp_all
- apply safe
- apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
- done
-
-lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
- by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
-
-lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
- apply (induct n arbitrary: m w)
- apply clarsimp
- apply (case_tac m, clarsimp)
- apply (clarsimp simp: bin_to_bl_def)
- apply (simp add: bin_to_bl_aux_alt)
- apply (case_tac m, clarsimp)
- apply (clarsimp simp: bin_to_bl_def)
- apply (simp add: bin_to_bl_aux_alt bit_Suc)
- done
-
-lemma nth_bin_to_bl_aux:
- "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
- (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
- apply (induction bl arbitrary: w)
- apply simp_all
- 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)"
- by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
-
-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)
-
-lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
-proof (induction bs arbitrary: w)
- case Nil
- then show ?case
- by simp
-next
- case (Cons b bs)
- from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
- show ?case
- apply (auto simp add: algebra_simps)
- apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
- apply (simp only: add.assoc)
- apply (rule pos_add_strict)
- apply simp_all
- done
-qed
-
-lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
-proof (induct bs)
- case Nil
- then show ?case by simp
-next
- case (Cons b bs)
- with bl_to_bin_lt2p_aux[where w=1] show ?case
- by (simp add: bl_to_bin_def)
-qed
-
-lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
- by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
-
-lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
-proof (induction bs arbitrary: w)
- case Nil
- then show ?case
- by simp
-next
- case (Cons b bs)
- from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
- show ?case
- apply (auto simp add: algebra_simps)
- apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
- apply (rule add_increasing)
- apply simp_all
- done
-qed
-
-lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
- apply (unfold bl_to_bin_def)
- apply (rule xtrans(4))
- apply (rule bl_to_bin_ge2p_aux)
- apply simp
- done
-
-lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
- apply (unfold bin_to_bl_def)
- apply (cases n, clarsimp)
- apply clarsimp
- apply (auto simp add: bin_to_bl_aux_alt)
- done
-
-lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
- using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
-
-lemma butlast_rest_bl2bin_aux:
- "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
- by (induct bl arbitrary: w) auto
-
-lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
- by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
-
-lemma trunc_bl2bin_aux:
- "bintrunc m (bl_to_bin_aux bl w) =
- bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
-proof (induct bl arbitrary: w)
- case Nil
- show ?case by simp
-next
- case (Cons b bl)
- show ?case
- proof (cases "m - length bl")
- case 0
- then have "Suc (length bl) - m = Suc (length bl - m)" by simp
- with Cons show ?thesis by simp
- next
- case (Suc n)
- then have "m - Suc (length bl) = n" by simp
- with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps)
- qed
-qed
-
-lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
- by (simp add: bl_to_bin_def trunc_bl2bin_aux)
-
-lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
- by (simp add: trunc_bl2bin)
-
-lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
- apply (rule trans)
- prefer 2
- apply (rule trunc_bl2bin [symmetric])
- apply (cases "k \<le> length bl")
- apply auto
- done
-
-lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
- apply (rule nth_equalityI)
- apply simp
- apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
- done
-
-lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
- by (induct xs arbitrary: w) auto
-
-lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
- unfolding bl_to_bin_def by (erule last_bin_last')
-
-lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
- by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
-
-lemma drop_bin2bl_aux:
- "drop m (bin_to_bl_aux n bin bs) =
- bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
- apply (induction n arbitrary: m bin bs)
- apply auto
- apply (case_tac "m \<le> n")
- apply (auto simp add: not_le Suc_diff_le)
- apply (case_tac "m - n")
- apply auto
- apply (use Suc_diff_Suc in fastforce)
- done
-
-lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
- by (simp add: bin_to_bl_def drop_bin2bl_aux)
-
-lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
- apply (induct m arbitrary: w bs)
- apply clarsimp
- apply clarsimp
- apply (simp add: bin_to_bl_aux_alt)
- apply (simp add: bin_to_bl_def)
- apply (simp add: bin_to_bl_aux_alt)
- done
-
-lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
- by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
-
-lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
- apply (induct n arbitrary: b c)
- apply clarsimp
- apply (clarsimp simp: Let_def split: prod.split_asm)
- apply (simp add: bin_to_bl_def)
- apply (simp add: take_bin2bl_lem drop_bit_Suc)
- done
-
-lemma bin_to_bl_drop_bit:
- "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
- using bin_split_take by simp
-
-lemma bin_split_take1:
- "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 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_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) =
- bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
- by (rule bit_eqI)
- (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
-
-lemma bin_to_bl_aux_cat:
- "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
- bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
- by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
-
-lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
- using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
- by (simp add: bl_to_bin_def [symmetric])
-
-lemma bin_to_bl_cat:
- "bin_to_bl (nv + nw) (bin_cat v nw w) =
- bin_to_bl_aux nv v (bin_to_bl nw w)"
- by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
-
-lemmas bl_to_bin_aux_app_cat =
- trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
-
-lemmas bin_to_bl_aux_cat_app =
- trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
-
-lemma bl_to_bin_app_cat:
- "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
- by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
-
-lemma bin_to_bl_cat_app:
- "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
- by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
-
-text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
-lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
- by (simp add: bl_to_bin_app_cat)
-
-lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
- apply (unfold bl_to_bin_def)
- apply (induct n)
- apply simp
- apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
- apply simp
- done
-
-lemma bin_exhaust:
- "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
- apply (cases \<open>even bin\<close>)
- apply (auto elim!: evenE oddE)
- apply fastforce
- apply fastforce
- done
-
-primrec rbl_succ :: "bool list \<Rightarrow> bool list"
- where
- Nil: "rbl_succ Nil = Nil"
- | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
-
-primrec rbl_pred :: "bool list \<Rightarrow> bool list"
- where
- Nil: "rbl_pred Nil = Nil"
- | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
-
-primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
- where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
- Nil: "rbl_add Nil x = Nil"
- | Cons: "rbl_add (y # ys) x =
- (let ws = rbl_add ys (tl x)
- in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
-
-primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
- where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
- Nil: "rbl_mult Nil x = Nil"
- | Cons: "rbl_mult (y # ys) x =
- (let ws = False # rbl_mult ys x
- in if y then rbl_add ws x else ws)"
-
-lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
- by (induct bl) auto
-
-lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
- by (induct bl) auto
-
-lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
- by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
-
-lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
- by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
-
-lemmas rbl_sizes [simp] =
- size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
-
-lemmas rbl_Nils =
- rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
-
-lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
- apply (induct bla arbitrary: blb)
- apply simp
- apply clarsimp
- apply (case_tac blb, clarsimp)
- apply (clarsimp simp: Let_def)
- done
-
-lemma rbl_add_take2:
- "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
- apply (induct bla arbitrary: blb)
- apply simp
- apply clarsimp
- apply (case_tac blb, clarsimp)
- apply (clarsimp simp: Let_def)
- done
-
-lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
- apply (induct bla arbitrary: blb)
- apply simp
- apply clarsimp
- apply (case_tac blb, clarsimp)
- apply (clarsimp simp: Let_def rbl_add_app2)
- done
-
-lemma rbl_mult_take2:
- "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
- apply (rule trans)
- apply (rule rbl_mult_app2 [symmetric])
- apply simp
- apply (rule_tac f = "rbl_mult bla" in arg_cong)
- apply (rule append_take_drop_id)
- done
-
-lemma rbl_add_split:
- "P (rbl_add (y # ys) (x # xs)) =
- (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
- (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
- (\<not> y \<longrightarrow> P (x # ws)))"
- by (cases y) (auto simp: Let_def)
-
-lemma rbl_mult_split:
- "P (rbl_mult (y # ys) xs) =
- (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
- (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
- by (auto simp: Let_def)
-
-lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
-proof (unfold bin_to_bl_def, induction n arbitrary: bin)
- case 0
- then show ?case
- by simp
-next
- case (Suc n)
- obtain b k where \<open>bin = of_bool b + 2 * k\<close>
- using bin_exhaust by blast
- moreover have \<open>(2 * k - 1) div 2 = k - 1\<close>
- using even_succ_div_2 [of \<open>2 * (k - 1)\<close>]
- by simp
- ultimately show ?case
- using Suc [of \<open>bin div 2\<close>]
- by simp (simp add: bin_to_bl_aux_alt)
-qed
-
-lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
- apply (unfold bin_to_bl_def)
- apply (induction n arbitrary: bin)
- apply simp_all
- apply (case_tac bin rule: bin_exhaust)
- apply simp
- apply (simp add: bin_to_bl_aux_alt ac_simps)
- done
-
-lemma rbl_add:
- "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
- rev (bin_to_bl n (bina + binb))"
- apply (unfold bin_to_bl_def)
- apply (induct n)
- apply simp
- apply clarsimp
- apply (case_tac bina rule: bin_exhaust)
- apply (case_tac binb rule: bin_exhaust)
- apply (case_tac b)
- apply (case_tac [!] "ba")
- apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
- done
-
-lemma rbl_add_long:
- "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
- rev (bin_to_bl n (bina + binb))"
- apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
- apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
- apply (rule rev_swap [THEN iffD1])
- apply (simp add: rev_take drop_bin2bl)
- apply simp
- done
-
-lemma rbl_mult_gt1:
- "m \<ge> length bl \<Longrightarrow>
- rbl_mult bl (rev (bin_to_bl m binb)) =
- rbl_mult bl (rev (bin_to_bl (length bl) binb))"
- apply (rule trans)
- apply (rule rbl_mult_take2 [symmetric])
- apply simp_all
- apply (rule_tac f = "rbl_mult bl" in arg_cong)
- apply (rule rev_swap [THEN iffD1])
- apply (simp add: rev_take drop_bin2bl)
- done
-
-lemma rbl_mult_gt:
- "m > n \<Longrightarrow>
- rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
- rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
- by (auto intro: trans [OF rbl_mult_gt1])
-
-lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
-
-lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
- by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
-
-lemma rbl_mult:
- "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
- rev (bin_to_bl n (bina * binb))"
- apply (induct n arbitrary: bina binb)
- apply simp_all
- apply (unfold bin_to_bl_def)
- apply clarsimp
- apply (case_tac bina rule: bin_exhaust)
- apply (case_tac binb rule: bin_exhaust)
- apply simp
- apply (simp add: bin_to_bl_aux_alt)
- apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
- done
-
-lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
- by (induct xs) auto
-
-lemma bin_cat_foldl_lem:
- "foldl (\<lambda>u. bin_cat u n) x xs =
- bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
- apply (induct xs arbitrary: x)
- apply simp
- apply (simp (no_asm))
- apply (frule asm_rl)
- apply (drule meta_spec)
- apply (erule trans)
- apply (drule_tac x = "bin_cat y n a" in meta_spec)
- apply (simp add: bin_cat_assoc_sym min.absorb2)
- done
-
-lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
- apply (unfold bin_rcat_def)
- apply (rule sym)
- apply (induct wl)
- apply (auto simp add: bl_to_bin_append)
- apply (simp add: bl_to_bin_aux_alt sclem)
- apply (simp add: bin_cat_foldl_lem [symmetric])
- done
-
-lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
-by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
-
-lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
-by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
-
-lemma bl_xor_aux_bin:
- "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
- apply (induction n arbitrary: v w bs cs)
- apply auto
- apply (case_tac v rule: bin_exhaust)
- apply (case_tac w rule: bin_exhaust)
- apply clarsimp
- done
-
-lemma bl_or_aux_bin:
- "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
- by (induct n arbitrary: v w bs cs) simp_all
-
-lemma bl_and_aux_bin:
- "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
- by (induction n arbitrary: v w bs cs) simp_all
-
-lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
- by (induct n arbitrary: w cs) auto
-
-lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
- by (simp add: bin_to_bl_def bl_not_aux_bin)
-
-lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
- by (simp add: bin_to_bl_def bl_and_aux_bin)
-
-lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
- by (simp add: bin_to_bl_def bl_or_aux_bin)
-
-lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
- using bl_xor_aux_bin by (simp add: bin_to_bl_def)
-
-end
--- a/src/HOL/Word/Bits_Int.thy Wed Aug 05 17:19:35 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy Wed Aug 05 19:06:39 2020 +0200
@@ -489,8 +489,17 @@
lemma bin_cat_assoc_sym: "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
by (fact concat_bit_assoc_sym)
-definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
- where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
+definition bin_rcat :: \<open>nat \<Rightarrow> int list \<Rightarrow> int\<close>
+ where \<open>bin_rcat n = horner_sum (take_bit n) (2 ^ n) \<circ> rev\<close>
+
+lemma bin_rcat_eq_foldl:
+ \<open>bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0\<close>
+proof
+ fix ks :: \<open>int list\<close>
+ show \<open>bin_rcat n ks = foldl (\<lambda>u v. bin_cat u n v) 0 ks\<close>
+ by (induction ks rule: rev_induct)
+ (simp_all add: bin_rcat_def concat_bit_eq push_bit_eq_mult)
+qed
fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
where "bin_rsplit_aux n m c bs =
@@ -719,7 +728,7 @@
lemma bin_rsplit_rcat [rule_format]:
"n > 0 \<longrightarrow> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
- apply (unfold bin_rsplit_def bin_rcat_def)
+ apply (unfold bin_rsplit_def bin_rcat_eq_foldl)
apply (rule_tac xs = ws in rev_induct)
apply clarsimp
apply clarsimp
--- a/src/HOL/Word/Misc_lsb.thy Wed Aug 05 17:19:35 2020 +0200
+++ b/src/HOL/Word/Misc_lsb.thy Wed Aug 05 19:06:39 2020 +0200
@@ -4,7 +4,9 @@
section \<open>Operation variant for the least significant bit\<close>
theory Misc_lsb
- imports Word
+ imports
+ Word
+ Reversed_Bit_Lists
begin
class lsb = semiring_bits +
--- a/src/HOL/Word/Misc_msb.thy Wed Aug 05 17:19:35 2020 +0200
+++ b/src/HOL/Word/Misc_msb.thy Wed Aug 05 19:06:39 2020 +0200
@@ -4,7 +4,9 @@
section \<open>Operation variant for the most significant bit\<close>
theory Misc_msb
- imports Word
+ imports
+ Word
+ Reversed_Bit_Lists
begin
class msb =
--- a/src/HOL/Word/More_Word.thy Wed Aug 05 17:19:35 2020 +0200
+++ b/src/HOL/Word/More_Word.thy Wed Aug 05 19:06:39 2020 +0200
@@ -7,6 +7,7 @@
imports
Word
Ancient_Numeral
+ Reversed_Bit_Lists
Misc_Auxiliary
Misc_Arithmetic
Misc_set_bit
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Reversed_Bit_Lists.thy Wed Aug 05 19:06:39 2020 +0200
@@ -0,0 +1,1835 @@
+(* Title: HOL/Word/Reversed_Bit_Lists.thy
+ Author: Jeremy Dawson, NICTA
+*)
+
+section \<open>Bit values as reversed lists of bools\<close>
+
+theory Reversed_Bit_Lists
+ imports Word
+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)
+
+
+subsection \<open>More\<close>
+
+definition rotater1 :: "'a list \<Rightarrow> 'a list"
+ where "rotater1 ys =
+ (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)"
+
+definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ where "rotater n = rotater1 ^^ n"
+
+lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
+
+lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
+ by (cases l) (auto simp: rotater1_def)
+
+lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
+ apply (unfold rotater1_def)
+ apply (cases "l")
+ apply (case_tac [2] "list")
+ apply auto
+ done
+
+lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
+ by (cases l) (auto simp: rotater1_def)
+
+lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
+ by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
+
+lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
+ by (induct n) (auto simp: rotater_def intro: rotater1_rev')
+
+lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
+ using rotater_rev' [where xs = "rev ys"] by simp
+
+lemma rotater_drop_take:
+ "rotater n xs =
+ drop (length xs - n mod length xs) xs @
+ take (length xs - n mod length xs) xs"
+ by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
+
+lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
+ unfolding rotater_def by auto
+
+lemma nth_rotater:
+ \<open>rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)\<close> if \<open>n < length xs\<close>
+ using that by (simp add: rotater_drop_take nth_append not_less less_diff_conv ac_simps le_mod_geq)
+
+lemma nth_rotater1:
+ \<open>rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)\<close> if \<open>n < length xs\<close>
+ using that nth_rotater [of n xs 1] by simp
+
+lemma rotate_inv_plus [rule_format]:
+ "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
+ rotate k (rotater n xs) = rotate m xs \<and>
+ rotater n (rotate k xs) = rotate m xs \<and>
+ rotate n (rotater k xs) = rotater m xs"
+ by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
+
+lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
+
+lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
+
+lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
+lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
+
+lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
+ by auto
+
+lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
+ by auto
+
+lemma length_rotater [simp]: "length (rotater n xs) = length xs"
+ by (simp add : rotater_rev)
+
+lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
+ apply (rule box_equals)
+ defer
+ apply (rule rotate_conv_mod [symmetric])+
+ apply simp
+ done
+
+lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
+ by simp
+
+lemmas rotate_eqs =
+ trans [OF rotate0 [THEN fun_cong] id_apply]
+ rotate_rotate [symmetric]
+ rotate_id
+ rotate_conv_mod
+ rotate_eq_mod
+
+lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
+ simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
+lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
+lemmas rotater_eqs = rrs1 [simplified length_rotater]
+lemmas rotater_0 = rotater_eqs (1)
+lemmas rotater_add = rotater_eqs (2)
+
+lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
+ by (induct xs) auto
+
+lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
+ by (cases xs) (auto simp: rotater1_def last_map butlast_map)
+
+lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
+ by (induct n) (auto simp: rotater_def rotater1_map)
+
+lemma but_last_zip [rule_format] :
+ "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
+ last (zip xs ys) = (last xs, last ys) \<and>
+ butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
+ apply (induct xs)
+ apply auto
+ apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
+ done
+
+lemma but_last_map2 [rule_format] :
+ "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
+ last (map2 f xs ys) = f (last xs) (last ys) \<and>
+ butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
+ apply (induct xs)
+ apply auto
+ apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
+ done
+
+lemma rotater1_zip:
+ "length xs = length ys \<Longrightarrow>
+ rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
+ apply (unfold rotater1_def)
+ apply (cases xs)
+ apply auto
+ apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
+ done
+
+lemma rotater1_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
+ by (simp add: rotater1_map rotater1_zip)
+
+lemmas lrth =
+ box_equals [OF asm_rl length_rotater [symmetric]
+ length_rotater [symmetric],
+ THEN rotater1_map2]
+
+lemma rotater_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
+ by (induct n) (auto intro!: lrth)
+
+lemma rotate1_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
+ by (cases xs; cases ys) auto
+
+lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
+ length_rotate [symmetric], THEN rotate1_map2]
+
+lemma rotate_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
+ by (induct n) (auto intro!: lth)
+
+
+subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close>
+
+primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
+ where
+ Nil: "bl_to_bin_aux [] w = w"
+ | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)"
+
+definition bl_to_bin :: "bool list \<Rightarrow> int"
+ where "bl_to_bin bs = bl_to_bin_aux bs 0"
+
+primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
+ where
+ Z: "bin_to_bl_aux 0 w bl = bl"
+ | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
+
+definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
+ where "bin_to_bl n w = bin_to_bl_aux n w []"
+
+lemma bin_to_bl_aux_zero_minus_simp [simp]:
+ "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_minus1_minus_simp [simp]:
+ "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_one_minus_simp [simp]:
+ "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
+ "0 < n \<Longrightarrow>
+ bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
+ by (cases n) simp_all
+
+lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
+ "0 < n \<Longrightarrow>
+ bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
+ by (cases n) simp_all
+
+lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
+ by (induct bs arbitrary: w) auto
+
+lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
+ by (induct n arbitrary: w bs) auto
+
+lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
+ unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
+
+lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
+ by (simp add: bin_to_bl_def bin_to_bl_aux_append)
+
+lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
+ by (auto simp: bin_to_bl_def)
+
+lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
+ by (induct n arbitrary: w bs) auto
+
+lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
+ by (simp add: bin_to_bl_def size_bin_to_bl_aux)
+
+lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
+ apply (induct bs arbitrary: w n)
+ apply auto
+ apply (simp_all only: add_Suc [symmetric])
+ apply (auto simp add: bin_to_bl_def)
+ done
+
+lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
+ unfolding bl_to_bin_def
+ apply (rule box_equals)
+ apply (rule bl_bin_bl')
+ prefer 2
+ apply (rule bin_to_bl_aux.Z)
+ apply simp
+ done
+
+lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
+ apply (rule_tac box_equals)
+ defer
+ apply (rule bl_bin_bl)
+ apply (rule bl_bin_bl)
+ apply simp
+ done
+
+lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
+ by (auto simp: bl_to_bin_def)
+
+lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
+ by (auto simp: bl_to_bin_def)
+
+lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
+ by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
+
+lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
+ by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
+
+lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
+ by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
+
+lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
+ by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
+
+
+subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
+
+lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
+ by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
+
+lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
+ by (auto simp: bin_to_bl_def bin_bl_bin')
+
+lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
+ by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
+
+lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
+ by (auto intro: bl_to_bin_inj)
+
+lemma bin_to_bl_aux_bintr:
+ "bin_to_bl_aux n (bintrunc m bin) bl =
+ replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
+ apply (induct n arbitrary: m bin bl)
+ apply clarsimp
+ apply clarsimp
+ apply (case_tac "m")
+ apply (clarsimp simp: bin_to_bl_zero_aux)
+ apply (erule thin_rl)
+ apply (induct_tac n)
+ apply (auto simp add: take_bit_Suc)
+ done
+
+lemma bin_to_bl_bintr:
+ "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
+ unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
+
+lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
+ by (induct n) auto
+
+lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
+ by (fact size_bin_to_bl_aux)
+
+lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
+ by (fact size_bin_to_bl) (* FIXME: duplicate *)
+
+lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
+ by (induction bs arbitrary: w) (simp_all add: bin_sign_def)
+
+lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
+ by (simp add: bl_to_bin_def sign_bl_bin')
+
+lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
+ by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
+
+lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
+ unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
+
+lemma bin_nth_of_bl_aux:
+ "bin_nth (bl_to_bin_aux bl w) n =
+ (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
+ apply (induction bl arbitrary: w)
+ apply simp_all
+ apply safe
+ apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
+ done
+
+lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
+ by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
+
+lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
+ apply (induct n arbitrary: m w)
+ apply clarsimp
+ apply (case_tac m, clarsimp)
+ apply (clarsimp simp: bin_to_bl_def)
+ apply (simp add: bin_to_bl_aux_alt)
+ apply (case_tac m, clarsimp)
+ apply (clarsimp simp: bin_to_bl_def)
+ apply (simp add: bin_to_bl_aux_alt bit_Suc)
+ done
+
+lemma nth_bin_to_bl_aux:
+ "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
+ (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
+ apply (induction bl arbitrary: w)
+ apply simp_all
+ 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)"
+ by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
+
+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)
+
+lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
+proof (induction bs arbitrary: w)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
+ show ?case
+ apply (auto simp add: algebra_simps)
+ apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
+ apply (simp only: add.assoc)
+ apply (rule pos_add_strict)
+ apply simp_all
+ done
+qed
+
+lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
+proof (induct bs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons b bs)
+ with bl_to_bin_lt2p_aux[where w=1] show ?case
+ by (simp add: bl_to_bin_def)
+qed
+
+lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
+ by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
+
+lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
+proof (induction bs arbitrary: w)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
+ show ?case
+ apply (auto simp add: algebra_simps)
+ apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
+ apply (rule add_increasing)
+ apply simp_all
+ done
+qed
+
+lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
+ apply (unfold bl_to_bin_def)
+ apply (rule xtrans(4))
+ apply (rule bl_to_bin_ge2p_aux)
+ apply simp
+ done
+
+lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
+ apply (unfold bin_to_bl_def)
+ apply (cases n, clarsimp)
+ apply clarsimp
+ apply (auto simp add: bin_to_bl_aux_alt)
+ done
+
+lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
+ using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
+
+lemma butlast_rest_bl2bin_aux:
+ "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
+ by (induct bl arbitrary: w) auto
+
+lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
+ by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
+
+lemma trunc_bl2bin_aux:
+ "bintrunc m (bl_to_bin_aux bl w) =
+ bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
+proof (induct bl arbitrary: w)
+ case Nil
+ show ?case by simp
+next
+ case (Cons b bl)
+ show ?case
+ proof (cases "m - length bl")
+ case 0
+ then have "Suc (length bl) - m = Suc (length bl - m)" by simp
+ with Cons show ?thesis by simp
+ next
+ case (Suc n)
+ then have "m - Suc (length bl) = n" by simp
+ with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps)
+ qed
+qed
+
+lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
+ by (simp add: bl_to_bin_def trunc_bl2bin_aux)
+
+lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
+ by (simp add: trunc_bl2bin)
+
+lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
+ apply (rule trans)
+ prefer 2
+ apply (rule trunc_bl2bin [symmetric])
+ apply (cases "k \<le> length bl")
+ apply auto
+ done
+
+lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
+ apply (rule nth_equalityI)
+ apply simp
+ apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
+ done
+
+lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
+ by (induct xs arbitrary: w) auto
+
+lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
+ unfolding bl_to_bin_def by (erule last_bin_last')
+
+lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
+ by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
+
+lemma drop_bin2bl_aux:
+ "drop m (bin_to_bl_aux n bin bs) =
+ bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
+ apply (induction n arbitrary: m bin bs)
+ apply auto
+ apply (case_tac "m \<le> n")
+ apply (auto simp add: not_le Suc_diff_le)
+ apply (case_tac "m - n")
+ apply auto
+ apply (use Suc_diff_Suc in fastforce)
+ done
+
+lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
+ by (simp add: bin_to_bl_def drop_bin2bl_aux)
+
+lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
+ apply (induct m arbitrary: w bs)
+ apply clarsimp
+ apply clarsimp
+ apply (simp add: bin_to_bl_aux_alt)
+ apply (simp add: bin_to_bl_def)
+ apply (simp add: bin_to_bl_aux_alt)
+ done
+
+lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
+ by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
+
+lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
+ apply (induct n arbitrary: b c)
+ apply clarsimp
+ apply (clarsimp simp: Let_def split: prod.split_asm)
+ apply (simp add: bin_to_bl_def)
+ apply (simp add: take_bin2bl_lem drop_bit_Suc)
+ done
+
+lemma bin_to_bl_drop_bit:
+ "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
+ using bin_split_take by simp
+
+lemma bin_split_take1:
+ "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 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_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) =
+ bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
+ by (rule bit_eqI)
+ (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
+
+lemma bin_to_bl_aux_cat:
+ "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
+ bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
+ by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
+
+lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
+ using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
+ by (simp add: bl_to_bin_def [symmetric])
+
+lemma bin_to_bl_cat:
+ "bin_to_bl (nv + nw) (bin_cat v nw w) =
+ bin_to_bl_aux nv v (bin_to_bl nw w)"
+ by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
+
+lemmas bl_to_bin_aux_app_cat =
+ trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
+
+lemmas bin_to_bl_aux_cat_app =
+ trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
+
+lemma bl_to_bin_app_cat:
+ "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
+ by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
+
+lemma bin_to_bl_cat_app:
+ "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
+ by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
+
+text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
+lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
+ by (simp add: bl_to_bin_app_cat)
+
+lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
+ apply (unfold bl_to_bin_def)
+ apply (induct n)
+ apply simp
+ apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
+ apply simp
+ done
+
+lemma bin_exhaust:
+ "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
+ apply (cases \<open>even bin\<close>)
+ apply (auto elim!: evenE oddE)
+ apply fastforce
+ apply fastforce
+ done
+
+primrec rbl_succ :: "bool list \<Rightarrow> bool list"
+ where
+ Nil: "rbl_succ Nil = Nil"
+ | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
+
+primrec rbl_pred :: "bool list \<Rightarrow> bool list"
+ where
+ Nil: "rbl_pred Nil = Nil"
+ | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
+
+primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+ where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
+ Nil: "rbl_add Nil x = Nil"
+ | Cons: "rbl_add (y # ys) x =
+ (let ws = rbl_add ys (tl x)
+ in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
+
+primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+ where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
+ Nil: "rbl_mult Nil x = Nil"
+ | Cons: "rbl_mult (y # ys) x =
+ (let ws = False # rbl_mult ys x
+ in if y then rbl_add ws x else ws)"
+
+lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
+ by (induct bl) auto
+
+lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
+ by (induct bl) auto
+
+lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
+ by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
+
+lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
+ by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
+
+lemmas rbl_sizes [simp] =
+ size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
+
+lemmas rbl_Nils =
+ rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
+
+lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
+ apply (induct bla arbitrary: blb)
+ apply simp
+ apply clarsimp
+ apply (case_tac blb, clarsimp)
+ apply (clarsimp simp: Let_def)
+ done
+
+lemma rbl_add_take2:
+ "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
+ apply (induct bla arbitrary: blb)
+ apply simp
+ apply clarsimp
+ apply (case_tac blb, clarsimp)
+ apply (clarsimp simp: Let_def)
+ done
+
+lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
+ apply (induct bla arbitrary: blb)
+ apply simp
+ apply clarsimp
+ apply (case_tac blb, clarsimp)
+ apply (clarsimp simp: Let_def rbl_add_app2)
+ done
+
+lemma rbl_mult_take2:
+ "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
+ apply (rule trans)
+ apply (rule rbl_mult_app2 [symmetric])
+ apply simp
+ apply (rule_tac f = "rbl_mult bla" in arg_cong)
+ apply (rule append_take_drop_id)
+ done
+
+lemma rbl_add_split:
+ "P (rbl_add (y # ys) (x # xs)) =
+ (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
+ (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
+ (\<not> y \<longrightarrow> P (x # ws)))"
+ by (cases y) (auto simp: Let_def)
+
+lemma rbl_mult_split:
+ "P (rbl_mult (y # ys) xs) =
+ (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
+ (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
+ by (auto simp: Let_def)
+
+lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
+proof (unfold bin_to_bl_def, induction n arbitrary: bin)
+ case 0
+ then show ?case
+ by simp
+next
+ case (Suc n)
+ obtain b k where \<open>bin = of_bool b + 2 * k\<close>
+ using bin_exhaust by blast
+ moreover have \<open>(2 * k - 1) div 2 = k - 1\<close>
+ using even_succ_div_2 [of \<open>2 * (k - 1)\<close>]
+ by simp
+ ultimately show ?case
+ using Suc [of \<open>bin div 2\<close>]
+ by simp (simp add: bin_to_bl_aux_alt)
+qed
+
+lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
+ apply (unfold bin_to_bl_def)
+ apply (induction n arbitrary: bin)
+ apply simp_all
+ apply (case_tac bin rule: bin_exhaust)
+ apply simp
+ apply (simp add: bin_to_bl_aux_alt ac_simps)
+ done
+
+lemma rbl_add:
+ "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+ rev (bin_to_bl n (bina + binb))"
+ apply (unfold bin_to_bl_def)
+ apply (induct n)
+ apply simp
+ apply clarsimp
+ apply (case_tac bina rule: bin_exhaust)
+ apply (case_tac binb rule: bin_exhaust)
+ apply (case_tac b)
+ apply (case_tac [!] "ba")
+ apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
+ done
+
+lemma rbl_add_long:
+ "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+ rev (bin_to_bl n (bina + binb))"
+ apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
+ apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
+ apply (rule rev_swap [THEN iffD1])
+ apply (simp add: rev_take drop_bin2bl)
+ apply simp
+ done
+
+lemma rbl_mult_gt1:
+ "m \<ge> length bl \<Longrightarrow>
+ rbl_mult bl (rev (bin_to_bl m binb)) =
+ rbl_mult bl (rev (bin_to_bl (length bl) binb))"
+ apply (rule trans)
+ apply (rule rbl_mult_take2 [symmetric])
+ apply simp_all
+ apply (rule_tac f = "rbl_mult bl" in arg_cong)
+ apply (rule rev_swap [THEN iffD1])
+ apply (simp add: rev_take drop_bin2bl)
+ done
+
+lemma rbl_mult_gt:
+ "m > n \<Longrightarrow>
+ rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+ rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
+ by (auto intro: trans [OF rbl_mult_gt1])
+
+lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
+
+lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
+ by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
+
+lemma rbl_mult:
+ "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+ rev (bin_to_bl n (bina * binb))"
+ apply (induct n arbitrary: bina binb)
+ apply simp_all
+ apply (unfold bin_to_bl_def)
+ apply clarsimp
+ apply (case_tac bina rule: bin_exhaust)
+ apply (case_tac binb rule: bin_exhaust)
+ apply simp
+ apply (simp add: bin_to_bl_aux_alt)
+ apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
+ done
+
+lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
+ by (induct xs) auto
+
+lemma bin_cat_foldl_lem:
+ "foldl (\<lambda>u. bin_cat u n) x xs =
+ bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
+ apply (induct xs arbitrary: x)
+ apply simp
+ apply (simp (no_asm))
+ apply (frule asm_rl)
+ apply (drule meta_spec)
+ apply (erule trans)
+ apply (drule_tac x = "bin_cat y n a" in meta_spec)
+ apply (simp add: bin_cat_assoc_sym min.absorb2)
+ done
+
+lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
+ apply (unfold bin_rcat_eq_foldl)
+ apply (rule sym)
+ apply (induct wl)
+ apply (auto simp add: bl_to_bin_append)
+ apply (simp add: bl_to_bin_aux_alt sclem)
+ apply (simp add: bin_cat_foldl_lem [symmetric])
+ done
+
+lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
+by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
+
+lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
+by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
+
+lemma bl_xor_aux_bin:
+ "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
+ apply (induction n arbitrary: v w bs cs)
+ apply auto
+ apply (case_tac v rule: bin_exhaust)
+ apply (case_tac w rule: bin_exhaust)
+ apply clarsimp
+ done
+
+lemma bl_or_aux_bin:
+ "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
+ by (induct n arbitrary: v w bs cs) simp_all
+
+lemma bl_and_aux_bin:
+ "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
+ by (induction n arbitrary: v w bs cs) simp_all
+
+lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
+ by (induct n arbitrary: w cs) auto
+
+lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
+ by (simp add: bin_to_bl_def bl_not_aux_bin)
+
+lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
+ by (simp add: bin_to_bl_def bl_and_aux_bin)
+
+lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
+ by (simp add: bin_to_bl_def bl_or_aux_bin)
+
+lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+ using bl_xor_aux_bin by (simp add: bin_to_bl_def)
+
+
+subsection \<open>Type \<^typ>\<open>'a word\<close>\<close>
+
+lift_definition of_bl :: \<open>bool list \<Rightarrow> 'a::len word\<close>
+ is bl_to_bin .
+
+lift_definition to_bl :: \<open>'a::len word \<Rightarrow> bool list\<close>
+ is \<open>bin_to_bl LENGTH('a)\<close>
+ by (simp add: bl_to_bin_inj)
+
+lemma to_bl_eq:
+ \<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer simp
+
+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)
+
+lemma rev_to_bl_eq:
+ \<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close>
+ for w :: \<open>'a::len word\<close>
+ apply (rule nth_equalityI)
+ apply (simp add: to_bl.rep_eq)
+ apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq)
+ done
+
+lemma of_bl_rev_eq:
+ \<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close>
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_of_bl_iff)
+ apply transfer
+ apply (simp add: bit_horner_sum_bit_iff ac_simps)
+ done
+
+lemma bshiftr1_eq:
+ \<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close>
+ apply transfer
+ apply auto
+ apply (subst bl_to_bin_app_cat [of \<open>[True]\<close>, simplified])
+ apply simp
+ apply (metis One_nat_def add.commute bin_bl_bin bin_last_bl_to_bin bin_rest_bl_to_bin butlast_bin_rest concat_bit_eq last.simps list.distinct(1) list.size(3) list.size(4) odd_iff_mod_2_eq_one plus_1_eq_Suc power_Suc0_right push_bit_of_1 size_bin_to_bl take_bit_eq_mod trunc_bl2bin_len)
+ apply (simp add: butlast_rest_bl2bin)
+ done
+
+lemma length_to_bl_eq:
+ \<open>length (to_bl w) = LENGTH('a)\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer simp
+
+lemma word_rotr_eq:
+ \<open>word_rotr n w = of_bl (rotater n (to_bl w))\<close>
+ apply (rule bit_word_eqI)
+ subgoal for n
+ apply (cases \<open>n < LENGTH('a)\<close>)
+ apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff rotater_rev length_to_bl_eq nth_rotate rev_to_bl_eq ac_simps)
+ done
+ done
+
+lemma word_rotl_eq:
+ \<open>word_rotl n w = of_bl (rotate n (to_bl w))\<close>
+proof -
+ have \<open>rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))\<close>
+ by (simp add: rotater_rev')
+ then show ?thesis
+ apply (simp add: word_rotl_eq_word_rotr bit_of_bl_iff length_to_bl_eq rev_to_bl_eq)
+ apply (rule bit_word_eqI)
+ subgoal for n
+ apply (cases \<open>n < LENGTH('a)\<close>)
+ apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff nth_rotater)
+ done
+ done
+qed
+
+lemma to_bl_def': "(to_bl :: 'a::len word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint"
+ by transfer (simp add: fun_eq_iff)
+
+\<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>
+lemma td_bl:
+ "type_definition
+ (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
+ done
+
+interpretation word_bl:
+ type_definition
+ "to_bl :: 'a::len word \<Rightarrow> bool list"
+ of_bl
+ "{bl. length bl = LENGTH('a::len)}"
+ by (fact td_bl)
+
+lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
+
+lemma word_size_bl: "size w = size (to_bl w)"
+ by (auto simp: word_size)
+
+lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)"
+ by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
+
+lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
+ for x :: "'a::len word"
+ unfolding word_bl_Rep' by (rule len_gt_0)
+
+lemma bl_not_Nil [iff]: "to_bl x \<noteq> []"
+ for x :: "'a::len word"
+ by (fact length_bl_gt_0 [unfolded length_greater_0_conv])
+
+lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
+ for x :: "'a::len word"
+ by (fact length_bl_gt_0 [THEN gr_implies_not0])
+
+lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
+ apply transfer
+ apply (auto simp add: bin_sign_def)
+ using bin_sign_lem bl_sbin_sign apply fastforce
+ using bin_sign_lem bl_sbin_sign apply force
+ done
+
+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])
+
+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)
+
+lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))"
+ by (simp add: of_bl_def)
+
+lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
+ by transfer simp
+
+lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
+ by (simp add: uint_bl word_size)
+
+lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len word) = bin_to_bl (LENGTH('a)) bin"
+ by (auto simp: uint_bl word_ubin.eq_norm word_size)
+
+lemma to_bl_numeral [simp]:
+ "to_bl (numeral bin::'a::len word) =
+ bin_to_bl (LENGTH('a)) (numeral bin)"
+ unfolding word_numeral_alt by (rule to_bl_of_bin)
+
+lemma to_bl_neg_numeral [simp]:
+ "to_bl (- numeral bin::'a::len word) =
+ bin_to_bl (LENGTH('a)) (- numeral bin)"
+ unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
+
+lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
+ by (simp add: uint_bl word_size)
+
+lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x"
+ for x :: "'a::len word"
+ by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
+
+lemma ucast_bl: "ucast w = of_bl (to_bl w)"
+ by transfer simp
+
+lemma ucast_down_bl:
+ \<open>(ucast :: 'a::len word \<Rightarrow> 'b::len word) (of_bl bl) = of_bl bl\<close>
+ if \<open>is_down (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
+ using that by transfer simp
+
+lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
+ by transfer (simp add: bl_to_bin_app_cat)
+
+lemma ucast_of_bl_up:
+ \<open>ucast (of_bl bl :: 'a::len word) = of_bl bl\<close>
+ if \<open>size bl \<le> size (of_bl bl :: 'a::len word)\<close>
+ using that
+ apply transfer
+ apply (rule bit_eqI)
+ apply (auto simp add: bit_take_bit_iff)
+ apply (subst (asm) trunc_bl2bin_len [symmetric])
+ apply (auto simp only: bit_take_bit_iff)
+ done
+
+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)
+
+lemma word_rep_drop:
+ "to_bl (of_bl bl::'a::len word) =
+ replicate (LENGTH('a) - length bl) False @
+ drop (length bl - LENGTH('a)) bl"
+ by (simp add: word_rev_tf takefill_alt rev_take)
+
+lemma to_bl_ucast:
+ "to_bl (ucast (w::'b::len word) ::'a::len word) =
+ replicate (LENGTH('a) - LENGTH('b)) False @
+ drop (LENGTH('b) - LENGTH('a)) (to_bl w)"
+ apply (unfold ucast_bl)
+ apply (rule trans)
+ apply (rule word_rep_drop)
+ apply simp
+ done
+
+lemma ucast_up_app:
+ \<open>to_bl (ucast w :: 'b::len word) = replicate n False @ (to_bl w)\<close>
+ if \<open>source_size (ucast :: 'a word \<Rightarrow> 'b word) + n = target_size (ucast :: 'a word \<Rightarrow> 'b word)\<close>
+ for w :: \<open>'a::len word\<close>
+ using that
+ by (auto simp add : source_size target_size to_bl_ucast)
+
+lemma ucast_down_drop [OF refl]:
+ "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
+ to_bl (uc w) = drop n (to_bl w)"
+ by (auto simp add : source_size target_size to_bl_ucast)
+
+lemma scast_down_drop [OF refl]:
+ "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
+ to_bl (sc w) = drop n (to_bl w)"
+ apply (subgoal_tac "sc = ucast")
+ apply safe
+ apply simp
+ apply (erule ucast_down_drop)
+ apply (rule down_cast_same [symmetric])
+ apply (simp add : source_size target_size is_down)
+ done
+
+lemma word_0_bl [simp]: "of_bl [] = 0"
+ by (simp add: of_bl_def)
+
+lemma word_1_bl: "of_bl [True] = 1"
+ by (simp add: of_bl_def 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)
+
+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)
+
+\<comment> \<open>links with \<open>rbl\<close> operations\<close>
+lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
+ by transfer (simp add: rbl_succ)
+
+lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
+ by transfer (simp add: rbl_pred)
+
+lemma word_add_rbl:
+ "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
+ to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))"
+ apply transfer
+ apply (drule sym)
+ apply (drule sym)
+ apply (simp add: rbl_add)
+ done
+
+lemma word_mult_rbl:
+ "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
+ to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))"
+ apply transfer
+ apply (drule sym)
+ apply (drule sym)
+ apply (simp add: rbl_mult)
+ done
+
+lemma rtb_rbl_ariths:
+ "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
+ "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
+ "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
+ "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
+ 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
+
+lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
+ by simp
+
+lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
+ by transfer (simp add: bl_not_bin)
+
+lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)"
+ by transfer (simp flip: bl_xor_bin)
+
+lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)"
+ by transfer (simp flip: bl_or_bin)
+
+lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)"
+ by transfer (simp flip: bl_and_bin)
+
+lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
+ apply (unfold word_size)
+ apply (safe elim!: bin_nth_uint_imp)
+ apply (frule bin_nth_uint_imp)
+ apply (fast dest!: bin_nth_bl)+
+ done
+
+lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
+
+lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
+ by transfer (auto simp add: bin_nth_bl)
+
+lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
+ 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>
+proof (rule nth_equalityI)
+ show \<open>length (map (bit w) [0..<n]) =
+ length (takefill False n (rev (to_bl w)))\<close>
+ by simp
+ fix m
+ assume \<open>m < length (map (bit w) [0..<n])\<close>
+ then have \<open>m < n\<close>
+ by simp
+ then have \<open>bit w m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
+ by (auto simp add: nth_takefill not_less rev_nth to_bl_nth word_size test_bit_word_eq dest: bit_imp_le_length)
+ with \<open>m < n \<close>show \<open>map (bit w) [0..<n] ! m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
+ by simp
+qed
+
+lemma to_bl_unfold:
+ \<open>to_bl w = rev (map (bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close>
+ by (simp add: map_bit_interval_eq takefill_bintrunc to_bl_def flip: bin_to_bl_def)
+
+lemma nth_rev_to_bl:
+ \<open>rev (to_bl w) ! n \<longleftrightarrow> bit w n\<close>
+ if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
+ using that by (simp add: to_bl_unfold)
+
+lemma nth_to_bl:
+ \<open>to_bl w ! n \<longleftrightarrow> bit w (LENGTH('a) - Suc n)\<close>
+ if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
+ using that by (simp add: to_bl_unfold rev_nth)
+
+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)
+ apply transfer
+ apply simp
+ done
+
+lemma [code]:
+ \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a::len)])\<close>
+ for w :: \<open>'a::len word\<close>
+ by (simp add: to_bl_unfold rev_map)
+
+lemma word_reverse_eq_of_bl_rev_to_bl:
+ \<open>word_reverse w = of_bl (rev (to_bl w))\<close>
+ by (rule bit_word_eqI)
+ (auto simp add: bit_word_reverse_iff bit_of_bl_iff nth_to_bl)
+
+lemmas word_reverse_no_def [simp] =
+ word_reverse_eq_of_bl_rev_to_bl [of "numeral w"] for w
+
+lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
+ by (rule nth_equalityI) (simp_all add: nth_rev_to_bl word_reverse_def word_rep_drop flip: of_bl_eq)
+
+lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True"
+ apply (rule word_bl.Abs_inverse')
+ apply simp
+ apply (rule word_eqI)
+ apply (clarsimp simp add: word_size)
+ apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
+ done
+
+lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
+ by (simp add: zip_rev bl_word_or rev_map)
+
+lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))"
+ by (simp add: zip_rev bl_word_and rev_map)
+
+lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))"
+ by (simp add: zip_rev bl_word_xor rev_map)
+
+lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
+ by (simp add: bl_word_not rev_map)
+
+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_eq)
+
+lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
+ 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)
+
+lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
+ for w :: "'a::len word"
+proof -
+ have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
+ by simp
+ also have "\<dots> = of_bl (to_bl w @ [False])"
+ by (rule shiftl1_of_bl)
+ finally show ?thesis .
+qed
+
+lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
+ for w :: "'a::len word"
+ by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
+
+\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>
+lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
+ by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
+
+lemma shiftr1_bl:
+ \<open>shiftr1 w = of_bl (butlast (to_bl w))\<close>
+proof (rule bit_word_eqI)
+ fix n
+ assume \<open>n < LENGTH('a)\<close>
+ show \<open>bit (shiftr1 w) n \<longleftrightarrow> bit (of_bl (butlast (to_bl w)) :: 'a word) n\<close>
+ proof (cases \<open>n = LENGTH('a) - 1\<close>)
+ case True
+ then show ?thesis
+ by (simp add: bit_shiftr1_iff bit_of_bl_iff)
+ next
+ case False
+ with \<open>n < LENGTH('a)\<close>
+ have \<open>n < LENGTH('a) - 1\<close>
+ by simp
+ with \<open>n < LENGTH('a)\<close> show ?thesis
+ by (simp add: bit_shiftr1_iff bit_of_bl_iff rev_nth nth_butlast
+ word_size test_bit_word_eq to_bl_nth)
+ qed
+qed
+
+lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
+ for w :: "'a::len word"
+ by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
+
+\<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close>
+lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
+ apply (rule word_bl.Abs_inverse')
+ apply (simp del: butlast.simps)
+ apply (simp add: shiftr1_bl of_bl_def)
+ done
+
+lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
+ for w :: "'a::len word"
+proof (rule nth_equalityI)
+ fix n
+ assume \<open>n < length (to_bl (sshiftr1 w))\<close>
+ then have \<open>n < LENGTH('a)\<close>
+ by simp
+ then show \<open>to_bl (sshiftr1 w) ! n \<longleftrightarrow> (hd (to_bl w) # butlast (to_bl w)) ! n\<close>
+ apply (cases n)
+ apply (simp_all add: to_bl_nth word_size hd_conv_nth test_bit_eq_bit bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl)
+ done
+qed simp
+
+lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
+ for w :: "'a::len word"
+ apply (unfold shiftr_def)
+ apply (induct n)
+ prefer 2
+ apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
+ apply (rule butlast_take [THEN trans])
+ apply (auto simp: word_size)
+ done
+
+lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
+ for w :: "'a::len word"
+ apply (unfold sshiftr_eq)
+ apply (induct n)
+ prefer 2
+ apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
+ apply (rule butlast_take [THEN trans])
+ apply (auto simp: word_size)
+ done
+
+lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
+ apply (unfold shiftr_def)
+ apply (induct n)
+ prefer 2
+ apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
+ apply (rule take_butlast [THEN trans])
+ apply (auto simp: word_size)
+ done
+
+lemma take_sshiftr' [rule_format] :
+ "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
+ take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
+ for w :: "'a::len word"
+ apply (unfold sshiftr_eq)
+ apply (induct n)
+ prefer 2
+ apply (simp add: bl_sshiftr1)
+ apply (rule impI)
+ apply (rule take_butlast [THEN trans])
+ apply (auto simp: word_size)
+ done
+
+lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
+lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
+
+lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
+ by (auto intro: append_take_drop_id [symmetric])
+
+lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
+lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
+
+lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
+ by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
+
+lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
+ for w :: "'a::len word"
+proof -
+ have "w << n = of_bl (to_bl w) << n"
+ by simp
+ also have "\<dots> = of_bl (to_bl w @ replicate n False)"
+ by (rule shiftl_of_bl)
+ finally show ?thesis .
+qed
+
+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)
+
+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)
+
+lemma shiftr_bl_of:
+ "length bl \<le> LENGTH('a) \<Longrightarrow>
+ (of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)"
+ apply (unfold shiftr_def)
+ apply (induct n)
+ apply clarsimp
+ apply clarsimp
+ apply (subst shiftr1_bl_of)
+ apply simp
+ apply (simp add: butlast_take)
+ done
+
+lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))"
+ for x :: "'a::len word"
+ using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
+
+lemma aligned_bl_add_size [OF refl]:
+ "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
+ take m (to_bl y) = replicate m False \<Longrightarrow>
+ to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)" for x :: \<open>'a::len word\<close>
+ apply (subgoal_tac "x AND y = 0")
+ prefer 2
+ apply (rule word_bl.Rep_eqD)
+ apply (simp add: bl_word_and)
+ apply (rule align_lem_and [THEN trans])
+ apply (simp_all add: word_size)[5]
+ apply simp
+ apply (subst word_plus_and_or [symmetric])
+ apply (simp add : bl_word_or)
+ apply (rule align_lem_or)
+ apply (simp_all add: word_size)
+ done
+
+lemma mask_bl: "mask n = of_bl (replicate n True)"
+ by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
+
+lemma bl_and_mask':
+ "to_bl (w AND mask n :: 'a::len word) =
+ replicate (LENGTH('a) - n) False @
+ drop (LENGTH('a) - n) (to_bl w)"
+ apply (rule nth_equalityI)
+ 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 rev_nth)
+ done
+
+lemma slice1_eq_of_bl:
+ \<open>(slice1 n w :: 'b::len word) = of_bl (takefill False n (to_bl w))\<close>
+ for w :: \<open>'a::len word\<close>
+proof (rule bit_word_eqI)
+ fix m
+ assume \<open>m < LENGTH('b)\<close>
+ show \<open>bit (slice1 n w :: 'b::len word) m \<longleftrightarrow> bit (of_bl (takefill False n (to_bl w)) :: 'b word) m\<close>
+ by (cases \<open>m \<ge> n\<close>; cases \<open>LENGTH('a) \<ge> n\<close>)
+ (auto simp add: bit_slice1_iff bit_of_bl_iff not_less rev_nth not_le nth_takefill nth_to_bl algebra_simps)
+qed
+
+lemma slice1_no_bin [simp]:
+ "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len)) (numeral w)))"
+ by (simp add: slice1_eq_of_bl) (* TODO: neg_numeral *)
+
+lemma slice_no_bin [simp]:
+ "slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len) - n)
+ (bin_to_bl (LENGTH('b::len)) (numeral w)))"
+ by (simp add: slice_def) (* TODO: neg_numeral *)
+
+lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
+ by (simp add: slice_def word_size slice1_eq_of_bl takefill_alt)
+
+lemmas slice_take = slice_take' [unfolded word_size]
+
+\<comment> \<open>shiftr to a word of the same size is just slice,
+ slice is just shiftr then ucast\<close>
+lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
+
+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)
+
+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
+ done
+
+lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
+lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
+lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
+lemmas slice1_up_alts =
+ le_add_diff_inverse [symmetric, THEN su1]
+ le_add_diff_inverse2 [symmetric, THEN su1]
+
+lemma slice1_tf_tf':
+ "to_bl (slice1 n w :: 'a::len word) =
+ rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))"
+ unfolding slice1_eq_of_bl by (rule word_rev_tf)
+
+lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
+
+lemma revcast_eq_of_bl:
+ \<open>(revcast w :: 'b::len word) = of_bl (takefill False (LENGTH('b)) (to_bl w))\<close>
+ for w :: \<open>'a::len word\<close>
+ by (simp add: revcast_def slice1_eq_of_bl)
+
+lemmas revcast_no_def [simp] = revcast_eq_of_bl [where w="numeral w", unfolded word_size] for w
+
+lemma to_bl_revcast:
+ "to_bl (revcast w :: 'a::len word) = takefill False (LENGTH('a)) (to_bl w)"
+ apply (rule nth_equalityI)
+ apply simp
+ apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>)
+ apply (auto simp add: nth_to_bl nth_takefill bit_revcast_iff)
+ done
+
+lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_word_cat_iff bit_of_bl_iff nth_append not_less nth_rev_to_bl)
+ apply (meson bit_word.rep_eq less_diff_conv2 nth_rev_to_bl)
+ done
+
+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)
+ done
+
+lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
+ by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
+
+lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
+ by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
+
+lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
+ by (cases x) simp_all
+
+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)
+ done
+
+lemma word_split_bl: "std = size c - size b \<Longrightarrow>
+ (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
+ word_split c = (a, b)"
+ apply (rule iffI)
+ defer
+ apply (erule (1) word_split_bl')
+ apply (case_tac "word_split c")
+ apply (auto simp add: word_size)
+ apply (frule word_split_bl' [rotated])
+ apply (auto simp add: word_size)
+ done
+
+lemma word_split_bl_eq:
+ "(word_split c :: ('c::len word \<times> 'd::len word)) =
+ (of_bl (take (LENGTH('a::len) - LENGTH('d::len)) (to_bl c)),
+ of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))"
+ for c :: "'a::len word"
+ apply (rule word_split_bl [THEN iffD1])
+ apply (unfold word_size)
+ 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 size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
+ by (induct wl) (auto simp: word_size)
+
+lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
+
+lemma nth_rcat_lem:
+ "n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow>
+ rev (concat (map to_bl wl)) ! n =
+ rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))"
+ apply (induct wl)
+ apply clarsimp
+ apply (clarsimp simp add : nth_append size_rcat_lem)
+ 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 foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0"
+ for x :: "'a::comm_monoid_add"
+ by (induct xs arbitrary: x) (auto simp: add.assoc)
+
+lemmas word_cat_bl_no_bin [simp] =
+ word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
+ for a b (* FIXME: negative numerals, 0 and 1 *)
+
+lemmas word_split_bl_no_bin [simp] =
+ word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
+
+lemmas word_rot_defs = word_roti_eq_word_rotr_word_rotl word_rotr_eq word_rotl_eq
+
+lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
+ by (simp add: word_rotl_eq to_bl_use_of_bl)
+
+lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
+
+lemmas word_rotl_eqs =
+ blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
+
+lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
+ by (simp add: word_rotr_eq to_bl_use_of_bl)
+
+lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
+
+lemmas word_rotr_eqs =
+ brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
+
+declare word_rotr_eqs (1) [simp]
+declare word_rotl_eqs (1) [simp]
+
+lemmas abl_cong = arg_cong [where f = "of_bl"]
+
+locale word_rotate
+begin
+
+lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
+
+lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
+
+lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
+
+lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
+
+lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
+
+lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
+
+end
+
+lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
+ simplified word_bl_Rep']
+
+lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
+ simplified word_bl_Rep']
+
+lemma bl_word_roti_dt':
+ "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow>
+ to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
+ apply (unfold word_roti_eq_word_rotr_word_rotl)
+ apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
+ apply safe
+ apply (simp add: zmod_zminus1_eq_if)
+ apply safe
+ apply (simp add: nat_mult_distrib)
+ apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
+ [THEN conjunct2, THEN order_less_imp_le]]
+ nat_mod_distrib)
+ apply (simp add: nat_mod_distrib)
+ done
+
+lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
+
+lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
+lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
+lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
+
+lemmas word_rotr_dt_no_bin' [simp] =
+ word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
+ (* FIXME: negative numerals, 0 and 1 *)
+
+lemmas word_rotl_dt_no_bin' [simp] =
+ word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
+ (* FIXME: negative numerals, 0 and 1 *)
+
+lemma max_word_bl: "to_bl (max_word::'a::len word) = replicate LENGTH('a) True"
+ by (fact to_bl_n1)
+
+lemma to_bl_mask:
+ "to_bl (mask n :: 'a::len word) =
+ replicate (LENGTH('a) - n) False @
+ replicate (min (LENGTH('a)) n) True"
+ by (simp add: mask_bl word_rep_drop min_def)
+
+lemma map_replicate_True:
+ "n = length xs \<Longrightarrow>
+ map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
+ by (induct xs arbitrary: n) auto
+
+lemma map_replicate_False:
+ "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
+ (zip xs (replicate n False)) = replicate n False"
+ by (induct xs arbitrary: n) auto
+
+lemma bl_and_mask:
+ fixes w :: "'a::len word"
+ and n :: nat
+ defines "n' \<equiv> LENGTH('a) - n"
+ shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
+proof -
+ note [simp] = map_replicate_True map_replicate_False
+ have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))"
+ by (simp add: bl_word_and)
+ also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
+ by simp
+ also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) =
+ replicate n' False @ drop n' (to_bl w)"
+ unfolding to_bl_mask n'_def by (subst zip_append) auto
+ finally show ?thesis .
+qed
+
+lemma drop_rev_takefill:
+ "length xs \<le> n \<Longrightarrow>
+ drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
+ by (simp add: takefill_alt rev_take)
+
+declare bin_to_bl_def [simp]
+
+end
--- a/src/HOL/Word/Word.thy Wed Aug 05 17:19:35 2020 +0200
+++ b/src/HOL/Word/Word.thy Wed Aug 05 19:06:39 2020 +0200
@@ -11,7 +11,6 @@
"HOL-Library.Bit_Operations"
Bits_Int
Bit_Comprehension
- Bit_Lists
Misc_Typedef
begin
@@ -147,18 +146,6 @@
for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq)
-lift_definition of_bl :: \<open>bool list \<Rightarrow> 'a::len word\<close>
- is bl_to_bin .
-
-lift_definition to_bl :: \<open>'a::len word \<Rightarrow> bool list\<close>
- is \<open>bin_to_bl LENGTH('a)\<close>
- by (simp add: bl_to_bin_inj)
-
-lemma to_bl_eq:
- \<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close>
- for w :: \<open>'a::len word\<close>
- by transfer simp
-
lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close>
is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp
@@ -902,7 +889,7 @@
end
lemma bit_word_eqI:
- \<open>a = b\<close> if \<open>\<And>n. n \<le> LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
+ \<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)
@@ -1054,19 +1041,13 @@
\<open>test_bit = (bit :: 'a word \<Rightarrow> _)\<close>
by transfer simp
-lemma [code]:
- \<open>bit w n \<longleftrightarrow> w AND push_bit n 1 \<noteq> 0\<close>
- for w :: \<open>'a::len word\<close>
- apply (simp add: bit_eq_iff)
- apply (auto simp add: bit_and_iff bit_push_bit_iff bit_1_iff exp_eq_0_imp_not_bit)
- done
+lemma bit_word_iff_drop_bit_and [code]:
+ \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
+ by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
lemma [code]:
- \<open>test_bit w n \<longleftrightarrow> w AND push_bit n 1 \<noteq> 0\<close>
- for w :: \<open>'a::len word\<close>
- apply (simp add: test_bit_word_eq bit_eq_iff)
- apply (auto simp add: bit_and_iff bit_push_bit_iff bit_1_iff exp_eq_0_imp_not_bit)
- done
+ \<open>test_bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
+ by (simp add: test_bit_word_eq bit_word_iff_drop_bit_and)
lift_definition shiftl_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
is \<open>\<lambda>k n. push_bit n k\<close>
@@ -1228,10 +1209,6 @@
\<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def)
-lemma bit_word_iff_drop_bit_and [code]:
- \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
- by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
-
lemma map_bit_range_eq_if_take_bit_eq:
\<open>map (bit k) [0..<n] = map (bit l) [0..<n]\<close>
if \<open>take_bit n k = take_bit n l\<close> for k l :: int
@@ -1253,26 +1230,6 @@
by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp
qed
-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)
-
-lemma rev_to_bl_eq:
- \<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close>
- for w :: \<open>'a::len word\<close>
- apply (rule nth_equalityI)
- apply (simp add: to_bl.rep_eq)
- apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq)
- done
-
-lemma of_bl_rev_eq:
- \<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close>
- apply (rule bit_word_eqI)
- apply (simp add: bit_of_bl_iff)
- apply transfer
- apply (simp add: bit_horner_sum_bit_iff ac_simps)
- done
-
subsection \<open>More shift operations\<close>
@@ -1292,16 +1249,6 @@
\<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close>
by transfer simp
-lemma bshiftr1_eq:
- \<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close>
- apply transfer
- apply auto
- apply (subst bl_to_bin_app_cat [of \<open>[True]\<close>, simplified])
- apply simp
- apply (metis One_nat_def add.commute bin_bl_bin bin_last_bl_to_bin bin_rest_bl_to_bin butlast_bin_rest concat_bit_eq last.simps list.distinct(1) list.size(3) list.size(4) odd_iff_mod_2_eq_one plus_1_eq_Suc power_Suc0_right push_bit_of_1 size_bin_to_bl take_bit_eq_mod trunc_bl2bin_len)
- apply (simp add: butlast_rest_bl2bin)
- done
-
lemma sshiftr_eq:
\<open>w >>> n = (sshiftr1 ^^ n) w\<close>
proof -
@@ -1339,11 +1286,6 @@
subsection \<open>Rotation\<close>
-lemma length_to_bl_eq:
- \<open>length (to_bl w) = LENGTH('a)\<close>
- for w :: \<open>'a::len word\<close>
- by transfer simp
-
lift_definition word_rotr :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close>
is \<open>\<lambda>n k. concat_bit (LENGTH('a) - n mod LENGTH('a))
(drop_bit (n mod LENGTH('a)) (take_bit LENGTH('a) k))
@@ -1483,30 +1425,6 @@
using mod_less_divisor not_less apply blast
done
-lemma word_rotr_eq:
- \<open>word_rotr n w = of_bl (rotater n (to_bl w))\<close>
- apply (rule bit_word_eqI)
- subgoal for n
- apply (cases \<open>n < LENGTH('a)\<close>)
- apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff rotater_rev length_to_bl_eq nth_rotate rev_to_bl_eq ac_simps)
- done
- done
-
-lemma word_rotl_eq:
- \<open>word_rotl n w = of_bl (rotate n (to_bl w))\<close>
-proof -
- have \<open>rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))\<close>
- by (simp add: rotater_rev')
- then show ?thesis
- apply (simp add: word_rotl_eq_word_rotr bit_of_bl_iff length_to_bl_eq rev_to_bl_eq)
- apply (rule bit_word_eqI)
- subgoal for n
- apply (cases \<open>n < LENGTH('a)\<close>)
- apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff nth_rotater)
- done
- done
-qed
-
subsection \<open>Split and cat operations\<close>
@@ -1534,8 +1452,16 @@
(case bin_split (LENGTH('c)) (uint a) of
(u, v) \<Rightarrow> (word_of_int u, word_of_int v))"
-definition word_rcat :: "'a::len word list \<Rightarrow> 'b::len word"
- where "word_rcat ws = word_of_int (bin_rcat (LENGTH('a)) (map uint ws))"
+definition word_rcat :: \<open>'a::len word list \<Rightarrow> 'b::len word\<close>
+ where \<open>word_rcat = word_of_int \<circ> horner_sum uint (2 ^ LENGTH('a)) \<circ> rev\<close>
+
+lemma word_rcat_eq:
+ \<open>word_rcat ws = word_of_int (bin_rcat (LENGTH('a::len)) (map uint ws))\<close>
+ for ws :: \<open>'a::len word list\<close>
+ apply (simp add: word_rcat_def bin_rcat_def rev_map)
+ apply transfer
+ apply (simp add: horner_sum_foldr foldr_map comp_def)
+ done
definition word_rsplit :: "'a::len word \<Rightarrow> 'b::len word list"
where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))"
@@ -1613,9 +1539,6 @@
lemmas td_sint = word_sint.td
-lemma to_bl_def': "(to_bl :: 'a::len word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint"
- by transfer (simp add: fun_eq_iff)
-
lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
by (fact uints_def [unfolded no_bintr_alt1])
@@ -1841,92 +1764,6 @@
apply (auto simp add: nth_sbintr)
done
-\<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>
-lemma td_bl:
- "type_definition
- (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
- done
-
-interpretation word_bl:
- type_definition
- "to_bl :: 'a::len word \<Rightarrow> bool list"
- of_bl
- "{bl. length bl = LENGTH('a::len)}"
- by (fact td_bl)
-
-lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
-
-lemma word_size_bl: "size w = size (to_bl w)"
- by (auto simp: word_size)
-
-lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)"
- by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
-
-lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
- for x :: "'a::len word"
- unfolding word_bl_Rep' by (rule len_gt_0)
-
-lemma bl_not_Nil [iff]: "to_bl x \<noteq> []"
- for x :: "'a::len word"
- by (fact length_bl_gt_0 [unfolded length_greater_0_conv])
-
-lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
- for x :: "'a::len word"
- by (fact length_bl_gt_0 [THEN gr_implies_not0])
-
-lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
- apply transfer
- apply (auto simp add: bin_sign_def)
- using bin_sign_lem bl_sbin_sign apply fastforce
- using bin_sign_lem bl_sbin_sign apply force
- done
-
-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])
-
-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)
-
-lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))"
- by (simp add: of_bl_def)
-
-lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
- by transfer simp
-
-lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
- by (simp add: uint_bl word_size)
-
-lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len word) = bin_to_bl (LENGTH('a)) bin"
- by (auto simp: uint_bl word_ubin.eq_norm word_size)
-
-lemma to_bl_numeral [simp]:
- "to_bl (numeral bin::'a::len word) =
- bin_to_bl (LENGTH('a)) (numeral bin)"
- unfolding word_numeral_alt by (rule to_bl_of_bin)
-
-lemma to_bl_neg_numeral [simp]:
- "to_bl (- numeral bin::'a::len word) =
- bin_to_bl (LENGTH('a)) (- numeral bin)"
- unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
-
-lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
- by (simp add: uint_bl word_size)
-
-lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x"
- for x :: "'a::len word"
- by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
-
lemmas bintr_num =
word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
lemmas sbintr_num =
@@ -1967,9 +1804,6 @@
lemma scast_id [simp]: "scast w = w"
by transfer simp
-lemma ucast_bl: "ucast w = of_bl (to_bl w)"
- by transfer simp
-
lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))"
by transfer (simp add: bit_take_bit_iff ac_simps)
@@ -2085,26 +1919,8 @@
\<open>UCAST (numeral bin) = numeral bin\<close> if \<open>is_down UCAST\<close>
using that by transfer simp
-lemma ucast_down_bl:
- "UCAST (of_bl bl) = of_bl bl" if \<open>is_down UCAST\<close>
- using that by transfer simp
-
end
-lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
- by transfer (simp add: bl_to_bin_app_cat)
-
-lemma ucast_of_bl_up:
- \<open>ucast (of_bl bl :: 'a::len word) = of_bl bl\<close>
- if \<open>size bl \<le> size (of_bl bl :: 'a::len word)\<close>
- using that
- apply transfer
- apply (rule bit_eqI)
- apply (auto simp add: bit_take_bit_iff)
- apply (subst (asm) trunc_bl2bin_len [symmetric])
- apply (auto simp only: bit_take_bit_iff)
- done
-
lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
@@ -2133,50 +1949,6 @@
apply (metis div_exp_eq mod_div_trivial mult.commute nonzero_mult_div_cancel_left power_Suc0_right power_add zero_neq_numeral)
done
-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)
-
-lemma word_rep_drop:
- "to_bl (of_bl bl::'a::len word) =
- replicate (LENGTH('a) - length bl) False @
- drop (length bl - LENGTH('a)) bl"
- by (simp add: word_rev_tf takefill_alt rev_take)
-
-lemma to_bl_ucast:
- "to_bl (ucast (w::'b::len word) ::'a::len word) =
- replicate (LENGTH('a) - LENGTH('b)) False @
- drop (LENGTH('b) - LENGTH('a)) (to_bl w)"
- apply (unfold ucast_bl)
- apply (rule trans)
- apply (rule word_rep_drop)
- apply simp
- done
-
-lemma ucast_up_app:
- \<open>to_bl (ucast w :: 'b::len word) = replicate n False @ (to_bl w)\<close>
- if \<open>source_size (ucast :: 'a word \<Rightarrow> 'b word) + n = target_size (ucast :: 'a word \<Rightarrow> 'b word)\<close>
- for w :: \<open>'a::len word\<close>
- using that
- by (auto simp add : source_size target_size to_bl_ucast)
-
-lemma ucast_down_drop [OF refl]:
- "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
- to_bl (uc w) = drop n (to_bl w)"
- by (auto simp add : source_size target_size to_bl_ucast)
-
-lemma scast_down_drop [OF refl]:
- "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
- to_bl (sc w) = drop n (to_bl w)"
- apply (subgoal_tac "sc = ucast")
- apply safe
- apply simp
- apply (erule ucast_down_drop)
- apply (rule down_cast_same [symmetric])
- apply (simp add : source_size target_size is_down)
- done
-
subsection \<open>Word Arithmetic\<close>
@@ -2202,18 +1974,6 @@
lemma word_m1_wi: "- 1 = word_of_int (- 1)"
by (simp add: word_neg_numeral_alt [of Num.One])
-lemma word_0_bl [simp]: "of_bl [] = 0"
- by (simp add: of_bl_def)
-
-lemma word_1_bl: "of_bl [True] = 1"
- by (simp add: of_bl_def 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)
-
-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)
-
lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
by (simp add: word_uint_eq_iff)
@@ -2250,8 +2010,8 @@
lemma scast_n1 [simp]: "scast (- 1) = - 1"
by transfer simp
-lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
- by transfer simp
+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
@@ -2751,38 +2511,6 @@
apply (simp add: mult_less_0_iff)
done
-\<comment> \<open>links with \<open>rbl\<close> operations\<close>
-lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
- by transfer (simp add: rbl_succ)
-
-lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
- by transfer (simp add: rbl_pred)
-
-lemma word_add_rbl:
- "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
- to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))"
- apply transfer
- apply (drule sym)
- apply (drule sym)
- apply (simp add: rbl_add)
- done
-
-lemma word_mult_rbl:
- "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
- to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))"
- apply transfer
- apply (drule sym)
- apply (drule sym)
- apply (simp add: rbl_mult)
- done
-
-lemma rtb_rbl_ariths:
- "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
- "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
- "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
- "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
- by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl)
-
subsection \<open>Arithmetic type class instantiations\<close>
@@ -3139,21 +2867,6 @@
lemma word_arith_power_alt: "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)"
by (simp add : word_of_int_power_hom [symmetric])
-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
-
lemma unatSuc: "1 + n \<noteq> 0 \<Longrightarrow> unat (1 + n) = Suc (unat n)"
for n :: "'a::len word"
by unat_arith
@@ -3192,9 +2905,6 @@
subsection \<open>Bitwise Operations on Words\<close>
-lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
- by simp
-
lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
\<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close>
@@ -3426,87 +3136,11 @@
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)"
- by transfer (simp add: bl_not_bin)
-
-lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)"
- by transfer (simp flip: bl_xor_bin)
-
-lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)"
- by transfer (simp flip: bl_or_bin)
-
-lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)"
- by transfer (simp flip: bl_and_bin)
-
-lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
- apply (unfold word_size)
- apply (safe elim!: bin_nth_uint_imp)
- apply (frule bin_nth_uint_imp)
- apply (fast dest!: bin_nth_bl)+
- done
-
-lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
-
-lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
- by transfer (auto simp add: bin_nth_bl)
-
-lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
- 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>
-proof (rule nth_equalityI)
- show \<open>length (map (bit w) [0..<n]) =
- length (takefill False n (rev (to_bl w)))\<close>
- by simp
- fix m
- assume \<open>m < length (map (bit w) [0..<n])\<close>
- then have \<open>m < n\<close>
- by simp
- then have \<open>bit w m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
- by (auto simp add: nth_takefill not_less rev_nth to_bl_nth word_size test_bit_word_eq dest: bit_imp_le_length)
- with \<open>m < n \<close>show \<open>map (bit w) [0..<n] ! m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
- by simp
-qed
-
-lemma to_bl_unfold:
- \<open>to_bl w = rev (map (bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close>
- by (simp add: map_bit_interval_eq takefill_bintrunc to_bl_def flip: bin_to_bl_def)
-
-lemma nth_rev_to_bl:
- \<open>rev (to_bl w) ! n \<longleftrightarrow> bit w n\<close>
- if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
- using that by (simp add: to_bl_unfold)
-
-lemma nth_to_bl:
- \<open>to_bl w ! n \<longleftrightarrow> bit w (LENGTH('a) - Suc n)\<close>
- if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
- using that by (simp add: to_bl_unfold rev_nth)
-
-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 bit_horner_sum_bit_word_iff:
\<open>bit (horner_sum of_bool (2 :: 'a::len word) bs) n
\<longleftrightarrow> n < min LENGTH('a) (length bs) \<and> bs ! n\<close>
by transfer (simp add: bit_horner_sum_bit_iff)
-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)
- apply transfer
- apply simp
- done
-
-lemma [code]:
- \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a::len)])\<close>
- for w :: \<open>'a::len word\<close>
- by (simp add: to_bl_unfold rev_map)
-
definition word_reverse :: \<open>'a::len word \<Rightarrow> 'a word\<close>
where \<open>word_reverse w = horner_sum of_bool 2 (rev (map (bit w) [0..<LENGTH('a)]))\<close>
@@ -3516,17 +3150,6 @@
by (cases \<open>n < LENGTH('a)\<close>)
(simp_all add: word_reverse_def bit_horner_sum_bit_word_iff rev_nth)
-lemma word_reverse_eq_of_bl_rev_to_bl:
- \<open>word_reverse w = of_bl (rev (to_bl w))\<close>
- by (rule bit_word_eqI)
- (auto simp add: bit_word_reverse_iff bit_of_bl_iff nth_to_bl)
-
-lemmas word_reverse_no_def [simp] =
- word_reverse_eq_of_bl_rev_to_bl [of "numeral w"] for w
-
-lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
- by (rule nth_equalityI) (simp_all add: nth_rev_to_bl word_reverse_def word_rep_drop flip: of_bl_eq)
-
lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
by (rule bit_word_eqI)
(auto simp add: bit_word_reverse_iff bit_imp_le_length Suc_diff_Suc)
@@ -3553,14 +3176,6 @@
"clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
by transfer (simp add: bin_sc_eq)
-lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True"
- apply (rule word_bl.Abs_inverse')
- apply simp
- apply (rule word_eqI)
- apply (clarsimp simp add: word_size)
- apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
- done
-
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)
@@ -3598,18 +3213,6 @@
apply (auto simp add: word_ao_nth nth_w2p word_size)
done
-lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
- by (simp add: zip_rev bl_word_or rev_map)
-
-lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))"
- by (simp add: zip_rev bl_word_and rev_map)
-
-lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))"
- by (simp add: zip_rev bl_word_xor rev_map)
-
-lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
- by (simp add: bl_word_not rev_map)
-
subsection \<open>Bit comprehension\<close>
@@ -3782,55 +3385,6 @@
subsubsection \<open>shift functions in terms of lists of bools\<close>
-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_eq)
-
-lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
- 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)
-
-lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
- for w :: "'a::len word"
-proof -
- have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
- by simp
- also have "\<dots> = of_bl (to_bl w @ [False])"
- by (rule shiftl1_of_bl)
- finally show ?thesis .
-qed
-
-lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
- for w :: "'a::len word"
- by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
-
-\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>
-lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
- by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
-
-lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
- apply (rule bit_word_eqI)
- apply (simp add: bit_shiftr1_iff bit_of_bl_iff)
- apply auto
- apply (metis bin_nth_of_bl bin_rest_bl_to_bin bit_Suc test_bit_bin test_bit_word_eq to_bl_to_bin)
- using bit_Suc nat_less_le not_bit_length apply blast
- apply (simp add: bit_imp_le_length less_diff_conv)
- apply (metis bin_nth_of_bl bin_rest_bl_to_bin bit_Suc butlast_bin_rest size_bin_to_bl test_bit_bin test_bit_word_eq to_bl_to_bin word_bl_Rep')
- done
-
-lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
- for w :: "'a::len word"
- by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
-
-\<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close>
-lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
- apply (rule word_bl.Abs_inverse')
- apply (simp del: butlast.simps)
- apply (simp add: shiftr1_bl of_bl_def)
- done
-
lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
apply (rule bit_word_eqI)
apply (auto simp add: bit_shiftl1_iff bit_word_reverse_iff bit_shiftr1_iff Suc_diff_Suc)
@@ -3848,95 +3402,14 @@
lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
by (simp add: shiftr_rev)
-lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
- for w :: "'a::len word"
-proof (rule nth_equalityI)
- fix n
- assume \<open>n < length (to_bl (sshiftr1 w))\<close>
- then have \<open>n < LENGTH('a)\<close>
- by simp
- then show \<open>to_bl (sshiftr1 w) ! n \<longleftrightarrow> (hd (to_bl w) # butlast (to_bl w)) ! n\<close>
- apply (cases n)
- apply (simp_all add: to_bl_nth word_size hd_conv_nth test_bit_eq_bit bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl)
- done
-qed simp
-
-lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
- for w :: "'a::len word"
- apply (unfold shiftr_def)
- apply (induct n)
- prefer 2
- apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
- apply (rule butlast_take [THEN trans])
- apply (auto simp: word_size)
- done
-
-lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
- for w :: "'a::len word"
- apply (unfold sshiftr_eq)
- apply (induct n)
- prefer 2
- apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
- apply (rule butlast_take [THEN trans])
- apply (auto simp: word_size)
- done
-
-lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
- apply (unfold shiftr_def)
- apply (induct n)
- prefer 2
- apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
- apply (rule take_butlast [THEN trans])
- apply (auto simp: word_size)
- done
-
-lemma take_sshiftr' [rule_format] :
- "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
- take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
- for w :: "'a::len word"
- apply (unfold sshiftr_eq)
- apply (induct n)
- prefer 2
- apply (simp add: bl_sshiftr1)
- apply (rule impI)
- apply (rule take_butlast [THEN trans])
- apply (auto simp: word_size)
- done
-
-lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
-lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
-
-lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
- by (auto intro: append_take_drop_id [symmetric])
-
-lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
-lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
-
-lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
- by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
-
-lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
- for w :: "'a::len word"
-proof -
- have "w << n = of_bl (to_bl w) << n"
- by simp
- also have "\<dots> = of_bl (to_bl w @ replicate n False)"
- by (rule shiftl_of_bl)
- finally show ?thesis .
-qed
-
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)
-
lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
for x :: "'a::len word"
- apply (unfold word_size)
- apply (rule word_eqI)
- apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
+ apply transfer
+ apply (simp add: take_bit_push_bit)
done
\<comment> \<open>note -- the following results use \<open>'a::len word < number_ring\<close>\<close>
@@ -3982,27 +3455,6 @@
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:
- "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)
-
-lemma shiftr_bl_of:
- "length bl \<le> LENGTH('a) \<Longrightarrow>
- (of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)"
- apply (unfold shiftr_def)
- apply (induct n)
- apply clarsimp
- apply clarsimp
- apply (subst shiftr1_bl_of)
- apply simp
- apply (simp add: butlast_take)
- done
-
-lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))"
- for x :: "'a::len word"
- using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
-
lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
apply (induct ys arbitrary: n)
apply simp_all
@@ -4040,23 +3492,6 @@
apply (auto simp: zip_replicate o_def map_replicate_const)
done
-lemma aligned_bl_add_size [OF refl]:
- "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
- take m (to_bl y) = replicate m False \<Longrightarrow>
- to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)" for x :: \<open>'a::len word\<close>
- apply (subgoal_tac "x AND y = 0")
- prefer 2
- apply (rule word_bl.Rep_eqD)
- apply (simp add: bl_word_and)
- apply (rule align_lem_and [THEN trans])
- apply (simp_all add: word_size)[5]
- apply simp
- apply (subst word_plus_and_or [symmetric])
- apply (simp add : bl_word_or)
- apply (rule align_lem_or)
- apply (simp_all add: word_size)
- done
-
subsubsection \<open>Mask\<close>
@@ -4085,9 +3520,6 @@
\<open>(mask n :: 'a::len word) !! i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close>
by (auto simp add: test_bit_word_eq word_size Word.bit_mask_iff)
-lemma mask_bl: "mask n = of_bl (replicate n True)"
- by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
-
lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
by (auto simp add: nth_bintr word_size intro: word_eqI)
@@ -4107,17 +3539,6 @@
lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
unfolding word_numeral_alt by (rule and_mask_wi)
-lemma bl_and_mask':
- "to_bl (w AND mask n :: 'a::len word) =
- replicate (LENGTH('a) - n) False @
- drop (LENGTH('a) - n) (to_bl w)"
- apply (rule nth_equalityI)
- 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 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)
@@ -4217,17 +3638,6 @@
by (auto simp add: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff exp_eq_zero_iff not_less not_le ac_simps
dest: bit_imp_le_length)
-lemma slice1_eq_of_bl:
- \<open>(slice1 n w :: 'b::len word) = of_bl (takefill False n (to_bl w))\<close>
- for w :: \<open>'a::len word\<close>
-proof (rule bit_word_eqI)
- fix m
- assume \<open>m \<le> LENGTH('b)\<close>
- show \<open>bit (slice1 n w :: 'b::len word) m \<longleftrightarrow> bit (of_bl (takefill False n (to_bl w)) :: 'b word) m\<close>
- by (cases \<open>m \<ge> n\<close>; cases \<open>LENGTH('a) \<ge> n\<close>)
- (auto simp add: bit_slice1_iff bit_of_bl_iff not_less rev_nth not_le nth_takefill nth_to_bl algebra_simps)
-qed
-
definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
where \<open>slice n = slice1 (LENGTH('a) - n)\<close>
@@ -4236,90 +3646,49 @@
for w :: \<open>'a::len word\<close>
by (simp add: slice_def word_size bit_slice1_iff)
-lemma slice1_no_bin [simp]:
- "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len)) (numeral w)))"
- by (simp add: slice1_eq_of_bl) (* TODO: neg_numeral *)
-
-lemma slice_no_bin [simp]:
- "slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len) - n)
- (bin_to_bl (LENGTH('b::len)) (numeral w)))"
- by (simp add: slice_def) (* TODO: neg_numeral *)
-
lemma slice1_0 [simp] : "slice1 n 0 = 0"
unfolding slice1_def by simp
lemma slice_0 [simp] : "slice n 0 = 0"
unfolding slice_def by auto
-lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
- by (simp add: slice_def word_size slice1_eq_of_bl takefill_alt)
-
-lemmas slice_take = slice_take' [unfolded word_size]
-
-\<comment> \<open>shiftr to a word of the same size is just slice,
- slice is just shiftr then ucast\<close>
-lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
-
lemma slice_shiftr: "slice n w = ucast (w >> n)"
- apply (unfold slice_take shiftr_bl)
- apply (rule ucast_of_bl_up [symmetric])
- apply (simp add: word_size)
+ apply (rule bit_word_eqI)
+ apply (cases \<open>n \<le> LENGTH('b)\<close>)
+ apply (auto simp add: bit_slice_iff bit_ucast_iff bit_shiftr_word_iff ac_simps
+ dest: bit_imp_le_length)
done
lemma nth_slice: "(slice n w :: 'a::len word) !! m = (w !! (m + n) \<and> m < LENGTH('a))"
by (simp add: slice_shiftr nth_ucast nth_shiftr)
-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)
-
-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
+lemma ucast_slice1: "ucast w = slice1 (size w) w"
+ apply (simp add: slice1_def)
+ apply transfer
+ apply simp
done
-lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
-lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
-lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
-lemmas slice1_up_alts =
- le_add_diff_inverse [symmetric, THEN su1]
- le_add_diff_inverse2 [symmetric, THEN su1]
-
-lemma ucast_slice1: "ucast w = slice1 (size w) w"
- by (simp add: slice1_def ucast_bl takefill_same' word_size)
-
lemma ucast_slice: "ucast w = slice 0 w"
by (simp add: slice_def slice1_def)
lemma slice_id: "slice 0 t = t"
by (simp only: ucast_slice [symmetric] ucast_id)
-lemma slice1_tf_tf':
- "to_bl (slice1 n w :: 'a::len word) =
- rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))"
- unfolding slice1_eq_of_bl by (rule word_rev_tf)
-
-lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
-
lemma rev_slice1:
- "n + k = LENGTH('a) + LENGTH('b) \<Longrightarrow>
- slice1 n (word_reverse w :: 'b::len word) =
- word_reverse (slice1 k w :: 'a::len word)"
- apply (unfold word_reverse_eq_of_bl_rev_to_bl slice1_tf_tf)
- apply (rule word_bl.Rep_inverse')
- apply (rule rev_swap [THEN iffD1])
- apply (rule trans [symmetric])
- apply (rule tf_rev)
- apply (simp add: word_bl.Abs_inverse)
- apply (simp add: word_bl.Abs_inverse)
- done
+ \<open>slice1 n (word_reverse w :: 'b::len word) = word_reverse (slice1 k w :: 'a::len word)\<close>
+ if \<open>n + k = LENGTH('a) + LENGTH('b)\<close>
+proof (rule bit_word_eqI)
+ fix m
+ assume *: \<open>m < LENGTH('a)\<close>
+ from that have **: \<open>LENGTH('b) = n + k - LENGTH('a)\<close>
+ by simp
+ show \<open>bit (slice1 n (word_reverse w :: 'b word) :: 'a word) m \<longleftrightarrow> bit (word_reverse (slice1 k w :: 'a word)) m\<close>
+ apply (simp add: bit_slice1_iff bit_word_reverse_iff)
+ using * **
+ apply (cases \<open>n \<le> LENGTH('a)\<close>; cases \<open>k \<le> LENGTH('a)\<close>)
+ apply auto
+ done
+qed
lemma rev_slice:
"n + k + LENGTH('a::len) = LENGTH('b::len) \<Longrightarrow>
@@ -4341,24 +3710,9 @@
for w :: \<open>'a::len word\<close>
by (simp add: revcast_def bit_slice1_iff)
-lemma revcast_eq_of_bl:
- \<open>(revcast w :: 'b::len word) = of_bl (takefill False (LENGTH('b)) (to_bl w))\<close>
- for w :: \<open>'a::len word\<close>
- by (simp add: revcast_def slice1_eq_of_bl)
-
lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
by (simp add: revcast_def word_size)
-lemmas revcast_no_def [simp] = revcast_eq_of_bl [where w="numeral w", unfolded word_size] for w
-
-lemma to_bl_revcast:
- "to_bl (revcast w :: 'a::len word) = takefill False (LENGTH('a)) (to_bl w)"
- apply (rule nth_equalityI)
- apply simp
- apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>)
- apply (auto simp add: nth_to_bl nth_takefill bit_revcast_iff)
- done
-
lemma revcast_rev_ucast [OF refl refl refl]:
"cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
rc = word_reverse uc"
@@ -4388,68 +3742,52 @@
lemma revcast_down_uu [OF refl]:
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
for w :: "'a::len word"
- apply (simp add: revcast_eq_of_bl)
- apply (rule word_bl.Rep_inverse')
- apply (rule trans, rule ucast_down_drop)
- prefer 2
- apply (rule trans, rule drop_shiftr)
- apply (auto simp: takefill_alt wsst_TYs)
+ apply (simp add: source_size_def target_size_def)
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_revcast_iff bit_ucast_iff bit_shiftr_word_iff ac_simps)
done
lemma revcast_down_us [OF refl]:
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
for w :: "'a::len word"
- apply (simp add: revcast_eq_of_bl)
- apply (rule word_bl.Rep_inverse')
- apply (rule trans, rule ucast_down_drop)
- prefer 2
- apply (rule trans, rule drop_sshiftr)
- apply (auto simp: takefill_alt wsst_TYs)
+ apply (simp add: source_size_def target_size_def)
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_revcast_iff bit_ucast_iff bit_sshiftr_word_iff ac_simps)
done
lemma revcast_down_su [OF refl]:
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
for w :: "'a::len word"
- apply (simp add: revcast_eq_of_bl)
- apply (rule word_bl.Rep_inverse')
- apply (rule trans, rule scast_down_drop)
- prefer 2
- apply (rule trans, rule drop_shiftr)
- apply (auto simp: takefill_alt wsst_TYs)
+ apply (simp add: source_size_def target_size_def)
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_revcast_iff bit_word_scast_iff bit_shiftr_word_iff ac_simps)
done
lemma revcast_down_ss [OF refl]:
"rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
for w :: "'a::len word"
- apply (simp add: revcast_eq_of_bl)
- apply (rule word_bl.Rep_inverse')
- apply (rule trans, rule scast_down_drop)
- prefer 2
- apply (rule trans, rule drop_sshiftr)
- apply (auto simp: takefill_alt wsst_TYs)
+ apply (simp add: source_size_def target_size_def)
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_revcast_iff bit_word_scast_iff bit_sshiftr_word_iff ac_simps)
done
lemma cast_down_rev [OF refl]:
"uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)"
for w :: "'a::len word"
- apply (unfold shiftl_rev)
- apply clarify
- apply (simp add: revcast_rev_ucast)
- apply (rule word_rev_gal')
- apply (rule trans [OF _ revcast_rev_ucast])
- apply (rule revcast_down_uu [symmetric])
- apply (auto simp add: wsst_TYs)
+ apply (simp add: source_size_def target_size_def)
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
done
lemma revcast_up [OF refl]:
"rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
rc w = (ucast w :: 'a::len word) << n"
- apply (simp add: revcast_eq_of_bl)
- apply (rule word_bl.Rep_inverse')
- apply (simp add: takefill_alt)
- apply (rule bl_shiftl [THEN trans])
- apply (subst ucast_up_app)
- apply (auto simp add: wsst_TYs)
+ apply (simp add: source_size_def target_size_def)
+ apply (rule bit_word_eqI)
+ apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
+ apply auto
+ apply (metis add.commute add_diff_cancel_right)
+ apply (metis diff_add_inverse2 diff_diff_add)
done
lemmas rc1 = revcast_up [THEN
@@ -4501,7 +3839,7 @@
subsection \<open>Split and cat\<close>
lemmas word_split_bin' = word_split_def
-lemmas word_cat_bin' = word_cat_def
+lemmas word_cat_bin' = word_cat_eq
lemma word_rsplit_no:
"(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) =
@@ -4519,24 +3857,6 @@
apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff)
done
-lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
- by (simp add: of_bl_def to_bl_def word_cat_bin' bl_to_bin_app_cat)
-
-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)
- done
-
-lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
- by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
-
-lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
- by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
-
-lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
- by (cases x) simp_all
-
lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
a = bintrunc (LENGTH('a) - n) a \<and> b = bintrunc (LENGTH('a)) b"
for w :: "'a::len word"
@@ -4547,51 +3867,6 @@
apply safe
done
-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)
- done
-
-lemma word_split_bl: "std = size c - size b \<Longrightarrow>
- (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
- word_split c = (a, b)"
- apply (rule iffI)
- defer
- apply (erule (1) word_split_bl')
- apply (case_tac "word_split c")
- apply (auto simp add: word_size)
- apply (frule word_split_bl' [rotated])
- apply (auto simp add: word_size)
- done
-
-lemma word_split_bl_eq:
- "(word_split c :: ('c::len word \<times> 'd::len word)) =
- (of_bl (take (LENGTH('a::len) - LENGTH('d::len)) (to_bl c)),
- of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))"
- for c :: "'a::len word"
- apply (rule word_split_bl [THEN iffD1])
- apply (unfold word_size)
- apply (rule refl conjI)+
- done
-
\<comment> \<open>keep quantifiers for use in simplification\<close>
lemma test_bit_split':
"word_split c = (a, b) \<longrightarrow>
@@ -4685,13 +3960,6 @@
apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
done
-lemmas word_cat_bl_no_bin [simp] =
- word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
- for a b (* FIXME: negative numerals, 0 and 1 *)
-
-lemmas word_split_bl_no_bin [simp] =
- word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
-
text \<open>
This odd result arises from the fact that the statement of the
result implies that the decoded words are of the same type,
@@ -4724,37 +3992,33 @@
apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
done
-lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
- by (auto simp: word_rcat_def to_bl_def' of_bl_def bin_rcat_bl)
-
-lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
- by (induct wl) (auto simp: word_size)
-
-lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
-
-lemma nth_rcat_lem:
- "n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow>
- rev (concat (map to_bl wl)) ! n =
- rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))"
- apply (induct wl)
- apply clarsimp
- apply (clarsimp simp add : nth_append size_rcat_lem)
- 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 horner_sum_uint_exp_Cons_eq:
+ \<open>horner_sum uint (2 ^ LENGTH('a)) (w # ws) =
+ concat_bit LENGTH('a) (uint w) (horner_sum uint (2 ^ LENGTH('a)) ws)\<close>
+ for ws :: \<open>'a::len word list\<close>
+ by (simp add: concat_bit_eq push_bit_eq_mult)
+
+lemma bit_horner_sum_uint_exp_iff:
+ \<open>bit (horner_sum uint (2 ^ LENGTH('a)) ws) n \<longleftrightarrow>
+ n div LENGTH('a) < length ws \<and> bit (ws ! (n div LENGTH('a))) (n mod LENGTH('a))\<close>
+ for ws :: \<open>'a::len word list\<close>
+proof (induction ws arbitrary: n)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons w ws)
+ then show ?case
+ by (cases \<open>n \<ge> LENGTH('a)\<close>)
+ (simp_all only: horner_sum_uint_exp_Cons_eq, simp_all add: bit_concat_bit_iff le_div_geq le_mod_geq bit_uint_iff Cons)
+qed
lemma test_bit_rcat:
"sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
(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)
- 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"
- for x :: "'a::comm_monoid_add"
- by (induct xs arbitrary: x) (auto simp: add.assoc)
+ by (simp add: word_size word_rcat_def bin_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff)
+ (simp add: test_bit_eq_bit)
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
@@ -4855,73 +4119,74 @@
subsection \<open>Rotation\<close>
-lemmas word_rot_defs = word_roti_eq_word_rotr_word_rotl word_rotr_eq word_rotl_eq
-
-lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
- by (simp add: word_rotl_eq to_bl_use_of_bl)
-
-lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
-
-lemmas word_rotl_eqs =
- blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
-
-lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
- by (simp add: word_rotr_eq to_bl_use_of_bl)
-
-lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
-
-lemmas word_rotr_eqs =
- brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
-
-declare word_rotr_eqs (1) [simp]
-declare word_rotl_eqs (1) [simp]
-
-lemma word_rot_rl [simp]: "word_rotl k (word_rotr k v) = v"
- and word_rot_lr [simp]: "word_rotr k (word_rotl k v) = v"
- by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
-
-lemma word_rot_gal: "word_rotr n v = w \<longleftrightarrow> word_rotl n w = v"
- and word_rot_gal': "w = word_rotr n v \<longleftrightarrow> v = word_rotl n w"
- by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] dest: sym)
-
-lemma word_rotr_rev: "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
- by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev to_bl_rotr to_bl_rotl rotater_rev)
+lemma word_rotr_word_rotr_eq:
+ \<open>word_rotr m (word_rotr n w) = word_rotr (m + n) w\<close>
+ by (rule bit_word_eqI) (simp add: bit_word_rotr_iff ac_simps mod_add_right_eq)
+
+lemma word_rot_rl [simp]:
+ \<open>word_rotl k (word_rotr k v) = v\<close>
+ apply (rule bit_word_eqI)
+ apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
+ apply (auto dest: bit_imp_le_length)
+ apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
+ apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' bit_imp_le_length div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
+ done
+
+lemma word_rot_lr [simp]:
+ \<open>word_rotr k (word_rotl k v) = v\<close>
+ apply (rule bit_word_eqI)
+ apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
+ apply (auto dest: bit_imp_le_length)
+ apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
+ apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' bit_imp_le_length div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
+ done
+
+lemma word_rot_gal:
+ \<open>word_rotr n v = w \<longleftrightarrow> word_rotl n w = v\<close>
+ by auto
+
+lemma word_rot_gal':
+ \<open>w = word_rotr n v \<longleftrightarrow> v = word_rotl n w\<close>
+ by auto
+
+lemma word_rotr_rev:
+ \<open>word_rotr n w = word_reverse (word_rotl n (word_reverse w))\<close>
+proof (rule bit_word_eqI)
+ fix m
+ assume \<open>m < LENGTH('a)\<close>
+ moreover have \<open>1 +
+ ((int m + int n mod int LENGTH('a)) mod int LENGTH('a) +
+ ((int LENGTH('a) * 2) mod int LENGTH('a) - (1 + (int m + int n mod int LENGTH('a)))) mod int LENGTH('a)) =
+ int LENGTH('a)\<close>
+ apply (cases \<open>(1 + (int m + int n mod int LENGTH('a))) mod
+ int LENGTH('a) = 0\<close>)
+ using zmod_zminus1_eq_if [of \<open>1 + (int m + int n mod int LENGTH('a))\<close> \<open>int LENGTH('a)\<close>]
+ apply simp_all
+ apply (auto simp add: algebra_simps)
+ apply (simp add: minus_equation_iff [of \<open>int m\<close>])
+ apply (drule sym [of _ \<open>int m\<close>])
+ apply simp
+ apply (metis add.commute add_minus_cancel diff_minus_eq_add len_gt_0 less_imp_of_nat_less less_nat_zero_code mod_mult_self3 of_nat_gt_0 zmod_minus1)
+ apply (metis (no_types, hide_lams) Abs_fnat_hom_add less_not_refl mod_Suc of_nat_Suc of_nat_gt_0 of_nat_mod)
+ done
+ then have \<open>int ((m + n) mod LENGTH('a)) =
+ int (LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a)))\<close>
+ using \<open>m < LENGTH('a)\<close>
+ by (simp only: of_nat_mod mod_simps)
+ (simp add: of_nat_diff of_nat_mod Suc_le_eq add_less_mono algebra_simps mod_simps)
+ then have \<open>(m + n) mod LENGTH('a) =
+ LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a))\<close>
+ by simp
+ ultimately show \<open>bit (word_rotr n w) m \<longleftrightarrow> bit (word_reverse (word_rotl n (word_reverse w))) m\<close>
+ by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff bit_word_reverse_iff)
+qed
lemma word_roti_0 [simp]: "word_roti 0 w = w"
by transfer simp
-lemmas abl_cong = arg_cong [where f = "of_bl"]
-
lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)"
-proof -
- have rotater_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
- by auto
-
- have rotate_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
- by auto
-
- note rpts [symmetric] =
- rotate_inv_plus [THEN conjunct1]
- rotate_inv_plus [THEN conjunct2, THEN conjunct1]
- rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
- rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
-
- note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
- note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
-
- show ?thesis
- apply (unfold word_rot_defs)
- apply (simp only: split: if_split)
- apply (safe intro!: abl_cong)
- apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
- to_bl_rotl
- to_bl_rotr [THEN word_bl.Rep_inverse']
- to_bl_rotr)
- apply (rule rrp rrrp rpts,
- simp add: nat_add_distrib [symmetric]
- nat_diff_distrib [symmetric])+
- done
-qed
+ by (rule bit_word_eqI)
+ (simp add: bit_word_roti_iff nat_less_iff mod_simps ac_simps)
lemma word_roti_conv_mod':
"word_roti n w = word_roti (n mod int (size w)) w"
@@ -4936,18 +4201,6 @@
locale word_rotate
begin
-lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
-
-lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
-
-lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
-
-lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
-
-lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
-
-lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
-
lemma word_rot_logs:
"word_rotl n (NOT v) = NOT (word_rotl n v)"
"word_rotr n (NOT v) = NOT (word_rotr n v)"
@@ -4957,56 +4210,34 @@
"word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
"word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
"word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
- by (rule word_bl.Rep_eqD,
- rule word_rot_defs' [THEN trans],
- simp only: blwl_syms [symmetric],
- rule th1s [THEN trans],
- rule refl)+
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotl_iff bit_not_iff algebra_simps exp_eq_zero_iff not_le)
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotr_iff bit_not_iff algebra_simps exp_eq_zero_iff not_le)
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotl_iff bit_and_iff algebra_simps exp_eq_zero_iff not_le)
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotr_iff bit_and_iff algebra_simps exp_eq_zero_iff not_le)
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotl_iff bit_or_iff algebra_simps exp_eq_zero_iff not_le)
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotr_iff bit_or_iff algebra_simps exp_eq_zero_iff not_le)
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotl_iff bit_xor_iff algebra_simps exp_eq_zero_iff not_le)
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_word_rotr_iff bit_xor_iff algebra_simps exp_eq_zero_iff not_le)
+ done
+
end
lemmas word_rot_logs = word_rotate.word_rot_logs
-lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
- simplified word_bl_Rep']
-
-lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
- simplified word_bl_Rep']
-
-lemma bl_word_roti_dt':
- "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow>
- to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
- apply (unfold word_roti_eq_word_rotr_word_rotl)
- apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
- apply safe
- apply (simp add: zmod_zminus1_eq_if)
- apply safe
- apply (simp add: nat_mult_distrib)
- apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
- [THEN conjunct2, THEN order_less_imp_le]]
- nat_mod_distrib)
- apply (simp add: nat_mod_distrib)
- done
-
-lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
-
-lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
-lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
-lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
-
lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0"
- by (simp add: word_rotr_dt word_rotl_dt replicate_add [symmetric])
+ by transfer simp_all
lemma word_roti_0' [simp] : "word_roti n 0 = 0"
by transfer simp
-lemmas word_rotr_dt_no_bin' [simp] =
- word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
- (* FIXME: negative numerals, 0 and 1 *)
-
-lemmas word_rotl_dt_no_bin' [simp] =
- word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
- (* FIXME: negative numerals, 0 and 1 *)
-
declare word_roti_eq_word_rotr_word_rotl [simp]
@@ -5034,9 +4265,6 @@
lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
by (simp add: eq_neg_iff_add_eq_0)
-lemma max_word_bl: "to_bl (max_word::'a::len word) = replicate LENGTH('a) True"
- by (fact to_bl_n1)
-
lemma max_test_bit: "(max_word::'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)"
by (fact nth_minus1)
@@ -5067,7 +4295,7 @@
lemma shiftr_x_0 [iff]: "x >> 0 = x"
for x :: "'a::len word"
- by (simp add: shiftr_bl)
+ by transfer simp
lemma shiftl_x_0 [simp]: "x << 0 = x"
for x :: "'a::len word"
@@ -5089,44 +4317,6 @@
for x :: "'a::len word"
by (simp add: word_less_nat_alt unat_0_iff)
-lemma to_bl_mask:
- "to_bl (mask n :: 'a::len word) =
- replicate (LENGTH('a) - n) False @
- replicate (min (LENGTH('a)) n) True"
- by (simp add: mask_bl word_rep_drop min_def)
-
-lemma map_replicate_True:
- "n = length xs \<Longrightarrow>
- map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
- by (induct xs arbitrary: n) auto
-
-lemma map_replicate_False:
- "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
- (zip xs (replicate n False)) = replicate n False"
- by (induct xs arbitrary: n) auto
-
-lemma bl_and_mask:
- fixes w :: "'a::len word"
- and n :: nat
- defines "n' \<equiv> LENGTH('a) - n"
- shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
-proof -
- note [simp] = map_replicate_True map_replicate_False
- have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))"
- by (simp add: bl_word_and)
- also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
- by simp
- also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) =
- replicate n' False @ drop n' (to_bl w)"
- unfolding to_bl_mask n'_def by (subst zip_append) auto
- finally show ?thesis .
-qed
-
-lemma drop_rev_takefill:
- "length xs \<le> n \<Longrightarrow>
- drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
- by (simp add: takefill_alt rev_take)
-
lemma map_nth_0 [simp]: "map ((!!) (0::'a::len word)) xs = replicate (length xs) False"
by (induct xs) auto
@@ -5380,8 +4570,6 @@
subsection \<open>Misc\<close>
-declare bin_to_bl_def [simp]
-
ML_file \<open>Tools/word_lib.ML\<close>
ML_file \<open>Tools/smt_word.ML\<close>