author  immler@in.tum.de 
Thu, 26 Feb 2009 10:13:43 +0100  
changeset 30151  629f3a92863e 
parent 22997  d4f3b015b50b 
child 30937  1fe5a573b552 
permissions  rwrr 
13516  1 
(* Title: Provers/Arith/cancel_div_mod.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, TU Muenchen 

4 

5 
Cancel div and mod terms: 

6 

7 
A + n*(m div n) + B + (m mod n) + C == A + B + C + m 

8 

22997  9 
FIXME: Is parameterized but assumes for simplicity that + and * are named 
10 
HOL.plus and HOL.minus 

13516  11 
*) 
12 

13 
signature CANCEL_DIV_MOD_DATA = 

14 
sig 

15 
(*abstract syntax*) 

16 
val div_name: string 

17 
val mod_name: string 

18 
val mk_binop: string > term * term > term 

19 
val mk_sum: term list > term 

20 
val dest_sum: term > term list 

21 
(*logic*) 

22 
val div_mod_eqs: thm list 

23 
(* (n*(m div n) + m mod n) + k == m + k and 

24 
((m div n)*n + m mod n) + k == m + k *) 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

25 
val prove_eq_sums: simpset > term * term > thm 
13516  26 
(* must prove ac0equivalence of sums *) 
27 
end; 

28 

29 
signature CANCEL_DIV_MOD = 

30 
sig 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

31 
val proc: simpset > term > thm option 
13516  32 
end; 
33 

34 

35 
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = 

36 
struct 

37 

22997  38 
fun coll_div_mod (Const(@{const_name HOL.plus},_) $ s $ t) dms = 
13516  39 
coll_div_mod t (coll_div_mod s dms) 
22997  40 
 coll_div_mod (Const(@{const_name HOL.times},_) $ m $ (Const(d,_) $ s $ n)) 
13516  41 
(dms as (divs,mods)) = 
42 
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms 

22997  43 
 coll_div_mod (Const(@{const_name HOL.times},_) $ (Const(d,_) $ s $ n) $ m) 
13516  44 
(dms as (divs,mods)) = 
45 
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms 

46 
 coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) = 

47 
if m = Data.mod_name then (divs,(s,n)::mods) else dms 

48 
 coll_div_mod _ dms = dms; 

49 

50 

51 
(* Proof principle: 

52 
1. (...div...)+(...mod...) == (div + mod) + rest 

53 
in function rearrange 

54 
2. (div + mod) + ?x = d + ?x 

55 
Data.div_mod_eq 

56 
==> thesis by transitivity 

57 
*) 

58 

22997  59 
val mk_plus = Data.mk_binop @{const_name HOL.plus}; 
60 
val mk_times = Data.mk_binop @{const_name HOL.times}; 

13516  61 

62 
fun rearrange t pq = 

63 
let 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 d1 mem ts 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(ts \ d \ m)) end 

69 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

70 
fun cancel ss t pq = 
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

71 
let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq) 
13516  72 
in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end; 
73 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

74 
fun proc ss t = 
13516  75 
let val (divs,mods) = coll_div_mod t ([],[]) 
15531  76 
in if null divs orelse null mods then NONE 
13516  77 
else case divs inter mods of 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

78 
pq :: _ => SOME (cancel ss t pq) 
15531  79 
 [] => NONE 
13516  80 
end 
81 

17613  82 
end 