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 

5610

18 
val thy : theory (*the theory of the group*)


19 
val T : typ (*the type of group elements*)

5589

20 

5610

21 
val zero : term

5589

22 
val add_cancel_21 : thm


23 
val add_cancel_end : thm


24 
val add_left_cancel : thm

5610

25 
val add_assoc : thm


26 
val add_commute : thm


27 
val add_left_commute : thm


28 
val add_0 : thm


29 
val add_0_right : thm

5589

30 


31 
val eq_diff_eq : thm


32 
val eqI_rules : thm list


33 
val dest_eqI : thm > term


34 


35 
val diff_def : thm


36 
val minus_add_distrib : thm


37 
val minus_minus : thm


38 
val minus_0 : thm


39 


40 
val add_inverses : thm list


41 
val cancel_simps : thm list


42 
end;


43 


44 


45 
functor Abel_Cancel (Data: ABEL_CANCEL) =


46 
let open Data in


47 
struct


48 


49 
val prepare_ss = Data.ss addsimps [add_assoc, diff_def,


50 
minus_add_distrib, minus_minus,


51 
minus_0, add_0, add_0_right];


52 


53 
(*prove while suppressing timing information*)


54 
fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);


55 


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


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


58 


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


60 
the same side!*)


61 
val cancel_ss =


62 
Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @


63 
Data.cancel_simps;


64 


65 
val inverse_ss = Data.ss addsimps Data.add_inverses;


66 


67 
fun mk_sum [] = Data.zero


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


69 


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


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


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


73 
 negate t = minus $ t;


74 


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


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


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


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


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


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


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


82 
add_terms (not neg) (x, ts)


83 
 add_terms neg (x, ts) =


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


85 


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


87 


88 
exception Cancel;


89 


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


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


92 
 cancelled _ = raise Cancel;


93 


94 


95 
val trace = ref false;


96 


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


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


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


100 
necessary. Rewriting is faster if the formula is already


101 
in that form.


102 
*)


103 


104 
fun sum_proc sg _ lhs =


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


106 
string_of_cterm (cterm_of sg lhs))


107 
else ()


108 
val (head::tail) = terms lhs


109 
val head' = negate head


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


111 
and chead' = Thm.cterm_of sg head'


112 
val _ = if !trace then


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


114 
else ()

5610

115 
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))

5589

116 
val thm = prove ct

5610

117 
(fn _ => [rtac eq_reflection 1,


118 
simp_tac prepare_ss 1,

5589

119 
IF_UNSOLVED (simp_tac cancel_ss 1),


120 
IF_UNSOLVED (simp_tac inverse_ss 1)])


121 
handle ERROR =>


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


123 
string_of_cterm ct)

5610

124 
in Some thm end

5589

125 
handle Cancel => None;


126 


127 


128 
val sum_conv =


129 
Simplifier.mk_simproc "cancel_sums"


130 
(map (Thm.read_cterm (sign_of Data.thy))


131 
[("x + y", Data.T), ("x  y", Data.T)])


132 
sum_proc;


133 


134 


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


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


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


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


139 
*)


140 


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


142 
calls to the simproc will be needed.*)


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


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


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


146 


147 


148 
val sum_cancel_ss = Data.ss addsimprocs [sum_conv]


149 
addsimps [add_0, add_0_right];


150 


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


152 


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


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


155 
string_of_cterm (cterm_of sg lhs))


156 
else ()


157 
val ltms = terms lt


158 
and rtms = terms rt


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


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


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


162 
else ()


163 


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


165 


166 
val lt' = cancelled ltms


167 
and rt' = cancelled rtms


168 


169 
val rhs = rel$lt'$rt'


170 
val _ = if !trace then


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


172 
else ()

5610

173 
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))

5589

174 


175 
val thm = prove ct

5610

176 
(fn _ => [rtac eq_reflection 1,


177 
resolve_tac eqI_rules 1,

5589

178 
simp_tac prepare_ss 1,


179 
simp_tac sum_cancel_ss 1,


180 
IF_UNSOLVED (simp_tac add_ac_ss 1)])


181 
handle ERROR =>


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


183 
string_of_cterm ct)

5610

184 
in Some thm end

5589

185 
handle Cancel => None;


186 


187 
val rel_conv =


188 
Simplifier.mk_simproc "cancel_relations"


189 
(map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)


190 
rel_proc;


191 


192 
end


193 
end;


194 
