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