kings-crown/FVELER_Isabelle huggingface dataset:
theory Bitwise

lemma rbl_add_suc_carry_fold:
  "length xs = length ys \<Longrightarrow>
    \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) =
      (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. [])) car" apply (erule list_induct2) apply simp apply (simp only: rbl_add_carry_Cons) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) car proof (prove)
goal (2 subgoals):
 1. \<forall>car. (if car then rbl_succ else id) (rbl_add [] []) = foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip [] []) (\<lambda>_. []) car
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) = foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) car\<rbrakk> \<Longrightarrow> \<forall>car. (if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) = foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip (x # xs) (y # ys)) (\<lambda>_. []) car proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) = foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) car\<rbrakk> \<Longrightarrow> \<forall>car. (if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) = foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip (x # xs) (y # ys)) (\<lambda>_. []) car proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) = foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) car\<rbrakk> \<Longrightarrow> \<forall>car. xor3 x y car # foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) (carry x y car) = foldr (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>res car. xor3 x y car # res (carry x y car)) (zip (x # xs) (y # ys)) (\<lambda>_. []) car proof (prove)
goal:
No subgoals!
theory Bitwise

lemma to_bl_plus_carry:
  "to_bl (x + y) =
    rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
      (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)" using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"] apply (simp add: word_add_rbl[OF refl refl]) apply (drule_tac x=False in spec) apply (simp add: zip_rev) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (x + y) = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False) proof (prove)
using this:
length (rev (to_bl x)) = length (rev (to_bl y)) \<Longrightarrow> \<forall>car. (if car then rbl_succ else id) (rbl_add (rev (to_bl x)) (rev (to_bl y))) = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (rev (to_bl x)) (rev (to_bl y))) (\<lambda>_. []) car

goal (1 subgoal):
 1. to_bl (x + y) = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False) proof (prove)
goal (1 subgoal):
 1. \<forall>car. (if car then rbl_succ else id) (rbl_add (rev (to_bl x)) (rev (to_bl y))) = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (rev (to_bl x)) (rev (to_bl y))) (\<lambda>_. []) car \<Longrightarrow> rbl_add (rev (to_bl x)) (rev (to_bl y)) = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False proof (prove)
goal (1 subgoal):
 1. (if False then rbl_succ else id) (rbl_add (rev (to_bl x)) (rev (to_bl y))) = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (rev (to_bl x)) (rev (to_bl y))) (\<lambda>_. []) False \<Longrightarrow> rbl_add (rev (to_bl x)) (rev (to_bl y)) = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False proof (prove)
goal:
No subgoals!
theory Bitwise

lemma rbl_plus_simps:
  "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
  "rbl_plus cin [] ys = []"
  "rbl_plus cin xs [] = []" by (simp_all add: rbl_plus_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys &&& rbl_plus cin [] ys = [] &&& rbl_plus cin xs [] = []
theory Bitwise

lemma rbl_succ2_simps:
  "rbl_succ2 b [] = []"
  "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs" by (simp_all add: rbl_succ2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rbl_succ2 b [] = [] &&& rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs
theory Bitwise

lemma twos_complement: "- x = word_succ (not x)" using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"] by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - x = word_succ (not x) proof (prove)
using this:
x + not x - x + 1 = - 1 - x + 1

goal (1 subgoal):
 1. - x = word_succ (not x)
theory Bitwise

lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
  for x :: \<open>'a::len word\<close> by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))
theory Bitwise

lemma rbl_word_slice:
  "rev (to_bl (slice n w :: 'a::len word)) =
    takefill False (LENGTH('a)) (drop n (rev (to_bl w)))" apply (simp add: slice_take word_rev_tf rev_take) apply (cases "n < LENGTH('b)", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (slice n w)) = takefill False LENGTH('a) (drop n (rev (to_bl w))) proof (prove)
goal (1 subgoal):
 1. takefill False LENGTH('a) (drop (LENGTH('b) - (LENGTH('b) - n)) (rev (to_bl w))) = takefill False LENGTH('a) (drop n (rev (to_bl w))) proof (prove)
goal:
No subgoals!
theory Bitwise

lemma rbl_word_ucast:
  "rev (to_bl (ucast x :: 'a::len word)) = takefill False (LENGTH('a)) (rev (to_bl x))" apply (simp add: to_bl_ucast takefill_alt) apply (simp add: rev_drop) apply (cases "LENGTH('a) < LENGTH('b)") apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (ucast x)) = takefill False LENGTH('a) (rev (to_bl x)) proof (prove)
goal (1 subgoal):
 1. rev (drop (LENGTH('b) - LENGTH('a)) (to_bl x)) = take LENGTH('a) (rev (to_bl x)) proof (prove)
goal (1 subgoal):
 1. take (LENGTH('b) - (LENGTH('b) - LENGTH('a))) (rev (to_bl x)) = take LENGTH('a) (rev (to_bl x)) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> take (LENGTH('b) - (LENGTH('b) - LENGTH('a))) (rev (to_bl x)) = take LENGTH('a) (rev (to_bl x))
 2. \<not> LENGTH('a) < LENGTH('b) \<Longrightarrow> take (LENGTH('b) - (LENGTH('b) - LENGTH('a))) (rev (to_bl x)) = take LENGTH('a) (rev (to_bl x)) proof (prove)
goal:
No subgoals!
theory Bitwise

lemma rbl_shiftl:
  "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))" by (simp add: bl_shiftl takefill_alt word_size rev_drop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))
theory Bitwise

lemma rbl_shiftr:
  "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))" by (simp add: shiftr_slice rbl_word_slice word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))
theory Bitwise

lemma drop_nonempty_simps:
  "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
  "drop_nonempty v 0 (x # xs) = (x # xs)"
  "drop_nonempty v n [] = [v]" by (simp_all add: drop_nonempty_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs &&& drop_nonempty v 0 (x # xs) = x # xs &&& drop_nonempty v n [] = [v]
theory Bitwise

lemma takefill_last_simps:
  "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
  "takefill_last z 0 xs = []"
  "takefill_last z n [] = replicate n z" by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs &&& takefill_last z 0 xs = [] &&& takefill_last z n [] = replicate n z
theory Bitwise

lemma nth_word_of_int:
  "bit (word_of_int x :: 'a::len word) n = (n < LENGTH('a) \<and> bit x n)" apply (simp add: test_bit_bl word_size to_bl_of_bin) apply (subst conj_cong[OF refl], erule bin_nth_bl) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (word_of_int x) n = (n < LENGTH('a) \<and> bit x n) proof (prove)
goal (1 subgoal):
 1. (rev (bin_to_bl_aux LENGTH('a) x []) ! n \<and> n < LENGTH('a)) = (n < LENGTH('a) \<and> bit x n) proof (prove)
goal (1 subgoal):
 1. (rev (bin_to_bl_aux LENGTH('a) x []) ! n \<and> n < LENGTH('a)) = (n < LENGTH('a) \<and> rev (bin_to_bl LENGTH('a) x) ! n) proof (prove)
goal:
No subgoals!
theory Bitwise

lemma nth_scast:
  "bit (scast (x :: 'a::len word) :: 'b::len word) n =
    (n < LENGTH('b) \<and>
    (if n < LENGTH('a) - 1 then bit x n
     else bit x (LENGTH('a) - 1)))" apply transfer apply (auto simp add: bit_signed_take_bit_iff min_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (scast x) n = (n < LENGTH('b) \<and> (if n < LENGTH('a) - 1 then bit x n else bit x (LENGTH('a) - 1))) proof (prove)
goal (1 subgoal):
 1. \<And>x n. (n < LENGTH('b) \<and> bit (signed_take_bit (LENGTH('a) - Suc 0) x) n) = (n < LENGTH('b) \<and> (if n < LENGTH('a) - 1 then n < LENGTH('a) \<and> bit x n else LENGTH('a) - 1 < LENGTH('a) \<and> bit x (LENGTH('a) - 1))) proof (prove)
goal:
No subgoals!
theory Bitwise

lemma rbl_word_scast:
  "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (LENGTH('a)) (rev (to_bl x))" apply (rule nth_equalityI) apply (simp add: word_size takefill_last_def) apply (clarsimp simp: nth_scast takefill_last_def
      nth_takefill word_size rev_nth to_bl_nth) apply (cases "LENGTH('b)") apply simp apply (clarsimp simp: less_Suc_eq_le linorder_not_less
      last_rev word_msb_alt[symmetric]
      msb_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (scast x)) = takefill_last False LENGTH('a) (rev (to_bl x)) proof (prove)
goal (2 subgoals):
 1. length (rev (to_bl (scast x))) = length (takefill_last False LENGTH('a) (rev (to_bl x)))
 2. \<And>i. i < length (rev (to_bl (scast x))) \<Longrightarrow> rev (to_bl (scast x)) ! i = takefill_last False LENGTH('a) (rev (to_bl x)) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (rev (to_bl (scast x))) \<Longrightarrow> rev (to_bl (scast x)) ! i = takefill_last False LENGTH('a) (rev (to_bl x)) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < LENGTH('a) \<Longrightarrow> (i < LENGTH('b) - Suc 0 \<longrightarrow> \<not> i < LENGTH('b) \<longrightarrow> bit x i = last (rev (to_bl x))) \<and> (\<not> i < LENGTH('b) - Suc 0 \<longrightarrow> (i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = bit x i) \<and> (\<not> i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = last (rev (to_bl x)))) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < LENGTH('a); LENGTH('b) = 0\<rbrakk> \<Longrightarrow> (i < LENGTH('b) - Suc 0 \<longrightarrow> \<not> i < LENGTH('b) \<longrightarrow> bit x i = last (rev (to_bl x))) \<and> (\<not> i < LENGTH('b) - Suc 0 \<longrightarrow> (i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = bit x i) \<and> (\<not> i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = last (rev (to_bl x))))
 2. \<And>i nat. \<lbrakk>i < LENGTH('a); LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> (i < LENGTH('b) - Suc 0 \<longrightarrow> \<not> i < LENGTH('b) \<longrightarrow> bit x i = last (rev (to_bl x))) \<and> (\<not> i < LENGTH('b) - Suc 0 \<longrightarrow> (i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = bit x i) \<and> (\<not> i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = last (rev (to_bl x)))) proof (prove)
goal (1 subgoal):
 1. \<And>i nat. \<lbrakk>i < LENGTH('a); LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> (i < LENGTH('b) - Suc 0 \<longrightarrow> \<not> i < LENGTH('b) \<longrightarrow> bit x i = last (rev (to_bl x))) \<and> (\<not> i < LENGTH('b) - Suc 0 \<longrightarrow> (i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = bit x i) \<and> (\<not> i < LENGTH('b) \<longrightarrow> bit x (LENGTH('b) - Suc 0) = last (rev (to_bl x)))) proof (prove)
goal:
No subgoals!
theory Bitwise

lemma rbl_mul_simps:
  "rbl_mul (x # xs) ys = rbl_plus False (map ((\<and>) x) ys) (False # rbl_mul xs ys)"
  "rbl_mul [] ys = []" by (simp_all add: rbl_mul_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rbl_mul (x # xs) ys = rbl_plus False (map ((\<and>) x) ys) (False # rbl_mul xs ys) &&& rbl_mul [] ys = []
theory Bitwise

lemma takefill_le2: "length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs" by (simp add: takefill_alt replicate_add[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs
theory Bitwise

lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
  for x :: "'a::len word" using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y)) proof (prove)
using this:
length (rev (to_bl x)) \<le> size y \<Longrightarrow> rbl_mul (rev (to_bl x)) (rev (to_bl y)) = take (length (rev (to_bl x))) (rev (to_bl (of_bl (rev (rev (to_bl x))) * y)))

goal (1 subgoal):
 1. rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))
theory Bitwise

lemma rev_bl_order_rev_simp:
  "length xs = length ys \<Longrightarrow>
   rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))" by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rev_bl_order F (xs @ [x]) (ys @ [y]) = (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> rev_bl_order F xs ys)
theory Bitwise

lemma rev_bl_order_bl_to_bin:
  "length xs = length ys \<Longrightarrow>
    rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and>
    rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))" apply (induct xs ys rule: list_induct2) apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat concat_bit_Suc) apply (auto simp add: bl_to_bin_def add1_zle_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and> rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys)) proof (prove)
goal (2 subgoals):
 1. rev_bl_order True [] [] = (bl_to_bin (rev []) \<le> bl_to_bin (rev [])) \<and> rev_bl_order False [] [] = (bl_to_bin (rev []) < bl_to_bin (rev []))
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and> rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))\<rbrakk> \<Longrightarrow> rev_bl_order True (x # xs) (y # ys) = (bl_to_bin (rev (x # xs)) \<le> bl_to_bin (rev (y # ys))) \<and> rev_bl_order False (x # xs) (y # ys) = (bl_to_bin (rev (x # xs)) < bl_to_bin (rev (y # ys))) proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and> rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))\<rbrakk> \<Longrightarrow> rev_bl_order (y \<and> \<not> x \<or> y \<or> \<not> x) xs ys = (bl_to_bin [x] mod 2 + 2 * bl_to_bin (rev xs) \<le> bl_to_bin [y] mod 2 + 2 * bl_to_bin (rev ys)) \<and> rev_bl_order (y \<and> \<not> x) xs ys = (bl_to_bin [x] mod 2 + 2 * bl_to_bin (rev xs) < bl_to_bin [y] mod 2 + 2 * bl_to_bin (rev ys)) proof (prove)
goal:
No subgoals!
theory Bitwise

lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
  for x y :: "'a::len word" by (simp add: rev_bl_order_bl_to_bin word_le_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))
theory Bitwise

lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
  for x y :: "'a::len word" by (simp add: word_less_alt rev_bl_order_bl_to_bin)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))
theory Bitwise

lemma map_last_simps:
  "map_last f [] = []"
  "map_last f [x] = [f x]"
  "map_last f (x # y # zs) = x # map_last f (y # zs)" by (simp_all add: map_last_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_last f [] = [] &&& map_last f [x] = [f x] &&& map_last f (x # y # zs) = x # map_last f (y # zs)
theory Bitwise

lemma rev_bin_to_bl_simps:
  "rev (bin_to_bl 0 x) = []"
  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))"
  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))"
  "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False"
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))"
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) =
    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
  "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
    False # rev (bin_to_bl n (- numeral (nm + num.One)))"
  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
    False # rev (bin_to_bl n (- numeral num.One))" by (simp_all add: bin_to_bl_aux_append bin_to_bl_zero_aux bin_to_bl_minus1_aux replicate_append_same)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rev (bin_to_bl 0 x) = [] &&& rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))) &&& rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm)) &&& rev (bin_to_bl (Suc n) Numeral1) = True # replicate n False &&& rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))) &&& (rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (- numeral (nm + num.One))) &&& rev (bin_to_bl (Suc n) (- Numeral1)) = True # replicate n True) &&& rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) = True # rev (bin_to_bl n (- numeral (nm + num.One))) &&& rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) = False # rev (bin_to_bl n (- numeral (nm + num.One))) &&& rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) = False # rev (bin_to_bl n (- Numeral1))
theory Bitwise

lemma to_bl_upt: "to_bl x = rev (map (bit x) [0 ..< size x])" by (simp add: to_bl_eq_rev word_size rev_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl x = rev (map (bit x) [0..<size x])
theory Bitwise

lemma upt_eq_list_intros:
  "j \<le> i \<Longrightarrow> [i ..< j] = []"
  "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)" by (simp_all add: upt_eq_Cons_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (j \<le> i \<Longrightarrow> [i..<j] = []) &&& (\<lbrakk>i = x; x < j; [x + 1..<j] = xs\<rbrakk> \<Longrightarrow> [i..<j] = x # xs)
theory Bitwise

lemma if_bool_simps:
  "If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and>
    If p y True = (p \<longrightarrow> y) \<and> If p y False = (p \<and> y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if p then True else y) = (p \<or> y) \<and> (if p then False else y) = (\<not> p \<and> y) \<and> (if p then y else True) = (p \<longrightarrow> y) \<and> (if p then y else False) = (p \<and> y)
theory Signed_Words

lemma card_signed [simp]: "CARD (('a::len0) signed) = CARD('a)" unfolding type_definition.card [OF type_definition_signed] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. CARD('a signed) = CARD('a) proof (prove)
goal (1 subgoal):
 1. CARD('a) = CARD('a)
theory Signed_Words

lemma scast_scast_id [simp]:
  "scast (scast x :: ('a::len) signed word) = (x :: 'a word)"
  "scast (scast y :: ('a::len) word) = (y :: 'a signed word)" by (auto simp: is_up scast_up_scast_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast (scast x) = x &&& scast (scast y) = y
theory Signed_Words

lemma ucast_scast_id [simp]:
  "ucast (scast (x :: 'a::len signed word) :: 'a word) = x" by transfer (simp add: take_bit_signed_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast (scast x) = x
theory Signed_Words

lemma scast_of_nat [simp]:
  "scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)" by transfer (simp add: take_bit_signed_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast (word_of_nat x) = word_of_nat x
theory Signed_Words

lemma scast_ucast_id [simp]:
  "scast (ucast (x :: 'a::len word) :: 'a signed word) = x" by transfer (simp add: take_bit_signed_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast (ucast x) = x
theory Signed_Words

lemma scast_eq_scast_id [simp]:
  "((scast (a :: 'a::len signed word) :: 'a word) = scast b) = (a = b)" by (metis ucast_scast_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (scast a = scast b) = (a = b)
theory Signed_Words

lemma ucast_eq_ucast_id [simp]:
  "((ucast (a :: 'a::len word) :: 'a signed word) = ucast b) = (a = b)" by (metis scast_ucast_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ucast a = ucast b) = (a = b)
theory Signed_Words

lemma scast_ucast_norm [simp]:
  "(ucast (a :: 'a::len word) = (b :: 'a signed word)) = (a = scast b)"
  "((b :: 'a signed word) = ucast (a :: 'a::len word)) = (a = scast b)" by (metis scast_ucast_id ucast_scast_id)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ucast a = b) = (a = scast b) &&& (b = ucast a) = (a = scast b)
theory Signed_Words

lemma scast_2_power [simp]: "scast ((2 :: 'a::len signed word) ^ x) = ((2 :: 'a word) ^ x)" by (rule bit_word_eqI) (auto simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast (2 ^ x) = 2 ^ x
theory Signed_Words

lemma ucast_nat_def':
  "of_nat (unat x) = (ucast :: 'a :: len word \<Rightarrow> ('b :: len) signed word) x" by (fact of_nat_unat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat (unat x) = ucast x
theory Signed_Words

lemma zero_sle_ucast_up:
  "\<not> is_down (ucast :: 'a word \<Rightarrow> 'b signed word) \<Longrightarrow>
          (0 <=s ((ucast (b::('a::len) word)) :: ('b::len) signed word))" by transfer (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_down ucast \<Longrightarrow> 0 \<le>s ucast b