(* Title: ZF/ex/BinEx.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Examples of performing binary arithmetic by simplification. theory BinEx imports ZF begin lemma "#13 $+ #19 = #32" by simplemma "#1234 $+ #5678 = #6912" by simplemma "#1359 $+ #-2468 = #-1109" by simplemma "#93746 $+ #-46375 = #47371" by simplemma "$- #65745 = #-65745" by simplemma "$- #-54321 = #54321" by simplemma "#13 $* #19 = #247" by simplemma "#-84 $* #51 = #-4284" by simp(*The worst case for 8-bit operands *) lemma "#255 $* #255 = #65025" by simplemma "#1359 $* #-2468 = #-3354012" by simp(** Comparisons **) lemma "(#89) $* #10 \ #889" by simplemma "(#13) $< #18 $- #4" by simplemma "(#-345) $< #-242 $+ #-100" by simplemma "(#13557456) $< #18678654" by simplemma "(#999999) $\ (#1000001 $+ #1) $- #2" by simplemma "(#1234567) $\ #1234567" by simp(*** Quotient and remainder [they could be faster] ***) lemma "#23 zdiv #3 = #7" by simplemma "#23 zmod #3 = #2" by simp(** negative dividend **) lemma "#-23 zdiv #3 = #-8" by simplemma "#-23 zmod #3 = #1" by simp(** negative divisor **) lemma "#23 zdiv #-3 = #-8" by simplemma "#23 zmod #-3 = #-1" by simp(** negative dividend and divisor **) lemma "#-23 zdiv #-3 = #7" by simplemma "#-23 zmod #-3 = #-2" by simpend quality 100%
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
