1(*  Title:      Provers/Arith/cancel_div_mod.ML
2    Author:     Tobias Nipkow, TU Muenchen
3
4Cancel div and mod terms:
5
6  A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
7
8FIXME: Is parameterized but assumes for simplicity that + and * are named
9as in HOL
10*)
11
12signature CANCEL_DIV_MOD_DATA =
13sig
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 *)
26end;
27
28signature CANCEL_DIV_MOD =
29sig
30  val proc: Proof.context -> cterm -> thm option
31end;
32
33
34functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
35struct
36
37fun coll_div_mod (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ s $ t) dms =
38      coll_div_mod t (coll_div_mod s dms)
39  | coll_div_mod (Const (\<^const_name>\<open>Groups.times\<close>, _) $ 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>\<open>Groups.times\<close>, _) $ (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
58val mk_plus = Data.mk_binop \<^const_name>\<open>Groups.plus\<close>;
59val mk_times = Data.mk_binop \<^const_name>\<open>Groups.times\<close>;
60
61fun 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
70fun 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
75fun 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
87end
88