src/Provers/Arith/cancel_div_mod.ML
author skalberg
Sun Feb 13 17:15:14 2005 +0100 (2005-02-13)
changeset 15531 08c8dad8e399
parent 15027 d23887300b96
child 17613 072c21e31b42
permissions -rw-r--r--
Deleted Library.option type.
     1 (*  Title:      Provers/Arith/cancel_div_mod.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, TU Muenchen
     4 
     5 Cancel div and mod terms:
     6 
     7   A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
     8 
     9 Is parameterized but assumes for simplicity that + and * are called
    10 "op +" and "op *"
    11 *)
    12 
    13 signature CANCEL_DIV_MOD_DATA =
    14 sig
    15   (*abstract syntax*)
    16   val div_name: string
    17   val mod_name: string
    18   val mk_binop: string -> term * term -> term
    19   val mk_sum: term list -> term
    20   val dest_sum: term -> term list
    21   (*logic*)
    22   val div_mod_eqs: thm list
    23   (* (n*(m div n) + m mod n) + k == m + k and
    24      ((m div n)*n + m mod n) + k == m + k *)
    25   val prove_eq_sums: Sign.sg -> term * term -> thm
    26   (* must prove ac0-equivalence of sums *)
    27 end;
    28 
    29 signature CANCEL_DIV_MOD =
    30 sig
    31   val proc: Sign.sg -> simpset -> term -> thm option
    32 end;
    33 
    34 
    35 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
    36 struct
    37 
    38 fun coll_div_mod (Const("op +",_) $ s $ t) dms =
    39       coll_div_mod t (coll_div_mod s dms)
    40   | coll_div_mod (Const("op *",_) $ m $ (Const(d,_) $ s $ n))
    41                  (dms as (divs,mods)) =
    42       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    43   | coll_div_mod (Const("op *",_) $ (Const(d,_) $ s $ n) $ m)
    44                  (dms as (divs,mods)) =
    45       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    46   | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
    47       if m = Data.mod_name then (divs,(s,n)::mods) else dms
    48   | coll_div_mod _ dms = dms;
    49 
    50 
    51 (* Proof principle:
    52    1. (...div...)+(...mod...) == (div + mod) + rest
    53       in function rearrange
    54    2. (div + mod) + ?x = d + ?x
    55       Data.div_mod_eq
    56    ==> thesis by transitivity
    57 *)
    58 
    59 val mk_plus = Data.mk_binop "op +"
    60 val mk_times = Data.mk_binop "op *"
    61 
    62 fun rearrange t pq =
    63   let val ts = Data.dest_sum t;
    64       val dpq = Data.mk_binop Data.div_name pq
    65       val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
    66       val d = if d1 mem ts then d1 else d2
    67       val m = Data.mk_binop Data.mod_name pq
    68   in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
    69 
    70 fun cancel sg t pq =
    71   let val teqt' = Data.prove_eq_sums sg (t, rearrange t pq)
    72   in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
    73 
    74 fun proc sg _ t =
    75   let val (divs,mods) = coll_div_mod t ([],[])
    76   in if null divs orelse null mods then NONE
    77      else case divs inter mods of
    78             pq :: _ => SOME(cancel sg t pq)
    79           | [] => NONE
    80   end
    81 
    82 end