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