src/ZF/IntDiv_ZF.thy
 changeset 46820 c656222c4dc1 parent 45602 2a858377c3d2 child 46821 ff6b0c1087f2
```     1.1 --- a/src/ZF/IntDiv_ZF.thy	Sun Mar 04 23:20:43 2012 +0100
1.2 +++ b/src/ZF/IntDiv_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
1.3 @@ -18,11 +18,11 @@
1.4
1.5      fun negateSnd (q,r:int) = (q,~r);
1.6
1.7 -    fun divAlg (a,b) = if 0<=a then
1.8 -                          if b>0 then posDivAlg (a,b)
1.9 +    fun divAlg (a,b) = if 0<=a then
1.10 +                          if b>0 then posDivAlg (a,b)
1.11                             else if a=0 then (0,0)
1.12                                  else negateSnd (negDivAlg (~a,~b))
1.13 -                       else
1.14 +                       else
1.15                            if 0<b then negDivAlg (a,b)
1.16                            else        negateSnd (posDivAlg (~a,~b));
1.17  *)
1.18 @@ -66,7 +66,7 @@
1.19               %<a,b> f. if (#0 \$<= a\$+b | b\$<=#0) then <#-1,a\$+b>
1.20                         else adjust(b, f ` <a,#2\$*b>))"
1.21
1.22 -(*for the general case b\<noteq>0*)
1.23 +(*for the general case @{term"b\<noteq>0"}*)
1.24
1.25  definition
1.26    negateSnd :: "i => i"  where
1.27 @@ -81,7 +81,7 @@
1.28                    if #0 \$<= b then posDivAlg (<a,b>)
1.29                    else if a=#0 then <#0,#0>
1.30                         else negateSnd (negDivAlg (<\$-a,\$-b>))
1.31 -               else
1.32 +               else
1.33                    if #0\$<b then negDivAlg (<a,b>)
1.34                    else         negateSnd (posDivAlg (<\$-a,\$-b>))"
1.35
1.36 @@ -226,7 +226,7 @@
1.37  (** strict, in 1st argument; proof is by induction on k>0 **)
1.38
1.39  lemma zmult_zless_mono2_lemma [rule_format]:
1.40 -     "[| i\$<j; k \<in> nat |] ==> 0<k --> \$#k \$* i \$< \$#k \$* j"
1.41 +     "[| i\$<j; k \<in> nat |] ==> 0<k \<longrightarrow> \$#k \$* i \$< \$#k \$* j"
1.42  apply (induct_tac "k")
1.43   prefer 2
1.44   apply (subst int_succ_int_1)
1.45 @@ -266,13 +266,13 @@
1.46
1.47  lemma zmult_zless_mono1_neg: "[| i \$< j;  k \$< #0 |] ==> j\$*k \$< i\$*k"
1.48  apply (rule zminus_zless_zminus [THEN iffD1])
1.49 -apply (simp del: zmult_zminus_right
1.50 +apply (simp del: zmult_zminus_right
1.51              add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
1.52  done
1.53
1.54  lemma zmult_zless_mono2_neg: "[| i \$< j;  k \$< #0 |] ==> k\$*j \$< k\$*i"
1.55  apply (rule zminus_zless_zminus [THEN iffD1])
1.56 -apply (simp del: zmult_zminus
1.57 +apply (simp del: zmult_zminus
1.58              add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
1.59  done
1.60
1.61 @@ -291,16 +291,16 @@
1.62  done
1.63
1.64
1.65 -(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
1.66 +(** Cancellation laws for k*m < k*n and m*k < n*k, also for @{text"\<le>"} and =,
1.67      but not (yet?) for k*m < n*k. **)
1.68
1.69  lemma zmult_zless_lemma:
1.70 -     "[| k \<in> int; m \<in> int; n \<in> int |]
1.71 +     "[| k \<in> int; m \<in> int; n \<in> int |]
1.72        ==> (m\$*k \$< n\$*k) <-> ((#0 \$< k & m\$<n) | (k \$< #0 & n\$<m))"
1.73  apply (case_tac "k = #0")
1.74  apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
1.75 -apply (auto simp add: not_zless_iff_zle
1.76 -                      not_zle_iff_zless [THEN iff_sym, of "m\$*k"]
1.77 +apply (auto simp add: not_zless_iff_zle
1.78 +                      not_zle_iff_zless [THEN iff_sym, of "m\$*k"]
1.79                        not_zle_iff_zless [THEN iff_sym, of m])
1.80  apply (auto elim: notE
1.81              simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
1.82 @@ -308,7 +308,7 @@
1.83
1.84  lemma zmult_zless_cancel2:
1.85       "(m\$*k \$< n\$*k) <-> ((#0 \$< k & m\$<n) | (k \$< #0 & n\$<m))"
1.86 -apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
1.87 +apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
1.88         in zmult_zless_lemma)
1.89  apply auto
1.90  done
1.91 @@ -318,11 +318,11 @@
1.92  by (simp add: zmult_commute [of k] zmult_zless_cancel2)
1.93
1.94  lemma zmult_zle_cancel2:
1.95 -     "(m\$*k \$<= n\$*k) <-> ((#0 \$< k --> m\$<=n) & (k \$< #0 --> n\$<=m))"
1.96 +     "(m\$*k \$<= n\$*k) <-> ((#0 \$< k \<longrightarrow> m\$<=n) & (k \$< #0 \<longrightarrow> n\$<=m))"
1.97  by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
1.98
1.99  lemma zmult_zle_cancel1:
1.100 -     "(k\$*m \$<= k\$*n) <-> ((#0 \$< k --> m\$<=n) & (k \$< #0 --> n\$<=m))"
1.101 +     "(k\$*m \$<= k\$*n) <-> ((#0 \$< k \<longrightarrow> m\$<=n) & (k \$< #0 \<longrightarrow> n\$<=m))"
1.102  by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
1.103
1.104  lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n <-> (m \$<= n & n \$<= m)"
1.105 @@ -350,7 +350,7 @@
1.106  subsection{* Uniqueness and monotonicity of quotients and remainders *}
1.107
1.108  lemma unique_quotient_lemma:
1.109 -     "[| b\$*q' \$+ r' \$<= b\$*q \$+ r;  #0 \$<= r';  #0 \$< b;  r \$< b |]
1.110 +     "[| b\$*q' \$+ r' \$<= b\$*q \$+ r;  #0 \$<= r';  #0 \$< b;  r \$< b |]
1.111        ==> q' \$<= q"
1.112  apply (subgoal_tac "r' \$+ b \$* (q'\$-q) \$<= r")
1.114 @@ -359,18 +359,18 @@
1.115   apply (erule zle_zless_trans)
1.117   apply (erule zle_zless_trans)
1.118 - apply (simp add: );
1.119 + apply (simp add: );
1.120  apply (subgoal_tac "b \$* q' \$< b \$* (#1 \$+ q)")
1.121 - prefer 2
1.122 + prefer 2
1.124  apply (auto elim: zless_asym
1.126  done
1.127
1.128  lemma unique_quotient_lemma_neg:
1.129 -     "[| b\$*q' \$+ r' \$<= b\$*q \$+ r;  r \$<= #0;  b \$< #0;  b \$< r' |]
1.130 +     "[| b\$*q' \$+ r' \$<= b\$*q \$+ r;  r \$<= #0;  b \$< #0;  b \$< r' |]
1.131        ==> q \$<= q'"
1.132 -apply (rule_tac b = "\$-b" and r = "\$-r'" and r' = "\$-r"
1.133 +apply (rule_tac b = "\$-b" and r = "\$-r'" and r' = "\$-r"
1.134         in unique_quotient_lemma)
1.135  apply (auto simp del: zminus_zadd_distrib
1.137 @@ -378,19 +378,19 @@
1.138
1.139
1.140  lemma unique_quotient:
1.141 -     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b ~= #0;
1.142 +     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
1.143           q \<in> int; q' \<in> int |] ==> q = q'"
1.144  apply (simp add: split_ifs quorem_def neq_iff_zless)
1.145  apply safe
1.146  apply simp_all
1.147  apply (blast intro: zle_anti_sym
1.148 -             dest: zle_eq_refl [THEN unique_quotient_lemma]
1.149 +             dest: zle_eq_refl [THEN unique_quotient_lemma]
1.150                     zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+
1.151  done
1.152
1.153  lemma unique_remainder:
1.154 -     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b ~= #0;
1.155 -         q \<in> int; q' \<in> int;
1.156 +     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
1.157 +         q \<in> int; q' \<in> int;
1.158           r \<in> int; r' \<in> int |] ==> r = r'"
1.159  apply (subgoal_tac "q = q'")
1.160   prefer 2 apply (blast intro: unique_quotient)
1.161 @@ -398,18 +398,18 @@
1.162  done
1.163
1.164
1.165 -subsection{*Correctness of posDivAlg,
1.166 +subsection{*Correctness of posDivAlg,
1.167             the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"} *}
1.168
1.170 -     "adjust(b, <q,r>) = (let diff = r\$-b in
1.171 -                          if #0 \$<= diff then <#2\$*q \$+ #1,diff>
1.172 +     "adjust(b, <q,r>) = (let diff = r\$-b in
1.173 +                          if #0 \$<= diff then <#2\$*q \$+ #1,diff>
1.174                                           else <#2\$*q,r>)"
1.176
1.177
1.178  lemma posDivAlg_termination:
1.179 -     "[| #0 \$< b; ~ a \$< b |]
1.180 +     "[| #0 \$< b; ~ a \$< b |]
1.181        ==> nat_of(a \$- #2 \$\<times> b \$+ #1) < nat_of(a \$- b \$+ #1)"
1.182  apply (simp (no_asm) add: zless_nat_conj)
1.184 @@ -418,8 +418,8 @@
1.185  lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure]
1.186
1.187  lemma posDivAlg_eqn:
1.188 -     "[| #0 \$< b; a \<in> int; b \<in> int |] ==>
1.189 -      posDivAlg(<a,b>) =
1.190 +     "[| #0 \$< b; a \<in> int; b \<in> int |] ==>
1.191 +      posDivAlg(<a,b>) =
1.192         (if a\$<b then <#0,a> else adjust(b, posDivAlg (<a, #2\$*b>)))"
1.193  apply (rule posDivAlg_unfold [THEN trans])
1.194  apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym])
1.195 @@ -428,11 +428,11 @@
1.196
1.197  lemma posDivAlg_induct_lemma [rule_format]:
1.198    assumes prem:
1.199 -        "!!a b. [| a \<in> int; b \<in> int;
1.200 -                   ~ (a \$< b | b \$<= #0) --> P(<a, #2 \$* b>) |] ==> P(<a,b>)"
1.201 -  shows "<u,v> \<in> int*int --> P(<u,v>)"
1.202 +        "!!a b. [| a \<in> int; b \<in> int;
1.203 +                   ~ (a \$< b | b \$<= #0) \<longrightarrow> P(<a, #2 \$* b>) |] ==> P(<a,b>)"
1.204 +  shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)"
1.205  apply (rule_tac a = "<u,v>" in wf_induct)
1.206 -apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a \$- b \$+ #1)"
1.207 +apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a \$- b \$+ #1)"
1.208         in wf_measure)
1.209  apply clarify
1.210  apply (rule prem)
1.211 @@ -446,7 +446,7 @@
1.212    assumes u_int: "u \<in> int"
1.213        and v_int: "v \<in> int"
1.214        and ih: "!!a b. [| a \<in> int; b \<in> int;
1.215 -                     ~ (a \$< b | b \$<= #0) --> P(a, #2 \$* b) |] ==> P(a,b)"
1.216 +                     ~ (a \$< b | b \$<= #0) \<longrightarrow> P(a, #2 \$* b) |] ==> P(a,b)"
1.217    shows "P(u,v)"
1.218  apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
1.219  apply simp
1.220 @@ -456,8 +456,8 @@
1.221  apply (auto simp add: u_int v_int)
1.222  done
1.223
1.224 -(*FIXME: use intify in integ_of so that we always have integ_of w \<in> int.
1.225 -    then this rewrite can work for ALL constants!!*)
1.226 +(*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
1.227 +    then this rewrite can work for all constants!!*)
1.228  lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m \$<= #0 & #0 \$<= m)"
1.229  apply (simp (no_asm) add: int_eq_iff_zle)
1.230  done
1.231 @@ -483,17 +483,17 @@
1.232  (** Inequality reasoning **)
1.233
1.234  lemma int_0_less_lemma:
1.235 -     "[| x \<in> int; y \<in> int |]
1.236 +     "[| x \<in> int; y \<in> int |]
1.237        ==> (#0 \$< x \$* y) <-> (#0 \$< x & #0 \$< y | x \$< #0 & y \$< #0)"
1.238  apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
1.239 -apply (rule ccontr)
1.240 -apply (rule_tac [2] ccontr)
1.241 +apply (rule ccontr)
1.242 +apply (rule_tac [2] ccontr)
1.243  apply (auto simp add: zle_def not_zless_iff_zle)
1.244  apply (erule_tac P = "#0\$< x\$* y" in rev_mp)
1.245  apply (erule_tac [2] P = "#0\$< x\$* y" in rev_mp)
1.246 -apply (drule zmult_pos_neg, assumption)
1.247 +apply (drule zmult_pos_neg, assumption)
1.248   prefer 2
1.249 - apply (drule zmult_pos_neg, assumption)
1.250 + apply (drule zmult_pos_neg, assumption)
1.251  apply (auto dest: zless_not_sym simp add: zmult_commute)
1.252  done
1.253
1.254 @@ -504,7 +504,7 @@
1.255  done
1.256
1.257  lemma int_0_le_lemma:
1.258 -     "[| x \<in> int; y \<in> int |]
1.259 +     "[| x \<in> int; y \<in> int |]
1.260        ==> (#0 \$<= x \$* y) <-> (#0 \$<= x & #0 \$<= y | x \$<= #0 & y \$<= #0)"
1.261  by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
1.262
1.263 @@ -532,7 +532,7 @@
1.264  apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
1.265  apply assumption+
1.266  apply (case_tac "#0 \$< ba")
1.270   apply clarify
1.271   apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
1.272 @@ -543,8 +543,8 @@
1.273
1.274  (*Correctness of posDivAlg: it computes quotients correctly*)
1.275  lemma posDivAlg_correct [rule_format]:
1.276 -     "[| a \<in> int; b \<in> int |]
1.277 -      ==> #0 \$<= a --> #0 \$< b --> quorem (<a,b>, posDivAlg(<a,b>))"
1.278 +     "[| a \<in> int; b \<in> int |]
1.279 +      ==> #0 \$<= a \<longrightarrow> #0 \$< b \<longrightarrow> quorem (<a,b>, posDivAlg(<a,b>))"
1.280  apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
1.281  apply auto
1.283 @@ -567,7 +567,7 @@
1.284  subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*}
1.285
1.286  lemma negDivAlg_termination:
1.287 -     "[| #0 \$< b; a \$+ b \$< #0 |]
1.288 +     "[| #0 \$< b; a \$+ b \$< #0 |]
1.289        ==> nat_of(\$- a \$- #2 \$* b) < nat_of(\$- a \$- b)"
1.290  apply (simp (no_asm) add: zless_nat_conj)
1.291  apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym]
1.292 @@ -577,9 +577,9 @@
1.293  lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure]
1.294
1.295  lemma negDivAlg_eqn:
1.296 -     "[| #0 \$< b; a : int; b : int |] ==>
1.297 -      negDivAlg(<a,b>) =
1.298 -       (if #0 \$<= a\$+b then <#-1,a\$+b>
1.299 +     "[| #0 \$< b; a \<in> int; b \<in> int |] ==>
1.300 +      negDivAlg(<a,b>) =
1.301 +       (if #0 \$<= a\$+b then <#-1,a\$+b>
1.302                         else adjust(b, negDivAlg (<a, #2\$*b>)))"
1.303  apply (rule negDivAlg_unfold [THEN trans])
1.304  apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym])
1.305 @@ -588,12 +588,12 @@
1.306
1.307  lemma negDivAlg_induct_lemma [rule_format]:
1.308    assumes prem:
1.309 -        "!!a b. [| a \<in> int; b \<in> int;
1.310 -                   ~ (#0 \$<= a \$+ b | b \$<= #0) --> P(<a, #2 \$* b>) |]
1.311 +        "!!a b. [| a \<in> int; b \<in> int;
1.312 +                   ~ (#0 \$<= a \$+ b | b \$<= #0) \<longrightarrow> P(<a, #2 \$* b>) |]
1.313                  ==> P(<a,b>)"
1.314 -  shows "<u,v> \<in> int*int --> P(<u,v>)"
1.315 +  shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)"
1.316  apply (rule_tac a = "<u,v>" in wf_induct)
1.317 -apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (\$- a \$- b)"
1.318 +apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (\$- a \$- b)"
1.319         in wf_measure)
1.320  apply clarify
1.321  apply (rule prem)
1.322 @@ -605,8 +605,8 @@
1.323  lemma negDivAlg_induct [consumes 2]:
1.324    assumes u_int: "u \<in> int"
1.325        and v_int: "v \<in> int"
1.326 -      and ih: "!!a b. [| a \<in> int; b \<in> int;
1.327 -                         ~ (#0 \$<= a \$+ b | b \$<= #0) --> P(a, #2 \$* b) |]
1.328 +      and ih: "!!a b. [| a \<in> int; b \<in> int;
1.329 +                         ~ (#0 \$<= a \$+ b | b \$<= #0) \<longrightarrow> P(a, #2 \$* b) |]
1.330                        ==> P(a,b)"
1.331    shows "P(u,v)"
1.332  apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
1.333 @@ -624,7 +624,7 @@
1.334  apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
1.335  apply assumption+
1.336  apply (case_tac "#0 \$< ba")
1.340   apply clarify
1.341   apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
1.342 @@ -637,8 +637,8 @@
1.343  (*Correctness of negDivAlg: it computes quotients correctly
1.344    It doesn't work if a=0 because the 0/b=0 rather than -1*)
1.345  lemma negDivAlg_correct [rule_format]:
1.346 -     "[| a \<in> int; b \<in> int |]
1.347 -      ==> a \$< #0 --> #0 \$< b --> quorem (<a,b>, negDivAlg(<a,b>))"
1.348 +     "[| a \<in> int; b \<in> int |]
1.349 +      ==> a \$< #0 \<longrightarrow> #0 \$< b \<longrightarrow> quorem (<a,b>, negDivAlg(<a,b>))"
1.350  apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
1.351    apply auto
1.353 @@ -698,7 +698,7 @@
1.354  done
1.355
1.356  lemma quorem_neg:
1.357 -     "[|quorem (<\$-a,\$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int|]
1.358 +     "[|quorem (<\$-a,\$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int|]
1.359        ==> quorem (<a,b>, negateSnd(qr))"
1.360  apply clarify
1.361  apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
1.362 @@ -714,7 +714,7 @@
1.363       "[|b \<noteq> #0;  a \<in> int;  b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
1.364  apply (auto simp add: quorem_0 divAlg_def)
1.365  apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
1.366 -                    posDivAlg_type negDivAlg_type)
1.367 +                    posDivAlg_type negDivAlg_type)
1.368  apply (auto simp add: quorem_def neq_iff_zless)
1.369  txt{*linear arithmetic from here on*}
1.370  apply (auto simp add: zle_def)
1.371 @@ -756,7 +756,7 @@
1.372  done
1.373
1.374
1.375 -(** Arbitrary definitions for division by zero.  Useful to simplify
1.376 +(** Arbitrary definitions for division by zero.  Useful to simplify
1.377      certain equations **)
1.378
1.379  lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
1.380 @@ -774,7 +774,7 @@
1.381  lemma raw_zmod_zdiv_equality:
1.382       "[| a \<in> int; b \<in> int |] ==> a = b \$* (a zdiv b) \$+ (a zmod b)"
1.383  apply (case_tac "b = #0")
1.384 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.385 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.386  apply (cut_tac a = "a" and b = "b" in divAlg_correct)
1.387  apply (auto simp add: quorem_def zdiv_def zmod_def split_def)
1.388  done
1.389 @@ -808,21 +808,21 @@
1.390  (** proving general properties of zdiv and zmod **)
1.391
1.392  lemma quorem_div_mod:
1.393 -     "[|b \<noteq> #0;  a \<in> int;  b \<in> int |]
1.394 +     "[|b \<noteq> #0;  a \<in> int;  b \<in> int |]
1.395        ==> quorem (<a,b>, <a zdiv b, a zmod b>)"
1.396  apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
1.397 -apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
1.398 +apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
1.399                        neg_mod_sign neg_mod_bound)
1.400  done
1.401
1.402 -(*Surely quorem(<a,b>,<q,r>) implies a \<in> int, but it doesn't matter*)
1.403 +(*Surely quorem(<a,b>,<q,r>) implies @{term"a \<in> int"}, but it doesn't matter*)
1.404  lemma quorem_div:
1.405 -     "[| quorem(<a,b>,<q,r>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int |]
1.406 +     "[| quorem(<a,b>,<q,r>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int |]
1.407        ==> a zdiv b = q"
1.408  by (blast intro: quorem_div_mod [THEN unique_quotient])
1.409
1.410  lemma quorem_mod:
1.411 -     "[| quorem(<a,b>,<q,r>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int |]
1.412 +     "[| quorem(<a,b>,<q,r>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int |]
1.413        ==> a zmod b = r"
1.414  by (blast intro: quorem_div_mod [THEN unique_remainder])
1.415
1.416 @@ -835,7 +835,7 @@
1.417  done
1.418
1.419  lemma zdiv_pos_pos_trivial: "[| #0 \$<= a;  a \$< b |] ==> a zdiv b = #0"
1.420 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.421 +apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.422         in zdiv_pos_pos_trivial_raw)
1.423  apply auto
1.424  done
1.425 @@ -849,7 +849,7 @@
1.426  done
1.427
1.428  lemma zdiv_neg_neg_trivial: "[| a \$<= #0;  b \$< a |] ==> a zdiv b = #0"
1.429 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.430 +apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.431         in zdiv_neg_neg_trivial_raw)
1.432  apply auto
1.433  done
1.434 @@ -869,7 +869,7 @@
1.435  done
1.436
1.437  lemma zdiv_pos_neg_trivial: "[| #0 \$< a;  a\$+b \$<= #0 |] ==> a zdiv b = #-1"
1.438 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.439 +apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.440         in zdiv_pos_neg_trivial_raw)
1.441  apply auto
1.442  done
1.443 @@ -886,7 +886,7 @@
1.444  done
1.445
1.446  lemma zmod_pos_pos_trivial: "[| #0 \$<= a;  a \$< b |] ==> a zmod b = intify(a)"
1.447 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.448 +apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.449         in zmod_pos_pos_trivial_raw)
1.450  apply auto
1.451  done
1.452 @@ -900,7 +900,7 @@
1.453  done
1.454
1.455  lemma zmod_neg_neg_trivial: "[| a \$<= #0;  b \$< a |] ==> a zmod b = intify(a)"
1.456 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.457 +apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.458         in zmod_neg_neg_trivial_raw)
1.459  apply auto
1.460  done
1.461 @@ -914,7 +914,7 @@
1.462  done
1.463
1.464  lemma zmod_pos_neg_trivial: "[| #0 \$< a;  a\$+b \$<= #0 |] ==> a zmod b = a\$+b"
1.465 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.466 +apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.467         in zmod_pos_neg_trivial_raw)
1.468  apply auto
1.469  done
1.470 @@ -927,7 +927,7 @@
1.471  lemma zdiv_zminus_zminus_raw:
1.472       "[|a \<in> int;  b \<in> int|] ==> (\$-a) zdiv (\$-b) = a zdiv b"
1.473  apply (case_tac "b = #0")
1.474 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.475 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.476  apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div])
1.477  apply auto
1.478  done
1.479 @@ -941,7 +941,7 @@
1.480  lemma zmod_zminus_zminus_raw:
1.481       "[|a \<in> int;  b \<in> int|] ==> (\$-a) zmod (\$-b) = \$- (a zmod b)"
1.482  apply (case_tac "b = #0")
1.483 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.484 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.485  apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod])
1.486  apply auto
1.487  done
1.488 @@ -1008,7 +1008,7 @@
1.489  (*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *)
1.490  lemma zmod_self_raw: "a \<in> int ==> a zmod a = #0"
1.491  apply (case_tac "a = #0")
1.492 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.493 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.494  apply (blast intro: quorem_div_mod [THEN self_remainder])
1.495  done
1.496
1.497 @@ -1042,14 +1042,14 @@
1.498
1.499  (** a positive, b positive **)
1.500
1.501 -lemma zdiv_pos_pos: "[| #0 \$< a;  #0 \$<= b |]
1.502 +lemma zdiv_pos_pos: "[| #0 \$< a;  #0 \$<= b |]
1.503        ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))"
1.504  apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.505  apply (auto simp add: zle_def)
1.506  done
1.507
1.508  lemma zmod_pos_pos:
1.509 -     "[| #0 \$< a;  #0 \$<= b |]
1.510 +     "[| #0 \$< a;  #0 \$<= b |]
1.511        ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))"
1.512  apply (simp (no_asm_simp) add: zmod_def divAlg_def)
1.513  apply (auto simp add: zle_def)
1.514 @@ -1058,14 +1058,14 @@
1.515  (** a negative, b positive **)
1.516
1.517  lemma zdiv_neg_pos:
1.518 -     "[| a \$< #0;  #0 \$< b |]
1.519 +     "[| a \$< #0;  #0 \$< b |]
1.520        ==> a zdiv b = fst (negDivAlg(<intify(a), intify(b)>))"
1.521  apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.522  apply (blast dest: zle_zless_trans)
1.523  done
1.524
1.525  lemma zmod_neg_pos:
1.526 -     "[| a \$< #0;  #0 \$< b |]
1.527 +     "[| a \$< #0;  #0 \$< b |]
1.528        ==> a zmod b = snd (negDivAlg(<intify(a), intify(b)>))"
1.529  apply (simp (no_asm_simp) add: zmod_def divAlg_def)
1.530  apply (blast dest: zle_zless_trans)
1.531 @@ -1074,7 +1074,7 @@
1.532  (** a positive, b negative **)
1.533
1.534  lemma zdiv_pos_neg:
1.535 -     "[| #0 \$< a;  b \$< #0 |]
1.536 +     "[| #0 \$< a;  b \$< #0 |]
1.537        ==> a zdiv b = fst (negateSnd(negDivAlg (<\$-a, \$-b>)))"
1.538  apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle)
1.539  apply auto
1.540 @@ -1084,7 +1084,7 @@
1.541  done
1.542
1.543  lemma zmod_pos_neg:
1.544 -     "[| #0 \$< a;  b \$< #0 |]
1.545 +     "[| #0 \$< a;  b \$< #0 |]
1.546        ==> a zmod b = snd (negateSnd(negDivAlg (<\$-a, \$-b>)))"
1.547  apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle)
1.548  apply auto
1.549 @@ -1096,7 +1096,7 @@
1.550  (** a negative, b negative **)
1.551
1.552  lemma zdiv_neg_neg:
1.553 -     "[| a \$< #0;  b \$<= #0 |]
1.554 +     "[| a \$< #0;  b \$<= #0 |]
1.555        ==> a zdiv b = fst (negateSnd(posDivAlg(<\$-a, \$-b>)))"
1.556  apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.557  apply auto
1.558 @@ -1104,7 +1104,7 @@
1.559  done
1.560
1.561  lemma zmod_neg_neg:
1.562 -     "[| a \$< #0;  b \$<= #0 |]
1.563 +     "[| a \$< #0;  b \$<= #0 |]
1.564        ==> a zmod b = snd (negateSnd(posDivAlg(<\$-a, \$-b>)))"
1.565  apply (simp (no_asm_simp) add: zmod_def divAlg_def)
1.566  apply auto
1.567 @@ -1198,10 +1198,10 @@
1.568  done
1.569
1.570  lemma zdiv_mono2_lemma:
1.571 -     "[| b\$*q \$+ r = b'\$*q' \$+ r';  #0 \$<= b'\$*q' \$+ r';
1.572 -         r' \$< b';  #0 \$<= r;  #0 \$< b';  b' \$<= b |]
1.573 +     "[| b\$*q \$+ r = b'\$*q' \$+ r';  #0 \$<= b'\$*q' \$+ r';
1.574 +         r' \$< b';  #0 \$<= r;  #0 \$< b';  b' \$<= b |]
1.575        ==> q \$<= q'"
1.576 -apply (frule q_pos_lemma, assumption+)
1.577 +apply (frule q_pos_lemma, assumption+)
1.578  apply (subgoal_tac "b\$*q \$< b\$* (q' \$+ #1)")
1.580   apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans)
1.581 @@ -1219,7 +1219,7 @@
1.582
1.583
1.584  lemma zdiv_mono2_raw:
1.585 -     "[| #0 \$<= a;  #0 \$< b';  b' \$<= b;  a \<in> int |]
1.586 +     "[| #0 \$<= a;  #0 \$< b';  b' \$<= b;  a \<in> int |]
1.587        ==> a zdiv b \$<= a zdiv b'"
1.588  apply (subgoal_tac "#0 \$< b")
1.589   prefer 2 apply (blast dest: zless_zle_trans)
1.590 @@ -1232,7 +1232,7 @@
1.591  done
1.592
1.593  lemma zdiv_mono2:
1.594 -     "[| #0 \$<= a;  #0 \$< b';  b' \$<= b |]
1.595 +     "[| #0 \$<= a;  #0 \$< b';  b' \$<= b |]
1.596        ==> a zdiv b \$<= a zdiv b'"
1.597  apply (cut_tac a = "intify (a)" in zdiv_mono2_raw)
1.598  apply auto
1.599 @@ -1249,12 +1249,12 @@
1.600
1.601
1.602  lemma zdiv_mono2_neg_lemma:
1.603 -     "[| b\$*q \$+ r = b'\$*q' \$+ r';  b'\$*q' \$+ r' \$< #0;
1.604 -         r \$< b;  #0 \$<= r';  #0 \$< b';  b' \$<= b |]
1.605 +     "[| b\$*q \$+ r = b'\$*q' \$+ r';  b'\$*q' \$+ r' \$< #0;
1.606 +         r \$< b;  #0 \$<= r';  #0 \$< b';  b' \$<= b |]
1.607        ==> q' \$<= q"
1.608  apply (subgoal_tac "#0 \$< b")
1.609   prefer 2 apply (blast dest: zless_zle_trans)
1.610 -apply (frule q_neg_lemma, assumption+)
1.611 +apply (frule q_neg_lemma, assumption+)
1.612  apply (subgoal_tac "b\$*q' \$< b\$* (q \$+ #1)")
1.614   apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
1.615 @@ -1278,7 +1278,7 @@
1.616  done
1.617
1.618  lemma zdiv_mono2_neg_raw:
1.619 -     "[| a \$< #0;  #0 \$< b';  b' \$<= b;  a \<in> int |]
1.620 +     "[| a \$< #0;  #0 \$< b';  b' \$<= b;  a \<in> int |]
1.621        ==> a zdiv b' \$<= a zdiv b"
1.622  apply (subgoal_tac "#0 \$< b")
1.623   prefer 2 apply (blast dest: zless_zle_trans)
1.624 @@ -1290,7 +1290,7 @@
1.625  apply (simp_all add: pos_mod_sign pos_mod_bound)
1.626  done
1.627
1.628 -lemma zdiv_mono2_neg: "[| a \$< #0;  #0 \$< b';  b' \$<= b |]
1.629 +lemma zdiv_mono2_neg: "[| a \$< #0;  #0 \$< b';  b' \$<= b |]
1.630        ==> a zdiv b' \$<= a zdiv b"
1.631  apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw)
1.632  apply auto
1.633 @@ -1303,18 +1303,18 @@
1.634  (** proving (a*b) zdiv c = a \$* (b zdiv c) \$+ a * (b zmod c) **)
1.635
1.636  lemma zmult1_lemma:
1.637 -     "[| quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0 |]
1.638 +     "[| quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0 |]
1.639        ==> quorem (<a\$*b, c>, <a\$*q \$+ (a\$*r) zdiv c, (a\$*r) zmod c>)"
1.641                        pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
1.642 -apply (auto intro: raw_zmod_zdiv_equality)
1.643 +apply (auto intro: raw_zmod_zdiv_equality)
1.644  done
1.645
1.646  lemma zdiv_zmult1_eq_raw:
1.647 -     "[|b \<in> int;  c \<in> int|]
1.648 +     "[|b \<in> int;  c \<in> int|]
1.649        ==> (a\$*b) zdiv c = a\$*(b zdiv c) \$+ a\$*(b zmod c) zdiv c"
1.650  apply (case_tac "c = #0")
1.651 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.652 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.653  apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
1.654  apply auto
1.655  done
1.656 @@ -1327,7 +1327,7 @@
1.657  lemma zmod_zmult1_eq_raw:
1.658       "[|b \<in> int;  c \<in> int|] ==> (a\$*b) zmod c = a\$*(b zmod c) zmod c"
1.659  apply (case_tac "c = #0")
1.660 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.661 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.662  apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
1.663  apply auto
1.664  done
1.665 @@ -1366,12 +1366,12 @@
1.666  done
1.667
1.668
1.669 -(** proving (a\$+b) zdiv c =
1.670 +(** proving (a\$+b) zdiv c =
1.671              a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c) **)
1.672
1.674 -     "[| quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);
1.675 -         c \<in> int;  c \<noteq> #0 |]
1.676 +     "[| quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);
1.677 +         c \<in> int;  c \<noteq> #0 |]
1.678        ==> quorem (<a\$+b, c>, <aq \$+ bq \$+ (ar\$+br) zdiv c, (ar\$+br) zmod c>)"
1.680                        pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
1.681 @@ -1380,32 +1380,32 @@
1.682
1.683  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.685 -     "[|a \<in> int; b \<in> int; c \<in> int|] ==>
1.686 +     "[|a \<in> int; b \<in> int; c \<in> int|] ==>
1.687        (a\$+b) zdiv c = a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c)"
1.688  apply (case_tac "c = #0")
1.689 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.690 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.691  apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
1.692                                   THEN quorem_div])
1.693  done
1.694
1.696       "(a\$+b) zdiv c = a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c)"
1.697 -apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
1.698 +apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
1.700  apply auto
1.701  done
1.702
1.704 -     "[|a \<in> int; b \<in> int; c \<in> int|]
1.705 +     "[|a \<in> int; b \<in> int; c \<in> int|]
1.706        ==> (a\$+b) zmod c = (a zmod c \$+ b zmod c) zmod c"
1.707  apply (case_tac "c = #0")
1.708 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.709 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
1.710 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.711 +apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
1.712                                   THEN quorem_mod])
1.713  done
1.714
1.715  lemma zmod_zadd1_eq: "(a\$+b) zmod c = (a zmod c \$+ b zmod c) zmod c"
1.716 -apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
1.717 +apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
1.719  apply auto
1.720  done
1.721 @@ -1413,7 +1413,7 @@
1.722  lemma zmod_div_trivial_raw:
1.723       "[|a \<in> int; b \<in> int|] ==> (a zmod b) zdiv b = #0"
1.724  apply (case_tac "b = #0")
1.725 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.726 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.727  apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
1.728           zdiv_pos_pos_trivial neg_mod_sign neg_mod_bound zdiv_neg_neg_trivial)
1.729  done
1.730 @@ -1426,8 +1426,8 @@
1.731  lemma zmod_mod_trivial_raw:
1.732       "[|a \<in> int; b \<in> int|] ==> (a zmod b) zmod b = a zmod b"
1.733  apply (case_tac "b = #0")
1.734 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.735 -apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
1.736 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.737 +apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
1.738         zmod_pos_pos_trivial neg_mod_sign neg_mod_bound zmod_neg_neg_trivial)
1.739  done
1.740
1.741 @@ -1461,13 +1461,13 @@
1.742
1.743  lemma zmod_zadd_self1 [simp]: "(a\$+b) zmod a = b zmod a"
1.744  apply (case_tac "a = #0")
1.745 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.746 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.748  done
1.749
1.750  lemma zmod_zadd_self2 [simp]: "(b\$+a) zmod a = b zmod a"
1.751  apply (case_tac "a = #0")
1.752 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.753 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.755  done
1.756
1.757 @@ -1495,7 +1495,7 @@
1.758       "[| #0 \$< c;   b \$< r;  r \$<= #0 |] ==> b \$* (q zmod c) \$+ r \$<= #0"
1.759  apply (subgoal_tac "b \$* (q zmod c) \$<= #0")
1.760   prefer 2
1.761 - apply (simp add: zmult_le_0_iff pos_mod_sign)
1.762 + apply (simp add: zmult_le_0_iff pos_mod_sign)
1.763   apply (blast intro: zless_imp_zle dest: zless_zle_trans)
1.764  (*arithmetic*)
1.766 @@ -1507,7 +1507,7 @@
1.767       "[| #0 \$< c;  #0 \$<= r;  r \$< b |] ==> #0 \$<= b \$* (q zmod c) \$+ r"
1.768  apply (subgoal_tac "#0 \$<= b \$* (q zmod c)")
1.769   prefer 2
1.770 - apply (simp add: int_0_le_mult_iff pos_mod_sign)
1.771 + apply (simp add: int_0_le_mult_iff pos_mod_sign)
1.772   apply (blast intro: zless_imp_zle dest: zle_zless_trans)
1.773  (*arithmetic*)
1.775 @@ -1527,10 +1527,10 @@
1.776  done
1.777
1.778  lemma zdiv_zmult2_lemma:
1.779 -     "[| quorem (<a,b>, <q,r>);  a \<in> int;  b \<in> int;  b \<noteq> #0;  #0 \$< c |]
1.780 +     "[| quorem (<a,b>, <q,r>);  a \<in> int;  b \<in> int;  b \<noteq> #0;  #0 \$< c |]
1.781        ==> quorem (<a,b\$*c>, <q zdiv c, b\$*(q zmod c) \$+ r>)"
1.782  apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
1.783 -               neq_iff_zless int_0_less_mult_iff
1.784 +               neq_iff_zless int_0_less_mult_iff
1.786                 zdiv_zmult2_aux3 zdiv_zmult2_aux4)
1.787  apply (blast dest: zless_trans)+
1.788 @@ -1539,7 +1539,7 @@
1.789  lemma zdiv_zmult2_eq_raw:
1.790       "[|#0 \$< c;  a \<in> int;  b \<in> int|] ==> a zdiv (b\$*c) = (a zdiv b) zdiv c"
1.791  apply (case_tac "b = #0")
1.792 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.793 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.794  apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_div])
1.795  apply (auto simp add: intify_eq_0_iff_zle)
1.796  apply (blast dest: zle_zless_trans)
1.797 @@ -1551,10 +1551,10 @@
1.798  done
1.799
1.800  lemma zmod_zmult2_eq_raw:
1.801 -     "[|#0 \$< c;  a \<in> int;  b \<in> int|]
1.802 +     "[|#0 \$< c;  a \<in> int;  b \<in> int|]
1.803        ==> a zmod (b\$*c) = b\$*(a zdiv b zmod c) \$+ a zmod b"
1.804  apply (case_tac "b = #0")
1.805 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.806 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.807  apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_mod])
1.808  apply (auto simp add: intify_eq_0_iff_zle)
1.809  apply (blast dest: zle_zless_trans)
1.810 @@ -1584,7 +1584,7 @@
1.811  lemma zdiv_zmult_zmult1_raw:
1.812       "[|intify(c) \<noteq> #0; b \<in> int|] ==> (c\$*a) zdiv (c\$*b) = a zdiv b"
1.813  apply (case_tac "b = #0")
1.814 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.815 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.816  apply (auto simp add: neq_iff_zless [of b]
1.817    zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
1.818  done
1.819 @@ -1603,14 +1603,14 @@
1.820  subsection{* Distribution of factors over "zmod" *}
1.821
1.822  lemma zmod_zmult_zmult1_aux1:
1.823 -     "[| #0 \$< b;  intify(c) \<noteq> #0 |]
1.824 +     "[| #0 \$< b;  intify(c) \<noteq> #0 |]
1.825        ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)"
1.826  apply (subst zmod_zmult2_eq)
1.827  apply auto
1.828  done
1.829
1.830  lemma zmod_zmult_zmult1_aux2:
1.831 -     "[| b \$< #0;  intify(c) \<noteq> #0 |]
1.832 +     "[| b \$< #0;  intify(c) \<noteq> #0 |]
1.833        ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)"
1.834  apply (subgoal_tac " (c \$* (\$-a)) zmod (c \$* (\$-b)) = c \$* ((\$-a) zmod (\$-b))")
1.835  apply (rule_tac [2] zmod_zmult_zmult1_aux1)
1.836 @@ -1620,9 +1620,9 @@
1.837  lemma zmod_zmult_zmult1_raw:
1.838       "[|b \<in> int; c \<in> int|] ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)"
1.839  apply (case_tac "b = #0")
1.840 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.841 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.842  apply (case_tac "c = #0")
1.843 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.844 + apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.845  apply (auto simp add: neq_iff_zless [of b]
1.846    zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
1.847  done
1.848 @@ -1726,9 +1726,9 @@
1.849   apply auto
1.850   done
1.851
1.852 - lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) =
1.853 -           (if ~b | #0 \$<= integ_of w
1.854 -            then integ_of v zdiv (integ_of w)
1.855 + lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) =
1.856 +           (if ~b | #0 \$<= integ_of w
1.857 +            then integ_of v zdiv (integ_of w)
1.858              else (integ_of v \$+ #1) zdiv (integ_of w))"
1.860   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)
1.861 @@ -1770,11 +1770,11 @@
1.862   apply auto
1.863   done
1.864
1.865 - lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) =
1.866 -           (if b then
1.867 -                 if #0 \$<= integ_of w
1.868 -                 then #2 \$* (integ_of v zmod integ_of w) \$+ #1
1.869 -                 else #2 \$* ((integ_of v \$+ #1) zmod integ_of w) - #1
1.870 + lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) =
1.871 +           (if b then
1.872 +                 if #0 \$<= integ_of w
1.873 +                 then #2 \$* (integ_of v zmod integ_of w) \$+ #1
1.874 +                 else #2 \$* ((integ_of v \$+ #1) zmod integ_of w) - #1
1.875              else #2 \$* (integ_of v zmod integ_of w))"