author  immler@in.tum.de 
Thu, 26 Feb 2009 10:13:43 +0100  
changeset 30151  629f3a92863e 
parent 29269  5c25a2012975 
child 35408  b48ab741683b 
permissions  rwrr 
4292  1 
(* Title: Provers/Arith/cancel_factor.ML 
2 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 

3 

4 
Cancel common constant factor from balanced exression (e.g. =, <=, < of sums). 

5 
*) 

6 

7 
signature CANCEL_FACTOR_DATA = 

8 
sig 

9 
(*abstract syntax*) 

10 
val mk_sum: term list > term 

11 
val dest_sum: term > term list 

12 
val mk_bal: term * term > term 

13 
val dest_bal: term > term * term 

14 
(*rules*) 

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

15 
val prove_conv: tactic > tactic > Proof.context > term * term > thm 
23261  16 
val norm_tac: tactic (*AC0 etc.*) 
17 
val multiply_tac: integer > tactic 

18 
(*apply a ~~ b == k * a ~~ k * b (for k > 0)*) 

4292  19 
end; 
20 

21 
signature CANCEL_FACTOR = 

22 
sig 

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

23 
val proc: simpset > term > thm option 
4292  24 
end; 
25 

26 

27 
functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR = 

28 
struct 

29 

30 

31 
(* count terms *) 

32 

33 
fun ins_term (t, []) = [(t, 1)] 

34 
 ins_term (t, (u, k) :: uks) = 

35 
if t aconv u then (u, k + 1) :: uks 

36 
else (t, 1) :: (u, k) :: uks; 

37 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

38 
fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []); 
4292  39 

40 

41 
(* divide sum *) 

42 

23261  43 
fun div_sum d = 
44 
Data.mk_sum o maps (fn (t, k) => replicate (k div d) t); 

4292  45 

46 

47 
(* the simplification procedure *) 

48 

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

49 
fun proc ss t = 
4292  50 
(case try Data.dest_bal t of 
15531  51 
NONE => NONE 
52 
 SOME bal => 

4292  53 
(case pairself Data.dest_sum bal of 
15531  54 
([_], _) => NONE 
55 
 (_, [_]) => NONE 

4292  56 
 ts_us => 
57 
let 

58 
val (tks, uks) = pairself count_terms ts_us; 

23261  59 
val d = 0 
60 
> fold (Integer.gcd o snd) tks 

61 
> fold (Integer.gcd o snd) uks; 

4292  62 
in 
15531  63 
if d = 0 orelse d = 1 then NONE 
64 
else SOME 

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

65 
(Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss) 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23261
diff
changeset

66 
(t, Data.mk_bal (div_sum d tks, div_sum d uks))) 
4292  67 
end)); 
68 

69 

70 
end; 