kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word_Operations

lemma word_ctz_not_minus_1:
  \<open>word_of_nat (word_ctz (w :: 'a :: len word)) \<noteq> (- 1 :: 'a::len word)\<close> if \<open>1 < LENGTH('a)\<close> proof - note word_ctz_le also from that have \<open>LENGTH('a) < mask LENGTH('a)\<close> by (simp add: less_mask) finally have \<open>word_ctz w < mask LENGTH('a)\<close> . then have \<open>word_of_nat (word_ctz w) < (word_of_nat (mask LENGTH('a)) :: 'a word)\<close> by (simp add: of_nat_word_less_iff) also have \<open>\<dots> = - 1\<close> by (rule bit_word_eqI) (simp add: bit_simps) finally show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (state)
goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (state)
this:
word_ctz ?w \<le> LENGTH(?'a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (state)
this:
word_ctz ?w \<le> LENGTH(?'a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (chain)
picking this:
1 < LENGTH('a) proof (prove)
using this:
1 < LENGTH('a)

goal (1 subgoal):
 1. LENGTH('a) < mask LENGTH('a) proof (state)
this:
LENGTH('a) < mask LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (chain)
picking this:
word_ctz ?w1 < mask LENGTH('a) proof (prove)
using this:
word_ctz ?w1 < mask LENGTH('a)

goal (1 subgoal):
 1. word_ctz w < mask LENGTH('a) proof (state)
this:
word_ctz w < mask LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (chain)
picking this:
word_ctz w < mask LENGTH('a) proof (prove)
using this:
word_ctz w < mask LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) < word_of_nat (mask LENGTH('a)) proof (state)
this:
word_of_nat (word_ctz w) < word_of_nat (mask LENGTH('a))

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (state)
this:
word_of_nat (word_ctz w) < word_of_nat (mask LENGTH('a))

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (prove)
goal (1 subgoal):
 1. word_of_nat (mask LENGTH('a)) = - 1 proof (state)
this:
word_of_nat (mask LENGTH('a)) = - 1

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (chain)
picking this:
word_of_nat (word_ctz w) < - 1 proof (prove)
using this:
word_of_nat (word_ctz w) < - 1

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1 proof (state)
this:
word_of_nat (word_ctz w) \<noteq> - 1

goal:
No subgoals!
theory More_Word_Operations

lemma unat_of_nat_ctz_mw:
  "unat (of_nat (word_ctz (w :: 'a :: len word)) :: 'a :: len word) = word_ctz w" by (simp add: unsigned_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat (word_ctz w)) = word_ctz w
theory More_Word_Operations

lemma unat_of_nat_ctz_smw:
  "unat (of_nat (word_ctz (w :: 'a :: len word)) :: 'a :: len signed word) = word_ctz w" by (simp add: unsigned_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat (word_ctz w)) = word_ctz w
theory More_Word_Operations

lemma sign_extend_eq_signed_take_bit:
  \<open>sign_extend = signed_take_bit\<close> proof (rule ext)+ fix n and w :: \<open>'a::len word\<close> show \<open>sign_extend n w = signed_take_bit n w\<close> proof (rule bit_word_eqI) fix q assume \<open>q < LENGTH('a)\<close> then show \<open>bit (sign_extend n w) q \<longleftrightarrow> bit (signed_take_bit n w) q\<close> by (auto simp add: bit_signed_take_bit_iff
        sign_extend_def bit_and_iff bit_or_iff bit_not_iff bit_mask_iff not_less
        exp_eq_0_imp_not_bit not_le min_def) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sign_extend = signed_take_bit proof (state)
goal (1 subgoal):
 1. \<And>x xa. sign_extend x xa = signed_take_bit x xa proof (state)
goal (1 subgoal):
 1. \<And>x xa. sign_extend x xa = signed_take_bit x xa proof (prove)
goal (1 subgoal):
 1. sign_extend n w = signed_take_bit n w proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (sign_extend n w) na = bit (signed_take_bit n w) na proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (sign_extend n w) na = bit (signed_take_bit n w) na proof (state)
this:
q < LENGTH('a)

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (sign_extend n w) na = bit (signed_take_bit n w) na proof (chain)
picking this:
q < LENGTH('a) proof (prove)
using this:
q < LENGTH('a)

goal (1 subgoal):
 1. bit (sign_extend n w) q = bit (signed_take_bit n w) q proof (state)
this:
bit (sign_extend n w) q = bit (signed_take_bit n w) q

goal:
No subgoals! proof (state)
this:
sign_extend n w = signed_take_bit n w

goal:
No subgoals!
theory More_Word_Operations

lemma ptr_add_0 [simp]:
  "ptr_add ref 0 = ref " unfolding ptr_add_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_add ref 0 = ref proof (prove)
goal (1 subgoal):
 1. ref + word_of_nat 0 = ref
theory More_Word_Operations

lemma pop_count_0[simp]:
  "pop_count 0 = 0" by (clarsimp simp:pop_count_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pop_count 0 = 0
theory More_Word_Operations

lemma pop_count_1[simp]:
  "pop_count 1 = 1" by (clarsimp simp:pop_count_def to_bl_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pop_count 1 = 1
theory More_Word_Operations

lemma pop_count_0_imp_0:
  "(pop_count w = 0) = (w = 0)" apply (rule iffI) apply (clarsimp simp:pop_count_def) apply (subst (asm) filter_empty_conv) apply (clarsimp simp:eq_zero_set_bl) apply fast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pop_count w = 0) = (w = 0) proof (prove)
goal (2 subgoals):
 1. pop_count w = 0 \<Longrightarrow> w = 0
 2. w = 0 \<Longrightarrow> pop_count w = 0 proof (prove)
goal (2 subgoals):
 1. filter id (to_bl w) = [] \<Longrightarrow> w = 0
 2. w = 0 \<Longrightarrow> pop_count w = 0 proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set (to_bl w). \<not> id x \<Longrightarrow> w = 0
 2. w = 0 \<Longrightarrow> pop_count w = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (to_bl w). \<not> x; True \<in> set (to_bl w)\<rbrakk> \<Longrightarrow> False
 2. w = 0 \<Longrightarrow> pop_count w = 0 proof (prove)
goal (1 subgoal):
 1. w = 0 \<Longrightarrow> pop_count w = 0 proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma word_log2_zero_eq [simp]:
  \<open>word_log2 0 = 0\<close> by (simp add: word_log2_def word_clz_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_log2 0 = 0
theory More_Word_Operations

lemma word_log2_eqI:
  \<open>word_log2 w = n\<close>
  if \<open>w \<noteq> 0\<close> \<open>bit w n\<close> \<open>\<And>m. bit w m \<Longrightarrow> m \<le> n\<close>
  for w :: \<open>'a::len word\<close> proof - from \<open>w \<noteq> 0\<close> have \<open>word_log2 w = Max {n. bit w n}\<close> by (simp add: word_log2_unfold) also have \<open>Max {n. bit w n} = n\<close> using that by (auto intro: Max_eqI) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_log2 w = n proof (state)
goal (1 subgoal):
 1. word_log2 w = n proof (chain)
picking this:
w \<noteq> 0 proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. word_log2 w = Max {n. bit w n} proof (state)
this:
word_log2 w = Max {n. bit w n}

goal (1 subgoal):
 1. word_log2 w = n proof (state)
this:
word_log2 w = Max {n. bit w n}

goal (1 subgoal):
 1. word_log2 w = n proof (prove)
goal (1 subgoal):
 1. Max {n. bit w n} = n proof (prove)
using this:
w \<noteq> 0
bit w n
bit w ?m \<Longrightarrow> ?m \<le> n

goal (1 subgoal):
 1. Max {n. bit w n} = n proof (state)
this:
Max {n. bit w n} = n

goal (1 subgoal):
 1. word_log2 w = n proof (chain)
picking this:
word_log2 w = n proof (prove)
using this:
word_log2 w = n

goal (1 subgoal):
 1. word_log2 w = n proof (state)
this:
word_log2 w = n

goal:
No subgoals!
theory More_Word_Operations

lemma word_log2_maximum:
  \<open>n \<le> word_log2 w\<close> if \<open>bit w n\<close> proof - have \<open>n \<le> Max {n. bit w n}\<close> using that by (auto intro: Max_ge) also from that have \<open>w \<noteq> 0\<close> by force then have \<open>Max {n. bit w n} = word_log2 w\<close> by (simp add: word_log2_unfold) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> word_log2 w proof (state)
goal (1 subgoal):
 1. n \<le> word_log2 w proof (prove)
goal (1 subgoal):
 1. n \<le> Max {n. bit w n} proof (prove)
using this:
bit w n

goal (1 subgoal):
 1. n \<le> Max {n. bit w n} proof (state)
this:
n \<le> Max {n. bit w n}

goal (1 subgoal):
 1. n \<le> word_log2 w proof (state)
this:
n \<le> Max {n. bit w n}

goal (1 subgoal):
 1. n \<le> word_log2 w proof (chain)
picking this:
bit w n proof (prove)
using this:
bit w n

goal (1 subgoal):
 1. w \<noteq> 0 proof (state)
this:
w \<noteq> 0

goal (1 subgoal):
 1. n \<le> word_log2 w proof (chain)
picking this:
w \<noteq> 0 proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. Max {n. bit w n} = word_log2 w proof (state)
this:
Max {n. bit w n} = word_log2 w

goal (1 subgoal):
 1. n \<le> word_log2 w proof (chain)
picking this:
n \<le> word_log2 w proof (prove)
using this:
n \<le> word_log2 w

goal (1 subgoal):
 1. n \<le> word_log2 w proof (state)
this:
n \<le> word_log2 w

goal:
No subgoals!
theory More_Word_Operations

lemma word_log2_nth_same:
  "w \<noteq> 0 \<Longrightarrow> bit w (word_log2 w)" by (drule bit_word_log2) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> bit w (word_log2 w)
theory More_Word_Operations

lemma word_log2_nth_not_set:
  "\<lbrakk> word_log2 w < i ; i < size w \<rbrakk> \<Longrightarrow> \<not> bit w i" using word_log2_maximum [of w i] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_log2 w < i; i < size w\<rbrakk> \<Longrightarrow> \<not> bit w i proof (prove)
using this:
bit w i \<Longrightarrow> i \<le> word_log2 w

goal (1 subgoal):
 1. \<lbrakk>word_log2 w < i; i < size w\<rbrakk> \<Longrightarrow> \<not> bit w i
theory More_Word_Operations

lemma word_log2_highest:
  assumes a: "bit w i"
  shows "i \<le> word_log2 w" using a by (simp add: word_log2_maximum)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i \<le> word_log2 w proof (prove)
using this:
bit w i

goal (1 subgoal):
 1. i \<le> word_log2 w
theory More_Word_Operations

lemma word_log2_max:
  "word_log2 w < size w" apply (cases \<open>w = 0\<close>) apply (simp_all add: word_size) apply (drule bit_word_log2) apply (fact bit_imp_le_length) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_log2 w < size w proof (prove)
goal (2 subgoals):
 1. w = 0 \<Longrightarrow> word_log2 w < size w
 2. w \<noteq> 0 \<Longrightarrow> word_log2 w < size w proof (prove)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. bit w (word_log2 w) \<Longrightarrow> word_log2 w < LENGTH('a) proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma word_clz_0[simp]:
  "word_clz (0::'a::len word) = LENGTH('a)" unfolding word_clz_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_clz 0 = LENGTH('a) proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (to_bl 0)) = LENGTH('a)
theory More_Word_Operations

lemma word_clz_minus_one[simp]:
  "word_clz (-1::'a::len word) = 0" unfolding word_clz_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_clz (- 1) = 0 proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (to_bl (- 1))) = 0
theory More_Word_Operations

lemma is_aligned_alignUp[simp]:
  "is_aligned (alignUp p n) n" by (simp add: alignUp_def is_aligned_mask mask_eq_decr_exp word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (alignUp p n) n
theory More_Word_Operations

lemma alignUp_idem:
  fixes a :: "'a::len word"
  assumes "is_aligned a n" "n < LENGTH('a)"
  shows "alignUp a n = a" using assms unfolding alignUp_def by (metis add_cancel_right_right add_diff_eq and_mask_eq_iff_le_mask mask_eq_decr_exp mask_out_add_aligned order_refl word_plus_and_or_coroll2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. alignUp a n = a proof (prove)
using this:
is_aligned a n
n < LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = a proof (prove)
using this:
is_aligned a n
n < LENGTH('a)

goal (1 subgoal):
 1. a + 2 ^ n - 1 AND NOT (2 ^ n - 1) = a
theory More_Word_Operations

lemma alignUp_def2:
  "alignUp a sz = a + 2 ^ sz - 1 AND NOT (mask sz)" by (simp add: alignUp_def flip: mask_eq_decr_exp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. alignUp a sz = a + 2 ^ sz - 1 AND NOT (mask sz)
theory More_Word_Operations

lemma alignUp_def3:
  "alignUp a sz = 2^ sz + (a - 1 AND NOT (mask sz))" by (simp add: alignUp_def2 is_aligned_triv field_simps mask_out_add_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. alignUp a sz = 2 ^ sz + (a - 1 AND NOT (mask sz))
theory More_Word_Operations

lemma is_aligned_diff_neg_mask:
  "is_aligned p sz \<Longrightarrow> (p - q AND NOT (mask sz)) = (p - ((alignUp q sz) AND NOT (mask sz)))" apply (clarsimp simp only:word_and_le2 diff_conv_add_uminus) apply (subst mask_out_add_aligned[symmetric]; simp) apply (simp add: eq_neg_iff_add_eq_0) apply (subst add.commute) apply (simp add: alignUp_distance is_aligned_neg_mask_eq mask_out_add_aligned and_mask_eq_iff_le_mask flip: mask_eq_x_eq_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> p - q AND NOT (mask sz) = p - (alignUp q sz AND NOT (mask sz)) proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> p + - q AND NOT (mask sz) = p + - (alignUp q sz AND NOT (mask sz)) proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> - q AND NOT (mask sz) = - (alignUp q sz AND NOT (mask sz)) proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> (- q AND NOT (mask sz)) + (alignUp q sz AND NOT (mask sz)) = 0 proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> (alignUp q sz AND NOT (mask sz)) + (- q AND NOT (mask sz)) = 0 proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma word_clz_max:
  "word_clz w \<le> size (w::'a::len word)" unfolding word_clz_def by (metis length_takeWhile_le word_size_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_clz w \<le> size w proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (to_bl w)) \<le> size w
theory More_Word_Operations

lemma word_clz_nonzero_max:
  fixes w :: "'a::len word"
  assumes nz: "w \<noteq> 0"
  shows "word_clz w < size (w::'a::len word)" proof - { assume a: "word_clz w = size (w::'a::len word)" hence "length (takeWhile Not (to_bl w)) = length (to_bl w)" by (simp add: word_clz_def word_size) hence allj: "\<forall>j\<in>set(to_bl w). \<not> j" by (metis a length_takeWhile_less less_irrefl_nat word_clz_def) hence "to_bl w = replicate (length (to_bl w)) False" using eq_zero_set_bl nz by fastforce hence "w = 0" by (metis to_bl_0 word_bl.Rep_eqD word_bl_Rep') with nz have False by simp } thus ?thesis using word_clz_max by (fastforce intro: le_neq_trans) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_clz w < size w proof (state)
goal (1 subgoal):
 1. word_clz w < size w proof (state)
goal (1 subgoal):
 1. word_clz w < size w proof (state)
this:
word_clz w = size w

goal (1 subgoal):
 1. word_clz w < size w proof (prove)
using this:
word_clz w = size w

goal (1 subgoal):
 1. length (takeWhile Not (to_bl w)) = length (to_bl w) proof (state)
this:
length (takeWhile Not (to_bl w)) = length (to_bl w)

goal (1 subgoal):
 1. word_clz w < size w proof (prove)
using this:
length (takeWhile Not (to_bl w)) = length (to_bl w)

goal (1 subgoal):
 1. \<forall>j\<in>set (to_bl w). \<not> j proof (state)
this:
\<forall>j\<in>set (to_bl w). \<not> j

goal (1 subgoal):
 1. word_clz w < size w proof (prove)
using this:
\<forall>j\<in>set (to_bl w). \<not> j

goal (1 subgoal):
 1. to_bl w = replicate (length (to_bl w)) False proof (prove)
using this:
\<forall>j\<in>set (to_bl w). \<not> j
(?w = 0) = (True \<notin> set (to_bl ?w))
w \<noteq> 0

goal (1 subgoal):
 1. to_bl w = replicate (length (to_bl w)) False proof (state)
this:
to_bl w = replicate (length (to_bl w)) False

goal (1 subgoal):
 1. word_clz w < size w proof (prove)
using this:
to_bl w = replicate (length (to_bl w)) False

goal (1 subgoal):
 1. w = 0 proof (state)
this:
w = 0

goal (1 subgoal):
 1. word_clz w < size w proof (chain)
picking this:
w \<noteq> 0
w = 0 proof (prove)
using this:
w \<noteq> 0
w = 0

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (1 subgoal):
 1. word_clz w < size w proof (state)
this:
word_clz w = size w \<Longrightarrow> False

goal (1 subgoal):
 1. word_clz w < size w proof (prove)
using this:
word_clz w = size w \<Longrightarrow> False

goal (1 subgoal):
 1. word_clz w < size w proof (prove)
using this:
word_clz w = size w \<Longrightarrow> False
word_clz ?w \<le> size ?w

goal (1 subgoal):
 1. word_clz w < size w proof (state)
this:
word_clz w < size w

goal:
No subgoals!
theory More_Word_Operations

lemma bin_sign_extend_iff [bit_simps]:
  \<open>bit (sign_extend e w) i \<longleftrightarrow> bit w (min e i)\<close>
  if \<open>i < LENGTH('a)\<close> for w :: \<open>'a::len word\<close> using that by (simp add: sign_extend_def bit_simps min_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (sign_extend e w) i = bit w (min e i) proof (prove)
using this:
i < LENGTH('a)

goal (1 subgoal):
 1. bit (sign_extend e w) i = bit w (min e i)
theory More_Word_Operations

lemma sign_extend_bitwise_if:
  "i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (if i < e then bit w i else bit w e)" by (simp add: word_size bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < size w \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e)
theory More_Word_Operations

lemma sign_extend_bitwise_if'  [word_eqI_simps]:
  \<open>i < LENGTH('a) \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (if i < e then bit w i else bit w e)\<close>
  for w :: \<open>'a::len word\<close> using sign_extend_bitwise_if [of i w e] by (simp add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e) proof (prove)
using this:
i < size w \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e)

goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e)
theory More_Word_Operations

lemma sign_extend_bitwise_disj:
  "i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> i \<le> e \<and> bit w i \<or> e \<le> i \<and> bit w e" by (auto simp: sign_extend_bitwise_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < size w \<Longrightarrow> bit (sign_extend e w) i = (i \<le> e \<and> bit w i \<or> e \<le> i \<and> bit w e)
theory More_Word_Operations

lemma sign_extend_bitwise_cases:
  "i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (i \<le> e \<longrightarrow> bit w i) \<and> (e \<le> i \<longrightarrow> bit w e)" by (auto simp: sign_extend_bitwise_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < size w \<Longrightarrow> bit (sign_extend e w) i = ((i \<le> e \<longrightarrow> bit w i) \<and> (e \<le> i \<longrightarrow> bit w e))
theory More_Word_Operations

lemma sign_extend_def':
  "sign_extend n w = (if bit w n then w OR NOT (mask (Suc n)) else w AND mask (Suc n))" by (rule bit_word_eqI) (auto simp add: bit_simps sign_extend_eq_signed_take_bit min_def less_Suc_eq_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sign_extend n w = (if bit w n then w OR NOT (mask (Suc n)) else w AND mask (Suc n))
theory More_Word_Operations

lemma sign_extended_sign_extend:
  "sign_extended n (sign_extend n w)" by (clarsimp simp: sign_extended_def word_size sign_extend_bitwise_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sign_extended n (sign_extend n w)
theory More_Word_Operations

lemma sign_extended_iff_sign_extend:
  "sign_extended n w \<longleftrightarrow> sign_extend n w = w" apply auto apply (auto simp add: bit_eq_iff) apply (simp_all add: bit_simps sign_extend_eq_signed_take_bit not_le min_def sign_extended_def word_size split: if_splits) using le_imp_less_or_eq apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sign_extended n w = (sign_extend n w = w) proof (prove)
goal (2 subgoals):
 1. sign_extended n w \<Longrightarrow> sign_extend n w = w
 2. sign_extend n w = w \<Longrightarrow> sign_extended n w proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>sign_extended n w; na < LENGTH('a); bit (sign_extend n w) na\<rbrakk> \<Longrightarrow> bit w na
 2. \<And>na. \<lbrakk>sign_extended n w; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> bit (sign_extend n w) na
 3. \<forall>na<LENGTH('a). bit (sign_extend n w) na = bit w na \<Longrightarrow> sign_extended n w proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i; na < LENGTH('a); n \<le> na; bit w n\<rbrakk> \<Longrightarrow> bit w na
 2. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> n \<le> na \<longrightarrow> bit w n
 3. \<forall>na<LENGTH('a). na < n \<or> bit w n = bit w na \<Longrightarrow> \<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x < ?y \<or> ?x = ?y

goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i; na < LENGTH('a); n \<le> na; bit w n\<rbrakk> \<Longrightarrow> bit w na
 2. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> n \<le> na \<longrightarrow> bit w n
 3. \<forall>na<LENGTH('a). na < n \<or> bit w n = bit w na \<Longrightarrow> \<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma sign_extended_weaken:
  "sign_extended n w \<Longrightarrow> n \<le> m \<Longrightarrow> sign_extended m w" unfolding sign_extended_def by (cases "n < m") auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sign_extended n w; n \<le> m\<rbrakk> \<Longrightarrow> sign_extended m w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i>n. i < size w \<longrightarrow> bit w i = bit w n; n \<le> m\<rbrakk> \<Longrightarrow> \<forall>i>m. i < size w \<longrightarrow> bit w i = bit w m
theory More_Word_Operations

lemma sign_extend_sign_extend_eq:
  "sign_extend m (sign_extend n w) = sign_extend (min m n) w" by (rule bit_word_eqI) (simp add: sign_extend_eq_signed_take_bit bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sign_extend m (sign_extend n w) = sign_extend (min m n) w
theory More_Word_Operations

lemma sign_extended_high_bits:
  "\<lbrakk> sign_extended e p; j < size p; e \<le> i; i < j \<rbrakk> \<Longrightarrow> bit p i = bit p j" by (drule (1) sign_extended_weaken; simp add: sign_extended_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sign_extended e p; j < size p; e \<le> i; i < j\<rbrakk> \<Longrightarrow> bit p i = bit p j
theory More_Word_Operations

lemma sign_extend_eq:
  "w AND mask (Suc n) = v AND mask (Suc n) \<Longrightarrow> sign_extend n w = sign_extend n v" by (simp flip: take_bit_eq_mask add: sign_extend_eq_signed_take_bit signed_take_bit_eq_iff_take_bit_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w AND mask (Suc n) = v AND mask (Suc n) \<Longrightarrow> sign_extend n w = sign_extend n v
theory More_Word_Operations

lemma sign_extended_neq_mask:
  "\<lbrakk>sign_extended n ptr; m \<le> n\<rbrakk> \<Longrightarrow> sign_extended n (ptr AND NOT (mask m))" by (fastforce simp: sign_extended_def word_size neg_mask_test_bit bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sign_extended n ptr; m \<le> n\<rbrakk> \<Longrightarrow> sign_extended n (ptr AND NOT (mask m))