kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> rbl_mult bl (rev (bin_to_bl m binb)) = rbl_mult bl (rev (bin_to_bl (length bl) binb)) proof (prove)
goal (2 subgoals):
 1. length bl \<le> m \<Longrightarrow> rbl_mult bl (rev (bin_to_bl m binb)) = ?s
 2. length bl \<le> m \<Longrightarrow> ?s = rbl_mult bl (rev (bin_to_bl (length bl) binb)) proof (prove)
goal (2 subgoals):
 1. length bl \<le> m \<Longrightarrow> length bl \<le> length (rev (bin_to_bl m binb))
 2. length bl \<le> m \<Longrightarrow> rbl_mult bl (take (length bl) (rev (bin_to_bl m binb))) = rbl_mult bl (rev (bin_to_bl (length bl) binb)) proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> rbl_mult bl (take (length bl) (rev (bin_to_bl m binb))) = rbl_mult bl (rev (bin_to_bl (length bl) binb)) proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> take (length bl) (rev (bin_to_bl m binb)) = rev (bin_to_bl (length bl) binb) proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> rev (take (length bl) (rev (bin_to_bl m binb))) = bin_to_bl (length bl) binb proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < m \<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))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))
theory Reversed_Bit_Lists

lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n" by (simp add: length_concat comp_def sum_list_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (concat (map (bin_to_bl n) xs)) = length xs * n
theory Reversed_Bit_Lists

lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))" apply (unfold bin_rcat_eq_foldl) apply (rule sym) apply (induct wl) apply (auto simp add: bl_to_bin_append) apply (simp add: bl_to_bin_aux_alt sclem) apply (simp add: bin_cat_foldl_lem [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl)) proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>u v. concat_bit n v u) 0 wl = bl_to_bin (concat (map (bin_to_bl n) wl)) proof (prove)
goal (1 subgoal):
 1. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl proof (prove)
goal (2 subgoals):
 1. bl_to_bin (concat (map (bin_to_bl n) [])) = foldl (\<lambda>u v. concat_bit n v u) 0 []
 2. \<And>a wl. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl \<Longrightarrow> bl_to_bin (concat (map (bin_to_bl n) (a # wl))) = foldl (\<lambda>u v. concat_bit n v u) 0 (a # wl) proof (prove)
goal (1 subgoal):
 1. \<And>a wl. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl \<Longrightarrow> bl_to_bin_aux (concat (map (bin_to_bl n) wl)) (take_bit n a) = foldl (\<lambda>u v. concat_bit n v u) (take_bit n a) wl proof (prove)
goal (1 subgoal):
 1. \<And>a wl. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl \<Longrightarrow> concat_bit (length wl * n) (foldl (\<lambda>u v. concat_bit n v u) 0 wl) (take_bit n a) = foldl (\<lambda>u v. concat_bit n v u) (take_bit n a) wl proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bin_last_bl_to_bin: "odd (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])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (bl_to_bin bs) = (bs \<noteq> [] \<and> last bs)
theory Reversed_Bit_Lists

lemma bin_rest_bl_to_bin: "bl_to_bin bs div 2 = bl_to_bin (butlast bs)" by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin bs div 2 = bl_to_bin (butlast bs)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map Not (bin_to_bl n w) = bin_to_bl n (NOT w)
theory Reversed_Bit_Lists

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)

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

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)

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

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w) proof (prove)
using this:
map2 (\<noteq>) (bin_to_bl_aux ?n ?v ?bs) (bin_to_bl_aux ?n ?w ?cs) = bin_to_bl_aux ?n (?v XOR ?w) (map2 (\<noteq>) ?bs ?cs)

goal (1 subgoal):
 1. map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)
theory Reversed_Bit_Lists

lemma to_bl_eq:
  \<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close>
  for w :: \<open>'a::len word\<close> by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w = bin_to_bl LENGTH('a) (uint w)
theory Reversed_Bit_Lists

lemma bit_of_bl_iff [bit_simps]:
  \<open>bit (of_bl bs :: 'a word) n \<longleftrightarrow> rev bs ! n \<and> n < LENGTH('a::len) \<and> n < length bs\<close> by transfer (simp add: bin_nth_of_bl ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (of_bl bs) n = (rev bs ! n \<and> n < LENGTH('a) \<and> n < length bs)
theory Reversed_Bit_Lists

lemma rev_to_bl_eq:
  \<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close>
  for w :: \<open>'a::len word\<close> apply (rule nth_equalityI) apply (simp add: to_bl.rep_eq) apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl w) = map (bit w) [0..<LENGTH('a)] proof (prove)
goal (2 subgoals):
 1. length (rev (to_bl w)) = length (map (bit w) [0..<LENGTH('a)])
 2. \<And>i. i < length (rev (to_bl w)) \<Longrightarrow> rev (to_bl w) ! i = map (bit w) [0..<LENGTH('a)] ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (rev (to_bl w)) \<Longrightarrow> rev (to_bl w) ! i = map (bit w) [0..<LENGTH('a)] ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma to_bl_eq_rev:
  \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a)])\<close>
  for w :: \<open>'a::len word\<close> using rev_to_bl_eq [of w] apply (subst rev_is_rev_conv [symmetric]) apply (simp add: rev_map) done

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

goal (1 subgoal):
 1. to_bl w = map (bit w) (rev [0..<LENGTH('a)]) proof (prove)
goal (1 subgoal):
 1. rev (to_bl w) = map (bit w) [0..<LENGTH('a)] \<Longrightarrow> rev (to_bl w) = rev (map (bit w) (rev [0..<LENGTH('a)])) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma of_bl_eq:
  \<open>of_bl bs = horner_sum of_bool 2 (rev bs)\<close> using of_bl_rev_eq [of \<open>rev bs\<close>] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl bs = horner_sum of_bool 2 (rev bs) proof (prove)
using this:
of_bl (rev (rev bs)) = horner_sum of_bool 2 (rev bs)

goal (1 subgoal):
 1. of_bl bs = horner_sum of_bool 2 (rev bs)
theory Reversed_Bit_Lists

lemma bshiftr1_eq:
  \<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close> apply (rule bit_word_eqI) apply (auto simp add: bit_simps to_bl_eq_rev nth_append rev_nth nth_butlast not_less simp flip: bit_Suc) apply (metis Suc_pred len_gt_0 less_eq_decr_length_iff not_bit_length verit_la_disequality) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b) = of_bl (b # butlast (to_bl w)) proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b)) n = bit (of_bl (b # butlast (to_bl w))) n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a); LENGTH('a) - Suc 0 \<le> n; bit w (Suc n)\<rbrakk> \<Longrightarrow> b proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma length_to_bl_eq:
  \<open>length (to_bl w) = LENGTH('a)\<close>
  for w :: \<open>'a::len word\<close> by transfer simp

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

lemma word_rotr_eq:
  \<open>word_rotr n w = of_bl (rotater n (to_bl w))\<close> apply (rule bit_word_eqI) subgoal for n apply (cases \<open>n < LENGTH('a)\<close>) apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff rotater_rev length_to_bl_eq nth_rotate rev_to_bl_eq ac_simps) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rotr n w = of_bl (rotater n (to_bl w)) proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (word_rotr n w) na = bit (of_bl (rotater n (to_bl w))) na proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> bit (word_rotr n w) n = bit (of_bl (rotater n (to_bl w))) n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr n w) n = bit (of_bl (rotater n (to_bl w))) n
 2. \<lbrakk>n < LENGTH('a); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr n w) n = bit (of_bl (rotater n (to_bl w))) n proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_rotl_eq:
  \<open>word_rotl n w = of_bl (rotate n (to_bl w))\<close> proof - have \<open>rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))\<close> by (simp add: rotater_rev') then show ?thesis apply (simp add: word_rotl_eq_word_rotr bit_of_bl_iff length_to_bl_eq rev_to_bl_eq) apply (rule bit_word_eqI) subgoal for n apply (cases \<open>n < LENGTH('a)\<close>) apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff nth_rotater) done done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w)) proof (state)
goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w)) proof (prove)
goal (1 subgoal):
 1. rotate n (to_bl w) = rev (rotater n (rev (to_bl w))) proof (state)
this:
rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))

goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w)) proof (chain)
picking this:
rotate n (to_bl w) = rev (rotater n (rev (to_bl w))) proof (prove)
using this:
rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))

goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w)) proof (prove)
goal (1 subgoal):
 1. rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])) \<Longrightarrow> word_rotr (LENGTH('a) - n mod LENGTH('a)) w = of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)]))) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) na = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) na proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) n = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); n < LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) n = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) n
 2. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); n < LENGTH('a); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) n = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) n proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals! proof (state)
this:
word_rotl n w = of_bl (rotate n (to_bl w))

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma td_bl:
  "type_definition
    (to_bl :: 'a::len word \<Rightarrow> bool list)
    of_bl
    {bl. length bl = LENGTH('a)}" apply (standard; transfer) apply (auto dest: sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. type_definition to_bl of_bl {bl. length bl = LENGTH('a)} proof (prove)
goal (3 subgoals):
 1. \<And>x. bin_to_bl LENGTH('a) x \<in> {bl. length bl = LENGTH('a)}
 2. \<And>x. take_bit LENGTH('a) (bl_to_bin (bin_to_bl LENGTH('a) x)) = take_bit LENGTH('a) x
 3. \<And>y. y \<in> {bl. length bl = LENGTH('a)} \<Longrightarrow> bin_to_bl LENGTH('a) (bl_to_bin y) = y proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_size_bl: "size w = size (to_bl w)" by (auto simp: word_size)

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

lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)" by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))
theory Reversed_Bit_Lists

lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
  for x :: "'a::len word" unfolding word_bl_Rep' by (rule len_gt_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < length (to_bl x) proof (prove)
goal (1 subgoal):
 1. 0 < LENGTH('a)
theory Reversed_Bit_Lists

lemma bl_not_Nil [iff]: "to_bl x \<noteq> []"
  for x :: "'a::len word" by (fact length_bl_gt_0 [unfolded length_greater_0_conv])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl x \<noteq> []
theory Reversed_Bit_Lists

lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
  for x :: "'a::len word" by (fact length_bl_gt_0 [THEN gr_implies_not0])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (to_bl x) \<noteq> 0
theory Reversed_Bit_Lists

lemma hd_to_bl_iff:
  \<open>hd (to_bl w) \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close>
  for w :: \<open>'a::len word\<close> by (simp add: to_bl_eq_rev hd_map hd_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hd (to_bl w) = bit w (LENGTH('a) - 1)
theory Reversed_Bit_Lists

lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)" by (simp add: hd_to_bl_iff bit_last_iff bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hd (to_bl w) = (bin_sign (sint w) = - 1)
theory Reversed_Bit_Lists

lemma of_bl_drop':
  "lend = length bl - LENGTH('a::len) \<Longrightarrow>
    of_bl (drop lend bl) = (of_bl bl :: 'a word)" by transfer (simp flip: trunc_bl2bin)

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

lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral bin = of_bl (bin_to_bl LENGTH('a) (numeral bin))
theory Reversed_Bit_Lists

lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w = bin_to_bl (size w) (uint w)
theory Reversed_Bit_Lists

lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w" by (simp add: uint_bl word_size)

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

lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len word) = bin_to_bl (LENGTH('a)) bin" by (auto simp: uint_bl word_ubin.eq_norm word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (word_of_int bin) = bin_to_bl LENGTH('a) bin
theory Reversed_Bit_Lists

lemma to_bl_numeral [simp]:
  "to_bl (numeral bin::'a::len word) =
    bin_to_bl (LENGTH('a)) (numeral bin)" unfolding word_numeral_alt by (rule to_bl_of_bin)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (numeral bin) = bin_to_bl LENGTH('a) (numeral bin) proof (prove)
goal (1 subgoal):
 1. to_bl (word_of_int (numeral bin)) = bin_to_bl LENGTH('a) (numeral bin)
theory Reversed_Bit_Lists

lemma to_bl_neg_numeral [simp]:
  "to_bl (- numeral bin::'a::len word) =
    bin_to_bl (LENGTH('a)) (- numeral bin)" unfolding word_neg_numeral_alt by (rule to_bl_of_bin)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (- numeral bin) = bin_to_bl LENGTH('a) (- numeral bin) proof (prove)
goal (1 subgoal):
 1. to_bl (word_of_int (- numeral bin)) = bin_to_bl LENGTH('a) (- numeral bin)
theory Reversed_Bit_Lists

lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w" by (simp add: uint_bl word_size)

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

lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x"
  for x :: "'a::len word" by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bin_to_bl LENGTH('a) (uint x)) = uint x
theory Reversed_Bit_Lists

lemma ucast_bl: "ucast w = of_bl (to_bl w)" by transfer simp

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

lemma ucast_down_bl:
  \<open>(ucast :: 'a::len word \<Rightarrow> 'b::len word) (of_bl bl) = of_bl bl\<close>
    if \<open>is_down (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close> using that by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast (of_bl bl) = of_bl bl proof (prove)
using this:
is_down ucast

goal (1 subgoal):
 1. ucast (of_bl bl) = of_bl bl
theory Reversed_Bit_Lists

lemma of_bl_append_same: "of_bl (X @ to_bl w) = w" by transfer (simp add: bl_to_bin_app_cat)

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

lemma ucast_of_bl_up:
  \<open>ucast (of_bl bl :: 'a::len word) = of_bl bl\<close>
  if \<open>size bl \<le> size (of_bl bl :: 'a::len word)\<close> using that apply transfer apply (rule bit_eqI) apply (auto simp add: bit_take_bit_iff) apply (subst (asm) trunc_bl2bin_len [symmetric]) apply (auto simp only: bit_take_bit_iff) done

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

goal (1 subgoal):
 1. ucast (of_bl bl) = of_bl bl proof (prove)
goal (1 subgoal):
 1. \<And>bl. length bl \<le> LENGTH('a) \<Longrightarrow> take_bit LENGTH('b) (take_bit LENGTH('a) (bl_to_bin bl)) = take_bit LENGTH('b) (bl_to_bin bl) proof (prove)
goal (1 subgoal):
 1. \<And>bl n. \<lbrakk>length bl \<le> LENGTH('a); possible_bit TYPE(int) n\<rbrakk> \<Longrightarrow> bit (take_bit LENGTH('b) (take_bit LENGTH('a) (bl_to_bin bl))) n = bit (take_bit LENGTH('b) (bl_to_bin bl)) n proof (prove)
goal (1 subgoal):
 1. \<And>bl n. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('b); bit (bl_to_bin bl) n\<rbrakk> \<Longrightarrow> n < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>bl n. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('b); bit (take_bit (length bl) (bl_to_bin bl)) n\<rbrakk> \<Longrightarrow> n < LENGTH('a) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_rev_tf:
  "to_bl (of_bl bl::'a::len word) =
    rev (takefill False (LENGTH('a)) (rev bl))" by transfer (simp add: bl_bin_bl_rtf)

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

lemma word_rep_drop:
  "to_bl (of_bl bl::'a::len word) =
    replicate (LENGTH('a) - length bl) False @
    drop (length bl - LENGTH('a)) bl" by (simp add: word_rev_tf takefill_alt rev_take)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl bl) = replicate (LENGTH('a) - length bl) False @ drop (length bl - LENGTH('a)) bl
theory Reversed_Bit_Lists

lemma to_bl_ucast:
  "to_bl (ucast (w::'b::len word) ::'a::len word) =
    replicate (LENGTH('a) - LENGTH('b)) False @
    drop (LENGTH('b) - LENGTH('a)) (to_bl w)" apply (unfold ucast_bl) apply (rule trans) apply (rule word_rep_drop) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (ucast w) = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w) proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl (to_bl w)) = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w) proof (prove)
goal (2 subgoals):
 1. to_bl (of_bl (to_bl w)) = ?s
 2. ?s = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w) proof (prove)
goal (1 subgoal):
 1. replicate (LENGTH('a) - length (to_bl w)) False @ drop (length (to_bl w) - LENGTH('a)) (to_bl w) = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma ucast_up_app:
  \<open>to_bl (ucast w :: 'b::len word) = replicate n False @ (to_bl w)\<close>
    if \<open>source_size (ucast :: 'a word \<Rightarrow> 'b word) + n = target_size (ucast :: 'a word \<Rightarrow> 'b word)\<close>
    for w :: \<open>'a::len word\<close> using that by (auto simp add : source_size target_size to_bl_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (ucast w) = replicate n False @ to_bl w proof (prove)
using this:
source_size ucast + n = target_size ucast

goal (1 subgoal):
 1. to_bl (ucast w) = replicate n False @ to_bl w
theory Reversed_Bit_Lists

lemma ucast_down_drop [OF refl]:
  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
    to_bl (uc w) = drop n (to_bl w)" by (auto simp add : source_size target_size to_bl_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = ucast; source_size uc = target_size uc + n\<rbrakk> \<Longrightarrow> to_bl (uc w) = drop n (to_bl w)