theory Strict_part_mono

lemma two_power_strict_part_mono:
  "strict_part_mono {..LENGTH('a) - 1} (\<lambda>x. (2 :: 'a :: len word) ^ x)" proof - { fix n have "n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} (\<lambda>x. (2 :: 'a :: len word) ^ x)" proof (induct n) case 0 then show ?case by simp next case (Suc n) from Suc.prems have "2 ^ n < (2 :: 'a :: len word) ^ Suc n" using power_strict_increasing unat_power_lower word_less_nat_alt by fastforce with Suc show ?case by (subst strict_part_mono_by_steps) simp qed } then show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strict_part_mono {..LENGTH('a) - 1} ((^) 2) proof (state)
goal (1 subgoal):
 1. strict_part_mono {..LENGTH('a) - 1} ((^) 2) proof (state)
goal (1 subgoal):
 1. strict_part_mono {..LENGTH('a) - 1} ((^) 2) proof (state)
goal (1 subgoal):
 1. strict_part_mono {..LENGTH('a) - 1} ((^) 2) proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2) proof (state)
goal (2 subgoals):
 1. 0 < LENGTH('a) \<Longrightarrow> strict_part_mono {..0} ((^) 2)
 2. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2); Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> strict_part_mono {..Suc n} ((^) 2) proof (state)
this:
0 < LENGTH('a)

goal (2 subgoals):
 1. 0 < LENGTH('a) \<Longrightarrow> strict_part_mono {..0} ((^) 2)
 2. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2); Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> strict_part_mono {..Suc n} ((^) 2) proof (chain)
picking this:
0 < LENGTH('a) proof (prove)
using this:
0 < LENGTH('a)

goal (1 subgoal):
 1. strict_part_mono {..0} ((^) 2) proof (state)
this:
strict_part_mono {..0} ((^) 2)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2); Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> strict_part_mono {..Suc n} ((^) 2) proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2); Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> strict_part_mono {..Suc n} ((^) 2) proof (state)
this:
n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2)
Suc n < LENGTH('a)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2); Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> strict_part_mono {..Suc n} ((^) 2) proof (chain)
picking this:
Suc n < LENGTH('a) proof (prove)
using this:
Suc n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n < 2 ^ Suc n proof (prove)
using this:
Suc n < LENGTH('a)
\<lbrakk>?n < ?N; (1::?'a) < ?a\<rbrakk> \<Longrightarrow> ?a ^ ?n < ?a ^ ?N
?n < LENGTH(?'a) \<Longrightarrow> unat (2 ^ ?n) = 2 ^ ?n
(?a < ?b) = (unat ?a < unat ?b)

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

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2); Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> strict_part_mono {..Suc n} ((^) 2) proof (chain)
picking this:
n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2)
Suc n < LENGTH('a)
2 ^ n < 2 ^ Suc n proof (prove)
using this:
n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2)
Suc n < LENGTH('a)
2 ^ n < 2 ^ Suc n

goal (1 subgoal):
 1. strict_part_mono {..Suc n} ((^) 2) proof (state)
this:
strict_part_mono {..Suc n} ((^) 2)

goal:
No subgoals! proof (state)
this:
n < LENGTH('a) \<Longrightarrow> strict_part_mono {..n} ((^) 2)

goal (1 subgoal):
 1. strict_part_mono {..LENGTH('a) - 1} ((^) 2) proof (state)
this:
?n2 < LENGTH('a) \<Longrightarrow> strict_part_mono {..?n2} ((^) 2)

goal (1 subgoal):
 1. strict_part_mono {..LENGTH('a) - 1} ((^) 2) proof (chain)
picking this:
?n2 < LENGTH('a) \<Longrightarrow> strict_part_mono {..?n2} ((^) 2) proof (prove)
using this:
?n2 < LENGTH('a) \<Longrightarrow> strict_part_mono {..?n2} ((^) 2)

goal (1 subgoal):
 1. strict_part_mono {..LENGTH('a) - 1} ((^) 2) proof (state)
this:
strict_part_mono {..LENGTH('a) - 1} ((^) 2)

goal:
No subgoals!