(* 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