kings-crown/FVELER_Isabelle huggingface dataset:
theory Signed_Words

lemma word_le_ucast_sless:
  "\<lbrakk> x \<le> y; y \<noteq> -1; LENGTH('a) < LENGTH('b) \<rbrakk> \<Longrightarrow>
    (ucast x :: ('b :: len) signed word) <s ucast (y + 1)"
  for x y :: \<open>'a::len word\<close> apply (cases \<open>LENGTH('b)\<close>) apply simp_all apply transfer apply (simp add: signed_take_bit_take_bit) apply (metis add.commute mask_eq_exp_minus_1 take_bit_incr_eq zle_add1_eq_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < LENGTH('b); LENGTH('b) = 0\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1)
 2. \<And>nat. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < LENGTH('b); LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1) proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>x \<le> y; y \<noteq> - 1; LENGTH('a) < Suc nat; LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> ucast x <s ucast (y + 1) proof (prove)
goal (1 subgoal):
 1. \<And>nat x y. \<lbrakk>take_bit LENGTH('a) x \<le> take_bit LENGTH('a) y; take_bit LENGTH('a) y \<noteq> take_bit LENGTH('a) (- 1); LENGTH('a) < Suc nat; LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('b signed) - Suc 0) (take_bit LENGTH('a) x) < signed_take_bit (LENGTH('b signed) - Suc 0) (take_bit LENGTH('a) (y + 1)) proof (prove)
goal (1 subgoal):
 1. \<And>nat x y. \<lbrakk>take_bit LENGTH('a) x \<le> take_bit LENGTH('a) y; take_bit LENGTH('a) y \<noteq> mask LENGTH('a); LENGTH('a) < Suc nat; LENGTH('b) = Suc nat\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) x < take_bit LENGTH('a) (y + 1) proof (prove)
goal:
No subgoals!
theory Signed_Words

lemma zero_sle_ucast:
  "(0 <=s ((ucast (b::('a::len) word)) :: ('a::len) signed word))
                = (uint b < 2 ^ (LENGTH('a) - 1))" apply transfer apply (cases \<open>LENGTH('a)\<close>) apply (simp_all add: take_bit_Suc_from_most bit_simps) apply (simp_all add: bit_simps disjunctive_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<le>s ucast b) = (uint b < 2 ^ (LENGTH('a) - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>b. (signed_take_bit (LENGTH('a signed) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a signed) - Suc 0) (take_bit LENGTH('a) b)) = (take_bit LENGTH('a) b < 2 ^ (LENGTH('a) - 1)) proof (prove)
goal (2 subgoals):
 1. \<And>b. LENGTH('a) = 0 \<Longrightarrow> (signed_take_bit (LENGTH('a signed) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a signed) - Suc 0) (take_bit LENGTH('a) b)) = (take_bit LENGTH('a) b < 2 ^ (LENGTH('a) - 1))
 2. \<And>b nat. LENGTH('a) = Suc nat \<Longrightarrow> (signed_take_bit (LENGTH('a signed) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a signed) - Suc 0) (take_bit LENGTH('a) b)) = (take_bit LENGTH('a) b < 2 ^ (LENGTH('a) - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>b nat. LENGTH('a) = Suc nat \<Longrightarrow> bit b nat \<longrightarrow> bit (2 ^ nat + take_bit nat b) nat proof (prove)
goal:
No subgoals!
theory Signed_Words

lemma nth_w2p_scast:
  "(bit (scast ((2::'a::len signed word) ^ n) :: 'a word) m)
         \<longleftrightarrow> (bit (((2::'a::len  word) ^ n) :: 'a word) m)" by (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (scast (2 ^ n)) m = bit (2 ^ n) m
theory Signed_Words

lemma scast_nop1 [simp]:
  "((scast ((of_int x)::('a::len) word))::'a signed word) = of_int x" by transfer (simp add: take_bit_signed_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast (word_of_int x) = word_of_int x
theory Signed_Words

lemma scast_nop2 [simp]:
  "((scast ((of_int x)::('a::len) signed word))::'a word) = of_int x" by transfer (simp add: take_bit_signed_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast (word_of_int x) = word_of_int x
theory Enumeration

lemma the_index_bounded:
  "x \<in> set xs \<Longrightarrow> the_index xs x < length xs" by (induct xs, clarsimp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> the_index xs x < length xs
theory Enumeration

lemma nth_the_index:
  "x \<in> set xs \<Longrightarrow> xs ! the_index xs x = x" by (induct xs, clarsimp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> xs ! the_index xs x = x
theory Enumeration

lemma distinct_the_index_is_index[simp]:
  "\<lbrakk> distinct xs ; n < length xs \<rbrakk> \<Longrightarrow> the_index xs (xs ! n) = n" by (meson nth_eq_iff_index_eq nth_mem nth_the_index the_index_bounded)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; n < length xs\<rbrakk> \<Longrightarrow> the_index xs (xs ! n) = n
theory Enumeration

lemma enum_nonempty[simp]: "(enum :: 'a list) \<noteq> []" using enum_surj by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enum_class.enum \<noteq> [] proof (prove)
using this:
set enum_class.enum = UNIV

goal (1 subgoal):
 1. enum_class.enum \<noteq> []
theory Enumeration

lemma maxBound_is_length:
  "fromEnum maxBound = length (enum :: 'a list) - 1" by (simp add: maxBound_def fromEnum_def the_index_last_distinct)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum maxBound = length enum_class.enum - 1
theory Enumeration

lemma maxBound_less_length:
  "(x \<le> fromEnum maxBound) = (x < length (enum :: 'a list))" unfolding maxBound_is_length by (cases "length enum") auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<le> fromEnum maxBound) = (x < length enum_class.enum) proof (prove)
goal (1 subgoal):
 1. (x \<le> length enum_class.enum - 1) = (x < length enum_class.enum)
theory Enumeration

lemma maxBound_is_bound [simp]:
  "fromEnum x \<le> fromEnum maxBound" unfolding maxBound_less_length by (fastforce simp: fromEnum_def intro: the_index_bounded)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum x \<le> fromEnum maxBound proof (prove)
goal (1 subgoal):
 1. fromEnum x < length enum_class.enum
theory Enumeration

lemma to_from_enum [simp]:
  fixes x :: 'a
  shows "toEnum (fromEnum x) = x" proof - have "x \<in> set enum" by simp then show ?thesis by (simp add: toEnum_def fromEnum_def nth_the_index the_index_bounded) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. toEnum (fromEnum x) = x proof (state)
goal (1 subgoal):
 1. toEnum (fromEnum x) = x proof (prove)
goal (1 subgoal):
 1. x \<in> set enum_class.enum proof (state)
this:
x \<in> set enum_class.enum

goal (1 subgoal):
 1. toEnum (fromEnum x) = x proof (chain)
picking this:
x \<in> set enum_class.enum proof (prove)
using this:
x \<in> set enum_class.enum

goal (1 subgoal):
 1. toEnum (fromEnum x) = x proof (state)
this:
toEnum (fromEnum x) = x

goal:
No subgoals!
theory Enumeration

lemma fromEnumTrue [simp]: "fromEnum True = 1" by (simp add: fromEnum_def enum_bool)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum True = 1
theory Enumeration

lemma fromEnumFalse [simp]: "fromEnum False = 0" by (simp add: fromEnum_def enum_bool)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum False = 0
theory Enumeration

lemma enum_alt_inj_2:
  assumes "enum_alt x = (enum_alt y :: 'a option)"
          "enum_alt x \<noteq> (None :: 'a option)"
  shows "x = y" proof - from assms have "(x = y) \<or> (enum_alt x = (None :: 'a option))" by (fastforce intro!: enum_alt_inj) with assms show ?thesis by clarsimp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y proof (state)
goal (1 subgoal):
 1. x = y proof (chain)
picking this:
enum_alt x = enum_alt y
enum_alt x \<noteq> None proof (prove)
using this:
enum_alt x = enum_alt y
enum_alt x \<noteq> None

goal (1 subgoal):
 1. x = y \<or> enum_alt x = None proof (state)
this:
x = y \<or> enum_alt x = None

goal (1 subgoal):
 1. x = y proof (chain)
picking this:
enum_alt x = enum_alt y
enum_alt x \<noteq> None
x = y \<or> enum_alt x = None proof (prove)
using this:
enum_alt x = enum_alt y
enum_alt x \<noteq> None
x = y \<or> enum_alt x = None

goal (1 subgoal):
 1. x = y proof (state)
this:
x = y

goal:
No subgoals!
theory Enumeration

lemma enum_alt_surj_2:
  "\<exists>x. enum_alt x = Some y" proof - have "Some y \<in> range enum_alt \<union> {None}" by (subst enum_alt_surj) simp then have "Some y \<in> range enum_alt" by simp then show ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. enum_alt x = Some y proof (state)
goal (1 subgoal):
 1. \<exists>x. enum_alt x = Some y proof (prove)
goal (1 subgoal):
 1. Some y \<in> range enum_alt \<union> {None} proof (state)
this:
Some y \<in> range enum_alt \<union> {None}

goal (1 subgoal):
 1. \<exists>x. enum_alt x = Some y proof (chain)
picking this:
Some y \<in> range enum_alt \<union> {None} proof (prove)
using this:
Some y \<in> range enum_alt \<union> {None}

goal (1 subgoal):
 1. Some y \<in> range enum_alt proof (state)
this:
Some y \<in> range enum_alt

goal (1 subgoal):
 1. \<exists>x. enum_alt x = Some y proof (chain)
picking this:
Some y \<in> range enum_alt proof (prove)
using this:
Some y \<in> range enum_alt

goal (1 subgoal):
 1. \<exists>x. enum_alt x = Some y proof (state)
this:
\<exists>x. enum_alt x = Some y

goal:
No subgoals!
theory Enumeration

lemma handy_if_lemma: "((if P then Some A else None) = Some B) = (P \<and> (A = B))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then Some A else None) = Some B) = (P \<and> A = B)
theory Enumeration

lemma fromEnum_alt_red[simp]:
  "fromEnumAlt = (fromEnum :: ('a :: enumeration_both) \<Rightarrow> nat)" apply (rule ext) apply (simp add: fromEnumAlt_def fromEnum_def enum_alt_rel alt_from_ord_def) apply (rule theI2) apply (rule conjI) apply (clarify, rule nth_the_index, simp) apply (rule the_index_bounded, simp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnumAlt = fromEnum proof (prove)
goal (1 subgoal):
 1. \<And>x. fromEnumAlt x = fromEnum x proof (prove)
goal (1 subgoal):
 1. \<And>x. (THE n. (n < length enum \<longrightarrow> enum ! n = x) \<and> n < length enum) = the_index enum x proof (prove)
goal (3 subgoals):
 1. \<And>x. (?a9 x < length enum \<longrightarrow> enum ! ?a9 x = x) \<and> ?a9 x < length enum
 2. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = ?a9 x
 3. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = the_index enum x proof (prove)
goal (4 subgoals):
 1. \<And>x. ?a9 x < length enum \<longrightarrow> enum ! ?a9 x = x
 2. \<And>x. ?a9 x < length enum
 3. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = ?a9 x
 4. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = the_index enum x proof (prove)
goal (3 subgoals):
 1. \<And>x. the_index enum x < length enum
 2. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = the_index enum x
 3. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = the_index enum x proof (prove)
goal (2 subgoals):
 1. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = the_index enum x
 2. \<And>x xa. (xa < length enum \<longrightarrow> enum ! xa = x) \<and> xa < length enum \<Longrightarrow> xa = the_index enum x proof (prove)
goal:
No subgoals!
theory Enumeration

lemma upto_enum_red:
  "[(n :: ('a :: enumeration_both)) .e. m] = map toEnum [fromEnum n ..< Suc (fromEnum m)]" unfolding upto_enum_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [n .e. m] = map toEnum [fromEnum n..<Suc (fromEnum m)] proof (prove)
goal (1 subgoal):
 1. map toEnumAlt [fromEnumAlt n..<Suc (fromEnumAlt m)] = map toEnum [fromEnum n..<Suc (fromEnum m)]
theory Enumeration

lemma toEnumAlt_nat[simp]: "toEnumAlt = id" by (rule ext) (simp add: toEnumAlt_def enum_alt_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. toEnumAlt = id
theory Enumeration

lemma fromEnumAlt_nat[simp]: "fromEnumAlt = id" by (rule ext) (simp add: fromEnumAlt_def enum_alt_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnumAlt = id
theory Enumeration

lemma upto_enum_nat[simp]: "[n .e. m] = [n ..< Suc m]" by (subst upto_enum_def) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [n .e. m] = [n..<Suc m]
theory Enumeration

lemma to_from_enum_alt[simp]:
  "toEnumAlt (fromEnumAlt x) = (x :: 'a :: enumeration_alt)" proof - have rl: "\<And>a b. a = Some b \<Longrightarrow> the a = b" by simp show ?thesis unfolding fromEnumAlt_def toEnumAlt_def by (rule rl, rule theI') (metis enum_alt_inj enum_alt_surj_2 not_None_eq) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. toEnumAlt (fromEnumAlt x) = x proof (state)
goal (1 subgoal):
 1. toEnumAlt (fromEnumAlt x) = x proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = Some b \<Longrightarrow> the a = b proof (state)
this:
?a = Some ?b \<Longrightarrow> the ?a = ?b

goal (1 subgoal):
 1. toEnumAlt (fromEnumAlt x) = x proof (prove)
goal (1 subgoal):
 1. toEnumAlt (fromEnumAlt x) = x proof (prove)
goal (1 subgoal):
 1. the (enum_alt (THE n. enum_alt n = Some x)) = x proof (state)
this:
toEnumAlt (fromEnumAlt x) = x

goal:
No subgoals!
theory Enumeration

lemma upto_enum_triv [simp]: "[x .e. x] = [x]" unfolding upto_enum_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [x .e. x] = [x] proof (prove)
goal (1 subgoal):
 1. map toEnumAlt [fromEnumAlt x..<Suc (fromEnumAlt x)] = [x]
theory Enumeration

lemma toEnum_eq_to_fromEnum_eq:
  fixes v :: "'a :: enum"
  shows "n \<le> fromEnum (maxBound :: 'a) \<Longrightarrow> (toEnum n = v) = (n = fromEnum v)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> fromEnum maxBound \<Longrightarrow> (toEnum n = v) = (n = fromEnum v)
theory Enumeration

lemma le_imp_diff_le:
  "(j::nat) \<le> k \<Longrightarrow> j - n \<le> k" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. j \<le> k \<Longrightarrow> j - n \<le> k
theory Enumeration

lemma fromEnum_upto_nth:
  fixes start :: "'a :: enumeration_both"
  assumes "n < length [start .e. end]"
  shows "fromEnum ([start .e. end] ! n) = fromEnum start + n" proof - have less_sub: "\<And>m k m' n. \<lbrakk> (n::nat) < m - k ; m \<le> m' \<rbrakk> \<Longrightarrow> n < m' - k" by fastforce note upt_Suc[simp del] show ?thesis using assms by (fastforce simp: upto_enum_red
                dest: less_sub[where m'="Suc (fromEnum maxBound)"] intro: maxBound_is_bound) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum ([start .e. end] ! n) = fromEnum start + n proof (state)
goal (1 subgoal):
 1. fromEnum ([start .e. end] ! n) = fromEnum start + n proof (prove)
goal (1 subgoal):
 1. \<And>m k m' n. \<lbrakk>n < m - k; m \<le> m'\<rbrakk> \<Longrightarrow> n < m' - k proof (state)
this:
\<lbrakk>?n < ?m - ?k; ?m \<le> ?m'\<rbrakk> \<Longrightarrow> ?n < ?m' - ?k

goal (1 subgoal):
 1. fromEnum ([start .e. end] ! n) = fromEnum start + n proof (state)
this:
[?i..<Suc ?j] = (if ?i \<le> ?j then [?i..<?j] @ [?j] else [])

goal (1 subgoal):
 1. fromEnum ([start .e. end] ! n) = fromEnum start + n proof (prove)
goal (1 subgoal):
 1. fromEnum ([start .e. end] ! n) = fromEnum start + n proof (prove)
using this:
n < length [start .e. end]

goal (1 subgoal):
 1. fromEnum ([start .e. end] ! n) = fromEnum start + n proof (state)
this:
fromEnum ([start .e. end] ! n) = fromEnum start + n

goal:
No subgoals!
theory Enumeration

lemma length_upto_enum_le_maxBound:
  fixes start :: "'a :: enumeration_both"
  shows "length [start .e. end] \<le> Suc (fromEnum (maxBound :: 'a))" apply (clarsimp simp add: upto_enum_red split: if_splits) apply (rule le_imp_diff_le[OF maxBound_is_bound[of "end"]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length [start .e. end] \<le> Suc (fromEnum maxBound) proof (prove)
goal (1 subgoal):
 1. fromEnum start \<le> fromEnum end \<Longrightarrow> fromEnum end - fromEnum start \<le> fromEnum maxBound proof (prove)
goal:
No subgoals!
theory Enumeration

lemma less_length_upto_enum_maxBoundD:
  fixes start :: "'a :: enumeration_both"
  assumes "n < length [start .e. end]"
  shows "n \<le> fromEnum (maxBound :: 'a)" using assms by (simp add: upto_enum_red less_Suc_eq_le
                le_trans[OF _ le_imp_diff_le[OF maxBound_is_bound[of "end"]]]
           split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> fromEnum maxBound proof (prove)
using this:
n < length [start .e. end]

goal (1 subgoal):
 1. n \<le> fromEnum maxBound
theory Enumeration

lemma fromEnum_eq_iff:
  "(fromEnum e = fromEnum f) = (e = f)" proof - have a: "e \<in> set enum" by auto have b: "f \<in> set enum" by auto from nth_the_index[OF a] nth_the_index[OF b] show ?thesis unfolding fromEnum_def by metis qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fromEnum e = fromEnum f) = (e = f) proof (state)
goal (1 subgoal):
 1. (fromEnum e = fromEnum f) = (e = f) proof (prove)
goal (1 subgoal):
 1. e \<in> set enum proof (state)
this:
e \<in> set enum

goal (1 subgoal):
 1. (fromEnum e = fromEnum f) = (e = f) proof (prove)
goal (1 subgoal):
 1. f \<in> set enum proof (state)
this:
f \<in> set enum

goal (1 subgoal):
 1. (fromEnum e = fromEnum f) = (e = f) proof (chain)
picking this:
enum ! the_index enum e = e
enum ! the_index enum f = f proof (prove)
using this:
enum ! the_index enum e = e
enum ! the_index enum f = f

goal (1 subgoal):
 1. (fromEnum e = fromEnum f) = (e = f) proof (prove)
using this:
enum ! the_index enum e = e
enum ! the_index enum f = f

goal (1 subgoal):
 1. (the_index enum e = the_index enum f) = (e = f) proof (state)
this:
(fromEnum e = fromEnum f) = (e = f)

goal:
No subgoals!
theory Enumeration

lemma maxBound_is_bound':
  "i = fromEnum (e::('a::enum)) \<Longrightarrow> i \<le> fromEnum (maxBound::('a::enum))" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i = fromEnum e \<Longrightarrow> i \<le> fromEnum maxBound
theory Enumeration_Word

lemma length_word_enum: "length (enum :: 'a :: len word list) = 2 ^ LENGTH('a)" by (simp add: enum_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length enum = 2 ^ LENGTH('a)
theory Enumeration_Word

lemma fromEnum_unat[simp]: "fromEnum (x :: 'a::len word) = unat x" proof - have "enum ! the_index enum x = x" by (auto intro: nth_the_index) moreover have "the_index enum x < length (enum::'a::len word list)" by (auto intro: the_index_bounded) moreover { fix y assume "of_nat y = x" moreover assume "y < 2 ^ LENGTH('a)" ultimately have "y = unat x" using of_nat_inverse by fastforce } ultimately show ?thesis by (simp add: fromEnum_def enum_word_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
goal (1 subgoal):
 1. fromEnum x = unat x proof (prove)
goal (1 subgoal):
 1. enum ! the_index enum x = x proof (state)
this:
enum ! the_index enum x = x

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
enum ! the_index enum x = x

goal (1 subgoal):
 1. fromEnum x = unat x proof (prove)
goal (1 subgoal):
 1. the_index enum x < length enum proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
word_of_nat y = x

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
word_of_nat y = x

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
y < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. fromEnum x = unat x proof (chain)
picking this:
word_of_nat y = x
y < 2 ^ LENGTH('a) proof (prove)
using this:
word_of_nat y = x
y < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. y = unat x proof (prove)
using this:
word_of_nat y = x
y < 2 ^ LENGTH('a)
\<lbrakk>word_of_nat ?r = ?a; ?r < 2 ^ LENGTH(?'a)\<rbrakk> \<Longrightarrow> unat ?a = ?r

goal (1 subgoal):
 1. y = unat x proof (state)
this:
y = unat x

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
\<lbrakk>word_of_nat ?y2 = x; ?y2 < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> ?y2 = unat x

goal (1 subgoal):
 1. fromEnum x = unat x proof (chain)
picking this:
enum ! the_index enum x = x
the_index enum x < length enum
\<lbrakk>word_of_nat ?y2 = x; ?y2 < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> ?y2 = unat x proof (prove)
using this:
enum ! the_index enum x = x
the_index enum x < length enum
\<lbrakk>word_of_nat ?y2 = x; ?y2 < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> ?y2 = unat x

goal (1 subgoal):
 1. fromEnum x = unat x proof (state)
this:
fromEnum x = unat x

goal:
No subgoals!
theory Enumeration_Word

lemma toEnum_of_nat[simp]: "n < 2 ^ LENGTH('a) \<Longrightarrow> (toEnum n :: 'a :: len word) = of_nat n" by (simp add: toEnum_def length_word_enum enum_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) \<Longrightarrow> toEnum n = word_of_nat n
theory Enumeration_Word

lemma maxBound_word:
  "(maxBound::'a::len word) = -1" by (simp add: maxBound_def enum_word_def last_map of_nat_diff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maxBound = - 1
theory Enumeration_Word

lemma minBound_word:
  "(minBound::'a::len word) = 0" by (simp add: minBound_def enum_word_def upt_conv_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. minBound = 0
theory Enumeration_Word

lemma maxBound_max_word:
  "(maxBound::'a::len word) = - 1" by (fact maxBound_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maxBound = - 1
theory Enumeration_Word

lemma upto_enum_red':
  assumes lt: "1 \<le> X"
  shows "[(0::'a :: len word) .e. X - 1] =  map of_nat [0 ..< unat X]" proof - have lt': "unat X < 2 ^ LENGTH('a)" by (rule unat_lt2p) show ?thesis apply (subst upto_enum_red) apply (simp del: upt.simps) apply (subst Suc_unat_diff_1 [OF lt]) apply (rule map_cong [OF refl]) apply (rule toEnum_of_nat) apply simp apply (erule order_less_trans [OF _ lt']) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [0 .e. X - 1] = map word_of_nat [0..<unat X] proof (state)
goal (1 subgoal):
 1. [0 .e. X - 1] = map word_of_nat [0..<unat X] proof (prove)
goal (1 subgoal):
 1. unat X < 2 ^ LENGTH('a) proof (state)
this:
unat X < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. [0 .e. X - 1] = map word_of_nat [0..<unat X] proof (prove)
goal (1 subgoal):
 1. [0 .e. X - 1] = map word_of_nat [0..<unat X] proof (prove)
goal (1 subgoal):
 1. map toEnum [fromEnum 0..<Suc (fromEnum (X - 1))] = map word_of_nat [0..<unat X] proof (prove)
goal (1 subgoal):
 1. map toEnum [0..<Suc (unat (X - 1))] = map word_of_nat [0..<unat X] proof (prove)
goal (1 subgoal):
 1. map toEnum [0..<unat X] = map word_of_nat [0..<unat X] proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<unat X] \<Longrightarrow> toEnum x = word_of_nat x proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<unat X] \<Longrightarrow> x < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>x. x < unat X \<Longrightarrow> x < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals! proof (state)
this:
[0 .e. X - 1] = map word_of_nat [0..<unat X]

goal:
No subgoals!