kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sc = scast; source_size sc = target_size sc + n\<rbrakk> \<Longrightarrow> to_bl (sc w) = drop n (to_bl w) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sc = scast; source_size sc = target_size sc + n; sc = ucast\<rbrakk> \<Longrightarrow> to_bl (sc w) = drop n (to_bl w)
 2. \<lbrakk>sc = scast; source_size sc = target_size sc + n\<rbrakk> \<Longrightarrow> sc = ucast proof (prove)
goal (2 subgoals):
 1. \<lbrakk>source_size scast = target_size scast + n; scast = ucast; sc = scast\<rbrakk> \<Longrightarrow> to_bl (scast w) = drop n (to_bl w)
 2. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> scast = ucast proof (prove)
goal (2 subgoals):
 1. \<lbrakk>source_size ucast = target_size ucast + n; scast = ucast; sc = ucast\<rbrakk> \<Longrightarrow> to_bl (ucast w) = drop n (to_bl w)
 2. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> scast = ucast proof (prove)
goal (1 subgoal):
 1. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> scast = ucast proof (prove)
goal (1 subgoal):
 1. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> is_down ucast proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_0_bl [simp]: "of_bl [] = 0" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl [] = 0
theory Reversed_Bit_Lists

lemma word_1_bl: "of_bl [True] = 1" by transfer (simp add: bl_to_bin_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl [True] = 1
theory Reversed_Bit_Lists

lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0" by transfer (simp add: bl_to_bin_rep_False)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (replicate n False) = 0
theory Reversed_Bit_Lists

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>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl 0 = replicate LENGTH('a) False
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_bl v = vbl; to_bl w = wbl\<rbrakk> \<Longrightarrow> to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl)) proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) v = vbl; bin_to_bl LENGTH('a) w = wbl\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v + w) = rev (rbl_add (rev vbl) (rev wbl)) proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) w = wbl; vbl = bin_to_bl LENGTH('a) v\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v + w) = rev (rbl_add (rev vbl) (rev wbl)) proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>vbl = bin_to_bl LENGTH('a) v; wbl = bin_to_bl LENGTH('a) w\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v + w) = rev (rbl_add (rev vbl) (rev wbl)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_bl v = vbl; to_bl w = wbl\<rbrakk> \<Longrightarrow> to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl)) proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) v = vbl; bin_to_bl LENGTH('a) w = wbl\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v * w) = rev (rbl_mult (rev vbl) (rev wbl)) proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) w = wbl; vbl = bin_to_bl LENGTH('a) v\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v * w) = rev (rbl_mult (rev vbl) (rev wbl)) proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>vbl = bin_to_bl LENGTH('a) v; wbl = bin_to_bl LENGTH('a) w\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v * w) = rev (rbl_mult (rev vbl) (rev wbl)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((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)) &&& (\<lbrakk>rev (to_bl v) = ys; rev (to_bl w) = xs\<rbrakk> \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs) &&& (\<lbrakk>rev (to_bl v) = ys; rev (to_bl w) = xs\<rbrakk> \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs)
theory Reversed_Bit_Lists

lemma of_bl_length_less:
  \<open>(of_bl x :: 'a::len word) < 2 ^ k\<close>
    if \<open>length x = k\<close> \<open>k < LENGTH('a)\<close> proof - from that have \<open>length x < LENGTH('a)\<close> by simp then have \<open>(of_bl x :: 'a::len word) < 2 ^ length x\<close> apply (simp add: of_bl_eq) apply transfer apply (simp add: take_bit_horner_sum_bit_eq) apply (subst length_rev [symmetric]) apply (simp only: horner_sum_of_bool_2_less) done with that show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl x < 2 ^ k proof (state)
goal (1 subgoal):
 1. of_bl x < 2 ^ k proof (chain)
picking this:
length x = k
k < LENGTH('a) proof (prove)
using this:
length x = k
k < LENGTH('a)

goal (1 subgoal):
 1. length x < LENGTH('a) proof (state)
this:
length x < LENGTH('a)

goal (1 subgoal):
 1. of_bl x < 2 ^ k proof (chain)
picking this:
length x < LENGTH('a) proof (prove)
using this:
length x < LENGTH('a)

goal (1 subgoal):
 1. of_bl x < 2 ^ length x proof (prove)
goal (1 subgoal):
 1. length x < LENGTH('a) \<Longrightarrow> horner_sum of_bool 2 (rev x) < 2 ^ length x proof (prove)
goal (1 subgoal):
 1. \<And>x. length x < LENGTH('a) \<Longrightarrow> take_bit LENGTH('a) (horner_sum of_bool 2 (rev x)) < take_bit LENGTH('a) (2 ^ length x) proof (prove)
goal (1 subgoal):
 1. \<And>x. length x < LENGTH('a) \<Longrightarrow> horner_sum of_bool 2 (rev x) < 2 ^ length x proof (prove)
goal (1 subgoal):
 1. \<And>x. length x < LENGTH('a) \<Longrightarrow> horner_sum of_bool 2 (rev x) < 2 ^ length (rev x) proof (prove)
goal:
No subgoals! proof (state)
this:
of_bl x < 2 ^ length x

goal (1 subgoal):
 1. of_bl x < 2 ^ k proof (chain)
picking this:
length x = k
k < LENGTH('a)
of_bl x < 2 ^ length x proof (prove)
using this:
length x = k
k < LENGTH('a)
of_bl x < 2 ^ length x

goal (1 subgoal):
 1. of_bl x < 2 ^ k proof (state)
this:
of_bl x < 2 ^ k

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)" by transfer (simp flip: bl_xor_bin)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)
theory Reversed_Bit_Lists

lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)" by transfer (simp flip: bl_or_bin)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)
theory Reversed_Bit_Lists

lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)" by transfer (simp flip: bl_and_bin)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)
theory Reversed_Bit_Lists

lemma bin_nth_uint': "bit (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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w) proof (prove)
goal (1 subgoal):
 1. bit (uint w) n = (rev (bin_to_bl LENGTH('a) (uint w)) ! n \<and> n < LENGTH('a)) proof (prove)
goal (2 subgoals):
 1. bit (uint w) n \<Longrightarrow> rev (bin_to_bl LENGTH('a) (uint w)) ! n
 2. \<lbrakk>rev (bin_to_bl LENGTH('a) (uint w)) ! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (uint w) n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bit (uint w) n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> rev (bin_to_bl LENGTH('a) (uint w)) ! n
 2. \<lbrakk>rev (bin_to_bl LENGTH('a) (uint w)) ! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (uint w) n proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma test_bit_bl: "bit w n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w" by transfer (auto simp add: bin_nth_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit w n = (rev (to_bl w) ! n \<and> n < size w)
theory Reversed_Bit_Lists

lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = bit w (size w - Suc n)" by (simp add: word_size rev_nth test_bit_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < size w \<Longrightarrow> to_bl w ! n = bit w (size w - Suc n)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map (bit w) [0..<n] = takefill False n (rev (to_bl w)) proof (state)
goal (2 subgoals):
 1. length (map (bit w) [0..<n]) = length (takefill False n (rev (to_bl w)))
 2. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i proof (prove)
goal (1 subgoal):
 1. length (map (bit w) [0..<n]) = length (takefill False n (rev (to_bl w))) proof (state)
this:
length (map (bit w) [0..<n]) = length (takefill False n (rev (to_bl w)))

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i proof (state)
goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i proof (state)
this:
m < length (map (bit w) [0..<n])

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i proof (chain)
picking this:
m < length (map (bit w) [0..<n]) proof (prove)
using this:
m < length (map (bit w) [0..<n])

goal (1 subgoal):
 1. m < n proof (state)
this:
m < n

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i proof (chain)
picking this:
m < n proof (prove)
using this:
m < n

goal (1 subgoal):
 1. bit w m = takefill False n (rev (to_bl w)) ! m proof (state)
this:
bit w m = takefill False n (rev (to_bl w)) ! m

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i proof (chain)
picking this:
m < n
bit w m = takefill False n (rev (to_bl w)) ! m proof (prove)
using this:
m < n
bit w m = takefill False n (rev (to_bl w)) ! m

goal (1 subgoal):
 1. map (bit w) [0..<n] ! m = takefill False n (rev (to_bl w)) ! m proof (state)
this:
map (bit w) [0..<n] ! m = takefill False n (rev (to_bl w)) ! m

goal:
No subgoals!
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w = rev (map (bit w) [0..<LENGTH('a)])
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl w) ! n = bit w n proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. rev (to_bl w) ! n = bit w n
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w ! n = bit w (LENGTH('a) - Suc n) proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. to_bl w ! n = bit w (LENGTH('a) - Suc n)
theory Reversed_Bit_Lists

lemma [code abstract]:
  \<open>Word.the_int (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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Word.the_int (of_bl bs) = horner_sum of_bool 2 (take LENGTH('a) (rev bs)) proof (prove)
goal (1 subgoal):
 1. uint (horner_sum of_bool 2 (rev bs)) = take_bit LENGTH('a) (horner_sum of_bool 2 (rev bs)) proof (prove)
goal (1 subgoal):
 1. \<And>bs. take_bit LENGTH('a) (horner_sum of_bool 2 (rev bs)) = take_bit LENGTH('a) (horner_sum of_bool 2 (rev bs)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma [code]:
  \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a::len)])\<close>
  for w :: \<open>'a::len word\<close> by (fact to_bl_eq_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w = map (bit w) (rev [0..<LENGTH('a)])
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_reverse w = of_bl (rev (to_bl w))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (word_reverse w) = rev (to_bl w)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (- 1) = replicate LENGTH('a) True proof (prove)
goal (2 subgoals):
 1. replicate LENGTH('a) True \<in> {bl. length bl = LENGTH('a)}
 2. of_bl (replicate LENGTH('a) True) = - 1 proof (prove)
goal (1 subgoal):
 1. of_bl (replicate LENGTH('a) True) = - 1 proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size (of_bl (replicate LENGTH('a) True)) \<longrightarrow> bit (of_bl (replicate LENGTH('a) True)) n = bit (- 1) n proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (of_bl (replicate LENGTH('a) True)) n proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))
theory Reversed_Bit_Lists

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 (rule bit_word_eqI) (auto simp add: bit_simps rev_nth nth_append nth_butlast nth_bin_to_bl simp flip: bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b) = of_bl (b # butlast (bin_to_bl LENGTH('a) (numeral w)))
theory Reversed_Bit_Lists

lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)" unfolding bshiftr1_eq by (rule word_bl.Abs_inverse) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b)) = b # butlast (to_bl w) proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl (b # butlast (to_bl w))) = b # butlast (to_bl w)
theory Reversed_Bit_Lists

lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])" apply (rule bit_word_eqI) apply (simp add: bit_simps) subgoal for n apply (cases n) apply simp_all done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 (of_bl bl) = of_bl (bl @ [False]) proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftl1 (of_bl bl)) n = bit (of_bl (bl @ [False])) n proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl)) proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n = 0\<rbrakk> \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl))
 2. \<And>nat. \<lbrakk>n < LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])" apply (rule bit_word_eqI) apply (simp add: bit_simps) subgoal for n apply (cases n) apply (simp_all add: nth_rev_to_bl) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 w = of_bl (to_bl w @ [False]) proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftl1 w) n = bit (of_bl (to_bl w @ [False])) n proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n = 0\<rbrakk> \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n
 2. \<And>nat. \<lbrakk>n < LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftl1 w) = tl (to_bl w) @ [False]
theory Reversed_Bit_Lists

lemma to_bl_double_eq:
  \<open>to_bl (2 * w) = tl (to_bl w) @ [False]\<close> using bl_shiftl1 [of w] by (simp add: shiftl1_def ac_simps)

\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (2 * w) = tl (to_bl w) @ [False] proof (prove)
using this:
to_bl (shiftl1 w) = tl (to_bl w) @ [False]

goal (1 subgoal):
 1. to_bl (2 * w) = tl (to_bl w) @ [False]
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftl1 w) = tl (to_bl w @ [False])