1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(* Author: Thomas Sewell *)
8
9section "Enumeration Instances for Words"
10
11theory Word_Enum
12imports Enumeration Word_Lib
13begin
14
15instantiation word :: (len) enum
16begin
17
18definition
19  "(enum_class.enum :: ('a :: len) word list) \<equiv> map of_nat [0 ..< 2 ^ LENGTH('a)]"
20
21definition
22  "enum_class.enum_all (P :: ('a :: len) word \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
23
24definition
25  "enum_class.enum_ex (P :: ('a :: len) word \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
26
27instance
28  apply (intro_classes)
29     apply (force simp: enum_word_def)
30    apply (simp add: distinct_map enum_word_def)
31    apply (rule subset_inj_on, rule word_unat.Abs_inj_on)
32    apply (clarsimp simp add: unats_def)
33   apply (simp add: enum_all_word_def)
34  apply (simp add: enum_ex_word_def)
35  done
36
37end
38
39lemma fromEnum_unat[simp]: "fromEnum (x :: 'a::len word) = unat x"
40proof -
41  have "enum ! the_index enum x = x" by (auto intro: nth_the_index)
42  moreover
43  have "the_index enum x < length (enum::'a::len word list)" by (auto intro: the_index_bounded)
44  moreover
45  { fix y assume "of_nat y = x"
46    moreover assume "y < 2 ^ LENGTH('a)"
47    ultimately have "y = unat x" using of_nat_inverse by fastforce
48  }
49  ultimately
50  show ?thesis by (simp add: fromEnum_def enum_word_def)
51qed
52
53lemma length_word_enum: "length (enum :: 'a :: len word list) = 2 ^ LENGTH('a)"
54  by (simp add: enum_word_def)
55
56lemma toEnum_of_nat[simp]: "n < 2 ^ LENGTH('a) \<Longrightarrow> (toEnum n :: 'a :: len word) = of_nat n"
57  by (simp add: toEnum_def length_word_enum enum_word_def)
58
59declare of_nat_diff [simp]
60
61instantiation word :: (len) enumeration_both
62begin
63
64definition
65  enum_alt_word_def: "enum_alt \<equiv> alt_from_ord (enum :: ('a :: len) word list)"
66
67instance
68  by (intro_classes, simp add: enum_alt_word_def)
69
70end
71
72definition
73  upto_enum_step :: "('a :: len) word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word list" ("[_ , _ .e. _]")
74where
75  "upto_enum_step a b c \<equiv>
76      if c < a then [] else map (\<lambda>x. a + x * (b - a)) [0 .e. (c - a) div (b - a)]"
77  (* in the wraparound case, bad things happen. *)
78
79lemma maxBound_word:
80  "(maxBound::'a::len word) = -1"
81  by (simp add: maxBound_def enum_word_def last_map)
82
83lemma minBound_word:
84  "(minBound::'a::len word) = 0"
85  by (simp add: minBound_def enum_word_def upt_conv_Cons)
86
87lemma maxBound_max_word:
88  "(maxBound::'a::len word) = max_word"
89  by (simp add: maxBound_word max_word_minus [symmetric])
90
91lemma leq_maxBound [simp]:
92  "(x::'a::len word) \<le> maxBound"
93  by (simp add: maxBound_max_word)
94
95end
96