src/HOL/Integ/IntDiv.thy
changeset 22744 5cbe966d67a2
parent 22091 d13ad9a479f9
child 22802 92026479179e
equal deleted inserted replaced
22743:e2b06bfe471a 22744:5cbe966d67a2
    16 declare zless_nat_conj [simp]
    16 declare zless_nat_conj [simp]
    17 
    17 
    18 constdefs
    18 constdefs
    19   quorem :: "(int*int) * (int*int) => bool"
    19   quorem :: "(int*int) * (int*int) => bool"
    20     --{*definition of quotient and remainder*}
    20     --{*definition of quotient and remainder*}
    21     "quorem == %((a,b), (q,r)).
    21     [code func]: "quorem == %((a,b), (q,r)).
    22                       a = b*q + r &
    22                       a = b*q + r &
    23                       (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
    23                       (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
    24 
    24 
    25   adjust :: "[int, int*int] => int*int"
    25   adjust :: "[int, int*int] => int*int"
    26     --{*for the division algorithm*}
    26     --{*for the division algorithm*}
    27     "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
    27     [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
    28                          else (2*q, r)"
    28                          else (2*q, r)"
    29 
    29 
    30 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
    30 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
    31 consts posDivAlg :: "int*int => int*int"
    31 consts posDivAlg :: "int*int => int*int"
    32 recdef posDivAlg "measure (%(a,b). nat(a - b + 1))"
    32 recdef posDivAlg "measure (%(a,b). nat(a - b + 1))"
    42         else adjust b (negDivAlg(a, 2*b)))"
    42         else adjust b (negDivAlg(a, 2*b)))"
    43 
    43 
    44 text{*algorithm for the general case @{term "b\<noteq>0"}*}
    44 text{*algorithm for the general case @{term "b\<noteq>0"}*}
    45 constdefs
    45 constdefs
    46   negateSnd :: "int*int => int*int"
    46   negateSnd :: "int*int => int*int"
    47     "negateSnd == %(q,r). (q,-r)"
    47     [code func]: "negateSnd == %(q,r). (q,-r)"
    48 
    48 
    49   divAlg :: "int*int => int*int"
    49   divAlg :: "int*int => int*int"
    50     --{*The full division algorithm considers all possible signs for a, b
    50     --{*The full division algorithm considers all possible signs for a, b
    51        including the special case @{text "a=0, b<0"} because 
    51        including the special case @{text "a=0, b<0"} because 
    52        @{term negDivAlg} requires @{term "a<0"}.*}
    52        @{term negDivAlg} requires @{term "a<0"}.*}
    53     "divAlg ==
    53     [code func]: "divAlg ==
    54        %(a,b). if 0\<le>a then
    54        %(a,b). if 0\<le>a then
    55                   if 0\<le>b then posDivAlg (a,b)
    55                   if 0\<le>b then posDivAlg (a,b)
    56                   else if a=0 then (0,0)
    56                   else if a=0 then (0,0)
    57                        else negateSnd (negDivAlg (-a,-b))
    57                        else negateSnd (negDivAlg (-a,-b))
    58                else 
    58                else 
    63   int :: "Divides.div" ..       --{*avoid clash with 'div' token*}
    63   int :: "Divides.div" ..       --{*avoid clash with 'div' token*}
    64 
    64 
    65 text{*The operators are defined with reference to the algorithm, which is
    65 text{*The operators are defined with reference to the algorithm, which is
    66 proved to satisfy the specification.*}
    66 proved to satisfy the specification.*}
    67 defs
    67 defs
    68   div_def:   "a div b == fst (divAlg (a,b))"
    68   div_def [code func]: "a div b == fst (divAlg (a,b))"
    69   mod_def:   "a mod b == snd (divAlg (a,b))"
    69   mod_def [code func]: "a mod b == snd (divAlg (a,b))"
    70 
    70 
    71 
    71 
    72 text{*
    72 text{*
    73 Here is the division algorithm in ML:
    73 Here is the division algorithm in ML:
    74 
    74