theory Enumeration_Word

lemma upto_enum_step_red:
  assumes szv: "sz < LENGTH('a)"
  and   usszv: "us \<le> sz"
  shows "[0 :: 'a :: len word , 2 ^ us .e. 2 ^ sz - 1] =
  map (\<lambda>x. of_nat x * 2 ^ us) [0 ..< 2 ^ (sz - us)]" using szv unfolding upto_enum_step_def apply (subst if_not_P) apply (rule leD) apply (subst word_le_nat_alt) apply (subst unat_minus_one) apply simp apply simp apply simp apply (subst upto_enum_red) apply (simp del: upt.simps) apply (subst Suc_div_unat_helper [where 'a = 'a, OF szv usszv, symmetric]) apply clarsimp apply (subst toEnum_of_nat) apply (erule order_less_trans) using szv apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [0 , 2 ^ us .e. 2 ^ sz - 1] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. [0 , 2 ^ us .e. 2 ^ sz - 1] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. (if 2 ^ sz - 1 < 0 then [] else map (\<lambda>x. 0 + x * (2 ^ us - 0)) [0 .e. (2 ^ sz - 1 - 0) div (2 ^ us - 0)]) = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> \<not> 2 ^ sz - 1 < 0
 2. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. 0 + x * (2 ^ us - 0)) [0 .e. (2 ^ sz - 1 - 0) div (2 ^ us - 0)] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> 0 \<le> 2 ^ sz - 1
 2. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. 0 + x * (2 ^ us - 0)) [0 .e. (2 ^ sz - 1 - 0) div (2 ^ us - 0)] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat 0 \<le> unat (2 ^ sz - 1)
 2. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. 0 + x * (2 ^ us - 0)) [0 .e. (2 ^ sz - 1 - 0) div (2 ^ us - 0)] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (3 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz \<noteq> 0
 2. sz < LENGTH('a) \<Longrightarrow> unat 0 \<le> unat (2 ^ sz) - 1
 3. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. 0 + x * (2 ^ us - 0)) [0 .e. (2 ^ sz - 1 - 0) div (2 ^ us - 0)] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat 0 \<le> unat (2 ^ sz) - 1
 2. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. 0 + x * (2 ^ us - 0)) [0 .e. (2 ^ sz - 1 - 0) div (2 ^ us - 0)] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. 0 + x * (2 ^ us - 0)) [0 .e. (2 ^ sz - 1 - 0) div (2 ^ us - 0)] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. x * 2 ^ us) [0 .e. (2 ^ sz - 1) div 2 ^ us] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> map (\<lambda>x. x * 2 ^ us) (map toEnum [fromEnum 0..<Suc (fromEnum ((2 ^ sz - 1) div 2 ^ us))]) = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> map ((\<lambda>x. x * 2 ^ us) \<circ> toEnum) [0..<Suc (unat ((2 ^ sz - 1) div 2 ^ us))] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> map ((\<lambda>x. x * 2 ^ us) \<circ> toEnum) [0..<2 ^ (sz - us)] = map (\<lambda>x. word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sz < LENGTH('a); x < 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> toEnum x * 2 ^ us = word_of_nat x * 2 ^ us proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>sz < LENGTH('a); x < 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>sz < LENGTH('a); x < 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> word_of_nat x * 2 ^ us = word_of_nat x * 2 ^ us proof (prove)
goal (2 subgoals):
 1. \<And>x. sz < LENGTH('a) \<Longrightarrow> 2 ^ (sz - us) < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>sz < LENGTH('a); x < 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> word_of_nat x * 2 ^ us = word_of_nat x * 2 ^ us proof (prove)
using this:
sz < LENGTH('a)

goal (2 subgoals):
 1. \<And>x. sz < LENGTH('a) \<Longrightarrow> 2 ^ (sz - us) < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>sz < LENGTH('a); x < 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> word_of_nat x * 2 ^ us = word_of_nat x * 2 ^ us proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sz < LENGTH('a); x < 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> word_of_nat x * 2 ^ us = word_of_nat x * 2 ^ us proof (prove)
goal:
No subgoals!