kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Divides

lemma power_sub:
  fixes a :: nat
  assumes lt: "n \<le> m"
  and     av: "0 < a"
  shows "a ^ (m - n) = a ^ m div a ^ n" proof (subst nat_mult_eq_cancel1 [symmetric]) show "(0::nat) < a ^ n" using av by simp next from lt obtain q where mv: "n + q = m" by (auto simp: le_iff_add) have "a ^ n * (a ^ m div a ^ n) = a ^ m" proof (subst mult.commute) have "a ^ m = (a ^ m div a ^ n) * a ^ n + a ^ m mod a ^ n" by (rule  div_mult_mod_eq [symmetric]) moreover have "a ^ m mod a ^ n = 0" by (subst mod_eq_0_iff_dvd, subst dvd_def, rule exI [where x = "a ^ q"],
      (subst power_add [symmetric] mv)+, rule refl) ultimately show "(a ^ m div a ^ n) * a ^ n = a ^ m" by simp qed then show "a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n)" using lt by (simp add: power_add [symmetric]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a ^ (m - n) = a ^ m div a ^ n proof (state)
goal (2 subgoals):
 1. 0 < ?k
 2. ?k * a ^ (m - n) = ?k * (a ^ m div a ^ n) proof (prove)
goal (1 subgoal):
 1. 0 < a ^ n proof (prove)
using this:
0 < a

goal (1 subgoal):
 1. 0 < a ^ n proof (state)
this:
0 < a ^ n

goal (1 subgoal):
 1. a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n) proof (state)
goal (1 subgoal):
 1. a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n) proof (chain)
picking this:
n \<le> m proof (prove)
using this:
n \<le> m

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

goal (1 subgoal):
 1. a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n) proof (prove)
goal (1 subgoal):
 1. a ^ n * (a ^ m div a ^ n) = a ^ m proof (state)
goal (1 subgoal):
 1. a ^ m div a ^ n * a ^ n = a ^ m proof (prove)
goal (1 subgoal):
 1. a ^ m = a ^ m div a ^ n * a ^ n + a ^ m mod a ^ n proof (state)
this:
a ^ m = a ^ m div a ^ n * a ^ n + a ^ m mod a ^ n

goal (1 subgoal):
 1. a ^ m div a ^ n * a ^ n = a ^ m proof (state)
this:
a ^ m = a ^ m div a ^ n * a ^ n + a ^ m mod a ^ n

goal (1 subgoal):
 1. a ^ m div a ^ n * a ^ n = a ^ m proof (prove)
goal (1 subgoal):
 1. a ^ m mod a ^ n = 0 proof (state)
this:
a ^ m mod a ^ n = 0

goal (1 subgoal):
 1. a ^ m div a ^ n * a ^ n = a ^ m proof (chain)
picking this:
a ^ m = a ^ m div a ^ n * a ^ n + a ^ m mod a ^ n
a ^ m mod a ^ n = 0 proof (prove)
using this:
a ^ m = a ^ m div a ^ n * a ^ n + a ^ m mod a ^ n
a ^ m mod a ^ n = 0

goal (1 subgoal):
 1. a ^ m div a ^ n * a ^ n = a ^ m proof (state)
this:
a ^ m div a ^ n * a ^ n = a ^ m

goal:
No subgoals! proof (state)
this:
a ^ n * (a ^ m div a ^ n) = a ^ m

goal (1 subgoal):
 1. a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n) proof (chain)
picking this:
a ^ n * (a ^ m div a ^ n) = a ^ m proof (prove)
using this:
a ^ n * (a ^ m div a ^ n) = a ^ m

goal (1 subgoal):
 1. a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n) proof (prove)
using this:
a ^ n * (a ^ m div a ^ n) = a ^ m
n \<le> m

goal (1 subgoal):
 1. a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n) proof (state)
this:
a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n)

goal:
No subgoals!
theory More_Divides

lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c" apply (cut_tac m = q and n = c in mod_less_divisor) apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto) apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst) apply (simp add: add_mult_distrib2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < c; r < b\<rbrakk> \<Longrightarrow> b * (q mod c) + r < b * c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < c; r < b\<rbrakk> \<Longrightarrow> 0 < c
 2. \<lbrakk>0 < c; r < b; q mod c < c\<rbrakk> \<Longrightarrow> b * (q mod c) + r < b * c proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>r < b; c = Suc (q mod c + k)\<rbrakk> \<Longrightarrow> b * (q mod c) + r < b * c proof (prove)
goal (1 subgoal):
 1. \<And>k. r < b \<Longrightarrow> b * (q mod c) + r < b * Suc (q mod c + k) proof (prove)
goal:
No subgoals!
theory More_Divides

lemma less_two_pow_divD:
  "\<lbrakk> (x :: nat) < 2 ^ n div 2 ^ m \<rbrakk>
    \<Longrightarrow> n \<ge> m \<and> (x < 2 ^ (n - m))" apply (rule context_conjI) apply (rule ccontr) apply (simp add: power_strict_increasing) apply (simp add: power_sub) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ n div 2 ^ m \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. x < 2 ^ n div 2 ^ m \<Longrightarrow> m \<le> n
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; m \<le> n\<rbrakk> \<Longrightarrow> x < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> m \<le> n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; m \<le> n\<rbrakk> \<Longrightarrow> x < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n div 2 ^ m; m \<le> n\<rbrakk> \<Longrightarrow> x < 2 ^ (n - m) proof (prove)
goal:
No subgoals!
theory More_Divides

lemma less_two_pow_divI:
  "\<lbrakk> (x :: nat) < 2 ^ (n - m); m \<le> n \<rbrakk> \<Longrightarrow> x < 2 ^ n div 2 ^ m" by (simp add: power_sub)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ (n - m); m \<le> n\<rbrakk> \<Longrightarrow> x < 2 ^ n div 2 ^ m
theory More_Divides

lemma mod_div_equality_div_eq:
  "a div b * b = (a - (a mod b) :: int)" by (simp add: field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a div b * b = a - a mod b
theory More_Divides

lemma zmod_helper:
  "n mod m = k \<Longrightarrow> ((n :: int) + a) mod m = (k + a) mod m" by (metis add.commute mod_add_right_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n mod m = k \<Longrightarrow> (n + a) mod m = (k + a) mod m
theory More_Divides

lemma power_minus_is_div:
  "b \<le> a \<Longrightarrow> (2 :: nat) ^ (a - b) = 2 ^ a div 2 ^ b" apply (induct a arbitrary: b) apply simp apply (erule le_SucE) apply (clarsimp simp:Suc_diff_le le_iff_add power_add) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b proof (prove)
goal (2 subgoals):
 1. \<And>b. b \<le> 0 \<Longrightarrow> 2 ^ (0 - b) = 2 ^ 0 div 2 ^ b
 2. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b \<le> Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b \<le> Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b \<le> a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b
 2. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b = Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>b. b \<le> a \<Longrightarrow> 2 ^ (a - b) = 2 ^ a div 2 ^ b; b = Suc a\<rbrakk> \<Longrightarrow> 2 ^ (Suc a - b) = 2 ^ Suc a div 2 ^ b proof (prove)
goal:
No subgoals!
theory More_Divides

lemma two_pow_div_gt_le:
  "v < 2 ^ n div (2 ^ m :: nat) \<Longrightarrow> m \<le> n" by (clarsimp dest!: less_two_pow_divD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v < 2 ^ n div 2 ^ m \<Longrightarrow> m \<le> n
theory More_Divides

lemma td_gal_lt:
  \<open>0 < c \<Longrightarrow> a < b * c \<longleftrightarrow> a div c < b\<close>
  for a b c :: nat by (simp add: div_less_iff_less_mult)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (a < b * c) = (a div c < b)
theory More_Divides

lemma td_gal:
  \<open>0 < c \<Longrightarrow> b * c \<le> a  \<longleftrightarrow> b \<le> a div c\<close>
  for a b c :: nat by (simp add: less_eq_div_iff_mult_less_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (b * c \<le> a) = (b \<le> a div c)
theory More_Bit_Ring

lemma disjunctive_add2:
  "(x AND y) = 0 \<Longrightarrow> x + y = x OR y" by (metis disjunctive_add bit_0_eq bit_and_iff bot_apply bot_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND y = (0::'a) \<Longrightarrow> x + y = x OR y
theory More_Bit_Ring

lemma not_xor_is_eqv:
  "NOT (x XOR y) = (x AND y) OR (NOT x AND NOT y)" by (simp add: bit.xor_def bit.disj_conj_distrib or.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (x XOR y) = x AND y OR NOT x AND NOT y
theory More_Bit_Ring

lemma not_xor_eq_xor_not:
  "(NOT x) XOR y = x XOR (NOT y)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT x XOR y = x XOR NOT y
theory More_Bit_Ring

lemma minus_not_eq_plus_1:
  "- NOT x = x + 1" by (simp add: minus_eq_not_plus_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - NOT x = x + (1::'a)
theory More_Bit_Ring

lemma not_minus_eq_minus_1:
  "NOT (- x) = x - 1" by (simp add: not_eq_complement)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (- x) = x - (1::'a)
theory More_Bit_Ring

lemma and_plus_not_and:
  "(x AND y) + (x AND NOT y) = x" by (metis and.left_commute and.right_neutral bit.conj_cancel_right bit.conj_disj_distrib
            bit.conj_zero_right bit.disj_cancel_right disjunctive_add2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND y) + (x AND NOT y) = x
theory More_Bit_Ring

lemma and_eq_not_or_minus:
  "x AND y = (NOT x OR y) - NOT x" by (metis and.idem and_eq_not_not_or eq_diff_eq or.commute or.idem or_eq_and_not_plus)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND y = (NOT x OR y) - NOT x
theory More_Bit_Ring

lemma and_not_eq_or_minus:
  "x AND NOT y = (x OR y) - y" by (simp add: or_eq_and_not_plus)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND NOT y = (x OR y) - y
theory More_Bit_Ring

lemma and_not_eq_minus_and:
  "x AND NOT y = x - (x AND y)" by (simp add: add.commute eq_diff_eq and_plus_not_and)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND NOT y = x - (x AND y)
theory More_Bit_Ring

lemma or_minus_eq_minus_and:
  "(x OR y) - y = x - (x AND y)" by (metis and_not_eq_minus_and and_not_eq_or_minus)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x OR y) - y = x - (x AND y)
theory More_Bit_Ring

lemma plus_eq_and_or:
  "x + y = (x OR y) + (x AND y)" using add_commute local.add.semigroup_axioms or_eq_and_not_plus semigroup.assoc by (fastforce simp: and_plus_not_and)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + y = (x OR y) + (x AND y) proof (prove)
using this:
?a + ?b = ?b + ?a
semigroup (+)
?x OR ?y = (?x AND NOT ?y) + ?y
semigroup ?f \<Longrightarrow> ?f (?f ?a ?b) ?c = ?f ?a (?f ?b ?c)

goal (1 subgoal):
 1. x + y = (x OR y) + (x AND y)
theory More_Bit_Ring

lemma xor_eq_or_minus_and:
  "x XOR y = (x OR y) - (x AND y)" by (metis (no_types) bit.de_Morgan_conj bit.xor_def2 bit_and_iff bit_or_iff disjunctive_diff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x XOR y = (x OR y) - (x AND y)
theory More_Bit_Ring

lemma not_xor_eq_and_plus_not_or:
  "NOT (x XOR y) = (x AND y) + NOT (x OR y)" by (metis (no_types, lifting) not_diff_distrib add.commute bit.de_Morgan_conj bit.xor_def2
                                bit_and_iff bit_or_iff disjunctive_diff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (x XOR y) = (x AND y) + NOT (x OR y)
theory More_Bit_Ring

lemma not_xor_eq_and_minus_or:
  "NOT (x XOR y) = (x AND y) - (x OR y) - 1" by (metis not_diff_distrib add.commute minus_diff_eq not_minus_eq_minus_1 not_xor_eq_and_plus_not_or)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (x XOR y) = (x AND y) - (x OR y) - (1::'a)
theory More_Bit_Ring

lemma plus_eq_xor_plus_carry:
  "x + y = (x XOR y) + 2 * (x AND y)" by (metis plus_eq_and_or add.commute add.left_commute diff_add_cancel mult_2 xor_eq_or_minus_and)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + y = (x XOR y) + (2::'a) * (x AND y)
theory More_Bit_Ring

lemma plus_eq_or_minus_xor:
  "x + y = 2 * (x OR y) - (x XOR y)" by (metis add_diff_cancel_left' diff_diff_eq2 local.mult_2 plus_eq_and_or xor_eq_or_minus_and)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + y = (2::'a) * (x OR y) - (x XOR y)
theory More_Bit_Ring

lemma plus_eq_minus_neg:
  "x + y = x - NOT y - 1" using add_commute local.not_diff_distrib not_minus by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + y = x - NOT y - (1::'a) proof (prove)
using this:
?a + ?b = ?b + ?a
NOT (?a - ?b) = NOT ?a + ?b
NOT (?x - ?y) = ?y - ?x - (1::'a)

goal (1 subgoal):
 1. x + y = x - NOT y - (1::'a)
theory More_Bit_Ring

lemma minus_eq_plus_neg:
  "x - y = x + NOT y + 1" by (simp add: add.semigroup_axioms diff_conv_add_uminus minus_eq_not_plus_1 semigroup.assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x - y = x + NOT y + (1::'a)
theory More_Bit_Ring

lemma minus_eq_and_not_minus_not_and:
  "x - y = (x AND NOT y) - (NOT x AND y)" by (metis bit.de_Morgan_conj bit.double_compl not_diff_distrib plus_eq_and_or)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x - y = (x AND NOT y) - (NOT x AND y)
theory More_Bit_Ring

lemma minus_eq_xor_minus_not_and:
  "x - y = (x XOR y) - 2 * (NOT x AND y)" by (metis (no_types) bit.compl_eq_compl_iff bit.xor_compl_left not_diff_distrib
                       plus_eq_xor_plus_carry)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x - y = (x XOR y) - (2::'a) * (NOT x AND y)
theory More_Bit_Ring

lemma minus_eq_and_not_minus_xor:
  "x - y = 2 * (x AND NOT y) - (x XOR y)" by (metis and.commute minus_diff_eq minus_eq_xor_minus_not_and xor.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x - y = (2::'a) * (x AND NOT y) - (x XOR y)
theory More_Bit_Ring

lemma and_one_neq_simps[simp]:
  "x AND 1 \<noteq> 0 \<longleftrightarrow> x AND 1 = 1"
  "x AND 1 \<noteq> 1 \<longleftrightarrow> x AND 1 = 0" by (clarsimp simp: and_one_eq)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND (1::'a) \<noteq> (0::'a)) = (x AND (1::'a) = (1::'a)) &&& (x AND (1::'a) \<noteq> (1::'a)) = (x AND (1::'a) = (0::'a))
theory More_Word

lemma unat_power_lower [simp]:
  "unat ((2::'a::len word) ^ n) = 2 ^ n" if "n < LENGTH('a::len)" using that by transfer simp

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

goal (1 subgoal):
 1. unat (2 ^ n) = 2 ^ n
theory More_Word

lemma word_div_lt_eq_0:
  "x < y \<Longrightarrow> x div y = 0" for x :: "'a :: len word" by (fact div_word_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> x div y = 0
theory More_Word

lemma word_div_eq_1_iff: "n div m = 1 \<longleftrightarrow> n \<ge> m \<and> unat n < 2 * unat (m :: 'a :: len word)" apply (simp only: word_arith_nat_defs word_le_nat_alt word_of_nat_eq_iff flip: nat_div_eq_Suc_0_iff) apply (simp flip: unat_div unsigned_take_bit_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n div m = 1) = (m \<le> n \<and> unat n < 2 * unat m) proof (prove)
goal (1 subgoal):
 1. (take_bit LENGTH('a) (unat n div unat m) = take_bit LENGTH('a) (Suc 0)) = (unat n div unat m = Suc 0) proof (prove)
goal:
No subgoals!
theory More_Word

lemma AND_twice [simp]:
  "(w AND m) AND m = w AND m" by (fact and.right_idem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w AND m) AND m = w AND m
theory More_Word

lemma word_combine_masks:
  "w AND m = z \<Longrightarrow> w AND m' = z' \<Longrightarrow> w AND (m OR m') = (z OR z')"
  for w m m' z z' :: \<open>'a::len word\<close> by (simp add: bit.conj_disj_distrib)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w AND m = z; w AND m' = z'\<rbrakk> \<Longrightarrow> w AND (m OR m') = z OR z'
theory More_Word

lemma p2_gt_0:
  "(0 < (2 ^ n :: 'a :: len word)) = (n < LENGTH('a))" by (simp add : word_gt_0 not_le)

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

lemma uint_2p_alt:
  \<open>n < LENGTH('a::len) \<Longrightarrow> uint ((2::'a::len word) ^ n) = 2 ^ n\<close> using p2_gt_0 [of n, where ?'a = 'a] by (simp add: uint_2p)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> uint (2 ^ n) = 2 ^ n proof (prove)
using this:
(0 < 2 ^ n) = (n < LENGTH('a))

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

lemma p2_eq_0:
  \<open>(2::'a::len word) ^ n = 0 \<longleftrightarrow> LENGTH('a::len) \<le> n\<close> by (fact exp_eq_zero_iff)

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

lemma p2len:
  \<open>(2 :: 'a word) ^ LENGTH('a::len) = 0\<close> by (fact word_pow_0)

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

lemma neg_mask_is_div:
  "w AND NOT (mask n) = (w div 2^n) * 2^n"
  for w :: \<open>'a::len word\<close> by (rule bit_word_eqI)
    (auto simp add: bit_simps simp flip: push_bit_eq_mult drop_bit_eq_div)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w AND NOT (mask n) = w div 2 ^ n * 2 ^ n
theory More_Word

lemma neg_mask_is_div':
  "n < size w \<Longrightarrow> w AND NOT (mask n) = ((w div (2 ^ n)) * (2 ^ n))"
  for w :: \<open>'a::len word\<close> by (rule neg_mask_is_div)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < size w \<Longrightarrow> w AND NOT (mask n) = w div 2 ^ n * 2 ^ n
theory More_Word

lemma and_mask_arith:
  "w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
  for w :: \<open>'a::len word\<close> by (rule bit_word_eqI)
    (auto simp add: bit_simps word_size simp flip: push_bit_eq_mult drop_bit_eq_div)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w AND mask n = w * 2 ^ (size w - n) div 2 ^ (size w - n)
theory More_Word

lemma and_mask_arith':
  "0 < n \<Longrightarrow> w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
  for w :: \<open>'a::len word\<close> by (rule and_mask_arith)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> w AND mask n = w * 2 ^ (size w - n) div 2 ^ (size w - n)
theory More_Word

lemma mask_2pm1: "mask n = 2 ^ n - (1 :: 'a::len word)" by (fact mask_eq_decr_exp)

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

lemma word_and_mask_le_2pm1: "w AND mask n \<le> 2 ^ n - 1"
  for w :: \<open>'a::len word\<close> by (simp add: mask_2pm1[symmetric] word_and_le1)

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

lemma is_aligned_AND_less_0:
  "u AND mask n = 0 \<Longrightarrow> v < 2^n \<Longrightarrow> u AND v = 0"
  for u v :: \<open>'a::len word\<close> apply (drule less_mask_eq) apply (simp flip: take_bit_eq_mask) apply (simp add: bit_eq_iff) apply (auto simp add: bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u AND mask n = 0; v < 2 ^ n\<rbrakk> \<Longrightarrow> u AND v = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u AND mask n = 0; v AND mask n = v\<rbrakk> \<Longrightarrow> u AND v = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_bit n u = 0; take_bit n v = v\<rbrakk> \<Longrightarrow> u AND v = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>na<LENGTH('a). \<not> bit (take_bit n u) na; \<forall>na<LENGTH('a). bit (take_bit n v) na = bit v na\<rbrakk> \<Longrightarrow> \<forall>n<LENGTH('a). \<not> bit (u AND v) n proof (prove)
goal:
No subgoals!
theory More_Word

lemma and_mask_eq_iff_le_mask:
  \<open>w AND mask n = w \<longleftrightarrow> w \<le> mask n\<close>
  for w :: \<open>'a::len word\<close> apply (simp flip: take_bit_eq_mask) apply (cases \<open>n \<ge> LENGTH('a)\<close>; transfer) apply (simp_all add: not_le min_def) apply (simp_all add: mask_eq_exp_minus_1) apply auto apply (metis take_bit_int_less_exp) apply (metis min_def nat_less_le take_bit_int_eq_self_iff take_bit_take_bit) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w AND mask n = w) = (w \<le> mask n) proof (prove)
goal (1 subgoal):
 1. (take_bit n w = w) = (w \<le> mask n) proof (prove)
goal (2 subgoals):
 1. \<And>n w. LENGTH('a) \<le> n \<Longrightarrow> (take_bit LENGTH('a) (take_bit (min LENGTH('a) n) w) = take_bit LENGTH('a) w) = (take_bit LENGTH('a) w \<le> take_bit LENGTH('a) (mask n))
 2. \<And>n w. \<not> LENGTH('a) \<le> n \<Longrightarrow> (take_bit LENGTH('a) (take_bit (min LENGTH('a) n) w) = take_bit LENGTH('a) w) = (take_bit LENGTH('a) w \<le> take_bit LENGTH('a) (mask n)) proof (prove)
goal (2 subgoals):
 1. \<And>n w. LENGTH('a) \<le> n \<Longrightarrow> take_bit LENGTH('a) w \<le> mask LENGTH('a)
 2. \<And>n w. n < LENGTH('a) \<Longrightarrow> (take_bit n w = take_bit LENGTH('a) w) = (take_bit LENGTH('a) w \<le> mask n) proof (prove)
goal (1 subgoal):
 1. \<And>n w. n < LENGTH('a) \<Longrightarrow> (take_bit n w = take_bit LENGTH('a) w) = (take_bit LENGTH('a) w < 2 ^ n) proof (prove)
goal (2 subgoals):
 1. \<And>n w. \<lbrakk>n < LENGTH('a); take_bit n w = take_bit LENGTH('a) w\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) w < 2 ^ n
 2. \<And>n w. \<lbrakk>n < LENGTH('a); take_bit LENGTH('a) w < 2 ^ n\<rbrakk> \<Longrightarrow> take_bit n w = take_bit LENGTH('a) w proof (prove)
goal (1 subgoal):
 1. \<And>n w. \<lbrakk>n < LENGTH('a); take_bit LENGTH('a) w < 2 ^ n\<rbrakk> \<Longrightarrow> take_bit n w = take_bit LENGTH('a) w proof (prove)
goal:
No subgoals!
theory More_Word

lemma less_eq_mask_iff_take_bit_eq_self:
  \<open>w \<le> mask n \<longleftrightarrow> take_bit n w = w\<close>
  for w :: \<open>'a::len word\<close> by (simp add: and_mask_eq_iff_le_mask take_bit_eq_mask)

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

lemma NOT_eq:
  "NOT (x :: 'a :: len word) = - x - 1" by (fact not_eq_complement)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT x = - x - 1
theory More_Word

lemma NOT_mask: "NOT (mask n :: 'a::len word) = - (2 ^ n)" by (simp add : NOT_eq mask_2pm1)

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

lemma le_m1_iff_lt: "(x > (0 :: 'a :: len word)) = ((y \<le> x - 1) = (y < x))" by uint_arith

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

lemma gt0_iff_gem1:
  \<open>0 < x \<longleftrightarrow> x - 1 < x\<close>
  for x :: \<open>'a::len word\<close> by (metis add.right_neutral diff_add_cancel less_irrefl measure_unat unat_arith_simps(2) word_neq_0_conv word_sub_less_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 < x) = (x - 1 < x)
theory More_Word

lemma power_2_ge_iff:
  \<open>2 ^ n - (1 :: 'a::len word) < 2 ^ n \<longleftrightarrow> n < LENGTH('a)\<close> using gt0_iff_gem1 p2_gt_0 by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 ^ n - 1 < 2 ^ n) = (n < LENGTH('a)) proof (prove)
using this:
(0 < ?x) = (?x - 1 < ?x)
(0 < 2 ^ ?n) = (?n < LENGTH(?'a))

goal (1 subgoal):
 1. (2 ^ n - 1 < 2 ^ n) = (n < LENGTH('a))
theory More_Word

lemma le_mask_iff_lt_2n:
  "n < len_of TYPE ('a) = (((w :: 'a :: len word) \<le> mask n) = (w < 2 ^ n))" unfolding mask_2pm1 by (rule trans [OF p2_gt_0 [THEN sym] le_m1_iff_lt])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n < LENGTH('a)) = ((w \<le> mask n) = (w < 2 ^ n)) proof (prove)
goal (1 subgoal):
 1. (n < LENGTH('a)) = ((w \<le> 2 ^ n - 1) = (w < 2 ^ n))
theory More_Word

lemma mask_lt_2pn:
  \<open>n < LENGTH('a) \<Longrightarrow> mask n < (2 :: 'a::len word) ^ n\<close> by (simp add: mask_eq_exp_minus_1 power_2_ge_iff)

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

lemma word_unat_power:
  "(2 :: 'a :: len word) ^ n = of_nat (2 ^ n)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ n = word_of_nat (2 ^ n)