kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

lemma to_bl_2p:
  "n < LENGTH('a) \<Longrightarrow>
   to_bl ((2::'a::len word) ^ n) =
   replicate (LENGTH('a) - Suc n) False @ True # replicate n False" apply (rule nth_equalityI) apply (auto simp add: nth_append to_bl_nth word_size bit_simps not_less nth_Cons le_diff_conv) subgoal for i apply (cases \<open>Suc (i + n) - LENGTH('a)\<close>) apply simp_all done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> to_bl (2 ^ n) = replicate (LENGTH('a) - Suc n) False @ True # replicate n False proof (prove)
goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> length (to_bl (2 ^ n)) = length (replicate (LENGTH('a) - Suc n) False @ True # replicate n False)
 2. \<And>i. \<lbrakk>n < LENGTH('a); i < length (to_bl (2 ^ n))\<rbrakk> \<Longrightarrow> to_bl (2 ^ n) ! i = (replicate (LENGTH('a) - Suc n) False @ True # replicate n False) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k; Suc (i + n) - LENGTH('a) = 0\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i
 2. \<And>nat. \<lbrakk>n < LENGTH('a); i < LENGTH('a); LENGTH('a) \<le> Suc (i + n); case Suc (i + n) - LENGTH('a) of 0 \<Rightarrow> True | Suc k \<Rightarrow> replicate n False ! k; Suc (i + n) - LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> n = LENGTH('a) - Suc i proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma xor_2p_to_bl:
  fixes x::"'a::len word"
  shows "to_bl (x XOR 2^n) =
  (if n < LENGTH('a)
   then take (LENGTH('a)-Suc n) (to_bl x) @ (\<not>rev (to_bl x)!n) # drop (LENGTH('a)-n) (to_bl x)
   else to_bl x)" apply (auto simp add: to_bl_eq_rev take_map drop_map take_rev drop_rev bit_simps) apply (rule nth_equalityI) apply (auto simp add: bit_simps rev_nth nth_append Suc_diff_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (x XOR 2 ^ n) = (if n < LENGTH('a) then take (LENGTH('a) - Suc n) (to_bl x) @ (\<not> rev (to_bl x) ! n) # drop (LENGTH('a) - n) (to_bl x) else to_bl x) proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)]) = map (bit x) (rev [Suc n..<LENGTH('a)]) @ (\<not> rev (map (bit x) (rev [0..<LENGTH('a)])) ! n) # map (bit x) (rev [0..<n]) proof (prove)
goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> length (map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)])) = length (map (bit x) (rev [Suc n..<LENGTH('a)]) @ (\<not> rev (map (bit x) (rev [0..<LENGTH('a)])) ! n) # map (bit x) (rev [0..<n]))
 2. \<And>i. \<lbrakk>n < LENGTH('a); i < length (map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)]))\<rbrakk> \<Longrightarrow> map (bit (x XOR 2 ^ n)) (rev [0..<LENGTH('a)]) ! i = (map (bit x) (rev [Suc n..<LENGTH('a)]) @ (\<not> rev (map (bit x) (rev [0..<LENGTH('a)])) ! n) # map (bit x) (rev [0..<n])) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma is_aligned_replicateD:
  "\<lbrakk> is_aligned (w::'a::len word) n; n \<le> LENGTH('a) \<rbrakk>
     \<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False
               \<and> length xs = size w - n" apply (subst is_aligned_replicate, assumption+) apply (rule exI, rule conjI, rule refl) apply (simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False \<and> length xs = size w - n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> \<exists>xs. take (LENGTH('a) - n) (to_bl w) @ replicate n False = xs @ replicate n False \<and> length xs = size w - n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> length (take (LENGTH('a) - n) (to_bl w)) = size w - n proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bl_pad_to_length:
  assumes lbl: "length bl \<le> sz"
  shows   "length (bl_pad_to bl sz) = sz" using lbl by (simp add: bl_pad_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (bl_pad_to bl sz) = sz proof (prove)
using this:
length bl \<le> sz

goal (1 subgoal):
 1. length (bl_pad_to bl sz) = sz
theory Reversed_Bit_Lists

lemma bl_pad_to_prefix:
  "prefix bl (bl_pad_to bl sz)" by (simp add: bl_pad_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix bl (bl_pad_to bl sz)
theory Reversed_Bit_Lists

lemma of_bl_length:
  "length xs < LENGTH('a) \<Longrightarrow> of_bl xs < (2 :: 'a::len word) ^ length xs" by (simp add: of_bl_length_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs < LENGTH('a) \<Longrightarrow> of_bl xs < 2 ^ length xs
theory Reversed_Bit_Lists

lemma of_bl_mult_and_not_mask_eq:
  "\<lbrakk>is_aligned (a :: 'a::len word) n; length b + m \<le> n\<rbrakk>
   \<Longrightarrow> a + of_bl b * (2^m) AND NOT(mask n) = a" apply (simp flip: push_bit_eq_mult subtract_mask(1) take_bit_eq_mask) apply (subst disjunctive_add) apply (auto simp add: bit_simps not_le not_less) apply (meson is_aligned_imp_not_bit is_aligned_weaken less_diff_conv2) apply (erule is_alignedE') apply (simp add: take_bit_push_bit) apply (rule bit_word_eqI) apply (auto simp add: bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ m AND NOT (mask n) = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n (a + push_bit m (of_bl b)) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> \<not> bit a na \<or> \<not> bit (push_bit m (of_bl b)) na
 2. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n (a OR push_bit m (of_bl b)) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + m \<le> n; rev b ! (na - m); bit a na; m \<le> na; na < LENGTH('a); na - m < length b\<rbrakk> \<Longrightarrow> LENGTH('a) \<le> na - m
 2. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n a OR take_bit n (push_bit m (of_bl b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n a OR take_bit n (push_bit m (of_bl b)) proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>length b + m \<le> n; a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = take_bit n a OR take_bit n (push_bit m (of_bl b)) proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>length b + m \<le> n; a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> push_bit m (of_bl b) = push_bit m (take_bit (n - m) (of_bl b)) proof (prove)
goal (1 subgoal):
 1. \<And>q na. \<lbrakk>length b + m \<le> n; a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (push_bit m (of_bl b)) na = bit (push_bit m (take_bit (n - m) (of_bl b))) na proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bin_to_bl_of_bl_eq:
  "\<lbrakk>is_aligned (a::'a::len word) n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk>
  \<Longrightarrow> bin_to_bl (length b) (uint ((a + of_bl b * 2^c) >> c)) = b" apply (simp flip: push_bit_eq_mult take_bit_eq_mask) apply (subst disjunctive_add) apply (auto simp add: bit_simps not_le not_less unsigned_or_eq unsigned_drop_bit_eq
     unsigned_push_bit_eq bin_to_bl_or simp flip: bin_to_bl_def) apply (meson is_aligned_imp_not_bit is_aligned_weaken less_diff_conv2) apply (erule is_alignedE') apply (rule nth_equalityI) apply (auto simp add: nth_bin_to_bl bit_simps rev_nth simp flip: bin_to_bl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a + of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length b) (uint (a + push_bit c (of_bl b) >> c)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> bit a na \<or> \<not> bit (push_bit c (of_bl b)) na
 2. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length b) (uint (a OR push_bit c (of_bl b) >> c)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); rev b ! (na - c); bit a na; c \<le> na; na < LENGTH('a); na - c < length b\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) = b proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) = b proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> length (bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c))) = length b
 2. \<And>q i. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n); i < length (bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)))\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a OR push_bit c (of_bl b) >> c)) ! i = b ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma length_drop_mask:
  fixes w::"'a::len word"
  shows "length (dropWhile Not (to_bl (w AND mask n))) \<le> n" proof - have "length (takeWhile Not (replicate n False @ ls)) = n + length (takeWhile Not ls)"
    for ls n by(subst takeWhile_append2) simp+ then show ?thesis unfolding bl_and_mask by (simp add: dropWhile_eq_drop) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n proof (state)
goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (replicate n False @ ls)) = n + length (takeWhile Not ls) proof (state)
this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls)

goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n proof (chain)
picking this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls) proof (prove)
using this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls)

goal (1 subgoal):
 1. length (dropWhile Not (to_bl (w AND mask n))) \<le> n proof (prove)
using this:
length (takeWhile Not (replicate ?n False @ ?ls)) = ?n + length (takeWhile Not ?ls)

goal (1 subgoal):
 1. length (dropWhile Not (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w))) \<le> n proof (state)
this:
length (dropWhile Not (to_bl (w AND mask n))) \<le> n

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma of_bl_length2:
  "length xs + c < LENGTH('a) \<Longrightarrow> of_bl xs * 2^c < (2::'a::len word) ^ (length xs + c)" by (simp add: of_bl_length word_less_power_trans2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs + c < LENGTH('a) \<Longrightarrow> of_bl xs * 2 ^ c < 2 ^ (length xs + c)
theory Reversed_Bit_Lists

lemma of_bl_max:
  "(of_bl xs :: 'a::len word) \<le> mask (length xs)" proof - define ys where \<open>ys = rev xs\<close> have \<open>take_bit (length ys) (horner_sum of_bool 2 ys :: 'a word) = horner_sum of_bool 2 ys\<close> by transfer (simp add: take_bit_horner_sum_bit_eq min_def) then have \<open>(of_bl (rev ys) :: 'a word) \<le> mask (length ys)\<close> by (simp only: of_bl_rev_eq less_eq_mask_iff_take_bit_eq_self) with ys_def show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs) proof (state)
goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs) proof (state)
this:
ys = rev xs

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs) proof (prove)
goal (1 subgoal):
 1. take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys proof (state)
this:
take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs) proof (chain)
picking this:
take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys proof (prove)
using this:
take_bit (length ys) (horner_sum of_bool 2 ys) = horner_sum of_bool 2 ys

goal (1 subgoal):
 1. of_bl (rev ys) \<le> mask (length ys) proof (state)
this:
of_bl (rev ys) \<le> mask (length ys)

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs) proof (chain)
picking this:
ys = rev xs
of_bl (rev ys) \<le> mask (length ys) proof (prove)
using this:
ys = rev xs
of_bl (rev ys) \<le> mask (length ys)

goal (1 subgoal):
 1. of_bl xs \<le> mask (length xs) proof (state)
this:
of_bl xs \<le> mask (length xs)

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma sshiftr_clamp_neg:
  assumes
    "LENGTH('a) \<le> n"
    "sint x < 0"
  shows "(x::'a::len word) >>> n = -1" apply (rule bit_word_eqI) using assms apply (auto simp add: bit_simps bit_last_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >>> n = - 1 proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (- 1) na proof (prove)
using this:
LENGTH('a) \<le> n
sint x < 0

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (- 1) na proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma sshiftr_clamp:
  assumes "LENGTH('a) \<le> n"
  shows "(x::'a::len word) >>> n = x >>> LENGTH('a)" apply (rule bit_word_eqI) using assms apply (auto simp add: bit_simps bit_last_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >>> n = x >>> LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (x >>> LENGTH('a)) na proof (prove)
using this:
LENGTH('a) \<le> n

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x >>> n) na = bit (x >>> LENGTH('a)) na proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma sshiftr1_bl_of:
  "length bl = LENGTH('a) \<Longrightarrow>
    sshiftr1 (of_bl bl::'a::len word) = of_bl (hd bl # butlast bl)" apply (rule word_bl.Rep_eqD) apply (subst bl_sshiftr1[of "of_bl bl :: 'a word"]) by (simp add: word_bl.Abs_inverse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length bl = LENGTH('a) \<Longrightarrow> sshiftr1 (of_bl bl) = of_bl (hd bl # butlast bl) proof (prove)
goal (1 subgoal):
 1. length bl = LENGTH('a) \<Longrightarrow> to_bl (sshiftr1 (of_bl bl)) = to_bl (of_bl (hd bl # butlast bl)) proof (prove)
goal (1 subgoal):
 1. length bl = LENGTH('a) \<Longrightarrow> hd (to_bl (of_bl bl)) # butlast (to_bl (of_bl bl)) = to_bl (of_bl (hd bl # butlast bl))
theory Reversed_Bit_Lists

lemma sshiftr1_bl_of':
  "LENGTH('a) \<le> length bl \<Longrightarrow>
    sshiftr1 (of_bl bl::'a::len word) =
    of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))" apply (subst of_bl_drop'[symmetric, of "length bl - LENGTH('a)"]) using sshiftr1_bl_of[of "drop (length bl - LENGTH('a)) bl"] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> length bl \<Longrightarrow> sshiftr1 (of_bl bl) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl)) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> length bl \<Longrightarrow> length bl - LENGTH('a) = length bl - LENGTH('a)
 2. LENGTH('a) \<le> length bl \<Longrightarrow> sshiftr1 (of_bl (drop (length bl - LENGTH('a)) bl)) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl)) proof (prove)
using this:
length (drop (length bl - LENGTH('a)) bl) = LENGTH(?'a) \<Longrightarrow> sshiftr1 (of_bl (drop (length bl - LENGTH('a)) bl)) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))

goal (2 subgoals):
 1. LENGTH('a) \<le> length bl \<Longrightarrow> length bl - LENGTH('a) = length bl - LENGTH('a)
 2. LENGTH('a) \<le> length bl \<Longrightarrow> sshiftr1 (of_bl (drop (length bl - LENGTH('a)) bl)) = of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))
theory Reversed_Bit_Lists

lemma sshiftr_bl_of:
  assumes "length bl = LENGTH('a)"
  shows "(of_bl bl::'a::len word) >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)" proof - from assms obtain b bs where \<open>bl = b # bs\<close> by (cases bl) simp_all then have *: \<open>bl ! 0 \<longleftrightarrow> b\<close> \<open>hd bl \<longleftrightarrow> b\<close> by simp_all show ?thesis apply (rule bit_word_eqI) using assms * by (auto simp add: bit_simps nth_append rev_nth not_less) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl) proof (state)
goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl) proof (chain)
picking this:
length bl = LENGTH('a) proof (prove)
using this:
length bl = LENGTH('a)

goal (1 subgoal):
 1. (\<And>b bs. bl = b # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
bl = b # bs

goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl) proof (chain)
picking this:
bl = b # bs proof (prove)
using this:
bl = b # bs

goal (1 subgoal):
 1. bl ! 0 = b &&& hd bl = b proof (state)
this:
bl ! 0 = b
hd bl = b

goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl) proof (prove)
goal (1 subgoal):
 1. of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl) proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl bl >>> n) na = bit (of_bl (replicate n (hd bl) @ take (length bl - n) bl)) na proof (prove)
using this:
length bl = LENGTH('a)
bl ! 0 = b
hd bl = b

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl bl >>> n) na = bit (of_bl (replicate n (hd bl) @ take (length bl - n) bl)) na proof (state)
this:
of_bl bl >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma sshiftr_bl: "x >>> n \<equiv> of_bl (replicate n (msb x) @ take (LENGTH('a) - n) (to_bl x))"
  for x :: "'a::len word" unfolding word_msb_alt by (smt (z3) length_to_bl_eq sshiftr_bl_of word_bl.Rep_inverse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >>> n \<equiv> of_bl (replicate n (msb x) @ take (LENGTH('a) - n) (to_bl x)) proof (prove)
goal (1 subgoal):
 1. x >>> n \<equiv> of_bl (replicate n (hd (to_bl x)) @ take (LENGTH('a) - n) (to_bl x))
theory Reversed_Bit_Lists

lemma of_bl_drop_eq_take_bit:
  \<open>of_bl (drop n xs) = take_bit (length xs - n) (of_bl xs)\<close> by (simp add: of_bl_drop take_bit_eq_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (drop n xs) = take_bit (length xs - n) (of_bl xs)
theory Reversed_Bit_Lists

lemma of_bl_take_to_bl_eq_drop_bit:
  \<open>of_bl (take n (to_bl w)) = drop_bit (LENGTH('a) - n) w\<close>
    if \<open>n \<le> LENGTH('a)\<close>
    for w :: \<open>'a::len word\<close> using that shiftr_bl [of w \<open>LENGTH('a) - n\<close>] by (simp add: shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (take n (to_bl w)) = drop_bit (LENGTH('a) - n) w proof (prove)
using this:
n \<le> LENGTH('a)
w >> LENGTH('a) - n \<equiv> of_bl (take (LENGTH('a) - (LENGTH('a) - n)) (to_bl w))

goal (1 subgoal):
 1. of_bl (take n (to_bl w)) = drop_bit (LENGTH('a) - n) w
theory Bitwise

lemma carry_simps:
  "carry True a b = (a \<or> b)"
  "carry a True b = (a \<or> b)"
  "carry a b True = (a \<or> b)"
  "carry False a b = (a \<and> b)"
  "carry a False b = (a \<and> b)"
  "carry a b False = (a \<and> b)" by (auto simp add: carry_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (carry True a b = (a \<or> b) &&& carry a True b = (a \<or> b) &&& carry a b True = (a \<or> b)) &&& carry False a b = (a \<and> b) &&& carry a False b = (a \<and> b) &&& carry a b False = (a \<and> b)
theory Bitwise

lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (x - y) = to_bl (x + - y)
theory Bitwise

lemma rbl_word_1: "rev (to_bl (1 :: 'a::len word)) = takefill False (LENGTH('a)) [True]" apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans) apply simp apply (simp only: rtb_rbl_ariths(1)[OF refl]) apply simp apply (case_tac "LENGTH('a)") apply simp apply (simp add: takefill_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl 1) = takefill False LENGTH('a) [True] proof (prove)
goal (2 subgoals):
 1. rev (to_bl 1) = rev (to_bl (word_succ 0))
 2. rev (to_bl (word_succ 0)) = takefill False LENGTH('a) [True] proof (prove)
goal (1 subgoal):
 1. rev (to_bl (word_succ 0)) = takefill False LENGTH('a) [True] proof (prove)
goal (1 subgoal):
 1. rbl_succ (rev (to_bl 0)) = takefill False LENGTH('a) [True] proof (prove)
goal (1 subgoal):
 1. rbl_succ (replicate LENGTH('a) False) = takefill False LENGTH('a) [True] proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> rbl_succ (replicate LENGTH('a) False) = takefill False LENGTH('a) [True]
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> rbl_succ (replicate LENGTH('a) False) = takefill False LENGTH('a) [True] proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> rbl_succ (replicate LENGTH('a) False) = takefill False LENGTH('a) [True] proof (prove)
goal:
No subgoals!
theory Bitwise

lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))
theory Bitwise

lemma rbl_add_carry_Cons:
  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) =
    xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)" by (simp add: carry_def xor3_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) = xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)