kings-crown/FVELER_Isabelle huggingface dataset:
theory Bits_Int

lemma bintrunc_Suc_numeral:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) 1 = 1"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- 1) = 1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral (w + Num.One))" by (simp_all add: take_bit_Suc del: take_bit_minus_one_eq_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (take_bit (Suc n) 1 = 1 &&& take_bit (Suc n) (- 1) = 1 + 2 * take_bit n (- 1) &&& take_bit (Suc n) (numeral (num.Bit0 w)) = 2 * take_bit n (numeral w)) &&& take_bit (Suc n) (numeral (num.Bit1 w)) = 1 + 2 * take_bit n (numeral w) &&& take_bit (Suc n) (- numeral (num.Bit0 w)) = 2 * take_bit n (- numeral w) &&& take_bit (Suc n) (- numeral (num.Bit1 w)) = 1 + 2 * take_bit n (- numeral (w + num.One))
theory Bits_Int

lemma sbintrunc_0_numeral [simp]:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 1 = -1"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (numeral (Num.Bit0 w)) = 0"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (numeral (Num.Bit1 w)) = -1"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (- numeral (Num.Bit0 w)) = 0"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (- numeral (Num.Bit1 w)) = -1" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit 0 1 = - 1 &&& signed_take_bit 0 (numeral (num.Bit0 w)) = 0) &&& signed_take_bit 0 (numeral (num.Bit1 w)) = - 1 &&& signed_take_bit 0 (- numeral (num.Bit0 w)) = 0 &&& signed_take_bit 0 (- numeral (num.Bit1 w)) = - 1
theory Bits_Int

lemma sbintrunc_Suc_numeral:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) 1 = 1"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral (w + Num.One))" by (simp_all add: signed_take_bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit (Suc n) 1 = 1 &&& signed_take_bit (Suc n) (numeral (num.Bit0 w)) = 2 * signed_take_bit n (numeral w)) &&& signed_take_bit (Suc n) (numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit n (numeral w) &&& signed_take_bit (Suc n) (- numeral (num.Bit0 w)) = 2 * signed_take_bit n (- numeral w) &&& signed_take_bit (Suc n) (- numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit n (- numeral (w + num.One))
theory Bits_Int

lemma bin_sign_lem: "(bin_sign ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin) = -1) = bit bin n" by (simp add: bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (bin_sign (signed_take_bit n bin) = - 1) = bit bin n
theory Bits_Int

lemma nth_bintr: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) n \<longleftrightarrow> n < m \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w n" by (fact bit_take_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (take_bit m w) n = (n < m \<and> bit w n)
theory Bits_Int

lemma nth_sbintr: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) n = (if n < m then (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w n else (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w m)" by (simp add: bit_signed_take_bit_iff min_def)

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

lemma bin_nth_Bit1:
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral (Num.Bit1 w)) n \<longleftrightarrow>
    n = 0 \<or> (\<exists>m. n = Suc m \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral w) m)" using even_bit_succ_iff [of \<open>2 * numeral w :: int\<close> n]
    bit_double_iff [of \<open>numeral w :: int\<close> n] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (numeral (num.Bit1 w)) n = (n = 0 \<or> (\<exists>m. n = Suc m \<and> bit (numeral w) m)) proof (prove)
using this:
even (2 * numeral w) \<Longrightarrow> bit (1 + 2 * numeral w) n = (bit (2 * numeral w) n \<or> n = 0)
bit (2 * numeral w) n = (bit (numeral w) (n - 1) \<and> n \<noteq> 0 \<and> possible_bit TYPE(int) n)

goal (1 subgoal):
 1. bit (numeral (num.Bit1 w)) n = (n = 0 \<or> (\<exists>m. n = Suc m \<and> bit (numeral w) m))
theory Bits_Int

lemma bintrunc_bintrunc_l: "n \<le> m \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by simp

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

lemma sbintrunc_sbintrunc_l: "n \<le> m \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> signed_take_bit m (signed_take_bit n w) = signed_take_bit n w
theory Bits_Int

lemma bintrunc_bintrunc_ge: "n \<le> m \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (rule bin_eqI) (auto simp: nth_bintr)

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

lemma bintrunc_bintrunc_min [simp]: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (min m n) w" by (rule take_bit_take_bit)

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

lemma sbintrunc_sbintrunc_min [simp]: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (min m n) w" by (rule signed_take_bit_signed_take_bit)

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

lemma bintrunc_minus: "0 < n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc (n - 1)) w = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by auto

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

lemma sbintrunc_minus: "0 < n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc (n - 1)) w = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by auto

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

lemma sbintrunc_BIT_I:
  \<open>0 < n \<Longrightarrow>
  (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) 0 = y \<Longrightarrow>
  (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n 0 = 2 * y\<close> by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; signed_take_bit (n - 1) 0 = y\<rbrakk> \<Longrightarrow> signed_take_bit n 0 = 2 * y
theory Bits_Int

lemma sbintrunc_Suc_Is:
  \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1) = y \<Longrightarrow>
  (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- 1) = 1 + 2 * y\<close> by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n (- 1) = y \<Longrightarrow> signed_take_bit (Suc n) (- 1) = 1 + 2 * y
theory Bits_Int

lemma sbintrunc_Suc_lem: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m x = y" by (rule ssubst)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>signed_take_bit (Suc n) x = y; m = Suc n\<rbrakk> \<Longrightarrow> signed_take_bit m x = y
theory Bits_Int

lemma sbintrunc_bintrunc_lt: "m > n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> signed_take_bit n (take_bit m w) = signed_take_bit n w
theory Bits_Int

lemma bintrunc_sbintrunc_le: "m \<le> Suc n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w" by (rule take_bit_signed_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> Suc n \<Longrightarrow> take_bit m (signed_take_bit n w) = take_bit m w
theory Bits_Int

lemma bintrunc_sbintrunc' [simp]: "0 < n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (cases n) simp_all

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

lemma sbintrunc_bintrunc' [simp]: "0 < n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) w" by (cases n) simp_all

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

lemma bin_sbin_eq_iff: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) x = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) y \<longleftrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y" apply (rule iffI) apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc]) apply simp apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (take_bit (Suc n) x = take_bit (Suc n) y) = (signed_take_bit n x = signed_take_bit n y) proof (prove)
goal (2 subgoals):
 1. take_bit (Suc n) x = take_bit (Suc n) y \<Longrightarrow> signed_take_bit n x = signed_take_bit n y
 2. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) x = take_bit (Suc n) y proof (prove)
goal (2 subgoals):
 1. take_bit (Suc n) x = take_bit (Suc n) y \<Longrightarrow> signed_take_bit n (take_bit (Suc n) x) = signed_take_bit n (take_bit (Suc n) y)
 2. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) x = take_bit (Suc n) y proof (prove)
goal (1 subgoal):
 1. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) x = take_bit (Suc n) y proof (prove)
goal (1 subgoal):
 1. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) (signed_take_bit n x) = take_bit (Suc n) (signed_take_bit n y) proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_sbin_eq_iff':
  "0 < n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y \<longleftrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) x = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) y" by (cases n) (simp_all add: bin_sbin_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (take_bit n x = take_bit n y) = (signed_take_bit (n - 1) x = signed_take_bit (n - 1) y)
theory Bits_Int

lemma bintrunc_numeral:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) x = of_bool (odd x) + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (x div 2)" by (simp add: numeral_eq_Suc take_bit_Suc mod_2_eq_odd)

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

lemma sbintrunc_numeral:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) x = of_bool (odd x) + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (x div 2)" by (simp add: numeral_eq_Suc signed_take_bit_Suc mod2_eq_if)

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

lemma bintrunc_numeral_simps [simp]:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit0 w)) =
    2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit1 w)) =
    1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit0 w)) =
    2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit1 w)) =
    1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral (w + Num.One))"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) 1 = 1" by (simp_all add: bintrunc_numeral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (take_bit (numeral k) (numeral (num.Bit0 w)) = 2 * take_bit (pred_numeral k) (numeral w) &&& take_bit (numeral k) (numeral (num.Bit1 w)) = 1 + 2 * take_bit (pred_numeral k) (numeral w)) &&& take_bit (numeral k) (- numeral (num.Bit0 w)) = 2 * take_bit (pred_numeral k) (- numeral w) &&& take_bit (numeral k) (- numeral (num.Bit1 w)) = 1 + 2 * take_bit (pred_numeral k) (- numeral (w + num.One)) &&& take_bit (numeral k) 1 = 1
theory Bits_Int

lemma sbintrunc_numeral_simps [simp]:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit0 w)) =
    2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit1 w)) =
    1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit0 w)) =
    2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit1 w)) =
    1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral (w + Num.One))"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) 1 = 1" by (simp_all add: sbintrunc_numeral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit (numeral k) (numeral (num.Bit0 w)) = 2 * signed_take_bit (pred_numeral k) (numeral w) &&& signed_take_bit (numeral k) (numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit (pred_numeral k) (numeral w)) &&& signed_take_bit (numeral k) (- numeral (num.Bit0 w)) = 2 * signed_take_bit (pred_numeral k) (- numeral w) &&& signed_take_bit (numeral k) (- numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit (pred_numeral k) (- numeral (w + num.One)) &&& signed_take_bit (numeral k) 1 = 1
theory Bits_Int

lemma no_bintr_alt1: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = (\<lambda>w. w mod 2 ^ n :: int)" by (rule ext) (rule bintrunc_mod2p)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n = (\<lambda>w. w mod 2 ^ n)
theory Bits_Int

lemma range_bintrunc: "range ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n) = {i. 0 \<le> i \<and> i < 2 ^ n}" by (auto simp add: take_bit_eq_mod image_iff) (metis mod_pos_pos_trivial)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range (take_bit n) = {i. 0 \<le> i \<and> i < 2 ^ n}
theory Bits_Int

lemma range_sbintrunc: "range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}" proof - have \<open>surj (\<lambda>k::int. k + 2 ^ n)\<close> by (rule surjI [of _ \<open>(\<lambda>k. k - 2 ^ n)\<close>]) simp moreover have \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = ((\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n))\<close> by (simp add: sbintrunc_eq_take_bit fun_eq_iff) ultimately show ?thesis apply (simp only: fun.set_map range_bintrunc) apply (auto simp add: image_iff) apply presburger done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n} proof (state)
goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n} proof (prove)
goal (1 subgoal):
 1. surj (\<lambda>k. k + 2 ^ n) proof (state)
this:
surj (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n} proof (state)
this:
surj (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n} proof (prove)
goal (1 subgoal):
 1. signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n) proof (state)
this:
signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n} proof (chain)
picking this:
surj (\<lambda>k. k + 2 ^ n)
signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n) proof (prove)
using this:
surj (\<lambda>k. k + 2 ^ n)
signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>surj (\<lambda>k. k + 2 ^ n); signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)\<rbrakk> \<Longrightarrow> (\<lambda>k. k - 2 ^ n) ` {i. 0 \<le> i \<and> i < 2 ^ Suc n} = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n); - (2 ^ n) \<le> x; x < 2 ^ n\<rbrakk> \<Longrightarrow> \<exists>xa\<ge>0. xa < 2 * 2 ^ n \<and> x = xa - 2 ^ n proof (prove)
goal:
No subgoals! proof (state)
this:
range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}

goal:
No subgoals!
theory Bits_Int

lemma sbintrunc_inc:
  \<open>k + 2 ^ Suc n \<le> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n k\<close> if \<open>k < - (2 ^ n)\<close> using that by (fact signed_take_bit_int_greater_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k + 2 ^ Suc n \<le> signed_take_bit n k proof (prove)
using this:
k < - (2 ^ n)

goal (1 subgoal):
 1. k + 2 ^ Suc n \<le> signed_take_bit n k
theory Bits_Int

lemma sbintrunc_dec:
  \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close> using that by (fact signed_take_bit_int_less_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n k \<le> k - 2 ^ Suc n proof (prove)
using this:
2 ^ n \<le> k

goal (1 subgoal):
 1. signed_take_bit n k \<le> k - 2 ^ Suc n
theory Bits_Int

lemma bintr_ge0: "0 \<le> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (simp add: bintrunc_mod2p)

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

lemma bintr_Min: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1) = 2 ^ n - 1" by (simp add: stable_imp_take_bit_eq mask_eq_exp_minus_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n (- 1) = 2 ^ n - 1
theory Bits_Int

lemma sbintr_ge: "- (2 ^ n) \<le> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (fact signed_take_bit_int_greater_eq_minus_exp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (2 ^ n) \<le> signed_take_bit n w
theory Bits_Int

lemma sbintr_lt: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w < 2 ^ n" by (fact signed_take_bit_int_less_exp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n w < 2 ^ n
theory Bits_Int

lemma sign_Pls_ge_0: "bin_sign bin = 0 \<longleftrightarrow> bin \<ge> 0"
  for bin :: int by (simp add: bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (bin_sign bin = 0) = (0 \<le> bin)
theory Bits_Int

lemma sign_Min_lt_0: "bin_sign bin = -1 \<longleftrightarrow> bin < 0"
  for bin :: int by (simp add: bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (bin_sign bin = - 1) = (bin < 0)
theory Bits_Int

lemma bin_rest_trunc: "(\<lambda>k::int. k div 2) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) ((\<lambda>k::int. k div 2) bin)" by (simp add: take_bit_rec [of n bin])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n bin div 2 = take_bit (n - 1) (bin div 2)
theory Bits_Int

lemma bin_rest_power_trunc:
  "((\<lambda>k::int. k div 2) ^^ k) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - k) (((\<lambda>k::int. k div 2) ^^ k) bin)" by (induct k) (auto simp: bin_rest_trunc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>k. k div 2) ^^ k) (take_bit n bin) = take_bit (n - k) (((\<lambda>k. k div 2) ^^ k) bin)
theory Bits_Int

lemma bin_rest_trunc_i: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((\<lambda>k::int. k div 2) bin) = (\<lambda>k::int. k div 2) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) bin)" by (auto simp add: take_bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n (bin div 2) = take_bit (Suc n) bin div 2