theory More_Divides

lemma power_mod_div:
  fixes x :: "nat"
  shows "x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)" (is "?LHS = ?RHS") proof (cases "n \<le> m") case True then have "?LHS = 0" apply - apply (rule div_less) apply (rule order_less_le_trans [OF mod_less_divisor]; simp) done also have "\<dots> = ?RHS" using True by simp finally show ?thesis . next case False then have lt: "m < n" by simp then obtain q where nv: "n = m + q" and "0 < q" by (auto dest: less_imp_Suc_add) then have "x mod 2 ^ n = 2 ^ m * (x div 2 ^ m mod 2 ^ q) + x mod 2 ^ m" by (simp add: power_add mod_mult2_eq) then have "?LHS = x div 2 ^ m mod 2 ^ q" by (simp add: div_add1_eq) also have "\<dots> = ?RHS" using nv by simp finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)
 2. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
n \<le> m

goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)
 2. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (chain)
picking this:
n \<le> m proof (prove)
using this:
n \<le> m

goal (1 subgoal):
 1. x mod 2 ^ n div 2 ^ m = 0 proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = 0 proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> x mod 2 ^ n < 2 ^ m proof (prove)
goal:
No subgoals! proof (state)
this:
x mod 2 ^ n div 2 ^ m = 0

goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)
 2. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
x mod 2 ^ n div 2 ^ m = 0

goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)
 2. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. 0 = x div 2 ^ m mod 2 ^ (n - m) proof (prove)
using this:
n \<le> m

goal (1 subgoal):
 1. 0 = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
0 = x div 2 ^ m mod 2 ^ (n - m)

goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)
 2. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (chain)
picking this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (prove)
using this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)

goal (1 subgoal):
 1. x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
\<not> n \<le> m

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (chain)
picking this:
\<not> n \<le> m proof (prove)
using this:
\<not> n \<le> m

goal (1 subgoal):
 1. m < n proof (state)
this:
m < n

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (chain)
picking this:
m < n proof (prove)
using this:
m < n

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

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (chain)
picking this:
n = m + q
0 < q proof (prove)
using this:
n = m + q
0 < q

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

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (chain)
picking this:
x mod 2 ^ n = 2 ^ m * (x div 2 ^ m mod 2 ^ q) + x mod 2 ^ m proof (prove)
using this:
x mod 2 ^ n = 2 ^ m * (x div 2 ^ m mod 2 ^ q) + x mod 2 ^ m

goal (1 subgoal):
 1. x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ q proof (state)
this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ q

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ q

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. x div 2 ^ m mod 2 ^ q = x div 2 ^ m mod 2 ^ (n - m) proof (prove)
using this:
n = m + q

goal (1 subgoal):
 1. x div 2 ^ m mod 2 ^ q = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
x div 2 ^ m mod 2 ^ q = x div 2 ^ m mod 2 ^ (n - m)

goal (1 subgoal):
 1. \<not> n \<le> m \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (chain)
picking this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (prove)
using this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)

goal (1 subgoal):
 1. x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m) proof (state)
this:
x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)

goal:
No subgoals!