kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

lemma word_split_bl':
  "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))" apply (simp add: word_split_def) apply transfer apply (cases \<open>LENGTH('b) \<le> LENGTH('a)\<close>) apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>] min_absorb2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>std = size c - size b; word_split c = (a, b)\<rbrakk> \<Longrightarrow> a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>std = size c - size b; ucast (drop_bit LENGTH('b) c) = a \<and> ucast c = b\<rbrakk> \<Longrightarrow> a = of_bl (take (size c - size b) (to_bl c)) \<and> b = of_bl (drop (size c - size b) (to_bl c)) proof (prove)
goal (1 subgoal):
 1. \<And>std c b a. \<lbrakk>std = LENGTH('a) - LENGTH('b); take_bit LENGTH('c) (take_bit LENGTH('a) ((drop_bit LENGTH('b) \<circ> take_bit LENGTH('a)) c)) = take_bit LENGTH('c) a \<and> take_bit LENGTH('b) (take_bit LENGTH('a) c) = take_bit LENGTH('b) b\<rbrakk> \<Longrightarrow> take_bit LENGTH('c) a = take_bit LENGTH('c) (bl_to_bin (take (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) \<and> take_bit LENGTH('b) b = take_bit LENGTH('b) (bl_to_bin (drop (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) proof (prove)
goal (2 subgoals):
 1. \<And>std c b a. \<lbrakk>std = LENGTH('a) - LENGTH('b); take_bit LENGTH('c) (take_bit LENGTH('a) ((drop_bit LENGTH('b) \<circ> take_bit LENGTH('a)) c)) = take_bit LENGTH('c) a \<and> take_bit LENGTH('b) (take_bit LENGTH('a) c) = take_bit LENGTH('b) b; LENGTH('b) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('c) a = take_bit LENGTH('c) (bl_to_bin (take (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) \<and> take_bit LENGTH('b) b = take_bit LENGTH('b) (bl_to_bin (drop (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c)))
 2. \<And>std c b a. \<lbrakk>std = LENGTH('a) - LENGTH('b); take_bit LENGTH('c) (take_bit LENGTH('a) ((drop_bit LENGTH('b) \<circ> take_bit LENGTH('a)) c)) = take_bit LENGTH('c) a \<and> take_bit LENGTH('b) (take_bit LENGTH('a) c) = take_bit LENGTH('b) b; \<not> LENGTH('b) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('c) a = take_bit LENGTH('c) (bl_to_bin (take (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) \<and> take_bit LENGTH('b) b = take_bit LENGTH('b) (bl_to_bin (drop (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_split_bl: "std = size c - size b \<Longrightarrow>
    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
    word_split c = (a, b)" apply (rule iffI) defer apply (erule (1) word_split_bl') apply (case_tac "word_split c") apply (auto simp add: word_size) apply (frule word_split_bl' [rotated]) apply (auto simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. std = size c - size b \<Longrightarrow> (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) = (word_split c = (a, b)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (a, b)
 2. \<lbrakk>std = size c - size b; word_split c = (a, b)\<rbrakk> \<Longrightarrow> a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>std = size c - size b; word_split c = (a, b)\<rbrakk> \<Longrightarrow> a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))
 2. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)); word_split c = (aa, ba)\<rbrakk> \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>std = LENGTH('a) - LENGTH('b); word_split c = (aa, ba); a = of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)); b = of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)), of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c))) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>std = LENGTH('a) - LENGTH('b); word_split c = (aa, ba); a = of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)); b = of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c))\<rbrakk> \<Longrightarrow> ?std8 aa ba = size c - size ba
 2. \<And>aa ba. \<lbrakk>std = LENGTH('a) - LENGTH('b); word_split c = (aa, ba); a = of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)); b = of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c)); aa = of_bl (take (?std8 aa ba) (to_bl c)) \<and> ba = of_bl (drop (?std8 aa ba) (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)), of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c))) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_split_bl_eq:
  "(word_split c :: ('c::len word \<times> 'd::len word)) =
    (of_bl (take (LENGTH('a::len) - LENGTH('d::len)) (to_bl c)),
     of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))"
  for c :: "'a::len word" apply (rule word_split_bl [THEN iffD1]) apply (unfold word_size) apply (rule refl conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_split c = (of_bl (take (LENGTH('a) - LENGTH('d)) (to_bl c)), of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c))) proof (prove)
goal (2 subgoals):
 1. ?std1 = size c - size (of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))
 2. of_bl (take (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (take ?std1 (to_bl c)) \<and> of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (drop ?std1 (to_bl c)) proof (prove)
goal (2 subgoals):
 1. ?std1 = LENGTH('a) - LENGTH('d)
 2. of_bl (take (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (take ?std1 (to_bl c)) \<and> of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (drop ?std1 (to_bl c)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_rcat_bl:
  \<open>word_rcat wl = of_bl (concat (map to_bl wl))\<close> proof - define ws where \<open>ws = rev wl\<close> moreover have \<open>word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))\<close> apply (simp add: word_rcat_def of_bl_eq rev_concat rev_map comp_def rev_to_bl_eq flip: horner_sum_of_bool_2_concat) apply transfer apply simp done ultimately show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl)) proof (state)
goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl)) proof (state)
this:
ws = rev wl

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl)) proof (state)
this:
ws = rev wl

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl)) proof (prove)
goal (1 subgoal):
 1. word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws))) proof (prove)
goal (1 subgoal):
 1. word_of_int (horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('b)]) ws))) = horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('b)]) ws)) proof (prove)
goal (1 subgoal):
 1. \<And>ws. take_bit LENGTH('c) (horner_sum of_bool 2 (concat (map (\<lambda>x. map (\<lambda>n. n < LENGTH('b) \<and> bit x n) [0..<LENGTH('b)]) ws))) = take_bit LENGTH('c) (horner_sum of_bool 2 (concat (map (\<lambda>x. map (\<lambda>n. n < LENGTH('b) \<and> bit x n) [0..<LENGTH('b)]) ws))) proof (prove)
goal:
No subgoals! proof (state)
this:
word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl)) proof (chain)
picking this:
ws = rev wl
word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws))) proof (prove)
using this:
ws = rev wl
word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl)) proof (state)
this:
word_rcat wl = of_bl (concat (map to_bl wl))

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0"
  for x :: "'a::comm_monoid_add" by (induct xs arbitrary: x) (auto simp: add.assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (+) x xs = foldr (+) (x # xs) (0::'a)
theory Reversed_Bit_Lists

lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)" by (simp add: word_rotl_eq to_bl_use_of_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (word_rotl n w) = rotate n (to_bl w)
theory Reversed_Bit_Lists

lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)" by (simp add: word_rotr_eq to_bl_use_of_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (word_rotr n w) = rotater n (to_bl w)
theory Reversed_Bit_Lists

lemma max_word_bl: "to_bl (- 1::'a::len word) = replicate LENGTH('a) True" by (fact to_bl_n1)

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

lemma to_bl_mask:
  "to_bl (mask n :: 'a::len word) =
  replicate (LENGTH('a) - n) False @
    replicate (min (LENGTH('a)) n) True" by (simp add: mask_bl word_rep_drop min_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (mask n) = replicate (LENGTH('a) - n) False @ replicate (min LENGTH('a) n) True
theory Reversed_Bit_Lists

lemma map_replicate_True:
  "n = length xs \<Longrightarrow>
    map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs" by (induct xs arbitrary: n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> map2 (\<and>) xs (replicate n True) = xs
theory Reversed_Bit_Lists

lemma map_replicate_False:
  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
    (zip xs (replicate n False)) = replicate n False" by (induct xs arbitrary: n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> map2 (\<and>) xs (replicate n False) = replicate n False
theory Reversed_Bit_Lists

lemma bl_and_mask:
  fixes w :: "'a::len word"
    and n :: nat
  defines "n' \<equiv> LENGTH('a) - n"
  shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)" proof - note [simp] = map_replicate_True map_replicate_False have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))" by (simp add: bl_word_and) also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) =
      replicate n' False @ drop n' (to_bl w)" unfolding to_bl_mask n'_def by (subst zip_append) auto finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (state)
goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (state)
this:
?n = length ?xs \<Longrightarrow> map2 (\<and>) ?xs (replicate ?n True) = ?xs
?n = length ?xs \<Longrightarrow> map2 (\<and>) ?xs (replicate ?n False) = replicate ?n False

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (prove)
goal (1 subgoal):
 1. to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n)) proof (state)
this:
to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n))

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (state)
this:
to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n))

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (prove)
goal (1 subgoal):
 1. to_bl w = take n' (to_bl w) @ drop n' (to_bl w) proof (state)
this:
to_bl w = take n' (to_bl w) @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (state)
this:
to_bl w = take n' (to_bl w) @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (prove)
goal (1 subgoal):
 1. map2 (\<and>) (take n' (to_bl w) @ drop n' (to_bl w)) (to_bl (mask n)) = replicate n' False @ drop n' (to_bl w) proof (prove)
goal (1 subgoal):
 1. map2 (\<and>) (take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl w)) (replicate (LENGTH('a) - n) False @ replicate (min LENGTH('a) n) True) = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w) proof (state)
this:
map2 (\<and>) (take n' (to_bl w) @ drop n' (to_bl w)) (to_bl (mask n)) = replicate n' False @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (chain)
picking this:
to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (prove)
using this:
to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w) proof (state)
this:
to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma drop_rev_takefill:
  "length xs \<le> n \<Longrightarrow>
    drop (n - length xs) (rev (takefill False n (rev xs))) = xs" by (simp add: takefill_alt rev_take)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> n \<Longrightarrow> drop (n - length xs) (rev (takefill False n (rev xs))) = xs
theory Reversed_Bit_Lists

lemma uint_of_bl_is_bl_to_bin_drop:
  "length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> uint (of_bl l :: 'a::len word) = bl_to_bin l" apply transfer apply (simp add: take_bit_eq_mod) apply (rule Divides.mod_less) apply (rule bl_to_bin_ge0) using bl_to_bin_lt2p_drop apply (rule order.strict_trans2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> uint (of_bl l) = bl_to_bin l proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> take_bit LENGTH('a) (bl_to_bin l) = bl_to_bin l proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l mod 2 ^ LENGTH('a) = bl_to_bin l proof (prove)
goal (2 subgoals):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> 0 \<le> bl_to_bin l
 2. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l < 2 ^ LENGTH('a) proof (prove)
using this:
bl_to_bin ?bs < 2 ^ length (dropWhile Not ?bs)

goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> 2 ^ length (dropWhile Not l) \<le> 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bin_to_bl_or:
  "bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b)" using bl_or_aux_bin[where n=n and v=a and w=b and bs="[]" and cs="[]"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b) proof (prove)
using this:
map2 (\<or>) (bin_to_bl_aux n a []) (bin_to_bl_aux n b []) = bin_to_bl_aux n (a OR b) (map2 (\<or>) [] [])

goal (1 subgoal):
 1. bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b)
theory Reversed_Bit_Lists

lemma word_and_1_bl:
  fixes x::"'a::len word"
  shows "(x AND 1) = of_bl [bit x 0]" by (simp add: word_and_1)

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

lemma word_1_and_bl:
  fixes x::"'a::len word"
  shows "(1 AND x) = of_bl [bit x 0]" using word_and_1_bl [of x] by (simp add: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 AND x = of_bl [bit x 0] proof (prove)
using this:
x AND 1 = of_bl [bit x 0]

goal (1 subgoal):
 1. 1 AND x = of_bl [bit x 0]
theory Reversed_Bit_Lists

lemma of_bl_drop:
  "of_bl (drop n xs) = (of_bl xs AND mask (length xs - n))" apply (rule bit_word_eqI) apply (auto simp: rev_nth bit_simps cong: rev_conj_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (drop n xs) = of_bl xs AND mask (length xs - n) proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl (drop n xs)) na = bit (of_bl xs AND mask (length xs - n)) na proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma to_bl_1:
  "to_bl (1::'a::len word) = replicate (LENGTH('a) - 1) False @ [True]" by (rule nth_equalityI) (auto simp add: to_bl_unfold nth_append rev_nth bit_1_iff not_less not_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl 1 = replicate (LENGTH('a) - 1) False @ [True]
theory Reversed_Bit_Lists

lemma eq_zero_set_bl:
  "(w = 0) = (True \<notin> set (to_bl w))" apply (auto simp add: to_bl_unfold) apply (rule bit_word_eqI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w = 0) = (True \<notin> set (to_bl w)) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..<LENGTH('a)}. \<not> bit w x \<Longrightarrow> w = 0 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>{0..<LENGTH('a)}. \<not> bit w x; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit w n = bit 0 n proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma of_drop_to_bl:
  "of_bl (drop n (to_bl x)) = (x AND mask (size x - n))" by (simp add: of_bl_drop word_size_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (drop n (to_bl x)) = x AND mask (size x - n)
theory Reversed_Bit_Lists

lemma word_msb_alt: "msb w \<longleftrightarrow> hd (to_bl w)"
  for w :: "'a::len word" apply (simp add: msb_word_eq) apply (subst hd_conv_nth) apply simp apply (subst nth_to_bl) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb w = hd (to_bl w) proof (prove)
goal (1 subgoal):
 1. bit w (LENGTH('a) - Suc 0) = hd (to_bl w) proof (prove)
goal (2 subgoals):
 1. to_bl w \<noteq> []
 2. bit w (LENGTH('a) - Suc 0) = to_bl w ! 0 proof (prove)
goal (1 subgoal):
 1. bit w (LENGTH('a) - Suc 0) = to_bl w ! 0 proof (prove)
goal (2 subgoals):
 1. 0 < LENGTH('a)
 2. bit w (LENGTH('a) - Suc 0) = bit w (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. bit w (LENGTH('a) - Suc 0) = bit w (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma word_lsb_last:
  \<open>lsb w \<longleftrightarrow> last (to_bl w)\<close>
  for w :: \<open>'a::len word\<close> using nth_to_bl [of \<open>LENGTH('a) - Suc 0\<close> w] by (simp add: last_conv_nth bit_0 lsb_odd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lsb w = last (to_bl w) proof (prove)
using this:
LENGTH('a) - Suc 0 < LENGTH('a) \<Longrightarrow> to_bl w ! (LENGTH('a) - Suc 0) = bit w (LENGTH('a) - Suc (LENGTH('a) - Suc 0))

goal (1 subgoal):
 1. lsb w = last (to_bl w)
theory Reversed_Bit_Lists

lemma is_aligned_replicate:
  fixes w::"'a::len word"
  assumes aligned: "is_aligned w n"
  and          nv: "n \<le> LENGTH('a)"
  shows   "to_bl w = (take (LENGTH('a) - n) (to_bl w)) @ replicate n False" apply (rule nth_equalityI) using assms apply (simp_all add: nth_append not_less word_size to_bl_nth is_aligned_imp_not_bit) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False proof (prove)
goal (2 subgoals):
 1. length (to_bl w) = length (take (LENGTH('a) - n) (to_bl w) @ replicate n False)
 2. \<And>i. i < length (to_bl w) \<Longrightarrow> to_bl w ! i = (take (LENGTH('a) - n) (to_bl w) @ replicate n False) ! i proof (prove)
using this:
is_aligned w n
n \<le> LENGTH('a)

goal (2 subgoals):
 1. length (to_bl w) = length (take (LENGTH('a) - n) (to_bl w) @ replicate n False)
 2. \<And>i. i < length (to_bl w) \<Longrightarrow> to_bl w ! i = (take (LENGTH('a) - n) (to_bl w) @ replicate n False) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma is_aligned_drop:
  fixes w::"'a::len word"
  assumes "is_aligned w n" "n \<le> LENGTH('a)"
  shows "drop (LENGTH('a) - n) (to_bl w) = replicate n False" proof - have "to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False" by (rule is_aligned_replicate) fact+ then have "drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) \<dots>" by simp also have "\<dots> = replicate n False" by simp finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (state)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (prove)
goal (1 subgoal):
 1. to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False proof (state)
this:
to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (chain)
picking this:
to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False proof (prove)
using this:
to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False) proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False)

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False)

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (prove)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False) = replicate n False proof (state)
this:
drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False) = replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (chain)
picking this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (prove)
using this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma less_is_drop_replicate:
  fixes x::"'a::len word"
  assumes lt: "x < 2 ^ n"
  shows   "to_bl x = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl x)" by (metis assms bl_and_mask' less_mask_eq)

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

lemma is_aligned_replicateI:
  "to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned (p::'a::len word) n" apply (simp add: is_aligned_to_bl word_size) apply (subgoal_tac "length addr = LENGTH('a) - n") apply (simp add: replicate_not_True) apply (drule arg_cong [where f=length]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned p n proof (prove)
goal (1 subgoal):
 1. to_bl p = addr @ replicate n False \<Longrightarrow> True \<notin> set (drop (LENGTH('a) - n) addr) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>to_bl p = addr @ replicate n False; length addr = LENGTH('a) - n\<rbrakk> \<Longrightarrow> True \<notin> set (drop (LENGTH('a) - n) addr)
 2. to_bl p = addr @ replicate n False \<Longrightarrow> length addr = LENGTH('a) - n proof (prove)
goal (1 subgoal):
 1. to_bl p = addr @ replicate n False \<Longrightarrow> length addr = LENGTH('a) - n proof (prove)
goal (1 subgoal):
 1. length (to_bl p) = length (addr @ replicate n False) \<Longrightarrow> length addr = LENGTH('a) - n proof (prove)
goal:
No subgoals!