theory More_Word

lemma word_add_offset_less:
  fixes x :: "'a :: len word"
  assumes yv: "y < 2 ^ n"
  and     xv: "x < 2 ^ m"
  and     mnv: "sz < LENGTH('a :: len)"
  and    xv': "x < 2 ^ (LENGTH('a :: len) - n)"
  and     mn: "sz = m + n"
  shows   "x * 2 ^ n + y < 2 ^ sz" proof (subst mn) from mnv mn have nv: "n < LENGTH('a)" and mv: "m < LENGTH('a)" by auto have uy: "unat y < 2 ^ n" by (rule order_less_le_trans [OF unat_mono [OF yv] order_eq_refl],
        rule unat_power_lower[OF nv]) have ux: "unat x < 2 ^ m" by (rule order_less_le_trans [OF unat_mono [OF xv] order_eq_refl],
        rule unat_power_lower[OF mv]) then show "x * 2 ^ n + y < 2 ^ (m + n)" using ux uy nv mnv xv' apply (subst word_less_nat_alt) apply (subst unat_word_ariths)+ apply (subst mod_less) apply simp apply (subst mult.commute) apply (rule nat_less_power_trans [OF _ order_less_imp_le [OF nv]]) apply (rule order_less_le_trans [OF unat_mono [OF xv']]) apply (cases "n = 0"; simp) apply (subst unat_power_lower[OF nv]) apply (subst mod_less) apply (erule order_less_le_trans [OF nat_add_offset_less], assumption) apply (rule mn) apply simp apply (simp add: mn mnv) apply (erule nat_add_offset_less; simp) done 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:
sz < LENGTH('a)
sz = m + n proof (prove)
using this:
sz < LENGTH('a)
sz = m + n

goal (1 subgoal):
 1. n < LENGTH('a) &&& m < LENGTH('a) proof (state)
this:
n < LENGTH('a)
m < LENGTH('a)

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

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

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

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (prove)
using this:
unat x < 2 ^ m
unat x < 2 ^ m
unat y < 2 ^ n
n < LENGTH('a)
sz < LENGTH('a)
x < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. x * 2 ^ n + y < 2 ^ (m + n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat (x * 2 ^ n + y) < unat (2 ^ (m + n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * unat (2 ^ n) mod 2 ^ LENGTH('a) + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * unat (2 ^ n) < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * unat (2 ^ n) + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * 2 ^ n < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * unat (2 ^ n) + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> 2 ^ n * unat x < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * unat (2 ^ n) + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x < 2 ^ (LENGTH('a) - n)
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * unat (2 ^ n) + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat (2 ^ (LENGTH('a) - n)) \<le> 2 ^ (LENGTH('a) - n)
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * unat (2 ^ n) + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * unat (2 ^ n) + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> (unat x * 2 ^ n + unat y) mod 2 ^ LENGTH('a) < unat (2 ^ (m + n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * 2 ^ n + unat y < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * 2 ^ n + unat y < unat (2 ^ (m + n)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> ?sz23 = m + n
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> 2 ^ ?sz23 \<le> 2 ^ LENGTH('a)
 3. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * 2 ^ n + unat y < unat (2 ^ (m + n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> 2 ^ LENGTH('a)
 2. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * 2 ^ n + unat y < unat (2 ^ (m + n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < 2 ^ m; unat x < 2 ^ m; unat y < 2 ^ n; n < LENGTH('a); sz < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * 2 ^ n + unat y < unat (2 ^ (m + n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < 2 ^ m; unat y < 2 ^ n; m + n < LENGTH('a); x < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat x * 2 ^ n + unat y < 2 ^ (m + n) proof (prove)
goal:
No subgoals! proof (state)
this:
x * 2 ^ n + y < 2 ^ (m + n)

goal:
No subgoals!