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;
nipkow@13516
     1
(*  Title:      Provers/Arith/cancel_div_mod.ML
nipkow@13516
     2
    Author:     Tobias Nipkow, TU Muenchen
nipkow@13516
     3
nipkow@13516
     4
Cancel div and mod terms:
nipkow@13516
     5
nipkow@13516
     6
  A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
nipkow@13516
     7
haftmann@22997
     8
FIXME: Is parameterized but assumes for simplicity that + and * are named
haftmann@34974
     9
as in HOL
nipkow@13516
    10
*)
nipkow@13516
    11
nipkow@13516
    12
signature CANCEL_DIV_MOD_DATA =
nipkow@13516
    13
sig
nipkow@13516
    14
  (*abstract syntax*)
nipkow@13516
    15
  val div_name: string
nipkow@13516
    16
  val mod_name: string
nipkow@13516
    17
  val mk_binop: string -> term * term -> term
haftmann@66810
    18
  val mk_sum: typ -> term list -> term
nipkow@13516
    19
  val dest_sum: term -> term list
nipkow@13516
    20
  (*logic*)
nipkow@13516
    21
  val div_mod_eqs: thm list
nipkow@13516
    22
  (* (n*(m div n) + m mod n) + k == m + k and
nipkow@13516
    23
     ((m div n)*n + m mod n) + k == m + k *)
wenzelm@51717
    24
  val prove_eq_sums: Proof.context -> term * term -> thm
nipkow@13516
    25
  (* must prove ac0-equivalence of sums *)
nipkow@13516
    26
end;
nipkow@13516
    27
nipkow@13516
    28
signature CANCEL_DIV_MOD =
nipkow@13516
    29
sig
wenzelm@51717
    30
  val proc: Proof.context -> cterm -> thm option
nipkow@13516
    31
end;
nipkow@13516
    32
nipkow@13516
    33
wenzelm@43594
    34
functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
nipkow@13516
    35
struct
nipkow@13516
    36
haftmann@66810
    37
fun coll_div_mod (Const (@{const_name Groups.plus}, _) $ s $ t) dms =
nipkow@13516
    38
      coll_div_mod t (coll_div_mod s dms)
haftmann@66810
    39
  | coll_div_mod (Const (@{const_name Groups.times}, _) $ m $ (Const (d, _) $ s $ n))
haftmann@66810
    40
                 (dms as (divs, mods)) =
haftmann@66810
    41
      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
haftmann@66810
    42
  | coll_div_mod (Const (@{const_name Groups.times}, _) $ (Const (d, _) $ s $ n) $ m)
haftmann@66810
    43
                 (dms as (divs, mods)) =
haftmann@66810
    44
      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
haftmann@66810
    45
  | coll_div_mod (Const (m, _) $ s $ n) (dms as (divs, mods)) =
haftmann@66810
    46
      if m = Data.mod_name then (divs, (s, n) :: mods) else dms
nipkow@13516
    47
  | coll_div_mod _ dms = dms;
nipkow@13516
    48
nipkow@13516
    49
nipkow@13516
    50
(* Proof principle:
nipkow@13516
    51
   1. (...div...)+(...mod...) == (div + mod) + rest
nipkow@13516
    52
      in function rearrange
nipkow@13516
    53
   2. (div + mod) + ?x = d + ?x
nipkow@13516
    54
      Data.div_mod_eq
nipkow@13516
    55
   ==> thesis by transitivity
nipkow@13516
    56
*)
nipkow@13516
    57
haftmann@35267
    58
val mk_plus = Data.mk_binop @{const_name Groups.plus};
haftmann@35267
    59
val mk_times = Data.mk_binop @{const_name Groups.times};
nipkow@13516
    60
haftmann@66810
    61
fun rearrange T t pq =
haftmann@66810
    62
  let
haftmann@66810
    63
    val ts = Data.dest_sum t;
haftmann@66810
    64
    val dpq = Data.mk_binop Data.div_name pq;
haftmann@66810
    65
    val d1 = mk_times (snd pq, dpq) and d2 = mk_times (dpq, snd pq);
haftmann@66810
    66
    val d = if member (op =) ts d1 then d1 else d2;
haftmann@66810
    67
    val m = Data.mk_binop Data.mod_name pq;
haftmann@66810
    68
  in mk_plus (mk_plus (d, m), Data.mk_sum T (ts |> remove (op =) d |> remove (op =) m)) end
nipkow@13516
    69
wenzelm@51717
    70
fun cancel ctxt t pq =
haftmann@66810
    71
  let
haftmann@66810
    72
    val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq);
haftmann@30937
    73
  in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
nipkow@13516
    74
wenzelm@51717
    75
fun proc ctxt ct =
wenzelm@43594
    76
  let
wenzelm@59582
    77
    val t = Thm.term_of ct;
wenzelm@43594
    78
    val (divs, mods) = coll_div_mod t ([], []);
wenzelm@43594
    79
  in
wenzelm@43594
    80
    if null divs orelse null mods then NONE
wenzelm@43594
    81
    else
wenzelm@43594
    82
      (case inter (op =) mods divs of
wenzelm@51717
    83
        pq :: _ => SOME (cancel ctxt t pq)
wenzelm@43594
    84
      | [] => NONE)
wenzelm@43594
    85
  end;
nipkow@13516
    86
wenzelm@17613
    87
end