src/ZF/IntDiv_ZF.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58871 c399ae4b836f
child 60770 240563fbf41d
permissions -rw-r--r--
proper context for match_tac etc.;
wenzelm@32960
     1
(*  Title:      ZF/IntDiv_ZF.thy
krauss@26056
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
krauss@26056
     3
    Copyright   1999  University of Cambridge
krauss@26056
     4
krauss@26056
     5
Here is the division algorithm in ML:
krauss@26056
     6
krauss@26056
     7
    fun posDivAlg (a,b) =
krauss@26056
     8
      if a<b then (0,a)
krauss@26056
     9
      else let val (q,r) = posDivAlg(a, 2*b)
wenzelm@32960
    10
               in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
wenzelm@32960
    11
           end
krauss@26056
    12
krauss@26056
    13
    fun negDivAlg (a,b) =
krauss@26056
    14
      if 0<=a+b then (~1,a+b)
krauss@26056
    15
      else let val (q,r) = negDivAlg(a, 2*b)
wenzelm@32960
    16
               in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
wenzelm@32960
    17
           end;
krauss@26056
    18
krauss@26056
    19
    fun negateSnd (q,r:int) = (q,~r);
krauss@26056
    20
paulson@46820
    21
    fun divAlg (a,b) = if 0<=a then
paulson@46820
    22
                          if b>0 then posDivAlg (a,b)
wenzelm@32960
    23
                           else if a=0 then (0,0)
wenzelm@32960
    24
                                else negateSnd (negDivAlg (~a,~b))
paulson@46820
    25
                       else
wenzelm@32960
    26
                          if 0<b then negDivAlg (a,b)
wenzelm@32960
    27
                          else        negateSnd (posDivAlg (~a,~b));
krauss@26056
    28
*)
krauss@26056
    29
wenzelm@58871
    30
section{*The Division Operators Div and Mod*}
krauss@26056
    31
haftmann@58022
    32
theory IntDiv_ZF
haftmann@58022
    33
imports Bin OrderArith
haftmann@58022
    34
begin
krauss@26056
    35
krauss@26056
    36
definition
krauss@26056
    37
  quorem :: "[i,i] => o"  where
krauss@26056
    38
    "quorem == %<a,b> <q,r>.
krauss@26056
    39
                      a = b$*q $+ r &
krauss@26056
    40
                      (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
krauss@26056
    41
krauss@26056
    42
definition
krauss@26056
    43
  adjust :: "[i,i] => i"  where
krauss@26056
    44
    "adjust(b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
krauss@26056
    45
                          else <#2$*q,r>"
krauss@26056
    46
krauss@26056
    47
krauss@26056
    48
(** the division algorithm **)
krauss@26056
    49
krauss@26056
    50
definition
krauss@26056
    51
  posDivAlg :: "i => i"  where
krauss@26056
    52
(*for the case a>=0, b>0*)
krauss@26056
    53
(*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*)
krauss@26056
    54
    "posDivAlg(ab) ==
krauss@26056
    55
       wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
wenzelm@32960
    56
             ab,
wenzelm@32960
    57
             %<a,b> f. if (a$<b | b$<=#0) then <#0,a>
krauss@26056
    58
                       else adjust(b, f ` <a,#2$*b>))"
krauss@26056
    59
krauss@26056
    60
krauss@26056
    61
(*for the case a<0, b>0*)
krauss@26056
    62
definition
krauss@26056
    63
  negDivAlg :: "i => i"  where
krauss@26056
    64
(*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a $- b))"*)
krauss@26056
    65
    "negDivAlg(ab) ==
krauss@26056
    66
       wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)),
wenzelm@32960
    67
             ab,
wenzelm@32960
    68
             %<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b>
krauss@26056
    69
                       else adjust(b, f ` <a,#2$*b>))"
krauss@26056
    70
paulson@46820
    71
(*for the general case @{term"b\<noteq>0"}*)
krauss@26056
    72
krauss@26056
    73
definition
krauss@26056
    74
  negateSnd :: "i => i"  where
krauss@26056
    75
    "negateSnd == %<q,r>. <q, $-r>"
krauss@26056
    76
krauss@26056
    77
  (*The full division algorithm considers all possible signs for a, b
krauss@26056
    78
    including the special case a=0, b<0, because negDivAlg requires a<0*)
krauss@26056
    79
definition
krauss@26056
    80
  divAlg :: "i => i"  where
krauss@26056
    81
    "divAlg ==
krauss@26056
    82
       %<a,b>. if #0 $<= a then
krauss@26056
    83
                  if #0 $<= b then posDivAlg (<a,b>)
krauss@26056
    84
                  else if a=#0 then <#0,#0>
krauss@26056
    85
                       else negateSnd (negDivAlg (<$-a,$-b>))
paulson@46820
    86
               else
krauss@26056
    87
                  if #0$<b then negDivAlg (<a,b>)
krauss@26056
    88
                  else         negateSnd (posDivAlg (<$-a,$-b>))"
krauss@26056
    89
krauss@26056
    90
definition
krauss@26056
    91
  zdiv  :: "[i,i]=>i"                    (infixl "zdiv" 70)  where
krauss@26056
    92
    "a zdiv b == fst (divAlg (<intify(a), intify(b)>))"
krauss@26056
    93
krauss@26056
    94
definition
krauss@26056
    95
  zmod  :: "[i,i]=>i"                    (infixl "zmod" 70)  where
krauss@26056
    96
    "a zmod b == snd (divAlg (<intify(a), intify(b)>))"
krauss@26056
    97
krauss@26056
    98
krauss@26056
    99
(** Some basic laws by Sidi Ehmety (need linear arithmetic!) **)
krauss@26056
   100
krauss@26056
   101
lemma zspos_add_zspos_imp_zspos: "[| #0 $< x;  #0 $< y |] ==> #0 $< x $+ y"
krauss@26056
   102
apply (rule_tac y = "y" in zless_trans)
krauss@26056
   103
apply (rule_tac [2] zdiff_zless_iff [THEN iffD1])
krauss@26056
   104
apply auto
krauss@26056
   105
done
krauss@26056
   106
krauss@26056
   107
lemma zpos_add_zpos_imp_zpos: "[| #0 $<= x;  #0 $<= y |] ==> #0 $<= x $+ y"
krauss@26056
   108
apply (rule_tac y = "y" in zle_trans)
krauss@26056
   109
apply (rule_tac [2] zdiff_zle_iff [THEN iffD1])
krauss@26056
   110
apply auto
krauss@26056
   111
done
krauss@26056
   112
krauss@26056
   113
lemma zneg_add_zneg_imp_zneg: "[| x $< #0;  y $< #0 |] ==> x $+ y $< #0"
krauss@26056
   114
apply (rule_tac y = "y" in zless_trans)
krauss@26056
   115
apply (rule zless_zdiff_iff [THEN iffD1])
krauss@26056
   116
apply auto
krauss@26056
   117
done
krauss@26056
   118
krauss@26056
   119
(* this theorem is used below *)
krauss@26056
   120
lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:
krauss@26056
   121
     "[| x $<= #0;  y $<= #0 |] ==> x $+ y $<= #0"
krauss@26056
   122
apply (rule_tac y = "y" in zle_trans)
krauss@26056
   123
apply (rule zle_zdiff_iff [THEN iffD1])
krauss@26056
   124
apply auto
krauss@26056
   125
done
krauss@26056
   126
krauss@26056
   127
lemma zero_lt_zmagnitude: "[| #0 $< k; k \<in> int |] ==> 0 < zmagnitude(k)"
krauss@26056
   128
apply (drule zero_zless_imp_znegative_zminus)
krauss@26056
   129
apply (drule_tac [2] zneg_int_of)
krauss@26056
   130
apply (auto simp add: zminus_equation [of k])
krauss@26056
   131
apply (subgoal_tac "0 < zmagnitude ($# succ (n))")
krauss@26056
   132
 apply simp
krauss@26056
   133
apply (simp only: zmagnitude_int_of)
krauss@26056
   134
apply simp
krauss@26056
   135
done
krauss@26056
   136
krauss@26056
   137
krauss@26056
   138
(*** Inequality lemmas involving $#succ(m) ***)
krauss@26056
   139
krauss@26056
   140
lemma zless_add_succ_iff:
paulson@46821
   141
     "(w $< z $+ $# succ(m)) \<longleftrightarrow> (w $< z $+ $#m | intify(w) = z $+ $#m)"
krauss@26056
   142
apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
krauss@26056
   143
apply (rule_tac [3] x = "0" in bexI)
krauss@26056
   144
apply (cut_tac m = "m" in int_succ_int_1)
krauss@26056
   145
apply (cut_tac m = "n" in int_succ_int_1)
krauss@26056
   146
apply simp
krauss@26056
   147
apply (erule natE)
krauss@26056
   148
apply auto
krauss@26056
   149
apply (rule_tac x = "succ (n) " in bexI)
krauss@26056
   150
apply auto
krauss@26056
   151
done
krauss@26056
   152
krauss@26056
   153
lemma zadd_succ_lemma:
paulson@46821
   154
     "z \<in> int ==> (w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
krauss@26056
   155
apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
krauss@26056
   156
apply (auto intro: zle_anti_sym elim: zless_asym
krauss@26056
   157
            simp add: zless_imp_zle not_zless_iff_zle)
krauss@26056
   158
done
krauss@26056
   159
paulson@46821
   160
lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
krauss@26056
   161
apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
krauss@26056
   162
apply auto
krauss@26056
   163
done
krauss@26056
   164
krauss@26056
   165
(** Inequality reasoning **)
krauss@26056
   166
paulson@46821
   167
lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$<=z)"
krauss@26056
   168
apply (subgoal_tac "#1 = $# 1")
krauss@26056
   169
apply (simp only: zless_add_succ_iff zle_def)
krauss@26056
   170
apply auto
krauss@26056
   171
done
krauss@26056
   172
paulson@46821
   173
lemma add1_zle_iff: "(w $+ #1 $<= z) \<longleftrightarrow> (w $< z)"
krauss@26056
   174
apply (subgoal_tac "#1 = $# 1")
krauss@26056
   175
apply (simp only: zadd_succ_zle_iff)
krauss@26056
   176
apply auto
krauss@26056
   177
done
krauss@26056
   178
paulson@46821
   179
lemma add1_left_zle_iff: "(#1 $+ w $<= z) \<longleftrightarrow> (w $< z)"
krauss@26056
   180
apply (subst zadd_commute)
krauss@26056
   181
apply (rule add1_zle_iff)
krauss@26056
   182
done
krauss@26056
   183
krauss@26056
   184
krauss@26056
   185
(*** Monotonicity of Multiplication ***)
krauss@26056
   186
krauss@26056
   187
lemma zmult_mono_lemma: "k \<in> nat ==> i $<= j ==> i $* $#k $<= j $* $#k"
krauss@26056
   188
apply (induct_tac "k")
krauss@26056
   189
 prefer 2 apply (subst int_succ_int_1)
krauss@26056
   190
apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono)
krauss@26056
   191
done
krauss@26056
   192
krauss@26056
   193
lemma zmult_zle_mono1: "[| i $<= j;  #0 $<= k |] ==> i$*k $<= j$*k"
krauss@26056
   194
apply (subgoal_tac "i $* intify (k) $<= j $* intify (k) ")
krauss@26056
   195
apply (simp (no_asm_use))
krauss@26056
   196
apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
krauss@26056
   197
apply (rule_tac [3] zmult_mono_lemma)
krauss@26056
   198
apply auto
krauss@26056
   199
apply (simp add: znegative_iff_zless_0 not_zless_iff_zle [THEN iff_sym])
krauss@26056
   200
done
krauss@26056
   201
krauss@26056
   202
lemma zmult_zle_mono1_neg: "[| i $<= j;  k $<= #0 |] ==> j$*k $<= i$*k"
krauss@26056
   203
apply (rule zminus_zle_zminus [THEN iffD1])
krauss@26056
   204
apply (simp del: zmult_zminus_right
krauss@26056
   205
            add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
krauss@26056
   206
done
krauss@26056
   207
krauss@26056
   208
lemma zmult_zle_mono2: "[| i $<= j;  #0 $<= k |] ==> k$*i $<= k$*j"
krauss@26056
   209
apply (drule zmult_zle_mono1)
krauss@26056
   210
apply (simp_all add: zmult_commute)
krauss@26056
   211
done
krauss@26056
   212
krauss@26056
   213
lemma zmult_zle_mono2_neg: "[| i $<= j;  k $<= #0 |] ==> k$*j $<= k$*i"
krauss@26056
   214
apply (drule zmult_zle_mono1_neg)
krauss@26056
   215
apply (simp_all add: zmult_commute)
krauss@26056
   216
done
krauss@26056
   217
krauss@26056
   218
(* $<= monotonicity, BOTH arguments*)
krauss@26056
   219
lemma zmult_zle_mono:
krauss@26056
   220
     "[| i $<= j;  k $<= l;  #0 $<= j;  #0 $<= k |] ==> i$*k $<= j$*l"
krauss@26056
   221
apply (erule zmult_zle_mono1 [THEN zle_trans])
krauss@26056
   222
apply assumption
krauss@26056
   223
apply (erule zmult_zle_mono2)
krauss@26056
   224
apply assumption
krauss@26056
   225
done
krauss@26056
   226
krauss@26056
   227
krauss@26056
   228
(** strict, in 1st argument; proof is by induction on k>0 **)
krauss@26056
   229
krauss@26056
   230
lemma zmult_zless_mono2_lemma [rule_format]:
paulson@46820
   231
     "[| i$<j; k \<in> nat |] ==> 0<k \<longrightarrow> $#k $* i $< $#k $* j"
krauss@26056
   232
apply (induct_tac "k")
krauss@26056
   233
 prefer 2
krauss@26056
   234
 apply (subst int_succ_int_1)
krauss@26056
   235
 apply (erule natE)
krauss@26056
   236
apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def)
krauss@26056
   237
apply (frule nat_0_le)
krauss@26056
   238
apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ")
krauss@26056
   239
apply (simp (no_asm_use))
krauss@26056
   240
apply (rule zadd_zless_mono)
krauss@26056
   241
apply (simp_all (no_asm_simp) add: zle_def)
krauss@26056
   242
done
krauss@26056
   243
krauss@26056
   244
lemma zmult_zless_mono2: "[| i$<j;  #0 $< k |] ==> k$*i $< k$*j"
krauss@26056
   245
apply (subgoal_tac "intify (k) $* i $< intify (k) $* j")
krauss@26056
   246
apply (simp (no_asm_use))
krauss@26056
   247
apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
krauss@26056
   248
apply (rule_tac [3] zmult_zless_mono2_lemma)
krauss@26056
   249
apply auto
krauss@26056
   250
apply (simp add: znegative_iff_zless_0)
krauss@26056
   251
apply (drule zless_trans, assumption)
krauss@26056
   252
apply (auto simp add: zero_lt_zmagnitude)
krauss@26056
   253
done
krauss@26056
   254
krauss@26056
   255
lemma zmult_zless_mono1: "[| i$<j;  #0 $< k |] ==> i$*k $< j$*k"
krauss@26056
   256
apply (drule zmult_zless_mono2)
krauss@26056
   257
apply (simp_all add: zmult_commute)
krauss@26056
   258
done
krauss@26056
   259
krauss@26056
   260
(* < monotonicity, BOTH arguments*)
krauss@26056
   261
lemma zmult_zless_mono:
krauss@26056
   262
     "[| i $< j;  k $< l;  #0 $< j;  #0 $< k |] ==> i$*k $< j$*l"
krauss@26056
   263
apply (erule zmult_zless_mono1 [THEN zless_trans])
krauss@26056
   264
apply assumption
krauss@26056
   265
apply (erule zmult_zless_mono2)
krauss@26056
   266
apply assumption
krauss@26056
   267
done
krauss@26056
   268
krauss@26056
   269
lemma zmult_zless_mono1_neg: "[| i $< j;  k $< #0 |] ==> j$*k $< i$*k"
krauss@26056
   270
apply (rule zminus_zless_zminus [THEN iffD1])
paulson@46820
   271
apply (simp del: zmult_zminus_right
krauss@26056
   272
            add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
krauss@26056
   273
done
krauss@26056
   274
krauss@26056
   275
lemma zmult_zless_mono2_neg: "[| i $< j;  k $< #0 |] ==> k$*j $< k$*i"
krauss@26056
   276
apply (rule zminus_zless_zminus [THEN iffD1])
paulson@46820
   277
apply (simp del: zmult_zminus
krauss@26056
   278
            add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
krauss@26056
   279
done
krauss@26056
   280
krauss@26056
   281
krauss@26056
   282
(** Products of zeroes **)
krauss@26056
   283
krauss@26056
   284
lemma zmult_eq_lemma:
paulson@46821
   285
     "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) \<longleftrightarrow> (m$*n = #0)"
krauss@26056
   286
apply (case_tac "m $< #0")
krauss@26056
   287
apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
krauss@26056
   288
apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
krauss@26056
   289
done
krauss@26056
   290
paulson@46821
   291
lemma zmult_eq_0_iff [iff]: "(m$*n = #0) \<longleftrightarrow> (intify(m) = #0 | intify(n) = #0)"
krauss@26056
   292
apply (simp add: zmult_eq_lemma)
krauss@26056
   293
done
krauss@26056
   294
krauss@26056
   295
paulson@46820
   296
(** Cancellation laws for k*m < k*n and m*k < n*k, also for @{text"\<le>"} and =,
krauss@26056
   297
    but not (yet?) for k*m < n*k. **)
krauss@26056
   298
krauss@26056
   299
lemma zmult_zless_lemma:
paulson@46820
   300
     "[| k \<in> int; m \<in> int; n \<in> int |]
paulson@46821
   301
      ==> (m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
krauss@26056
   302
apply (case_tac "k = #0")
krauss@26056
   303
apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
paulson@46820
   304
apply (auto simp add: not_zless_iff_zle
paulson@46820
   305
                      not_zle_iff_zless [THEN iff_sym, of "m$*k"]
krauss@26056
   306
                      not_zle_iff_zless [THEN iff_sym, of m])
krauss@26056
   307
apply (auto elim: notE
krauss@26056
   308
            simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
krauss@26056
   309
done
krauss@26056
   310
krauss@26056
   311
lemma zmult_zless_cancel2:
paulson@46821
   312
     "(m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
paulson@46820
   313
apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
krauss@26056
   314
       in zmult_zless_lemma)
krauss@26056
   315
apply auto
krauss@26056
   316
done
krauss@26056
   317
krauss@26056
   318
lemma zmult_zless_cancel1:
paulson@46821
   319
     "(k$*m $< k$*n) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
krauss@26056
   320
by (simp add: zmult_commute [of k] zmult_zless_cancel2)
krauss@26056
   321
krauss@26056
   322
lemma zmult_zle_cancel2:
paulson@46821
   323
     "(m$*k $<= n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
krauss@26056
   324
by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
krauss@26056
   325
krauss@26056
   326
lemma zmult_zle_cancel1:
paulson@46821
   327
     "(k$*m $<= k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
krauss@26056
   328
by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
krauss@26056
   329
paulson@46821
   330
lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $<= n & n $<= m)"
krauss@26056
   331
apply (blast intro: zle_refl zle_anti_sym)
krauss@26056
   332
done
krauss@26056
   333
krauss@26056
   334
lemma zmult_cancel2_lemma:
paulson@46821
   335
     "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) \<longleftrightarrow> (k=#0 | m=n)"
krauss@26056
   336
apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m])
krauss@26056
   337
apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
krauss@26056
   338
done
krauss@26056
   339
krauss@26056
   340
lemma zmult_cancel2 [simp]:
paulson@46821
   341
     "(m$*k = n$*k) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
krauss@26056
   342
apply (rule iff_trans)
krauss@26056
   343
apply (rule_tac [2] zmult_cancel2_lemma)
krauss@26056
   344
apply auto
krauss@26056
   345
done
krauss@26056
   346
krauss@26056
   347
lemma zmult_cancel1 [simp]:
paulson@46821
   348
     "(k$*m = k$*n) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
krauss@26056
   349
by (simp add: zmult_commute [of k] zmult_cancel2)
krauss@26056
   350
krauss@26056
   351
krauss@26056
   352
subsection{* Uniqueness and monotonicity of quotients and remainders *}
krauss@26056
   353
krauss@26056
   354
lemma unique_quotient_lemma:
paulson@46820
   355
     "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |]
krauss@26056
   356
      ==> q' $<= q"
krauss@26056
   357
apply (subgoal_tac "r' $+ b $* (q'$-q) $<= r")
krauss@26056
   358
 prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls)
krauss@26056
   359
apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ")
krauss@26056
   360
 prefer 2
krauss@26056
   361
 apply (erule zle_zless_trans)
krauss@26056
   362
 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
krauss@26056
   363
 apply (erule zle_zless_trans)
paulson@46993
   364
 apply simp
krauss@26056
   365
apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)")
paulson@46820
   366
 prefer 2
krauss@26056
   367
 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
krauss@26056
   368
apply (auto elim: zless_asym
krauss@26056
   369
        simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls)
krauss@26056
   370
done
krauss@26056
   371
krauss@26056
   372
lemma unique_quotient_lemma_neg:
paulson@46820
   373
     "[| b$*q' $+ r' $<= b$*q $+ r;  r $<= #0;  b $< #0;  b $< r' |]
krauss@26056
   374
      ==> q $<= q'"
paulson@46820
   375
apply (rule_tac b = "$-b" and r = "$-r'" and r' = "$-r"
krauss@26056
   376
       in unique_quotient_lemma)
krauss@26056
   377
apply (auto simp del: zminus_zadd_distrib
krauss@26056
   378
            simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus)
krauss@26056
   379
done
krauss@26056
   380
krauss@26056
   381
krauss@26056
   382
lemma unique_quotient:
paulson@46820
   383
     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
krauss@26056
   384
         q \<in> int; q' \<in> int |] ==> q = q'"
krauss@26056
   385
apply (simp add: split_ifs quorem_def neq_iff_zless)
krauss@26056
   386
apply safe
krauss@26056
   387
apply simp_all
krauss@26056
   388
apply (blast intro: zle_anti_sym
paulson@46820
   389
             dest: zle_eq_refl [THEN unique_quotient_lemma]
krauss@26056
   390
                   zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+
krauss@26056
   391
done
krauss@26056
   392
krauss@26056
   393
lemma unique_remainder:
paulson@46820
   394
     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
paulson@46820
   395
         q \<in> int; q' \<in> int;
krauss@26056
   396
         r \<in> int; r' \<in> int |] ==> r = r'"
krauss@26056
   397
apply (subgoal_tac "q = q'")
krauss@26056
   398
 prefer 2 apply (blast intro: unique_quotient)
krauss@26056
   399
apply (simp add: quorem_def)
krauss@26056
   400
done
krauss@26056
   401
krauss@26056
   402
paulson@46820
   403
subsection{*Correctness of posDivAlg,
krauss@26056
   404
           the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"} *}
krauss@26056
   405
krauss@26056
   406
lemma adjust_eq [simp]:
paulson@46820
   407
     "adjust(b, <q,r>) = (let diff = r$-b in
paulson@46820
   408
                          if #0 $<= diff then <#2$*q $+ #1,diff>
krauss@26056
   409
                                         else <#2$*q,r>)"
krauss@26056
   410
by (simp add: Let_def adjust_def)
krauss@26056
   411
krauss@26056
   412
krauss@26056
   413
lemma posDivAlg_termination:
paulson@46820
   414
     "[| #0 $< b; ~ a $< b |]
krauss@26056
   415
      ==> nat_of(a $- #2 $\<times> b $+ #1) < nat_of(a $- b $+ #1)"
krauss@26056
   416
apply (simp (no_asm) add: zless_nat_conj)
krauss@26056
   417
apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls)
krauss@26056
   418
done
krauss@26056
   419
krauss@26056
   420
lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure]
krauss@26056
   421
krauss@26056
   422
lemma posDivAlg_eqn:
paulson@46820
   423
     "[| #0 $< b; a \<in> int; b \<in> int |] ==>
paulson@46820
   424
      posDivAlg(<a,b>) =
krauss@26056
   425
       (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))"
krauss@26056
   426
apply (rule posDivAlg_unfold [THEN trans])
krauss@26056
   427
apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym])
krauss@26056
   428
apply (blast intro: posDivAlg_termination)
krauss@26056
   429
done
krauss@26056
   430
krauss@26056
   431
lemma posDivAlg_induct_lemma [rule_format]:
krauss@26056
   432
  assumes prem:
paulson@46820
   433
        "!!a b. [| a \<in> int; b \<in> int;
paulson@46820
   434
                   ~ (a $< b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)"
paulson@46993
   435
  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
paulson@46993
   436
using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"]
paulson@46993
   437
proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
paulson@46993
   438
  case (step x)
paulson@46993
   439
  hence uv: "u \<in> int" "v \<in> int" by auto
paulson@46993
   440
  thus ?case
paulson@46993
   441
    apply (rule prem) 
paulson@46993
   442
    apply (rule impI) 
paulson@46993
   443
    apply (rule step) 
paulson@46993
   444
    apply (auto simp add: step uv not_zle_iff_zless posDivAlg_termination)
paulson@46993
   445
    done
paulson@46993
   446
qed
krauss@26056
   447
krauss@26056
   448
krauss@26056
   449
lemma posDivAlg_induct [consumes 2]:
krauss@26056
   450
  assumes u_int: "u \<in> int"
krauss@26056
   451
      and v_int: "v \<in> int"
krauss@26056
   452
      and ih: "!!a b. [| a \<in> int; b \<in> int;
paulson@46820
   453
                     ~ (a $< b | b $<= #0) \<longrightarrow> P(a, #2 $* b) |] ==> P(a,b)"
krauss@26056
   454
  shows "P(u,v)"
krauss@26056
   455
apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
krauss@26056
   456
apply simp
krauss@26056
   457
apply (rule posDivAlg_induct_lemma)
krauss@26056
   458
apply (simp (no_asm_use))
krauss@26056
   459
apply (rule ih)
krauss@26056
   460
apply (auto simp add: u_int v_int)
krauss@26056
   461
done
krauss@26056
   462
paulson@46820
   463
(*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
paulson@46820
   464
    then this rewrite can work for all constants!!*)
paulson@46821
   465
lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
paulson@46993
   466
  by (simp add: int_eq_iff_zle)
krauss@26056
   467
krauss@26056
   468
krauss@26056
   469
subsection{* Some convenient biconditionals for products of signs *}
krauss@26056
   470
krauss@26056
   471
lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j"
paulson@46993
   472
  by (drule zmult_zless_mono1, auto)
krauss@26056
   473
krauss@26056
   474
lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j"
paulson@46993
   475
  by (drule zmult_zless_mono1_neg, auto)
krauss@26056
   476
krauss@26056
   477
lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0"
paulson@46993
   478
  by (drule zmult_zless_mono1_neg, auto)
paulson@46993
   479
krauss@26056
   480
krauss@26056
   481
(** Inequality reasoning **)
krauss@26056
   482
krauss@26056
   483
lemma int_0_less_lemma:
paulson@46820
   484
     "[| x \<in> int; y \<in> int |]
paulson@46821
   485
      ==> (#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
krauss@26056
   486
apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
paulson@46820
   487
apply (rule ccontr)
paulson@46820
   488
apply (rule_tac [2] ccontr)
krauss@26056
   489
apply (auto simp add: zle_def not_zless_iff_zle)
krauss@26056
   490
apply (erule_tac P = "#0$< x$* y" in rev_mp)
krauss@26056
   491
apply (erule_tac [2] P = "#0$< x$* y" in rev_mp)
paulson@46820
   492
apply (drule zmult_pos_neg, assumption)
krauss@26056
   493
 prefer 2
paulson@46820
   494
 apply (drule zmult_pos_neg, assumption)
krauss@26056
   495
apply (auto dest: zless_not_sym simp add: zmult_commute)
krauss@26056
   496
done
krauss@26056
   497
krauss@26056
   498
lemma int_0_less_mult_iff:
paulson@46821
   499
     "(#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
krauss@26056
   500
apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
krauss@26056
   501
apply auto
krauss@26056
   502
done
krauss@26056
   503
krauss@26056
   504
lemma int_0_le_lemma:
paulson@46820
   505
     "[| x \<in> int; y \<in> int |]
paulson@46821
   506
      ==> (#0 $<= x $* y) \<longleftrightarrow> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
krauss@26056
   507
by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
krauss@26056
   508
krauss@26056
   509
lemma int_0_le_mult_iff:
paulson@46821
   510
     "(#0 $<= x $* y) \<longleftrightarrow> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
krauss@26056
   511
apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
krauss@26056
   512
apply auto
krauss@26056
   513
done
krauss@26056
   514
krauss@26056
   515
lemma zmult_less_0_iff:
paulson@46821
   516
     "(x $* y $< #0) \<longleftrightarrow> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
krauss@26056
   517
apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
krauss@26056
   518
apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
krauss@26056
   519
done
krauss@26056
   520
krauss@26056
   521
lemma zmult_le_0_iff:
paulson@46821
   522
     "(x $* y $<= #0) \<longleftrightarrow> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
krauss@26056
   523
by (auto dest: zless_not_sym
krauss@26056
   524
         simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])
krauss@26056
   525
krauss@26056
   526
krauss@26056
   527
(*Typechecking for posDivAlg*)
krauss@26056
   528
lemma posDivAlg_type [rule_format]:
krauss@26056
   529
     "[| a \<in> int; b \<in> int |] ==> posDivAlg(<a,b>) \<in> int * int"
krauss@26056
   530
apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
krauss@26056
   531
apply assumption+
krauss@26056
   532
apply (case_tac "#0 $< ba")
paulson@46820
   533
 apply (simp add: posDivAlg_eqn adjust_def integ_of_type
krauss@26056
   534
             split add: split_if_asm)
krauss@26056
   535
 apply clarify
krauss@26056
   536
 apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
krauss@26056
   537
apply (simp add: not_zless_iff_zle)
krauss@26056
   538
apply (subst posDivAlg_unfold)
krauss@26056
   539
apply simp
krauss@26056
   540
done
krauss@26056
   541
krauss@26056
   542
(*Correctness of posDivAlg: it computes quotients correctly*)
krauss@26056
   543
lemma posDivAlg_correct [rule_format]:
paulson@46820
   544
     "[| a \<in> int; b \<in> int |]
paulson@46820
   545
      ==> #0 $<= a \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, posDivAlg(<a,b>))"
krauss@26056
   546
apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
krauss@26056
   547
apply auto
krauss@26056
   548
   apply (simp_all add: quorem_def)
krauss@26056
   549
   txt{*base case: a<b*}
krauss@26056
   550
   apply (simp add: posDivAlg_eqn)
krauss@26056
   551
  apply (simp add: not_zless_iff_zle [THEN iff_sym])
krauss@26056
   552
 apply (simp add: int_0_less_mult_iff)
krauss@26056
   553
txt{*main argument*}
krauss@26056
   554
apply (subst posDivAlg_eqn)
krauss@26056
   555
apply (simp_all (no_asm_simp))
krauss@26056
   556
apply (erule splitE)
krauss@26056
   557
apply (rule posDivAlg_type)
krauss@26056
   558
apply (simp_all add: int_0_less_mult_iff)
krauss@26056
   559
apply (auto simp add: zadd_zmult_distrib2 Let_def)
krauss@26056
   560
txt{*now just linear arithmetic*}
krauss@26056
   561
apply (simp add: not_zle_iff_zless zdiff_zless_iff)
krauss@26056
   562
done
krauss@26056
   563
krauss@26056
   564
krauss@26056
   565
subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*}
krauss@26056
   566
krauss@26056
   567
lemma negDivAlg_termination:
paulson@46820
   568
     "[| #0 $< b; a $+ b $< #0 |]
krauss@26056
   569
      ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)"
krauss@26056
   570
apply (simp (no_asm) add: zless_nat_conj)
krauss@26056
   571
apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym]
krauss@26056
   572
                 zless_zminus)
krauss@26056
   573
done
krauss@26056
   574
krauss@26056
   575
lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure]
krauss@26056
   576
krauss@26056
   577
lemma negDivAlg_eqn:
paulson@46820
   578
     "[| #0 $< b; a \<in> int; b \<in> int |] ==>
paulson@46820
   579
      negDivAlg(<a,b>) =
paulson@46820
   580
       (if #0 $<= a$+b then <#-1,a$+b>
krauss@26056
   581
                       else adjust(b, negDivAlg (<a, #2$*b>)))"
krauss@26056
   582
apply (rule negDivAlg_unfold [THEN trans])
krauss@26056
   583
apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym])
krauss@26056
   584
apply (blast intro: negDivAlg_termination)
krauss@26056
   585
done
krauss@26056
   586
krauss@26056
   587
lemma negDivAlg_induct_lemma [rule_format]:
krauss@26056
   588
  assumes prem:
paulson@46820
   589
        "!!a b. [| a \<in> int; b \<in> int;
paulson@46820
   590
                   ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |]
krauss@26056
   591
                ==> P(<a,b>)"
paulson@46993
   592
  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
paulson@46993
   593
using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"]
paulson@46993
   594
proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
paulson@46993
   595
  case (step x)
paulson@46993
   596
  hence uv: "u \<in> int" "v \<in> int" by auto
paulson@46993
   597
  thus ?case
paulson@46993
   598
    apply (rule prem) 
paulson@46993
   599
    apply (rule impI) 
paulson@46993
   600
    apply (rule step) 
paulson@46993
   601
    apply (auto simp add: step uv not_zle_iff_zless negDivAlg_termination)
paulson@46993
   602
    done
paulson@46993
   603
qed
krauss@26056
   604
krauss@26056
   605
lemma negDivAlg_induct [consumes 2]:
krauss@26056
   606
  assumes u_int: "u \<in> int"
krauss@26056
   607
      and v_int: "v \<in> int"
paulson@46820
   608
      and ih: "!!a b. [| a \<in> int; b \<in> int;
paulson@46820
   609
                         ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(a, #2 $* b) |]
krauss@26056
   610
                      ==> P(a,b)"
krauss@26056
   611
  shows "P(u,v)"
krauss@26056
   612
apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
krauss@26056
   613
apply simp
krauss@26056
   614
apply (rule negDivAlg_induct_lemma)
krauss@26056
   615
apply (simp (no_asm_use))
krauss@26056
   616
apply (rule ih)
krauss@26056
   617
apply (auto simp add: u_int v_int)
krauss@26056
   618
done
krauss@26056
   619
krauss@26056
   620
krauss@26056
   621
(*Typechecking for negDivAlg*)
krauss@26056
   622
lemma negDivAlg_type:
krauss@26056
   623
     "[| a \<in> int; b \<in> int |] ==> negDivAlg(<a,b>) \<in> int * int"
krauss@26056
   624
apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
krauss@26056
   625
apply assumption+
krauss@26056
   626
apply (case_tac "#0 $< ba")
paulson@46820
   627
 apply (simp add: negDivAlg_eqn adjust_def integ_of_type
krauss@26056
   628
             split add: split_if_asm)
krauss@26056
   629
 apply clarify
krauss@26056
   630
 apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
krauss@26056
   631
apply (simp add: not_zless_iff_zle)
krauss@26056
   632
apply (subst negDivAlg_unfold)
krauss@26056
   633
apply simp
krauss@26056
   634
done
krauss@26056
   635
krauss@26056
   636
krauss@26056
   637
(*Correctness of negDivAlg: it computes quotients correctly
krauss@26056
   638
  It doesn't work if a=0 because the 0/b=0 rather than -1*)
krauss@26056
   639
lemma negDivAlg_correct [rule_format]:
paulson@46820
   640
     "[| a \<in> int; b \<in> int |]
paulson@46820
   641
      ==> a $< #0 \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, negDivAlg(<a,b>))"
krauss@26056
   642
apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
krauss@26056
   643
  apply auto
krauss@26056
   644
   apply (simp_all add: quorem_def)
krauss@26056
   645
   txt{*base case: @{term "0$<=a$+b"}*}
krauss@26056
   646
   apply (simp add: negDivAlg_eqn)
krauss@26056
   647
  apply (simp add: not_zless_iff_zle [THEN iff_sym])
krauss@26056
   648
 apply (simp add: int_0_less_mult_iff)
krauss@26056
   649
txt{*main argument*}
krauss@26056
   650
apply (subst negDivAlg_eqn)
krauss@26056
   651
apply (simp_all (no_asm_simp))
krauss@26056
   652
apply (erule splitE)
krauss@26056
   653
apply (rule negDivAlg_type)
krauss@26056
   654
apply (simp_all add: int_0_less_mult_iff)
krauss@26056
   655
apply (auto simp add: zadd_zmult_distrib2 Let_def)
krauss@26056
   656
txt{*now just linear arithmetic*}
krauss@26056
   657
apply (simp add: not_zle_iff_zless zdiff_zless_iff)
krauss@26056
   658
done
krauss@26056
   659
krauss@26056
   660
krauss@26056
   661
subsection{* Existence shown by proving the division algorithm to be correct *}
krauss@26056
   662
krauss@26056
   663
(*the case a=0*)
krauss@26056
   664
lemma quorem_0: "[|b \<noteq> #0;  b \<in> int|] ==> quorem (<#0,b>, <#0,#0>)"
krauss@26056
   665
by (force simp add: quorem_def neq_iff_zless)
krauss@26056
   666
krauss@26056
   667
lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>"
krauss@26056
   668
apply (subst posDivAlg_unfold)
krauss@26056
   669
apply simp
krauss@26056
   670
done
krauss@26056
   671
krauss@26056
   672
lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>"
krauss@26056
   673
apply (subst posDivAlg_unfold)
krauss@26056
   674
apply (simp add: not_zle_iff_zless)
krauss@26056
   675
done
krauss@26056
   676
krauss@26056
   677
krauss@26056
   678
(*Needed below.  Actually it's an equivalence.*)
krauss@26056
   679
lemma linear_arith_lemma: "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)"
krauss@26056
   680
apply (simp add: not_zle_iff_zless)
krauss@26056
   681
apply (drule zminus_zless_zminus [THEN iffD2])
krauss@26056
   682
apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus)
krauss@26056
   683
done
krauss@26056
   684
krauss@26056
   685
lemma negDivAlg_minus1 [simp]: "negDivAlg (<#-1,b>) = <#-1, b$-#1>"
krauss@26056
   686
apply (subst negDivAlg_unfold)
krauss@26056
   687
apply (simp add: linear_arith_lemma integ_of_type vimage_iff)
krauss@26056
   688
done
krauss@26056
   689
krauss@26056
   690
lemma negateSnd_eq [simp]: "negateSnd (<q,r>) = <q, $-r>"
krauss@26056
   691
apply (unfold negateSnd_def)
krauss@26056
   692
apply auto
krauss@26056
   693
done
krauss@26056
   694
krauss@26056
   695
lemma negateSnd_type: "qr \<in> int * int ==> negateSnd (qr) \<in> int * int"
krauss@26056
   696
apply (unfold negateSnd_def)
krauss@26056
   697
apply auto
krauss@26056
   698
done
krauss@26056
   699
krauss@26056
   700
lemma quorem_neg:
paulson@46820
   701
     "[|quorem (<$-a,$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int|]
krauss@26056
   702
      ==> quorem (<a,b>, negateSnd(qr))"
krauss@26056
   703
apply clarify
krauss@26056
   704
apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
krauss@26056
   705
txt{*linear arithmetic from here on*}
krauss@26056
   706
apply (simp_all add: zminus_equation [of a] zminus_zless)
krauss@26056
   707
apply (cut_tac [2] z = "b" and w = "#0" in zless_linear)
krauss@26056
   708
apply (cut_tac [1] z = "b" and w = "#0" in zless_linear)
krauss@26056
   709
apply auto
krauss@26056
   710
apply (blast dest: zle_zless_trans)+
krauss@26056
   711
done
krauss@26056
   712
krauss@26056
   713
lemma divAlg_correct:
krauss@26056
   714
     "[|b \<noteq> #0;  a \<in> int;  b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
krauss@26056
   715
apply (auto simp add: quorem_0 divAlg_def)
krauss@26056
   716
apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
paulson@46820
   717
                    posDivAlg_type negDivAlg_type)
krauss@26056
   718
apply (auto simp add: quorem_def neq_iff_zless)
krauss@26056
   719
txt{*linear arithmetic from here on*}
krauss@26056
   720
apply (auto simp add: zle_def)
krauss@26056
   721
done
krauss@26056
   722
krauss@26056
   723
lemma divAlg_type: "[|a \<in> int;  b \<in> int|] ==> divAlg(<a,b>) \<in> int * int"
krauss@26056
   724
apply (auto simp add: divAlg_def)
krauss@26056
   725
apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type)
krauss@26056
   726
done
krauss@26056
   727
krauss@26056
   728
krauss@26056
   729
(** intify cancellation **)
krauss@26056
   730
krauss@26056
   731
lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y"
paulson@46993
   732
  by (simp add: zdiv_def)
krauss@26056
   733
krauss@26056
   734
lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y"
paulson@46993
   735
  by (simp add: zdiv_def)
krauss@26056
   736
krauss@26056
   737
lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
krauss@26056
   738
apply (unfold zdiv_def)
krauss@26056
   739
apply (blast intro: fst_type divAlg_type)
krauss@26056
   740
done
krauss@26056
   741
krauss@26056
   742
lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y"
paulson@46993
   743
  by (simp add: zmod_def)
krauss@26056
   744
krauss@26056
   745
lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y"
paulson@46993
   746
  by (simp add: zmod_def)
krauss@26056
   747
krauss@26056
   748
lemma zmod_type [iff,TC]: "z zmod w \<in> int"
krauss@26056
   749
apply (unfold zmod_def)
krauss@26056
   750
apply (rule snd_type)
krauss@26056
   751
apply (blast intro: divAlg_type)
krauss@26056
   752
done
krauss@26056
   753
krauss@26056
   754
paulson@46820
   755
(** Arbitrary definitions for division by zero.  Useful to simplify
krauss@26056
   756
    certain equations **)
krauss@26056
   757
krauss@26056
   758
lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
paulson@46993
   759
  by (simp add: zdiv_def divAlg_def posDivAlg_zero_divisor)
krauss@26056
   760
krauss@26056
   761
lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)"
paulson@46993
   762
  by (simp add: zmod_def divAlg_def posDivAlg_zero_divisor)
krauss@26056
   763
krauss@26056
   764
krauss@26056
   765
(** Basic laws about division and remainder **)
krauss@26056
   766
krauss@26056
   767
lemma raw_zmod_zdiv_equality:
krauss@26056
   768
     "[| a \<in> int; b \<in> int |] ==> a = b $* (a zdiv b) $+ (a zmod b)"
krauss@26056
   769
apply (case_tac "b = #0")
paulson@46820
   770
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
   771
apply (cut_tac a = "a" and b = "b" in divAlg_correct)
krauss@26056
   772
apply (auto simp add: quorem_def zdiv_def zmod_def split_def)
krauss@26056
   773
done
krauss@26056
   774
krauss@26056
   775
lemma zmod_zdiv_equality: "intify(a) = b $* (a zdiv b) $+ (a zmod b)"
krauss@26056
   776
apply (rule trans)
krauss@26056
   777
apply (rule_tac b = "intify (b)" in raw_zmod_zdiv_equality)
krauss@26056
   778
apply auto
krauss@26056
   779
done
krauss@26056
   780
krauss@26056
   781
lemma pos_mod: "#0 $< b ==> #0 $<= a zmod b & a zmod b $< b"
krauss@26056
   782
apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
krauss@26056
   783
apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
krauss@26056
   784
apply (blast dest: zle_zless_trans)+
krauss@26056
   785
done
krauss@26056
   786
wenzelm@45602
   787
lemmas pos_mod_sign = pos_mod [THEN conjunct1]
wenzelm@45602
   788
  and pos_mod_bound = pos_mod [THEN conjunct2]
krauss@26056
   789
krauss@26056
   790
lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b"
krauss@26056
   791
apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
krauss@26056
   792
apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
krauss@26056
   793
apply (blast dest: zle_zless_trans)
krauss@26056
   794
apply (blast dest: zless_trans)+
krauss@26056
   795
done
krauss@26056
   796
wenzelm@45602
   797
lemmas neg_mod_sign = neg_mod [THEN conjunct1]
wenzelm@45602
   798
  and neg_mod_bound = neg_mod [THEN conjunct2]
krauss@26056
   799
krauss@26056
   800
krauss@26056
   801
(** proving general properties of zdiv and zmod **)
krauss@26056
   802
krauss@26056
   803
lemma quorem_div_mod:
paulson@46820
   804
     "[|b \<noteq> #0;  a \<in> int;  b \<in> int |]
krauss@26056
   805
      ==> quorem (<a,b>, <a zdiv b, a zmod b>)"
krauss@26056
   806
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
paulson@46820
   807
apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
krauss@26056
   808
                      neg_mod_sign neg_mod_bound)
krauss@26056
   809
done
krauss@26056
   810
paulson@46820
   811
(*Surely quorem(<a,b>,<q,r>) implies @{term"a \<in> int"}, but it doesn't matter*)
krauss@26056
   812
lemma quorem_div:
paulson@46820
   813
     "[| quorem(<a,b>,<q,r>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int |]
krauss@26056
   814
      ==> a zdiv b = q"
krauss@26056
   815
by (blast intro: quorem_div_mod [THEN unique_quotient])
krauss@26056
   816
krauss@26056
   817
lemma quorem_mod:
paulson@46820
   818
     "[| quorem(<a,b>,<q,r>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int |]
krauss@26056
   819
      ==> a zmod b = r"
krauss@26056
   820
by (blast intro: quorem_div_mod [THEN unique_remainder])
krauss@26056
   821
krauss@26056
   822
lemma zdiv_pos_pos_trivial_raw:
krauss@26056
   823
     "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zdiv b = #0"
krauss@26056
   824
apply (rule quorem_div)
krauss@26056
   825
apply (auto simp add: quorem_def)
krauss@26056
   826
(*linear arithmetic*)
krauss@26056
   827
apply (blast dest: zle_zless_trans)+
krauss@26056
   828
done
krauss@26056
   829
krauss@26056
   830
lemma zdiv_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zdiv b = #0"
paulson@46820
   831
apply (cut_tac a = "intify (a)" and b = "intify (b)"
krauss@26056
   832
       in zdiv_pos_pos_trivial_raw)
krauss@26056
   833
apply auto
krauss@26056
   834
done
krauss@26056
   835
krauss@26056
   836
lemma zdiv_neg_neg_trivial_raw:
krauss@26056
   837
     "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zdiv b = #0"
krauss@26056
   838
apply (rule_tac r = "a" in quorem_div)
krauss@26056
   839
apply (auto simp add: quorem_def)
krauss@26056
   840
(*linear arithmetic*)
krauss@26056
   841
apply (blast dest: zle_zless_trans zless_trans)+
krauss@26056
   842
done
krauss@26056
   843
krauss@26056
   844
lemma zdiv_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zdiv b = #0"
paulson@46820
   845
apply (cut_tac a = "intify (a)" and b = "intify (b)"
krauss@26056
   846
       in zdiv_neg_neg_trivial_raw)
krauss@26056
   847
apply auto
krauss@26056
   848
done
krauss@26056
   849
krauss@26056
   850
lemma zadd_le_0_lemma: "[| a$+b $<= #0;  #0 $< a;  #0 $< b |] ==> False"
krauss@26056
   851
apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono)
krauss@26056
   852
apply (auto simp add: zle_def)
krauss@26056
   853
apply (blast dest: zless_trans)
krauss@26056
   854
done
krauss@26056
   855
krauss@26056
   856
lemma zdiv_pos_neg_trivial_raw:
krauss@26056
   857
     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
krauss@26056
   858
apply (rule_tac r = "a $+ b" in quorem_div)
krauss@26056
   859
apply (auto simp add: quorem_def)
krauss@26056
   860
(*linear arithmetic*)
krauss@26056
   861
apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
krauss@26056
   862
done
krauss@26056
   863
krauss@26056
   864
lemma zdiv_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
paulson@46820
   865
apply (cut_tac a = "intify (a)" and b = "intify (b)"
krauss@26056
   866
       in zdiv_pos_neg_trivial_raw)
krauss@26056
   867
apply auto
krauss@26056
   868
done
krauss@26056
   869
krauss@26056
   870
(*There is no zdiv_neg_pos_trivial because  #0 zdiv b = #0 would supersede it*)
krauss@26056
   871
krauss@26056
   872
krauss@26056
   873
lemma zmod_pos_pos_trivial_raw:
krauss@26056
   874
     "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zmod b = a"
krauss@26056
   875
apply (rule_tac q = "#0" in quorem_mod)
krauss@26056
   876
apply (auto simp add: quorem_def)
krauss@26056
   877
(*linear arithmetic*)
krauss@26056
   878
apply (blast dest: zle_zless_trans)+
krauss@26056
   879
done
krauss@26056
   880
krauss@26056
   881
lemma zmod_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zmod b = intify(a)"
paulson@46820
   882
apply (cut_tac a = "intify (a)" and b = "intify (b)"
krauss@26056
   883
       in zmod_pos_pos_trivial_raw)
krauss@26056
   884
apply auto
krauss@26056
   885
done
krauss@26056
   886
krauss@26056
   887
lemma zmod_neg_neg_trivial_raw:
krauss@26056
   888
     "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zmod b = a"
krauss@26056
   889
apply (rule_tac q = "#0" in quorem_mod)
krauss@26056
   890
apply (auto simp add: quorem_def)
krauss@26056
   891
(*linear arithmetic*)
krauss@26056
   892
apply (blast dest: zle_zless_trans zless_trans)+
krauss@26056
   893
done
krauss@26056
   894
krauss@26056
   895
lemma zmod_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zmod b = intify(a)"
paulson@46820
   896
apply (cut_tac a = "intify (a)" and b = "intify (b)"
krauss@26056
   897
       in zmod_neg_neg_trivial_raw)
krauss@26056
   898
apply auto
krauss@26056
   899
done
krauss@26056
   900
krauss@26056
   901
lemma zmod_pos_neg_trivial_raw:
krauss@26056
   902
     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
krauss@26056
   903
apply (rule_tac q = "#-1" in quorem_mod)
krauss@26056
   904
apply (auto simp add: quorem_def)
krauss@26056
   905
(*linear arithmetic*)
krauss@26056
   906
apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
krauss@26056
   907
done
krauss@26056
   908
krauss@26056
   909
lemma zmod_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
paulson@46820
   910
apply (cut_tac a = "intify (a)" and b = "intify (b)"
krauss@26056
   911
       in zmod_pos_neg_trivial_raw)
krauss@26056
   912
apply auto
krauss@26056
   913
done
krauss@26056
   914
krauss@26056
   915
(*There is no zmod_neg_pos_trivial...*)
krauss@26056
   916
krauss@26056
   917
krauss@26056
   918
(*Simpler laws such as -a zdiv b = -(a zdiv b) FAIL*)
krauss@26056
   919
krauss@26056
   920
lemma zdiv_zminus_zminus_raw:
krauss@26056
   921
     "[|a \<in> int;  b \<in> int|] ==> ($-a) zdiv ($-b) = a zdiv b"
krauss@26056
   922
apply (case_tac "b = #0")
paulson@46820
   923
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
   924
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div])
krauss@26056
   925
apply auto
krauss@26056
   926
done
krauss@26056
   927
krauss@26056
   928
lemma zdiv_zminus_zminus [simp]: "($-a) zdiv ($-b) = a zdiv b"
krauss@26056
   929
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zminus_zminus_raw)
krauss@26056
   930
apply auto
krauss@26056
   931
done
krauss@26056
   932
krauss@26056
   933
(*Simpler laws such as -a zmod b = -(a zmod b) FAIL*)
krauss@26056
   934
lemma zmod_zminus_zminus_raw:
krauss@26056
   935
     "[|a \<in> int;  b \<in> int|] ==> ($-a) zmod ($-b) = $- (a zmod b)"
krauss@26056
   936
apply (case_tac "b = #0")
paulson@46820
   937
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
   938
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod])
krauss@26056
   939
apply auto
krauss@26056
   940
done
krauss@26056
   941
krauss@26056
   942
lemma zmod_zminus_zminus [simp]: "($-a) zmod ($-b) = $- (a zmod b)"
krauss@26056
   943
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw)
krauss@26056
   944
apply auto
krauss@26056
   945
done
krauss@26056
   946
krauss@26056
   947
krauss@26056
   948
subsection{* division of a number by itself *}
krauss@26056
   949
krauss@26056
   950
lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
krauss@26056
   951
apply (subgoal_tac "#0 $< a$*q")
krauss@26056
   952
apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
krauss@26056
   953
apply (simp add: int_0_less_mult_iff)
krauss@26056
   954
apply (blast dest: zless_trans)
krauss@26056
   955
(*linear arithmetic...*)
krauss@26056
   956
apply (drule_tac t = "%x. x $- r" in subst_context)
krauss@26056
   957
apply (drule sym)
krauss@26056
   958
apply (simp add: zcompare_rls)
krauss@26056
   959
done
krauss@26056
   960
krauss@26056
   961
lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
krauss@26056
   962
apply (subgoal_tac "#0 $<= a$* (#1$-q)")
krauss@26056
   963
 apply (simp add: int_0_le_mult_iff zcompare_rls)
krauss@26056
   964
 apply (blast dest: zle_zless_trans)
krauss@26056
   965
apply (simp add: zdiff_zmult_distrib2)
krauss@26056
   966
apply (drule_tac t = "%x. x $- a $* q" in subst_context)
krauss@26056
   967
apply (simp add: zcompare_rls)
krauss@26056
   968
done
krauss@26056
   969
krauss@26056
   970
lemma self_quotient:
krauss@26056
   971
     "[| quorem(<a,a>,<q,r>);  a \<in> int;  q \<in> int;  a \<noteq> #0|] ==> q = #1"
krauss@26056
   972
apply (simp add: split_ifs quorem_def neq_iff_zless)
krauss@26056
   973
apply (rule zle_anti_sym)
krauss@26056
   974
apply safe
krauss@26056
   975
apply auto
krauss@26056
   976
prefer 4 apply (blast dest: zless_trans)
krauss@26056
   977
apply (blast dest: zless_trans)
krauss@26056
   978
apply (rule_tac [3] a = "$-a" and r = "$-r" in self_quotient_aux1)
krauss@26056
   979
apply (rule_tac a = "$-a" and r = "$-r" in self_quotient_aux2)
krauss@26056
   980
apply (rule_tac [6] zminus_equation [THEN iffD1])
krauss@26056
   981
apply (rule_tac [2] zminus_equation [THEN iffD1])
krauss@26056
   982
apply (force intro: self_quotient_aux1 self_quotient_aux2
krauss@26056
   983
  simp add: zadd_commute zmult_zminus)+
krauss@26056
   984
done
krauss@26056
   985
krauss@26056
   986
lemma self_remainder:
krauss@26056
   987
     "[|quorem(<a,a>,<q,r>); a \<in> int; q \<in> int; r \<in> int; a \<noteq> #0|] ==> r = #0"
krauss@26056
   988
apply (frule self_quotient)
krauss@26056
   989
apply (auto simp add: quorem_def)
krauss@26056
   990
done
krauss@26056
   991
krauss@26056
   992
lemma zdiv_self_raw: "[|a \<noteq> #0; a \<in> int|] ==> a zdiv a = #1"
krauss@26056
   993
apply (blast intro: quorem_div_mod [THEN self_quotient])
krauss@26056
   994
done
krauss@26056
   995
krauss@26056
   996
lemma zdiv_self [simp]: "intify(a) \<noteq> #0 ==> a zdiv a = #1"
krauss@26056
   997
apply (drule zdiv_self_raw)
krauss@26056
   998
apply auto
krauss@26056
   999
done
krauss@26056
  1000
krauss@26056
  1001
(*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *)
krauss@26056
  1002
lemma zmod_self_raw: "a \<in> int ==> a zmod a = #0"
krauss@26056
  1003
apply (case_tac "a = #0")
paulson@46820
  1004
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1005
apply (blast intro: quorem_div_mod [THEN self_remainder])
krauss@26056
  1006
done
krauss@26056
  1007
krauss@26056
  1008
lemma zmod_self [simp]: "a zmod a = #0"
krauss@26056
  1009
apply (cut_tac a = "intify (a)" in zmod_self_raw)
krauss@26056
  1010
apply auto
krauss@26056
  1011
done
krauss@26056
  1012
krauss@26056
  1013
krauss@26056
  1014
subsection{* Computation of division and remainder *}
krauss@26056
  1015
krauss@26056
  1016
lemma zdiv_zero [simp]: "#0 zdiv b = #0"
paulson@46993
  1017
  by (simp add: zdiv_def divAlg_def)
krauss@26056
  1018
krauss@26056
  1019
lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
paulson@46993
  1020
  by (simp (no_asm_simp) add: zdiv_def divAlg_def)
krauss@26056
  1021
krauss@26056
  1022
lemma zmod_zero [simp]: "#0 zmod b = #0"
paulson@46993
  1023
  by (simp add: zmod_def divAlg_def)
krauss@26056
  1024
krauss@26056
  1025
lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
paulson@46993
  1026
  by (simp add: zdiv_def divAlg_def)
krauss@26056
  1027
krauss@26056
  1028
lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1"
paulson@46993
  1029
  by (simp add: zmod_def divAlg_def)
krauss@26056
  1030
krauss@26056
  1031
(** a positive, b positive **)
krauss@26056
  1032
paulson@46820
  1033
lemma zdiv_pos_pos: "[| #0 $< a;  #0 $<= b |]
krauss@26056
  1034
      ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))"
krauss@26056
  1035
apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
krauss@26056
  1036
apply (auto simp add: zle_def)
krauss@26056
  1037
done
krauss@26056
  1038
krauss@26056
  1039
lemma zmod_pos_pos:
paulson@46820
  1040
     "[| #0 $< a;  #0 $<= b |]
krauss@26056
  1041
      ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))"
krauss@26056
  1042
apply (simp (no_asm_simp) add: zmod_def divAlg_def)
krauss@26056
  1043
apply (auto simp add: zle_def)
krauss@26056
  1044
done
krauss@26056
  1045
krauss@26056
  1046
(** a negative, b positive **)
krauss@26056
  1047
krauss@26056
  1048
lemma zdiv_neg_pos:
paulson@46820
  1049
     "[| a $< #0;  #0 $< b |]
krauss@26056
  1050
      ==> a zdiv b = fst (negDivAlg(<intify(a), intify(b)>))"
krauss@26056
  1051
apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
krauss@26056
  1052
apply (blast dest: zle_zless_trans)
krauss@26056
  1053
done
krauss@26056
  1054
krauss@26056
  1055
lemma zmod_neg_pos:
paulson@46820
  1056
     "[| a $< #0;  #0 $< b |]
krauss@26056
  1057
      ==> a zmod b = snd (negDivAlg(<intify(a), intify(b)>))"
krauss@26056
  1058
apply (simp (no_asm_simp) add: zmod_def divAlg_def)
krauss@26056
  1059
apply (blast dest: zle_zless_trans)
krauss@26056
  1060
done
krauss@26056
  1061
krauss@26056
  1062
(** a positive, b negative **)
krauss@26056
  1063
krauss@26056
  1064
lemma zdiv_pos_neg:
paulson@46820
  1065
     "[| #0 $< a;  b $< #0 |]
krauss@26056
  1066
      ==> a zdiv b = fst (negateSnd(negDivAlg (<$-a, $-b>)))"
krauss@26056
  1067
apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle)
krauss@26056
  1068
apply auto
krauss@26056
  1069
apply (blast dest: zle_zless_trans)+
krauss@26056
  1070
apply (blast dest: zless_trans)
krauss@26056
  1071
apply (blast intro: zless_imp_zle)
krauss@26056
  1072
done
krauss@26056
  1073
krauss@26056
  1074
lemma zmod_pos_neg:
paulson@46820
  1075
     "[| #0 $< a;  b $< #0 |]
krauss@26056
  1076
      ==> a zmod b = snd (negateSnd(negDivAlg (<$-a, $-b>)))"
krauss@26056
  1077
apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle)
krauss@26056
  1078
apply auto
krauss@26056
  1079
apply (blast dest: zle_zless_trans)+
krauss@26056
  1080
apply (blast dest: zless_trans)
krauss@26056
  1081
apply (blast intro: zless_imp_zle)
krauss@26056
  1082
done
krauss@26056
  1083
krauss@26056
  1084
(** a negative, b negative **)
krauss@26056
  1085
krauss@26056
  1086
lemma zdiv_neg_neg:
paulson@46820
  1087
     "[| a $< #0;  b $<= #0 |]
krauss@26056
  1088
      ==> a zdiv b = fst (negateSnd(posDivAlg(<$-a, $-b>)))"
krauss@26056
  1089
apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
krauss@26056
  1090
apply auto
krauss@26056
  1091
apply (blast dest!: zle_zless_trans)+
krauss@26056
  1092
done
krauss@26056
  1093
krauss@26056
  1094
lemma zmod_neg_neg:
paulson@46820
  1095
     "[| a $< #0;  b $<= #0 |]
krauss@26056
  1096
      ==> a zmod b = snd (negateSnd(posDivAlg(<$-a, $-b>)))"
krauss@26056
  1097
apply (simp (no_asm_simp) add: zmod_def divAlg_def)
krauss@26056
  1098
apply auto
krauss@26056
  1099
apply (blast dest!: zle_zless_trans)+
krauss@26056
  1100
done
krauss@26056
  1101
wenzelm@45602
  1102
declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1103
declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1104
declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1105
declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1106
declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1107
declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1108
declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1109
declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1110
declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
wenzelm@45602
  1111
declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
krauss@26056
  1112
krauss@26056
  1113
krauss@26056
  1114
(** Special-case simplification **)
krauss@26056
  1115
krauss@26056
  1116
lemma zmod_1 [simp]: "a zmod #1 = #0"
krauss@26056
  1117
apply (cut_tac a = "a" and b = "#1" in pos_mod_sign)
krauss@26056
  1118
apply (cut_tac [2] a = "a" and b = "#1" in pos_mod_bound)
krauss@26056
  1119
apply auto
krauss@26056
  1120
(*arithmetic*)
krauss@26056
  1121
apply (drule add1_zle_iff [THEN iffD2])
krauss@26056
  1122
apply (rule zle_anti_sym)
krauss@26056
  1123
apply auto
krauss@26056
  1124
done
krauss@26056
  1125
krauss@26056
  1126
lemma zdiv_1 [simp]: "a zdiv #1 = intify(a)"
krauss@26056
  1127
apply (cut_tac a = "a" and b = "#1" in zmod_zdiv_equality)
krauss@26056
  1128
apply auto
krauss@26056
  1129
done
krauss@26056
  1130
krauss@26056
  1131
lemma zmod_minus1_right [simp]: "a zmod #-1 = #0"
krauss@26056
  1132
apply (cut_tac a = "a" and b = "#-1" in neg_mod_sign)
krauss@26056
  1133
apply (cut_tac [2] a = "a" and b = "#-1" in neg_mod_bound)
krauss@26056
  1134
apply auto
krauss@26056
  1135
(*arithmetic*)
krauss@26056
  1136
apply (drule add1_zle_iff [THEN iffD2])
krauss@26056
  1137
apply (rule zle_anti_sym)
krauss@26056
  1138
apply auto
krauss@26056
  1139
done
krauss@26056
  1140
krauss@26056
  1141
lemma zdiv_minus1_right_raw: "a \<in> int ==> a zdiv #-1 = $-a"
krauss@26056
  1142
apply (cut_tac a = "a" and b = "#-1" in zmod_zdiv_equality)
krauss@26056
  1143
apply auto
krauss@26056
  1144
apply (rule equation_zminus [THEN iffD2])
krauss@26056
  1145
apply auto
krauss@26056
  1146
done
krauss@26056
  1147
krauss@26056
  1148
lemma zdiv_minus1_right: "a zdiv #-1 = $-a"
krauss@26056
  1149
apply (cut_tac a = "intify (a)" in zdiv_minus1_right_raw)
krauss@26056
  1150
apply auto
krauss@26056
  1151
done
krauss@26056
  1152
declare zdiv_minus1_right [simp]
krauss@26056
  1153
krauss@26056
  1154
krauss@26056
  1155
subsection{* Monotonicity in the first argument (divisor) *}
krauss@26056
  1156
krauss@26056
  1157
lemma zdiv_mono1: "[| a $<= a';  #0 $< b |] ==> a zdiv b $<= a' zdiv b"
krauss@26056
  1158
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
krauss@26056
  1159
apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
krauss@26056
  1160
apply (rule unique_quotient_lemma)
krauss@26056
  1161
apply (erule subst)
krauss@26056
  1162
apply (erule subst)
krauss@26056
  1163
apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound)
krauss@26056
  1164
done
krauss@26056
  1165
krauss@26056
  1166
lemma zdiv_mono1_neg: "[| a $<= a';  b $< #0 |] ==> a' zdiv b $<= a zdiv b"
krauss@26056
  1167
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
krauss@26056
  1168
apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
krauss@26056
  1169
apply (rule unique_quotient_lemma_neg)
krauss@26056
  1170
apply (erule subst)
krauss@26056
  1171
apply (erule subst)
krauss@26056
  1172
apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound)
krauss@26056
  1173
done
krauss@26056
  1174
krauss@26056
  1175
krauss@26056
  1176
subsection{* Monotonicity in the second argument (dividend) *}
krauss@26056
  1177
krauss@26056
  1178
lemma q_pos_lemma:
krauss@26056
  1179
     "[| #0 $<= b'$*q' $+ r'; r' $< b';  #0 $< b' |] ==> #0 $<= q'"
krauss@26056
  1180
apply (subgoal_tac "#0 $< b'$* (q' $+ #1)")
krauss@26056
  1181
 apply (simp add: int_0_less_mult_iff)
krauss@26056
  1182
 apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1])
krauss@26056
  1183
apply (simp add: zadd_zmult_distrib2)
krauss@26056
  1184
apply (erule zle_zless_trans)
krauss@26056
  1185
apply (erule zadd_zless_mono2)
krauss@26056
  1186
done
krauss@26056
  1187
krauss@26056
  1188
lemma zdiv_mono2_lemma:
paulson@46820
  1189
     "[| b$*q $+ r = b'$*q' $+ r';  #0 $<= b'$*q' $+ r';
paulson@46820
  1190
         r' $< b';  #0 $<= r;  #0 $< b';  b' $<= b |]
krauss@26056
  1191
      ==> q $<= q'"
paulson@46820
  1192
apply (frule q_pos_lemma, assumption+)
krauss@26056
  1193
apply (subgoal_tac "b$*q $< b$* (q' $+ #1)")
krauss@26056
  1194
 apply (simp add: zmult_zless_cancel1)
krauss@26056
  1195
 apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans)
krauss@26056
  1196
apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'")
krauss@26056
  1197
 prefer 2 apply (simp add: zcompare_rls)
krauss@26056
  1198
apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
krauss@26056
  1199
apply (subst zadd_commute [of "b $\<times> q'"], rule zadd_zless_mono)
krauss@26056
  1200
 prefer 2 apply (blast intro: zmult_zle_mono1)
krauss@26056
  1201
apply (subgoal_tac "r' $+ #0 $< b $+ r")
krauss@26056
  1202
 apply (simp add: zcompare_rls)
krauss@26056
  1203
apply (rule zadd_zless_mono)
krauss@26056
  1204
 apply auto
krauss@26056
  1205
apply (blast dest: zless_zle_trans)
krauss@26056
  1206
done
krauss@26056
  1207
krauss@26056
  1208
krauss@26056
  1209
lemma zdiv_mono2_raw:
paulson@46820
  1210
     "[| #0 $<= a;  #0 $< b';  b' $<= b;  a \<in> int |]
krauss@26056
  1211
      ==> a zdiv b $<= a zdiv b'"
krauss@26056
  1212
apply (subgoal_tac "#0 $< b")
krauss@26056
  1213
 prefer 2 apply (blast dest: zless_zle_trans)
krauss@26056
  1214
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
krauss@26056
  1215
apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
krauss@26056
  1216
apply (rule zdiv_mono2_lemma)
krauss@26056
  1217
apply (erule subst)
krauss@26056
  1218
apply (erule subst)
krauss@26056
  1219
apply (simp_all add: pos_mod_sign pos_mod_bound)
krauss@26056
  1220
done
krauss@26056
  1221
krauss@26056
  1222
lemma zdiv_mono2:
paulson@46820
  1223
     "[| #0 $<= a;  #0 $< b';  b' $<= b |]
krauss@26056
  1224
      ==> a zdiv b $<= a zdiv b'"
krauss@26056
  1225
apply (cut_tac a = "intify (a)" in zdiv_mono2_raw)
krauss@26056
  1226
apply auto
krauss@26056
  1227
done
krauss@26056
  1228
krauss@26056
  1229
lemma q_neg_lemma:
krauss@26056
  1230
     "[| b'$*q' $+ r' $< #0;  #0 $<= r';  #0 $< b' |] ==> q' $< #0"
krauss@26056
  1231
apply (subgoal_tac "b'$*q' $< #0")
krauss@26056
  1232
 prefer 2 apply (force intro: zle_zless_trans)
krauss@26056
  1233
apply (simp add: zmult_less_0_iff)
krauss@26056
  1234
apply (blast dest: zless_trans)
krauss@26056
  1235
done
krauss@26056
  1236
krauss@26056
  1237
krauss@26056
  1238
krauss@26056
  1239
lemma zdiv_mono2_neg_lemma:
paulson@46820
  1240
     "[| b$*q $+ r = b'$*q' $+ r';  b'$*q' $+ r' $< #0;
paulson@46820
  1241
         r $< b;  #0 $<= r';  #0 $< b';  b' $<= b |]
krauss@26056
  1242
      ==> q' $<= q"
krauss@26056
  1243
apply (subgoal_tac "#0 $< b")
krauss@26056
  1244
 prefer 2 apply (blast dest: zless_zle_trans)
paulson@46820
  1245
apply (frule q_neg_lemma, assumption+)
krauss@26056
  1246
apply (subgoal_tac "b$*q' $< b$* (q $+ #1)")
krauss@26056
  1247
 apply (simp add: zmult_zless_cancel1)
krauss@26056
  1248
 apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
krauss@26056
  1249
apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
krauss@26056
  1250
apply (subgoal_tac "b$*q' $<= b'$*q'")
krauss@26056
  1251
 prefer 2
krauss@26056
  1252
 apply (simp add: zmult_zle_cancel2)
krauss@26056
  1253
 apply (blast dest: zless_trans)
krauss@26056
  1254
apply (subgoal_tac "b'$*q' $+ r $< b $+ (b$*q $+ r)")
krauss@26056
  1255
 prefer 2
krauss@26056
  1256
 apply (erule ssubst)
krauss@26056
  1257
 apply simp
krauss@26056
  1258
 apply (drule_tac w' = "r" and z' = "#0" in zadd_zless_mono)
krauss@26056
  1259
  apply (assumption)
krauss@26056
  1260
 apply simp
krauss@26056
  1261
apply (simp (no_asm_use) add: zadd_commute)
krauss@26056
  1262
apply (rule zle_zless_trans)
krauss@26056
  1263
 prefer 2 apply (assumption)
krauss@26056
  1264
apply (simp (no_asm_simp) add: zmult_zle_cancel2)
krauss@26056
  1265
apply (blast dest: zless_trans)
krauss@26056
  1266
done
krauss@26056
  1267
krauss@26056
  1268
lemma zdiv_mono2_neg_raw:
paulson@46820
  1269
     "[| a $< #0;  #0 $< b';  b' $<= b;  a \<in> int |]
krauss@26056
  1270
      ==> a zdiv b' $<= a zdiv b"
krauss@26056
  1271
apply (subgoal_tac "#0 $< b")
krauss@26056
  1272
 prefer 2 apply (blast dest: zless_zle_trans)
krauss@26056
  1273
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
krauss@26056
  1274
apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
krauss@26056
  1275
apply (rule zdiv_mono2_neg_lemma)
krauss@26056
  1276
apply (erule subst)
krauss@26056
  1277
apply (erule subst)
krauss@26056
  1278
apply (simp_all add: pos_mod_sign pos_mod_bound)
krauss@26056
  1279
done
krauss@26056
  1280
paulson@46820
  1281
lemma zdiv_mono2_neg: "[| a $< #0;  #0 $< b';  b' $<= b |]
krauss@26056
  1282
      ==> a zdiv b' $<= a zdiv b"
krauss@26056
  1283
apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw)
krauss@26056
  1284
apply auto
krauss@26056
  1285
done
krauss@26056
  1286
krauss@26056
  1287
krauss@26056
  1288
krauss@26056
  1289
subsection{* More algebraic laws for zdiv and zmod *}
krauss@26056
  1290
krauss@26056
  1291
(** proving (a*b) zdiv c = a $* (b zdiv c) $+ a * (b zmod c) **)
krauss@26056
  1292
krauss@26056
  1293
lemma zmult1_lemma:
paulson@46820
  1294
     "[| quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0 |]
krauss@26056
  1295
      ==> quorem (<a$*b, c>, <a$*q $+ (a$*r) zdiv c, (a$*r) zmod c>)"
krauss@26056
  1296
apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
krauss@26056
  1297
                      pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
paulson@46820
  1298
apply (auto intro: raw_zmod_zdiv_equality)
krauss@26056
  1299
done
krauss@26056
  1300
krauss@26056
  1301
lemma zdiv_zmult1_eq_raw:
paulson@46820
  1302
     "[|b \<in> int;  c \<in> int|]
krauss@26056
  1303
      ==> (a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
krauss@26056
  1304
apply (case_tac "c = #0")
paulson@46820
  1305
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1306
apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
krauss@26056
  1307
apply auto
krauss@26056
  1308
done
krauss@26056
  1309
krauss@26056
  1310
lemma zdiv_zmult1_eq: "(a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
krauss@26056
  1311
apply (cut_tac b = "intify (b)" and c = "intify (c)" in zdiv_zmult1_eq_raw)
krauss@26056
  1312
apply auto
krauss@26056
  1313
done
krauss@26056
  1314
krauss@26056
  1315
lemma zmod_zmult1_eq_raw:
krauss@26056
  1316
     "[|b \<in> int;  c \<in> int|] ==> (a$*b) zmod c = a$*(b zmod c) zmod c"
krauss@26056
  1317
apply (case_tac "c = #0")
paulson@46820
  1318
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1319
apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
krauss@26056
  1320
apply auto
krauss@26056
  1321
done
krauss@26056
  1322
krauss@26056
  1323
lemma zmod_zmult1_eq: "(a$*b) zmod c = a$*(b zmod c) zmod c"
krauss@26056
  1324
apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult1_eq_raw)
krauss@26056
  1325
apply auto
krauss@26056
  1326
done
krauss@26056
  1327
krauss@26056
  1328
lemma zmod_zmult1_eq': "(a$*b) zmod c = ((a zmod c) $* b) zmod c"
krauss@26056
  1329
apply (rule trans)
krauss@26056
  1330
apply (rule_tac b = " (b $* a) zmod c" in trans)
krauss@26056
  1331
apply (rule_tac [2] zmod_zmult1_eq)
krauss@26056
  1332
apply (simp_all (no_asm) add: zmult_commute)
krauss@26056
  1333
done
krauss@26056
  1334
krauss@26056
  1335
lemma zmod_zmult_distrib: "(a$*b) zmod c = ((a zmod c) $* (b zmod c)) zmod c"
krauss@26056
  1336
apply (rule zmod_zmult1_eq' [THEN trans])
krauss@26056
  1337
apply (rule zmod_zmult1_eq)
krauss@26056
  1338
done
krauss@26056
  1339
krauss@26056
  1340
lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a$*b) zdiv b = intify(a)"
paulson@46993
  1341
  by (simp add: zdiv_zmult1_eq)
krauss@26056
  1342
krauss@26056
  1343
lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b$*a) zdiv b = intify(a)"
paulson@46993
  1344
  by (simp add: zmult_commute) 
krauss@26056
  1345
krauss@26056
  1346
lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0"
paulson@46993
  1347
  by (simp add: zmod_zmult1_eq)
krauss@26056
  1348
krauss@26056
  1349
lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0"
paulson@46993
  1350
  by (simp add: zmult_commute zmod_zmult1_eq)
krauss@26056
  1351
krauss@26056
  1352
paulson@46820
  1353
(** proving (a$+b) zdiv c =
krauss@26056
  1354
            a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **)
krauss@26056
  1355
krauss@26056
  1356
lemma zadd1_lemma:
paulson@46820
  1357
     "[| quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);
paulson@46820
  1358
         c \<in> int;  c \<noteq> #0 |]
krauss@26056
  1359
      ==> quorem (<a$+b, c>, <aq $+ bq $+ (ar$+br) zdiv c, (ar$+br) zmod c>)"
krauss@26056
  1360
apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
krauss@26056
  1361
                      pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
krauss@26056
  1362
apply (auto intro: raw_zmod_zdiv_equality)
krauss@26056
  1363
done
krauss@26056
  1364
krauss@26056
  1365
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
krauss@26056
  1366
lemma zdiv_zadd1_eq_raw:
paulson@46820
  1367
     "[|a \<in> int; b \<in> int; c \<in> int|] ==>
krauss@26056
  1368
      (a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
krauss@26056
  1369
apply (case_tac "c = #0")
paulson@46820
  1370
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1371
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
krauss@26056
  1372
                                 THEN quorem_div])
krauss@26056
  1373
done
krauss@26056
  1374
krauss@26056
  1375
lemma zdiv_zadd1_eq:
krauss@26056
  1376
     "(a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
paulson@46820
  1377
apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
krauss@26056
  1378
       in zdiv_zadd1_eq_raw)
krauss@26056
  1379
apply auto
krauss@26056
  1380
done
krauss@26056
  1381
krauss@26056
  1382
lemma zmod_zadd1_eq_raw:
paulson@46820
  1383
     "[|a \<in> int; b \<in> int; c \<in> int|]
krauss@26056
  1384
      ==> (a$+b) zmod c = (a zmod c $+ b zmod c) zmod c"
krauss@26056
  1385
apply (case_tac "c = #0")
paulson@46820
  1386
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
paulson@46820
  1387
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
krauss@26056
  1388
                                 THEN quorem_mod])
krauss@26056
  1389
done
krauss@26056
  1390
krauss@26056
  1391
lemma zmod_zadd1_eq: "(a$+b) zmod c = (a zmod c $+ b zmod c) zmod c"
paulson@46820
  1392
apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
krauss@26056
  1393
       in zmod_zadd1_eq_raw)
krauss@26056
  1394
apply auto
krauss@26056
  1395
done
krauss@26056
  1396
krauss@26056
  1397
lemma zmod_div_trivial_raw:
krauss@26056
  1398
     "[|a \<in> int; b \<in> int|] ==> (a zmod b) zdiv b = #0"
krauss@26056
  1399
apply (case_tac "b = #0")
paulson@46820
  1400
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1401
apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
krauss@26056
  1402
         zdiv_pos_pos_trivial neg_mod_sign neg_mod_bound zdiv_neg_neg_trivial)
krauss@26056
  1403
done
krauss@26056
  1404
krauss@26056
  1405
lemma zmod_div_trivial [simp]: "(a zmod b) zdiv b = #0"
krauss@26056
  1406
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_div_trivial_raw)
krauss@26056
  1407
apply auto
krauss@26056
  1408
done
krauss@26056
  1409
krauss@26056
  1410
lemma zmod_mod_trivial_raw:
krauss@26056
  1411
     "[|a \<in> int; b \<in> int|] ==> (a zmod b) zmod b = a zmod b"
krauss@26056
  1412
apply (case_tac "b = #0")
paulson@46820
  1413
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
paulson@46820
  1414
apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
krauss@26056
  1415
       zmod_pos_pos_trivial neg_mod_sign neg_mod_bound zmod_neg_neg_trivial)
krauss@26056
  1416
done
krauss@26056
  1417
krauss@26056
  1418
lemma zmod_mod_trivial [simp]: "(a zmod b) zmod b = a zmod b"
krauss@26056
  1419
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_mod_trivial_raw)
krauss@26056
  1420
apply auto
krauss@26056
  1421
done
krauss@26056
  1422
krauss@26056
  1423
lemma zmod_zadd_left_eq: "(a$+b) zmod c = ((a zmod c) $+ b) zmod c"
krauss@26056
  1424
apply (rule trans [symmetric])
krauss@26056
  1425
apply (rule zmod_zadd1_eq)
krauss@26056
  1426
apply (simp (no_asm))
krauss@26056
  1427
apply (rule zmod_zadd1_eq [symmetric])
krauss@26056
  1428
done
krauss@26056
  1429
krauss@26056
  1430
lemma zmod_zadd_right_eq: "(a$+b) zmod c = (a $+ (b zmod c)) zmod c"
krauss@26056
  1431
apply (rule trans [symmetric])
krauss@26056
  1432
apply (rule zmod_zadd1_eq)
krauss@26056
  1433
apply (simp (no_asm))
krauss@26056
  1434
apply (rule zmod_zadd1_eq [symmetric])
krauss@26056
  1435
done
krauss@26056
  1436
krauss@26056
  1437
krauss@26056
  1438
lemma zdiv_zadd_self1 [simp]:
krauss@26056
  1439
     "intify(a) \<noteq> #0 ==> (a$+b) zdiv a = b zdiv a $+ #1"
krauss@26056
  1440
by (simp (no_asm_simp) add: zdiv_zadd1_eq)
krauss@26056
  1441
krauss@26056
  1442
lemma zdiv_zadd_self2 [simp]:
krauss@26056
  1443
     "intify(a) \<noteq> #0 ==> (b$+a) zdiv a = b zdiv a $+ #1"
krauss@26056
  1444
by (simp (no_asm_simp) add: zdiv_zadd1_eq)
krauss@26056
  1445
krauss@26056
  1446
lemma zmod_zadd_self1 [simp]: "(a$+b) zmod a = b zmod a"
krauss@26056
  1447
apply (case_tac "a = #0")
paulson@46820
  1448
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1449
apply (simp (no_asm_simp) add: zmod_zadd1_eq)
krauss@26056
  1450
done
krauss@26056
  1451
krauss@26056
  1452
lemma zmod_zadd_self2 [simp]: "(b$+a) zmod a = b zmod a"
krauss@26056
  1453
apply (case_tac "a = #0")
paulson@46820
  1454
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1455
apply (simp (no_asm_simp) add: zmod_zadd1_eq)
krauss@26056
  1456
done
krauss@26056
  1457
krauss@26056
  1458
krauss@26056
  1459
subsection{* proving  a zdiv (b*c) = (a zdiv b) zdiv c *}
krauss@26056
  1460
krauss@26056
  1461
(*The condition c>0 seems necessary.  Consider that 7 zdiv ~6 = ~2 but
krauss@26056
  1462
  7 zdiv 2 zdiv ~3 = 3 zdiv ~3 = ~1.  The subcase (a zdiv b) zmod c = 0 seems
krauss@26056
  1463
  to cause particular problems.*)
krauss@26056
  1464
krauss@26056
  1465
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
krauss@26056
  1466
krauss@26056
  1467
lemma zdiv_zmult2_aux1:
krauss@26056
  1468
     "[| #0 $< c;  b $< r;  r $<= #0 |] ==> b$*c $< b$*(q zmod c) $+ r"
krauss@26056
  1469
apply (subgoal_tac "b $* (c $- q zmod c) $< r $* #1")
krauss@26056
  1470
apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
krauss@26056
  1471
apply (rule zle_zless_trans)
krauss@26056
  1472
apply (erule_tac [2] zmult_zless_mono1)
krauss@26056
  1473
apply (rule zmult_zle_mono2_neg)
krauss@26056
  1474
apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
krauss@26056
  1475
apply (blast intro: zless_imp_zle dest: zless_zle_trans)
krauss@26056
  1476
done
krauss@26056
  1477
krauss@26056
  1478
lemma zdiv_zmult2_aux2:
krauss@26056
  1479
     "[| #0 $< c;   b $< r;  r $<= #0 |] ==> b $* (q zmod c) $+ r $<= #0"
krauss@26056
  1480
apply (subgoal_tac "b $* (q zmod c) $<= #0")
krauss@26056
  1481
 prefer 2
paulson@46820
  1482
 apply (simp add: zmult_le_0_iff pos_mod_sign)
krauss@26056
  1483
 apply (blast intro: zless_imp_zle dest: zless_zle_trans)
krauss@26056
  1484
(*arithmetic*)
krauss@26056
  1485
apply (drule zadd_zle_mono)
krauss@26056
  1486
apply assumption
krauss@26056
  1487
apply (simp add: zadd_commute)
krauss@26056
  1488
done
krauss@26056
  1489
krauss@26056
  1490
lemma zdiv_zmult2_aux3:
krauss@26056
  1491
     "[| #0 $< c;  #0 $<= r;  r $< b |] ==> #0 $<= b $* (q zmod c) $+ r"
krauss@26056
  1492
apply (subgoal_tac "#0 $<= b $* (q zmod c)")
krauss@26056
  1493
 prefer 2
paulson@46820
  1494
 apply (simp add: int_0_le_mult_iff pos_mod_sign)
krauss@26056
  1495
 apply (blast intro: zless_imp_zle dest: zle_zless_trans)
krauss@26056
  1496
(*arithmetic*)
krauss@26056
  1497
apply (drule zadd_zle_mono)
krauss@26056
  1498
apply assumption
krauss@26056
  1499
apply (simp add: zadd_commute)
krauss@26056
  1500
done
krauss@26056
  1501
krauss@26056
  1502
lemma zdiv_zmult2_aux4:
krauss@26056
  1503
     "[| #0 $< c; #0 $<= r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c"
krauss@26056
  1504
apply (subgoal_tac "r $* #1 $< b $* (c $- q zmod c)")
krauss@26056
  1505
apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
krauss@26056
  1506
apply (rule zless_zle_trans)
krauss@26056
  1507
apply (erule zmult_zless_mono1)
krauss@26056
  1508
apply (rule_tac [2] zmult_zle_mono2)
krauss@26056
  1509
apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
krauss@26056
  1510
apply (blast intro: zless_imp_zle dest: zle_zless_trans)
krauss@26056
  1511
done
krauss@26056
  1512
krauss@26056
  1513
lemma zdiv_zmult2_lemma:
paulson@46820
  1514
     "[| quorem (<a,b>, <q,r>);  a \<in> int;  b \<in> int;  b \<noteq> #0;  #0 $< c |]
krauss@26056
  1515
      ==> quorem (<a,b$*c>, <q zdiv c, b$*(q zmod c) $+ r>)"
krauss@26056
  1516
apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
paulson@46820
  1517
               neq_iff_zless int_0_less_mult_iff
krauss@26056
  1518
               zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2
krauss@26056
  1519
               zdiv_zmult2_aux3 zdiv_zmult2_aux4)
krauss@26056
  1520
apply (blast dest: zless_trans)+
krauss@26056
  1521
done
krauss@26056
  1522
krauss@26056
  1523
lemma zdiv_zmult2_eq_raw:
krauss@26056
  1524
     "[|#0 $< c;  a \<in> int;  b \<in> int|] ==> a zdiv (b$*c) = (a zdiv b) zdiv c"
krauss@26056
  1525
apply (case_tac "b = #0")
paulson@46820
  1526
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1527
apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_div])
krauss@26056
  1528
apply (auto simp add: intify_eq_0_iff_zle)
krauss@26056
  1529
apply (blast dest: zle_zless_trans)
krauss@26056
  1530
done
krauss@26056
  1531
krauss@26056
  1532
lemma zdiv_zmult2_eq: "#0 $< c ==> a zdiv (b$*c) = (a zdiv b) zdiv c"
krauss@26056
  1533
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zmult2_eq_raw)
krauss@26056
  1534
apply auto
krauss@26056
  1535
done
krauss@26056
  1536
krauss@26056
  1537
lemma zmod_zmult2_eq_raw:
paulson@46820
  1538
     "[|#0 $< c;  a \<in> int;  b \<in> int|]
krauss@26056
  1539
      ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b"
krauss@26056
  1540
apply (case_tac "b = #0")
paulson@46820
  1541
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1542
apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_mod])
krauss@26056
  1543
apply (auto simp add: intify_eq_0_iff_zle)
krauss@26056
  1544
apply (blast dest: zle_zless_trans)
krauss@26056
  1545
done
krauss@26056
  1546
krauss@26056
  1547
lemma zmod_zmult2_eq:
krauss@26056
  1548
     "#0 $< c ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b"
krauss@26056
  1549
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zmult2_eq_raw)
krauss@26056
  1550
apply auto
krauss@26056
  1551
done
krauss@26056
  1552
krauss@26056
  1553
subsection{* Cancellation of common factors in "zdiv" *}
krauss@26056
  1554
krauss@26056
  1555
lemma zdiv_zmult_zmult1_aux1:
krauss@26056
  1556
     "[| #0 $< b;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
krauss@26056
  1557
apply (subst zdiv_zmult2_eq)
krauss@26056
  1558
apply auto
krauss@26056
  1559
done
krauss@26056
  1560
krauss@26056
  1561
lemma zdiv_zmult_zmult1_aux2:
krauss@26056
  1562
     "[| b $< #0;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
krauss@26056
  1563
apply (subgoal_tac " (c $* ($-a)) zdiv (c $* ($-b)) = ($-a) zdiv ($-b)")
krauss@26056
  1564
apply (rule_tac [2] zdiv_zmult_zmult1_aux1)
krauss@26056
  1565
apply auto
krauss@26056
  1566
done
krauss@26056
  1567
krauss@26056
  1568
lemma zdiv_zmult_zmult1_raw:
krauss@26056
  1569
     "[|intify(c) \<noteq> #0; b \<in> int|] ==> (c$*a) zdiv (c$*b) = a zdiv b"
krauss@26056
  1570
apply (case_tac "b = #0")
paulson@46820
  1571
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1572
apply (auto simp add: neq_iff_zless [of b]
krauss@26056
  1573
  zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
krauss@26056
  1574
done
krauss@26056
  1575
krauss@26056
  1576
lemma zdiv_zmult_zmult1: "intify(c) \<noteq> #0 ==> (c$*a) zdiv (c$*b) = a zdiv b"
krauss@26056
  1577
apply (cut_tac b = "intify (b)" in zdiv_zmult_zmult1_raw)
krauss@26056
  1578
apply auto
krauss@26056
  1579
done
krauss@26056
  1580
krauss@26056
  1581
lemma zdiv_zmult_zmult2: "intify(c) \<noteq> #0 ==> (a$*c) zdiv (b$*c) = a zdiv b"
krauss@26056
  1582
apply (drule zdiv_zmult_zmult1)
krauss@26056
  1583
apply (auto simp add: zmult_commute)
krauss@26056
  1584
done
krauss@26056
  1585
krauss@26056
  1586
krauss@26056
  1587
subsection{* Distribution of factors over "zmod" *}
krauss@26056
  1588
krauss@26056
  1589
lemma zmod_zmult_zmult1_aux1:
paulson@46820
  1590
     "[| #0 $< b;  intify(c) \<noteq> #0 |]
krauss@26056
  1591
      ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
krauss@26056
  1592
apply (subst zmod_zmult2_eq)
krauss@26056
  1593
apply auto
krauss@26056
  1594
done
krauss@26056
  1595
krauss@26056
  1596
lemma zmod_zmult_zmult1_aux2:
paulson@46820
  1597
     "[| b $< #0;  intify(c) \<noteq> #0 |]
krauss@26056
  1598
      ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
krauss@26056
  1599
apply (subgoal_tac " (c $* ($-a)) zmod (c $* ($-b)) = c $* (($-a) zmod ($-b))")
krauss@26056
  1600
apply (rule_tac [2] zmod_zmult_zmult1_aux1)
krauss@26056
  1601
apply auto
krauss@26056
  1602
done
krauss@26056
  1603
krauss@26056
  1604
lemma zmod_zmult_zmult1_raw:
krauss@26056
  1605
     "[|b \<in> int; c \<in> int|] ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
krauss@26056
  1606
apply (case_tac "b = #0")
paulson@46820
  1607
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1608
apply (case_tac "c = #0")
paulson@46820
  1609
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
krauss@26056
  1610
apply (auto simp add: neq_iff_zless [of b]
krauss@26056
  1611
  zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
krauss@26056
  1612
done
krauss@26056
  1613
krauss@26056
  1614
lemma zmod_zmult_zmult1: "(c$*a) zmod (c$*b) = c $* (a zmod b)"
krauss@26056
  1615
apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult_zmult1_raw)
krauss@26056
  1616
apply auto
krauss@26056
  1617
done
krauss@26056
  1618
krauss@26056
  1619
lemma zmod_zmult_zmult2: "(a$*c) zmod (b$*c) = (a zmod b) $* c"
krauss@26056
  1620
apply (cut_tac c = "c" in zmod_zmult_zmult1)
krauss@26056
  1621
apply (auto simp add: zmult_commute)
krauss@26056
  1622
done
krauss@26056
  1623
krauss@26056
  1624
krauss@26056
  1625
(** Quotients of signs **)
krauss@26056
  1626
krauss@26056
  1627
lemma zdiv_neg_pos_less0: "[| a $< #0;  #0 $< b |] ==> a zdiv b $< #0"
krauss@26056
  1628
apply (subgoal_tac "a zdiv b $<= #-1")
krauss@26056
  1629
apply (erule zle_zless_trans)
krauss@26056
  1630
apply (simp (no_asm))
krauss@26056
  1631
apply (rule zle_trans)
krauss@26056
  1632
apply (rule_tac a' = "#-1" in zdiv_mono1)
krauss@26056
  1633
apply (rule zless_add1_iff_zle [THEN iffD1])
krauss@26056
  1634
apply (simp (no_asm))
krauss@26056
  1635
apply (auto simp add: zdiv_minus1)
krauss@26056
  1636
done
krauss@26056
  1637
krauss@26056
  1638
lemma zdiv_nonneg_neg_le0: "[| #0 $<= a;  b $< #0 |] ==> a zdiv b $<= #0"
krauss@26056
  1639
apply (drule zdiv_mono1_neg)
krauss@26056
  1640
apply auto
krauss@26056
  1641
done
krauss@26056
  1642
paulson@46821
  1643
lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) \<longleftrightarrow> (#0 $<= a)"
krauss@26056
  1644
apply auto
krauss@26056
  1645
apply (drule_tac [2] zdiv_mono1)
krauss@26056
  1646
apply (auto simp add: neq_iff_zless)
krauss@26056
  1647
apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym])
krauss@26056
  1648
apply (blast intro: zdiv_neg_pos_less0)
krauss@26056
  1649
done
krauss@26056
  1650
paulson@46821
  1651
lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) \<longleftrightarrow> (a $<= #0)"
krauss@26056
  1652
apply (subst zdiv_zminus_zminus [symmetric])
krauss@26056
  1653
apply (rule iff_trans)
krauss@26056
  1654
apply (rule pos_imp_zdiv_nonneg_iff)
krauss@26056
  1655
apply auto
krauss@26056
  1656
done
krauss@26056
  1657
krauss@26056
  1658
(*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*)
paulson@46821
  1659
lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) \<longleftrightarrow> (a $< #0)"
krauss@26056
  1660
apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
krauss@26056
  1661
apply (erule pos_imp_zdiv_nonneg_iff)
krauss@26056
  1662
done
krauss@26056
  1663
krauss@26056
  1664
(*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*)
paulson@46821
  1665
lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) \<longleftrightarrow> (#0 $< a)"
krauss@26056
  1666
apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
krauss@26056
  1667
apply (erule neg_imp_zdiv_nonneg_iff)
krauss@26056
  1668
done
krauss@26056
  1669
krauss@26056
  1670
(*
krauss@26056
  1671
 THESE REMAIN TO BE CONVERTED -- but aren't that useful!
krauss@26056
  1672
krauss@26056
  1673
 subsection{* Speeding up the division algorithm with shifting *}
krauss@26056
  1674
krauss@26056
  1675
 (** computing "zdiv" by shifting **)
krauss@26056
  1676
krauss@26056
  1677
 lemma pos_zdiv_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zdiv (#2$*a) = b zdiv a"
krauss@26056
  1678
 apply (case_tac "a = #0")
krauss@26056
  1679
 apply (subgoal_tac "#1 $<= a")
krauss@26056
  1680
  apply (arith_tac 2)
krauss@26056
  1681
 apply (subgoal_tac "#1 $< a $* #2")
krauss@26056
  1682
  apply (arith_tac 2)
krauss@26056
  1683
 apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
krauss@26056
  1684
  apply (rule_tac [2] zmult_zle_mono2)
krauss@26056
  1685
 apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
krauss@26056
  1686
 apply (subst zdiv_zadd1_eq)
krauss@26056
  1687
 apply (simp (no_asm_simp) add: zdiv_zmult_zmult2 zmod_zmult_zmult2 zdiv_pos_pos_trivial)
krauss@26056
  1688
 apply (subst zdiv_pos_pos_trivial)
krauss@26056
  1689
 apply (simp (no_asm_simp) add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
krauss@26056
  1690
 apply (auto simp add: zmod_pos_pos_trivial)
krauss@26056
  1691
 apply (subgoal_tac "#0 $<= b zmod a")
krauss@26056
  1692
  apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
krauss@26056
  1693
 apply arith
krauss@26056
  1694
 done
krauss@26056
  1695
krauss@26056
  1696
paulson@46821
  1697
 lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) \<longleftrightarrow> (b$+#1) zdiv a"
paulson@46821
  1698
 apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) \<longleftrightarrow> ($-b-#1) zdiv ($-a)")
krauss@26056
  1699
 apply (rule_tac [2] pos_zdiv_mult_2)
krauss@26056
  1700
 apply (auto simp add: zmult_zminus_right)
krauss@26056
  1701
 apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
krauss@26056
  1702
 apply (Simp_tac 2)
krauss@26056
  1703
 apply (asm_full_simp_tac (HOL_ss add: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
krauss@26056
  1704
 done
krauss@26056
  1705
krauss@26056
  1706
krauss@26056
  1707
 (*Not clear why this must be proved separately; probably integ_of causes
krauss@26056
  1708
   simplification problems*)
krauss@26056
  1709
 lemma lemma: "~ #0 $<= x ==> x $<= #0"
krauss@26056
  1710
 apply auto
krauss@26056
  1711
 done
krauss@26056
  1712
paulson@46820
  1713
 lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) =
paulson@46820
  1714
           (if ~b | #0 $<= integ_of w
paulson@46820
  1715
            then integ_of v zdiv (integ_of w)
krauss@26056
  1716
            else (integ_of v $+ #1) zdiv (integ_of w))"
wenzelm@51686
  1717
 apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT)
krauss@26056
  1718
 apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2)
krauss@26056
  1719
 done
krauss@26056
  1720
krauss@26056
  1721
 declare zdiv_integ_of_BIT [simp]
krauss@26056
  1722
krauss@26056
  1723
krauss@26056
  1724
 (** computing "zmod" by shifting (proofs resemble those for "zdiv") **)
krauss@26056
  1725
krauss@26056
  1726
 lemma pos_zmod_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zmod (#2$*a) = #1 $+ #2 $* (b zmod a)"
krauss@26056
  1727
 apply (case_tac "a = #0")
krauss@26056
  1728
 apply (subgoal_tac "#1 $<= a")
krauss@26056
  1729
  apply (arith_tac 2)
krauss@26056
  1730
 apply (subgoal_tac "#1 $< a $* #2")
krauss@26056
  1731
  apply (arith_tac 2)
krauss@26056
  1732
 apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
krauss@26056
  1733
  apply (rule_tac [2] zmult_zle_mono2)
krauss@26056
  1734
 apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
krauss@26056
  1735
 apply (subst zmod_zadd1_eq)
krauss@26056
  1736
 apply (simp (no_asm_simp) add: zmod_zmult_zmult2 zmod_pos_pos_trivial)
krauss@26056
  1737
 apply (rule zmod_pos_pos_trivial)
krauss@26056
  1738
 apply (simp (no_asm_simp) # add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
krauss@26056
  1739
 apply (auto simp add: zmod_pos_pos_trivial)
krauss@26056
  1740
 apply (subgoal_tac "#0 $<= b zmod a")
krauss@26056
  1741
  apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
krauss@26056
  1742
 apply arith
krauss@26056
  1743
 done
krauss@26056
  1744
krauss@26056
  1745
krauss@26056
  1746
 lemma neg_zmod_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zmod (#2$*a) = #2 $* ((b$+#1) zmod a) - #1"
krauss@26056
  1747
 apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zmod (#2$* ($-a)) = #1 $+ #2$* (($-b-#1) zmod ($-a))")
krauss@26056
  1748
 apply (rule_tac [2] pos_zmod_mult_2)
krauss@26056
  1749
 apply (auto simp add: zmult_zminus_right)
krauss@26056
  1750
 apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
krauss@26056
  1751
 apply (Simp_tac 2)
krauss@26056
  1752
 apply (asm_full_simp_tac (HOL_ss add: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
krauss@26056
  1753
 apply (dtac (zminus_equation [THEN iffD1, symmetric])
krauss@26056
  1754
 apply auto
krauss@26056
  1755
 done
krauss@26056
  1756
paulson@46820
  1757
 lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) =
paulson@46820
  1758
           (if b then
paulson@46820
  1759
                 if #0 $<= integ_of w
paulson@46820
  1760
                 then #2 $* (integ_of v zmod integ_of w) $+ #1
paulson@46820
  1761
                 else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1
krauss@26056
  1762
            else #2 $* (integ_of v zmod integ_of w))"
wenzelm@51686
  1763
 apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT)
krauss@26056
  1764
 apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2)
krauss@26056
  1765
 done
krauss@26056
  1766
krauss@26056
  1767
 declare zmod_integ_of_BIT [simp]
krauss@26056
  1768
*)
krauss@26056
  1769
krauss@26056
  1770
end
krauss@26056
  1771