# HG changeset patch # User haftmann # Date 1592471249 0 # Node ID 6ede899d26d329324b9b41afec244dd55aebef34 # Parent 476b9e6904d97b580c658805b736e503360d9627 fundamental construction of word type following existing transfer rules diff -r 476b9e6904d9 -r 6ede899d26d3 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000 +++ b/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000 @@ -19,36 +19,34 @@ subsection \Type definition\ -typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ LENGTH('a::len0)}" - morphisms uint Abs_word by auto +quotient_type (overloaded) 'a word = int / \\k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l\ + morphisms rep_word word_of_int by (auto intro!: equivpI reflpI sympI transpI) + +lift_definition uint :: \'a::len0 word \ int\ + is \take_bit LENGTH('a)\ . lemma uint_nonnegative: "0 \ uint w" - using word.uint [of w] by simp + by transfer simp lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" for w :: "'a::len0 word" - using word.uint [of w] by simp + by transfer (simp add: take_bit_eq_mod) lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" for w :: "'a::len0 word" using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial) +lemma word_uint_eqI: "uint a = uint b \ a = b" + by transfer simp + lemma word_uint_eq_iff: "a = b \ uint a = uint b" - by (simp add: uint_inject) - -lemma word_uint_eqI: "uint a = uint b \ a = b" - by (simp add: word_uint_eq_iff) - -definition word_of_int :: "int \ 'a::len0 word" - \ \representation of words using unsigned or signed bins, - only difference in these is the type class\ - where "word_of_int k = Abs_word (k mod 2 ^ LENGTH('a))" + using word_uint_eqI by auto lemma uint_word_of_int: "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ LENGTH('a)" - by (auto simp add: word_of_int_def intro: Abs_word_inverse) - + by transfer (simp add: take_bit_eq_mod) + lemma word_of_int_uint: "word_of_int (uint w) = w" - by (simp add: word_of_int_def uint_idem uint_inverse) + by transfer simp lemma split_word_all: "(\x::'a::len0 word. PROP P x) \ (\x. PROP P (word_of_int x))" proof @@ -143,31 +141,6 @@ "case x of (XCONST of_int :: 'a) y \ b" \ "CONST word_int_case (\y. b) x" -subsection \Correspondence relation for theorem transfer\ - -definition cr_word :: "int \ 'a::len0 word \ bool" - where "cr_word = (\x y. word_of_int x = y)" - -lemma Quotient_word: - "Quotient (\x y. bintrunc (LENGTH('a)) x = bintrunc (LENGTH('a)) y) - word_of_int uint (cr_word :: _ \ 'a::len0 word \ bool)" - unfolding Quotient_alt_def cr_word_def - by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject) - -lemma reflp_word: - "reflp (\x y. bintrunc (LENGTH('a::len0)) x = bintrunc (LENGTH('a)) y)" - by (simp add: reflp_def) - -setup_lifting Quotient_word reflp_word - -text \TODO: The next lemma could be generated automatically.\ - -lemma uint_transfer [transfer_rule]: - "(rel_fun pcr_word (=)) (bintrunc (LENGTH('a))) (uint :: 'a::len0 word \ int)" - unfolding rel_fun_def word.pcr_cr_eq cr_word_def - by (simp add: no_bintr_alt1 uint_word_of_int) - - subsection \Basic code generation setup\ definition Word :: "int \ 'a::len0 word" @@ -218,9 +191,8 @@ "td_ext (uint :: 'a word \ int) word_of_int (uints (LENGTH('a::len0))) (\w::int. w mod 2 ^ LENGTH('a))" apply (unfold td_ext_def') - apply (simp add: uints_num word_of_int_def bintrunc_mod2p) - apply (simp add: uint_mod_same uint_0 uint_lt - word.uint_inverse word.Abs_word_inverse int_mod_lem) + apply transfer + apply (simp add: uints_num take_bit_eq_mod) done interpretation word_uint: @@ -301,9 +273,14 @@ and word_pred_alt: "word_pred a = word_of_int (uint a - 1)" and word_0_wi: "0 = word_of_int 0" and word_1_wi: "1 = word_of_int 1" - unfolding plus_word_def minus_word_def times_word_def uminus_word_def - unfolding word_succ_def word_pred_def zero_word_def one_word_def - by simp_all + apply (simp_all flip: plus_word.abs_eq minus_word.abs_eq + times_word.abs_eq uminus_word.abs_eq + zero_word.abs_eq one_word.abs_eq) + apply transfer + apply simp + apply transfer + apply simp + done lemma wi_homs: shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" @@ -410,7 +387,8 @@ and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" - by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def) + by (simp_all flip: bitNOT_word.abs_eq bitAND_word.abs_eq + bitOR_word.abs_eq bitXOR_word.abs_eq) definition setBit :: "'a::len0 word \ nat \ 'a word" where "setBit w n = set_bit w n True" @@ -736,10 +714,35 @@ apply fast done -lemma word_eq_iff: "x = y \ (\n (\n?P \ ?Q\) for x y :: "'a::len0 word" - unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric] - by (metis test_bit_size [unfolded word_size]) +proof + assume ?P + then show ?Q + by simp +next + assume ?Q + then have *: \bit (uint x) n \ bit (uint y) n\ if \n < LENGTH('a)\ for n + using that by (simp add: word_test_bit_def bin_nth_iff) + show ?P + proof (rule word_uint_eqI, rule bit_eqI, rule iffI) + fix n + assume \bit (uint x) n\ + then have \n < LENGTH('a)\ + by (simp add: bit_take_bit_iff uint.rep_eq) + with * \bit (uint x) n\ + show \bit (uint y) n\ + by simp + next + fix n + assume \bit (uint y) n\ + then have \n < LENGTH('a)\ + by (simp add: bit_take_bit_iff uint.rep_eq) + with * \bit (uint y) n\ + show \bit (uint x) n\ + by simp + qed +qed lemma word_eqI: "(\n. n < size u \ u !! n = v !! n) \ u = v" for u :: "'a::len0 word" @@ -1661,14 +1664,14 @@ \ \links with \rbl\ operations\ lemma word_succ_rbl: "to_bl w = bl \ to_bl (word_succ w) = rev (rbl_succ (rev bl))" - apply (unfold word_succ_def) + apply (unfold word_succ_alt) apply clarify apply (simp add: to_bl_of_bin) apply (simp add: to_bl_def rbl_succ) done lemma word_pred_rbl: "to_bl w = bl \ to_bl (word_pred w) = rev (rbl_pred (rev bl))" - apply (unfold word_pred_def) + apply (unfold word_pred_alt) apply clarify apply (simp add: to_bl_of_bin) apply (simp add: to_bl_def rbl_pred) @@ -2089,16 +2092,34 @@ subsection \Cardinality, finiteness of set of words\ -instance word :: (len0) finite - by standard (simp add: type_definition.univ [OF type_definition_word]) +lemma inj_on_word_of_int: \inj_on (word_of_int :: int \ 'a word) {0..<2 ^ LENGTH('a::len0)}\ + by (rule inj_onI) (simp add: word.abs_eq_iff take_bit_eq_mod) + +lemma inj_uint: \inj uint\ + by (rule injI) simp + +lemma range_uint: \range (uint :: 'a word \ int) = {0..<2 ^ LENGTH('a::len0)}\ + by transfer (auto simp add: bintr_lt2p range_bintrunc) + +lemma UNIV_eq: \(UNIV :: 'a word set) = word_of_int ` {0..<2 ^ LENGTH('a::len0)}\ +proof - + have \uint ` (UNIV :: 'a word set) = uint ` (word_of_int :: int \ 'a word) ` {0..<2 ^ LENGTH('a::len0)}\ + by (simp add: range_uint image_image uint.abs_eq take_bit_eq_mod) + then show ?thesis + using inj_image_eq_iff [of \uint :: 'a word \ int\ \UNIV :: 'a word set\ \word_of_int ` {0..<2 ^ LENGTH('a)} :: 'a word set\, OF inj_uint] + by simp +qed lemma card_word: "CARD('a word) = 2 ^ LENGTH('a::len0)" - by (simp add: type_definition.card [OF type_definition_word] nat_power_eq) + by (simp add: UNIV_eq card_image inj_on_word_of_int) lemma card_word_size: "CARD('a word) = 2 ^ size x" for x :: "'a::len0 word" unfolding word_size by (rule card_word) +instance word :: (len0) finite + by standard (simp add: UNIV_eq) + subsection \Bitwise Operations on Words\ @@ -3182,7 +3203,7 @@ simp del: word_of_int_numeral) apply (drule xtr8 [rotated]) apply (rule int_mod_le) - apply (auto simp add : mod_pos_pos_trivial) + apply simp_all done lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]