kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Arithmetic

lemma n_less_equal_power_2:
  "n < 2 ^ n" by (fact less_exp)

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

lemma min_pm [simp]: "min a b + (a - b) = a"
  for a b :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. min a b + (a - b) = a
theory More_Arithmetic

lemma min_pm1 [simp]: "a - b + min a b = a"
  for a b :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a - b + min a b = a
theory More_Arithmetic

lemma rev_min_pm [simp]: "min b a + (a - b) = a"
  for a b :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. min b a + (a - b) = a
theory More_Arithmetic

lemma rev_min_pm1 [simp]: "a - b + min b a = a"
  for a b :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a - b + min b a = a
theory More_Arithmetic

lemma min_minus' [simp]: "min (m - k) m = m - k"
  for m k :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. min (m - k) m = m - k
theory More_Arithmetic

lemma nat_less_power_trans:
  fixes n :: nat
  assumes nv: "n < 2 ^ (m - k)"
  and     kv: "k \<le> m"
  shows "2 ^ k * n < 2 ^ m" proof (rule order_less_le_trans) show "2 ^ k * n < 2 ^ k * 2 ^ (m - k)" by (rule mult_less_mono2 [OF nv zero_less_power]) simp show "(2::nat) ^ k * 2 ^ (m - k) \<le> 2 ^ m" using nv kv by (subst power_add [symmetric]) simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * n < 2 ^ m proof (state)
goal (2 subgoals):
 1. 2 ^ k * n < ?y
 2. ?y \<le> 2 ^ m proof (prove)
goal (1 subgoal):
 1. 2 ^ k * n < 2 ^ k * 2 ^ (m - k) proof (state)
this:
2 ^ k * n < 2 ^ k * 2 ^ (m - k)

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

goal (1 subgoal):
 1. 2 ^ k * 2 ^ (m - k) \<le> 2 ^ m proof (state)
this:
2 ^ k * 2 ^ (m - k) \<le> 2 ^ m

goal:
No subgoals!
theory More_Arithmetic

lemma nat_le_power_trans:
  fixes n :: nat
  shows "\<lbrakk>n \<le> 2 ^ (m - k); k \<le> m\<rbrakk> \<Longrightarrow> 2 ^ k * n \<le> 2 ^ m" by (metis le_add_diff_inverse mult_le_mono2 semiring_normalization_rules(26))

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

lemma nat_add_offset_less:
  fixes x :: nat
  assumes yv: "y < 2 ^ n"
  and     xv: "x < 2 ^ m"
  and     mn: "sz = m + n"
  shows   "x * 2 ^ n + y < 2 ^ sz" proof (subst mn) from yv obtain qy where "y + qy = 2 ^ n" and "0 < qy" by (auto dest: less_imp_add_positive) have "x * 2 ^ n + y < x * 2 ^ n + 2 ^ n" by simp fact+ also have "\<dots> = (x + 1) * 2 ^ n" by simp also have "\<dots> \<le> 2 ^ (m + n)" using xv by (subst power_add) (rule mult_le_mono1, simp) finally show "x * 2 ^ n + y < 2 ^ (m + n)" . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ sz proof (state)
goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (chain)
picking this:
y < 2 ^ n proof (prove)
using this:
y < 2 ^ n

goal (1 subgoal):
 1. (\<And>qy. \<lbrakk>y + qy = 2 ^ n; 0 < qy\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
y + qy = 2 ^ n
0 < qy

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n + y < x * 2 ^ n + 2 ^ n proof (state)
this:
x * 2 ^ n + y < x * 2 ^ n + 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (state)
this:
x * 2 ^ n + y < x * 2 ^ n + 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n + 2 ^ n = (x + 1) * 2 ^ n proof (state)
this:
x * 2 ^ n + 2 ^ n = (x + 1) * 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (state)
this:
x * 2 ^ n + 2 ^ n = (x + 1) * 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (prove)
goal (1 subgoal):
 1. (x + 1) * 2 ^ n \<le> 2 ^ (m + n) proof (prove)
using this:
x < 2 ^ m

goal (1 subgoal):
 1. (x + 1) * 2 ^ n \<le> 2 ^ (m + n) proof (state)
this:
(x + 1) * 2 ^ n \<le> 2 ^ (m + n)

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (chain)
picking this:
x * 2 ^ n + y < 2 ^ (m + n) proof (prove)
using this:
x * 2 ^ n + y < 2 ^ (m + n)

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (state)
this:
x * 2 ^ n + y < 2 ^ (m + n)

goal:
No subgoals!
theory More_Arithmetic

lemma power_2_mult_step_le:
  "\<lbrakk>n' \<le> n; 2 ^ n' * k' < 2 ^ n * k\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * (k::nat)" apply (cases "n'=n", simp) apply (metis Suc_leI le_refl mult_Suc_right mult_le_mono semiring_normalization_rules(7)) apply (drule (1) le_neq_trans) apply clarsimp apply (subgoal_tac "\<exists>m. n = n' + m") prefer 2 apply (simp add: le_Suc_ex) apply (clarsimp simp: power_add) apply (metis Suc_leI mult.assoc mult_Suc_right nat_mult_le_cancel_disj) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; 2 ^ n' * k' < 2 ^ n * k\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k' < k; n' = n\<rbrakk> \<Longrightarrow> 2 ^ n + 2 ^ n * k' \<le> 2 ^ n * k
 2. \<lbrakk>n' \<le> n; 2 ^ n' * k' < 2 ^ n * k; n' \<noteq> n\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; 2 ^ n' * k' < 2 ^ n * k; n' \<noteq> n\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n' * k' < 2 ^ n * k; n' \<noteq> n; n' < n\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n' * k' < 2 ^ n * k; n' < n\<rbrakk> \<Longrightarrow> 2 ^ n' + 2 ^ n' * k' \<le> 2 ^ n * k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 ^ n' * k' < 2 ^ n * k; n' < n; \<exists>m. n = n' + m\<rbrakk> \<Longrightarrow> 2 ^ n' + 2 ^ n' * k' \<le> 2 ^ n * k
 2. \<lbrakk>2 ^ n' * k' < 2 ^ n * k; n' < n\<rbrakk> \<Longrightarrow> \<exists>m. n = n' + m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 ^ n' * k' < 2 ^ n * k; n' < n\<rbrakk> \<Longrightarrow> \<exists>m. n = n' + m
 2. \<lbrakk>2 ^ n' * k' < 2 ^ n * k; n' < n; \<exists>m. n = n' + m\<rbrakk> \<Longrightarrow> 2 ^ n' + 2 ^ n' * k' \<le> 2 ^ n * k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n' * k' < 2 ^ n * k; n' < n; \<exists>m. n = n' + m\<rbrakk> \<Longrightarrow> 2 ^ n' + 2 ^ n' * k' \<le> 2 ^ n * k proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>k' < 2 ^ m * k; 0 < m; n = n' + m\<rbrakk> \<Longrightarrow> 2 ^ n' + 2 ^ n' * k' \<le> 2 ^ n' * 2 ^ m * k proof (prove)
goal:
No subgoals!
theory More_Arithmetic

lemma nat_mult_power_less_eq:
  "b > 0 \<Longrightarrow> (a * b ^ n < (b :: nat) ^ m) = (a < b ^ (m - n))" using mult_less_cancel2[where m = a and k = "b ^ n" and n="b ^ (m - n)"]
        mult_less_cancel2[where m="a * b ^ (n - m)" and k="b ^ m" and n=1] apply (simp only: power_add[symmetric] nat_minus_add_max) apply (simp only: power_add[symmetric] nat_minus_add_max ac_simps) apply (simp add: max_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < b \<Longrightarrow> (a * b ^ n < b ^ m) = (a < b ^ (m - n)) proof (prove)
using this:
(a * b ^ n < b ^ (m - n) * b ^ n) = (0 < b ^ n \<and> a < b ^ (m - n))
(a * b ^ (n - m) * b ^ m < 1 * b ^ m) = (0 < b ^ m \<and> a * b ^ (n - m) < 1)

goal (1 subgoal):
 1. 0 < b \<Longrightarrow> (a * b ^ n < b ^ m) = (a < b ^ (m - n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < b; (a * b ^ n < b ^ max m n) = (0 < b ^ n \<and> a < b ^ (m - n)); (a * b ^ (n - m) * b ^ m < 1 * b ^ m) = (0 < b ^ m \<and> a * b ^ (n - m) < 1)\<rbrakk> \<Longrightarrow> (a * b ^ n < b ^ m) = (a < b ^ (m - n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < b; (a * b ^ n < b ^ max m n) = (0 < b ^ n \<and> a < b ^ (m - n)); (a * b ^ (m + (n - m)) < 1 * b ^ m) = (0 < b ^ m \<and> a * b ^ (n - m) < 1)\<rbrakk> \<Longrightarrow> (a * b ^ n < b ^ m) = (a < b ^ (m - n)) proof (prove)
goal:
No subgoals!
theory More_Arithmetic

lemma diff_diff_less:
  "(i < m - (m - (n :: nat))) = (i < m \<and> i < n)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (i < m - (m - n)) = (i < m \<and> i < n)
theory More_Arithmetic

lemma small_powers_of_2:
  \<open>x < 2 ^ (x - 1)\<close> if \<open>x \<ge> 3\<close> for x :: nat proof - define m where \<open>m = x - 3\<close> with that have \<open>x = m + 3\<close> by simp moreover have \<open>m + 3 < 4 * 2 ^ m\<close> by (induction m) simp_all ultimately show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ (x - 1) proof (state)
goal (1 subgoal):
 1. x < 2 ^ (x - 1) proof (state)
this:
m = x - 3

goal (1 subgoal):
 1. x < 2 ^ (x - 1) proof (chain)
picking this:
3 \<le> x
m = x - 3 proof (prove)
using this:
3 \<le> x
m = x - 3

goal (1 subgoal):
 1. x = m + 3 proof (state)
this:
x = m + 3

goal (1 subgoal):
 1. x < 2 ^ (x - 1) proof (state)
this:
x = m + 3

goal (1 subgoal):
 1. x < 2 ^ (x - 1) proof (prove)
goal (1 subgoal):
 1. m + 3 < 4 * 2 ^ m proof (state)
this:
m + 3 < 4 * 2 ^ m

goal (1 subgoal):
 1. x < 2 ^ (x - 1) proof (chain)
picking this:
x = m + 3
m + 3 < 4 * 2 ^ m proof (prove)
using this:
x = m + 3
m + 3 < 4 * 2 ^ m

goal (1 subgoal):
 1. x < 2 ^ (x - 1) proof (state)
this:
x < 2 ^ (x - 1)

goal:
No subgoals!
theory More_Arithmetic

lemma msrevs:
  "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
  "(k * n + m) mod n = m mod n"
  for n :: nat by simp_all

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

lemma int_div_same_is_1 [simp]:
  \<open>a div b = a \<longleftrightarrow> b = 1\<close> if \<open>0 < a\<close> for a b :: int using that by (metis div_by_1 abs_ge_zero abs_of_pos int_div_less_self neq_iff
            nonneg1_imp_zdiv_pos_iff zabs_less_one_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a div b = a) = (b = 1) proof (prove)
using this:
0 < a

goal (1 subgoal):
 1. (a div b = a) = (b = 1)
theory More_Divides

lemma int_div_minus_is_minus1 [simp]:
  \<open>a div b = - a \<longleftrightarrow> b = - 1\<close> if \<open>0 > a\<close> for a b :: int using that by (metis div_minus_right equation_minus_iff int_div_same_is_1 neg_0_less_iff_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a div b = - a) = (b = - 1) proof (prove)
using this:
a < 0

goal (1 subgoal):
 1. (a div b = - a) = (b = - 1)
theory More_Divides

lemma nat_div_eq_Suc_0_iff: "n div m = Suc 0 \<longleftrightarrow> m \<le> n \<and> n < 2 * m" apply auto using div_greater_zero_iff apply fastforce apply (metis One_nat_def div_greater_zero_iff dividend_less_div_times mult.right_neutral mult_Suc mult_numeral_1 numeral_2_eq_2 zero_less_numeral) apply (simp add: div_nat_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n div m = Suc 0) = (m \<le> n \<and> n < 2 * m) proof (prove)
goal (3 subgoals):
 1. n div m = Suc 0 \<Longrightarrow> m \<le> n
 2. n div m = Suc 0 \<Longrightarrow> n < 2 * m
 3. \<lbrakk>m \<le> n; n < 2 * m\<rbrakk> \<Longrightarrow> n div m = Suc 0 proof (prove)
using this:
(0 < ?m div ?n) = (?n \<le> ?m \<and> 0 < ?n)

goal (3 subgoals):
 1. n div m = Suc 0 \<Longrightarrow> m \<le> n
 2. n div m = Suc 0 \<Longrightarrow> n < 2 * m
 3. \<lbrakk>m \<le> n; n < 2 * m\<rbrakk> \<Longrightarrow> n div m = Suc 0 proof (prove)
goal (2 subgoals):
 1. n div m = Suc 0 \<Longrightarrow> n < 2 * m
 2. \<lbrakk>m \<le> n; n < 2 * m\<rbrakk> \<Longrightarrow> n div m = Suc 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; n < 2 * m\<rbrakk> \<Longrightarrow> n div m = Suc 0 proof (prove)
goal:
No subgoals!
theory More_Divides

lemma one_mod_exp_eq_one [simp]:
  "1 mod (2 * 2 ^ n) = (1::int)" using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 mod (2 * 2 ^ n) = 1 proof (prove)
using this:
(1::?'a1) < (2::?'a1) \<Longrightarrow> (1::?'a1) < (2::?'a1) ^ Suc n

goal (1 subgoal):
 1. 1 mod (2 * 2 ^ n) = 1
theory More_Divides

lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
  for b n :: int apply safe apply (erule (1) mod_pos_pos_trivial) apply (erule_tac [!] subst) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (0 \<le> b \<and> b < n) = (b mod n = b) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; 0 \<le> b; b < n\<rbrakk> \<Longrightarrow> b mod n = b
 2. \<lbrakk>0 < n; b mod n = b\<rbrakk> \<Longrightarrow> 0 \<le> b
 3. \<lbrakk>0 < n; b mod n = b\<rbrakk> \<Longrightarrow> b < n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; b mod n = b\<rbrakk> \<Longrightarrow> 0 \<le> b
 2. \<lbrakk>0 < n; b mod n = b\<rbrakk> \<Longrightarrow> b < n proof (prove)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> 0 \<le> b mod n
 2. 0 < n \<Longrightarrow> b mod n < n proof (prove)
goal:
No subgoals!
theory More_Divides

lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
  for b n :: int by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < 0; 0 < n\<rbrakk> \<Longrightarrow> b + n \<le> b mod n
theory More_Divides

lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
  for b n :: int by (metis minus_mod_self2 zmod_le_nonneg_dividend)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n
theory More_Divides

lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
  for n d :: int by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (n + 1) mod d = n mod d + 1
theory More_Divides

lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)" by (rule zmod_minus1) simp

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

lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
  for a :: int using int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + 2 ^ k < 0 \<Longrightarrow> a + 2 ^ k + 2 ^ Suc k \<le> (a + 2 ^ k) mod 2 ^ Suc k proof (prove)
using this:
\<lbrakk>a + 2 ^ k < 0; 0 < 2 ^ Suc k\<rbrakk> \<Longrightarrow> a + 2 ^ k + 2 ^ Suc k \<le> (a + 2 ^ k) mod 2 ^ Suc k

goal (1 subgoal):
 1. a + 2 ^ k < 0 \<Longrightarrow> a + 2 ^ k + 2 ^ Suc k \<le> (a + 2 ^ k) mod 2 ^ Suc k
theory More_Divides

lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
  for a :: int by (rule sb_inc_lem) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < - (2 ^ k) \<Longrightarrow> a + 2 ^ k + 2 ^ Suc k \<le> (a + 2 ^ k) mod 2 ^ Suc k
theory More_Divides

lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
  for a :: int using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp

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

goal (1 subgoal):
 1. 0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a
theory More_Divides

lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
  for a :: int by (rule sb_dec_lem) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a
theory More_Divides

lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
  for k :: int by (fact not_mod_2_eq_1_eq_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (k mod 2 \<noteq> 1) = (k mod 2 = 0)
theory More_Divides

lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)"
  for b :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 * b + 1) mod 2 = 1
theory More_Divides

lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
  for b :: int by (rule pos_zmod_mult_2) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)
theory More_Divides

lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
  for b :: int by (simp add: p1mod22k' add.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1
theory More_Divides

lemma pos_mod_sign2:
  \<open>0 \<le> a mod 2\<close> for a :: int by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a mod 2
theory More_Divides

lemma pos_mod_bound2:
  \<open>a mod 2 < 2\<close> for a :: int by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a mod 2 < 2
theory More_Divides

lemma nmod2: "n mod 2 = 0 \<or> n mod 2 = 1"
  for n :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n mod 2 = 0 \<or> n mod 2 = 1
theory More_Divides

lemma eme1p:
  "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (1 + n) mod d = 1 + n mod d" for n d :: int using emep1 [of n d] by (simp add: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (1 + n) mod d = 1 + n mod d proof (prove)
using this:
\<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (n + 1) mod d = n mod d + 1

goal (1 subgoal):
 1. \<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (1 + n) mod d = 1 + n mod d
theory More_Divides

lemma m1mod22k:
  \<open>- 1 mod (2 * 2 ^ n) = 2 * 2 ^ n - (1::int)\<close> by (simp add: zmod_minus1)

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

lemma z1pdiv2: "(2 * b + 1) div 2 = b"
  for b :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 * b + 1) div 2 = b
theory More_Divides

lemma zdiv_le_dividend:
  \<open>0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> a div b \<le> a\<close> for a b :: int by (metis div_by_1 int_one_le_iff_zero_less zdiv_mono2 zero_less_one)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 < b\<rbrakk> \<Longrightarrow> a div b \<le> a
theory More_Divides

lemma axxmod2: "(1 + x + x) mod 2 = 1 \<and> (0 + x + x) mod 2 = 0"
  for x :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (1 + x + x) mod 2 = 1 \<and> (0 + x + x) mod 2 = 0
theory More_Divides

lemma axxdiv2: "(1 + x + x) div 2 = x \<and> (0 + x + x) div 2 = x"
  for x :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (1 + x + x) div 2 = x \<and> (0 + x + x) div 2 = x
theory More_Divides

lemma mod_plus_right: "(a + x) mod m = (b + x) mod m \<longleftrightarrow> a mod m = b mod m"
  for a b m x :: nat by (induct x) (simp_all add: mod_Suc, arith)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a + x) mod m = (b + x) mod m) = (a mod m = b mod m)
theory More_Divides

lemma nat_minus_mod: "(n - n mod m) mod m = 0"
  for m n :: nat by (induct n) (simp_all add: mod_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n - n mod m) mod m = 0
theory More_Divides

lemma nat_mod_eq: "b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
  for a b n :: nat by (induct a) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < n; a mod n = b mod n\<rbrakk> \<Longrightarrow> a mod n = b
theory More_Divides

lemma mod_nat_add: "x < z \<Longrightarrow> y < z \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z)"
  for x y z :: nat apply (rule nat_mod_eq) apply auto apply (rule trans) apply (rule le_mod_geq) apply simp apply (rule nat_mod_eq') apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < z; y < z\<rbrakk> \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < z; y < z\<rbrakk> \<Longrightarrow> (if x + y < z then x + y else x + y - z) < z
 2. \<lbrakk>x < z; y < z\<rbrakk> \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z) mod z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < z; y < z; \<not> x + y < z\<rbrakk> \<Longrightarrow> (x + y) mod z = x + y - z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < z; y < z; \<not> x + y < z\<rbrakk> \<Longrightarrow> (x + y) mod z = ?s56
 2. \<lbrakk>x < z; y < z; \<not> x + y < z\<rbrakk> \<Longrightarrow> ?s56 = x + y - z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < z; y < z; \<not> x + y < z\<rbrakk> \<Longrightarrow> z \<le> x + y
 2. \<lbrakk>x < z; y < z; \<not> x + y < z\<rbrakk> \<Longrightarrow> (x + y - z) mod z = x + y - z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < z; y < z; \<not> x + y < z\<rbrakk> \<Longrightarrow> (x + y - z) mod z = x + y - z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < z; y < z; \<not> x + y < z\<rbrakk> \<Longrightarrow> x + y - z < z proof (prove)
goal:
No subgoals!
theory More_Divides

lemma mod_nat_sub: "x < z \<Longrightarrow> (x - y) mod z = x - y"
  for x y :: nat by (rule nat_mod_eq') arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < z \<Longrightarrow> (x - y) mod z = x - y
theory More_Divides

lemma int_mod_eq: "0 \<le> b \<Longrightarrow> b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
  for a b n :: int by (metis mod_pos_pos_trivial)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> b; b < n; a mod n = b mod n\<rbrakk> \<Longrightarrow> a mod n = b
theory More_Divides

lemma zmde:
  \<open>b * (a div b) = a - a mod b\<close> for a b :: \<open>'a::{group_add,semiring_modulo}\<close> using mult_div_mod_eq [of b a] by (simp add: eq_diff_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b * (a div b) = a - a mod b proof (prove)
using this:
b * (a div b) + a mod b = a

goal (1 subgoal):
 1. b * (a div b) = a - a mod b
theory More_Divides

lemma zdiv_mult_self: "m \<noteq> 0 \<Longrightarrow> (a + m * n) div m = a div m + n"
  for a m n :: int by simp

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

lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
  for a :: int by (simp add: mod_eq_0_iff_dvd le_imp_power_dvd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < a \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)
theory More_Divides

lemma nonneg_mod_div: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> (a mod b) \<and> 0 \<le> a div b"
  for a b :: int by (cases "b = 0") (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 \<le> b\<rbrakk> \<Longrightarrow> 0 \<le> a mod b \<and> 0 \<le> a div b
theory More_Divides

lemma mod_exp_less_eq_exp:
  \<open>a mod 2 ^ n < 2 ^ n\<close> for a :: int by (rule pos_mod_bound) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n < 2 ^ n
theory More_Divides

lemma div_mult_le:
  \<open>a div b * b \<le> a\<close> for a b :: nat by (fact div_times_less_eq_dividend)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a div b * b \<le> a