kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

lemma odd_word_imp_even_next:"odd (unat (x::('a::len) word)) \<Longrightarrow> x + 1 = 0 \<or> even (unat (x + 1))" apply (cut_tac x=x in word_overflow_unat) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (unat x) \<Longrightarrow> x + 1 = 0 \<or> even (unat (x + 1)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>odd (unat x); unat (x + 1) = unat x + 1 \<or> x + 1 = 0\<rbrakk> \<Longrightarrow> x + 1 = 0 \<or> even (unat (x + 1)) proof (prove)
goal:
No subgoals!
theory More_Word

lemma overflow_imp_lsb:"(x::('a::len) word) + 1 = 0 \<Longrightarrow> bit x 0" using even_plus_one_iff [of x] by (simp add: bit_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + 1 = 0 \<Longrightarrow> bit x 0 proof (prove)
using this:
even (x + 1) = odd x

goal (1 subgoal):
 1. x + 1 = 0 \<Longrightarrow> bit x 0
theory More_Word

lemma odd_iff_lsb:"odd (unat (x::('a::len) word)) = bit x 0" by transfer (simp add: even_nat_iff bit_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (unat x) = bit x 0
theory More_Word

lemma of_nat_neq_iff_word:
      "x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a) \<Longrightarrow>
         (((of_nat x)::('a::len) word) \<noteq> of_nat y) = (x \<noteq> y)" apply (rule iffI) apply (case_tac "x = y") apply (subst (asm) of_nat_eq_iff[symmetric]) apply auto apply (case_tac "((of_nat x)::('a::len) word) = of_nat y") apply auto apply (metis unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a) \<Longrightarrow> (word_of_nat x \<noteq> word_of_nat y) = (x \<noteq> y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); word_of_nat x \<noteq> word_of_nat y\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); x \<noteq> y\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> word_of_nat y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); word_of_nat x \<noteq> word_of_nat y; x = y\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); word_of_nat x \<noteq> word_of_nat y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<noteq> y
 3. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); x \<noteq> y\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> word_of_nat y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>of_nat (x mod 2 ^ LENGTH('a)) \<noteq> of_nat (y mod 2 ^ LENGTH('a)); word_of_nat x \<noteq> word_of_nat y; x = y\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); word_of_nat x \<noteq> word_of_nat y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<noteq> y
 3. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); x \<noteq> y\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> word_of_nat y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); x \<noteq> y; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); x \<noteq> y; word_of_nat x = word_of_nat y; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); x \<noteq> y; word_of_nat x = word_of_nat y; word_of_nat x \<noteq> word_of_nat y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a); x \<noteq> y; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory More_Word

lemma lsb_this_or_next: "\<not> (bit ((x::('a::len) word) + 1) 0) \<Longrightarrow> bit x 0" by (simp add: bit_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit (x + 1) 0 \<Longrightarrow> bit x 0
theory More_Word

lemma mask_or_not_mask:
  "x AND mask n OR x AND NOT (mask n) = x"
  for x :: \<open>'a::len word\<close> apply (subst word_oa_dist, simp) apply (subst word_oa_dist2, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND mask n OR x AND NOT (mask n) = x proof (prove)
goal (1 subgoal):
 1. x AND (mask n OR x AND NOT (mask n)) = x proof (prove)
goal:
No subgoals!
theory More_Word

lemma word_gr0_conv_Suc: "(m::'a::len word) > 0 \<Longrightarrow> \<exists>n. m = n + 1" by (metis add.commute add_minus_cancel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < m \<Longrightarrow> \<exists>n. m = n + 1
theory More_Word

lemma revcast_down_us [OF refl]:
  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (signed_drop_bit n w)"
  for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; source_size rc = target_size rc + n\<rbrakk> \<Longrightarrow> rc w = ucast (signed_drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n\<rbrakk> \<Longrightarrow> revcast w = ucast (signed_drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n; na < LENGTH('b)\<rbrakk> \<Longrightarrow> bit (revcast w) na = bit (ucast (signed_drop_bit n w)) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma revcast_down_ss [OF refl]:
  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (signed_drop_bit n w)"
  for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; source_size rc = target_size rc + n\<rbrakk> \<Longrightarrow> rc w = scast (signed_drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n\<rbrakk> \<Longrightarrow> revcast w = scast (signed_drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n; na < LENGTH('b)\<rbrakk> \<Longrightarrow> bit (revcast w) na = bit (scast (signed_drop_bit n w)) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma revcast_down_uu [OF refl]:
  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (drop_bit n w)"
  for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; source_size rc = target_size rc + n\<rbrakk> \<Longrightarrow> rc w = ucast (drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n\<rbrakk> \<Longrightarrow> revcast w = ucast (drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n; na < LENGTH('b)\<rbrakk> \<Longrightarrow> bit (revcast w) na = bit (ucast (drop_bit n w)) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma revcast_down_su [OF refl]:
  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (drop_bit n w)"
  for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; source_size rc = target_size rc + n\<rbrakk> \<Longrightarrow> rc w = scast (drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n\<rbrakk> \<Longrightarrow> revcast w = scast (drop_bit n w) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('a) = LENGTH('b) + n; na < LENGTH('b)\<rbrakk> \<Longrightarrow> bit (revcast w) na = bit (scast (drop_bit n w)) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma cast_down_rev [OF refl]:
  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (push_bit n w)"
  for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = ucast; source_size uc = target_size uc + n\<rbrakk> \<Longrightarrow> uc w = revcast (push_bit n w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = ucast; LENGTH('a) = LENGTH('b) + n\<rbrakk> \<Longrightarrow> ucast w = revcast (push_bit n w) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>uc = ucast; LENGTH('a) = LENGTH('b) + n; na < LENGTH('b)\<rbrakk> \<Longrightarrow> bit (ucast w) na = bit (revcast (push_bit n w)) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma revcast_up [OF refl]:
  "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
    rc w = push_bit n (ucast w :: 'a::len word)" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps) apply auto apply (metis add.commute add_diff_cancel_right) apply (metis diff_add_inverse2 diff_diff_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; source_size rc + n = target_size rc\<rbrakk> \<Longrightarrow> rc w = push_bit n (ucast w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rc = revcast; LENGTH('b) + n = LENGTH('a)\<rbrakk> \<Longrightarrow> revcast w = push_bit n (ucast w) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('b) + n = LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (revcast w) na = bit (push_bit n (ucast w)) na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('b) + n = LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> (LENGTH('a) - LENGTH('b) \<le> na \<and> bit w (na + LENGTH('b) - LENGTH('a))) = (n \<le> na \<and> na - n < LENGTH('a) \<and> bit w (na - n)) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('b) + n = LENGTH('a); na < LENGTH('a); LENGTH('a) - LENGTH('b) \<le> na; bit w (na + LENGTH('b) - LENGTH('a))\<rbrakk> \<Longrightarrow> bit w (na - n)
 2. \<And>na. \<lbrakk>rc = revcast; LENGTH('b) + n = LENGTH('a); na < LENGTH('a); n \<le> na; na - n < LENGTH('a); bit w (na - n)\<rbrakk> \<Longrightarrow> bit w (na + LENGTH('b) - LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rc = revcast; LENGTH('b) + n = LENGTH('a); na < LENGTH('a); n \<le> na; na - n < LENGTH('a); bit w (na - n)\<rbrakk> \<Longrightarrow> bit w (na + LENGTH('b) - LENGTH('a)) proof (prove)
goal:
No subgoals!
theory More_Word

lemma word_ops_nth:
  fixes x y :: \<open>'a::len word\<close>
  shows
  word_or_nth:  "bit (x OR y) n = (bit x n \<or> bit y n)" and
  word_and_nth: "bit (x AND y) n = (bit x n \<and> bit y n)" and
  word_xor_nth: "bit (x XOR y) n = (bit x n \<noteq> bit y n)" by (simp_all add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (x OR y) n = (bit x n \<or> bit y n) &&& bit (x AND y) n = (bit x n \<and> bit y n) &&& bit (x XOR y) n = (bit x n \<noteq> bit y n)
theory More_Word

lemma less_1_helper:
  "n \<le> m \<Longrightarrow> (n - 1 :: int) < m" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> n - 1 < m
theory More_Word

lemma div_power_helper:
  "\<lbrakk> x \<le> y; y < LENGTH('a) \<rbrakk> \<Longrightarrow> (2 ^ y - 1) div (2 ^ x :: 'a::len word) = 2 ^ (y - x) - 1" apply (simp flip: mask_eq_exp_minus_1 drop_bit_eq_div) apply (rule bit_word_eqI) apply (auto simp add: bit_simps not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y < LENGTH('a)\<rbrakk> \<Longrightarrow> (2 ^ y - 1) div 2 ^ x = 2 ^ (y - x) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y < LENGTH('a)\<rbrakk> \<Longrightarrow> drop_bit x (mask y) = mask (y - x) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<le> y; y < LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (drop_bit x (mask y)) n = bit (mask (y - x)) n proof (prove)
goal:
No subgoals!
theory More_Word

lemma max_word_mask:
  "(- 1 :: 'a::len word) = mask LENGTH('a)" by (fact minus_1_eq_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 = mask LENGTH('a)
theory More_Word

lemma mask_out_first_mask_some:
  "\<lbrakk> x AND NOT (mask n) = y; n \<le> m \<rbrakk> \<Longrightarrow> x AND NOT (mask m) = y AND NOT (mask m)"
  for x y :: \<open>'a::len word\<close> by (rule bit_word_eqI) (auto simp add: bit_simps word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND NOT (mask n) = y; n \<le> m\<rbrakk> \<Longrightarrow> x AND NOT (mask m) = y AND NOT (mask m)
theory More_Word

lemma mask_lower_twice:
  "n \<le> m \<Longrightarrow> (x AND NOT (mask n)) AND NOT (mask m) = x AND NOT (mask m)"
  for x :: \<open>'a::len word\<close> by (rule bit_word_eqI) (auto simp add: bit_simps word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> (x AND NOT (mask n)) AND NOT (mask m) = x AND NOT (mask m)
theory More_Word

lemma mask_lower_twice2:
  "(a AND NOT (mask n)) AND NOT (mask m) = a AND NOT (mask (max n m))"
  for a :: \<open>'a::len word\<close> by (rule bit_word_eqI) (auto simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a AND NOT (mask n)) AND NOT (mask m) = a AND NOT (mask (max n m))
theory More_Word

lemma ucast_and_neg_mask:
  "ucast (x AND NOT (mask n)) = ucast x AND NOT (mask n)" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast (x AND NOT (mask n)) = ucast x AND NOT (mask n) proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (ucast (x AND NOT (mask n))) na = bit (ucast x AND NOT (mask n)) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma ucast_and_mask:
  "ucast (x AND mask n) = ucast x AND mask n" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast (x AND mask n) = ucast x AND mask n proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (ucast (x AND mask n)) na = bit (ucast x AND mask n) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma ucast_mask_drop:
  "LENGTH('a :: len) \<le> n \<Longrightarrow> (ucast (x AND mask n) :: 'a word) = ucast x" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> ucast (x AND mask n) = ucast x proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>LENGTH('a) \<le> n; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (ucast (x AND mask n)) na = bit (ucast x) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma mask_exceed:
  "n \<ge> LENGTH('a) \<Longrightarrow> (x::'a::len word) AND NOT (mask n) = 0" by (rule bit_word_eqI) (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> x AND NOT (mask n) = 0
theory More_Word

lemma word_add_no_overflow:"(x::'a::len word) < - 1 \<Longrightarrow> x < x + 1" using less_x_plus_1 order_less_le by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < - 1 \<Longrightarrow> x < x + 1 proof (prove)
using this:
?x \<noteq> - 1 \<Longrightarrow> (?y < ?x + 1) = (?y < ?x \<or> ?y = ?x)
(?x < ?y) = (?x \<le> ?y \<and> ?x \<noteq> ?y)

goal (1 subgoal):
 1. x < - 1 \<Longrightarrow> x < x + 1
theory More_Word

lemma lt_plus_1_le_word:
  fixes x :: "'a::len word"
  assumes bound:"n < unat (maxBound::'a word)"
  shows "x < 1 + of_nat n = (x \<le> of_nat n)" by (metis add.commute bound max_word_max word_Suc_leq word_not_le word_of_nat_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x < 1 + word_of_nat n) = (x \<le> word_of_nat n)
theory More_Word

lemma unat_ucast_up_simp:
  fixes x :: "'a::len word"
  assumes "LENGTH('a) \<le> LENGTH('b)"
  shows "unat (ucast x :: 'b::len word) = unat x" apply (rule bit_eqI) using assms apply (auto simp add: bit_simps dest: bit_imp_le_length) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (ucast x) = unat x proof (prove)
goal (1 subgoal):
 1. \<And>n. possible_bit TYPE(nat) n \<Longrightarrow> bit (unat (ucast x)) n = bit (unat x) n proof (prove)
using this:
LENGTH('a) \<le> LENGTH('b)

goal (1 subgoal):
 1. \<And>n. possible_bit TYPE(nat) n \<Longrightarrow> bit (unat (ucast x)) n = bit (unat x) n proof (prove)
goal:
No subgoals!
theory More_Word

lemma unat_ucast_less_no_overflow:
  "\<lbrakk>n < 2 ^ LENGTH('a); unat f < n\<rbrakk> \<Longrightarrow> (f::('a::len) word) < of_nat n" by (erule (1)  order_le_less_trans[OF _ of_nat_mono_maybe,rotated]) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ LENGTH('a); unat f < n\<rbrakk> \<Longrightarrow> f < word_of_nat n
theory More_Word

lemma unat_ucast_less_no_overflow_simp:
  "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat f < n) = ((f::('a::len) word) < of_nat n)" using unat_less_helper unat_ucast_less_no_overflow by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) \<Longrightarrow> (unat f < n) = (f < word_of_nat n) proof (prove)
using this:
?x < word_of_nat ?n \<Longrightarrow> unat ?x < ?n
\<lbrakk>?n < 2 ^ LENGTH(?'a); unat ?f < ?n\<rbrakk> \<Longrightarrow> ?f < word_of_nat ?n

goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) \<Longrightarrow> (unat f < n) = (f < word_of_nat n)
theory More_Word

lemma minus_one_word:
  "(-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 = 2 ^ LENGTH('a) - 1
theory More_Word

lemma le_2p_upper_bits:
  "\<lbrakk> (p::'a::len word) \<le> 2^n - 1; n < LENGTH('a) \<rbrakk> \<Longrightarrow>
  \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'" by (subst upper_bits_unset_is_l2p; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<le> 2 ^ n - 1; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'
theory More_Word

lemma le2p_bits_unset:
  "p \<le> 2 ^ n - 1 \<Longrightarrow> \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit (p::'a::len word) n'" using upper_bits_unset_is_l2p [where p=p] by (cases "n < LENGTH('a)") auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<le> 2 ^ n - 1 \<Longrightarrow> \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' proof (prove)
using this:
?n < LENGTH('a) \<Longrightarrow> (\<forall>n'\<ge>?n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n') = (p < 2 ^ ?n)

goal (1 subgoal):
 1. p \<le> 2 ^ n - 1 \<Longrightarrow> \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'
theory More_Word

lemma complement_nth_w2p:
  shows "n' < LENGTH('a) \<Longrightarrow> bit (NOT (2 ^ n :: 'a::len word)) n' = (n' \<noteq> n)" by (fastforce simp: word_ops_nth_size word_size nth_w2p)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' < LENGTH('a) \<Longrightarrow> bit (NOT (2 ^ n)) n' = (n' \<noteq> n)
theory More_Word

lemma word_unat_and_lt:
  "unat x < n \<or> unat y < n \<Longrightarrow> unat (x AND y) < n" by (meson le_less_trans word_and_le1 word_and_le2 word_le_nat_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < n \<or> unat y < n \<Longrightarrow> unat (x AND y) < n
theory More_Word

lemma word_unat_mask_lt:
  "m \<le> size w \<Longrightarrow> unat ((w::'a::len word) AND mask m) < 2 ^ m" by (rule word_unat_and_lt) (simp add: unat_mask word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> size w \<Longrightarrow> unat (w AND mask m) < 2 ^ m
theory More_Word

lemma word_sless_sint_le:"x <s y \<Longrightarrow> sint x \<le> sint y - 1" by (metis word_sless_alt zle_diff1_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x <s y \<Longrightarrow> sint x \<le> sint y - 1
theory More_Word

lemma upper_trivial:
  fixes x :: "'a::len word"
  shows "x \<noteq> 2 ^ LENGTH('a) - 1 \<Longrightarrow> x < 2 ^ LENGTH('a) - 1" by (simp add: less_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 2 ^ LENGTH('a) - 1 \<Longrightarrow> x < 2 ^ LENGTH('a) - 1
theory More_Word

lemma card_map_elide:
  "card ((of_nat :: nat \<Rightarrow> 'a::len word) ` {0..<n}) = card {0..<n}"
  if "n \<le> CARD('a::len word)" proof - let ?of_nat = "of_nat :: nat \<Rightarrow> 'a word" have "inj_on ?of_nat {i. i < CARD('a word)}" by (rule inj_onI) (simp add: card_word of_nat_inj) moreover have "{0..<n} \<subseteq> {i. i < CARD('a word)}" using that by auto ultimately have "inj_on ?of_nat {0..<n}" by (rule inj_on_subset) then show ?thesis by (simp add: card_image) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (state)
goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (state)
goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (prove)
goal (1 subgoal):
 1. inj_on word_of_nat {i. i < CARD('a word)} proof (state)
this:
inj_on word_of_nat {i. i < CARD('a word)}

goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (state)
this:
inj_on word_of_nat {i. i < CARD('a word)}

goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (prove)
goal (1 subgoal):
 1. {0..<n} \<subseteq> {i. i < CARD('a word)} proof (prove)
using this:
n \<le> CARD('a word)

goal (1 subgoal):
 1. {0..<n} \<subseteq> {i. i < CARD('a word)} proof (state)
this:
{0..<n} \<subseteq> {i. i < CARD('a word)}

goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (chain)
picking this:
inj_on word_of_nat {i. i < CARD('a word)}
{0..<n} \<subseteq> {i. i < CARD('a word)} proof (prove)
using this:
inj_on word_of_nat {i. i < CARD('a word)}
{0..<n} \<subseteq> {i. i < CARD('a word)}

goal (1 subgoal):
 1. inj_on word_of_nat {0..<n} proof (state)
this:
inj_on word_of_nat {0..<n}

goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (chain)
picking this:
inj_on word_of_nat {0..<n} proof (prove)
using this:
inj_on word_of_nat {0..<n}

goal (1 subgoal):
 1. card (word_of_nat ` {0..<n}) = card {0..<n} proof (state)
this:
card (word_of_nat ` {0..<n}) = card {0..<n}

goal:
No subgoals!
theory More_Word

lemma card_map_elide2:
  "n \<le> CARD('a::len word) \<Longrightarrow> card ((of_nat::nat \<Rightarrow> 'a::len word) ` {0..<n}) = n" by (subst card_map_elide) clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> CARD('a word) \<Longrightarrow> card (word_of_nat ` {0..<n}) = n
theory More_Word

lemma eq_ucast_ucast_eq:
  "LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> x = ucast y \<Longrightarrow> ucast x = y"
  for x :: "'a::len word" and y :: "'b::len word" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) \<le> LENGTH('a); x = ucast y\<rbrakk> \<Longrightarrow> ucast x = y
theory More_Word

lemma less_ucast_ucast_less:
  "LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> x < ucast y \<Longrightarrow> ucast x < y"
  for x :: "'a::len word" and y :: "'b::len word" by (metis ucast_nat_def unat_mono unat_ucast_up_simp word_of_nat_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) \<le> LENGTH('a); x < ucast y\<rbrakk> \<Longrightarrow> ucast x < y
theory More_Word

lemma ucast_le_ucast:
  "LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (ucast x \<le> (ucast y::'b::len word)) = (x \<le> y)"
  for x :: "'a::len word" by (simp add: unat_arith_simps(1) unat_ucast_up_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (ucast x \<le> ucast y) = (x \<le> y)