kings-crown/FVELER_Isabelle huggingface dataset:
theory Aligned

lemma aligned_less_plus_1:
  "\<lbrakk> is_aligned x n; n > 0 \<rbrakk> \<Longrightarrow> x < x + 1" apply (rule plus_one_helper2) apply (rule order_refl) apply (clarsimp simp: field_simps) apply (drule arg_cong[where f="\<lambda>x. x - 1"]) apply (clarsimp simp: is_aligned_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x < x + 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x \<le> x
 2. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x + 1 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x + 1 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n; 1 + x = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n; 1 + x - 1 = 0 - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Aligned

lemma gap_between_aligned:
  "\<lbrakk>a < (b :: 'a ::len word); is_aligned a n; is_aligned b n; n < LENGTH('a) \<rbrakk>
  \<Longrightarrow> a + (2^n - 1) < b" by (simp add: aligned_add_offset_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; is_aligned a n; is_aligned b n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a + (2 ^ n - 1) < b
theory Aligned

lemma is_aligned_add_step_le:
  "\<lbrakk> is_aligned (a::'a::len word) n; is_aligned b n; a < b; b \<le> a + mask n \<rbrakk> \<Longrightarrow> False" apply (simp flip: not_le) apply (erule notE) apply (cases "LENGTH('a) \<le> n") apply (drule (1) is_aligned_over_length)+ apply (drule mask_over_length) apply clarsimp apply (clarsimp simp: word_le_nat_alt not_less not_le) apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) apply (subst (asm) unat_add_lem' [symmetric]) apply (simp add: is_aligned_mask_offset_unat) apply (metis gap_between_aligned linorder_not_less mask_eq_decr_exp unat_arith_simps(2)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; a < b; b \<le> a + mask n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; \<not> b \<le> a; b \<le> a + mask n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n\<rbrakk> \<Longrightarrow> b \<le> a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a
 2. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<le> a + mask n; LENGTH('a) \<le> n; a = 0; b = 0\<rbrakk> \<Longrightarrow> b \<le> a
 2. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<le> a + mask n; a = 0; b = 0; mask n = - 1\<rbrakk> \<Longrightarrow> b \<le> a
 2. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat (a + mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat a + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); is_aligned a n; is_aligned b n\<rbrakk> \<Longrightarrow> unat a + unat (mask n) < 2 ^ LENGTH('a)
 2. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat (a + mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat (a + mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a proof (prove)
goal:
No subgoals!
theory Aligned

lemma aligned_add_mask_lessD:
  "\<lbrakk> x + mask n < y; is_aligned x n \<rbrakk> \<Longrightarrow> x < y" for y::"'a::len word" by (metis is_aligned_no_overflow' mask_2pm1 order_le_less_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x + mask n < y; is_aligned x n\<rbrakk> \<Longrightarrow> x < y
theory Aligned

lemma aligned_add_mask_less_eq:
  "\<lbrakk> is_aligned x n; is_aligned y n;  n < LENGTH('a) \<rbrakk> \<Longrightarrow> (x + mask n < y) = (x < y)"
  for y::"'a::len word" using aligned_add_mask_lessD is_aligned_add_step_le word_le_not_less by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x + mask n < y) = (x < y) proof (prove)
using this:
\<lbrakk>?x + mask ?n < ?y; is_aligned ?x ?n\<rbrakk> \<Longrightarrow> ?x < ?y
\<lbrakk>is_aligned ?a ?n; is_aligned ?b ?n; ?a < ?b; ?b \<le> ?a + mask ?n\<rbrakk> \<Longrightarrow> False
(?b \<le> ?a) = (\<not> ?a < ?b)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x + mask n < y) = (x < y)
theory Aligned

lemma is_aligned_add:
  "\<lbrakk>is_aligned p n; is_aligned q n\<rbrakk> \<Longrightarrow> is_aligned (p + q) n" by (simp add: is_aligned_mask mask_add_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned q n\<rbrakk> \<Longrightarrow> is_aligned (p + q) n
theory Aligned

lemma aligned_shift:
  "\<lbrakk>x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \<le> LENGTH('a)\<rbrakk>
   \<Longrightarrow> (x + y) >> n = y >> n" apply (subst word_plus_and_or_coroll; rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth) apply (metis less_2p_is_upper_bits_unset not_le) apply (metis le_add1 less_2p_is_upper_bits_unset test_bit_bin) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> x + y >> n = y >> n proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (x AND y) na = bit 0 na
 2. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (x OR y >> n) na = bit (y >> n) na proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x na; bit y na\<rbrakk> \<Longrightarrow> False
 2. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na) proof (prove)
goal:
No subgoals!
theory Aligned

lemma aligned_shift':
  "\<lbrakk>x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \<le> LENGTH('a)\<rbrakk>
   \<Longrightarrow> (y + x) >> n = y >> n" apply (subst word_plus_and_or_coroll; rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth) apply (metis less_2p_is_upper_bits_unset not_le) apply (metis bit_imp_le_length le_add1 less_2p_is_upper_bits_unset) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> y + x >> n = y >> n proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (y AND x) na = bit 0 na
 2. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (y OR x >> n) na = bit (y >> n) na proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit y na; bit x na\<rbrakk> \<Longrightarrow> False
 2. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na) proof (prove)
goal:
No subgoals!
theory Aligned

lemma and_neg_mask_plus_mask_mono: "(p AND NOT (mask n)) + mask n \<ge> p"
  for p :: \<open>'a::len word\<close> apply (rule word_le_minus_cancel[where x = "p AND NOT (mask n)"]) apply (clarsimp simp: subtract_mask) using word_and_le1[where a = "mask n" and y = p] apply (clarsimp simp: mask_eq_decr_exp word_le_less_eq) apply (rule is_aligned_no_overflow'[folded mask_2pm1]) apply (clarsimp simp: is_aligned_neg_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<le> (p AND NOT (mask n)) + mask n proof (prove)
goal (2 subgoals):
 1. p - (p AND NOT (mask n)) \<le> (p AND NOT (mask n)) + mask n - (p AND NOT (mask n))
 2. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n proof (prove)
goal (2 subgoals):
 1. p AND mask n \<le> mask n
 2. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n proof (prove)
using this:
p AND mask n \<le> mask n

goal (2 subgoals):
 1. p AND mask n \<le> mask n
 2. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n proof (prove)
goal (1 subgoal):
 1. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n proof (prove)
goal (1 subgoal):
 1. is_aligned (p AND NOT (mask n)) n proof (prove)
goal:
No subgoals!
theory Aligned

lemma word_neg_and_le:
  "ptr \<le> (ptr AND NOT (mask n)) + (2 ^ n - 1)"
  for ptr :: \<open>'a::len word\<close> by (simp add: and_neg_mask_plus_mask_mono mask_2pm1[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<le> (ptr AND NOT (mask n)) + (2 ^ n - 1)
theory Aligned

lemma is_aligned_sub_helper:
  "\<lbrakk> is_aligned (p - d) n; d < 2 ^ n \<rbrakk>
     \<Longrightarrow> (p AND mask n = d) \<and> (p AND (NOT (mask n)) = p - d)" by (drule(1) is_aligned_add_helper, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (p - d) n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p AND mask n = d \<and> p AND NOT (mask n) = p - d
theory Aligned

lemma is_aligned_after_mask:
  "\<lbrakk>is_aligned k m;m\<le> n\<rbrakk> \<Longrightarrow> is_aligned (k AND mask n) m" by (rule is_aligned_andI1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned k m; m \<le> n\<rbrakk> \<Longrightarrow> is_aligned (k AND mask n) m
theory Aligned

lemma is_aligned_add_not_aligned:
  "\<lbrakk>is_aligned (p::'a::len word) n; \<not> is_aligned (q::'a::len word) n\<rbrakk> \<Longrightarrow> \<not> is_aligned (p + q) n" by (metis is_aligned_addD1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<not> is_aligned q n\<rbrakk> \<Longrightarrow> \<not> is_aligned (p + q) n
theory Aligned

lemma neg_mask_add_aligned:
  "\<lbrakk> is_aligned p n; q < 2 ^ n \<rbrakk> \<Longrightarrow> (p + q) AND NOT (mask n) = p AND NOT (mask n)" by (metis is_aligned_add_helper is_aligned_neg_mask_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; q < 2 ^ n\<rbrakk> \<Longrightarrow> p + q AND NOT (mask n) = p AND NOT (mask n)
theory Aligned

lemma offset_not_aligned:
  "\<lbrakk> is_aligned (p::'a::len word) n; i > 0; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow>
   \<not> is_aligned (p + of_nat i) n" apply (erule is_aligned_add_not_aligned) apply transfer apply (auto simp add: is_aligned_iff_udvd) apply (metis (no_types, lifting) le_less_trans less_not_refl2 less_or_eq_imp_le of_nat_eq_0_iff take_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_of_nat unat_lt2p unat_power_lower) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; 0 < i; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> is_aligned (p + word_of_nat i) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < i; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> is_aligned (word_of_nat i) n proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>0 < i; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> 2 ^ n dvd take_bit LENGTH('a) (int i) proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>0 < i; i < 2 ^ n; n < LENGTH('a); 2 ^ n dvd take_bit LENGTH('a) (int i)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Aligned

lemma le_or_mask:
  "w \<le> w' \<Longrightarrow> w OR mask x \<le> w' OR mask x"
  for w w' :: \<open>'a::len word\<close> by (metis neg_mask_add_mask add.commute le_word_or1 mask_2pm1 neg_mask_mono_le word_plus_mono_left)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<le> w' \<Longrightarrow> w OR mask x \<le> w' OR mask x
theory Bit_Comprehension

lemma set_bits_False_eq [simp]:
  \<open>(BITS _. False) = 0\<close> using set_bits_bit_eq [of 0] by (simp add: bot_fun_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (BITS _. False) = (0::'a) proof (prove)
using this:
set_bits (bit (0::'a)) = (0::'a)

goal (1 subgoal):
 1. (BITS _. False) = (0::'a)
theory Bit_Comprehension

lemma bit_set_bits_word_iff [bit_simps]:
  \<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close> by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bits P) n = (n < LENGTH('a) \<and> P n)
theory Bit_Comprehension

lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. bit i n)" by (rule bit_eqI) (auto simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_int i = (BITS n. bit i n)
theory Bit_Comprehension

lemma set_bits_K_False:
  \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close> by (fact set_bits_False_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (BITS _. False) = 0
theory Bit_Comprehension

lemma word_test_bit_set_bits: "bit (BITS n. f n :: 'a :: len word) n \<longleftrightarrow> n < LENGTH('a) \<and> f n" by (fact bit_set_bits_word_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (BITS n. f n) n = (n < LENGTH('a) \<and> f n)
theory Bit_Comprehension

lemma bit_set_bit_aux [bit_simps]:
  \<open>bit (set_bits_aux n w) m \<longleftrightarrow> m < LENGTH('a) \<and>
    (if m < n then f m else bit w (m - n))\<close> for w :: \<open>'a::len word\<close> by (auto simp add: bit_simps set_bits_aux_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (local.set_bits_aux n w) m = (m < LENGTH('a) \<and> (if m < n then f m else bit w (m - n)))
theory Bit_Comprehension

lemma set_bits_aux_0 [simp]:
  \<open>set_bits_aux 0 w = w\<close> by (simp add: set_bits_aux_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.set_bits_aux 0 w = w
theory Bit_Comprehension

lemma set_bits_aux_Suc [simp]:
  \<open>set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\<close> by (rule bit_word_eqI) (auto simp add: bit_simps le_less_Suc_eq mult.commute [of _ 2])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.set_bits_aux (Suc n) w = local.set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))
theory Bit_Comprehension

lemma set_bits_aux_simps [code]:
  \<open>set_bits_aux 0 w = w\<close>
  \<open>set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\<close> by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.set_bits_aux 0 w = w &&& local.set_bits_aux (Suc n) w = local.set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))
theory Bit_Comprehension

lemma set_bits_aux_rec:
  \<open>set_bits_aux n w =
  (if n = 0 then w
   else let n' = n - 1 in set_bits_aux n' (push_bit 1 w OR (if f n' then 1 else 0)))\<close> by (cases n) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.set_bits_aux n w = (if n = 0 then w else let n' = n - 1 in local.set_bits_aux n' (push_bit 1 w OR (if f n' then 1 else 0)))
theory Bit_Comprehension_Int

lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)" by (simp add: set_bits_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (BITS _. False) = 0
theory Bit_Comprehension_Int

lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)" by (simp add: set_bits_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (BITS _. True) = - 1
theory Bit_Comprehension_Int

lemma set_bits_code [code]:
  "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (\<lambda>_. set_bits :: _ \<Rightarrow> int)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bits = Code.abort STR ''set_bits is unsupported on type int'' (\<lambda>_. set_bits)
theory Bit_Comprehension_Int

lemma wf_set_bits_int_simps: "wf_set_bits_int f \<longleftrightarrow> (\<exists>n. (\<forall>n'\<ge>n. \<not> f n') \<or> (\<forall>n'\<ge>n. f n'))" by(auto simp add: wf_set_bits_int.simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf_set_bits_int f = (\<exists>n. (\<forall>n'\<ge>n. \<not> f n') \<or> (\<forall>n'\<ge>n. f n'))
theory Bit_Comprehension_Int

lemma wf_set_bits_int_Suc [simp]:
  "wf_set_bits_int (\<lambda>n. f (Suc n)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs") by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf_set_bits_int (\<lambda>n. f (Suc n)) = wf_set_bits_int f
theory Bit_Comprehension_Int

lemma bin_last_set_bits [simp]:
  "odd (set_bits f :: int) = f 0" by (subst int_set_bits_unfold_BIT) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (set_bits f) = f 0
theory Bit_Comprehension_Int

lemma bin_rest_set_bits [simp]:
  "set_bits f div (2 :: int) = set_bits (f \<circ> Suc)" by (subst int_set_bits_unfold_BIT) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bits f div 2 = set_bits (f \<circ> Suc)
theory Bit_Comprehension_Int

lemma bin_nth_set_bits [simp]:
  "bit (set_bits f :: int) m \<longleftrightarrow> f m" using wff proof (induction m arbitrary: f) case 0 then show ?case by (simp add: Bit_Comprehension_Int.bin_last_set_bits bit_0) next case Suc from Suc.IH [of "f \<circ> Suc"] Suc.prems show ?case by (simp add: Bit_Comprehension_Int.bin_rest_set_bits comp_def bit_Suc) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bits f) m = f m proof (prove)
using this:
wf_set_bits_int f

goal (1 subgoal):
 1. bit (set_bits f) m = f m proof (state)
goal (2 subgoals):
 1. \<And>f. wf_set_bits_int f \<Longrightarrow> bit (set_bits f) 0 = f 0
 2. \<And>m f. \<lbrakk>\<And>f. wf_set_bits_int f \<Longrightarrow> bit (set_bits f) m = f m; wf_set_bits_int f\<rbrakk> \<Longrightarrow> bit (set_bits f) (Suc m) = f (Suc m) proof (state)
this:
wf_set_bits_int f

goal (2 subgoals):
 1. \<And>f. wf_set_bits_int f \<Longrightarrow> bit (set_bits f) 0 = f 0
 2. \<And>m f. \<lbrakk>\<And>f. wf_set_bits_int f \<Longrightarrow> bit (set_bits f) m = f m; wf_set_bits_int f\<rbrakk> \<Longrightarrow> bit (set_bits f) (Suc m) = f (Suc m) proof (chain)
picking this:
wf_set_bits_int f proof (prove)
using this:
wf_set_bits_int f

goal (1 subgoal):
 1. bit (BITS a. f a) 0 = f 0 proof (state)
this:
bit (BITS a. f a) 0 = f 0

goal (1 subgoal):
 1. \<And>m f. \<lbrakk>\<And>f. wf_set_bits_int f \<Longrightarrow> bit (set_bits f) m = f m; wf_set_bits_int f\<rbrakk> \<Longrightarrow> bit (set_bits f) (Suc m) = f (Suc m) proof (state)
goal (1 subgoal):
 1. \<And>m f. \<lbrakk>\<And>f. wf_set_bits_int f \<Longrightarrow> bit (set_bits f) m = f m; wf_set_bits_int f\<rbrakk> \<Longrightarrow> bit (set_bits f) (Suc m) = f (Suc m) proof (state)
this:
wf_set_bits_int ?f \<Longrightarrow> bit (BITS a. ?f a) m_ = ?f m_
wf_set_bits_int f

goal (1 subgoal):
 1. \<And>m f. \<lbrakk>\<And>f. wf_set_bits_int f \<Longrightarrow> bit (set_bits f) m = f m; wf_set_bits_int f\<rbrakk> \<Longrightarrow> bit (set_bits f) (Suc m) = f (Suc m) proof (chain)
picking this:
wf_set_bits_int (f \<circ> Suc) \<Longrightarrow> bit (BITS a. (f \<circ> Suc) a) m_ = (f \<circ> Suc) m_
wf_set_bits_int f proof (prove)
using this:
wf_set_bits_int (f \<circ> Suc) \<Longrightarrow> bit (BITS a. (f \<circ> Suc) a) m_ = (f \<circ> Suc) m_
wf_set_bits_int f

goal (1 subgoal):
 1. bit (BITS a. f a) (Suc m_) = f (Suc m_) proof (state)
this:
bit (BITS a. f a) (Suc m_) = f (Suc m_)

goal:
No subgoals!
theory Most_significant_bit

lemma msb_bin_rest [simp]: "msb (x div 2) = msb x"
  for x :: int by (simp add: msb_int_def)

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

lemma int_msb_and [simp]: "msb ((x :: int) AND y) \<longleftrightarrow> msb x \<and> msb y" by(simp add: msb_int_def)

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

lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) \<longleftrightarrow> msb x \<noteq> msb y" by(simp add: msb_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (x XOR y) = (msb x \<noteq> msb y)
theory Most_significant_bit

lemma msb_shiftl [simp]: "msb ((x :: int) << n) \<longleftrightarrow> msb x" by (simp add: msb_int_def shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (x << n) = msb x
theory Most_significant_bit

lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \<longleftrightarrow> msb x" by (simp add: msb_int_def shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (x >> r) = msb x
theory Most_significant_bit

lemma msb_0 [simp]: "msb (0 :: int) = False" by(simp add: msb_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb 0 = False
theory Most_significant_bit

lemma msb_1 [simp]: "msb (1 :: int) = False" by(simp add: msb_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb 1 = False
theory Most_significant_bit

lemma msb_numeral [simp]:
  "msb (numeral n :: int) = False"
  "msb (- numeral n :: int) = True" by(simp_all add: msb_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (numeral n) = False &&& msb (- numeral n) = True
theory Most_significant_bit

lemma msb_word_eq:
  \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close> by (simp add: msb_word_iff_bit)

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

lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0" by (simp add: msb_word_eq bit_last_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb w = (sint w < 0)
theory Most_significant_bit

lemma msb_word_iff_sless_0:
  \<open>msb w \<longleftrightarrow> w <s 0\<close> by (simp add: word_msb_sint word_sless_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb w = (w <s 0)
theory Most_significant_bit

lemma msb_word_of_int:
  "msb (word_of_int x::'a::len word) = bit x (LENGTH('a) - 1)" by (simp add: msb_word_iff_bit bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (word_of_int x) = bit x (LENGTH('a) - 1)
theory Most_significant_bit

lemma word_msb_neg_numeral [simp]:
  "msb (- numeral w::'a::len word) = bit (- numeral w :: int) (LENGTH('a) - 1)" unfolding word_neg_numeral_alt by (rule msb_word_of_int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (- numeral w) = bit (- numeral w) (LENGTH('a) - 1) proof (prove)
goal (1 subgoal):
 1. msb (word_of_int (- numeral w)) = bit (- numeral w) (LENGTH('a) - 1)
theory Most_significant_bit

lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)" by (simp add: msb_word_iff_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> msb 0