src/Provers/Arith/cancel_div_mod.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66810 cc2b490f9dc4
child 69593 3dda49e08b9d
permissions -rw-r--r--
more robust sorted_entries;
     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: typ -> 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: Proof.context -> term * term -> thm
    25   (* must prove ac0-equivalence of sums *)
    26 end;
    27 
    28 signature CANCEL_DIV_MOD =
    29 sig
    30   val proc: Proof.context -> cterm -> thm option
    31 end;
    32 
    33 
    34 functor Cancel_Div_Mod(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 t pq =
    62   let
    63     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 member (op =) ts d1 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 T (ts |> remove (op =) d |> remove (op =) m)) end
    69 
    70 fun cancel ctxt t pq =
    71   let
    72     val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq);
    73   in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
    74 
    75 fun proc ctxt ct =
    76   let
    77     val t = Thm.term_of ct;
    78     val (divs, mods) = coll_div_mod t ([], []);
    79   in
    80     if null divs orelse null mods then NONE
    81     else
    82       (case inter (op =) mods divs of
    83         pq :: _ => SOME (cancel ctxt t pq)
    84       | [] => NONE)
    85   end;
    86 
    87 end