src/ZF/Integ/IntDiv.thy

'insert' made proper;
'erule' etc.: assm arg;

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

The division operators div, mod
*)

IntDiv = IntArith + OrderArith + 

constdefs
  quorem :: "[i,i] => o"
    "quorem == %<a,b> <q,r>.
                      a = b$*q $+ r &
                      (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"

  adjust :: "[i,i,i] => i"
    "adjust(a,b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
                            else <#2$*q,r>"


(** the division algorithm **)

constdefs posDivAlg :: "i => i"
(*for the case a>=0, b>0*)
(*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*)
    "posDivAlg(ab) ==
       wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
	     ab,
	     %<a,b> f. if (a$<b | b$<=#0) then <#0,a>
                       else adjust(a, b, f ` <a,#2$*b>))"

(**TO BE COMPLETED**)

end