author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 9419  e46de4af70e4 
child 12262  11ff5f47df6e 
permissions  rwrr 
5589  1 
(* Title: Provers/Arith/abel_cancel.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
Simplification procedures for abelian groups (e.g. integers, reals) 

7 

8 
 Cancel complementary terms in sums 

9 
 Cancel like terms on opposite sides of relations 

10 
*) 

11 

12 

13 
signature ABEL_CANCEL = 

14 
sig 

5610  15 
val ss : simpset (*basic simpset of objectlogtic*) 
16 
val eq_reflection : thm (*objectequality to metaequality*) 

5589  17 

9419  18 
val sg_ref : Sign.sg_ref (*signature of the theory of the group*) 
5610  19 
val T : typ (*the type of group elements*) 
5589  20 

5610  21 
val zero : term 
7586  22 
val restrict_to_left : thm 
5589  23 
val add_cancel_21 : thm 
24 
val add_cancel_end : thm 

25 
val add_left_cancel : thm 

5610  26 
val add_assoc : thm 
27 
val add_commute : thm 

28 
val add_left_commute : thm 

29 
val add_0 : thm 

30 
val add_0_right : thm 

5589  31 

32 
val eq_diff_eq : thm 

33 
val eqI_rules : thm list 

34 
val dest_eqI : thm > term 

35 

36 
val diff_def : thm 

37 
val minus_add_distrib : thm 

38 
val minus_minus : thm 

39 
val minus_0 : thm 

40 

41 
val add_inverses : thm list 

42 
val cancel_simps : thm list 

43 
end; 

44 

45 

46 
functor Abel_Cancel (Data: ABEL_CANCEL) = 

47 
struct 

48 

5728
1d1175ef2d56
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents:
5610
diff
changeset

49 
open Data; 
1d1175ef2d56
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents:
5610
diff
changeset

50 

5589  51 
val prepare_ss = Data.ss addsimps [add_assoc, diff_def, 
52 
minus_add_distrib, minus_minus, 

53 
minus_0, add_0, add_0_right]; 

54 

55 
(*prove while suppressing timing information*) 

8999  56 
fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct); 
5589  57 

58 
val plus = Const ("op +", [Data.T,Data.T] > Data.T); 

59 
val minus = Const ("uminus", Data.T > Data.T); 

60 

61 
(*Cancel corresponding terms on the two sides of the equation, NOT on 

62 
the same side!*) 

63 
val cancel_ss = 

7586  64 
Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ 
65 
(map (fn th => th RS restrict_to_left) Data.cancel_simps); 

5589  66 

7586  67 
val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps; 
5589  68 

69 
fun mk_sum [] = Data.zero 

70 
 mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms; 

71 

72 
(*We map t to t and (in other cases) t to t. No need to check the type of 

73 
uminus, since the simproc is only called on sums of type T.*) 

74 
fun negate (Const("uminus",_) $ t) = t 

75 
 negate t = minus $ t; 

76 

77 
(*Flatten a formula built from +, binary  and unary . 

78 
No need to check types PROVIDED they are checked upon entry!*) 

79 
fun add_terms neg (Const ("op +", _) $ x $ y, ts) = 

80 
add_terms neg (x, add_terms neg (y, ts)) 

81 
 add_terms neg (Const ("op ", _) $ x $ y, ts) = 

82 
add_terms neg (x, add_terms (not neg) (y, ts)) 

83 
 add_terms neg (Const ("uminus", _) $ x, ts) = 

84 
add_terms (not neg) (x, ts) 

85 
 add_terms neg (x, ts) = 

86 
(if neg then negate x else x) :: ts; 

87 

88 
fun terms fml = add_terms false (fml, []); 

89 

90 
exception Cancel; 

91 

92 
(*Cancels just the first occurrence of u, leaving the rest unchanged*) 

93 
fun cancelled (u, t::ts) = if u aconv t then ts else t :: cancelled(u,ts) 

94 
 cancelled _ = raise Cancel; 

95 

96 

97 
val trace = ref false; 

98 

99 
(*Make a simproc to cancel complementary terms in sums. Examples: 

100 
xx = 0 x+(yx) = y x+(y+(x+z)) = y+z 

101 
It will unfold the definition of diff and associate to the right if 

102 
necessary. Rewriting is faster if the formula is already 

103 
in that form. 

104 
*) 

105 

106 
fun sum_proc sg _ lhs = 

107 
let val _ = if !trace then writeln ("cancel_sums: LHS = " ^ 

108 
string_of_cterm (cterm_of sg lhs)) 

109 
else () 

110 
val (head::tail) = terms lhs 

111 
val head' = negate head 

112 
val rhs = mk_sum (cancelled (head',tail)) 

113 
and chead' = Thm.cterm_of sg head' 

114 
val _ = if !trace then 

115 
writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) 

116 
else () 

5610  117 
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)) 
5589  118 
val thm = prove ct 
5610  119 
(fn _ => [rtac eq_reflection 1, 
120 
simp_tac prepare_ss 1, 

5589  121 
IF_UNSOLVED (simp_tac cancel_ss 1), 
122 
IF_UNSOLVED (simp_tac inverse_ss 1)]) 

123 
handle ERROR => 

124 
error("cancel_sums simproc:\nfailed to prove " ^ 

125 
string_of_cterm ct) 

5610  126 
in Some thm end 
5589  127 
handle Cancel => None; 
128 

129 

130 
val sum_conv = 

131 
Simplifier.mk_simproc "cancel_sums" 

9419  132 
(map (Thm.read_cterm (Sign.deref sg_ref)) 
5589  133 
[("x + y", Data.T), ("x  y", Data.T)]) 
134 
sum_proc; 

135 

136 

137 
(*A simproc to cancel like terms on the opposite sides of relations: 

138 
(x + y  z < z + x) = (y < 0) 

139 
Works for (=) and (<=) as well as (<), if the necessary rules are supplied. 

140 
Reduces the problem to subtraction and calls the previous simproc. 

141 
*) 

142 

143 
(*Cancel the FIRST occurrence of a term. If it's repeated, then repeated 

144 
calls to the simproc will be needed.*) 

145 
fun cancel1 ([], u) = raise Match (*impossible: it's a common term*) 

146 
 cancel1 (t::ts, u) = if t aconv u then ts 

147 
else t :: cancel1 (ts,u); 

148 

149 

150 
val sum_cancel_ss = Data.ss addsimprocs [sum_conv] 

151 
addsimps [add_0, add_0_right]; 

152 

153 
val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute]; 

154 

155 
fun rel_proc sg _ (lhs as (rel$lt$rt)) = 

156 
let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ 

157 
string_of_cterm (cterm_of sg lhs)) 

158 
else () 

159 
val ltms = terms lt 

160 
and rtms = terms rt 

161 
val common = (*inter_term miscounts repetitions, so squash them*) 

162 
gen_distinct (op aconv) (inter_term (ltms, rtms)) 

163 
val _ = if null common then raise Cancel (*nothing to do*) 

164 
else () 

165 

166 
fun cancelled tms = mk_sum (foldl cancel1 (tms, common)) 

167 

168 
val lt' = cancelled ltms 

169 
and rt' = cancelled rtms 

170 

171 
val rhs = rel$lt'$rt' 

172 
val _ = if !trace then 

173 
writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) 

174 
else () 

5610  175 
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs)) 
5589  176 

177 
val thm = prove ct 

5610  178 
(fn _ => [rtac eq_reflection 1, 
179 
resolve_tac eqI_rules 1, 

5589  180 
simp_tac prepare_ss 1, 
181 
simp_tac sum_cancel_ss 1, 

182 
IF_UNSOLVED (simp_tac add_ac_ss 1)]) 

183 
handle ERROR => 

184 
error("cancel_relations simproc:\nfailed to prove " ^ 

185 
string_of_cterm ct) 

5610  186 
in Some thm end 
5589  187 
handle Cancel => None; 
188 

189 
val rel_conv = 

190 
Simplifier.mk_simproc "cancel_relations" 

9419  191 
(map (Thm.cterm_of (Sign.deref sg_ref) o Data.dest_eqI) eqI_rules) 
5589  192 
rel_proc; 
193 

194 
end; 