1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7section "Normalising Word Numerals" 8 9theory Norm_Words 10imports "Signed_Words" 11begin 12 13text \<open> 14 Normalise word numerals, including negative ones apart from @{term "-1"}, to the 15 interval \<open>[0..2^len_of 'a)\<close>. Only for concrete word lengths. 16\<close> 17 18lemma neg_num_bintr: 19 "(- numeral x :: 'a::len word) = 20 word_of_int (bintrunc (LENGTH('a)) (-numeral x))" 21 by (simp only: word_ubin.Abs_norm word_neg_numeral_alt) 22 23ML \<open> 24 fun is_refl (Const (@{const_name Pure.eq}, _) $ x $ y) = (x = y) 25 | is_refl _ = false; 26 27 fun signed_dest_wordT (Type (@{type_name word}, [Type (@{type_name signed}, [T])])) = Word_Lib.dest_binT T 28 | signed_dest_wordT T = Word_Lib.dest_wordT T 29 30 fun typ_size_of t = signed_dest_wordT (type_of (Thm.term_of t)); 31 32 fun num_len (Const (@{const_name Num.Bit0}, _) $ n) = num_len n + 1 33 | num_len (Const (@{const_name Num.Bit1}, _) $ n) = num_len n + 1 34 | num_len (Const (@{const_name Num.One}, _)) = 1 35 | num_len (Const (@{const_name numeral}, _) $ t) = num_len t 36 | num_len (Const (@{const_name uminus}, _) $ t) = num_len t 37 | num_len t = raise TERM ("num_len", [t]) 38 39 fun unsigned_norm is_neg _ ctxt ct = 40 (if is_neg orelse num_len (Thm.term_of ct) > typ_size_of ct then let 41 val btr = if is_neg 42 then @{thm neg_num_bintr} else @{thm num_abs_bintr} 43 val th = [Thm.reflexive ct, mk_eq btr] MRS transitive_thm 44 45 (* will work in context of theory Word as well *) 46 val ss = simpset_of (@{context} addsimps @{thms bintrunc_numeral}) 47 val cnv = simplify (put_simpset ss ctxt) th 48 in if is_refl (Thm.prop_of cnv) then NONE else SOME cnv end 49 else NONE) 50 handle TERM ("num_len", _) => NONE 51 | TYPE ("dest_binT", _, _) => NONE 52\<close> 53 54simproc_setup 55 unsigned_norm ("numeral n::'a::len word") = \<open>unsigned_norm false\<close> 56 57simproc_setup 58 unsigned_norm_neg0 ("-numeral (num.Bit0 num)::'a::len word") = \<open>unsigned_norm true\<close> 59 60simproc_setup 61 unsigned_norm_neg1 ("-numeral (num.Bit1 num)::'a::len word") = \<open>unsigned_norm true\<close> 62 63declare word_pow_0 [simp] 64 65lemma minus_one_norm: 66 "(-1 :: 'a :: len word) = of_nat (2 ^ LENGTH('a) - 1)" 67 by (simp add:of_nat_diff) 68 69lemmas minus_one_norm_num = 70 minus_one_norm [where 'a="'b::len bit0"] minus_one_norm [where 'a="'b::len0 bit1"] 71 72lemma "f (7 :: 2 word) = f 3" by simp 73 74lemma "f 7 = f (3 :: 2 word)" by simp 75 76lemma "f (-2) = f (21 + 1 :: 3 word)" by simp 77 78lemma "f (-2) = f (13 + 1 :: 'a::len word)" 79 apply simp (* does not touch generic word length *) 80 oops 81 82lemma "f (-2) = f (0xFFFFFFFE :: 32 word)" by simp 83 84lemma "(-1 :: 2 word) = 3" by simp 85 86lemma "f (-2) = f (0xFFFFFFFE :: 32 signed word)" by simp 87 88 89text \<open> 90 We leave @{term "-1"} untouched by default, because it is often useful 91 and its normal form can be large. 92 To include it in the normalisation, add @{thm [source] minus_one_norm_num}. 93 The additional normalisation is restricted to concrete numeral word lengths, 94 like the rest. 95\<close> 96context 97 notes minus_one_norm_num [simp] 98begin 99 100lemma "f (-1) = f (15 :: 4 word)" by simp 101 102lemma "f (-1) = f (7 :: 3 word)" by simp 103 104lemma "f (-1) = f (0xFFFF :: 16 word)" by simp 105 106lemma "f (-1) = f (0xFFFF + 1 :: 'a::len word)" 107 apply simp (* does not touch generic -1 *) 108 oops 109 110end 111 112end 113