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