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