src/ZF/Bin.thy
 author wenzelm Sat Feb 13 23:24:57 2010 +0100 (2010-02-13) changeset 35123 e286d5df187a parent 35112 ff6f60e6ab85 child 45703 c7a13ce60161 permissions -rw-r--r--
modernized structures;
```     1 (*  Title:      ZF/Bin.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1994  University of Cambridge
```
```     4
```
```     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.
```
```     7
```
```     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.
```
```    11
```
```    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 *)
```
```    15
```
```    16 header{*Arithmetic on Binary Integers*}
```
```    17
```
```    18 theory Bin
```
```    19 imports Int_ZF Datatype_ZF
```
```    20 uses ("Tools/numeral_syntax.ML")
```
```    21 begin
```
```    22
```
```    23 consts  bin :: i
```
```    24 datatype
```
```    25   "bin" = Pls
```
```    26         | Min
```
```    27         | Bit ("w: bin", "b: bool")     (infixl "BIT" 90)
```
```    28
```
```    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"
```
```    35   bin_adder :: "i=>i"
```
```    36   bin_mult  :: "[i,i]=>i"
```
```    37
```
```    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)"
```
```    42
```
```    43     (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
```
```    44
```
```    45 primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
```
```    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"
```
```    49
```
```    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))"
```
```    54
```
```    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)"
```
```    59
```
```    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)"
```
```    68
```
```    69 primrec (*sum*)
```
```    70   bin_adder_Pls:
```
```    71     "bin_adder (Pls)     = (lam w:bin. w)"
```
```    72   bin_adder_Min:
```
```    73     "bin_adder (Min)     = (lam w:bin. bin_pred(w))"
```
```    74   bin_adder_BIT:
```
```    75     "bin_adder (v BIT x) =
```
```    76        (lam w: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))"
```
```    81
```
```    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 *)
```
```    89
```
```    90 definition
```
```    91   bin_add   :: "[i,i]=>i"  where
```
```    92     "bin_add(v,w) == bin_adder(v)`w"
```
```    93
```
```    94
```
```    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))"
```
```   103
```
```   104 syntax
```
```   105   "_Int"    :: "xnum => i"        ("_")
```
```   106
```
```   107 use "Tools/numeral_syntax.ML"
```
```   108 setup Numeral_Syntax.setup
```
```   109
```
```   110
```
```   111 declare bin.intros [simp,TC]
```
```   112
```
```   113 lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
```
```   114 by simp
```
```   115
```
```   116 lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
```
```   117 by simp
```
```   118
```
```   119 lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
```
```   120 by simp
```
```   121
```
```   122 lemma NCons_Min_1: "NCons(Min,1) = Min"
```
```   123 by simp
```
```   124
```
```   125 lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
```
```   126 by (simp add: bin.case_eqns)
```
```   127
```
```   128 lemmas NCons_simps [simp] =
```
```   129     NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
```
```   130
```
```   131
```
```   132
```
```   133 (** Type checking **)
```
```   134
```
```   135 lemma integ_of_type [TC]: "w: bin ==> integ_of(w) : int"
```
```   136 apply (induct_tac "w")
```
```   137 apply (simp_all add: bool_into_nat)
```
```   138 done
```
```   139
```
```   140 lemma NCons_type [TC]: "[| w: bin; b: bool |] ==> NCons(w,b) : bin"
```
```   141 by (induct_tac "w", auto)
```
```   142
```
```   143 lemma bin_succ_type [TC]: "w: bin ==> bin_succ(w) : bin"
```
```   144 by (induct_tac "w", auto)
```
```   145
```
```   146 lemma bin_pred_type [TC]: "w: bin ==> bin_pred(w) : bin"
```
```   147 by (induct_tac "w", auto)
```
```   148
```
```   149 lemma bin_minus_type [TC]: "w: bin ==> bin_minus(w) : bin"
```
```   150 by (induct_tac "w", auto)
```
```   151
```
```   152 (*This proof is complicated by the mutual recursion*)
```
```   153 lemma bin_add_type [rule_format,TC]:
```
```   154      "v: bin ==> ALL w: bin. bin_add(v,w) : bin"
```
```   155 apply (unfold bin_add_def)
```
```   156 apply (induct_tac "v")
```
```   157 apply (rule_tac [3] ballI)
```
```   158 apply (rename_tac [3] "w'")
```
```   159 apply (induct_tac [3] "w'")
```
```   160 apply (simp_all add: NCons_type)
```
```   161 done
```
```   162
```
```   163 lemma bin_mult_type [TC]: "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin"
```
```   164 by (induct_tac "v", auto)
```
```   165
```
```   166
```
```   167 subsubsection{*The Carry and Borrow Functions,
```
```   168             @{term bin_succ} and @{term bin_pred}*}
```
```   169
```
```   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
```
```   176
```
```   177 lemma integ_of_succ [simp]:
```
```   178      "w: bin ==> integ_of(bin_succ(w)) = \$#1 \$+ integ_of(w)"
```
```   179 apply (erule bin.induct)
```
```   180 apply (auto simp add: zadd_ac elim!: boolE)
```
```   181 done
```
```   182
```
```   183 lemma integ_of_pred [simp]:
```
```   184      "w: bin ==> integ_of(bin_pred(w)) = \$- (\$#1) \$+ integ_of(w)"
```
```   185 apply (erule bin.induct)
```
```   186 apply (auto simp add: zadd_ac elim!: boolE)
```
```   187 done
```
```   188
```
```   189
```
```   190 subsubsection{*@{term bin_minus}: Unary Negation of Binary Integers*}
```
```   191
```
```   192 lemma integ_of_minus: "w: bin ==> integ_of(bin_minus(w)) = \$- integ_of(w)"
```
```   193 apply (erule bin.induct)
```
```   194 apply (auto simp add: zadd_ac zminus_zadd_distrib  elim!: boolE)
```
```   195 done
```
```   196
```
```   197
```
```   198 subsubsection{*@{term bin_add}: Binary Addition*}
```
```   199
```
```   200 lemma bin_add_Pls [simp]: "w: bin ==> bin_add(Pls,w) = w"
```
```   201 by (unfold bin_add_def, simp)
```
```   202
```
```   203 lemma bin_add_Pls_right: "w: bin ==> bin_add(w,Pls) = w"
```
```   204 apply (unfold bin_add_def)
```
```   205 apply (erule bin.induct, auto)
```
```   206 done
```
```   207
```
```   208 lemma bin_add_Min [simp]: "w: bin ==> bin_add(Min,w) = bin_pred(w)"
```
```   209 by (unfold bin_add_def, simp)
```
```   210
```
```   211 lemma bin_add_Min_right: "w: bin ==> bin_add(w,Min) = bin_pred(w)"
```
```   212 apply (unfold bin_add_def)
```
```   213 apply (erule bin.induct, auto)
```
```   214 done
```
```   215
```
```   216 lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x"
```
```   217 by (unfold bin_add_def, simp)
```
```   218
```
```   219 lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)"
```
```   220 by (unfold bin_add_def, simp)
```
```   221
```
```   222 lemma bin_add_BIT_BIT [simp]:
```
```   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)"
```
```   226 by (unfold bin_add_def, simp)
```
```   227
```
```   228 lemma integ_of_add [rule_format]:
```
```   229      "v: bin ==>
```
```   230           ALL w: 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")
```
```   234 apply (auto simp add: zadd_ac elim!: boolE)
```
```   235 done
```
```   236
```
```   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)
```
```   242 apply (simp add: integ_of_add integ_of_minus)
```
```   243 done
```
```   244
```
```   245
```
```   246 subsubsection{*@{term bin_mult}: Binary Multiplication*}
```
```   247
```
```   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)
```
```   252 apply (simp add: integ_of_minus)
```
```   253 apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib  elim!: boolE)
```
```   254 done
```
```   255
```
```   256
```
```   257 subsection{*Computations*}
```
```   258
```
```   259 (** extra rules for bin_succ, bin_pred **)
```
```   260
```
```   261 lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
```
```   262 by simp
```
```   263
```
```   264 lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
```
```   265 by simp
```
```   266
```
```   267 lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
```
```   268 by simp
```
```   269
```
```   270 lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
```
```   271 by simp
```
```   272
```
```   273 (** extra rules for bin_minus **)
```
```   274
```
```   275 lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
```
```   276 by simp
```
```   277
```
```   278 lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
```
```   279 by simp
```
```   280
```
```   281 (** extra rules for bin_add **)
```
```   282
```
```   283 lemma bin_add_BIT_11: "w: bin ==> bin_add(v BIT 1, w BIT 1) =
```
```   284                      NCons(bin_add(v, bin_succ(w)), 0)"
```
```   285 by simp
```
```   286
```
```   287 lemma bin_add_BIT_10: "w: bin ==> bin_add(v BIT 1, w BIT 0) =
```
```   288                      NCons(bin_add(v,w), 1)"
```
```   289 by simp
```
```   290
```
```   291 lemma bin_add_BIT_0: "[| w: bin;  y: bool |]
```
```   292       ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)"
```
```   293 by simp
```
```   294
```
```   295 (** extra rules for bin_mult **)
```
```   296
```
```   297 lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
```
```   298 by simp
```
```   299
```
```   300 lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
```
```   301 by simp
```
```   302
```
```   303
```
```   304 (** Simplification rules with integer constants **)
```
```   305
```
```   306 lemma int_of_0: "\$#0 = #0"
```
```   307 by simp
```
```   308
```
```   309 lemma int_of_succ: "\$# succ(n) = #1 \$+ \$#n"
```
```   310 by (simp add: int_of_add [symmetric] natify_succ)
```
```   311
```
```   312 lemma zminus_0 [simp]: "\$- #0 = #0"
```
```   313 by simp
```
```   314
```
```   315 lemma zadd_0_intify [simp]: "#0 \$+ z = intify(z)"
```
```   316 by simp
```
```   317
```
```   318 lemma zadd_0_right_intify [simp]: "z \$+ #0 = intify(z)"
```
```   319 by simp
```
```   320
```
```   321 lemma zmult_1_intify [simp]: "#1 \$* z = intify(z)"
```
```   322 by simp
```
```   323
```
```   324 lemma zmult_1_right_intify [simp]: "z \$* #1 = intify(z)"
```
```   325 by (subst zmult_commute, simp)
```
```   326
```
```   327 lemma zmult_0 [simp]: "#0 \$* z = #0"
```
```   328 by simp
```
```   329
```
```   330 lemma zmult_0_right [simp]: "z \$* #0 = #0"
```
```   331 by (subst zmult_commute, simp)
```
```   332
```
```   333 lemma zmult_minus1 [simp]: "#-1 \$* z = \$-z"
```
```   334 by (simp add: zcompare_rls)
```
```   335
```
```   336 lemma zmult_minus1_right [simp]: "z \$* #-1 = \$-z"
```
```   337 apply (subst zmult_commute)
```
```   338 apply (rule zmult_minus1)
```
```   339 done
```
```   340
```
```   341
```
```   342 subsection{*Simplification Rules for Comparison of Binary Numbers*}
```
```   343 text{*Thanks to Norbert Voelker*}
```
```   344
```
```   345 (** Equals (=) **)
```
```   346
```
```   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)
```
```   352 apply (simp add: zcompare_rls integ_of_add integ_of_minus)
```
```   353 done
```
```   354
```
```   355 lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
```
```   356 by (unfold iszero_def, simp)
```
```   357
```
```   358
```
```   359 lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
```
```   360 apply (unfold iszero_def)
```
```   361 apply (simp add: zminus_equation)
```
```   362 done
```
```   363
```
```   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) : int")
```
```   369 apply typecheck
```
```   370 apply (drule int_cases)
```
```   371 apply (safe elim!: boolE)
```
```   372 apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric]
```
```   373                      int_of_add [symmetric])
```
```   374 done
```
```   375
```
```   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)
```
```   379
```
```   380 lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
```
```   381 by (simp only: iszero_integ_of_BIT, blast)
```
```   382
```
```   383
```
```   384
```
```   385 (** Less-than (<) **)
```
```   386
```
```   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)
```
```   392 apply (simp add: integ_of_minus integ_of_add)
```
```   393 done
```
```   394
```
```   395 lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
```
```   396 by simp
```
```   397
```
```   398 lemma neg_integ_of_Min: "znegative (integ_of(Min))"
```
```   399 by simp
```
```   400
```
```   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) : int")
```
```   406 apply typecheck
```
```   407 apply (drule int_cases)
```
```   408 apply (auto elim!: boolE simp add: int_of_add [symmetric]  zcompare_rls)
```
```   409 apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def
```
```   410                      int_of_add [symmetric])
```
```   411 apply (subgoal_tac "\$#1 \$- \$# succ (succ (n #+ n)) = \$- \$# succ (n #+ n) ")
```
```   412  apply (simp add: zdiff_def)
```
```   413 apply (simp add: equation_zminus int_of_diff [symmetric])
```
```   414 done
```
```   415
```
```   416 (** Less-than-or-equals (<=) **)
```
```   417
```
```   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])
```
```   421
```
```   422
```
```   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]
```
```   429         bin_adder_BIT [simp del]
```
```   430         bin_mult_BIT [simp del]
```
```   431
```
```   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]
```
```   434
```
```   435
```
```   436 lemmas bin_arith_extra_simps =
```
```   437      integ_of_add [symmetric]
```
```   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
```
```   443      bin_add_Pls_right bin_add_Min_right
```
```   444      bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
```
```   445      diff_integ_of_eq
```
```   446      bin_mult_1 bin_mult_0 NCons_simps
```
```   447
```
```   448
```
```   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
```
```   454      bin_add_Pls bin_add_Min
```
```   455      bin_minus_Pls bin_minus_Min
```
```   456      bin_mult_Pls bin_mult_Min
```
```   457      bin_arith_extra_simps
```
```   458
```
```   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
```
```   466
```
```   467 declare bin_arith_simps [simp]
```
```   468 declare bin_rel_simps [simp]
```
```   469
```
```   470
```
```   471 (** Simplification of arithmetic when nested to the right **)
```
```   472
```
```   473 lemma add_integ_of_left [simp]:
```
```   474      "[| v: bin;  w: bin |]
```
```   475       ==> integ_of(v) \$+ (integ_of(w) \$+ z) = (integ_of(bin_add(v,w)) \$+ z)"
```
```   476 by (simp add: zadd_assoc [symmetric])
```
```   477
```
```   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])
```
```   482
```
```   483 lemma add_integ_of_diff1 [simp]:
```
```   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)
```
```   487 apply (rule add_integ_of_left, auto)
```
```   488 done
```
```   489
```
```   490 lemma add_integ_of_diff2 [simp]:
```
```   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])
```
```   495 apply (simp_all add: zdiff_def zadd_ac)
```
```   496 done
```
```   497
```
```   498
```
```   499 (** More for integer constants **)
```
```   500
```
```   501 declare int_of_0 [simp] int_of_succ [simp]
```
```   502
```
```   503 lemma zdiff0 [simp]: "#0 \$- x = \$-x"
```
```   504 by (simp add: zdiff_def)
```
```   505
```
```   506 lemma zdiff0_right [simp]: "x \$- #0 = intify(x)"
```
```   507 by (simp add: zdiff_def)
```
```   508
```
```   509 lemma zdiff_self [simp]: "x \$- x = #0"
```
```   510 by (simp add: zdiff_def)
```
```   511
```
```   512 lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k \$< #0"
```
```   513 by (simp add: zless_def)
```
```   514
```
```   515 lemma zero_zless_imp_znegative_zminus: "[|#0 \$< k; k: int|] ==> znegative(\$-k)"
```
```   516 by (simp add: zless_def)
```
```   517
```
```   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])
```
```   520
```
```   521 lemma nat_of_0 [simp]: "nat_of(#0) = 0"
```
```   522 by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
```
```   523
```
```   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)
```
```   526
```
```   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
```
```   531
```
```   532 lemma int_of_eq_0_imp_natify_eq_0: "\$# n = #0 ==> natify(n) = 0"
```
```   533 by (rule not_znegative_imp_zero, auto)
```
```   534
```
```   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)
```
```   537
```
```   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
```
```   542
```
```   543 declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
```
```   544
```
```   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)
```
```   547
```
```   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]
```
```   552             simp add: znegative_iff_zless_0)
```
```   553 done
```
```   554
```
```   555
```
```   556 (** nat_of and zless **)
```
```   557
```
```   558 (*An alternative condition is  \$#0 <= 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
```
```   566
```
```   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
```
```   571
```
```   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 *)
```
```   581
```
```   582 lemma integ_of_minus_reorient [simp]:
```
```   583      "(integ_of(w) = \$- x) <-> (\$- x = integ_of(w))"
```
```   584 by auto
```
```   585
```
```   586 lemma integ_of_add_reorient [simp]:
```
```   587      "(integ_of(w) = x \$+ y) <-> (x \$+ y = integ_of(w))"
```
```   588 by auto
```
```   589
```
```   590 lemma integ_of_diff_reorient [simp]:
```
```   591      "(integ_of(w) = x \$- y) <-> (x \$- y = integ_of(w))"
```
```   592 by auto
```
```   593
```
```   594 lemma integ_of_mult_reorient [simp]:
```
```   595      "(integ_of(w) = x \$* y) <-> (x \$* y = integ_of(w))"
```
```   596 by auto
```
```   597
```
```   598 end
```