author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 38052  04a8de29e8f7 
child 42361  23f352990944 
permissions  rwrr 
4291  1 
(* Title: Provers/Arith/cancel_sums.ML 
2 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 

3 

4 
Cancel common summands of balanced expressions: 

5 

6 
A + x + B ~~ A' + x + B' == A + B ~~ A' + B' 

7 

8 
where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, ). 

9 
*) 

10 

11 
signature CANCEL_SUMS_DATA = 

12 
sig 

13 
(*abstract syntax*) 

14 
val mk_sum: term list > term 

15 
val dest_sum: term > term list 

16 
val mk_bal: term * term > term 

17 
val dest_bal: term > term * term 

18 
(*rules*) 

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

19 
val prove_conv: tactic > (simpset > tactic) > simpset > term * term > thm 
17613  20 
val norm_tac: simpset > tactic (*AC0 etc.*) 
21 
val uncancel_tac: cterm > tactic (*apply A ~~ B == x + A ~~ x + B*) 

4291  22 
end; 
23 

24 
signature CANCEL_SUMS = 

25 
sig 

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

26 
val proc: simpset > term > thm option 
4291  27 
end; 
28 

29 

30 
functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS = 

31 
struct 

32 

33 

34 
(* cancel *) 

35 

36 
fun cons1 x (xs, y, z) = (x :: xs, y, z); 

37 
fun cons2 y (x, ys, z) = (x, y :: ys, z); 

38 

35408  39 
(*symmetric difference of multisets  assumed to be sorted wrt. Term_Ord.term_ord*) 
4291  40 
fun cancel ts [] vs = (ts, [], vs) 
41 
 cancel [] us vs = ([], us, vs) 

42 
 cancel (t :: ts) (u :: us) vs = 

35408  43 
(case Term_Ord.term_ord (t, u) of 
4346  44 
EQUAL => cancel ts us (t :: vs) 
4291  45 
 LESS => cons1 t (cancel ts (u :: us) vs) 
46 
 GREATER => cons2 u (cancel (t :: ts) us vs)); 

47 

48 

49 
(* uncancel *) 

50 

51 
fun uncancel_sums_tac _ [] = all_tac 

17613  52 
 uncancel_sums_tac thy (t :: ts) = 
53 
Data.uncancel_tac (Thm.cterm_of thy t) THEN 

54 
uncancel_sums_tac thy ts; 

4291  55 

56 

57 
(* the simplification procedure *) 

58 

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

59 
fun proc ss t = 
4291  60 
(case try Data.dest_bal t of 
15531  61 
NONE => NONE 
62 
 SOME bal => 

4291  63 
let 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
17613
diff
changeset

64 
val thy = ProofContext.theory_of (Simplifier.the_context ss); 
35408  65 
val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal; 
4291  66 
val (ts', us', vs) = cancel ts us []; 
67 
in 

15531  68 
if null vs then NONE 
69 
else SOME 

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

70 
(Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss 
4291  71 
(t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us'))) 
72 
end); 

73 

74 
end; 