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