1 (* Title: HOL/Integ/Bin.thy
3 Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1994 University of Cambridge
6 Ported from ZF to HOL by David Spelt.
9 header{*Arithmetic on Binary Integers*}
11 theory Bin = IntDef + Numeral:
13 axclass number_ring \<subseteq> number, comm_ring_1
14 number_of_Pls: "number_of bin.Pls = 0"
15 number_of_Min: "number_of bin.Min = - 1"
16 number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
17 (number_of w) + (number_of w)"
18 subsection{*Converting Numerals to Rings: @{term number_of}*}
20 lemmas number_of = number_of_Pls number_of_Min number_of_BIT
22 lemma number_of_NCons [simp]:
23 "number_of(NCons w b) = (number_of(w BIT b)::'a::number_ring)"
24 by (induct_tac "w", simp_all add: number_of)
26 lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
27 apply (induct_tac "w")
28 apply (simp_all add: number_of add_ac)
31 lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
32 apply (induct_tac "w")
33 apply (simp_all add: number_of add_assoc [symmetric])
34 apply (simp add: add_ac)
37 lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
38 apply (induct_tac "w")
39 apply (simp_all del: bin_pred_Pls bin_pred_Min bin_pred_BIT
40 add: number_of number_of_succ number_of_pred add_assoc)
43 text{*This proof is complicated by the mutual recursion*}
44 lemma number_of_add [rule_format]:
45 "\<forall>w. number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
46 apply (induct_tac "v")
47 apply (simp add: number_of)
48 apply (simp add: number_of number_of_pred)
50 apply (induct_tac "w")
51 apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac)
52 apply (simp add: add_left_commute [of "1::'a::number_ring"])
56 "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
57 apply (induct_tac "v", simp add: number_of)
58 apply (simp add: number_of number_of_minus)
59 apply (simp add: number_of number_of_add left_distrib add_ac)
62 text{*The correctness of shifting. But it doesn't seem to give a measurable
64 lemma double_number_of_BIT:
65 "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
66 apply (induct_tac "w")
67 apply (simp_all add: number_of number_of_add left_distrib add_ac)
71 text{*Converting numerals 0 and 1 to their abstract versions*}
72 lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
73 by (simp add: number_of)
75 lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
76 by (simp add: number_of)
78 text{*Special-case simplification for small constants*}
80 text{*Unary minus for the abstract constant 1. Cannot be inserted
81 as a simprule until later: it is @{text number_of_Min} re-oriented!*}
82 lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
83 by (simp add: number_of)
85 lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
86 by (simp add: numeral_m1_eq_minus_1)
88 lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
89 by (simp add: numeral_m1_eq_minus_1)
91 (*Negation of a coefficient*)
92 lemma minus_number_of_mult [simp]:
93 "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
94 by (simp add: number_of_minus)
97 lemma diff_number_of_eq:
98 "number_of v - number_of w =
99 (number_of(bin_add v (bin_minus w))::'a::number_ring)"
100 by (simp add: diff_minus number_of_add number_of_minus)
103 subsection{*Equality of Binary Numbers*}
105 text{*First version by Norbert Voelker*}
107 lemma eq_number_of_eq:
108 "((number_of x::'a::number_ring) = number_of y) =
109 iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
110 by (simp add: iszero_def compare_rls number_of_add number_of_minus)
112 lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::'a::number_ring)"
113 by (simp add: iszero_def numeral_0_eq_0)
115 lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::'a::number_ring)"
116 by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
119 subsection{*Comparisons, for Ordered Rings*}
121 lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
123 have "a + a = (1+1)*a" by (simp add: left_distrib)
124 with zero_less_two [where 'a = 'a]
125 show ?thesis by force
129 assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
132 also have "... < z + 1" by (rule less_add_one)
133 also have "... = 1 + z" by (simp add: add_ac)
134 finally show "0 < 1 + z" .
137 lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
138 proof (cases z rule: int_cases)
140 have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
141 thus ?thesis using le_imp_0_less [OF le]
142 by (auto simp add: add_assoc)
147 assume eq: "1 + z + z = 0"
148 have "0 < 1 + (int n + int n)"
149 by (simp add: le_imp_0_less add_increasing)
150 also have "... = - (1 + z + z)"
151 by (simp add: neg add_assoc [symmetric], simp add: add_commute)
152 also have "... = 0" by (simp add: eq)
153 finally have "0<0" ..
159 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
160 lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
161 proof (unfold Ints_def)
162 assume "a \<in> range of_int"
163 then obtain z where a: "a = of_int z" ..
166 assume eq: "1 + a + a = 0"
167 hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
168 hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
169 with odd_nonzero show False by blast
173 lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
174 by (induct_tac "w", simp_all add: number_of)
176 lemma iszero_number_of_BIT:
177 "iszero (number_of (w BIT x)::'a) =
178 (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
179 by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff
180 number_of Ints_odd_nonzero [OF Ints_number_of])
182 lemma iszero_number_of_0:
183 "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) =
184 iszero (number_of w :: 'a)"
185 by (simp only: iszero_number_of_BIT simp_thms)
187 lemma iszero_number_of_1:
188 "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
189 by (simp only: iszero_number_of_BIT simp_thms)
193 subsection{*The Less-Than Relation*}
195 lemma less_number_of_eq_neg:
196 "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
197 = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
198 apply (subst less_iff_diff_less_0)
199 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
202 text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
203 @{term Numeral0} IS @{term "number_of Pls"} *}
204 lemma not_neg_number_of_Pls:
205 "~ neg (number_of bin.Pls ::'a::{ordered_idom,number_ring})"
206 by (simp add: neg_def numeral_0_eq_0)
208 lemma neg_number_of_Min:
209 "neg (number_of bin.Min ::'a::{ordered_idom,number_ring})"
210 by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
212 lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
214 have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
215 also have "... = (a < 0)"
216 by (simp add: mult_less_0_iff zero_less_two
217 order_less_not_sym [OF zero_less_two])
218 finally show ?thesis .
221 lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
222 proof (cases z rule: int_cases)
224 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
225 le_imp_0_less [THEN order_less_imp_le])
228 thus ?thesis by (simp del: int_Suc
229 add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
232 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
233 lemma Ints_odd_less_0:
234 "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
235 proof (unfold Ints_def)
236 assume "a \<in> range of_int"
237 then obtain z where a: "a = of_int z" ..
238 hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
240 also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
241 also have "... = (a < 0)" by (simp add: a)
242 finally show ?thesis .
245 lemma neg_number_of_BIT:
246 "neg (number_of (w BIT x)::'a) =
247 neg (number_of w :: 'a::{ordered_idom,number_ring})"
248 by (simp add: number_of neg_def double_less_0_iff
249 Ints_odd_less_0 [OF Ints_number_of])
252 text{*Less-Than or Equals*}
254 text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
255 lemmas le_number_of_eq_not_less =
256 linorder_not_less [of "number_of w" "number_of v", symmetric,
259 lemma le_number_of_eq:
260 "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
261 = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
262 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
265 text{*Absolute value (@{term abs})*}
268 "abs(number_of x::'a::{ordered_idom,number_ring}) =
269 (if number_of x < (0::'a) then -number_of x else number_of x)"
270 by (simp add: abs_if)
273 text{*Re-orientation of the equation nnn=x*}
274 lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
278 (*Delete the original rewrites, with their clumsy conditional expressions*)
279 declare bin_succ_BIT [simp del] bin_pred_BIT [simp del]
280 bin_minus_BIT [simp del]
282 declare bin_add_BIT [simp del] bin_mult_BIT [simp del]
283 declare NCons_Pls [simp del] NCons_Min [simp del]
285 (*Hide the binary representation of integer constants*)
286 declare number_of_Pls [simp del] number_of_Min [simp del]
287 number_of_BIT [simp del]
291 (*Simplification of arithmetic operations on integer constants.
292 Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
294 lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
296 lemmas bin_arith_extra_simps =
297 number_of_add [symmetric]
298 number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
299 number_of_mult [symmetric]
300 bin_succ_1 bin_succ_0
301 bin_pred_1 bin_pred_0
302 bin_minus_1 bin_minus_0
303 bin_add_Pls_right bin_add_Min_right
304 bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
305 diff_number_of_eq abs_number_of abs_zero abs_one
306 bin_mult_1 bin_mult_0 NCons_simps
308 (*For making a minimal simpset, one must include these default simprules
309 of thy. Also include simp_thms, or at least (~False)=True*)
310 lemmas bin_arith_simps =
311 bin_pred_Pls bin_pred_Min
312 bin_succ_Pls bin_succ_Min
313 bin_add_Pls bin_add_Min
314 bin_minus_Pls bin_minus_Min
315 bin_mult_Pls bin_mult_Min bin_arith_extra_simps
317 (*Simplification of relational operations*)
318 lemmas bin_rel_simps =
319 eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
320 iszero_number_of_0 iszero_number_of_1
321 less_number_of_eq_neg
322 not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
323 neg_number_of_Min neg_number_of_BIT
326 declare bin_arith_extra_simps [simp]
327 declare bin_rel_simps [simp]
330 subsection{*Simplification of arithmetic when nested to the right*}
332 lemma add_number_of_left [simp]:
333 "number_of v + (number_of w + z) =
334 (number_of(bin_add v w) + z::'a::number_ring)"
335 by (simp add: add_assoc [symmetric])
337 lemma mult_number_of_left [simp]:
338 "number_of v * (number_of w * z) =
339 (number_of(bin_mult v w) * z::'a::number_ring)"
340 by (simp add: mult_assoc [symmetric])
342 lemma add_number_of_diff1:
343 "number_of v + (number_of w - c) =
344 number_of(bin_add v w) - (c::'a::number_ring)"
345 by (simp add: diff_minus add_number_of_left)
347 lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
348 number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
349 apply (subst diff_number_of_eq [symmetric])
350 apply (simp only: compare_rls)