src/ZF/Bin.thy
 author wenzelm Thu Dec 14 11:24:26 2017 +0100 (20 months ago) changeset 67198 694f29a5433b parent 61798 27f3c10b0b50 child 68233 5e0e9376b2b0 permissions -rw-r--r--
merged
```     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 section\<open>Arithmetic on Binary Integers\<close>
```
```    17
```
```    18 theory Bin
```
```    19 imports Int_ZF Datatype_ZF
```
```    20 begin
```
```    21
```
```    22 consts  bin :: i
```
```    23 datatype
```
```    24   "bin" = Pls
```
```    25         | Min
```
```    26         | Bit ("w \<in> bin", "b \<in> bool")     (infixl "BIT" 90)
```
```    27
```
```    28 consts
```
```    29   integ_of  :: "i=>i"
```
```    30   NCons     :: "[i,i]=>i"
```
```    31   bin_succ  :: "i=>i"
```
```    32   bin_pred  :: "i=>i"
```
```    33   bin_minus :: "i=>i"
```
```    34   bin_adder :: "i=>i"
```
```    35   bin_mult  :: "[i,i]=>i"
```
```    36
```
```    37 primrec
```
```    38   integ_of_Pls:  "integ_of (Pls)     = \$# 0"
```
```    39   integ_of_Min:  "integ_of (Min)     = \$-(\$#1)"
```
```    40   integ_of_BIT:  "integ_of (w BIT b) = \$#b \$+ integ_of(w) \$+ integ_of(w)"
```
```    41
```
```    42     (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
```
```    43
```
```    44 primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
```
```    45   NCons_Pls: "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
```
```    46   NCons_Min: "NCons (Min,b)     = cond(b,Min,Min BIT b)"
```
```    47   NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b"
```
```    48
```
```    49 primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
```
```    50   bin_succ_Pls:  "bin_succ (Pls)     = Pls BIT 1"
```
```    51   bin_succ_Min:  "bin_succ (Min)     = Pls"
```
```    52   bin_succ_BIT:  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
```
```    53
```
```    54 primrec (*predecessor*)
```
```    55   bin_pred_Pls:  "bin_pred (Pls)     = Min"
```
```    56   bin_pred_Min:  "bin_pred (Min)     = Min BIT 0"
```
```    57   bin_pred_BIT:  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
```
```    58
```
```    59 primrec (*unary negation*)
```
```    60   bin_minus_Pls:
```
```    61     "bin_minus (Pls)       = Pls"
```
```    62   bin_minus_Min:
```
```    63     "bin_minus (Min)       = Pls BIT 1"
```
```    64   bin_minus_BIT:
```
```    65     "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
```
```    66                                 bin_minus(w) BIT 0)"
```
```    67
```
```    68 primrec (*sum*)
```
```    69   bin_adder_Pls:
```
```    70     "bin_adder (Pls)     = (\<lambda>w\<in>bin. w)"
```
```    71   bin_adder_Min:
```
```    72     "bin_adder (Min)     = (\<lambda>w\<in>bin. bin_pred(w))"
```
```    73   bin_adder_BIT:
```
```    74     "bin_adder (v BIT x) =
```
```    75        (\<lambda>w\<in>bin.
```
```    76          bin_case (v BIT x, bin_pred(v BIT x),
```
```    77                    %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w),
```
```    78                                x xor y),
```
```    79                    w))"
```
```    80
```
```    81 (*The bin_case above replaces the following mutually recursive function:
```
```    82 primrec
```
```    83   "adding (v,x,Pls)     = v BIT x"
```
```    84   "adding (v,x,Min)     = bin_pred(v BIT x)"
```
```    85   "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)),
```
```    86                                 x xor y)"
```
```    87 *)
```
```    88
```
```    89 definition
```
```    90   bin_add   :: "[i,i]=>i"  where
```
```    91     "bin_add(v,w) == bin_adder(v)`w"
```
```    92
```
```    93
```
```    94 primrec
```
```    95   bin_mult_Pls:
```
```    96     "bin_mult (Pls,w)     = Pls"
```
```    97   bin_mult_Min:
```
```    98     "bin_mult (Min,w)     = bin_minus(w)"
```
```    99   bin_mult_BIT:
```
```   100     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
```
```   101                                  NCons(bin_mult(v,w),0))"
```
```   102
```
```   103 syntax
```
```   104   "_Int0" :: i  ("#()0")
```
```   105   "_Int1" :: i  ("#()1")
```
```   106   "_Int2" :: i  ("#()2")
```
```   107   "_Neg_Int1" :: i  ("#-()1")
```
```   108   "_Neg_Int2" :: i  ("#-()2")
```
```   109 translations
```
```   110   "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
```
```   111   "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
```
```   112   "#2" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1 BIT 0)"
```
```   113   "#-1" \<rightleftharpoons> "CONST integ_of(CONST Min)"
```
```   114   "#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
```
```   115
```
```   116 syntax
```
```   117   "_Int" :: "num_token => i"  ("#_" 1000)
```
```   118   "_Neg_Int" :: "num_token => i"  ("#-_" 1000)
```
```   119
```
```   120 ML_file "Tools/numeral_syntax.ML"
```
```   121
```
```   122
```
```   123 declare bin.intros [simp,TC]
```
```   124
```
```   125 lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
```
```   126 by simp
```
```   127
```
```   128 lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
```
```   129 by simp
```
```   130
```
```   131 lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
```
```   132 by simp
```
```   133
```
```   134 lemma NCons_Min_1: "NCons(Min,1) = Min"
```
```   135 by simp
```
```   136
```
```   137 lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
```
```   138 by (simp add: bin.case_eqns)
```
```   139
```
```   140 lemmas NCons_simps [simp] =
```
```   141     NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
```
```   142
```
```   143
```
```   144
```
```   145 (** Type checking **)
```
```   146
```
```   147 lemma integ_of_type [TC]: "w \<in> bin ==> integ_of(w) \<in> int"
```
```   148 apply (induct_tac "w")
```
```   149 apply (simp_all add: bool_into_nat)
```
```   150 done
```
```   151
```
```   152 lemma NCons_type [TC]: "[| w \<in> bin; b \<in> bool |] ==> NCons(w,b) \<in> bin"
```
```   153 by (induct_tac "w", auto)
```
```   154
```
```   155 lemma bin_succ_type [TC]: "w \<in> bin ==> bin_succ(w) \<in> bin"
```
```   156 by (induct_tac "w", auto)
```
```   157
```
```   158 lemma bin_pred_type [TC]: "w \<in> bin ==> bin_pred(w) \<in> bin"
```
```   159 by (induct_tac "w", auto)
```
```   160
```
```   161 lemma bin_minus_type [TC]: "w \<in> bin ==> bin_minus(w) \<in> bin"
```
```   162 by (induct_tac "w", auto)
```
```   163
```
```   164 (*This proof is complicated by the mutual recursion*)
```
```   165 lemma bin_add_type [rule_format,TC]:
```
```   166      "v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
```
```   167 apply (unfold bin_add_def)
```
```   168 apply (induct_tac "v")
```
```   169 apply (rule_tac [3] ballI)
```
```   170 apply (rename_tac [3] "w'")
```
```   171 apply (induct_tac [3] "w'")
```
```   172 apply (simp_all add: NCons_type)
```
```   173 done
```
```   174
```
```   175 lemma bin_mult_type [TC]: "[| v \<in> bin; w \<in> bin |] ==> bin_mult(v,w) \<in> bin"
```
```   176 by (induct_tac "v", auto)
```
```   177
```
```   178
```
```   179 subsubsection\<open>The Carry and Borrow Functions,
```
```   180             @{term bin_succ} and @{term bin_pred}\<close>
```
```   181
```
```   182 (*NCons preserves the integer value of its argument*)
```
```   183 lemma integ_of_NCons [simp]:
```
```   184      "[| w \<in> bin; b \<in> bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"
```
```   185 apply (erule bin.cases)
```
```   186 apply (auto elim!: boolE)
```
```   187 done
```
```   188
```
```   189 lemma integ_of_succ [simp]:
```
```   190      "w \<in> bin ==> integ_of(bin_succ(w)) = \$#1 \$+ integ_of(w)"
```
```   191 apply (erule bin.induct)
```
```   192 apply (auto simp add: zadd_ac elim!: boolE)
```
```   193 done
```
```   194
```
```   195 lemma integ_of_pred [simp]:
```
```   196      "w \<in> bin ==> integ_of(bin_pred(w)) = \$- (\$#1) \$+ integ_of(w)"
```
```   197 apply (erule bin.induct)
```
```   198 apply (auto simp add: zadd_ac elim!: boolE)
```
```   199 done
```
```   200
```
```   201
```
```   202 subsubsection\<open>@{term bin_minus}: Unary Negation of Binary Integers\<close>
```
```   203
```
```   204 lemma integ_of_minus: "w \<in> bin ==> integ_of(bin_minus(w)) = \$- integ_of(w)"
```
```   205 apply (erule bin.induct)
```
```   206 apply (auto simp add: zadd_ac zminus_zadd_distrib  elim!: boolE)
```
```   207 done
```
```   208
```
```   209
```
```   210 subsubsection\<open>@{term bin_add}: Binary Addition\<close>
```
```   211
```
```   212 lemma bin_add_Pls [simp]: "w \<in> bin ==> bin_add(Pls,w) = w"
```
```   213 by (unfold bin_add_def, simp)
```
```   214
```
```   215 lemma bin_add_Pls_right: "w \<in> bin ==> bin_add(w,Pls) = w"
```
```   216 apply (unfold bin_add_def)
```
```   217 apply (erule bin.induct, auto)
```
```   218 done
```
```   219
```
```   220 lemma bin_add_Min [simp]: "w \<in> bin ==> bin_add(Min,w) = bin_pred(w)"
```
```   221 by (unfold bin_add_def, simp)
```
```   222
```
```   223 lemma bin_add_Min_right: "w \<in> bin ==> bin_add(w,Min) = bin_pred(w)"
```
```   224 apply (unfold bin_add_def)
```
```   225 apply (erule bin.induct, auto)
```
```   226 done
```
```   227
```
```   228 lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x"
```
```   229 by (unfold bin_add_def, simp)
```
```   230
```
```   231 lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)"
```
```   232 by (unfold bin_add_def, simp)
```
```   233
```
```   234 lemma bin_add_BIT_BIT [simp]:
```
```   235      "[| w \<in> bin;  y \<in> bool |]
```
```   236       ==> bin_add(v BIT x, w BIT y) =
```
```   237           NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"
```
```   238 by (unfold bin_add_def, simp)
```
```   239
```
```   240 lemma integ_of_add [rule_format]:
```
```   241      "v \<in> bin ==>
```
```   242           \<forall>w\<in>bin. integ_of(bin_add(v,w)) = integ_of(v) \$+ integ_of(w)"
```
```   243 apply (erule bin.induct, simp, simp)
```
```   244 apply (rule ballI)
```
```   245 apply (induct_tac "wa")
```
```   246 apply (auto simp add: zadd_ac elim!: boolE)
```
```   247 done
```
```   248
```
```   249 (*Subtraction*)
```
```   250 lemma diff_integ_of_eq:
```
```   251      "[| v \<in> bin;  w \<in> bin |]
```
```   252       ==> integ_of(v) \$- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
```
```   253 apply (unfold zdiff_def)
```
```   254 apply (simp add: integ_of_add integ_of_minus)
```
```   255 done
```
```   256
```
```   257
```
```   258 subsubsection\<open>@{term bin_mult}: Binary Multiplication\<close>
```
```   259
```
```   260 lemma integ_of_mult:
```
```   261      "[| v \<in> bin;  w \<in> bin |]
```
```   262       ==> integ_of(bin_mult(v,w)) = integ_of(v) \$* integ_of(w)"
```
```   263 apply (induct_tac "v", simp)
```
```   264 apply (simp add: integ_of_minus)
```
```   265 apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib  elim!: boolE)
```
```   266 done
```
```   267
```
```   268
```
```   269 subsection\<open>Computations\<close>
```
```   270
```
```   271 (** extra rules for bin_succ, bin_pred **)
```
```   272
```
```   273 lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
```
```   274 by simp
```
```   275
```
```   276 lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
```
```   277 by simp
```
```   278
```
```   279 lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
```
```   280 by simp
```
```   281
```
```   282 lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
```
```   283 by simp
```
```   284
```
```   285 (** extra rules for bin_minus **)
```
```   286
```
```   287 lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
```
```   288 by simp
```
```   289
```
```   290 lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
```
```   291 by simp
```
```   292
```
```   293 (** extra rules for bin_add **)
```
```   294
```
```   295 lemma bin_add_BIT_11: "w \<in> bin ==> bin_add(v BIT 1, w BIT 1) =
```
```   296                      NCons(bin_add(v, bin_succ(w)), 0)"
```
```   297 by simp
```
```   298
```
```   299 lemma bin_add_BIT_10: "w \<in> bin ==> bin_add(v BIT 1, w BIT 0) =
```
```   300                      NCons(bin_add(v,w), 1)"
```
```   301 by simp
```
```   302
```
```   303 lemma bin_add_BIT_0: "[| w \<in> bin;  y \<in> bool |]
```
```   304       ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)"
```
```   305 by simp
```
```   306
```
```   307 (** extra rules for bin_mult **)
```
```   308
```
```   309 lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
```
```   310 by simp
```
```   311
```
```   312 lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
```
```   313 by simp
```
```   314
```
```   315
```
```   316 (** Simplification rules with integer constants **)
```
```   317
```
```   318 lemma int_of_0: "\$#0 = #0"
```
```   319 by simp
```
```   320
```
```   321 lemma int_of_succ: "\$# succ(n) = #1 \$+ \$#n"
```
```   322 by (simp add: int_of_add [symmetric] natify_succ)
```
```   323
```
```   324 lemma zminus_0 [simp]: "\$- #0 = #0"
```
```   325 by simp
```
```   326
```
```   327 lemma zadd_0_intify [simp]: "#0 \$+ z = intify(z)"
```
```   328 by simp
```
```   329
```
```   330 lemma zadd_0_right_intify [simp]: "z \$+ #0 = intify(z)"
```
```   331 by simp
```
```   332
```
```   333 lemma zmult_1_intify [simp]: "#1 \$* z = intify(z)"
```
```   334 by simp
```
```   335
```
```   336 lemma zmult_1_right_intify [simp]: "z \$* #1 = intify(z)"
```
```   337 by (subst zmult_commute, simp)
```
```   338
```
```   339 lemma zmult_0 [simp]: "#0 \$* z = #0"
```
```   340 by simp
```
```   341
```
```   342 lemma zmult_0_right [simp]: "z \$* #0 = #0"
```
```   343 by (subst zmult_commute, simp)
```
```   344
```
```   345 lemma zmult_minus1 [simp]: "#-1 \$* z = \$-z"
```
```   346 by (simp add: zcompare_rls)
```
```   347
```
```   348 lemma zmult_minus1_right [simp]: "z \$* #-1 = \$-z"
```
```   349 apply (subst zmult_commute)
```
```   350 apply (rule zmult_minus1)
```
```   351 done
```
```   352
```
```   353
```
```   354 subsection\<open>Simplification Rules for Comparison of Binary Numbers\<close>
```
```   355 text\<open>Thanks to Norbert Voelker\<close>
```
```   356
```
```   357 (** Equals (=) **)
```
```   358
```
```   359 lemma eq_integ_of_eq:
```
```   360      "[| v \<in> bin;  w \<in> bin |]
```
```   361       ==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
```
```   362           iszero (integ_of (bin_add (v, bin_minus(w))))"
```
```   363 apply (unfold iszero_def)
```
```   364 apply (simp add: zcompare_rls integ_of_add integ_of_minus)
```
```   365 done
```
```   366
```
```   367 lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
```
```   368 by (unfold iszero_def, simp)
```
```   369
```
```   370
```
```   371 lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
```
```   372 apply (unfold iszero_def)
```
```   373 apply (simp add: zminus_equation)
```
```   374 done
```
```   375
```
```   376 lemma iszero_integ_of_BIT:
```
```   377      "[| w \<in> bin; x \<in> bool |]
```
```   378       ==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))"
```
```   379 apply (unfold iszero_def, simp)
```
```   380 apply (subgoal_tac "integ_of (w) \<in> int")
```
```   381 apply typecheck
```
```   382 apply (drule int_cases)
```
```   383 apply (safe elim!: boolE)
```
```   384 apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric]
```
```   385                      int_of_add [symmetric])
```
```   386 done
```
```   387
```
```   388 lemma iszero_integ_of_0:
```
```   389      "w \<in> bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))"
```
```   390 by (simp only: iszero_integ_of_BIT, blast)
```
```   391
```
```   392 lemma iszero_integ_of_1: "w \<in> bin ==> ~ iszero (integ_of (w BIT 1))"
```
```   393 by (simp only: iszero_integ_of_BIT, blast)
```
```   394
```
```   395
```
```   396
```
```   397 (** Less-than (<) **)
```
```   398
```
```   399 lemma less_integ_of_eq_neg:
```
```   400      "[| v \<in> bin;  w \<in> bin |]
```
```   401       ==> integ_of(v) \$< integ_of(w)
```
```   402           \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
```
```   403 apply (unfold zless_def zdiff_def)
```
```   404 apply (simp add: integ_of_minus integ_of_add)
```
```   405 done
```
```   406
```
```   407 lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
```
```   408 by simp
```
```   409
```
```   410 lemma neg_integ_of_Min: "znegative (integ_of(Min))"
```
```   411 by simp
```
```   412
```
```   413 lemma neg_integ_of_BIT:
```
```   414      "[| w \<in> bin; x \<in> bool |]
```
```   415       ==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))"
```
```   416 apply simp
```
```   417 apply (subgoal_tac "integ_of (w) \<in> int")
```
```   418 apply typecheck
```
```   419 apply (drule int_cases)
```
```   420 apply (auto elim!: boolE simp add: int_of_add [symmetric]  zcompare_rls)
```
```   421 apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def
```
```   422                      int_of_add [symmetric])
```
```   423 apply (subgoal_tac "\$#1 \$- \$# succ (succ (n #+ n)) = \$- \$# succ (n #+ n) ")
```
```   424  apply (simp add: zdiff_def)
```
```   425 apply (simp add: equation_zminus int_of_diff [symmetric])
```
```   426 done
```
```   427
```
```   428 (** Less-than-or-equals (<=) **)
```
```   429
```
```   430 lemma le_integ_of_eq_not_less:
```
```   431      "(integ_of(x) \$\<le> (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) \$< (integ_of(x)))"
```
```   432 by (simp add: not_zless_iff_zle [THEN iff_sym])
```
```   433
```
```   434
```
```   435 (*Delete the original rewrites, with their clumsy conditional expressions*)
```
```   436 declare bin_succ_BIT [simp del]
```
```   437         bin_pred_BIT [simp del]
```
```   438         bin_minus_BIT [simp del]
```
```   439         NCons_Pls [simp del]
```
```   440         NCons_Min [simp del]
```
```   441         bin_adder_BIT [simp del]
```
```   442         bin_mult_BIT [simp del]
```
```   443
```
```   444 (*Hide the binary representation of integer constants*)
```
```   445 declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del]
```
```   446
```
```   447
```
```   448 lemmas bin_arith_extra_simps =
```
```   449      integ_of_add [symmetric]
```
```   450      integ_of_minus [symmetric]
```
```   451      integ_of_mult [symmetric]
```
```   452      bin_succ_1 bin_succ_0
```
```   453      bin_pred_1 bin_pred_0
```
```   454      bin_minus_1 bin_minus_0
```
```   455      bin_add_Pls_right bin_add_Min_right
```
```   456      bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
```
```   457      diff_integ_of_eq
```
```   458      bin_mult_1 bin_mult_0 NCons_simps
```
```   459
```
```   460
```
```   461 (*For making a minimal simpset, one must include these default simprules
```
```   462   of thy.  Also include simp_thms, or at least (~False)=True*)
```
```   463 lemmas bin_arith_simps =
```
```   464      bin_pred_Pls bin_pred_Min
```
```   465      bin_succ_Pls bin_succ_Min
```
```   466      bin_add_Pls bin_add_Min
```
```   467      bin_minus_Pls bin_minus_Min
```
```   468      bin_mult_Pls bin_mult_Min
```
```   469      bin_arith_extra_simps
```
```   470
```
```   471 (*Simplification of relational operations*)
```
```   472 lemmas bin_rel_simps =
```
```   473      eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min
```
```   474      iszero_integ_of_0 iszero_integ_of_1
```
```   475      less_integ_of_eq_neg
```
```   476      not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT
```
```   477      le_integ_of_eq_not_less
```
```   478
```
```   479 declare bin_arith_simps [simp]
```
```   480 declare bin_rel_simps [simp]
```
```   481
```
```   482
```
```   483 (** Simplification of arithmetic when nested to the right **)
```
```   484
```
```   485 lemma add_integ_of_left [simp]:
```
```   486      "[| v \<in> bin;  w \<in> bin |]
```
```   487       ==> integ_of(v) \$+ (integ_of(w) \$+ z) = (integ_of(bin_add(v,w)) \$+ z)"
```
```   488 by (simp add: zadd_assoc [symmetric])
```
```   489
```
```   490 lemma mult_integ_of_left [simp]:
```
```   491      "[| v \<in> bin;  w \<in> bin |]
```
```   492       ==> integ_of(v) \$* (integ_of(w) \$* z) = (integ_of(bin_mult(v,w)) \$* z)"
```
```   493 by (simp add: zmult_assoc [symmetric])
```
```   494
```
```   495 lemma add_integ_of_diff1 [simp]:
```
```   496     "[| v \<in> bin;  w \<in> bin |]
```
```   497       ==> integ_of(v) \$+ (integ_of(w) \$- c) = integ_of(bin_add(v,w)) \$- (c)"
```
```   498 apply (unfold zdiff_def)
```
```   499 apply (rule add_integ_of_left, auto)
```
```   500 done
```
```   501
```
```   502 lemma add_integ_of_diff2 [simp]:
```
```   503      "[| v \<in> bin;  w \<in> bin |]
```
```   504       ==> integ_of(v) \$+ (c \$- integ_of(w)) =
```
```   505           integ_of (bin_add (v, bin_minus(w))) \$+ (c)"
```
```   506 apply (subst diff_integ_of_eq [symmetric])
```
```   507 apply (simp_all add: zdiff_def zadd_ac)
```
```   508 done
```
```   509
```
```   510
```
```   511 (** More for integer constants **)
```
```   512
```
```   513 declare int_of_0 [simp] int_of_succ [simp]
```
```   514
```
```   515 lemma zdiff0 [simp]: "#0 \$- x = \$-x"
```
```   516 by (simp add: zdiff_def)
```
```   517
```
```   518 lemma zdiff0_right [simp]: "x \$- #0 = intify(x)"
```
```   519 by (simp add: zdiff_def)
```
```   520
```
```   521 lemma zdiff_self [simp]: "x \$- x = #0"
```
```   522 by (simp add: zdiff_def)
```
```   523
```
```   524 lemma znegative_iff_zless_0: "k \<in> int ==> znegative(k) \<longleftrightarrow> k \$< #0"
```
```   525 by (simp add: zless_def)
```
```   526
```
```   527 lemma zero_zless_imp_znegative_zminus: "[|#0 \$< k; k \<in> int|] ==> znegative(\$-k)"
```
```   528 by (simp add: zless_def)
```
```   529
```
```   530 lemma zero_zle_int_of [simp]: "#0 \$\<le> \$# n"
```
```   531 by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
```
```   532
```
```   533 lemma nat_of_0 [simp]: "nat_of(#0) = 0"
```
```   534 by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
```
```   535
```
```   536 lemma nat_le_int0_lemma: "[| z \$\<le> \$#0; z \<in> int |] ==> nat_of(z) = 0"
```
```   537 by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of)
```
```   538
```
```   539 lemma nat_le_int0: "z \$\<le> \$#0 ==> nat_of(z) = 0"
```
```   540 apply (subgoal_tac "nat_of (intify (z)) = 0")
```
```   541 apply (rule_tac [2] nat_le_int0_lemma, auto)
```
```   542 done
```
```   543
```
```   544 lemma int_of_eq_0_imp_natify_eq_0: "\$# n = #0 ==> natify(n) = 0"
```
```   545 by (rule not_znegative_imp_zero, auto)
```
```   546
```
```   547 lemma nat_of_zminus_int_of: "nat_of(\$- \$# n) = 0"
```
```   548 by (simp add: nat_of_def int_of_def raw_nat_of zminus image_intrel_int)
```
```   549
```
```   550 lemma int_of_nat_of: "#0 \$\<le> z ==> \$# nat_of(z) = intify(z)"
```
```   551 apply (rule not_zneg_nat_of_intify)
```
```   552 apply (simp add: znegative_iff_zless_0 not_zless_iff_zle)
```
```   553 done
```
```   554
```
```   555 declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
```
```   556
```
```   557 lemma int_of_nat_of_if: "\$# nat_of(z) = (if #0 \$\<le> z then intify(z) else #0)"
```
```   558 by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
```
```   559
```
```   560 lemma zless_nat_iff_int_zless: "[| m \<in> nat; z \<in> int |] ==> (m < nat_of(z)) \<longleftrightarrow> (\$#m \$< z)"
```
```   561 apply (case_tac "znegative (z) ")
```
```   562 apply (erule_tac [2] not_zneg_nat_of [THEN subst])
```
```   563 apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
```
```   564             simp add: znegative_iff_zless_0)
```
```   565 done
```
```   566
```
```   567
```
```   568 (** nat_of and zless **)
```
```   569
```
```   570 (*An alternative condition is  @{term"\$#0 \<subseteq> w"}  *)
```
```   571 lemma zless_nat_conj_lemma: "\$#0 \$< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w \$< z)"
```
```   572 apply (rule iff_trans)
```
```   573 apply (rule zless_int_of [THEN iff_sym])
```
```   574 apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
```
```   575 apply (auto elim: zless_asym simp add: not_zle_iff_zless)
```
```   576 apply (blast intro: zless_zle_trans)
```
```   577 done
```
```   578
```
```   579 lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> (\$#0 \$< z & w \$< z)"
```
```   580 apply (case_tac "\$#0 \$< z")
```
```   581 apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
```
```   582 done
```
```   583
```
```   584 (*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
```
```   585   unconditional!
```
```   586   [The condition "True" is a hack to prevent looping.
```
```   587     Conditional rewrite rules are tried after unconditional ones, so a rule
```
```   588     like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
```
```   589   lemma integ_of_reorient [simp]:
```
```   590        "True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))"
```
```   591   by auto
```
```   592 *)
```
```   593
```
```   594 lemma integ_of_minus_reorient [simp]:
```
```   595      "(integ_of(w) = \$- x) \<longleftrightarrow> (\$- x = integ_of(w))"
```
```   596 by auto
```
```   597
```
```   598 lemma integ_of_add_reorient [simp]:
```
```   599      "(integ_of(w) = x \$+ y) \<longleftrightarrow> (x \$+ y = integ_of(w))"
```
```   600 by auto
```
```   601
```
```   602 lemma integ_of_diff_reorient [simp]:
```
```   603      "(integ_of(w) = x \$- y) \<longleftrightarrow> (x \$- y = integ_of(w))"
```
```   604 by auto
```
```   605
```
```   606 lemma integ_of_mult_reorient [simp]:
```
```   607      "(integ_of(w) = x \$* y) \<longleftrightarrow> (x \$* y = integ_of(w))"
```
```   608 by auto
```
```   609
```
```   610 (** To simplify inequalities involving integer negation and literals,
```
```   611     such as -x = #3
```
```   612 **)
```
```   613
```
```   614 lemmas [simp] =
```
```   615   zminus_equation [where y = "integ_of(w)"]
```
```   616   equation_zminus [where x = "integ_of(w)"]
```
```   617   for w
```
```   618
```
```   619 lemmas [iff] =
```
```   620   zminus_zless [where y = "integ_of(w)"]
```
```   621   zless_zminus [where x = "integ_of(w)"]
```
```   622   for w
```
```   623
```
```   624 lemmas [iff] =
```
```   625   zminus_zle [where y = "integ_of(w)"]
```
```   626   zle_zminus [where x = "integ_of(w)"]
```
```   627   for w
```
```   628
```
```   629 lemmas [simp] =
```
```   630   Let_def [where s = "integ_of(w)"] for w
```
```   631
```
```   632
```
```   633 (*** Simprocs for numeric literals ***)
```
```   634
```
```   635 (** Combining of literal coefficients in sums of products **)
```
```   636
```
```   637 lemma zless_iff_zdiff_zless_0: "(x \$< y) \<longleftrightarrow> (x\$-y \$< #0)"
```
```   638   by (simp add: zcompare_rls)
```
```   639
```
```   640 lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x\$-y = #0)"
```
```   641   by (simp add: zcompare_rls)
```
```   642
```
```   643 lemma zle_iff_zdiff_zle_0: "(x \$\<le> y) \<longleftrightarrow> (x\$-y \$\<le> #0)"
```
```   644   by (simp add: zcompare_rls)
```
```   645
```
```   646
```
```   647 (** For combine_numerals **)
```
```   648
```
```   649 lemma left_zadd_zmult_distrib: "i\$*u \$+ (j\$*u \$+ k) = (i\$+j)\$*u \$+ k"
```
```   650   by (simp add: zadd_zmult_distrib zadd_ac)
```
```   651
```
```   652
```
```   653 (** For cancel_numerals **)
```
```   654
```
```   655 lemmas rel_iff_rel_0_rls =
```
```   656   zless_iff_zdiff_zless_0 [where y = "u \$+ v"]
```
```   657   eq_iff_zdiff_eq_0 [where y = "u \$+ v"]
```
```   658   zle_iff_zdiff_zle_0 [where y = "u \$+ v"]
```
```   659   zless_iff_zdiff_zless_0 [where y = n]
```
```   660   eq_iff_zdiff_eq_0 [where y = n]
```
```   661   zle_iff_zdiff_zle_0 [where y = n]
```
```   662   for u v (* FIXME n (!?) *)
```
```   663
```
```   664 lemma eq_add_iff1: "(i\$*u \$+ m = j\$*u \$+ n) \<longleftrightarrow> ((i\$-j)\$*u \$+ m = intify(n))"
```
```   665   apply (simp add: zdiff_def zadd_zmult_distrib)
```
```   666   apply (simp add: zcompare_rls)
```
```   667   apply (simp add: zadd_ac)
```
```   668   done
```
```   669
```
```   670 lemma eq_add_iff2: "(i\$*u \$+ m = j\$*u \$+ n) \<longleftrightarrow> (intify(m) = (j\$-i)\$*u \$+ n)"
```
```   671   apply (simp add: zdiff_def zadd_zmult_distrib)
```
```   672   apply (simp add: zcompare_rls)
```
```   673   apply (simp add: zadd_ac)
```
```   674   done
```
```   675
```
```   676 lemma less_add_iff1: "(i\$*u \$+ m \$< j\$*u \$+ n) \<longleftrightarrow> ((i\$-j)\$*u \$+ m \$< n)"
```
```   677   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
```
```   678   done
```
```   679
```
```   680 lemma less_add_iff2: "(i\$*u \$+ m \$< j\$*u \$+ n) \<longleftrightarrow> (m \$< (j\$-i)\$*u \$+ n)"
```
```   681   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
```
```   682   done
```
```   683
```
```   684 lemma le_add_iff1: "(i\$*u \$+ m \$\<le> j\$*u \$+ n) \<longleftrightarrow> ((i\$-j)\$*u \$+ m \$\<le> n)"
```
```   685   apply (simp add: zdiff_def zadd_zmult_distrib)
```
```   686   apply (simp add: zcompare_rls)
```
```   687   apply (simp add: zadd_ac)
```
```   688   done
```
```   689
```
```   690 lemma le_add_iff2: "(i\$*u \$+ m \$\<le> j\$*u \$+ n) \<longleftrightarrow> (m \$\<le> (j\$-i)\$*u \$+ n)"
```
```   691   apply (simp add: zdiff_def zadd_zmult_distrib)
```
```   692   apply (simp add: zcompare_rls)
```
```   693   apply (simp add: zadd_ac)
```
```   694   done
```
```   695
```
```   696 ML_file "int_arith.ML"
```
```   697
```
```   698 subsection \<open>examples:\<close>
```
```   699
```
```   700 text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close>
```
```   701 lemma "#5 \$* x \$* #3 = y" apply simp oops
```
```   702
```
```   703 schematic_goal "y2 \$+ ?x42 = y \$+ y2" apply simp oops
```
```   704
```
```   705 lemma "oo : int ==> l \$+ (l \$+ #2) \$+ oo = oo" apply simp oops
```
```   706
```
```   707 lemma "#9\$*x \$+ y = x\$*#23 \$+ z" apply simp oops
```
```   708 lemma "y \$+ x = x \$+ z" apply simp oops
```
```   709
```
```   710 lemma "x : int ==> x \$+ y \$+ z = x \$+ z" apply simp oops
```
```   711 lemma "x : int ==> y \$+ (z \$+ x) = z \$+ x" apply simp oops
```
```   712 lemma "z : int ==> x \$+ y \$+ z = (z \$+ y) \$+ (x \$+ w)" apply simp oops
```
```   713 lemma "z : int ==> x\$*y \$+ z = (z \$+ y) \$+ (y\$*x \$+ w)" apply simp oops
```
```   714
```
```   715 lemma "#-3 \$* x \$+ y \$\<le> x \$* #2 \$+ z" apply simp oops
```
```   716 lemma "y \$+ x \$\<le> x \$+ z" apply simp oops
```
```   717 lemma "x \$+ y \$+ z \$\<le> x \$+ z" apply simp oops
```
```   718
```
```   719 lemma "y \$+ (z \$+ x) \$< z \$+ x" apply simp oops
```
```   720 lemma "x \$+ y \$+ z \$< (z \$+ y) \$+ (x \$+ w)" apply simp oops
```
```   721 lemma "x\$*y \$+ z \$< (z \$+ y) \$+ (y\$*x \$+ w)" apply simp oops
```
```   722
```
```   723 lemma "l \$+ #2 \$+ #2 \$+ #2 \$+ (l \$+ #2) \$+ (oo \$+ #2) = uu" apply simp oops
```
```   724 lemma "u : int ==> #2 \$* u = u" apply simp oops
```
```   725 lemma "(i \$+ j \$+ #12 \$+ k) \$- #15 = y" apply simp oops
```
```   726 lemma "(i \$+ j \$+ #12 \$+ k) \$- #5 = y" apply simp oops
```
```   727
```
```   728 lemma "y \$- b \$< b" apply simp oops
```
```   729 lemma "y \$- (#3 \$* b \$+ c) \$< b \$- #2 \$* c" apply simp oops
```
```   730
```
```   731 lemma "(#2 \$* x \$- (u \$* v) \$+ y) \$- v \$* #3 \$* u = w" apply simp oops
```
```   732 lemma "(#2 \$* x \$* u \$* v \$+ (u \$* v) \$* #4 \$+ y) \$- v \$* u \$* #4 = w" apply simp oops
```
```   733 lemma "(#2 \$* x \$* u \$* v \$+ (u \$* v) \$* #4 \$+ y) \$- v \$* u = w" apply simp oops
```
```   734 lemma "u \$* v \$- (x \$* u \$* v \$+ (u \$* v) \$* #4 \$+ y) = w" apply simp oops
```
```   735
```
```   736 lemma "(i \$+ j \$+ #12 \$+ k) = u \$+ #15 \$+ y" apply simp oops
```
```   737 lemma "(i \$+ j \$* #2 \$+ #12 \$+ k) = j \$+ #5 \$+ y" apply simp oops
```
```   738
```
```   739 lemma "#2 \$* y \$+ #3 \$* z \$+ #6 \$* w \$+ #2 \$* y \$+ #3 \$* z \$+ #2 \$* u = #2 \$* y' \$+ #3 \$* z' \$+ #6 \$* w' \$+ #2 \$* y' \$+ #3 \$* z' \$+ u \$+ vv" apply simp oops
```
```   740
```
```   741 lemma "a \$+ \$-(b\$+c) \$+ b = d" apply simp oops
```
```   742 lemma "a \$+ \$-(b\$+c) \$- b = d" apply simp oops
```
```   743
```
```   744 text \<open>negative numerals\<close>
```
```   745 lemma "(i \$+ j \$+ #-2 \$+ k) \$- (u \$+ #5 \$+ y) = zz" apply simp oops
```
```   746 lemma "(i \$+ j \$+ #-3 \$+ k) \$< u \$+ #5 \$+ y" apply simp oops
```
```   747 lemma "(i \$+ j \$+ #3 \$+ k) \$< u \$+ #-6 \$+ y" apply simp oops
```
```   748 lemma "(i \$+ j \$+ #-12 \$+ k) \$- #15 = y" apply simp oops
```
```   749 lemma "(i \$+ j \$+ #12 \$+ k) \$- #-15 = y" apply simp oops
```
```   750 lemma "(i \$+ j \$+ #-12 \$+ k) \$- #-15 = y" apply simp oops
```
```   751
```
```   752 text \<open>Multiplying separated numerals\<close>
```
```   753 lemma "#6 \$* (\$# x \$* #2) =  uu" apply simp oops
```
```   754 lemma "#4 \$* (\$# x \$* \$# x) \$* (#2 \$* \$# x) =  uu" apply simp oops
```
```   755
```
```   756 end
```