src/HOL/Integ/IntDiv.ML
changeset 11868 56db9f3a6b3e
parent 11704 3c50a2cd6f00
equal deleted inserted replaced
11867:76401b2ee871 11868:56db9f3a6b3e
    32 
    32 
    33 Addsimps [zless_nat_conj];
    33 Addsimps [zless_nat_conj];
    34 
    34 
    35 (*** Uniqueness and monotonicity of quotients and remainders ***)
    35 (*** Uniqueness and monotonicity of quotients and remainders ***)
    36 
    36 
    37 Goal "[| b*q' + r'  <= b*q + r;  Numeral0 <= r';  Numeral0 < b;  r < b |] \
    37 Goal "[| b*q' + r'  <= b*q + r;  0 <= r';  0 < b;  r < b |] \
    38 \     ==> q' <= (q::int)";
    38 \     ==> q' <= (q::int)";
    39 by (subgoal_tac "r' + b * (q'-q) <= r" 1);
    39 by (subgoal_tac "r' + b * (q'-q) <= r" 1);
    40 by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
    40 by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
    41 by (subgoal_tac "Numeral0 < b * (Numeral1 + q - q')" 1);
    41 by (subgoal_tac "0 < b * (1 + q - q')" 1);
    42 by (etac order_le_less_trans 2);
    42 by (etac order_le_less_trans 2);
    43 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
    43 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
    44 				       zadd_zmult_distrib2]) 2);
    44 				       zadd_zmult_distrib2]) 2);
    45 by (subgoal_tac "b * q' < b * (Numeral1 + q)" 1);
    45 by (subgoal_tac "b * q' < b * (1 + q)" 1);
    46 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
    46 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
    47 				       zadd_zmult_distrib2]) 2);
    47 				       zadd_zmult_distrib2]) 2);
    48 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
    48 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
    49 qed "unique_quotient_lemma";
    49 qed "unique_quotient_lemma";
    50 
    50 
    51 Goal "[| b*q' + r' <= b*q + r;  r <= Numeral0;  b < Numeral0;  b < r' |] \
    51 Goal "[| b*q' + r' <= b*q + r;  r <= 0;  b < 0;  b < r' |] \
    52 \     ==> q <= (q'::int)";
    52 \     ==> q <= (q'::int)";
    53 by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")] 
    53 by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")] 
    54     unique_quotient_lemma 1);
    54     unique_quotient_lemma 1);
    55 by (auto_tac (claset(), 
    55 by (auto_tac (claset(), 
    56 	      simpset() addsimps [zmult_zminus, zmult_zminus_right])); 
    56 	      simpset() addsimps [zmult_zminus, zmult_zminus_right])); 
    57 qed "unique_quotient_lemma_neg";
    57 qed "unique_quotient_lemma_neg";
    58 
    58 
    59 
    59 
    60 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= Numeral0 |] \
    60 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= 0 |] \
    61 \     ==> q = q'";
    61 \     ==> q = q'";
    62 by (asm_full_simp_tac 
    62 by (asm_full_simp_tac 
    63     (simpset() addsimps split_ifs@
    63     (simpset() addsimps split_ifs@
    64                         [quorem_def, linorder_neq_iff]) 1);
    64                         [quorem_def, linorder_neq_iff]) 1);
    65 by Safe_tac; 
    65 by Safe_tac; 
    70 				order_eq_refl RS unique_quotient_lemma_neg,
    70 				order_eq_refl RS unique_quotient_lemma_neg,
    71 				sym]) 1));
    71 				sym]) 1));
    72 qed "unique_quotient";
    72 qed "unique_quotient";
    73 
    73 
    74 
    74 
    75 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= Numeral0 |] \
    75 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= 0 |] \
    76 \     ==> r = r'";
    76 \     ==> r = r'";
    77 by (subgoal_tac "q = q'" 1);
    77 by (subgoal_tac "q = q'" 1);
    78 by (blast_tac (claset() addIs [unique_quotient]) 2);
    78 by (blast_tac (claset() addIs [unique_quotient]) 2);
    79 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
    79 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
    80 qed "unique_remainder";
    80 qed "unique_remainder";
    81 
    81 
    82 
    82 
    83 (*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
    83 (*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
    84 
    84 
    85 
    85 
    86 Goal "adjust a b (q,r) = (let diff = r-b in \
    86 Goal "adjust b (q,r) = (let diff = r-b in \
    87 \                         if Numeral0 <= diff then (2*q + Numeral1, diff)  \
    87 \                         if 0 <= diff then (2*q + 1, diff)  \
    88 \                                       else (2*q, r))";
    88 \                                      else (2*q, r))";
    89 by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
    89 by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
    90 qed "adjust_eq";
    90 qed "adjust_eq";
    91 Addsimps [adjust_eq];
    91 Addsimps [adjust_eq];
    92 
    92 
    93 (*Proving posDivAlg's termination condition*)
    93 (*Proving posDivAlg's termination condition*)
    99 (* removing the termination condition from the generated theorems *)
    99 (* removing the termination condition from the generated theorems *)
   100 
   100 
   101 bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps);
   101 bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps);
   102 
   102 
   103 (**use with simproc to avoid re-proving the premise*)
   103 (**use with simproc to avoid re-proving the premise*)
   104 Goal "Numeral0 < b ==> \
   104 Goal "0 < b ==> \
   105 \     posDivAlg (a,b) =      \
   105 \     posDivAlg (a,b) =      \
   106 \      (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, 2*b)))";
   106 \      (if a<b then (0,a) else adjust b (posDivAlg(a, 2*b)))";
   107 by (rtac (posDivAlg_raw_eqn RS trans) 1);
   107 by (rtac (posDivAlg_raw_eqn RS trans) 1);
   108 by (Asm_simp_tac 1);
   108 by (Asm_simp_tac 1);
   109 qed "posDivAlg_eqn";
   109 qed "posDivAlg_eqn";
   110 
   110 
   111 bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct);
   111 bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct);
   112 
   112 
   113 
   113 
   114 (*Correctness of posDivAlg: it computes quotients correctly*)
   114 (*Correctness of posDivAlg: it computes quotients correctly*)
   115 Goal "Numeral0 <= a --> Numeral0 < b --> quorem ((a, b), posDivAlg (a, b))";
   115 Goal "0 <= a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))";
   116 by (induct_thm_tac posDivAlg_induct "a b" 1);
   116 by (induct_thm_tac posDivAlg_induct "a b" 1);
   117 by Auto_tac;
   117 by Auto_tac;
   118 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
   118 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
   119 (*base case: a<b*)
   119 (*base case: a<b*)
   120 by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
   120 by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
   137 (* removing the termination condition from the generated theorems *)
   137 (* removing the termination condition from the generated theorems *)
   138 
   138 
   139 bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps);
   139 bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps);
   140 
   140 
   141 (**use with simproc to avoid re-proving the premise*)
   141 (**use with simproc to avoid re-proving the premise*)
   142 Goal "Numeral0 < b ==> \
   142 Goal "0 < b ==> \
   143 \     negDivAlg (a,b) =      \
   143 \     negDivAlg (a,b) =      \
   144 \      (if Numeral0<=a+b then (-1,a+b) else adjust a b (negDivAlg(a, 2*b)))";
   144 \      (if 0<=a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))";
   145 by (rtac (negDivAlg_raw_eqn RS trans) 1);
   145 by (rtac (negDivAlg_raw_eqn RS trans) 1);
   146 by (Asm_simp_tac 1);
   146 by (Asm_simp_tac 1);
   147 qed "negDivAlg_eqn";
   147 qed "negDivAlg_eqn";
   148 
   148 
   149 bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct);
   149 bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct);
   150 
   150 
   151 
   151 
   152 (*Correctness of negDivAlg: it computes quotients correctly
   152 (*Correctness of negDivAlg: it computes quotients correctly
   153   It doesn't work if a=0 because the 0/b=0 rather than -1*)
   153   It doesn't work if a=0 because the 0/b=0 rather than -1*)
   154 Goal "a < Numeral0 --> Numeral0 < b --> quorem ((a, b), negDivAlg (a, b))";
   154 Goal "a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))";
   155 by (induct_thm_tac negDivAlg_induct "a b" 1);
   155 by (induct_thm_tac negDivAlg_induct "a b" 1);
   156 by Auto_tac;
   156 by Auto_tac;
   157 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
   157 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
   158 (*base case: 0<=a+b*)
   158 (*base case: 0<=a+b*)
   159 by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
   159 by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
   166 
   166 
   167 
   167 
   168 (*** Existence shown by proving the division algorithm to be correct ***)
   168 (*** Existence shown by proving the division algorithm to be correct ***)
   169 
   169 
   170 (*the case a=0*)
   170 (*the case a=0*)
   171 Goal "b ~= Numeral0 ==> quorem ((Numeral0,b), (Numeral0,Numeral0))";
   171 Goal "b ~= 0 ==> quorem ((0,b), (0,0))";
   172 by (auto_tac (claset(), 
   172 by (auto_tac (claset(), 
   173 	      simpset() addsimps [quorem_def, linorder_neq_iff]));
   173 	      simpset() addsimps [quorem_def, linorder_neq_iff]));
   174 qed "quorem_0";
   174 qed "quorem_0";
   175 
   175 
   176 Goal "posDivAlg (Numeral0, b) = (Numeral0, Numeral0)";
   176 Goal "posDivAlg (0, b) = (0, 0)";
   177 by (stac posDivAlg_raw_eqn 1);
   177 by (stac posDivAlg_raw_eqn 1);
   178 by Auto_tac;
   178 by Auto_tac;
   179 qed "posDivAlg_0";
   179 qed "posDivAlg_0";
   180 Addsimps [posDivAlg_0];
   180 Addsimps [posDivAlg_0];
   181 
   181 
   182 Goal "negDivAlg (-1, b) = (-1, b-Numeral1)";
   182 Goal "negDivAlg (-1, b) = (-1, b - 1)";
   183 by (stac negDivAlg_raw_eqn 1);
   183 by (stac negDivAlg_raw_eqn 1);
   184 by Auto_tac;
   184 by Auto_tac;
   185 qed "negDivAlg_minus1";
   185 qed "negDivAlg_minus1";
   186 Addsimps [negDivAlg_minus1];
   186 Addsimps [negDivAlg_minus1];
   187 
   187 
   192 
   192 
   193 Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)";
   193 Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)";
   194 by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
   194 by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
   195 qed "quorem_neg";
   195 qed "quorem_neg";
   196 
   196 
   197 Goal "b ~= Numeral0 ==> quorem ((a,b), divAlg(a,b))";
   197 Goal "b ~= 0 ==> quorem ((a,b), divAlg(a,b))";
   198 by (auto_tac (claset(), 
   198 by (auto_tac (claset(), 
   199 	      simpset() addsimps [quorem_0, divAlg_def]));
   199 	      simpset() addsimps [quorem_0, divAlg_def]));
   200 by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
   200 by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
   201 			       negDivAlg_correct]));
   201 			       negDivAlg_correct]));
   202 by (auto_tac (claset(), 
   202 by (auto_tac (claset(), 
   204 qed "divAlg_correct";
   204 qed "divAlg_correct";
   205 
   205 
   206 (** Arbitrary definitions for division by zero.  Useful to simplify 
   206 (** Arbitrary definitions for division by zero.  Useful to simplify 
   207     certain equations **)
   207     certain equations **)
   208 
   208 
   209 Goal "a div (Numeral0::int) = Numeral0";
   209 Goal "a div (0::int) = 0";
   210 by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1);
   210 by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1);
   211 qed "DIVISION_BY_ZERO_ZDIV";  (*NOT for adding to default simpset*)
   211 qed "DIVISION_BY_ZERO_ZDIV";  (*NOT for adding to default simpset*)
   212 
   212 
   213 Goal "a mod (Numeral0::int) = a";
   213 Goal "a mod (0::int) = a";
   214 by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1);
   214 by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1);
   215 qed "DIVISION_BY_ZERO_ZMOD";  (*NOT for adding to default simpset*)
   215 qed "DIVISION_BY_ZERO_ZMOD";  (*NOT for adding to default simpset*)
   216 
   216 
   217 fun zdiv_undefined_case_tac s i =
   217 fun zdiv_undefined_case_tac s i =
   218   case_tac s i THEN 
   218   case_tac s i THEN 
   220 				    DIVISION_BY_ZERO_ZMOD]) i;
   220 				    DIVISION_BY_ZERO_ZMOD]) i;
   221 
   221 
   222 (** Basic laws about division and remainder **)
   222 (** Basic laws about division and remainder **)
   223 
   223 
   224 Goal "(a::int) = b * (a div b) + (a mod b)";
   224 Goal "(a::int) = b * (a div b) + (a mod b)";
   225 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   225 by (zdiv_undefined_case_tac "b = 0" 1);
   226 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   226 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   227 by (auto_tac (claset(), 
   227 by (auto_tac (claset(), 
   228 	      simpset() addsimps [quorem_def, div_def, mod_def]));
   228 	      simpset() addsimps [quorem_def, div_def, mod_def]));
   229 qed "zmod_zdiv_equality";  
   229 qed "zmod_zdiv_equality";  
   230 
   230 
   231 Goal "(Numeral0::int) < b ==> Numeral0 <= a mod b & a mod b < b";
   231 Goal "(0::int) < b ==> 0 <= a mod b & a mod b < b";
   232 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   232 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   233 by (auto_tac (claset(), 
   233 by (auto_tac (claset(), 
   234 	      simpset() addsimps [quorem_def, mod_def]));
   234 	      simpset() addsimps [quorem_def, mod_def]));
   235 bind_thm ("pos_mod_sign", result() RS conjunct1);
   235 bind_thm ("pos_mod_sign", result() RS conjunct1);
   236 bind_thm ("pos_mod_bound", result() RS conjunct2);
   236 bind_thm ("pos_mod_bound", result() RS conjunct2);
   237 
   237 
   238 Goal "b < (Numeral0::int) ==> a mod b <= Numeral0 & b < a mod b";
   238 Goal "b < (0::int) ==> a mod b <= 0 & b < a mod b";
   239 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   239 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
   240 by (auto_tac (claset(), 
   240 by (auto_tac (claset(), 
   241 	      simpset() addsimps [quorem_def, div_def, mod_def]));
   241 	      simpset() addsimps [quorem_def, div_def, mod_def]));
   242 bind_thm ("neg_mod_sign", result() RS conjunct1);
   242 bind_thm ("neg_mod_sign", result() RS conjunct1);
   243 bind_thm ("neg_mod_bound", result() RS conjunct2);
   243 bind_thm ("neg_mod_bound", result() RS conjunct2);
   244 
   244 
   245 
   245 
   246 (** proving general properties of div and mod **)
   246 (** proving general properties of div and mod **)
   247 
   247 
   248 Goal "b ~= Numeral0 ==> quorem ((a, b), (a div b, a mod b))";
   248 Goal "b ~= 0 ==> quorem ((a, b), (a div b, a mod b))";
   249 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   249 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   250 by (auto_tac
   250 by (auto_tac
   251     (claset(),
   251     (claset(),
   252      simpset() addsimps [quorem_def, linorder_neq_iff, 
   252      simpset() addsimps [quorem_def, linorder_neq_iff, 
   253 			 pos_mod_sign,pos_mod_bound,
   253 			 pos_mod_sign,pos_mod_bound,
   254 			 neg_mod_sign, neg_mod_bound]));
   254 			 neg_mod_sign, neg_mod_bound]));
   255 qed "quorem_div_mod";
   255 qed "quorem_div_mod";
   256 
   256 
   257 Goal "[| quorem((a,b),(q,r));  b ~= Numeral0 |] ==> a div b = q";
   257 Goal "[| quorem((a,b),(q,r));  b ~= 0 |] ==> a div b = q";
   258 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
   258 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
   259 qed "quorem_div";
   259 qed "quorem_div";
   260 
   260 
   261 Goal "[| quorem((a,b),(q,r));  b ~= Numeral0 |] ==> a mod b = r";
   261 Goal "[| quorem((a,b),(q,r));  b ~= 0 |] ==> a mod b = r";
   262 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
   262 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
   263 qed "quorem_mod";
   263 qed "quorem_mod";
   264 
   264 
   265 Goal "[| (Numeral0::int) <= a;  a < b |] ==> a div b = Numeral0";
   265 Goal "[| (0::int) <= a;  a < b |] ==> a div b = 0";
   266 by (rtac quorem_div 1);
   266 by (rtac quorem_div 1);
   267 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   267 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   268 qed "div_pos_pos_trivial";
   268 qed "div_pos_pos_trivial";
   269 
   269 
   270 Goal "[| a <= (Numeral0::int);  b < a |] ==> a div b = Numeral0";
   270 Goal "[| a <= (0::int);  b < a |] ==> a div b = 0";
   271 by (rtac quorem_div 1);
   271 by (rtac quorem_div 1);
   272 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   272 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   273 qed "div_neg_neg_trivial";
   273 qed "div_neg_neg_trivial";
   274 
   274 
   275 Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a div b = -1";
   275 Goal "[| (0::int) < a;  a+b <= 0 |] ==> a div b = -1";
   276 by (rtac quorem_div 1);
   276 by (rtac quorem_div 1);
   277 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   277 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   278 qed "div_pos_neg_trivial";
   278 qed "div_pos_neg_trivial";
   279 
   279 
   280 (*There is no div_neg_pos_trivial because  Numeral0 div b = Numeral0 would supersede it*)
   280 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
   281 
   281 
   282 Goal "[| (Numeral0::int) <= a;  a < b |] ==> a mod b = a";
   282 Goal "[| (0::int) <= a;  a < b |] ==> a mod b = a";
   283 by (res_inst_tac [("q","Numeral0")] quorem_mod 1);
   283 by (res_inst_tac [("q","0")] quorem_mod 1);
   284 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   284 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   285 qed "mod_pos_pos_trivial";
   285 qed "mod_pos_pos_trivial";
   286 
   286 
   287 Goal "[| a <= (Numeral0::int);  b < a |] ==> a mod b = a";
   287 Goal "[| a <= (0::int);  b < a |] ==> a mod b = a";
   288 by (res_inst_tac [("q","Numeral0")] quorem_mod 1);
   288 by (res_inst_tac [("q","0")] quorem_mod 1);
   289 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   289 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   290 qed "mod_neg_neg_trivial";
   290 qed "mod_neg_neg_trivial";
   291 
   291 
   292 Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a mod b = a+b";
   292 Goal "[| (0::int) < a;  a+b <= 0 |] ==> a mod b = a+b";
   293 by (res_inst_tac [("q","-1")] quorem_mod 1);
   293 by (res_inst_tac [("q","-1")] quorem_mod 1);
   294 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   294 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   295 qed "mod_pos_neg_trivial";
   295 qed "mod_pos_neg_trivial";
   296 
   296 
   297 (*There is no mod_neg_pos_trivial...*)
   297 (*There is no mod_neg_pos_trivial...*)
   298 
   298 
   299 
   299 
   300 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
   300 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
   301 Goal "(-a) div (-b) = a div (b::int)";
   301 Goal "(-a) div (-b) = a div (b::int)";
   302 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   302 by (zdiv_undefined_case_tac "b = 0" 1);
   303 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
   303 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
   304 	  RS quorem_div) 1);
   304 	  RS quorem_div) 1);
   305 by Auto_tac;
   305 by Auto_tac;
   306 qed "zdiv_zminus_zminus";
   306 qed "zdiv_zminus_zminus";
   307 Addsimps [zdiv_zminus_zminus];
   307 Addsimps [zdiv_zminus_zminus];
   308 
   308 
   309 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
   309 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
   310 Goal "(-a) mod (-b) = - (a mod (b::int))";
   310 Goal "(-a) mod (-b) = - (a mod (b::int))";
   311 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   311 by (zdiv_undefined_case_tac "b = 0" 1);
   312 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
   312 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
   313 	  RS quorem_mod) 1);
   313 	  RS quorem_mod) 1);
   314 by Auto_tac;
   314 by Auto_tac;
   315 qed "zmod_zminus_zminus";
   315 qed "zmod_zminus_zminus";
   316 Addsimps [zmod_zminus_zminus];
   316 Addsimps [zmod_zminus_zminus];
   317 
   317 
   318 
   318 
   319 (*** div, mod and unary minus ***)
   319 (*** div, mod and unary minus ***)
   320 
   320 
   321 Goal "quorem((a,b),(q,r)) \
   321 Goal "quorem((a,b),(q,r)) \
   322 \     ==> quorem ((-a,b), (if r=Numeral0 then -q else -q-Numeral1), \
   322 \     ==> quorem ((-a,b), (if r=0 then -q else -q - 1), \
   323 \                         (if r=Numeral0 then Numeral0 else b-r))";
   323 \                         (if r=0 then 0 else b-r))";
   324 by (auto_tac
   324 by (auto_tac
   325     (claset(),
   325     (claset(),
   326      simpset() addsimps split_ifs@
   326      simpset() addsimps split_ifs@
   327                         [quorem_def, linorder_neq_iff, 
   327                         [quorem_def, linorder_neq_iff, 
   328 			 zdiff_zmult_distrib2]));
   328 			 zdiff_zmult_distrib2]));
   329 val lemma = result();
   329 val lemma = result();
   330 
   330 
   331 Goal "b ~= (Numeral0::int) \
   331 Goal "b ~= (0::int) \
   332 \     ==> (-a) div b = \
   332 \     ==> (-a) div b = \
   333 \         (if a mod b = Numeral0 then - (a div b) else  - (a div b) - Numeral1)";
   333 \         (if a mod b = 0 then - (a div b) else  - (a div b) - 1)";
   334 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
   334 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
   335 qed "zdiv_zminus1_eq_if";
   335 qed "zdiv_zminus1_eq_if";
   336 
   336 
   337 Goal "(-a::int) mod b = (if a mod b = Numeral0 then Numeral0 else  b - (a mod b))";
   337 Goal "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))";
   338 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   338 by (zdiv_undefined_case_tac "b = 0" 1);
   339 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
   339 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
   340 qed "zmod_zminus1_eq_if";
   340 qed "zmod_zminus1_eq_if";
   341 
   341 
   342 Goal "a div (-b) = (-a::int) div b";
   342 Goal "a div (-b) = (-a::int) div b";
   343 by (cut_inst_tac [("a","-a")] zdiv_zminus_zminus 1);
   343 by (cut_inst_tac [("a","-a")] zdiv_zminus_zminus 1);
   347 Goal "a mod (-b) = - ((-a::int) mod b)";
   347 Goal "a mod (-b) = - ((-a::int) mod b)";
   348 by (cut_inst_tac [("a","-a"),("b","b")] zmod_zminus_zminus 1);
   348 by (cut_inst_tac [("a","-a"),("b","b")] zmod_zminus_zminus 1);
   349 by Auto_tac;  
   349 by Auto_tac;  
   350 qed "zmod_zminus2";
   350 qed "zmod_zminus2";
   351 
   351 
   352 Goal "b ~= (Numeral0::int) \
   352 Goal "b ~= (0::int) \
   353 \     ==> a div (-b) = \
   353 \     ==> a div (-b) = \
   354 \         (if a mod b = Numeral0 then - (a div b) else  - (a div b) - Numeral1)";
   354 \         (if a mod b = 0 then - (a div b) else  - (a div b) - 1)";
   355 by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); 
   355 by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); 
   356 qed "zdiv_zminus2_eq_if";
   356 qed "zdiv_zminus2_eq_if";
   357 
   357 
   358 Goal "a mod (-b::int) = (if a mod b = Numeral0 then Numeral0 else  (a mod b) - b)";
   358 Goal "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)";
   359 by (asm_simp_tac (simpset() addsimps [zmod_zminus1_eq_if, zmod_zminus2]) 1); 
   359 by (asm_simp_tac (simpset() addsimps [zmod_zminus1_eq_if, zmod_zminus2]) 1); 
   360 qed "zmod_zminus2_eq_if";
   360 qed "zmod_zminus2_eq_if";
   361 
   361 
   362 
   362 
   363 (*** division of a number by itself ***)
   363 (*** division of a number by itself ***)
   364 
   364 
   365 Goal "[| (Numeral0::int) < a; a = r + a*q; r < a |] ==> Numeral1 <= q";
   365 Goal "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q";
   366 by (subgoal_tac "Numeral0 < a*q" 1);
   366 by (subgoal_tac "0 < a*q" 1);
   367 by (arith_tac 2);
   367 by (arith_tac 2);
   368 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
   368 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
   369 val lemma1 = result();
   369 val lemma1 = result();
   370 
   370 
   371 Goal "[| (Numeral0::int) < a; a = r + a*q; Numeral0 <= r |] ==> q <= Numeral1";
   371 Goal "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1";
   372 by (subgoal_tac "Numeral0 <= a*(Numeral1-q)" 1);
   372 by (subgoal_tac "0 <= a*(1-q)" 1);
   373 by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
   373 by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
   374 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
   374 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
   375 val lemma2 = result();
   375 val lemma2 = result();
   376 
   376 
   377 Goal "[| quorem((a,a),(q,r));  a ~= (Numeral0::int) |] ==> q = Numeral1";
   377 Goal "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> q = 1";
   378 by (asm_full_simp_tac 
   378 by (asm_full_simp_tac 
   379     (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1);
   379     (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1);
   380 by (rtac order_antisym 1);
   380 by (rtac order_antisym 1);
   381 by Safe_tac;
   381 by Safe_tac;
   382 by Auto_tac;
   382 by Auto_tac;
   384 by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1);
   384 by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1);
   385 by (REPEAT (force_tac  (claset() addIs [lemma1,lemma2], 
   385 by (REPEAT (force_tac  (claset() addIs [lemma1,lemma2], 
   386 	      simpset() addsimps [zadd_commute, zmult_zminus]) 1));
   386 	      simpset() addsimps [zadd_commute, zmult_zminus]) 1));
   387 qed "self_quotient";
   387 qed "self_quotient";
   388 
   388 
   389 Goal "[| quorem((a,a),(q,r));  a ~= (Numeral0::int) |] ==> r = Numeral0";
   389 Goal "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> r = 0";
   390 by (ftac self_quotient 1);
   390 by (ftac self_quotient 1);
   391 by (assume_tac 1);
   391 by (assume_tac 1);
   392 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
   392 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
   393 qed "self_remainder";
   393 qed "self_remainder";
   394 
   394 
   395 Goal "a ~= Numeral0 ==> a div a = (Numeral1::int)";
   395 Goal "a ~= 0 ==> a div a = (1::int)";
   396 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1);
   396 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1);
   397 qed "zdiv_self";
   397 qed "zdiv_self";
   398 Addsimps [zdiv_self];
   398 Addsimps [zdiv_self];
   399 
   399 
   400 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
   400 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
   401 Goal "a mod a = (Numeral0::int)";
   401 Goal "a mod a = (0::int)";
   402 by (zdiv_undefined_case_tac "a = Numeral0" 1);
   402 by (zdiv_undefined_case_tac "a = 0" 1);
   403 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1);
   403 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1);
   404 qed "zmod_self";
   404 qed "zmod_self";
   405 Addsimps [zmod_self];
   405 Addsimps [zmod_self];
   406 
   406 
   407 
   407 
   408 (*** Computation of division and remainder ***)
   408 (*** Computation of division and remainder ***)
   409 
   409 
   410 Goal "(Numeral0::int) div b = Numeral0";
   410 Goal "(0::int) div b = 0";
   411 by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   411 by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   412 qed "zdiv_zero";
   412 qed "zdiv_zero";
   413 
   413 
   414 Goal "(Numeral0::int) < b ==> -1 div b = -1";
   414 Goal "(0::int) < b ==> -1 div b = -1";
   415 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   415 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   416 qed "div_eq_minus1";
   416 qed "div_eq_minus1";
   417 
   417 
   418 Goal "(Numeral0::int) mod b = Numeral0";
   418 Goal "(0::int) mod b = 0";
   419 by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   419 by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   420 qed "zmod_zero";
   420 qed "zmod_zero";
   421 
   421 
   422 Addsimps [zdiv_zero, zmod_zero];
   422 Addsimps [zdiv_zero, zmod_zero];
   423 
   423 
   424 Goal "(Numeral0::int) < b ==> -1 div b = -1";
   424 Goal "(0::int) < b ==> -1 div b = -1";
   425 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   425 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   426 qed "zdiv_minus1";
   426 qed "zdiv_minus1";
   427 
   427 
   428 Goal "(Numeral0::int) < b ==> -1 mod b = b-Numeral1";
   428 Goal "(0::int) < b ==> -1 mod b = b - 1";
   429 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   429 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   430 qed "zmod_minus1";
   430 qed "zmod_minus1";
   431 
   431 
   432 (** a positive, b positive **)
   432 (** a positive, b positive **)
   433 
   433 
   434 Goal "[| Numeral0 < a;  Numeral0 <= b |] ==> a div b = fst (posDivAlg(a,b))";
   434 Goal "[| 0 < a;  0 <= b |] ==> a div b = fst (posDivAlg(a,b))";
   435 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   435 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   436 qed "div_pos_pos";
   436 qed "div_pos_pos";
   437 
   437 
   438 Goal "[| Numeral0 < a;  Numeral0 <= b |] ==> a mod b = snd (posDivAlg(a,b))";
   438 Goal "[| 0 < a;  0 <= b |] ==> a mod b = snd (posDivAlg(a,b))";
   439 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   439 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   440 qed "mod_pos_pos";
   440 qed "mod_pos_pos";
   441 
   441 
   442 (** a negative, b positive **)
   442 (** a negative, b positive **)
   443 
   443 
   444 Goal "[| a < Numeral0;  Numeral0 < b |] ==> a div b = fst (negDivAlg(a,b))";
   444 Goal "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg(a,b))";
   445 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   445 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   446 qed "div_neg_pos";
   446 qed "div_neg_pos";
   447 
   447 
   448 Goal "[| a < Numeral0;  Numeral0 < b |] ==> a mod b = snd (negDivAlg(a,b))";
   448 Goal "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg(a,b))";
   449 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   449 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   450 qed "mod_neg_pos";
   450 qed "mod_neg_pos";
   451 
   451 
   452 (** a positive, b negative **)
   452 (** a positive, b negative **)
   453 
   453 
   454 Goal "[| Numeral0 < a;  b < Numeral0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))";
   454 Goal "[| 0 < a;  b < 0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))";
   455 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   455 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   456 qed "div_pos_neg";
   456 qed "div_pos_neg";
   457 
   457 
   458 Goal "[| Numeral0 < a;  b < Numeral0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))";
   458 Goal "[| 0 < a;  b < 0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))";
   459 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   459 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   460 qed "mod_pos_neg";
   460 qed "mod_pos_neg";
   461 
   461 
   462 (** a negative, b negative **)
   462 (** a negative, b negative **)
   463 
   463 
   464 Goal "[| a < Numeral0;  b <= Numeral0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))";
   464 Goal "[| a < 0;  b <= 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))";
   465 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   465 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   466 qed "div_neg_neg";
   466 qed "div_neg_neg";
   467 
   467 
   468 Goal "[| a < Numeral0;  b <= Numeral0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))";
   468 Goal "[| a < 0;  b <= 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))";
   469 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   469 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   470 qed "mod_neg_neg";
   470 qed "mod_neg_neg";
   471 
   471 
   472 Addsimps (map (read_instantiate_sg (sign_of (the_context ()))
   472 Addsimps (map (read_instantiate_sg (sign_of (the_context ()))
   473 	       [("a", "number_of ?v"), ("b", "number_of ?w")])
   473 	       [("a", "number_of ?v"), ("b", "number_of ?w")])
   476 	   posDivAlg_eqn, negDivAlg_eqn]);
   476 	   posDivAlg_eqn, negDivAlg_eqn]);
   477 
   477 
   478 
   478 
   479 (** Special-case simplification **)
   479 (** Special-case simplification **)
   480 
   480 
   481 Goal "a mod (Numeral1::int) = Numeral0";
   481 Goal "a mod (1::int) = 0";
   482 by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_sign 1);
   482 by (cut_inst_tac [("a","a"),("b","1")] pos_mod_sign 1);
   483 by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_bound 2);
   483 by (cut_inst_tac [("a","a"),("b","1")] pos_mod_bound 2);
   484 by Auto_tac;
   484 by Auto_tac;
   485 qed "zmod_1";
   485 qed "zmod_1";
   486 Addsimps [zmod_1];
   486 Addsimps [zmod_1];
   487 
   487 
   488 Goal "a div (Numeral1::int) = a";
   488 Goal "a div (1::int) = a";
   489 by (cut_inst_tac [("a","a"),("b","Numeral1")] zmod_zdiv_equality 1);
   489 by (cut_inst_tac [("a","a"),("b","1")] zmod_zdiv_equality 1);
   490 by Auto_tac;
   490 by Auto_tac;
   491 qed "zdiv_1";
   491 qed "zdiv_1";
   492 Addsimps [zdiv_1];
   492 Addsimps [zdiv_1];
   493 
   493 
   494 Goal "a mod (-1::int) = Numeral0";
   494 Goal "a mod (-1::int) = 0";
   495 by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_sign 1);
   495 by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_sign 1);
   496 by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_bound 2);
   496 by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_bound 2);
   497 by Auto_tac;
   497 by Auto_tac;
   498 qed "zmod_minus1_right";
   498 qed "zmod_minus1_right";
   499 Addsimps [zmod_minus1_right];
   499 Addsimps [zmod_minus1_right];
   502 by (cut_inst_tac [("a","a"),("b","-1")] zmod_zdiv_equality 1);
   502 by (cut_inst_tac [("a","a"),("b","-1")] zmod_zdiv_equality 1);
   503 by Auto_tac;
   503 by Auto_tac;
   504 qed "zdiv_minus1_right";
   504 qed "zdiv_minus1_right";
   505 Addsimps [zdiv_minus1_right];
   505 Addsimps [zdiv_minus1_right];
   506 
   506 
       
   507 (** The last remaining cases: 1 div z and 1 mod z **)
       
   508 
       
   509 Addsimps (map (fn th => int_0_less_1 RS inst "b" "number_of ?w" th) 
       
   510               [div_pos_pos, div_pos_neg, mod_pos_pos, mod_pos_neg]);
       
   511 
       
   512 Addsimps (map (read_instantiate_sg (sign_of (the_context ()))
       
   513 	       [("a", "1"), ("b", "number_of ?w")])
       
   514 	  [posDivAlg_eqn, negDivAlg_eqn]);
       
   515 
   507 
   516 
   508 (*** Monotonicity in the first argument (divisor) ***)
   517 (*** Monotonicity in the first argument (divisor) ***)
   509 
   518 
   510 Goal "[| a <= a';  Numeral0 < (b::int) |] ==> a div b <= a' div b";
   519 Goal "[| a <= a';  0 < (b::int) |] ==> a div b <= a' div b";
   511 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   520 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   512 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
   521 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
   513 by (rtac unique_quotient_lemma 1);
   522 by (rtac unique_quotient_lemma 1);
   514 by (etac subst 1);
   523 by (etac subst 1);
   515 by (etac subst 1);
   524 by (etac subst 1);
   516 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
   525 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
   517 qed "zdiv_mono1";
   526 qed "zdiv_mono1";
   518 
   527 
   519 Goal "[| a <= a';  (b::int) < Numeral0 |] ==> a' div b <= a div b";
   528 Goal "[| a <= a';  (b::int) < 0 |] ==> a' div b <= a div b";
   520 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   529 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   521 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
   530 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
   522 by (rtac unique_quotient_lemma_neg 1);
   531 by (rtac unique_quotient_lemma_neg 1);
   523 by (etac subst 1);
   532 by (etac subst 1);
   524 by (etac subst 1);
   533 by (etac subst 1);
   526 qed "zdiv_mono1_neg";
   535 qed "zdiv_mono1_neg";
   527 
   536 
   528 
   537 
   529 (*** Monotonicity in the second argument (dividend) ***)
   538 (*** Monotonicity in the second argument (dividend) ***)
   530 
   539 
   531 Goal "[| b*q + r = b'*q' + r';  Numeral0 <= b'*q' + r';  \
   540 Goal "[| b*q + r = b'*q' + r';  0 <= b'*q' + r';  \
   532 \        r' < b';  Numeral0 <= r;  Numeral0 < b';  b' <= b |]  \
   541 \        r' < b';  0 <= r;  0 < b';  b' <= b |]  \
   533 \     ==> q <= (q'::int)";
   542 \     ==> q <= (q'::int)";
   534 by (subgoal_tac "Numeral0 <= q'" 1);
   543 by (subgoal_tac "0 <= q'" 1);
   535  by (subgoal_tac "Numeral0 < b'*(q' + Numeral1)" 2);
   544  by (subgoal_tac "0 < b'*(q' + 1)" 2);
   536   by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
   545   by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
   537  by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2);
   546  by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2);
   538 by (subgoal_tac "b*q < b*(q' + Numeral1)" 1);
   547 by (subgoal_tac "b*q < b*(q' + 1)" 1);
   539  by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
   548  by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
   540 by (subgoal_tac "b*q = r' - r + b'*q'" 1);
   549 by (subgoal_tac "b*q = r' - r + b'*q'" 1);
   541  by (Simp_tac 2);
   550  by (Simp_tac 2);
   542 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
   551 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
   543 by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1);
   552 by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1);
   544 by (rtac zmult_zle_mono1 1);
   553 by (rtac zmult_zle_mono1 1);
   545 by Auto_tac;
   554 by Auto_tac;
   546 qed "zdiv_mono2_lemma";
   555 qed "zdiv_mono2_lemma";
   547 
   556 
   548 Goal "[| (Numeral0::int) <= a;  Numeral0 < b';  b' <= b |]  \
   557 Goal "[| (0::int) <= a;  0 < b';  b' <= b |]  \
   549 \     ==> a div b <= a div b'";
   558 \     ==> a div b <= a div b'";
   550 by (subgoal_tac "b ~= Numeral0" 1);
   559 by (subgoal_tac "b ~= 0" 1);
   551 by (arith_tac 2);
   560 by (arith_tac 2);
   552 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   561 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   553 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
   562 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
   554 by (rtac zdiv_mono2_lemma 1);
   563 by (rtac zdiv_mono2_lemma 1);
   555 by (etac subst 1);
   564 by (etac subst 1);
   556 by (etac subst 1);
   565 by (etac subst 1);
   557 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
   566 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
   558 qed "zdiv_mono2";
   567 qed "zdiv_mono2";
   559 
   568 
   560 Goal "[| b*q + r = b'*q' + r';  b'*q' + r' < Numeral0;  \
   569 Goal "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;  \
   561 \        r < b;  Numeral0 <= r';  Numeral0 < b';  b' <= b |]  \
   570 \        r < b;  0 <= r';  0 < b';  b' <= b |]  \
   562 \     ==> q' <= (q::int)";
   571 \     ==> q' <= (q::int)";
   563 by (subgoal_tac "q' < Numeral0" 1);
   572 by (subgoal_tac "q' < 0" 1);
   564  by (subgoal_tac "b'*q' < Numeral0" 2);
   573  by (subgoal_tac "b'*q' < 0" 2);
   565   by (arith_tac 3);
   574   by (arith_tac 3);
   566  by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2);
   575  by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2);
   567 by (subgoal_tac "b*q' < b*(q + Numeral1)" 1);
   576 by (subgoal_tac "b*q' < b*(q + 1)" 1);
   568  by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
   577  by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
   569 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
   578 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
   570 by (subgoal_tac "b*q' <= b'*q'" 1);
   579 by (subgoal_tac "b*q' <= b'*q'" 1);
   571  by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2);
   580  by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2);
   572 by (subgoal_tac "b'*q' < b + b*q" 1);
   581 by (subgoal_tac "b'*q' < b + b*q" 1);
   573  by (Asm_simp_tac 2);
   582  by (Asm_simp_tac 2);
   574 by (arith_tac 1);
   583 by (arith_tac 1);
   575 qed "zdiv_mono2_neg_lemma";
   584 qed "zdiv_mono2_neg_lemma";
   576 
   585 
   577 Goal "[| a < (Numeral0::int);  Numeral0 < b';  b' <= b |]  \
   586 Goal "[| a < (0::int);  0 < b';  b' <= b |]  \
   578 \     ==> a div b' <= a div b";
   587 \     ==> a div b' <= a div b";
   579 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   588 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
   580 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
   589 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
   581 by (rtac zdiv_mono2_neg_lemma 1);
   590 by (rtac zdiv_mono2_neg_lemma 1);
   582 by (etac subst 1);
   591 by (etac subst 1);
   587 
   596 
   588 (*** More algebraic laws for div and mod ***)
   597 (*** More algebraic laws for div and mod ***)
   589 
   598 
   590 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   599 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   591 
   600 
   592 Goal "[| quorem((b,c),(q,r));  c ~= Numeral0 |] \
   601 Goal "[| quorem((b,c),(q,r));  c ~= 0 |] \
   593 \     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
   602 \     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
   594 by (auto_tac
   603 by (auto_tac
   595     (claset(),
   604     (claset(),
   596      simpset() addsimps split_ifs@
   605      simpset() addsimps split_ifs@
   597                         [quorem_def, linorder_neq_iff, 
   606                         [quorem_def, linorder_neq_iff, 
   600 			 neg_mod_sign, neg_mod_bound]));
   609 			 neg_mod_sign, neg_mod_bound]));
   601 by (ALLGOALS(rtac zmod_zdiv_equality));
   610 by (ALLGOALS(rtac zmod_zdiv_equality));
   602 val lemma = result();
   611 val lemma = result();
   603 
   612 
   604 Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)";
   613 Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)";
   605 by (zdiv_undefined_case_tac "c = Numeral0" 1);
   614 by (zdiv_undefined_case_tac "c = 0" 1);
   606 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
   615 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
   607 qed "zdiv_zmult1_eq";
   616 qed "zdiv_zmult1_eq";
   608 
   617 
   609 Goal "(a*b) mod c = a*(b mod c) mod (c::int)";
   618 Goal "(a*b) mod c = a*(b mod c) mod (c::int)";
   610 by (zdiv_undefined_case_tac "c = Numeral0" 1);
   619 by (zdiv_undefined_case_tac "c = 0" 1);
   611 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
   620 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
   612 qed "zmod_zmult1_eq";
   621 qed "zmod_zmult1_eq";
   613 
   622 
   614 Goal "(a*b) mod (c::int) = ((a mod c) * b) mod c";
   623 Goal "(a*b) mod (c::int) = ((a mod c) * b) mod c";
   615 by (rtac trans 1);
   624 by (rtac trans 1);
   621 Goal "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c";
   630 Goal "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c";
   622 by (rtac (zmod_zmult1_eq' RS trans) 1);
   631 by (rtac (zmod_zmult1_eq' RS trans) 1);
   623 by (rtac zmod_zmult1_eq 1);
   632 by (rtac zmod_zmult1_eq 1);
   624 qed "zmod_zmult_distrib";
   633 qed "zmod_zmult_distrib";
   625 
   634 
   626 Goal "b ~= (Numeral0::int) ==> (a*b) div b = a";
   635 Goal "b ~= (0::int) ==> (a*b) div b = a";
   627 by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1);
   636 by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1);
   628 qed "zdiv_zmult_self1";
   637 qed "zdiv_zmult_self1";
   629 
   638 
   630 Goal "b ~= (Numeral0::int) ==> (b*a) div b = a";
   639 Goal "b ~= (0::int) ==> (b*a) div b = a";
   631 by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1);
   640 by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1);
   632 qed "zdiv_zmult_self2";
   641 qed "zdiv_zmult_self2";
   633 
   642 
   634 Addsimps [zdiv_zmult_self1, zdiv_zmult_self2];
   643 Addsimps [zdiv_zmult_self1, zdiv_zmult_self2];
   635 
   644 
   636 Goal "(a*b) mod b = (Numeral0::int)";
   645 Goal "(a*b) mod b = (0::int)";
   637 by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1);
   646 by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1);
   638 qed "zmod_zmult_self1";
   647 qed "zmod_zmult_self1";
   639 
   648 
   640 Goal "(b*a) mod b = (Numeral0::int)";
   649 Goal "(b*a) mod b = (0::int)";
   641 by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1);
   650 by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1);
   642 qed "zmod_zmult_self2";
   651 qed "zmod_zmult_self2";
   643 
   652 
   644 Addsimps [zmod_zmult_self1, zmod_zmult_self2];
   653 Addsimps [zmod_zmult_self1, zmod_zmult_self2];
   645 
   654 
   646 Goal "(m mod d = Numeral0) = (EX q::int. m = d*q)";
   655 Goal "(m mod d = 0) = (EX q::int. m = d*q)";
   647 by (cut_inst_tac [("a","m"),("b","d")] zmod_zdiv_equality 1);
   656 by (cut_inst_tac [("a","m"),("b","d")] zmod_zdiv_equality 1);
   648 by Auto_tac;  
   657 by Auto_tac;  
   649 qed "zmod_eq_0_iff";
   658 qed "zmod_eq_0_iff";
   650 AddSDs [zmod_eq_0_iff RS iffD1];
   659 AddSDs [zmod_eq_0_iff RS iffD1];
   651 
   660 
   652 
   661 
   653 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   662 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   654 
   663 
   655 Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= Numeral0 |] \
   664 Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= 0 |] \
   656 \     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
   665 \     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
   657 by (auto_tac
   666 by (auto_tac
   658     (claset(),
   667     (claset(),
   659      simpset() addsimps split_ifs@
   668      simpset() addsimps split_ifs@
   660                         [quorem_def, linorder_neq_iff, 
   669                         [quorem_def, linorder_neq_iff, 
   664 by (ALLGOALS(rtac zmod_zdiv_equality));
   673 by (ALLGOALS(rtac zmod_zdiv_equality));
   665 val lemma = result();
   674 val lemma = result();
   666 
   675 
   667 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   676 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   668 Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)";
   677 Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)";
   669 by (zdiv_undefined_case_tac "c = Numeral0" 1);
   678 by (zdiv_undefined_case_tac "c = 0" 1);
   670 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   679 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   671 			       MRS lemma RS quorem_div]) 1);
   680 			       MRS lemma RS quorem_div]) 1);
   672 qed "zdiv_zadd1_eq";
   681 qed "zdiv_zadd1_eq";
   673 
   682 
   674 Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c";
   683 Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c";
   675 by (zdiv_undefined_case_tac "c = Numeral0" 1);
   684 by (zdiv_undefined_case_tac "c = 0" 1);
   676 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   685 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   677 			       MRS lemma RS quorem_mod]) 1);
   686 			       MRS lemma RS quorem_mod]) 1);
   678 qed "zmod_zadd1_eq";
   687 qed "zmod_zadd1_eq";
   679 
   688 
   680 Goal "(a mod b) div b = (Numeral0::int)";
   689 Goal "(a mod b) div b = (0::int)";
   681 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   690 by (zdiv_undefined_case_tac "b = 0" 1);
   682 by (auto_tac (claset(), 
   691 by (auto_tac (claset(), 
   683        simpset() addsimps [linorder_neq_iff, 
   692        simpset() addsimps [linorder_neq_iff, 
   684 			   pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, 
   693 			   pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, 
   685 			   neg_mod_sign, neg_mod_bound, div_neg_neg_trivial]));
   694 			   neg_mod_sign, neg_mod_bound, div_neg_neg_trivial]));
   686 qed "mod_div_trivial";
   695 qed "mod_div_trivial";
   687 Addsimps [mod_div_trivial];
   696 Addsimps [mod_div_trivial];
   688 
   697 
   689 Goal "(a mod b) mod b = a mod (b::int)";
   698 Goal "(a mod b) mod b = a mod (b::int)";
   690 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   699 by (zdiv_undefined_case_tac "b = 0" 1);
   691 by (auto_tac (claset(), 
   700 by (auto_tac (claset(), 
   692        simpset() addsimps [linorder_neq_iff, 
   701        simpset() addsimps [linorder_neq_iff, 
   693 			   pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, 
   702 			   pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, 
   694 			   neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial]));
   703 			   neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial]));
   695 qed "mod_mod_trivial";
   704 qed "mod_mod_trivial";
   708 by (Simp_tac 1);
   717 by (Simp_tac 1);
   709 by (rtac (zmod_zadd1_eq RS sym) 1);
   718 by (rtac (zmod_zadd1_eq RS sym) 1);
   710 qed "zmod_zadd_right_eq";
   719 qed "zmod_zadd_right_eq";
   711 
   720 
   712 
   721 
   713 Goal "a ~= (Numeral0::int) ==> (a+b) div a = b div a + Numeral1";
   722 Goal "a ~= (0::int) ==> (a+b) div a = b div a + 1";
   714 by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
   723 by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
   715 qed "zdiv_zadd_self1";
   724 qed "zdiv_zadd_self1";
   716 
   725 
   717 Goal "a ~= (Numeral0::int) ==> (b+a) div a = b div a + Numeral1";
   726 Goal "a ~= (0::int) ==> (b+a) div a = b div a + 1";
   718 by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
   727 by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
   719 qed "zdiv_zadd_self2";
   728 qed "zdiv_zadd_self2";
   720 Addsimps [zdiv_zadd_self1, zdiv_zadd_self2];
   729 Addsimps [zdiv_zadd_self1, zdiv_zadd_self2];
   721 
   730 
   722 Goal "(a+b) mod a = b mod (a::int)";
   731 Goal "(a+b) mod a = b mod (a::int)";
   723 by (zdiv_undefined_case_tac "a = Numeral0" 1);
   732 by (zdiv_undefined_case_tac "a = 0" 1);
   724 by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
   733 by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
   725 qed "zmod_zadd_self1";
   734 qed "zmod_zadd_self1";
   726 
   735 
   727 Goal "(b+a) mod a = b mod (a::int)";
   736 Goal "(b+a) mod a = b mod (a::int)";
   728 by (zdiv_undefined_case_tac "a = Numeral0" 1);
   737 by (zdiv_undefined_case_tac "a = 0" 1);
   729 by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
   738 by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
   730 qed "zmod_zadd_self2";
   739 qed "zmod_zadd_self2";
   731 Addsimps [zmod_zadd_self1, zmod_zadd_self2];
   740 Addsimps [zmod_zadd_self1, zmod_zadd_self2];
   732 
   741 
   733 
   742 
   737   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
   746   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
   738   to cause particular problems.*)
   747   to cause particular problems.*)
   739 
   748 
   740 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
   749 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
   741 
   750 
   742 Goal "[| (Numeral0::int) < c;  b < r;  r <= Numeral0 |] ==> b*c < b*(q mod c) + r";
   751 Goal "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r";
   743 by (subgoal_tac "b * (c - q mod c) < r * Numeral1" 1);
   752 by (subgoal_tac "b * (c - q mod c) < r * 1" 1);
   744 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
   753 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
   745 by (rtac order_le_less_trans 1);
   754 by (rtac order_le_less_trans 1);
   746 by (etac zmult_zless_mono1 2);
   755 by (etac zmult_zless_mono1 2);
   747 by (rtac zmult_zle_mono2_neg 1);
   756 by (rtac zmult_zle_mono2_neg 1);
   748 by (auto_tac
   757 by (auto_tac
   749     (claset(),
   758     (claset(),
   750      simpset() addsimps zcompare_rls@
   759      simpset() addsimps zcompare_rls@
   751                         [zadd_commute, add1_zle_eq, pos_mod_bound]));
   760                         [inst "z" "1" zadd_commute, add1_zle_eq, 
       
   761                          pos_mod_bound]));
   752 val lemma1 = result();
   762 val lemma1 = result();
   753 
   763 
   754 Goal "[| (Numeral0::int) < c;   b < r;  r <= Numeral0 |] ==> b * (q mod c) + r <= Numeral0";
   764 Goal "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0";
   755 by (subgoal_tac "b * (q mod c) <= Numeral0" 1);
   765 by (subgoal_tac "b * (q mod c) <= 0" 1);
   756 by (arith_tac 1);
   766 by (arith_tac 1);
   757 by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1);
   767 by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1);
   758 val lemma2 = result();
   768 val lemma2 = result();
   759 
   769 
   760 Goal "[| (Numeral0::int) < c;  Numeral0 <= r;  r < b |] ==> Numeral0 <= b * (q mod c) + r";
   770 Goal "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r";
   761 by (subgoal_tac "Numeral0 <= b * (q mod c)" 1);
   771 by (subgoal_tac "0 <= b * (q mod c)" 1);
   762 by (arith_tac 1);
   772 by (arith_tac 1);
   763 by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1);
   773 by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1);
   764 val lemma3 = result();
   774 val lemma3 = result();
   765 
   775 
   766 Goal "[| (Numeral0::int) < c; Numeral0 <= r; r < b |] ==> b * (q mod c) + r < b * c";
   776 Goal "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c";
   767 by (subgoal_tac "r * Numeral1 < b * (c - q mod c)" 1);
   777 by (subgoal_tac "r * 1 < b * (c - q mod c)" 1);
   768 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
   778 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
   769 by (rtac order_less_le_trans 1);
   779 by (rtac order_less_le_trans 1);
   770 by (etac zmult_zless_mono1 1);
   780 by (etac zmult_zless_mono1 1);
   771 by (rtac zmult_zle_mono2 2);
   781 by (rtac zmult_zle_mono2 2);
   772 by (auto_tac
   782 by (auto_tac
   773     (claset(),
   783     (claset(),
   774      simpset() addsimps zcompare_rls@
   784      simpset() addsimps zcompare_rls@
   775                         [zadd_commute, add1_zle_eq, pos_mod_bound]));
   785                         [inst "z" "1" zadd_commute, add1_zle_eq,
       
   786                          pos_mod_bound]));
   776 val lemma4 = result();
   787 val lemma4 = result();
   777 
   788 
   778 Goal "[| quorem ((a,b), (q,r));  b ~= Numeral0;  Numeral0 < c |] \
   789 Goal "[| quorem ((a,b), (q,r));  b ~= 0;  0 < c |] \
   779 \     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
   790 \     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
   780 by (auto_tac  
   791 by (auto_tac  
   781     (claset(),
   792     (claset(),
   782      simpset() addsimps zmult_ac@
   793      simpset() addsimps zmult_ac@
   783                         [zmod_zdiv_equality, quorem_def, linorder_neq_iff,
   794                         [zmod_zdiv_equality, quorem_def, linorder_neq_iff,
   784 			 int_0_less_mult_iff,
   795 			 int_0_less_mult_iff,
   785 			 zadd_zmult_distrib2 RS sym,
   796 			 zadd_zmult_distrib2 RS sym,
   786 			 lemma1, lemma2, lemma3, lemma4]));
   797 			 lemma1, lemma2, lemma3, lemma4]));
   787 val lemma = result();
   798 val lemma = result();
   788 
   799 
   789 Goal "(Numeral0::int) < c ==> a div (b*c) = (a div b) div c";
   800 Goal "(0::int) < c ==> a div (b*c) = (a div b) div c";
   790 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   801 by (zdiv_undefined_case_tac "b = 0" 1);
   791 by (force_tac (claset(),
   802 by (force_tac (claset(),
   792 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, 
   803 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, 
   793 				   zmult_eq_0_iff]) 1);
   804 				   zmult_eq_0_iff]) 1);
   794 qed "zdiv_zmult2_eq";
   805 qed "zdiv_zmult2_eq";
   795 
   806 
   796 Goal "(Numeral0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b";
   807 Goal "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b";
   797 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   808 by (zdiv_undefined_case_tac "b = 0" 1);
   798 by (force_tac (claset(),
   809 by (force_tac (claset(),
   799 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, 
   810 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, 
   800 				   zmult_eq_0_iff]) 1);
   811 				   zmult_eq_0_iff]) 1);
   801 qed "zmod_zmult2_eq";
   812 qed "zmod_zmult2_eq";
   802 
   813 
   803 
   814 
   804 (*** Cancellation of common factors in "div" ***)
   815 (*** Cancellation of common factors in "div" ***)
   805 
   816 
   806 Goal "[| (Numeral0::int) < b;  c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b";
   817 Goal "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b";
   807 by (stac zdiv_zmult2_eq 1);
   818 by (stac zdiv_zmult2_eq 1);
   808 by Auto_tac;
   819 by Auto_tac;
   809 val lemma1 = result();
   820 val lemma1 = result();
   810 
   821 
   811 Goal "[| b < (Numeral0::int);  c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b";
   822 Goal "[| b < (0::int);  c ~= 0 |] ==> (c*a) div (c*b) = a div b";
   812 by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1);
   823 by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1);
   813 by (rtac lemma1 2);
   824 by (rtac lemma1 2);
   814 by Auto_tac;
   825 by Auto_tac;
   815 val lemma2 = result();
   826 val lemma2 = result();
   816 
   827 
   817 Goal "c ~= (Numeral0::int) ==> (c*a) div (c*b) = a div b";
   828 Goal "c ~= (0::int) ==> (c*a) div (c*b) = a div b";
   818 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   829 by (zdiv_undefined_case_tac "b = 0" 1);
   819 by (auto_tac
   830 by (auto_tac
   820     (claset(), 
   831     (claset(), 
   821      simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
   832      simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
   822 			 lemma1, lemma2]));
   833 			 lemma1, lemma2]));
   823 qed "zdiv_zmult_zmult1";
   834 qed "zdiv_zmult_zmult1";
   824 
   835 
   825 Goal "c ~= (Numeral0::int) ==> (a*c) div (b*c) = a div b";
   836 Goal "c ~= (0::int) ==> (a*c) div (b*c) = a div b";
   826 by (dtac zdiv_zmult_zmult1 1);
   837 by (dtac zdiv_zmult_zmult1 1);
   827 by (auto_tac (claset(), simpset() addsimps [zmult_commute]));
   838 by (auto_tac (claset(), simpset() addsimps [zmult_commute]));
   828 qed "zdiv_zmult_zmult2";
   839 qed "zdiv_zmult_zmult2";
   829 
   840 
   830 
   841 
   831 
   842 
   832 (*** Distribution of factors over "mod" ***)
   843 (*** Distribution of factors over "mod" ***)
   833 
   844 
   834 Goal "[| (Numeral0::int) < b;  c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)";
   845 Goal "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)";
   835 by (stac zmod_zmult2_eq 1);
   846 by (stac zmod_zmult2_eq 1);
   836 by Auto_tac;
   847 by Auto_tac;
   837 val lemma1 = result();
   848 val lemma1 = result();
   838 
   849 
   839 Goal "[| b < (Numeral0::int);  c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)";
   850 Goal "[| b < (0::int);  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)";
   840 by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1);
   851 by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1);
   841 by (rtac lemma1 2);
   852 by (rtac lemma1 2);
   842 by Auto_tac;
   853 by Auto_tac;
   843 val lemma2 = result();
   854 val lemma2 = result();
   844 
   855 
   845 Goal "(c*a) mod (c*b) = (c::int) * (a mod b)";
   856 Goal "(c*a) mod (c*b) = (c::int) * (a mod b)";
   846 by (zdiv_undefined_case_tac "b = Numeral0" 1);
   857 by (zdiv_undefined_case_tac "b = 0" 1);
   847 by (zdiv_undefined_case_tac "c = Numeral0" 1);
   858 by (zdiv_undefined_case_tac "c = 0" 1);
   848 by (auto_tac
   859 by (auto_tac
   849     (claset(), 
   860     (claset(), 
   850      simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
   861      simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
   851 			 lemma1, lemma2]));
   862 			 lemma1, lemma2]));
   852 qed "zmod_zmult_zmult1";
   863 qed "zmod_zmult_zmult1";
   859 
   870 
   860 (*** Speeding up the division algorithm with shifting ***)
   871 (*** Speeding up the division algorithm with shifting ***)
   861 
   872 
   862 (** computing "div" by shifting **)
   873 (** computing "div" by shifting **)
   863 
   874 
   864 Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) div (2*a) = b div a";
   875 Goal "(0::int) <= a ==> (1 + 2*b) div (2*a) = b div a";
   865 by (zdiv_undefined_case_tac "a = Numeral0" 1);
   876 by (zdiv_undefined_case_tac "a = 0" 1);
   866 by (subgoal_tac "Numeral1 <= a" 1);
   877 by (subgoal_tac "1 <= a" 1);
   867  by (arith_tac 2);
   878  by (arith_tac 2);
   868 by (subgoal_tac "Numeral1 < a * 2" 1);
   879 by (subgoal_tac "1 < a * 2" 1);
   869  by (arith_tac 2);
   880  by (arith_tac 2);
   870 by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
   881 by (subgoal_tac "2*(1 + b mod a) <= 2*a" 1);
   871  by (rtac zmult_zle_mono2 2);
   882  by (rtac zmult_zle_mono2 2);
   872 by (auto_tac (claset(),
   883 by (auto_tac (claset(),
   873 	      simpset() addsimps [zadd_commute, zmult_commute, 
   884 	      simpset() addsimps [inst "z" "1" zadd_commute, zmult_commute, 
   874 				  add1_zle_eq, pos_mod_bound]));
   885 				  add1_zle_eq, pos_mod_bound]));
   875 by (stac zdiv_zadd1_eq 1);
   886 by (stac zdiv_zadd1_eq 1);
   876 by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2, 
   887 by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2, 
   877 				      div_pos_pos_trivial]) 1);
   888 				      div_pos_pos_trivial]) 1);
   878 by (stac div_pos_pos_trivial 1);
   889 by (stac div_pos_pos_trivial 1);
   879 by (asm_simp_tac (simpset() 
   890 by (asm_simp_tac (simpset() 
   880            addsimps [mod_pos_pos_trivial,
   891            addsimps [mod_pos_pos_trivial,
   881                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
   892                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
   882 by (auto_tac (claset(),
   893 by (auto_tac (claset(),
   883 	      simpset() addsimps [mod_pos_pos_trivial]));
   894 	      simpset() addsimps [mod_pos_pos_trivial]));
   884 by (subgoal_tac "Numeral0 <= b mod a" 1);
   895 by (subgoal_tac "0 <= b mod a" 1);
   885  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
   896  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
   886 by (arith_tac 1);
   897 by (arith_tac 1);
   887 qed "pos_zdiv_mult_2";
   898 qed "pos_zdiv_mult_2";
   888 
   899 
   889 
   900 
   890 Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) div (2*a) = (b+Numeral1) div a";
   901 Goal "a <= (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a";
   891 by (subgoal_tac "(Numeral1 + 2*(-b-Numeral1)) div (2 * (-a)) = (-b-Numeral1) div (-a)" 1);
   902 by (subgoal_tac "(1 + 2*(-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)" 1);
   892 by (rtac pos_zdiv_mult_2 2);
   903 by (rtac pos_zdiv_mult_2 2);
   893 by (auto_tac (claset(),
   904 by (auto_tac (claset(),
   894 	      simpset() addsimps [zmult_zminus_right]));
   905 	      simpset() addsimps [zmult_zminus_right]));
   895 by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
   906 by (subgoal_tac "(-1 - (2 * b)) = - (1 + (2 * b))" 1);
   896 by (Simp_tac 2);
   907 by (Simp_tac 2);
   897 by (asm_full_simp_tac (HOL_ss
   908 by (asm_full_simp_tac (HOL_ss
   898 		       addsimps [zdiv_zminus_zminus, zdiff_def,
   909 		       addsimps [zdiv_zminus_zminus, zdiff_def,
   899 				 zminus_zadd_distrib RS sym]) 1);
   910 				 zminus_zadd_distrib RS sym]) 1);
   900 qed "neg_zdiv_mult_2";
   911 qed "neg_zdiv_mult_2";
   901 
   912 
   902 
   913 
   903 (*Not clear why this must be proved separately; probably number_of causes
   914 (*Not clear why this must be proved separately; probably number_of causes
   904   simplification problems*)
   915   simplification problems*)
   905 Goal "~ Numeral0 <= x ==> x <= (Numeral0::int)";
   916 Goal "~ 0 <= x ==> x <= (0::int)";
   906 by Auto_tac;
   917 by Auto_tac;
   907 val lemma = result();
   918 val lemma = result();
   908 
   919 
   909 Goal "number_of (v BIT b) div number_of (w BIT False) = \
   920 Goal "number_of (v BIT b) div number_of (w BIT False) = \
   910 \         (if ~b | (Numeral0::int) <= number_of w                   \
   921 \         (if ~b | (0::int) <= number_of w                   \
   911 \          then number_of v div (number_of w)    \
   922 \          then number_of v div (number_of w)    \
   912 \          else (number_of v + (Numeral1::int)) div (number_of w))";
   923 \          else (number_of v + (1::int)) div (number_of w))";
   913 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
   924 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
       
   925 by (subgoal_tac "2 ~= (0::int)" 1);
       
   926  by (Simp_tac 2);  (*we do this because the next step can't simplify numerals*)
   914 by (asm_simp_tac (simpset()
   927 by (asm_simp_tac (simpset()
   915            delsimps [thm "number_of_reorient"]@bin_arith_extra_simps@bin_rel_simps
   928            delsimps bin_arith_extra_simps
   916  	   addsimps [zdiv_zmult_zmult1, pos_zdiv_mult_2, lemma, 
   929  	   addsimps [zdiv_zmult_zmult1, pos_zdiv_mult_2, lemma, 
   917                      neg_zdiv_mult_2]) 1);
   930                      neg_zdiv_mult_2]) 1);
   918 qed "zdiv_number_of_BIT";
   931 qed "zdiv_number_of_BIT";
   919 Addsimps [zdiv_number_of_BIT];
   932 Addsimps [zdiv_number_of_BIT];
   920 
   933 
   921 
   934 
   922 (** computing "mod" by shifting (proofs resemble those for "div") **)
   935 (** computing "mod" by shifting (proofs resemble those for "div") **)
   923 
   936 
   924 Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) mod (2*a) = Numeral1 + 2 * (b mod a)";
   937 Goal "(0::int) <= a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)";
   925 by (zdiv_undefined_case_tac "a = Numeral0" 1);
   938 by (zdiv_undefined_case_tac "a = 0" 1);
   926 by (subgoal_tac "Numeral1 <= a" 1);
   939 by (subgoal_tac "1 <= a" 1);
   927  by (arith_tac 2);
   940  by (arith_tac 2);
   928 by (subgoal_tac "Numeral1 < a * 2" 1);
   941 by (subgoal_tac "1 < a * 2" 1);
   929  by (arith_tac 2);
   942  by (arith_tac 2);
   930 by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
   943 by (subgoal_tac "2*(1 + b mod a) <= 2*a" 1);
   931  by (rtac zmult_zle_mono2 2);
   944  by (rtac zmult_zle_mono2 2);
   932 by (auto_tac (claset(),
   945 by (auto_tac (claset(),
   933 	      simpset() addsimps [zadd_commute, zmult_commute, 
   946 	      simpset() addsimps [inst "z" "1" zadd_commute, zmult_commute, 
   934 				  add1_zle_eq, pos_mod_bound]));
   947 				  add1_zle_eq, pos_mod_bound]));
   935 by (stac zmod_zadd1_eq 1);
   948 by (stac zmod_zadd1_eq 1);
   936 by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2, 
   949 by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2, 
   937 				      mod_pos_pos_trivial]) 1);
   950 				      mod_pos_pos_trivial]) 1);
   938 by (rtac mod_pos_pos_trivial 1);
   951 by (rtac mod_pos_pos_trivial 1);
   939 by (asm_simp_tac (simpset() 
   952 by (asm_simp_tac (simpset() 
   940                   addsimps [mod_pos_pos_trivial,
   953                   addsimps [mod_pos_pos_trivial,
   941                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
   954                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
   942 by (auto_tac (claset(),
   955 by (auto_tac (claset(),
   943 	      simpset() addsimps [mod_pos_pos_trivial]));
   956 	      simpset() addsimps [mod_pos_pos_trivial]));
   944 by (subgoal_tac "Numeral0 <= b mod a" 1);
   957 by (subgoal_tac "0 <= b mod a" 1);
   945  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
   958  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
   946 by (arith_tac 1);
   959 by (arith_tac 1);
   947 qed "pos_zmod_mult_2";
   960 qed "pos_zmod_mult_2";
   948 
   961 
   949 
   962 
   950 Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) mod (2*a) = 2 * ((b+Numeral1) mod a) - Numeral1";
   963 Goal "a <= (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1";
   951 by (subgoal_tac 
   964 by (subgoal_tac 
   952     "(Numeral1 + 2*(-b-Numeral1)) mod (2*(-a)) = Numeral1 + 2*((-b-Numeral1) mod (-a))" 1);
   965     "(1 + 2*(-b - 1)) mod (2*(-a)) = 1 + 2*((-b - 1) mod (-a))" 1);
   953 by (rtac pos_zmod_mult_2 2);
   966 by (rtac pos_zmod_mult_2 2);
   954 by (auto_tac (claset(),
   967 by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right]));
   955 	      simpset() addsimps [zmult_zminus_right]));
   968 by (subgoal_tac "(-1 - (2 * b)) = - (1 + (2 * b))" 1);
   956 by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
       
   957 by (Simp_tac 2);
   969 by (Simp_tac 2);
   958 by (asm_full_simp_tac (HOL_ss
   970 by (asm_full_simp_tac (HOL_ss
   959 		       addsimps [zmod_zminus_zminus, zdiff_def,
   971 		       addsimps [zmod_zminus_zminus, zdiff_def,
   960 				 zminus_zadd_distrib RS sym]) 1);
   972 				 zminus_zadd_distrib RS sym]) 1);
   961 by (dtac (zminus_equation RS iffD1 RS sym) 1);
   973 by (dtac (zminus_equation RS iffD1 RS sym) 1);
   962 by Auto_tac;
   974 by Auto_tac;
   963 qed "neg_zmod_mult_2";
   975 qed "neg_zmod_mult_2";
   964 
   976 
   965 Goal "number_of (v BIT b) mod number_of (w BIT False) = \
   977 Goal "number_of (v BIT b) mod number_of (w BIT False) = \
   966 \         (if b then \
   978 \         (if b then \
   967 \               if (Numeral0::int) <= number_of w \
   979 \               if (0::int) <= number_of w \
   968 \               then 2 * (number_of v mod number_of w) + Numeral1    \
   980 \               then 2 * (number_of v mod number_of w) + 1    \
   969 \               else 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1  \
   981 \               else 2 * ((number_of v + (1::int)) mod number_of w) - 1  \
   970 \          else 2 * (number_of v mod number_of w))";
   982 \          else 2 * (number_of v mod number_of w))";
   971 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
   983 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
   972 by (asm_simp_tac (simpset()
   984 by (asm_simp_tac (simpset()
   973 		  delsimps bin_arith_extra_simps@bin_rel_simps
   985 		  delsimps bin_arith_extra_simps@bin_rel_simps
   974 		  addsimps [zmod_zmult_zmult1,
   986 		  addsimps [zmod_zmult_zmult1,
   975 			    pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1);
   987 			    pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1);
       
   988 by (Simp_tac 1); 
   976 qed "zmod_number_of_BIT";
   989 qed "zmod_number_of_BIT";
   977 
   990 
   978 Addsimps [zmod_number_of_BIT];
   991 Addsimps [zmod_number_of_BIT];
   979 
   992 
   980 
   993 
   981 (** Quotients of signs **)
   994 (** Quotients of signs **)
   982 
   995 
   983 Goal "[| a < (Numeral0::int);  Numeral0 < b |] ==> a div b < Numeral0";
   996 Goal "[| a < (0::int);  0 < b |] ==> a div b < 0";
   984 by (subgoal_tac "a div b <= -1" 1);
   997 by (subgoal_tac "a div b <= -1" 1);
   985 by (Force_tac 1);
   998 by (Force_tac 1);
   986 by (rtac order_trans 1);
   999 by (rtac order_trans 1);
   987 by (res_inst_tac [("a'","-1")]  zdiv_mono1 1);
  1000 by (res_inst_tac [("a'","-1")]  zdiv_mono1 1);
   988 by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
  1001 by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
   989 qed "div_neg_pos_less0";
  1002 qed "div_neg_pos_less0";
   990 
  1003 
   991 Goal "[| (Numeral0::int) <= a;  b < Numeral0 |] ==> a div b <= Numeral0";
  1004 Goal "[| (0::int) <= a;  b < 0 |] ==> a div b <= 0";
   992 by (dtac zdiv_mono1_neg 1);
  1005 by (dtac zdiv_mono1_neg 1);
   993 by Auto_tac;
  1006 by Auto_tac;
   994 qed "div_nonneg_neg_le0";
  1007 qed "div_nonneg_neg_le0";
   995 
  1008 
   996 Goal "(Numeral0::int) < b ==> (Numeral0 <= a div b) = (Numeral0 <= a)";
  1009 Goal "(0::int) < b ==> (0 <= a div b) = (0 <= a)";
   997 by Auto_tac;
  1010 by Auto_tac;
   998 by (dtac zdiv_mono1 2);
  1011 by (dtac zdiv_mono1 2);
   999 by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
  1012 by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
  1000 by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
  1013 by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
  1001 by (blast_tac (claset() addIs [div_neg_pos_less0]) 1);
  1014 by (blast_tac (claset() addIs [div_neg_pos_less0]) 1);
  1002 qed "pos_imp_zdiv_nonneg_iff";
  1015 qed "pos_imp_zdiv_nonneg_iff";
  1003 
  1016 
  1004 Goal "b < (Numeral0::int) ==> (Numeral0 <= a div b) = (a <= (Numeral0::int))";
  1017 Goal "b < (0::int) ==> (0 <= a div b) = (a <= (0::int))";
  1005 by (stac (zdiv_zminus_zminus RS sym) 1);
  1018 by (stac (zdiv_zminus_zminus RS sym) 1);
  1006 by (stac pos_imp_zdiv_nonneg_iff 1);
  1019 by (stac pos_imp_zdiv_nonneg_iff 1);
  1007 by Auto_tac;
  1020 by Auto_tac;
  1008 qed "neg_imp_zdiv_nonneg_iff";
  1021 qed "neg_imp_zdiv_nonneg_iff";
  1009 
  1022 
  1010 (*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*)
  1023 (*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*)
  1011 Goal "(Numeral0::int) < b ==> (a div b < Numeral0) = (a < Numeral0)";
  1024 Goal "(0::int) < b ==> (a div b < 0) = (a < 0)";
  1012 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
  1025 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
  1013 				      pos_imp_zdiv_nonneg_iff]) 1);
  1026 				      pos_imp_zdiv_nonneg_iff]) 1);
  1014 qed "pos_imp_zdiv_neg_iff";
  1027 qed "pos_imp_zdiv_neg_iff";
  1015 
  1028 
  1016 (*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*)
  1029 (*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*)
  1017 Goal "b < (Numeral0::int) ==> (a div b < Numeral0) = (Numeral0 < a)";
  1030 Goal "b < (0::int) ==> (a div b < 0) = (0 < a)";
  1018 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
  1031 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
  1019 				      neg_imp_zdiv_nonneg_iff]) 1);
  1032 				      neg_imp_zdiv_nonneg_iff]) 1);
  1020 qed "neg_imp_zdiv_neg_iff";
  1033 qed "neg_imp_zdiv_neg_iff";