theory More_Divides

lemma mod_mod_power:
  fixes k :: nat
  shows "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ (min m n)" proof (cases "m \<le> n") case True then have "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ m" apply - apply (subst mod_less [where n = "2 ^ n"]) apply (rule order_less_le_trans [OF mod_less_divisor]) apply simp+ done also have "\<dots> = k mod  2 ^ (min m n)" using True by simp finally show ?thesis . next case False then have "n < m" by simp then obtain d where md: "m = n + d" by (auto dest: less_imp_add_positive) then have "k mod 2 ^ m = 2 ^ n * (k div 2 ^ n mod 2 ^ d) + k mod 2 ^ n" by (simp add: mod_mult2_eq power_add) then have "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ n" by (simp add: mod_add_left_eq) then show ?thesis using False by simp qed

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

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

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

goal (2 subgoals):
 1. m \<le> n \<Longrightarrow> k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n
 2. \<not> m \<le> n \<Longrightarrow> k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n proof (state)
this:
k mod 2 ^ m mod 2 ^ n = k mod 2 ^ m

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

goal (1 subgoal):
 1. k mod 2 ^ m = k mod 2 ^ min m n proof (state)
this:
k mod 2 ^ m = k mod 2 ^ min m n

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

goal (1 subgoal):
 1. k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n proof (state)
this:
k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n

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

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

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

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

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

goal (1 subgoal):
 1. \<not> m \<le> n \<Longrightarrow> k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n proof (chain)
picking this:
m = n + d proof (prove)
using this:
m = n + d

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

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

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

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

goal (1 subgoal):
 1. k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n proof (prove)
using this:
k mod 2 ^ m mod 2 ^ n = k mod 2 ^ n
\<not> m \<le> n

goal (1 subgoal):
 1. k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n proof (state)
this:
k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n

goal:
No subgoals!