wneuper/isa: src/HOL/ex/BinEx.thy@279facb4253a

     1 (*  Title:      HOL/ex/BinEx.thy

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1998  University of Cambridge

     5 *)

     7 header {* Binary arithmetic examples *}

     9 theory BinEx = Main:

    11 subsection {* The Integers *}

    13 text {* Addition *}

    15 lemma "(13::int) + 19 = 32"

    16   by simp

    18 lemma "(1234::int) + 5678 = 6912"

    19   by simp

    21 lemma "(1359::int) + -2468 = -1109"

    22   by simp

    24 lemma "(93746::int) + -46375 = 47371"

    25   by simp

    28 text {* \medskip Negation *}

    30 lemma "- (65745::int) = -65745"

    31   by simp

    33 lemma "- (-54321::int) = 54321"

    34   by simp

    37 text {* \medskip Multiplication *}

    39 lemma "(13::int) * 19 = 247"

    40   by simp

    42 lemma "(-84::int) * 51 = -4284"

    43   by simp

    45 lemma "(255::int) * 255 = 65025"

    46   by simp

    48 lemma "(1359::int) * -2468 = -3354012"

    49   by simp

    51 lemma "(89::int) * 10 \<noteq> 889"

    52   by simp

    54 lemma "(13::int) < 18 - 4"

    55   by simp

    57 lemma "(-345::int) < -242 + -100"

    58   by simp

    60 lemma "(13557456::int) < 18678654"

    61   by simp

    63 lemma "(999999::int) \<le> (1000001 + 1) - 2"

    64   by simp

    66 lemma "(1234567::int) \<le> 1234567"

    67   by simp

    70 text {* \medskip Quotient and Remainder *}

    72 lemma "(10::int) div 3 = 3"

    73   by simp

    75 lemma "(10::int) mod 3 = 1"

    76   by simp

    78 text {* A negative divisor *}

    80 lemma "(10::int) div -3 = -4"

    81   by simp

    83 lemma "(10::int) mod -3 = -2"

    84   by simp

    86 text {*

    87   A negative dividend\footnote{The definition agrees with mathematical

    88   convention but not with the hardware of most computers}

    89 *}

    91 lemma "(-10::int) div 3 = -4"

    92   by simp

    94 lemma "(-10::int) mod 3 = 2"

    95   by simp

    97 text {* A negative dividend \emph{and} divisor *}

    99 lemma "(-10::int) div -3 = 3"

   100   by simp

   102 lemma "(-10::int) mod -3 = -1"

   103   by simp

   105 text {* A few bigger examples *}

   107 lemma "(8452::int) mod 3 = 1"

   108   by simp

   110 lemma "(59485::int) div 434 = 137"

   111   by simp

   113 lemma "(1000006::int) mod 10 = 6"

   114   by simp

   117 text {* \medskip Division by shifting *}

   119 lemma "10000000 div 2 = (5000000::int)"

   120   by simp

   122 lemma "10000001 mod 2 = (1::int)"

   123   by simp

   125 lemma "10000055 div 32 = (312501::int)"

   126   by simp

   128 lemma "10000055 mod 32 = (23::int)"

   129   by simp

   131 lemma "100094 div 144 = (695::int)"

   132   by simp

   134 lemma "100094 mod 144 = (14::int)"

   135   by simp

   138 text {* \medskip Powers *}

   140 lemma "2 ^ 10 = (1024::int)"

   141   by simp

   143 lemma "-3 ^ 7 = (-2187::int)"

   144   by simp

   146 lemma "13 ^ 7 = (62748517::int)"

   147   by simp

   149 lemma "3 ^ 15 = (14348907::int)"

   150   by simp

   152 lemma "-5 ^ 11 = (-48828125::int)"

   153   by simp

   156 subsection {* The Natural Numbers *}

   158 text {* Successor *}

   160 lemma "Suc 99999 = 100000"

   161   by (simp add: Suc_nat_number_of)

   162     -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}

   165 text {* \medskip Addition *}

   167 lemma "(13::nat) + 19 = 32"

   168   by simp

   170 lemma "(1234::nat) + 5678 = 6912"

   171   by simp

   173 lemma "(973646::nat) + 6475 = 980121"

   174   by simp

   177 text {* \medskip Subtraction *}

   179 lemma "(32::nat) - 14 = 18"

   180   by simp

   182 lemma "(14::nat) - 15 = 0"

   183   by simp

   185 lemma "(14::nat) - 1576644 = 0"

   186   by simp

   188 lemma "(48273776::nat) - 3873737 = 44400039"

   189   by simp

   192 text {* \medskip Multiplication *}

   194 lemma "(12::nat) * 11 = 132"

   195   by simp

   197 lemma "(647::nat) * 3643 = 2357021"

   198   by simp

   201 text {* \medskip Quotient and Remainder *}

   203 lemma "(10::nat) div 3 = 3"

   204   by simp

   206 lemma "(10::nat) mod 3 = 1"

   207   by simp

   209 lemma "(10000::nat) div 9 = 1111"

   210   by simp

   212 lemma "(10000::nat) mod 9 = 1"

   213   by simp

   215 lemma "(10000::nat) div 16 = 625"

   216   by simp

   218 lemma "(10000::nat) mod 16 = 0"

   219   by simp

   222 text {* \medskip Powers *}

   224 lemma "2 ^ 12 = (4096::nat)"

   225   by simp

   227 lemma "3 ^ 10 = (59049::nat)"

   228   by simp

   230 lemma "12 ^ 7 = (35831808::nat)"

   231   by simp

   233 lemma "3 ^ 14 = (4782969::nat)"

   234   by simp

   236 lemma "5 ^ 11 = (48828125::nat)"

   237   by simp

   240 text {* \medskip Testing the cancellation of complementary terms *}

   242 lemma "y + (x + -x) = (0::int) + y"

   243   by simp

   245 lemma "y + (-x + (- y + x)) = (0::int)"

   246   by simp

   248 lemma "-x + (y + (- y + x)) = (0::int)"

   249   by simp

   251 lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"

   252   by simp

   254 lemma "x + x - x - x - y - z = (0::int) - y - z"

   255   by simp

   257 lemma "x + y + z - (x + z) = y - (0::int)"

   258   by simp

   260 lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"

   261   by simp

   263 lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"

   264   by simp

   266 lemma "x + y - x + z - x - y - z + x < (1::int)"

   267   by simp

   270 subsection {* Normal form of bit strings *}

   272 text {*

   273   Definition of normal form for proving that binary arithmetic on

   274   normalized operands yields normalized results.  Normal means no

   275   leading 0s on positive numbers and no leading 1s on negatives.

   276 *}

   278 consts normal :: "bin set"

   279 inductive normal

   280   intros

   281     Pls [simp]: "Pls: normal"

   282     Min [simp]: "Min: normal"

   283     BIT_F [simp]: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"

   284     BIT_T [simp]: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"

   286 text {*

   287   \medskip Binary arithmetic on normalized operands yields normalized

   288   results.

   289 *}

   291 lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal"

   292   apply (case_tac c)

   293    apply auto

   294   done

   296 lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal"

   297   apply (erule normal.cases)

   298      apply auto

   299   done

   301 lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal"

   302   apply (induct w)

   303     apply (auto simp add: NCons_Pls NCons_Min)

   304   done

   306 lemma NCons_True: "NCons w True \<noteq> Pls"

   307   apply (induct w)

   308     apply auto

   309   done

   311 lemma NCons_False: "NCons w False \<noteq> Min"

   312   apply (induct w)

   313     apply auto

   314   done

   316 lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> normal"

   317   apply (erule normal.induct)

   318      apply (case_tac [4] w)

   319   apply (auto simp add: NCons_True bin_succ_BIT)

   320   done

   322 lemma bin_pred_normal [simp]: "w \<in> normal ==> bin_pred w \<in> normal"

   323   apply (erule normal.induct)

   324      apply (case_tac [3] w)

   325   apply (auto simp add: NCons_False bin_pred_BIT)

   326   done

   328 lemma bin_add_normal [rule_format]:

   329   "w \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> normal)"

   330   apply (induct w)

   331     apply simp

   332    apply simp

   333   apply (rule impI)

   334   apply (rule allI)

   335   apply (induct_tac z)

   336     apply (simp_all add: bin_add_BIT)

   337   apply (safe dest!: normal_BIT_D)

   338     apply simp_all

   339   done

   341 lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (0::int))"

   342   apply (erule normal.induct)

   343      apply auto

   344   done

   346 lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"

   347   apply (erule normal.induct)

   348      apply (simp_all add: bin_minus_BIT)

   349   apply (rule normal.intros)

   350   apply assumption

   351   apply (simp add: normal_Pls_eq_0)

   352   apply (simp only: number_of_minus iszero_def zminus_equation [of _ "0"])

   353   apply (rule not_sym)

   354   apply simp

   355   done

   357 lemma bin_mult_normal [rule_format]:

   358     "w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"

   359   apply (erule normal.induct)

   360      apply (simp_all add: bin_minus_normal bin_mult_BIT)

   361   apply (safe dest!: normal_BIT_D)

   362   apply (simp add: bin_add_normal)

   363   done

   365 end

author	paulson
	Wed, 02 Jan 2002 16:06:31 +0100
changeset 12613	279facb4253a
parent 11868	56db9f3a6b3e
child 13187	e5434b822a96
permissions	-rw-r--r--