theory Enumeration_Word

lemma enum_word_div:
  fixes v :: "'a :: len word" shows
  "\<exists>xs ys. enum = xs @ [v] @ ys
             \<and> (\<forall>x \<in> set xs. x < v)
             \<and> (\<forall>y \<in> set ys. v < y)" apply (simp only: enum_word_def) apply (subst upt_add_eq_append'[where j="unat v"]) apply simp apply (rule order_less_imp_le, simp) apply (simp add: upt_conv_Cons) apply (intro exI conjI) apply fastforce apply clarsimp apply (drule of_nat_mono_maybe[rotated, where 'a='a]) apply simp apply simp apply (clarsimp simp: Suc_le_eq) apply (drule of_nat_mono_maybe[rotated, where 'a='a]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. enum = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>y\<in>set ys. v < y) proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. map word_of_nat [0..<2 ^ LENGTH('a)] = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>y\<in>set ys. v < y) proof (prove)
goal (3 subgoals):
 1. \<And>ys xs. 0 \<le> unat v
 2. \<And>ys xs. unat v \<le> 2 ^ LENGTH('a)
 3. \<exists>xs ys. map word_of_nat ([0..<unat v] @ [unat v..<2 ^ LENGTH('a)]) = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> Ball (set ys) ((<) v) proof (prove)
goal (2 subgoals):
 1. \<And>ys xs. unat v \<le> 2 ^ LENGTH('a)
 2. \<exists>xs ys. map word_of_nat ([0..<unat v] @ [unat v..<2 ^ LENGTH('a)]) = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> Ball (set ys) ((<) v) proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. map word_of_nat ([0..<unat v] @ [unat v..<2 ^ LENGTH('a)]) = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> Ball (set ys) ((<) v) proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. map word_of_nat [0..<unat v] @ v # map word_of_nat [Suc (unat v)..<2 ^ LENGTH('a)] = xs @ v # ys \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>x\<in>set ys. v < x) proof (prove)
goal (3 subgoals):
 1. map word_of_nat [0..<unat v] @ v # map word_of_nat [Suc (unat v)..<2 ^ LENGTH('a)] = ?xs4 @ v # ?ys5
 2. \<forall>x\<in>set ?xs4. x < v
 3. \<forall>x\<in>set ?ys5. v < x proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set (map word_of_nat [0..<unat v]). x < v
 2. \<forall>x\<in>set (map word_of_nat [Suc (unat v)..<2 ^ LENGTH('a)]). v < x proof (prove)
goal (2 subgoals):
 1. \<And>x. x < unat v \<Longrightarrow> word_of_nat x < v
 2. \<forall>x\<in>set (map word_of_nat [Suc (unat v)..<2 ^ LENGTH('a)]). v < x proof (prove)
goal (3 subgoals):
 1. \<And>x. unat v < 2 ^ LENGTH('a)
 2. \<And>x. word_of_nat x < word_of_nat (unat v) \<Longrightarrow> word_of_nat x < v
 3. \<forall>x\<in>set (map word_of_nat [Suc (unat v)..<2 ^ LENGTH('a)]). v < x proof (prove)
goal (2 subgoals):
 1. \<And>x. word_of_nat x < word_of_nat (unat v) \<Longrightarrow> word_of_nat x < v
 2. \<forall>x\<in>set (map word_of_nat [Suc (unat v)..<2 ^ LENGTH('a)]). v < x proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (map word_of_nat [Suc (unat v)..<2 ^ LENGTH('a)]). v < x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>unat v < x; x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> v < word_of_nat x proof (prove)
goal (2 subgoals):
 1. \<And>x. x < 2 ^ LENGTH('a) \<Longrightarrow> x < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>x < 2 ^ LENGTH('a); word_of_nat (unat v) < word_of_nat x\<rbrakk> \<Longrightarrow> v < word_of_nat x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < 2 ^ LENGTH('a); word_of_nat (unat v) < word_of_nat x\<rbrakk> \<Longrightarrow> v < word_of_nat x proof (prove)
goal:
No subgoals!