theory More_Arithmetic

lemma nat_power_less_diff:
  assumes lt: "(2::nat) ^ n * q < 2 ^ m"
  shows "q < 2 ^ (m - n)" using lt proof (induct n arbitrary: m) case 0 then show ?case by simp next case (Suc n) have ih: "\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n)"
    and prem: "2 ^ Suc n * q < 2 ^ m" by fact+ show ?case proof (cases m) case 0 then show ?thesis using Suc by simp next case (Suc m') then show ?thesis using prem by (simp add: ac_simps ih) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. q < 2 ^ (m - n) proof (prove)
using this:
2 ^ n * q < 2 ^ m

goal (1 subgoal):
 1. q < 2 ^ (m - n) proof (state)
goal (2 subgoals):
 1. \<And>m. 2 ^ 0 * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - 0)
 2. \<And>n m. \<lbrakk>\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n); 2 ^ Suc n * q < 2 ^ m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - Suc n) proof (state)
this:
2 ^ 0 * q < 2 ^ m

goal (2 subgoals):
 1. \<And>m. 2 ^ 0 * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - 0)
 2. \<And>n m. \<lbrakk>\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n); 2 ^ Suc n * q < 2 ^ m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - Suc n) proof (chain)
picking this:
2 ^ 0 * q < 2 ^ m proof (prove)
using this:
2 ^ 0 * q < 2 ^ m

goal (1 subgoal):
 1. q < 2 ^ (m - 0) proof (state)
this:
q < 2 ^ (m - 0)

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n); 2 ^ Suc n * q < 2 ^ m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - Suc n) proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n); 2 ^ Suc n * q < 2 ^ m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - Suc n) proof (state)
this:
2 ^ n * q < 2 ^ ?m \<Longrightarrow> q < 2 ^ (?m - n)
2 ^ Suc n * q < 2 ^ m

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n); 2 ^ Suc n * q < 2 ^ m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - Suc n) proof (prove)
goal (1 subgoal):
 1. (\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n)) &&& 2 ^ Suc n * q < 2 ^ m proof (state)
this:
2 ^ n * q < 2 ^ ?m \<Longrightarrow> q < 2 ^ (?m - n)
2 ^ Suc n * q < 2 ^ m

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n); 2 ^ Suc n * q < 2 ^ m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - Suc n) proof (prove)
goal (1 subgoal):
 1. q < 2 ^ (m - Suc n) proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> q < 2 ^ (m - Suc n)
 2. \<And>nat. m = Suc nat \<Longrightarrow> q < 2 ^ (m - Suc n) proof (state)
this:
m = 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> q < 2 ^ (m - Suc n)
 2. \<And>nat. m = Suc nat \<Longrightarrow> q < 2 ^ (m - Suc n) proof (chain)
picking this:
m = 0 proof (prove)
using this:
m = 0

goal (1 subgoal):
 1. q < 2 ^ (m - Suc n) proof (prove)
using this:
m = 0
2 ^ n * q < 2 ^ ?m \<Longrightarrow> q < 2 ^ (?m - n)
2 ^ Suc n * q < 2 ^ m

goal (1 subgoal):
 1. q < 2 ^ (m - Suc n) proof (state)
this:
q < 2 ^ (m - Suc n)

goal (1 subgoal):
 1. \<And>nat. m = Suc nat \<Longrightarrow> q < 2 ^ (m - Suc n) proof (state)
goal (1 subgoal):
 1. \<And>nat. m = Suc nat \<Longrightarrow> q < 2 ^ (m - Suc n) proof (state)
this:
m = Suc m'

goal (1 subgoal):
 1. \<And>nat. m = Suc nat \<Longrightarrow> q < 2 ^ (m - Suc n) proof (chain)
picking this:
m = Suc m' proof (prove)
using this:
m = Suc m'

goal (1 subgoal):
 1. q < 2 ^ (m - Suc n) proof (prove)
using this:
m = Suc m'
2 ^ Suc n * q < 2 ^ m

goal (1 subgoal):
 1. q < 2 ^ (m - Suc n) proof (state)
this:
q < 2 ^ (m - Suc n)

goal:
No subgoals! proof (state)
this:
q < 2 ^ (m - Suc n)

goal:
No subgoals!