author  wenzelm 
Mon, 16 Feb 2009 21:23:33 +0100  
changeset 29758  7a3b5bbed313 
parent 29269  5c25a2012975 
child 35408  b48ab741683b 
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 
fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z); 

39 

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

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

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

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

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

48 

49 

50 
(* uncancel *) 

51 

52 
fun uncancel_sums_tac _ [] = all_tac 

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

55 
uncancel_sums_tac thy ts; 

4291  56 

57 

58 
(* the simplification procedure *) 

59 

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

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

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

65 
val thy = ProofContext.theory_of (Simplifier.the_context ss); 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
20044
diff
changeset

66 
val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal; 
4291  67 
val (ts', us', vs) = cancel ts us []; 
68 
in 

15531  69 
if null vs then NONE 
70 
else SOME 

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

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

74 

75 
end; 