1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "Enumeration extensions and alternative definition"
8
9theory Enumeration
10imports Main
11begin
12
13abbreviation
14  "enum \<equiv> enum_class.enum"
15abbreviation
16  "enum_all \<equiv> enum_class.enum_all"
17abbreviation
18  "enum_ex \<equiv> enum_class.enum_ex"
19
20primrec (nonexhaustive)
21  the_index :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
22where
23  "the_index (x # xs) y = (if x = y then 0 else Suc (the_index xs y))"
24
25lemma the_index_bounded:
26  "x \<in> set xs \<Longrightarrow> the_index xs x < length xs"
27  by (induct xs, clarsimp+)
28
29lemma nth_the_index:
30  "x \<in> set xs \<Longrightarrow> xs ! the_index xs x = x"
31  by (induct xs, clarsimp+)
32
33lemma distinct_the_index_is_index[simp]:
34  "\<lbrakk> distinct xs ; n < length xs \<rbrakk> \<Longrightarrow> the_index xs (xs ! n) = n"
35  by (meson nth_eq_iff_index_eq nth_mem nth_the_index the_index_bounded)
36
37lemma the_index_last_distinct:
38  "distinct xs \<and> xs \<noteq> [] \<Longrightarrow> the_index xs (last xs) = length xs - 1"
39  apply safe
40  apply (subgoal_tac "xs ! (length xs - 1) = last xs")
41   apply (subgoal_tac "xs ! the_index xs (last xs) = last xs")
42    apply (subst nth_eq_iff_index_eq[symmetric])
43       apply assumption
44      apply (rule the_index_bounded)
45      apply simp_all
46   apply (rule nth_the_index)
47   apply simp
48  apply (induct xs, auto)
49  done
50
51context enum begin
52
53(* These two are added for historical reasons. *)
54lemmas enum_surj[simp] = enum_UNIV
55declare enum_distinct[simp]
56
57lemma enum_nonempty[simp]: "(enum :: 'a list) \<noteq> []"
58  using enum_surj by fastforce
59
60definition
61  maxBound :: 'a where
62  "maxBound \<equiv> last enum"
63
64definition
65  minBound :: 'a where
66  "minBound \<equiv> hd enum"
67
68definition
69  toEnum :: "nat \<Rightarrow> 'a" where
70  "toEnum n \<equiv> if n < length (enum :: 'a list) then enum ! n else the None"
71
72definition
73  fromEnum :: "'a \<Rightarrow> nat" where
74  "fromEnum x \<equiv> the_index enum x"
75
76
77lemma maxBound_is_length:
78  "fromEnum maxBound = length (enum :: 'a list) - 1"
79  by (simp add: maxBound_def fromEnum_def the_index_last_distinct)
80
81lemma maxBound_less_length:
82  "(x \<le> fromEnum maxBound) = (x < length (enum :: 'a list))"
83  unfolding maxBound_is_length by (cases "length enum") auto
84
85lemma maxBound_is_bound [simp]:
86  "fromEnum x \<le> fromEnum maxBound"
87  unfolding maxBound_less_length
88  by (fastforce simp: fromEnum_def intro: the_index_bounded)
89
90lemma to_from_enum [simp]:
91  fixes x :: 'a
92  shows "toEnum (fromEnum x) = x"
93proof -
94  have "x \<in> set enum" by simp
95  then show ?thesis by (simp add: toEnum_def fromEnum_def nth_the_index the_index_bounded)
96qed
97
98lemma from_to_enum [simp]:
99  "x \<le> fromEnum maxBound \<Longrightarrow> fromEnum (toEnum x) = x"
100  unfolding maxBound_less_length by (simp add: toEnum_def fromEnum_def)
101
102lemma map_enum:
103  fixes x :: 'a
104  shows "map f enum ! fromEnum x = f x"
105proof -
106  have "fromEnum x \<le> fromEnum (maxBound :: 'a)"
107    by (rule maxBound_is_bound)
108  then have "fromEnum x < length (enum::'a list)"
109    by (simp add: maxBound_less_length)
110  then have "map f enum ! fromEnum x = f (enum ! fromEnum x)" by simp
111  also
112  have "x \<in> set enum" by simp
113  then have "enum ! fromEnum x = x"
114    by (simp add: fromEnum_def nth_the_index)
115  finally
116  show ?thesis .
117qed
118
119definition
120  assocs :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list" where
121 "assocs f \<equiv> map (\<lambda>x. (x, f x)) enum"
122
123end
124
125(* For historical naming reasons. *)
126lemmas enum_bool = enum_bool_def
127
128lemma fromEnumTrue [simp]: "fromEnum True = 1"
129  by (simp add: fromEnum_def enum_bool)
130
131lemma fromEnumFalse [simp]: "fromEnum False = 0"
132  by (simp add: fromEnum_def enum_bool)
133
134
135class enum_alt =
136  fixes enum_alt :: "nat \<Rightarrow> 'a option"
137
138class enumeration_alt = enum_alt +
139  assumes enum_alt_one_bound:
140    "enum_alt x = (None :: 'a option) \<Longrightarrow> enum_alt (Suc x) = (None :: 'a option)"
141  assumes enum_alt_surj:
142    "range enum_alt \<union> {None} = UNIV"
143  assumes enum_alt_inj:
144    "(enum_alt x :: 'a option) = enum_alt y \<Longrightarrow> (x = y) \<or> (enum_alt x = (None :: 'a option))"
145begin
146
147lemma enum_alt_inj_2:
148  assumes "enum_alt x = (enum_alt y :: 'a option)"
149          "enum_alt x \<noteq> (None :: 'a option)"
150  shows "x = y"
151proof -
152  from assms
153  have "(x = y) \<or> (enum_alt x = (None :: 'a option))" by (fastforce intro!: enum_alt_inj)
154  with assms show ?thesis by clarsimp
155qed
156
157lemma enum_alt_surj_2:
158  "\<exists>x. enum_alt x = Some y"
159proof -
160  have "Some y \<in> range enum_alt \<union> {None}" by (subst enum_alt_surj) simp
161  then have "Some y \<in> range enum_alt" by simp
162  then show ?thesis by auto
163qed
164
165end
166
167definition
168  alt_from_ord :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option"
169where
170  "alt_from_ord L \<equiv> \<lambda>n. if (n < length L) then Some (L ! n) else None"
171
172lemma handy_if_lemma: "((if P then Some A else None) = Some B) = (P \<and> (A = B))"
173  by simp
174
175class enumeration_both = enum_alt + enum +
176  assumes enum_alt_rel: "enum_alt = alt_from_ord enum"
177
178instance enumeration_both < enumeration_alt
179  apply (intro_classes; simp add: enum_alt_rel alt_from_ord_def)
180    apply auto[1]
181   apply (safe; simp)[1]
182   apply (rule rev_image_eqI; simp)
183    apply (rule the_index_bounded; simp)
184   apply (subst nth_the_index; simp)
185  apply (clarsimp simp: handy_if_lemma)
186  apply (subst nth_eq_iff_index_eq[symmetric]; simp)
187  done
188
189instantiation bool :: enumeration_both
190begin
191  definition enum_alt_bool: "enum_alt \<equiv> alt_from_ord [False, True]"
192  instance by (intro_classes, simp add: enum_bool_def enum_alt_bool)
193end
194
195definition
196  toEnumAlt :: "nat \<Rightarrow> ('a :: enum_alt)" where
197 "toEnumAlt n \<equiv> the (enum_alt n)"
198
199definition
200  fromEnumAlt :: "('a :: enum_alt) \<Rightarrow> nat" where
201 "fromEnumAlt x \<equiv> THE n. enum_alt n = Some x"
202
203definition
204  upto_enum :: "('a :: enumeration_alt) \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_ .e. _])") where
205 "upto_enum n m \<equiv> map toEnumAlt [fromEnumAlt n ..< Suc (fromEnumAlt m)]"
206
207lemma fromEnum_alt_red[simp]:
208  "fromEnumAlt = (fromEnum :: ('a :: enumeration_both) \<Rightarrow> nat)"
209  apply (rule ext)
210  apply (simp add: fromEnumAlt_def fromEnum_def enum_alt_rel alt_from_ord_def)
211  apply (rule theI2)
212    apply (rule conjI)
213     apply (clarify, rule nth_the_index, simp)
214    apply (rule the_index_bounded, simp)
215   apply auto
216  done
217
218lemma toEnum_alt_red[simp]:
219  "toEnumAlt = (toEnum :: nat \<Rightarrow> 'a :: enumeration_both)"
220  by (rule ext) (simp add: enum_alt_rel alt_from_ord_def toEnum_def toEnumAlt_def)
221
222lemma upto_enum_red:
223  "[(n :: ('a :: enumeration_both)) .e. m] = map toEnum [fromEnum n ..< Suc (fromEnum m)]"
224  unfolding upto_enum_def by simp
225
226instantiation nat :: enumeration_alt
227begin
228  definition enum_alt_nat: "enum_alt \<equiv> Some"
229  instance by (intro_classes; simp add: enum_alt_nat UNIV_option_conv)
230end
231
232lemma toEnumAlt_nat[simp]: "toEnumAlt = id"
233  by (rule ext) (simp add: toEnumAlt_def enum_alt_nat)
234
235lemma fromEnumAlt_nat[simp]: "fromEnumAlt = id"
236  by (rule ext) (simp add: fromEnumAlt_def enum_alt_nat)
237
238lemma upto_enum_nat[simp]: "[n .e. m] = [n ..< Suc m]"
239  by (subst upto_enum_def) simp
240
241definition
242  zipE1 :: "'a :: enum_alt \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list"
243where
244  "zipE1 x L \<equiv> zip (map toEnumAlt [fromEnumAlt x ..< fromEnumAlt x + length L]) L"
245
246definition
247  zipE2 :: "'a :: enum_alt \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list"
248where
249  "zipE2 x xn L \<equiv> zip (map (\<lambda>n. toEnumAlt (fromEnumAlt x + (fromEnumAlt xn - fromEnumAlt x) * n))
250                      [0 ..< length L]) L"
251
252definition
253  zipE3 :: "'a list \<Rightarrow> 'b :: enum_alt \<Rightarrow> ('a \<times> 'b) list"
254where
255  "zipE3 L x \<equiv> zip L (map toEnumAlt [fromEnumAlt x ..< fromEnumAlt x + length L])"
256
257definition
258  zipE4 :: "'a list \<Rightarrow> 'b :: enum_alt \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list"
259where
260  "zipE4 L x xn \<equiv> zip L (map (\<lambda>n. toEnumAlt (fromEnumAlt x + (fromEnumAlt xn - fromEnumAlt x) * n))
261                         [0 ..< length L])"
262
263
264lemma to_from_enum_alt[simp]:
265  "toEnumAlt (fromEnumAlt x) = (x :: 'a :: enumeration_alt)"
266proof -
267  have rl: "\<And>a b. a = Some b \<Longrightarrow> the a = b" by simp
268  show ?thesis
269    unfolding fromEnumAlt_def toEnumAlt_def
270    by (rule rl, rule theI') (metis enum_alt_inj enum_alt_surj_2 not_None_eq)
271qed
272
273lemma upto_enum_triv [simp]: "[x .e. x] = [x]"
274  unfolding upto_enum_def by simp
275
276lemma toEnum_eq_to_fromEnum_eq:
277  fixes v :: "'a :: enum"
278  shows "n \<le> fromEnum (maxBound :: 'a) \<Longrightarrow> (toEnum n = v) = (n = fromEnum v)"
279  by auto
280
281lemma le_imp_diff_le:
282  "(j::nat) \<le> k \<Longrightarrow> j - n \<le> k"
283  by simp
284
285lemma fromEnum_upto_nth:
286  fixes start :: "'a :: enumeration_both"
287  assumes "n < length [start .e. end]"
288  shows "fromEnum ([start .e. end] ! n) = fromEnum start + n"
289proof -
290  have less_sub: "\<And>m k m' n. \<lbrakk> (n::nat) < m - k ; m \<le> m' \<rbrakk> \<Longrightarrow> n < m' - k" by fastforce
291  note upt_Suc[simp del]
292  show ?thesis using assms
293  by (fastforce simp: upto_enum_red
294                dest: less_sub[where m'="Suc (fromEnum maxBound)"] intro: maxBound_is_bound)
295qed
296
297lemma length_upto_enum_le_maxBound:
298  fixes start :: "'a :: enumeration_both"
299  shows "length [start .e. end] \<le> Suc (fromEnum (maxBound :: 'a))"
300  apply (clarsimp simp add: upto_enum_red split: if_splits)
301  apply (rule le_imp_diff_le[OF maxBound_is_bound[of "end"]])
302  done
303
304lemma less_length_upto_enum_maxBoundD:
305  fixes start :: "'a :: enumeration_both"
306  assumes "n < length [start .e. end]"
307  shows "n \<le> fromEnum (maxBound :: 'a)"
308  using assms
309  by (simp add: upto_enum_red less_Suc_eq_le
310                le_trans[OF _ le_imp_diff_le[OF maxBound_is_bound[of "end"]]]
311           split: if_splits)
312
313lemma fromEnum_eq_iff:
314  "(fromEnum e = fromEnum f) = (e = f)"
315proof -
316  have a: "e \<in> set enum" by auto
317  have b: "f \<in> set enum" by auto
318  from nth_the_index[OF a] nth_the_index[OF b] show ?thesis unfolding fromEnum_def by metis
319qed
320
321lemma maxBound_is_bound':
322  "i = fromEnum (e::('a::enum)) \<Longrightarrow> i \<le> fromEnum (maxBound::('a::enum))"
323  by clarsimp
324
325end
326