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.113   prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls)
   1.114 @@ -359,18 +359,18 @@
   1.115   apply (erule zle_zless_trans)
   1.116   apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
   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.123   apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
   1.124  apply (auto elim: zless_asym
   1.125          simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls)
   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.136              simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus)
   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.169  lemma adjust_eq [simp]:
   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.175  by (simp add: Let_def adjust_def)
   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.183  apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls)
   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.267 - apply (simp add: posDivAlg_eqn adjust_def integ_of_type 
   1.268 + apply (simp add: posDivAlg_eqn adjust_def integ_of_type
   1.269               split add: split_if_asm)
   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.282     apply (simp_all add: quorem_def)
   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.337 - apply (simp add: negDivAlg_eqn adjust_def integ_of_type 
   1.338 + apply (simp add: negDivAlg_eqn adjust_def integ_of_type
   1.339               split add: split_if_asm)
   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.352     apply (simp_all add: quorem_def)
   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.579   apply (simp add: zmult_zless_cancel1)
   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.613   apply (simp add: zmult_zless_cancel1)
   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.640  apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
   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.673  lemma zadd1_lemma:
   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.679  apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
   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.684  lemma zdiv_zadd1_eq_raw:
   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.695  lemma zdiv_zadd1_eq:
   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.699         in zdiv_zadd1_eq_raw)
   1.700  apply auto
   1.701  done
   1.702  
   1.703  lemma zmod_zadd1_eq_raw:
   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.718         in zmod_zadd1_eq_raw)
   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.747  apply (simp (no_asm_simp) add: zmod_zadd1_eq)
   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.754  apply (simp (no_asm_simp) add: zmod_zadd1_eq)
   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.765  apply (drule zadd_zle_mono)
   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.774  apply (drule zadd_zle_mono)
   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.785                 zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2
   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.859   apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
   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))"
   1.876   apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
   1.877   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)