src/HOL/Integ/IntDiv.ML

more monotonicity laws for times

(*  Title:      HOL/IntDiv.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1999  University of Cambridge

The division operators div, mod and the divides relation "dvd"
*)

Addsimps [zless_nat_conj];

(*** Uniqueness and monotonicity of quotients and remainders ***)

Goal "[| r' + b*q' <= r + b*q;  #0 <= r';  #0 < b;  r < b |] \
\     ==> q' <= (q::int)";
by (subgoal_tac "r' + b * (q'-q) <= r" 1);
by (simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2]) 2);
by (subgoal_tac "#0 < b * (#1 + q - q')" 1);
by (etac order_le_less_trans 2);
by (full_simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2,
						    zadd_zmult_distrib2]) 2);
by (subgoal_tac "b * q' < b * (#1 + q)" 1);
by (full_simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2,
						    zadd_zmult_distrib2]) 2);
by (Asm_full_simp_tac 1);
qed "unique_quotient_lemma";

Goal "[| r' + b*q' <= r + b*q;  r <= #0;  b < #0;  b < r' |] \
\     ==> q <= (q'::int)";
by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")] 
    unique_quotient_lemma 1);
by (auto_tac (claset(), 
	      simpset() addsimps zcompare_rls@[zmult_zminus_right])); 
qed "unique_quotient_lemma_neg";


Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= #0 |] \
\     ==> q = q'";
by (asm_full_simp_tac 
    (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1);
by Safe_tac; 
by (ALLGOALS Asm_full_simp_tac);
by (REPEAT 
    (blast_tac (claset() addIs [order_antisym]
			 addDs [order_eq_refl RS unique_quotient_lemma, 
				order_eq_refl RS unique_quotient_lemma_neg,
				sym]) 1));
qed "unique_quotient";


Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= #0 |] \
\     ==> r = r'";
by (subgoal_tac "q = q'" 1);
by (blast_tac (claset() addIs [unique_quotient]) 2);
by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
qed "unique_remainder";


(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)

Goal "adjust a b (q,r) = (if #0 <= r-b then (#2*q + #1, r-b)  \
\                         else (#2*q, r))";
by (simp_tac (simpset() addsimps [adjust_def]) 1);
qed "adjust_eq";
Addsimps [adjust_eq];

(*Proving posDivAlg's termination condition*)
val [tc] = posDivAlg.tcs;
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
by (auto_tac (claset(), simpset() addsimps [zmult_2_right]));
val lemma = result();

(* removing the termination condition from the generated theorems *)

bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.rules);

(**use with simproc to avoid re-proving the premise*)
Goal "#0 < b ==> \
\     posDivAlg (a,b) =      \
\      (if a<b then (#0,a) else adjust a b (posDivAlg(a, #2*b)))";
by (rtac (posDivAlg_raw_eqn RS trans) 1);
by (Asm_simp_tac 1);
qed "posDivAlg_eqn";

val posDivAlg_induct = lemma RS posDivAlg.induct;


(*Correctness of posDivAlg: it computes quotients correctly*)
Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
by Auto_tac;
by (ALLGOALS 
    (asm_full_simp_tac (simpset() addsimps [quorem_def,
					    pos_times_pos_is_pos])));
(*base case: a<b*)
by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
(*main argument*)
by (stac posDivAlg_eqn 1);
by (ALLGOALS Asm_simp_tac);
by (etac splitE 1);
by Auto_tac;
(*the "add one" case*)
by (asm_full_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
(*the "just double" case*)
by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
qed_spec_mp "posDivAlg_correct";


(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)

(*Proving negDivAlg's termination condition*)
val [tc] = negDivAlg.tcs;
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
by (auto_tac (claset(), simpset() addsimps [zmult_2_right]));
val lemma = result();

(* removing the termination condition from the generated theorems *)

bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.rules);

(**use with simproc to avoid re-proving the premise*)
Goal "#0 < b ==> \
\     negDivAlg (a,b) =      \
\      (if #0<=a+b then (#-1,a+b) else adjust a b (negDivAlg(a, #2*b)))";
by (rtac (negDivAlg_raw_eqn RS trans) 1);
by (Asm_simp_tac 1);
qed "negDivAlg_eqn";

val negDivAlg_induct = lemma RS negDivAlg.induct;


(*Correctness of negDivAlg: it computes quotients correctly
  It doesn't work if a=0 because the 0/b=0 rather than -1*)
Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
by Auto_tac;
by (ALLGOALS 
    (asm_full_simp_tac (simpset() addsimps [quorem_def,
					    pos_times_pos_is_pos])));
(*base case: 0<=a+b*)
by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
(*main argument*)
by (stac negDivAlg_eqn 1);
by (ALLGOALS Asm_simp_tac);
by (etac splitE 1);
by Auto_tac;
(*the "add one" case*)
by (asm_full_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
(*the "just double" case*)
by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
qed_spec_mp "negDivAlg_correct";


(*** Existence shown by proving the division algorithm to be correct ***)

(*the case a=0*)
Goal "b ~= #0 ==> quorem ((#0,b), (#0,#0))";
by (auto_tac (claset(), 
	      simpset() addsimps [quorem_def, linorder_neq_iff]));
qed "quorem_0";

Goal "posDivAlg (#0, b) = (#0, #0)";
by (stac posDivAlg_raw_eqn 1);
by Auto_tac;
qed "posDivAlg_0";
Addsimps [posDivAlg_0];

Goal "negDivAlg (#-1, b) = (#-1, b-#1)";
by (stac negDivAlg_raw_eqn 1);
by Auto_tac;
qed "negDivAlg_minus1";
Addsimps [negDivAlg_minus1];

Goalw [negateSnd_def] "negateSnd(q,r) = (q,-r)";
by Auto_tac;
qed "negateSnd_eq";
Addsimps [negateSnd_eq];

Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)";
by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
qed "quorem_neg";

Goal "b ~= #0 ==> quorem ((a,b), divAlg(a,b))";
by (auto_tac (claset(), 
	      simpset() addsimps [quorem_0, divAlg_def]));
by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
			       negDivAlg_correct]));
by (auto_tac (claset(), 
	      simpset() addsimps [quorem_def, linorder_neq_iff]));
qed "divAlg_correct";

Goal "b ~= (#0::int) ==> a = b * (a div b) + (a mod b)";
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
by (auto_tac (claset(), 
	      simpset() addsimps [quorem_def, div_def, mod_def]));
qed "zmod_zdiv_equality";  
   (*the name mod_div_equality would hide the other one proved in Divides.ML
     existing users aren't using name spaces for theorems*)

Goal "(#0::int) < b ==> #0 <= a mod b & a mod b < b";
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
by (auto_tac (claset(), 
	      simpset() addsimps [quorem_def, mod_def]));
bind_thm ("pos_mod_sign", result() RS conjunct1);
bind_thm ("pos_mod_bound", result() RS conjunct2);

Goal "b < (#0::int) ==> a mod b <= #0 & b < a mod b";
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
by (auto_tac (claset(), 
	      simpset() addsimps [quorem_def, div_def, mod_def]));
bind_thm ("neg_mod_sign", result() RS conjunct1);
bind_thm ("neg_mod_bound", result() RS conjunct2);


(*** Computation of division and remainder ***)

Goal "(#0::int) div b = #0";
by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "div_zero";

Goal "(#0::int) mod b = #0";
by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
qed "mod_zero";

Addsimps [div_zero, mod_zero];

(** a positive, b positive **)

Goal "[| #0 < a;  #0 < b |] ==> a div b = fst (posDivAlg(a,b))";
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "div_pos_pos";

Goal "[| #0 < a;  #0 < b |] ==> a mod b = snd (posDivAlg(a,b))";
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
qed "mod_pos_pos";

(** a negative, b positive **)

Goal "[| a < #0;  #0 < b |] ==> a div b = fst (negDivAlg(a,b))";
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "div_neg_pos";

Goal "[| a < #0;  #0 < b |] ==> a mod b = snd (negDivAlg(a,b))";
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
qed "mod_neg_pos";

(** a positive, b negative **)

Goal "[| #0 < a;  b < #0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))";
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "div_pos_neg";

Goal "[| #0 < a;  b < #0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))";
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
qed "mod_pos_neg";

(** a negative, b negative **)

Goal "[| a < #0;  b < #0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))";
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
qed "div_neg_neg";

Goal "[| a < #0;  b < #0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))";
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
qed "mod_neg_neg";

Addsimps (map (read_instantiate_sg (sign_of IntDiv.thy)
	       [("a", "number_of ?v"), ("b", "number_of ?w")])
	  [div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg,
	   mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg,
	   posDivAlg_eqn, negDivAlg_eqn]);
	   

(** Special-case simplification **)

Goal "a mod (#1::int) = #0";
by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_sign 1);
by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_bound 2);
by Auto_tac;
qed "zmod_1";
Addsimps [zmod_1];

Goal "a div (#1::int) = a";
by (cut_inst_tac [("a","a"),("b","#1")] zmod_zdiv_equality 1);
by Auto_tac;
qed "zdiv_1";
Addsimps [zdiv_1];

Goal "a mod (#-1::int) = #0";
by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_sign 1);
by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_bound 2);
by Auto_tac;
qed "zmod_minus1";
Addsimps [zmod_minus1];

Goal "a div (#-1::int) = -a";
by (cut_inst_tac [("a","a"),("b","#-1")] zmod_zdiv_equality 1);
by Auto_tac;
qed "zdiv_minus1";
Addsimps [zdiv_minus1];


(** Monotonicity results **)


Goal "[| a <= a';  #0 < (b::int) |] ==> a div b <= a' div b";
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 2);
by Auto_tac;
by (rtac unique_quotient_lemma 1);
by (etac subst 1);
by (etac subst 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
qed "zdiv_mono1";

Goal "[| a <= a';  (b::int) < #0 |] ==> a' div b <= a div b";
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 2);
by Auto_tac;
by (rtac unique_quotient_lemma_neg 1);
by (etac subst 1);
by (etac subst 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [neg_mod_sign,neg_mod_bound])));
qed "zdiv_mono1_neg";



(** The division algorithm in ML **)

fun posDivAlg (a,b) =
  if a<b then (0,a)
  else let val (q,r) = posDivAlg(a, 2*b)
           in  if 0<=r-b then (2*q+1, r-b)
               else (2*q, r)
       end;

fun negDivAlg (a,b) =
  if 0<=a+b then (~1,a+b)
  else let val (q,r) = negDivAlg(a, 2*b)
           in  if 0<=r-b then (2*q+1, r-b)
               else (2*q, r)
       end;

fun negateSnd (q,r:int) = (q,~r);

fun divAlg (a,b) = if 0<=a then 
                      if b>0 then posDivAlg (a,b) 
                       else if a=0 then (0,0)
                            else negateSnd (negDivAlg (~a,~b))
                   else 
                      if 0<b then negDivAlg (a,b)
                      else        negateSnd (posDivAlg (~a,~b));