theory Enumeration_Word

lemma upto_enum_set_conv [simp]:
  fixes a :: "'a :: len word"
  shows "set [a .e. b] = {x. a \<le> x \<and> x \<le> b}" apply (subst upto_enum_red) apply (subst set_map) apply safe apply simp apply clarsimp apply (erule disjE) apply simp apply (erule iffD2 [OF word_le_nat_alt]) apply clarsimp apply simp_all apply (metis le_unat_uoi nat_less_le toEnum_of_nat unsigned_less word_le_nat_alt) apply (metis le_unat_uoi less_or_eq_imp_le toEnum_of_nat unsigned_less word_le_nat_alt) apply (rule_tac x="fromEnum x" in image_eqI) apply clarsimp apply clarsimp apply transfer apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set [a .e. b] = {x. a \<le> x \<and> x \<le> b} proof (prove)
goal (1 subgoal):
 1. set (map toEnum [fromEnum a..<Suc (fromEnum b)]) = {x. a \<le> x \<and> x \<le> b} proof (prove)
goal (1 subgoal):
 1. toEnum ` set [fromEnum a..<Suc (fromEnum b)] = {x. a \<le> x \<and> x \<le> b} proof (prove)
goal (3 subgoals):
 1. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> a \<le> toEnum xa
 2. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> toEnum xa \<le> b
 3. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` set [fromEnum a..<Suc (fromEnum b)] proof (prove)
goal (3 subgoals):
 1. \<And>xa. unat a \<le> unat b \<and> (xa = unat b \<or> unat a \<le> xa \<and> xa < unat b) \<Longrightarrow> a \<le> toEnum xa
 2. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> toEnum xa \<le> b
 3. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` set [fromEnum a..<Suc (fromEnum b)] proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>unat a \<le> unat b; xa = unat b \<or> unat a \<le> xa \<and> xa < unat b\<rbrakk> \<Longrightarrow> a \<le> toEnum xa
 2. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> toEnum xa \<le> b
 3. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` set [fromEnum a..<Suc (fromEnum b)] proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>unat a \<le> unat b; xa = unat b\<rbrakk> \<Longrightarrow> a \<le> toEnum xa
 2. \<And>xa. \<lbrakk>unat a \<le> unat b; unat a \<le> xa \<and> xa < unat b\<rbrakk> \<Longrightarrow> a \<le> toEnum xa
 3. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> toEnum xa \<le> b
 4. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` set [fromEnum a..<Suc (fromEnum b)] proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>unat a \<le> unat b; xa = unat b\<rbrakk> \<Longrightarrow> a \<le> b
 2. \<And>xa. \<lbrakk>unat a \<le> unat b; unat a \<le> xa \<and> xa < unat b\<rbrakk> \<Longrightarrow> a \<le> toEnum xa
 3. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> toEnum xa \<le> b
 4. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` set [fromEnum a..<Suc (fromEnum b)] proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>unat a \<le> unat b; unat a \<le> xa \<and> xa < unat b\<rbrakk> \<Longrightarrow> a \<le> toEnum xa
 2. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> toEnum xa \<le> b
 3. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` set [fromEnum a..<Suc (fromEnum b)] proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>unat a \<le> xa; xa < unat b\<rbrakk> \<Longrightarrow> a \<le> toEnum xa
 2. \<And>x xa. xa \<in> set [fromEnum a..<Suc (fromEnum b)] \<Longrightarrow> toEnum xa \<le> b
 3. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` set [fromEnum a..<Suc (fromEnum b)] proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>unat a \<le> xa; xa < unat b\<rbrakk> \<Longrightarrow> a \<le> toEnum xa
 2. \<And>xa. unat a \<le> unat b \<and> (xa = unat b \<or> unat a \<le> xa \<and> xa < unat b) \<Longrightarrow> toEnum xa \<le> b
 3. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` {x. unat a \<le> unat b \<and> (x = unat b \<or> unat a \<le> x \<and> x < unat b)} proof (prove)
goal (2 subgoals):
 1. \<And>xa. unat a \<le> unat b \<and> (xa = unat b \<or> unat a \<le> xa \<and> xa < unat b) \<Longrightarrow> toEnum xa \<le> b
 2. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` {x. unat a \<le> unat b \<and> (x = unat b \<or> unat a \<le> x \<and> x < unat b)} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x \<in> toEnum ` {x. unat a \<le> unat b \<and> (x = unat b \<or> unat a \<le> x \<and> x < unat b)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> x = toEnum (fromEnum x)
 2. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> fromEnum x \<in> {x. unat a \<le> unat b \<and> (x = unat b \<or> unat a \<le> x \<and> x < unat b)} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> fromEnum x \<in> {x. unat a \<le> unat b \<and> (x = unat b \<or> unat a \<le> x \<and> x < unat b)} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> unat a \<le> unat b \<and> (unat x = unat b \<or> unat a \<le> unat x \<and> unat x < unat b) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>take_bit LENGTH('a) a \<le> take_bit LENGTH('a) x; take_bit LENGTH('a) x \<le> take_bit LENGTH('a) b\<rbrakk> \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) a \<le> (nat \<circ> take_bit LENGTH('a)) b \<and> ((nat \<circ> take_bit LENGTH('a)) x = (nat \<circ> take_bit LENGTH('a)) b \<or> (nat \<circ> take_bit LENGTH('a)) a \<le> (nat \<circ> take_bit LENGTH('a)) x \<and> (nat \<circ> take_bit LENGTH('a)) x < (nat \<circ> take_bit LENGTH('a)) b) proof (prove)
goal:
No subgoals!