kings-crown/FVELER_Isabelle huggingface dataset:
theory Typedef_Morphisms

lemma td_ext_ubin:
  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
    (take_bit (LENGTH('a)))" apply standard apply transfer apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. td_ext uint word_of_int (uints LENGTH('a)) (take_bit LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. \<And>x. uint (word_of_int x) = take_bit LENGTH('a) x proof (prove)
goal (1 subgoal):
 1. \<And>x. take_bit LENGTH('a) x = take_bit LENGTH('a) x proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma td_ext_unat [OF refl]:
  "n = LENGTH('a::len) \<Longrightarrow>
    td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" apply (standard; transfer) apply (simp_all add: unats_def take_bit_of_nat take_bit_nat_eq_self_iff
      flip: take_bit_eq_mod) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = LENGTH('a) \<Longrightarrow> td_ext unat word_of_nat (unats n) (\<lambda>i. i mod 2 ^ n) proof (prove)
goal (4 subgoals):
 1. \<And>x n. n = LENGTH('a) \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) x \<in> unats n
 2. \<And>x n. n = LENGTH('a) \<Longrightarrow> take_bit LENGTH('a) (int ((nat \<circ> take_bit LENGTH('a)) x)) = take_bit LENGTH('a) x
 3. \<And>y n. \<lbrakk>n = LENGTH('a); y \<in> unats n\<rbrakk> \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (int y) = y
 4. \<And>x n. n = LENGTH('a) \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (int x) = x mod 2 ^ n proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))"
  for z :: "'a::len word" apply (unfold unats_def) apply clarsimp apply (metis le_unat_uoi unsigned_less) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<le> unat z \<Longrightarrow> y \<in> unats LENGTH('a) proof (prove)
goal (1 subgoal):
 1. y \<le> unat z \<Longrightarrow> y \<in> {i. i < 2 ^ LENGTH('a)} proof (prove)
goal (1 subgoal):
 1. y \<le> unat z \<Longrightarrow> y < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma td_ext_sbin:
  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
    (signed_take_bit (LENGTH('a) - 1))" by (standard; transfer) (auto simp add: sints_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. td_ext sint word_of_int (sints LENGTH('a)) (signed_take_bit (LENGTH('a) - 1))
theory Typedef_Morphisms

lemma td_ext_sint:
  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
     (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
         2 ^ (LENGTH('a) - 1))" using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. td_ext sint word_of_int (sints LENGTH('a)) (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)) proof (prove)
using this:
td_ext sint word_of_int (sints LENGTH('a)) (signed_take_bit (LENGTH('a) - 1))

goal (1 subgoal):
 1. td_ext sint word_of_int (sints LENGTH('a)) (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1))
theory Typedef_Morphisms

lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)" by (fact uints_def [unfolded no_bintr_alt1])

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

lemma uints_mono_iff: "uints l \<subseteq> uints m \<longleftrightarrow> l \<le> m" using power_increasing_iff[of "2::int" l m] apply (auto simp: uints_num subset_iff simp del: power_increasing_iff) apply (meson less_irrefl not_le zero_le_numeral zero_le_power) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (uints l \<subseteq> uints m) = (l \<le> m) proof (prove)
using this:
1 < 2 \<Longrightarrow> (2 ^ l \<le> 2 ^ m) = (l \<le> m)

goal (1 subgoal):
 1. (uints l \<subseteq> uints m) = (l \<le> m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> 2 ^ l \<le> 2 ^ m; \<not> l \<le> m; \<forall>t. 0 \<le> t \<and> t < 2 ^ l \<longrightarrow> t < 2 ^ m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma Bit_in_uints_Suc: "of_bool c + 2 * w \<in> uints (Suc m)" if "w \<in> uints m" using that by (auto simp: uints_num)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bool c + 2 * w \<in> uints (Suc m) proof (prove)
using this:
w \<in> uints m

goal (1 subgoal):
 1. of_bool c + 2 * w \<in> uints (Suc m)
theory Typedef_Morphisms

lemma Bit_in_uintsI: "of_bool c + 2 * w \<in> uints m" if "w \<in> uints (m - 1)" "m > 0" using Bit_in_uints_Suc[OF that(1)] that(2) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bool c + 2 * w \<in> uints m proof (prove)
using this:
of_bool ?c + 2 * w \<in> uints (Suc (m - 1))
0 < m

goal (1 subgoal):
 1. of_bool c + 2 * w \<in> uints m
theory Typedef_Morphisms

lemma bin_cat_in_uintsI:
  \<open>concat_bit n b a \<in> uints m\<close> if \<open>a \<in> uints l\<close> \<open>m \<ge> l + n\<close> proof - from \<open>m \<ge> l + n\<close> obtain q where \<open>m = l + n + q\<close> using le_Suc_ex by blast then have \<open>(2::int) ^ m = 2 ^ n * 2 ^ (l + q)\<close> by (simp add: ac_simps power_add) moreover have \<open>a mod 2 ^ (l + q) = a\<close> using \<open>a \<in> uints l\<close> by (auto simp add: uints_def take_bit_eq_mod power_add Divides.mod_mult2_eq) ultimately have \<open>concat_bit n b a = take_bit m (concat_bit n b a)\<close> by (simp add: concat_bit_eq take_bit_eq_mod push_bit_eq_mult Divides.mod_mult2_eq) then show ?thesis by (simp add: uints_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (state)
goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (chain)
picking this:
l + n \<le> m proof (prove)
using this:
l + n \<le> m

goal (1 subgoal):
 1. (\<And>q. m = l + n + q \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
l + n \<le> m
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

goal (1 subgoal):
 1. (\<And>q. m = l + n + q \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
m = l + n + q

goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (chain)
picking this:
m = l + n + q proof (prove)
using this:
m = l + n + q

goal (1 subgoal):
 1. 2 ^ m = 2 ^ n * 2 ^ (l + q) proof (state)
this:
2 ^ m = 2 ^ n * 2 ^ (l + q)

goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (state)
this:
2 ^ m = 2 ^ n * 2 ^ (l + q)

goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ (l + q) = a proof (prove)
using this:
a \<in> uints l

goal (1 subgoal):
 1. a mod 2 ^ (l + q) = a proof (state)
this:
a mod 2 ^ (l + q) = a

goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (chain)
picking this:
2 ^ m = 2 ^ n * 2 ^ (l + q)
a mod 2 ^ (l + q) = a proof (prove)
using this:
2 ^ m = 2 ^ n * 2 ^ (l + q)
a mod 2 ^ (l + q) = a

goal (1 subgoal):
 1. concat_bit n b a = take_bit m (concat_bit n b a) proof (state)
this:
concat_bit n b a = take_bit m (concat_bit n b a)

goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (chain)
picking this:
concat_bit n b a = take_bit m (concat_bit n b a) proof (prove)
using this:
concat_bit n b a = take_bit m (concat_bit n b a)

goal (1 subgoal):
 1. concat_bit n b a \<in> uints m proof (state)
this:
concat_bit n b a \<in> uints m

goal:
No subgoals!
theory Even_More_List

lemma upt_add_eq_append':
  assumes "i \<le> j" and "j \<le> k"
  shows "[i..<k] = [i..<j] @ [j..<k]" using assms le_Suc_ex upt_add_eq_append by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [i..<k] = [i..<j] @ [j..<k] proof (prove)
using this:
i \<le> j
j \<le> k
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n
?i \<le> ?j \<Longrightarrow> [?i..<?j + ?k] = [?i..<?j] @ [?j..<?j + ?k]

goal (1 subgoal):
 1. [i..<k] = [i..<j] @ [j..<k]
theory Even_More_List

lemma map_idem_upt_eq:
  \<open>map f [m..<n] = [m..<n]\<close> if \<open>\<And>q. m \<le> q \<Longrightarrow> q < n \<Longrightarrow> f q = q\<close> proof (cases \<open>n \<ge> m\<close>) case False then show ?thesis by simp next case True moreover define r where \<open>r = n - m\<close> ultimately have \<open>n = m + r\<close> by simp with that have \<open>\<And>q. m \<le> q \<Longrightarrow> q < m + r \<Longrightarrow> f q = q\<close> by simp then have \<open>map f [m..<m + r] = [m..<m + r]\<close> by (induction r) simp_all with \<open>n = m + r\<close> show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map f [m..<n] = [m..<n] proof (state)
goal (2 subgoals):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n]
 2. \<not> m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (state)
this:
\<not> m \<le> n

goal (2 subgoals):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n]
 2. \<not> m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (chain)
picking this:
\<not> m \<le> n proof (prove)
using this:
\<not> m \<le> n

goal (1 subgoal):
 1. map f [m..<n] = [m..<n] proof (state)
this:
map f [m..<n] = [m..<n]

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (state)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (state)
this:
m \<le> n

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (state)
this:
m \<le> n

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (state)
this:
r = n - m

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (chain)
picking this:
m \<le> n
r = n - m proof (prove)
using this:
m \<le> n
r = n - m

goal (1 subgoal):
 1. n = m + r proof (state)
this:
n = m + r

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (chain)
picking this:
\<lbrakk>m \<le> ?q; ?q < n\<rbrakk> \<Longrightarrow> f ?q = ?q
n = m + r proof (prove)
using this:
\<lbrakk>m \<le> ?q; ?q < n\<rbrakk> \<Longrightarrow> f ?q = ?q
n = m + r

goal (1 subgoal):
 1. \<And>q. \<lbrakk>m \<le> q; q < m + r\<rbrakk> \<Longrightarrow> f q = q proof (state)
this:
\<lbrakk>m \<le> ?q; ?q < m + r\<rbrakk> \<Longrightarrow> f ?q = ?q

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (chain)
picking this:
\<lbrakk>m \<le> ?q; ?q < m + r\<rbrakk> \<Longrightarrow> f ?q = ?q proof (prove)
using this:
\<lbrakk>m \<le> ?q; ?q < m + r\<rbrakk> \<Longrightarrow> f ?q = ?q

goal (1 subgoal):
 1. map f [m..<m + r] = [m..<m + r] proof (state)
this:
map f [m..<m + r] = [m..<m + r]

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> map f [m..<n] = [m..<n] proof (chain)
picking this:
n = m + r
map f [m..<m + r] = [m..<m + r] proof (prove)
using this:
n = m + r
map f [m..<m + r] = [m..<m + r]

goal (1 subgoal):
 1. map f [m..<n] = [m..<n] proof (state)
this:
map f [m..<n] = [m..<n]

goal:
No subgoals!
theory Even_More_List

lemma upt_zero_numeral_unfold:
  \<open>[0..<numeral n] = [0..<pred_numeral n] @ [pred_numeral n]\<close> by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [0..<numeral n] = [0..<pred_numeral n] @ [pred_numeral n]
theory Even_More_List

lemma length_takeWhile_less:
  "\<exists>x\<in>set xs. \<not> P x \<Longrightarrow> length (takeWhile P xs) < length xs" by (induct xs) (auto split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>set xs. \<not> P x \<Longrightarrow> length (takeWhile P xs) < length xs
theory Singleton_Bit_Shifts

lemma bit_shiftr1_iff [bit_simps]:
  \<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
  for w :: \<open>'a::len word\<close> by (simp add: shiftr1_def bit_drop_bit_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (shiftr1 w) n = bit w (Suc n)
theory Singleton_Bit_Shifts

lemma bit_sshiftr1_iff [bit_simps]:
  \<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
  for w :: \<open>'a::len word\<close> by (auto simp add: sshiftr1_def bit_signed_drop_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (sshiftr1 w) n = bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)
theory Singleton_Bit_Shifts

lemma shiftr1_1: "shiftr1 (1::'a::len word) = 0" by (simp add: shiftr1_def)

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

lemma sshiftr1_eq:
  \<open>sshiftr1 w = word_of_int (sint w div 2)\<close> by (rule bit_word_eqI) (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sshiftr1 w = word_of_int (sint w div 2)
theory Singleton_Bit_Shifts

lemma shiftr1_eq:
  \<open>shiftr1 w = word_of_int (uint w div 2)\<close> by (rule bit_word_eqI) (simp add: bit_simps flip: bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftr1 w = word_of_int (uint w div 2)
theory Singleton_Bit_Shifts

lemma shiftl1_rev:
  "shiftl1 w = word_reverse (shiftr1 (word_reverse w))" by (rule bit_word_eqI) (auto simp add: bit_simps Suc_diff_Suc simp flip: bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 w = word_reverse (shiftr1 (word_reverse w))
theory Singleton_Bit_Shifts

lemma shiftr1_bintr:
  "(shiftr1 (numeral w) :: 'a::len word) =
    word_of_int (take_bit LENGTH('a) (numeral w) div 2)" by (rule bit_word_eqI) (simp add: bit_simps bit_numeral_iff [where ?'a = int] flip: bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftr1 (numeral w) = word_of_int (take_bit LENGTH('a) (numeral w) div 2)
theory Singleton_Bit_Shifts

lemma sshiftr1_sbintr:
  "(sshiftr1 (numeral w) :: 'a::len word) =
    word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)" apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply (rule bit_word_eqI) apply (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sshiftr1 (numeral w) = word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> sshiftr1 (numeral w) = word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sshiftr1 (numeral w) = word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sshiftr1 (numeral w) = word_of_int (signed_take_bit nat (numeral w) div 2) proof (prove)
goal (1 subgoal):
 1. \<And>nat n. \<lbrakk>LENGTH('a) = Suc nat; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (sshiftr1 (numeral w)) n = bit (word_of_int (signed_take_bit nat (numeral w) div 2)) n proof (prove)
goal:
No subgoals!
theory Singleton_Bit_Shifts

lemma shiftl1_wi:
  "shiftl1 (word_of_int w) = word_of_int (2 * w)" by (rule bit_word_eqI) (auto simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 (word_of_int w) = word_of_int (2 * w)
theory Singleton_Bit_Shifts

lemma shiftl1_numeral:
  "shiftl1 (numeral w) = numeral (Num.Bit0 w)" unfolding word_numeral_alt shiftl1_wi by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 (numeral w) = numeral (num.Bit0 w) proof (prove)
goal (1 subgoal):
 1. word_of_int (2 * numeral w) = word_of_int (numeral (num.Bit0 w))
theory Singleton_Bit_Shifts

lemma shiftl1_neg_numeral:
  "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)" unfolding word_neg_numeral_alt shiftl1_wi by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 (- numeral w) = - numeral (num.Bit0 w) proof (prove)
goal (1 subgoal):
 1. word_of_int (2 * - numeral w) = word_of_int (- numeral (num.Bit0 w))
theory Singleton_Bit_Shifts

lemma shiftl1_0:
  "shiftl1 0 = 0" by (simp add: shiftl1_def)

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

lemma shiftl1_def_u:
  "shiftl1 w = word_of_int (2 * uint w)" by (fact shiftl1_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 w = word_of_int (2 * uint w)
theory Singleton_Bit_Shifts

lemma shiftl1_def_s:
  "shiftl1 w = word_of_int (2 * sint w)" by (simp add: shiftl1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shiftl1 w = word_of_int (2 * sint w)
theory Singleton_Bit_Shifts

lemma shiftr1_0:
  "shiftr1 0 = 0" by (simp add: shiftr1_def)

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

lemma sshiftr1_0:
  "sshiftr1 0 = 0" by (simp add: sshiftr1_def)

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

lemma sshiftr1_n1:
  "sshiftr1 (- 1) = - 1" by (simp add: sshiftr1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sshiftr1 (- 1) = - 1
theory Singleton_Bit_Shifts

lemma uint_shiftr1:
  "uint (shiftr1 w) = uint w div 2" by (rule bit_eqI) (simp add: bit_simps flip: bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (shiftr1 w) = uint w div 2
theory Singleton_Bit_Shifts

lemma shiftr1_div_2:
  "uint (shiftr1 w) = uint w div 2" by (fact uint_shiftr1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (shiftr1 w) = uint w div 2
theory Singleton_Bit_Shifts

lemma sshiftr1_div_2:
  "sint (sshiftr1 w) = sint w div 2" by (rule bit_eqI) (auto simp add: bit_simps ac_simps min_def simp flip: bit_Suc elim: le_SucE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (sshiftr1 w) = sint w div 2
theory Singleton_Bit_Shifts

lemma nth_shiftl1:
  "bit (shiftl1 w) n \<longleftrightarrow> n < size w \<and> n > 0 \<and> bit w (n - 1)" by (auto simp add: word_size bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (shiftl1 w) n = (n < size w \<and> 0 < n \<and> bit w (n - 1))
theory Singleton_Bit_Shifts

lemma nth_shiftr1:
  "bit (shiftr1 w) n = bit w (Suc n)" by (fact bit_shiftr1_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (shiftr1 w) n = bit w (Suc n)
theory Singleton_Bit_Shifts

lemma nth_sshiftr1: "bit (sshiftr1 w) n = (if n = size w - 1 then bit w n else bit w (Suc n))" by (auto simp add: word_size bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (sshiftr1 w) n = (if n = size w - 1 then bit w n else bit w (Suc n))
theory Singleton_Bit_Shifts

lemma shiftl_power:
  "(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y" by (induction x) (simp_all add: shiftl1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (shiftl1 ^^ x) y = 2 ^ x * y
theory Singleton_Bit_Shifts

lemma le_shiftr1':
  "\<lbrakk> shiftr1 u \<le> shiftr1 v ; shiftr1 u \<noteq> shiftr1 v \<rbrakk> \<Longrightarrow> u \<le> v" by (meson dual_order.antisym le_cases le_shiftr1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>shiftr1 u \<le> shiftr1 v; shiftr1 u \<noteq> shiftr1 v\<rbrakk> \<Longrightarrow> u \<le> v
theory Singleton_Bit_Shifts

lemma sshiftr_eq_funpow_sshiftr1:
  \<open>w >>> n = (sshiftr1 ^^ n) w\<close> apply (rule sym) apply (simp add: sshiftr1_def sshiftr_def) apply (induction n) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w >>> n = (sshiftr1 ^^ n) w proof (prove)
goal (1 subgoal):
 1. (sshiftr1 ^^ n) w = w >>> n proof (prove)
goal (1 subgoal):
 1. (signed_drop_bit (Suc 0) ^^ n) w = signed_drop_bit n w proof (prove)
goal (2 subgoals):
 1. (signed_drop_bit (Suc 0) ^^ 0) w = signed_drop_bit 0 w
 2. \<And>n. (signed_drop_bit (Suc 0) ^^ n) w = signed_drop_bit n w \<Longrightarrow> (signed_drop_bit (Suc 0) ^^ Suc n) w = signed_drop_bit (Suc n) w proof (prove)
goal:
No subgoals!
theory Legacy_Aliases

lemma conj_assoc: "(x \<^bold>\<sqinter> y) \<^bold>\<sqinter> z = x \<^bold>\<sqinter> (y \<^bold>\<sqinter> z)" by (fact conj.assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<^bold>\<sqinter> y) \<^bold>\<sqinter> z = x \<^bold>\<sqinter> y \<^bold>\<sqinter> z
theory Legacy_Aliases

lemma conj_one_left: "\<^bold>1 \<^bold>\<sqinter> x = x" by (fact conj.left_neutral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<^bold>1 \<^bold>\<sqinter> x = x
theory Legacy_Aliases

lemma conj_left_absorb: "x \<^bold>\<sqinter> (x \<^bold>\<sqinter> y) = x \<^bold>\<sqinter> y" by (fact conj.left_idem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<sqinter> x \<^bold>\<sqinter> y = x \<^bold>\<sqinter> y
theory Legacy_Aliases

lemma conj_absorb: "x \<^bold>\<sqinter> x = x" by (fact conj.idem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<sqinter> x = x
theory Legacy_Aliases

lemma disj_assoc: "(x \<^bold>\<squnion> y) \<^bold>\<squnion> z = x \<^bold>\<squnion> (y \<^bold>\<squnion> z)" by (fact disj.assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<^bold>\<squnion> y) \<^bold>\<squnion> z = x \<^bold>\<squnion> y \<^bold>\<squnion> z
theory Legacy_Aliases

lemma disj_commute: "x \<^bold>\<squnion> y = y \<^bold>\<squnion> x" by (fact disj.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<squnion> y = y \<^bold>\<squnion> x
theory Legacy_Aliases

lemma disj_zero_left: "\<^bold>0 \<^bold>\<squnion> x = x" by (fact disj.left_neutral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<^bold>0 \<^bold>\<squnion> x = x
theory Legacy_Aliases

lemma disj_left_absorb: "x \<^bold>\<squnion> (x \<^bold>\<squnion> y) = x \<^bold>\<squnion> y" by (fact disj.left_idem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<squnion> x \<^bold>\<squnion> y = x \<^bold>\<squnion> y
theory Legacy_Aliases

lemma disj_absorb: "x \<^bold>\<squnion> x = x" by (fact disj.idem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<squnion> x = x
theory Legacy_Aliases

lemma xor_zero_left: "\<^bold>0 \<^bold>\<ominus> x = x" by (fact xor.left_neutral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<^bold>0 \<^bold>\<ominus> x = x
theory Legacy_Aliases

lemma complement_mask:
  "complement (2 ^ n - 1) = not (mask n)" unfolding mask_eq_decr_exp by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not (2 ^ n - 1) = not (mask n) proof (prove)
goal (1 subgoal):
 1. not (2 ^ n - 1) = not (2 ^ n - 1)
theory Legacy_Aliases

lemma bit_bshiftr1_iff:
  \<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
    for w :: \<open>'a::len word\<close> by (auto simp add: bit_simps simp flip: bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (or (w div 2) (push_bit (LENGTH('a) - Suc 0) (of_bool b))) n = (b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n))
theory Legacy_Aliases

lemma bit_setBit_iff:
  \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
  for w :: \<open>'a::len word\<close> by (auto simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bit m w) n = (m = n \<and> n < LENGTH('a) \<or> bit w n)
theory Legacy_Aliases

lemma bit_clearBit_iff:
  \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
  for w :: \<open>'a::len word\<close> by (auto simp add: bit_simps)

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