kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

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 to_bl_nth) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftr1 w = of_bl (butlast (to_bl w)) proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (prove)
goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
goal (2 subgoals):
 1. n = LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
 2. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
this:
n = LENGTH('a) - 1

goal (2 subgoals):
 1. n = LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
 2. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (chain)
picking this:
n = LENGTH('a) - 1 proof (prove)
using this:
n = LENGTH('a) - 1

goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
this:
n \<noteq> LENGTH('a) - 1

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (chain)
picking this:
n < LENGTH('a)
n \<noteq> LENGTH('a) - 1 proof (prove)
using this:
n < LENGTH('a)
n \<noteq> LENGTH('a) - 1

goal (1 subgoal):
 1. n < LENGTH('a) - 1 proof (state)
this:
n < LENGTH('a) - 1

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (chain)
picking this:
n < LENGTH('a)
n < LENGTH('a) - 1 proof (prove)
using this:
n < LENGTH('a)
n < LENGTH('a) - 1

goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal:
No subgoals! proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal:
No subgoals!
theory Reversed_Bit_Lists

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>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftr1 w) = False # butlast (to_bl w)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftr1 w) = butlast (False # to_bl w) proof (prove)
goal (2 subgoals):
 1. butlast (False # to_bl w) \<in> {bl. length bl = LENGTH('a)}
 2. of_bl (butlast (False # to_bl w)) = shiftr1 w proof (prove)
goal (1 subgoal):
 1. of_bl (butlast (False # to_bl w)) = shiftr1 w proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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 bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl) done qed simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w) proof (state)
goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i proof (state)
goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i proof (state)
this:
n < length (to_bl (sshiftr1 w))

goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i proof (chain)
picking this:
n < length (to_bl (sshiftr1 w)) proof (prove)
using this:
n < length (to_bl (sshiftr1 w))

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

goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i proof (chain)
picking this:
n < LENGTH('a) proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n = 0\<rbrakk> \<Longrightarrow> to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n
 2. \<And>nat. \<lbrakk>n < LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n proof (prove)
goal:
No subgoals! proof (state)
this:
to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n

goal (1 subgoal):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
theory Reversed_Bit_Lists

lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
  for w :: "'a::len word" apply (rule nth_equalityI) apply (simp_all add: word_size nth_to_bl bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w) proof (prove)
goal (2 subgoals):
 1. length (drop n (to_bl (w >>> n))) = length (take (size w - n) (to_bl w))
 2. \<And>i. i < length (drop n (to_bl (w >>> n))) \<Longrightarrow> drop n (to_bl (w >>> n)) ! i = take (size w - n) (to_bl w) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma take_sshiftr':
  "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 (cases n) apply (auto simp add: hd_to_bl_iff bit_simps not_less word_size) apply (rule nth_equalityI) apply (auto simp add: nth_to_bl bit_simps nth_Cons split: nat.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> size w; n = 0\<rbrakk> \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and> take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))
 2. \<And>nat. \<lbrakk>n \<le> size w; n = Suc nat\<rbrakk> \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and> take n (to_bl (w >>> n)) = replicate n (hd (to_bl w)) proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> take (Suc nat) (to_bl (w >>> Suc nat)) = bit w (LENGTH('a) - Suc 0) # replicate nat (bit w (LENGTH('a) - Suc 0)) proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>Suc nat \<le> LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> length (take (Suc nat) (to_bl (w >>> Suc nat))) = length (bit w (LENGTH('a) - Suc 0) # replicate nat (bit w (LENGTH('a) - Suc 0)))
 2. \<And>nat i. \<lbrakk>Suc nat \<le> LENGTH('a); n = Suc nat; i < length (take (Suc nat) (to_bl (w >>> Suc nat)))\<rbrakk> \<Longrightarrow> take (Suc nat) (to_bl (w >>> Suc nat)) ! i = (bit w (LENGTH('a) - Suc 0) # replicate nat (bit w (LENGTH('a) - Suc 0))) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d" by (auto intro: append_take_drop_id [symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take n xs = t; drop n xs = d\<rbrakk> \<Longrightarrow> xs = t @ d
theory Reversed_Bit_Lists

lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)" apply (rule bit_word_eqI) apply (auto simp add: bit_simps nth_append) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl bl << n = of_bl (bl @ replicate n False) proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl bl << n) na = bit (of_bl (bl @ replicate n False)) na proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
  for w :: "'a::len word" by (simp flip: shiftl_of_bl)

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

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False
theory Reversed_Bit_Lists

lemma shiftr1_bl_of:
  "length bl \<le> LENGTH('a) \<Longrightarrow>
    shiftr1 (of_bl bl::'a::len word) = of_bl (butlast bl)" apply (rule bit_word_eqI) apply (simp add: bit_simps) apply (cases bl rule: rev_cases) apply auto done

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

lemma shiftr_bl_of:
  "length bl \<le> LENGTH('a) \<Longrightarrow>
     (of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)" by (rule bit_word_eqI) (auto simp add: bit_simps rev_nth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length bl \<le> LENGTH('a) \<Longrightarrow> of_bl bl >> n = of_bl (take (length bl - n) bl)
theory Reversed_Bit_Lists

lemma mask_bl: "mask n = of_bl (replicate n True)" by (auto simp add: bit_simps intro!: word_eqI)

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

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 bit_simps) apply (auto simp add: word_size test_bit_bl nth_append rev_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w) proof (prove)
goal (2 subgoals):
 1. length (to_bl (w AND mask n)) = length (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w))
 2. \<And>i. i < length (to_bl (w AND mask n)) \<Longrightarrow> to_bl (w AND mask n) ! i = (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (to_bl (w AND mask n)) \<Longrightarrow> to_bl (w AND mask n) ! i = (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < LENGTH('a) \<Longrightarrow> (bit w (LENGTH('a) - Suc i) \<and> LENGTH('a) - Suc i < n) = (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slice1 n w = of_bl (takefill False n (to_bl w)) proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('b) \<Longrightarrow> bit (slice1 n w) na = bit (of_bl (takefill False n (to_bl w))) na proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('b) \<Longrightarrow> bit (slice1 n w) na = bit (of_bl (takefill False n (to_bl w))) na proof (state)
this:
m < LENGTH('b)

goal (1 subgoal):
 1. \<And>na. na < LENGTH('b) \<Longrightarrow> bit (slice1 n w) na = bit (of_bl (takefill False n (to_bl w))) na proof (prove)
goal (1 subgoal):
 1. bit (slice1 n w) m = bit (of_bl (takefill False n (to_bl w))) m proof (state)
this:
bit (slice1 n w) m = bit (of_bl (takefill False n (to_bl w))) m

goal:
No subgoals!
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slice1 n (numeral w) = of_bl (takefill False n (bin_to_bl LENGTH('b) (numeral w)))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slice n (numeral w) = of_bl (takefill False (LENGTH('b) - n) (bin_to_bl LENGTH('b) (numeral w)))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slice n w = of_bl (take (size w - n) (to_bl w))
theory Reversed_Bit_Lists

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))" apply (simp add: slice1_eq_of_bl) apply transfer apply (simp add: bl_bin_bl_rep_drop) using drop_takefill apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = slice1 n w; fs = size sl; fs + k = n\<rbrakk> \<Longrightarrow> to_bl sl = takefill False fs (drop k (to_bl w)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = of_bl (takefill False n (to_bl w)); fs = size (of_bl (takefill False n (to_bl w))); size (of_bl (takefill False n (to_bl w))) + k = n\<rbrakk> \<Longrightarrow> to_bl (of_bl (takefill False n (to_bl w))) = takefill False (size (of_bl (takefill False n (to_bl w)))) (drop k (to_bl w)) proof (prove)
goal (1 subgoal):
 1. \<And>sl n w fs k. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); fs = LENGTH('a); LENGTH('a) + k = n\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))) = takefill False LENGTH('a) (drop k (bin_to_bl LENGTH('b) w)) proof (prove)
goal (1 subgoal):
 1. \<And>sl n w fs k. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); fs = LENGTH('a); LENGTH('a) + k = n\<rbrakk> \<Longrightarrow> drop (n - LENGTH('a)) (takefill False n (bin_to_bl LENGTH('b) w)) = takefill False LENGTH('a) (drop k (bin_to_bl LENGTH('b) w)) proof (prove)
using this:
drop ?k (takefill ?fill (?m + ?k) ?w) = takefill ?fill ?m (drop ?k ?w)

goal (1 subgoal):
 1. \<And>sl n w fs k. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); fs = LENGTH('a); LENGTH('a) + k = n\<rbrakk> \<Longrightarrow> drop (n - LENGTH('a)) (takefill False n (bin_to_bl LENGTH('b) w)) = takefill False LENGTH('a) (drop k (bin_to_bl LENGTH('b) w)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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 (simp add: slice1_eq_of_bl) apply transfer apply (simp add: bl_bin_bl_rep_drop flip: takefill_append) apply (metis diff_add_inverse) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = slice1 n w; fs = size sl; fs = n + k\<rbrakk> \<Longrightarrow> to_bl sl = takefill False fs (replicate k False @ to_bl w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = of_bl (takefill False n (to_bl w)); n + k = size (of_bl (takefill False n (to_bl w))); fs = size (of_bl (takefill False n (to_bl w)))\<rbrakk> \<Longrightarrow> to_bl (of_bl (takefill False n (to_bl w))) = takefill False (size (of_bl (takefill False n (to_bl w)))) (replicate k False @ to_bl w) proof (prove)
goal (1 subgoal):
 1. \<And>sl n w k fs. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); n + k = LENGTH('a); fs = LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))) = takefill False LENGTH('a) (replicate k False @ bin_to_bl LENGTH('b) w) proof (prove)
goal (1 subgoal):
 1. \<And>sl n w k fs. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); n + k = LENGTH('a); fs = LENGTH('a)\<rbrakk> \<Longrightarrow> takefill False LENGTH('a) (replicate (LENGTH('a) - n) False @ bin_to_bl LENGTH('b) w) = takefill False LENGTH('a) (replicate k False @ bin_to_bl LENGTH('b) w) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (slice1 n w) = rev (takefill False LENGTH('a) (rev (takefill False n (to_bl w)))) proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl (takefill False n (to_bl w))) = rev (takefill False LENGTH('a) (rev (takefill False n (to_bl w))))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. revcast w = of_bl (takefill False LENGTH('b) (to_bl w))
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (revcast w) = takefill False LENGTH('a) (to_bl w) proof (prove)
goal (2 subgoals):
 1. length (to_bl (revcast w)) = length (takefill False LENGTH('a) (to_bl w))
 2. \<And>i. i < length (to_bl (revcast w)) \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (to_bl (revcast w)) \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length (to_bl (revcast w)); LENGTH('a) \<le> LENGTH('b)\<rbrakk> \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i
 2. \<And>i. \<lbrakk>i < length (to_bl (revcast w)); \<not> LENGTH('a) \<le> LENGTH('b)\<rbrakk> \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_cat a b = of_bl (to_bl a @ to_bl b) proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (word_cat a b) n = bit (of_bl (to_bl a @ to_bl b)) n proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> LENGTH('c) \<le> n \<longrightarrow> bit a (n - LENGTH('c)) = (rev (to_bl a) ! (n - LENGTH('c)) \<and> n < LENGTH('b) + LENGTH('c)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma of_bl_append:
  "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys" apply transfer apply (simp add: bl_to_bin_app_cat bin_cat_num) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (xs @ ys) = of_bl xs * 2 ^ length ys + of_bl ys proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. take_bit LENGTH('a) (bl_to_bin (xs @ ys)) = take_bit LENGTH('a) (bl_to_bin xs * 2 ^ length ys + bl_to_bin ys) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs" by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (False # xs) = of_bl xs
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (True # xs) = 2 ^ length xs + of_bl xs
theory Reversed_Bit_Lists

lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs" by (cases x) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (x # xs) = of_bool x * 2 ^ length xs + of_bl xs