theory More_Word

lemma Suc_div_unat_helper:
  assumes szv: "sz < LENGTH('a :: len)"
  and   usszv: "us \<le> sz"
  shows "2 ^ (sz - us) = Suc (unat (((2::'a :: len word) ^ sz - 1) div 2 ^ us))" proof - note usv = order_le_less_trans [OF usszv szv] from usszv obtain q where qv: "sz = us + q" by (auto simp: le_iff_add) have "Suc (unat (((2:: 'a word) ^ sz - 1) div 2 ^ us)) =
    (2 ^ us + unat ((2:: 'a word) ^ sz - 1)) div 2 ^ us" apply (subst unat_div unat_power_lower[OF usv])+ apply (subst div_add_self1, simp+) done also have "\<dots> = ((2 ^ us - 1) + 2 ^ sz) div 2 ^ us" using szv by (simp add: unat_minus_one) also have "\<dots> = 2 ^ q + ((2 ^ us - 1) div 2 ^ us)" apply (subst qv) apply (subst power_add) apply (subst div_mult_self2; simp) done also have "\<dots> = 2 ^ (sz - us)" using qv by simp finally show ?thesis .. qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (state)
goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (state)
this:
us < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (chain)
picking this:
us \<le> sz proof (prove)
using this:
us \<le> sz

goal (1 subgoal):
 1. (\<And>q. sz = us + q \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
sz = us + q

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (prove)
goal (1 subgoal):
 1. Suc (unat ((2 ^ sz - 1) div 2 ^ us)) = (2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us proof (prove)
goal (1 subgoal):
 1. Suc (unat (2 ^ sz - 1) div 2 ^ us) = (2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us proof (prove)
goal:
No subgoals! proof (state)
this:
Suc (unat ((2 ^ sz - 1) div 2 ^ us)) = (2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (state)
this:
Suc (unat ((2 ^ sz - 1) div 2 ^ us)) = (2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (prove)
goal (1 subgoal):
 1. (2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us = (2 ^ us - 1 + 2 ^ sz) div 2 ^ us proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. (2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us = (2 ^ us - 1 + 2 ^ sz) div 2 ^ us proof (state)
this:
(2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us = (2 ^ us - 1 + 2 ^ sz) div 2 ^ us

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (state)
this:
(2 ^ us + unat (2 ^ sz - 1)) div 2 ^ us = (2 ^ us - 1 + 2 ^ sz) div 2 ^ us

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (prove)
goal (1 subgoal):
 1. (2 ^ us - 1 + 2 ^ sz) div 2 ^ us = 2 ^ q + (2 ^ us - 1) div 2 ^ us proof (prove)
goal (1 subgoal):
 1. (2 ^ us - 1 + 2 ^ (us + q)) div 2 ^ us = 2 ^ q + (2 ^ us - 1) div 2 ^ us proof (prove)
goal (1 subgoal):
 1. (2 ^ us - 1 + 2 ^ us * 2 ^ q) div 2 ^ us = 2 ^ q + (2 ^ us - 1) div 2 ^ us proof (prove)
goal:
No subgoals! proof (state)
this:
(2 ^ us - 1 + 2 ^ sz) div 2 ^ us = 2 ^ q + (2 ^ us - 1) div 2 ^ us

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (state)
this:
(2 ^ us - 1 + 2 ^ sz) div 2 ^ us = 2 ^ q + (2 ^ us - 1) div 2 ^ us

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (prove)
goal (1 subgoal):
 1. 2 ^ q + (2 ^ us - 1) div 2 ^ us = 2 ^ (sz - us) proof (prove)
using this:
sz = us + q

goal (1 subgoal):
 1. 2 ^ q + (2 ^ us - 1) div 2 ^ us = 2 ^ (sz - us) proof (state)
this:
2 ^ q + (2 ^ us - 1) div 2 ^ us = 2 ^ (sz - us)

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (chain)
picking this:
Suc (unat ((2 ^ sz - 1) div 2 ^ us)) = 2 ^ (sz - us) proof (prove)
using this:
Suc (unat ((2 ^ sz - 1) div 2 ^ us)) = 2 ^ (sz - us)

goal (1 subgoal):
 1. 2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us)) proof (state)
this:
2 ^ (sz - us) = Suc (unat ((2 ^ sz - 1) div 2 ^ us))

goal:
No subgoals!