kings-crown/FVELER_Isabelle huggingface dataset:
theory Bits_Int

lemma bin_rsplit_rcat [rule_format]:
  "n > 0 \<longrightarrow> bin_rsplit n (n * size ws, bin_rcat n ws) = map ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n) ws" apply (unfold bin_rsplit_def bin_rcat_eq_foldl) apply (rule_tac xs = ws in rev_induct) apply clarsimp apply clarsimp apply (subst rsplit_aux_alts) apply (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> bin_rsplit n (n * length ws, bin_rcat n ws) = map (take_bit n) ws proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> bin_rsplit_aux n (fst (n * length ws, foldl (\<lambda>u v. concat_bit n v u) 0 ws)) (snd (n * length ws, foldl (\<lambda>u v. concat_bit n v u) 0 ws)) [] = map (take_bit n) ws proof (prove)
goal (2 subgoals):
 1. 0 < n \<longrightarrow> bin_rsplit_aux n (fst (n * length [], foldl (\<lambda>u v. concat_bit n v u) 0 [])) (snd (n * length [], foldl (\<lambda>u v. concat_bit n v u) 0 [])) [] = map (take_bit n) []
 2. \<And>x xs. 0 < n \<longrightarrow> bin_rsplit_aux n (fst (n * length xs, foldl (\<lambda>u v. concat_bit n v u) 0 xs)) (snd (n * length xs, foldl (\<lambda>u v. concat_bit n v u) 0 xs)) [] = map (take_bit n) xs \<Longrightarrow> 0 < n \<longrightarrow> bin_rsplit_aux n (fst (n * length (xs @ [x]), foldl (\<lambda>u v. concat_bit n v u) 0 (xs @ [x]))) (snd (n * length (xs @ [x]), foldl (\<lambda>u v. concat_bit n v u) 0 (xs @ [x]))) [] = map (take_bit n) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. 0 < n \<longrightarrow> bin_rsplit_aux n (fst (n * length xs, foldl (\<lambda>u v. concat_bit n v u) 0 xs)) (snd (n * length xs, foldl (\<lambda>u v. concat_bit n v u) 0 xs)) [] = map (take_bit n) xs \<Longrightarrow> 0 < n \<longrightarrow> bin_rsplit_aux n (fst (n * length (xs @ [x]), foldl (\<lambda>u v. concat_bit n v u) 0 (xs @ [x]))) (snd (n * length (xs @ [x]), foldl (\<lambda>u v. concat_bit n v u) 0 (xs @ [x]))) [] = map (take_bit n) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>0 < n; bin_rsplit_aux n (n * length xs) (foldl (\<lambda>u v. concat_bit n v u) 0 xs) [] = map (take_bit n) xs\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (n * length xs) (drop_bit n (concat_bit n x (foldl (\<lambda>u v. concat_bit n v u) 0 xs))) [take_bit n x] = map (take_bit n) xs @ [take_bit n x] proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>0 < n; bin_rsplit_aux n (n * length xs) (foldl (\<lambda>u v. concat_bit n v u) 0 xs) [] = map (take_bit n) xs\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (n * length xs) (drop_bit n (concat_bit n x (foldl (\<lambda>u v. concat_bit n v u) 0 xs))) [] @ [take_bit n x] = map (take_bit n) xs @ [take_bit n x] proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_rsplit_len_le: "n \<noteq> 0 \<longrightarrow> ws = bin_rsplit n (nw, w) \<longrightarrow> length ws \<le> m \<longleftrightarrow> nw \<le> m * n" by (auto simp: bin_rsplit_def bin_rsplit_aux_len_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit n (nw, w) \<longrightarrow> (length ws \<le> m) = (nw \<le> m * n)
theory Bits_Int

lemma bin_rsplit_aux_len:
  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) = (nw + n - 1) div n + length cs" apply (induct n nw w cs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) apply (clarsimp simp: Let_def split: prod.split) apply (erule thin_rl) apply (case_tac m) apply simp apply (case_tac "m \<le> n") apply (auto simp add: div_add_self2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) = (nw + n - 1) div n + length cs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. \<lbrakk>\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x; n \<noteq> 0\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) xa (y # bs)) = (m - n + n - 1) div n + length (y # bs); n \<noteq> 0\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n m c bs) = (m + n - 1) div n + length bs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. \<lbrakk>\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x; n \<noteq> 0\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) xa (y # bs)) = (m - n + n - 1) div n + length (y # bs); n \<noteq> 0\<rbrakk> \<Longrightarrow> length (if m = 0 \<or> n = 0 then bs else let (a, b) = bin_split n c in bin_rsplit_aux n (m - n) a (b # bs)) = (m + n - 1) div n + length bs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. \<lbrakk>\<And>a xa. \<lbrakk>a = drop_bit n c; xa = drop_bit n c\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) (drop_bit n c) (take_bit n c # bs)) = Suc ((m - n + n - Suc 0) div n + length bs); 0 < n; 0 < m\<rbrakk> \<Longrightarrow> Suc ((m - n + n - Suc 0) div n) = (m + n - Suc 0) div n proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. \<lbrakk>0 < n; 0 < m\<rbrakk> \<Longrightarrow> Suc ((m - n + n - Suc 0) div n) = (m + n - Suc 0) div n proof (prove)
goal (2 subgoals):
 1. \<And>n m c bs. \<lbrakk>0 < n; 0 < m; m = 0\<rbrakk> \<Longrightarrow> Suc ((m - n + n - Suc 0) div n) = (m + n - Suc 0) div n
 2. \<And>n m c bs nat. \<lbrakk>0 < n; 0 < m; m = Suc nat\<rbrakk> \<Longrightarrow> Suc ((m - n + n - Suc 0) div n) = (m + n - Suc 0) div n proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs nat. \<lbrakk>0 < n; 0 < m; m = Suc nat\<rbrakk> \<Longrightarrow> Suc ((m - n + n - Suc 0) div n) = (m + n - Suc 0) div n proof (prove)
goal (2 subgoals):
 1. \<And>n m c bs nat. \<lbrakk>0 < n; 0 < m; m = Suc nat; m \<le> n\<rbrakk> \<Longrightarrow> Suc ((m - n + n - Suc 0) div n) = (m + n - Suc 0) div n
 2. \<And>n m c bs nat. \<lbrakk>0 < n; 0 < m; m = Suc nat; \<not> m \<le> n\<rbrakk> \<Longrightarrow> Suc ((m - n + n - Suc 0) div n) = (m + n - Suc 0) div n proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_rsplit_len: "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" by (auto simp: bin_rsplit_def bin_rsplit_aux_len)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n
theory Bits_Int

lemma bin_rsplit_len_indep:
  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" apply (unfold bin_rsplit_def) apply (simp (no_asm)) apply (erule bin_rsplit_aux_len_indep) apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w)) proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n (fst (nw, v)) (snd (nw, v)) []) = length (bin_rsplit_aux n (fst (nw, w)) (snd (nw, w)) []) proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw v []) = length (bin_rsplit_aux n nw w []) proof (prove)
goal (1 subgoal):
 1. length [] = length [] proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_sc_0 [simp]:
  "bin_sc 0 b w = of_bool b + 2 * (\<lambda>k::int. k div 2) w" by (simp add: set_bit_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit w 0 b = of_bool b + 2 * (w div 2)
theory Bits_Int

lemma bin_sc_Suc [simp]:
  "bin_sc (Suc n) b w = of_bool (odd w) + 2 * bin_sc n b (w div 2)" by (simp add: set_bit_int_def set_bit_Suc unset_bit_Suc bin_last_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit w (Suc n) b = of_bool (odd w) + 2 * set_bit_class.set_bit (w div 2) n b
theory Bits_Int

lemma bin_nth_sc [bit_simps]: "bit (bin_sc n b w) n \<longleftrightarrow> b" by (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bit_class.set_bit w n b) n = b
theory Bits_Int

lemma bin_sc_sc_same [simp]: "bin_sc n c (bin_sc n b w) = bin_sc n c w" by (induction n arbitrary: w) (simp_all add: bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (set_bit_class.set_bit w n b) n c = set_bit_class.set_bit w n c
theory Bits_Int

lemma bin_sc_sc_diff: "m \<noteq> n \<Longrightarrow> bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" apply (induct n arbitrary: w m) apply (case_tac [!] m) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w n b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) n b proof (prove)
goal (2 subgoals):
 1. \<And>w m. m \<noteq> 0 \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w 0 b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) 0 b
 2. \<And>n w m. \<lbrakk>\<And>w m. m \<noteq> n \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w n b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) n b; m \<noteq> Suc n\<rbrakk> \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w (Suc n) b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) (Suc n) b proof (prove)
goal (4 subgoals):
 1. \<And>w m. \<lbrakk>m \<noteq> 0; m = 0\<rbrakk> \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w 0 b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) 0 b
 2. \<And>w m nat. \<lbrakk>m \<noteq> 0; m = Suc nat\<rbrakk> \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w 0 b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) 0 b
 3. \<And>n w m. \<lbrakk>\<And>w m. m \<noteq> n \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w n b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) n b; m \<noteq> Suc n; m = 0\<rbrakk> \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w (Suc n) b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) (Suc n) b
 4. \<And>n w m nat. \<lbrakk>\<And>w m. m \<noteq> n \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w n b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) n b; m \<noteq> Suc n; m = Suc nat\<rbrakk> \<Longrightarrow> set_bit_class.set_bit (set_bit_class.set_bit w (Suc n) b) m c = set_bit_class.set_bit (set_bit_class.set_bit w m c) (Suc n) b proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_nth_sc_gen: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (bin_sc n b w) m = (if m = n then b else (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w m)" by (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bit_class.set_bit w n b) m = (if m = n then b else bit w m)
theory Bits_Int

lemma bin_sc_eq:
  \<open>bin_sc n False = unset_bit n\<close>
  \<open>bin_sc n True = Bit_Operations.set_bit n\<close> apply (simp_all add: fun_eq_iff bit_eq_iff) apply (simp_all add: bit_simps bin_nth_sc_gen) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. set_bit_class.set_bit i n False) = unset_bit n &&& (\<lambda>i. set_bit_class.set_bit i n True) = semiring_bit_operations_class.set_bit n proof (prove)
goal (2 subgoals):
 1. \<forall>x na. bit (set_bit_class.set_bit x n False) na = bit (unset_bit n x) na
 2. \<forall>x na. bit (set_bit_class.set_bit x n True) na = bit (semiring_bit_operations_class.set_bit n x) na proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_sc_nth [simp]: "bin_sc n ((bit :: int \<Rightarrow> nat \<Rightarrow> bool) w n) w = w" by (rule bit_eqI) (simp add: bin_nth_sc_gen)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit w n (bit w n) = w
theory Bits_Int

lemma bin_sc_bintr [simp]:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m (bin_sc n x ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w)) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m (bin_sc n x w)" apply (rule bit_eqI) apply (cases x) apply (auto simp add: bit_simps bin_sc_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit m (set_bit_class.set_bit (take_bit m w) n x) = take_bit m (set_bit_class.set_bit w n x) proof (prove)
goal (1 subgoal):
 1. \<And>na. possible_bit TYPE(int) na \<Longrightarrow> bit (take_bit m (set_bit_class.set_bit (take_bit m w) n x)) na = bit (take_bit m (set_bit_class.set_bit w n x)) na proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>possible_bit TYPE(int) na; x\<rbrakk> \<Longrightarrow> bit (take_bit m (set_bit_class.set_bit (take_bit m w) n x)) na = bit (take_bit m (set_bit_class.set_bit w n x)) na
 2. \<And>na. \<lbrakk>possible_bit TYPE(int) na; \<not> x\<rbrakk> \<Longrightarrow> bit (take_bit m (set_bit_class.set_bit (take_bit m w) n x)) na = bit (take_bit m (set_bit_class.set_bit w n x)) na proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_clr_le: "bin_sc n False w \<le> w" by (simp add: set_bit_int_def unset_bit_less_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit w n False \<le> w
theory Bits_Int

lemma bin_set_ge: "bin_sc n True w \<ge> w" by (simp add: set_bit_int_def set_bit_greater_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<le> set_bit_class.set_bit w n True
theory Bits_Int

lemma bintr_bin_clr_le: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (bin_sc m False w) \<le> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (simp add: set_bit_int_def take_bit_unset_bit_eq unset_bit_less_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n (set_bit_class.set_bit w m False) \<le> take_bit n w
theory Bits_Int

lemma bintr_bin_set_ge: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (bin_sc m True w) \<ge> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (simp add: set_bit_int_def take_bit_set_bit_eq set_bit_greater_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n w \<le> take_bit n (set_bit_class.set_bit w m True)
theory Bits_Int

lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0" by (induct n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 0 n False = 0
theory Bits_Int

lemma bin_sc_minus: "0 < n \<Longrightarrow> bin_sc (Suc (n - 1)) b w = bin_sc n b w" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> set_bit_class.set_bit w (Suc (n - 1)) b = set_bit_class.set_bit w n b
theory Bits_Int

lemma bin_sc_numeral [simp]:
  "bin_sc (numeral k) b w =
    of_bool (odd w) + 2 * bin_sc (pred_numeral k) b (w div 2)" by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit w (numeral k) b = of_bool (odd w) + 2 * set_bit_class.set_bit (w div 2) (pred_numeral k) b
theory Bits_Int

lemma int_set_bit_0 [simp]: fixes x :: int shows
  "set_bit x 0 b = of_bool b + 2 * (x div 2)" by (fact bin_sc_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit x 0 b = of_bool b + 2 * (x div 2)
theory Bits_Int

lemma int_set_bit_Suc: fixes x :: int shows
  "set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit (x div 2) n b" by (fact bin_sc_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit_class.set_bit (x div 2) n b
theory Bits_Int

lemma bin_last_set_bit:
  "odd (set_bit x n b :: int) = (if n > 0 then odd x else b)" by (cases n) (simp_all add: int_set_bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (set_bit_class.set_bit x n b) = (if 0 < n then odd x else b)
theory Bits_Int

lemma bin_rest_set_bit:
  "(set_bit x n b :: int) div 2 = (if n > 0 then set_bit (x div 2) (n - 1) b else x div 2)" by (cases n) (simp_all add: int_set_bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit x n b div 2 = (if 0 < n then set_bit_class.set_bit (x div 2) (n - 1) b else x div 2)
theory Bits_Int

lemma int_set_bit_numeral: fixes x :: int shows
  "set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit (x div 2) (pred_numeral w) b" by (fact bin_sc_numeral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit_class.set_bit (x div 2) (pred_numeral w) b
theory Bits_Int

lemma msb_set_bit [simp]:
  "msb (set_bit (x :: int) n b) \<longleftrightarrow> msb x" by (simp add: msb_int_def set_bit_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (set_bit_class.set_bit x n b) = msb x
theory Bits_Int

lemma word_set_bit_def:
  \<open>set_bit a n x = word_of_int (bin_sc n x (uint a))\<close> apply (rule bit_word_eqI) apply (cases x) apply (simp_all add: bit_simps bin_sc_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit a n x = word_of_int (set_bit_class.set_bit (uint a) n x) proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (set_bit_class.set_bit a n x) na = bit (word_of_int (set_bit_class.set_bit (uint a) n x)) na proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>na < LENGTH('a); x\<rbrakk> \<Longrightarrow> bit (set_bit_class.set_bit a n x) na = bit (word_of_int (set_bit_class.set_bit (uint a) n x)) na
 2. \<And>na. \<lbrakk>na < LENGTH('a); \<not> x\<rbrakk> \<Longrightarrow> bit (set_bit_class.set_bit a n x) na = bit (word_of_int (set_bit_class.set_bit (uint a) n x)) na proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma set_bit_word_of_int:
  "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)" unfolding word_set_bit_def by (rule word_eqI) (simp add: word_size bin_nth_sc_gen nth_bintr bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (word_of_int x) n b = word_of_int (set_bit_class.set_bit x n b) proof (prove)
goal (1 subgoal):
 1. word_of_int (set_bit_class.set_bit (uint (word_of_int x)) n b) = word_of_int (set_bit_class.set_bit x n b)
theory Bits_Int

lemma word_set_numeral [simp]:
  "set_bit (numeral bin::'a::len word) n b =
    word_of_int (bin_sc n b (numeral bin))" unfolding word_numeral_alt by (rule set_bit_word_of_int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (numeral bin) n b = word_of_int (set_bit_class.set_bit (numeral bin) n b) proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (word_of_int (numeral bin)) n b = word_of_int (set_bit_class.set_bit (numeral bin) n b)
theory Bits_Int

lemma word_set_neg_numeral [simp]:
  "set_bit (- numeral bin::'a::len word) n b =
    word_of_int (bin_sc n b (- numeral bin))" unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (- numeral bin) n b = word_of_int (set_bit_class.set_bit (- numeral bin) n b) proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (word_of_int (- numeral bin)) n b = word_of_int (set_bit_class.set_bit (- numeral bin) n b)
theory Bits_Int

lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)" unfolding word_0_wi by (rule set_bit_word_of_int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 0 n b = word_of_int (set_bit_class.set_bit 0 n b) proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (word_of_int 0) n b = word_of_int (set_bit_class.set_bit 0 n b)
theory Bits_Int

lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)" unfolding word_1_wi by (rule set_bit_word_of_int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 1 n b = word_of_int (set_bit_class.set_bit 1 n b) proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (word_of_int 1) n b = word_of_int (set_bit_class.set_bit 1 n b)
theory Bits_Int

lemma int_not_simps:
  "NOT (0::int) = -1"
  "NOT (1::int) = -2"
  "NOT (- 1::int) = 0"
  "NOT (numeral w::int) = - numeral (w + Num.One)"
  "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
  "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)" by (simp_all add: not_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (NOT 0 = - 1 &&& NOT 1 = - 2 &&& NOT (- 1) = 0) &&& NOT (numeral w) = - numeral (w + num.One) &&& NOT (- numeral (num.Bit0 w)) = numeral (Num.BitM w) &&& NOT (- numeral (num.Bit1 w)) = numeral (num.Bit0 w)
theory Bits_Int

lemma int_not_not: "NOT (NOT x) = x"
  for x :: int by (fact bit.double_compl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (NOT x) = x
theory Bits_Int

lemma int_and_0 [simp]: "0 AND x = 0"
  for x :: int by (fact bit.conj_zero_left)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 AND x = 0
theory Bits_Int

lemma int_and_m1 [simp]: "-1 AND x = x"
  for x :: int by (fact and.left_neutral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 AND x = x
theory Bits_Int

lemma int_or_zero [simp]: "0 OR x = x"
  for x :: int by (fact or.left_neutral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 OR x = x
theory Bits_Int

lemma int_xor_zero [simp]: "0 XOR x = x"
  for x :: int by (fact xor.left_neutral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 XOR x = x
theory Bits_Int

lemma bin_rest_NOT [simp]: "(\<lambda>k::int. k div 2) (NOT x) = NOT ((\<lambda>k::int. k div 2) x)" by (fact not_int_div_2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT x div 2 = NOT (x div 2)
theory Bits_Int

lemma bin_last_NOT [simp]: "(odd :: int \<Rightarrow> bool) (NOT x) \<longleftrightarrow> \<not> (odd :: int \<Rightarrow> bool) x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (NOT x) = (\<not> odd x)
theory Bits_Int

lemma bin_rest_AND [simp]: "(\<lambda>k::int. k div 2) (x AND y) = (\<lambda>k::int. k div 2) x AND (\<lambda>k::int. k div 2) y" by (subst and_int_rec) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND y) div 2 = x div 2 AND y div 2
theory Bits_Int

lemma bin_last_AND [simp]: "(odd :: int \<Rightarrow> bool) (x AND y) \<longleftrightarrow> (odd :: int \<Rightarrow> bool) x \<and> (odd :: int \<Rightarrow> bool) y" by (subst and_int_rec) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (x AND y) = (odd x \<and> odd y)
theory Bits_Int

lemma bin_rest_OR [simp]: "(\<lambda>k::int. k div 2) (x OR y) = (\<lambda>k::int. k div 2) x OR (\<lambda>k::int. k div 2) y" by (subst or_int_rec) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x OR y) div 2 = x div 2 OR y div 2
theory Bits_Int

lemma bin_last_OR [simp]: "(odd :: int \<Rightarrow> bool) (x OR y) \<longleftrightarrow> (odd :: int \<Rightarrow> bool) x \<or> (odd :: int \<Rightarrow> bool) y" by (subst or_int_rec) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (x OR y) = (odd x \<or> odd y)
theory Bits_Int

lemma bin_rest_XOR [simp]: "(\<lambda>k::int. k div 2) (x XOR y) = (\<lambda>k::int. k div 2) x XOR (\<lambda>k::int. k div 2) y" by (subst xor_int_rec) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x XOR y) div 2 = x div 2 XOR y div 2
theory Bits_Int

lemma bin_last_XOR [simp]: "(odd :: int \<Rightarrow> bool) (x XOR y) \<longleftrightarrow> ((odd :: int \<Rightarrow> bool) x \<or> (odd :: int \<Rightarrow> bool) y) \<and> \<not> ((odd :: int \<Rightarrow> bool) x \<and> (odd :: int \<Rightarrow> bool) y)" by (subst xor_int_rec) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (x XOR y) = ((odd x \<or> odd y) \<and> \<not> (odd x \<and> odd y))