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