src/Provers/Arith/cancel_div_mod.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05 ago)
changeset 36692 54b64d4ad524
parent 35267 8dfd816713c6
child 43594 ef1ddc59b825
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
     1 (*  Title:      Provers/Arith/cancel_div_mod.ML
     2     Author:     Tobias Nipkow, TU Muenchen
     3 
     4 Cancel div and mod terms:
     5 
     6   A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
     7 
     8 FIXME: Is parameterized but assumes for simplicity that + and * are named
     9 as in HOL
    10 *)
    11 
    12 signature CANCEL_DIV_MOD_DATA =
    13 sig
    14   (*abstract syntax*)
    15   val div_name: string
    16   val mod_name: string
    17   val mk_binop: string -> term * term -> term
    18   val mk_sum: term list -> term
    19   val dest_sum: term -> term list
    20   (*logic*)
    21   val div_mod_eqs: thm list
    22   (* (n*(m div n) + m mod n) + k == m + k and
    23      ((m div n)*n + m mod n) + k == m + k *)
    24   val prove_eq_sums: simpset -> term * term -> thm
    25   (* must prove ac0-equivalence of sums *)
    26 end;
    27 
    28 signature CANCEL_DIV_MOD =
    29 sig
    30   val proc: simpset -> term -> thm option
    31 end;
    32 
    33 
    34 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
    35 struct
    36 
    37 fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
    38       coll_div_mod t (coll_div_mod s dms)
    39   | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n))
    40                  (dms as (divs,mods)) =
    41       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    42   | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m)
    43                  (dms as (divs,mods)) =
    44       if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    45   | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
    46       if m = Data.mod_name then (divs,(s,n)::mods) else dms
    47   | coll_div_mod _ dms = dms;
    48 
    49 
    50 (* Proof principle:
    51    1. (...div...)+(...mod...) == (div + mod) + rest
    52       in function rearrange
    53    2. (div + mod) + ?x = d + ?x
    54       Data.div_mod_eq
    55    ==> thesis by transitivity
    56 *)
    57 
    58 val mk_plus = Data.mk_binop @{const_name Groups.plus};
    59 val mk_times = Data.mk_binop @{const_name Groups.times};
    60 
    61 fun rearrange t pq =
    62   let val ts = Data.dest_sum t;
    63       val dpq = Data.mk_binop Data.div_name pq
    64       val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
    65       val d = if member (op =) ts d1 then d1 else d2
    66       val m = Data.mk_binop Data.mod_name pq
    67   in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
    68 
    69 fun cancel ss t pq =
    70   let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
    71   in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
    72 
    73 fun proc ss t =
    74   let val (divs,mods) = coll_div_mod t ([],[])
    75   in if null divs orelse null mods then NONE
    76      else case inter (op =) mods divs of
    77             pq :: _ => SOME (cancel ss t pq)
    78           | [] => NONE
    79   end
    80 
    81 end