src/ZF/Bin.thy
 author paulson Tue Mar 06 15:15:49 2012 +0000 (2012-03-06) changeset 46820 c656222c4dc1 parent 45703 c7a13ce60161 child 46821 ff6b0c1087f2 permissions -rw-r--r--
1 (*  Title:      ZF/Bin.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1994  University of Cambridge
5    The sign Pls stands for an infinite string of leading 0's.
6    The sign Min stands for an infinite string of leading 1's.
8 A number can have multiple representations, namely leading 0's with sign
9 Pls and leading 1's with sign Min.  See twos-compl.ML/int_of_binary for
10 the numerical interpretation.
12 The representation expects that (m mod 2) is 0 or 1, even if m is negative;
13 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
14 *)
18 theory Bin
19 imports Int_ZF Datatype_ZF
20 uses ("Tools/numeral_syntax.ML")
21 begin
23 consts  bin :: i
24 datatype
25   "bin" = Pls
26         | Min
27         | Bit ("w: bin", "b: bool")     (infixl "BIT" 90)
29 consts
30   integ_of  :: "i=>i"
31   NCons     :: "[i,i]=>i"
32   bin_succ  :: "i=>i"
33   bin_pred  :: "i=>i"
34   bin_minus :: "i=>i"
36   bin_mult  :: "[i,i]=>i"
38 primrec
39   integ_of_Pls:  "integ_of (Pls)     = \$# 0"
40   integ_of_Min:  "integ_of (Min)     = \$-(\$#1)"
41   integ_of_BIT:  "integ_of (w BIT b) = \$#b \$+ integ_of(w) \$+ integ_of(w)"
43     (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
46   NCons_Pls: "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
47   NCons_Min: "NCons (Min,b)     = cond(b,Min,Min BIT b)"
48   NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b"
50 primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
51   bin_succ_Pls:  "bin_succ (Pls)     = Pls BIT 1"
52   bin_succ_Min:  "bin_succ (Min)     = Pls"
53   bin_succ_BIT:  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
55 primrec (*predecessor*)
56   bin_pred_Pls:  "bin_pred (Pls)     = Min"
57   bin_pred_Min:  "bin_pred (Min)     = Min BIT 0"
58   bin_pred_BIT:  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
60 primrec (*unary negation*)
61   bin_minus_Pls:
62     "bin_minus (Pls)       = Pls"
63   bin_minus_Min:
64     "bin_minus (Min)       = Pls BIT 1"
65   bin_minus_BIT:
66     "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
67                                 bin_minus(w) BIT 0)"
69 primrec (*sum*)
71     "bin_adder (Pls)     = (\<lambda>w\<in>bin. w)"
73     "bin_adder (Min)     = (\<lambda>w\<in>bin. bin_pred(w))"
75     "bin_adder (v BIT x) =
76        (\<lambda>w\<in>bin.
77          bin_case (v BIT x, bin_pred(v BIT x),
78                    %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w),
79                                x xor y),
80                    w))"
82 (*The bin_case above replaces the following mutually recursive function:
83 primrec
84   "adding (v,x,Pls)     = v BIT x"
85   "adding (v,x,Min)     = bin_pred(v BIT x)"
86   "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)),
87                                 x xor y)"
88 *)
90 definition
95 primrec
96   bin_mult_Pls:
97     "bin_mult (Pls,w)     = Pls"
98   bin_mult_Min:
99     "bin_mult (Min,w)     = bin_minus(w)"
100   bin_mult_BIT:
101     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
102                                  NCons(bin_mult(v,w),0))"
104 syntax
105   "_Int"    :: "xnum_token => i"        ("_")
107 use "Tools/numeral_syntax.ML"
108 setup Numeral_Syntax.setup
111 declare bin.intros [simp,TC]
113 lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
114 by simp
116 lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
117 by simp
119 lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
120 by simp
122 lemma NCons_Min_1: "NCons(Min,1) = Min"
123 by simp
125 lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
128 lemmas NCons_simps [simp] =
129     NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
133 (** Type checking **)
135 lemma integ_of_type [TC]: "w: bin ==> integ_of(w) \<in> int"
136 apply (induct_tac "w")
138 done
140 lemma NCons_type [TC]: "[| w: bin; b: bool |] ==> NCons(w,b) \<in> bin"
141 by (induct_tac "w", auto)
143 lemma bin_succ_type [TC]: "w: bin ==> bin_succ(w) \<in> bin"
144 by (induct_tac "w", auto)
146 lemma bin_pred_type [TC]: "w: bin ==> bin_pred(w) \<in> bin"
147 by (induct_tac "w", auto)
149 lemma bin_minus_type [TC]: "w: bin ==> bin_minus(w) \<in> bin"
150 by (induct_tac "w", auto)
152 (*This proof is complicated by the mutual recursion*)
154      "v: bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
156 apply (induct_tac "v")
157 apply (rule_tac [3] ballI)
158 apply (rename_tac [3] "w'")
159 apply (induct_tac [3] "w'")
161 done
163 lemma bin_mult_type [TC]: "[| v: bin; w: bin |] ==> bin_mult(v,w) \<in> bin"
164 by (induct_tac "v", auto)
167 subsubsection{*The Carry and Borrow Functions,
168             @{term bin_succ} and @{term bin_pred}*}
170 (*NCons preserves the integer value of its argument*)
171 lemma integ_of_NCons [simp]:
172      "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"
173 apply (erule bin.cases)
174 apply (auto elim!: boolE)
175 done
177 lemma integ_of_succ [simp]:
178      "w: bin ==> integ_of(bin_succ(w)) = \$#1 \$+ integ_of(w)"
179 apply (erule bin.induct)
181 done
183 lemma integ_of_pred [simp]:
184      "w: bin ==> integ_of(bin_pred(w)) = \$- (\$#1) \$+ integ_of(w)"
185 apply (erule bin.induct)
187 done
190 subsubsection{*@{term bin_minus}: Unary Negation of Binary Integers*}
192 lemma integ_of_minus: "w: bin ==> integ_of(bin_minus(w)) = \$- integ_of(w)"
193 apply (erule bin.induct)
195 done
205 apply (erule bin.induct, auto)
206 done
213 apply (erule bin.induct, auto)
214 done
223      "[| w: bin;  y: bool |]
224       ==> bin_add(v BIT x, w BIT y) =
225           NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"
229      "v: bin ==>
230           \<forall>w\<in>bin. integ_of(bin_add(v,w)) = integ_of(v) \$+ integ_of(w)"
231 apply (erule bin.induct, simp, simp)
232 apply (rule ballI)
233 apply (induct_tac "wa")
235 done
237 (*Subtraction*)
238 lemma diff_integ_of_eq:
239      "[| v: bin;  w: bin |]
240       ==> integ_of(v) \$- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
241 apply (unfold zdiff_def)
243 done
246 subsubsection{*@{term bin_mult}: Binary Multiplication*}
248 lemma integ_of_mult:
249      "[| v: bin;  w: bin |]
250       ==> integ_of(bin_mult(v,w)) = integ_of(v) \$* integ_of(w)"
251 apply (induct_tac "v", simp)
254 done
257 subsection{*Computations*}
259 (** extra rules for bin_succ, bin_pred **)
261 lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
262 by simp
264 lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
265 by simp
267 lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
268 by simp
270 lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
271 by simp
273 (** extra rules for bin_minus **)
275 lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
276 by simp
278 lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
279 by simp
281 (** extra rules for bin_add **)
283 lemma bin_add_BIT_11: "w: bin ==> bin_add(v BIT 1, w BIT 1) =
285 by simp
287 lemma bin_add_BIT_10: "w: bin ==> bin_add(v BIT 1, w BIT 0) =
289 by simp
291 lemma bin_add_BIT_0: "[| w: bin;  y: bool |]
293 by simp
295 (** extra rules for bin_mult **)
297 lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
298 by simp
300 lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
301 by simp
304 (** Simplification rules with integer constants **)
306 lemma int_of_0: "\$#0 = #0"
307 by simp
309 lemma int_of_succ: "\$# succ(n) = #1 \$+ \$#n"
312 lemma zminus_0 [simp]: "\$- #0 = #0"
313 by simp
315 lemma zadd_0_intify [simp]: "#0 \$+ z = intify(z)"
316 by simp
318 lemma zadd_0_right_intify [simp]: "z \$+ #0 = intify(z)"
319 by simp
321 lemma zmult_1_intify [simp]: "#1 \$* z = intify(z)"
322 by simp
324 lemma zmult_1_right_intify [simp]: "z \$* #1 = intify(z)"
325 by (subst zmult_commute, simp)
327 lemma zmult_0 [simp]: "#0 \$* z = #0"
328 by simp
330 lemma zmult_0_right [simp]: "z \$* #0 = #0"
331 by (subst zmult_commute, simp)
333 lemma zmult_minus1 [simp]: "#-1 \$* z = \$-z"
336 lemma zmult_minus1_right [simp]: "z \$* #-1 = \$-z"
337 apply (subst zmult_commute)
338 apply (rule zmult_minus1)
339 done
342 subsection{*Simplification Rules for Comparison of Binary Numbers*}
343 text{*Thanks to Norbert Voelker*}
345 (** Equals (=) **)
347 lemma eq_integ_of_eq:
348      "[| v: bin;  w: bin |]
349       ==> ((integ_of(v)) = integ_of(w)) <->
350           iszero (integ_of (bin_add (v, bin_minus(w))))"
351 apply (unfold iszero_def)
353 done
355 lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
356 by (unfold iszero_def, simp)
359 lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
360 apply (unfold iszero_def)
362 done
364 lemma iszero_integ_of_BIT:
365      "[| w: bin; x: bool |]
366       ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"
367 apply (unfold iszero_def, simp)
368 apply (subgoal_tac "integ_of (w) \<in> int")
369 apply typecheck
370 apply (drule int_cases)
371 apply (safe elim!: boolE)
374 done
376 lemma iszero_integ_of_0:
377      "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"
378 by (simp only: iszero_integ_of_BIT, blast)
380 lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
381 by (simp only: iszero_integ_of_BIT, blast)
385 (** Less-than (<) **)
387 lemma less_integ_of_eq_neg:
388      "[| v: bin;  w: bin |]
389       ==> integ_of(v) \$< integ_of(w)
390           <-> znegative (integ_of (bin_add (v, bin_minus(w))))"
391 apply (unfold zless_def zdiff_def)
393 done
395 lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
396 by simp
398 lemma neg_integ_of_Min: "znegative (integ_of(Min))"
399 by simp
401 lemma neg_integ_of_BIT:
402      "[| w: bin; x: bool |]
403       ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"
404 apply simp
405 apply (subgoal_tac "integ_of (w) \<in> int")
406 apply typecheck
407 apply (drule int_cases)
411 apply (subgoal_tac "\$#1 \$- \$# succ (succ (n #+ n)) = \$- \$# succ (n #+ n) ")
413 apply (simp add: equation_zminus int_of_diff [symmetric])
414 done
416 (** Less-than-or-equals (<=) **)
418 lemma le_integ_of_eq_not_less:
419      "(integ_of(x) \$<= (integ_of(w))) <-> ~ (integ_of(w) \$< (integ_of(x)))"
420 by (simp add: not_zless_iff_zle [THEN iff_sym])
423 (*Delete the original rewrites, with their clumsy conditional expressions*)
424 declare bin_succ_BIT [simp del]
425         bin_pred_BIT [simp del]
426         bin_minus_BIT [simp del]
427         NCons_Pls [simp del]
428         NCons_Min [simp del]
430         bin_mult_BIT [simp del]
432 (*Hide the binary representation of integer constants*)
433 declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del]
436 lemmas bin_arith_extra_simps =
438      integ_of_minus [symmetric]
439      integ_of_mult [symmetric]
440      bin_succ_1 bin_succ_0
441      bin_pred_1 bin_pred_0
442      bin_minus_1 bin_minus_0
445      diff_integ_of_eq
446      bin_mult_1 bin_mult_0 NCons_simps
449 (*For making a minimal simpset, one must include these default simprules
450   of thy.  Also include simp_thms, or at least (~False)=True*)
451 lemmas bin_arith_simps =
452      bin_pred_Pls bin_pred_Min
453      bin_succ_Pls bin_succ_Min
455      bin_minus_Pls bin_minus_Min
456      bin_mult_Pls bin_mult_Min
457      bin_arith_extra_simps
459 (*Simplification of relational operations*)
460 lemmas bin_rel_simps =
461      eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min
462      iszero_integ_of_0 iszero_integ_of_1
463      less_integ_of_eq_neg
464      not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT
465      le_integ_of_eq_not_less
467 declare bin_arith_simps [simp]
468 declare bin_rel_simps [simp]
471 (** Simplification of arithmetic when nested to the right **)
474      "[| v: bin;  w: bin |]
475       ==> integ_of(v) \$+ (integ_of(w) \$+ z) = (integ_of(bin_add(v,w)) \$+ z)"
478 lemma mult_integ_of_left [simp]:
479      "[| v: bin;  w: bin |]
480       ==> integ_of(v) \$* (integ_of(w) \$* z) = (integ_of(bin_mult(v,w)) \$* z)"
481 by (simp add: zmult_assoc [symmetric])
484     "[| v: bin;  w: bin |]
485       ==> integ_of(v) \$+ (integ_of(w) \$- c) = integ_of(bin_add(v,w)) \$- (c)"
486 apply (unfold zdiff_def)
488 done
491      "[| v: bin;  w: bin |]
492       ==> integ_of(v) \$+ (c \$- integ_of(w)) =
493           integ_of (bin_add (v, bin_minus(w))) \$+ (c)"
494 apply (subst diff_integ_of_eq [symmetric])
496 done
499 (** More for integer constants **)
501 declare int_of_0 [simp] int_of_succ [simp]
503 lemma zdiff0 [simp]: "#0 \$- x = \$-x"
506 lemma zdiff0_right [simp]: "x \$- #0 = intify(x)"
509 lemma zdiff_self [simp]: "x \$- x = #0"
512 lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k \$< #0"
515 lemma zero_zless_imp_znegative_zminus: "[|#0 \$< k; k: int|] ==> znegative(\$-k)"
518 lemma zero_zle_int_of [simp]: "#0 \$<= \$# n"
519 by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
521 lemma nat_of_0 [simp]: "nat_of(#0) = 0"
522 by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
524 lemma nat_le_int0_lemma: "[| z \$<= \$#0; z: int |] ==> nat_of(z) = 0"
525 by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of)
527 lemma nat_le_int0: "z \$<= \$#0 ==> nat_of(z) = 0"
528 apply (subgoal_tac "nat_of (intify (z)) = 0")
529 apply (rule_tac [2] nat_le_int0_lemma, auto)
530 done
532 lemma int_of_eq_0_imp_natify_eq_0: "\$# n = #0 ==> natify(n) = 0"
533 by (rule not_znegative_imp_zero, auto)
535 lemma nat_of_zminus_int_of: "nat_of(\$- \$# n) = 0"
536 by (simp add: nat_of_def int_of_def raw_nat_of zminus image_intrel_int)
538 lemma int_of_nat_of: "#0 \$<= z ==> \$# nat_of(z) = intify(z)"
539 apply (rule not_zneg_nat_of_intify)
540 apply (simp add: znegative_iff_zless_0 not_zless_iff_zle)
541 done
543 declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
545 lemma int_of_nat_of_if: "\$# nat_of(z) = (if #0 \$<= z then intify(z) else #0)"
546 by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
548 lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> (\$#m \$< z)"
549 apply (case_tac "znegative (z) ")
550 apply (erule_tac [2] not_zneg_nat_of [THEN subst])
551 apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
553 done
556 (** nat_of and zless **)
558 (*An alternative condition is  @{term"\$#0 \<subseteq> w"}  *)
559 lemma zless_nat_conj_lemma: "\$#0 \$< z ==> (nat_of(w) < nat_of(z)) <-> (w \$< z)"
560 apply (rule iff_trans)
561 apply (rule zless_int_of [THEN iff_sym])
562 apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
563 apply (auto elim: zless_asym simp add: not_zle_iff_zless)
564 apply (blast intro: zless_zle_trans)
565 done
567 lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) <-> (\$#0 \$< z & w \$< z)"
568 apply (case_tac "\$#0 \$< z")
569 apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
570 done
572 (*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
573   unconditional!
574   [The condition "True" is a hack to prevent looping.
575     Conditional rewrite rules are tried after unconditional ones, so a rule
576     like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
577   lemma integ_of_reorient [simp]:
578        "True ==> (integ_of(w) = x) <-> (x = integ_of(w))"
579   by auto
580 *)
582 lemma integ_of_minus_reorient [simp]:
583      "(integ_of(w) = \$- x) <-> (\$- x = integ_of(w))"
584 by auto