# HG changeset patch # User nipkow # Date 1119708433 -7200 # Node ID a12992c34c12ea15a50a2a7db1e84652b129579e # Parent e02fe7ae212b19f7eca407d53728cca8146da289 cancels completely within terms as well now. diff -r e02fe7ae212b -r a12992c34c12 src/Provers/Arith/abel_cancel.ML --- a/src/Provers/Arith/abel_cancel.ML Sat Jun 25 16:06:17 2005 +0200 +++ b/src/Provers/Arith/abel_cancel.ML Sat Jun 25 16:07:13 2005 +0200 @@ -8,39 +8,20 @@ - Cancel complementary terms in sums - Cancel like terms on opposite sides of relations +Modification in May 2004 by Steven Obua: polymorphic types work also now +Modification in June 2005 by Tobias Nipkow: cancel_sums works in general now +(using Clemens Ballarin's code for ordered rewriting in abelian groups) +and the whole file is reduced to a fraction of its former size. *) -(* Modification in May 2004 by Steven Obua: polymorphic types work also now *) - signature ABEL_CANCEL = sig - val ss : simpset (*basic simpset of object-logic*) - val eq_reflection : thm (*object-equality to meta-equality*) - - val thy_ref : theory_ref (*signature of the theory of the group*) - val T : typ (*the type of group elements*) - - val restrict_to_left : thm - val add_cancel_21 : thm - val add_cancel_end : thm - val add_left_cancel : thm - val add_assoc : thm - val add_commute : thm - val add_left_commute : thm - val add_0 : thm - val add_0_right : thm - - val eq_diff_eq : thm - val eqI_rules : thm list - val dest_eqI : thm -> term - - val diff_def : thm - val minus_add_distrib : thm - val minus_minus : thm - val minus_0 : thm - - val add_inverses : thm list - val cancel_simps : thm list + val cancel_ss : simpset (*abelian group cancel simpset*) + val thy_ref : theory_ref (*signature of the theory of the group*) + val T : typ (*the type of group elements*) + val eq_reflection : thm (*object-equality to meta-equality*) + val eqI_rules : thm list + val dest_eqI : thm -> term end; @@ -49,80 +30,71 @@ open Data; - val prepare_ss = Data.ss addsimps [add_assoc, diff_def, - minus_add_distrib, minus_minus, - minus_0, add_0, add_0_right]; - - fun zero t = Const ("0", t); - fun plus t = Const ("op +", [t,t] ---> t); fun minus t = Const ("uminus", t --> t); - (*Cancel corresponding terms on the two sides of the equation, NOT on - the same side!*) - val cancel_ss = - Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ - (map (fn th => th RS restrict_to_left) Data.cancel_simps); + fun add_terms pos (Const ("op +", _) $ x $ y, ts) = + add_terms pos (x, add_terms pos (y, ts)) + | add_terms pos (Const ("op -", _) $ x $ y, ts) = + add_terms pos (x, add_terms (not pos) (y, ts)) + | add_terms pos (Const ("uminus", _) $ x, ts) = + add_terms (not pos) (x, ts) + | add_terms pos (x, ts) = (pos,x) :: ts; - val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps; - - fun mk_sum ty [] = zero ty - | mk_sum ty tms = foldr1 (fn (x,y) => (plus ty) $ x $ y) tms; + fun terms fml = add_terms true (fml, []); - (*We map -t to t and (in other cases) t to -t. No need to check the type of - uminus, since the simproc is only called on sums of type T.*) - fun negate (Const("uminus",_) $ t) = t - | negate t = (minus (fastype_of t)) $ t; - - (*Flatten a formula built from +, binary - and unary -. - No need to check types PROVIDED they are checked upon entry!*) - fun add_terms neg (Const ("op +", _) $ x $ y, ts) = - add_terms neg (x, add_terms neg (y, ts)) - | add_terms neg (Const ("op -", _) $ x $ y, ts) = - add_terms neg (x, add_terms (not neg) (y, ts)) - | add_terms neg (Const ("uminus", _) $ x, ts) = - add_terms (not neg) (x, ts) - | add_terms neg (x, ts) = - (if neg then negate x else x) :: ts; - - fun terms fml = add_terms false (fml, []); +fun zero1 pt (u as (c as Const("op +",_)) $ x $ y) = + (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE + | SOME z => SOME(c $ x $ z)) + | SOME z => SOME(c $ z $ y)) + | zero1 (pos,t) (u as (c as Const("op -",_)) $ x $ y) = + (case zero1 (pos,t) x of + NONE => (case zero1 (not pos,t) y of NONE => NONE + | SOME z => SOME(c $ x $ z)) + | SOME z => SOME(c $ z $ y)) + | zero1 (pos,t) (u as (c as Const("uminus",_)) $ x) = + (case zero1 (not pos,t) x of NONE => NONE + | SOME z => SOME(c $ z)) + | zero1 (pos,t) u = + if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE exception Cancel; - (*Cancels just the first occurrence of u, leaving the rest unchanged*) - fun cancelled (u, t::ts) = if u aconv t then ts else t :: cancelled(u,ts) - | cancelled _ = raise Cancel; - - val trace = ref false; - (*Make a simproc to cancel complementary terms in sums. Examples: - x-x = 0 x+(y-x) = y -x+(y+(x+z)) = y+z - It will unfold the definition of diff and associate to the right if - necessary. Rewriting is faster if the formula is already - in that form. - *) +fun find_common _ [] _ = raise Cancel + | find_common opp ((p,l)::ls) rs = + let val pr = if opp then not p else p + in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l) + else find_common opp ls rs + end - fun sum_proc sg _ lhs = - let val _ = if !trace then tracing ("cancel_sums: LHS = " ^ - string_of_cterm (cterm_of sg lhs)) - else () - val (head::tail) = terms lhs - val head' = negate head - val rhs = mk_sum (fastype_of head) (cancelled (head',tail)) - and chead' = Thm.cterm_of sg head' - val _ = if !trace then - tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) - else () - val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs)) - (fn _ => rtac eq_reflection 1 THEN - simp_tac prepare_ss 1 THEN - IF_UNSOLVED (simp_tac cancel_ss 1) THEN - IF_UNSOLVED (simp_tac inverse_ss 1)) +(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc. + If OP = +, it must be t2(-t) rather than t2(t) +*) +fun cancel sg t = + let val _ = if !trace + then tracing ("Abel cancel: " ^ string_of_cterm (cterm_of sg t)) + else () + val c $ lhs $ rhs = t + val opp = case c of Const("op +",_) => true | _ => false; + val (pos,l) = find_common opp (terms lhs) (terms rhs) + val posr = if opp then not pos else pos + val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs)) + val _ = if !trace + then tracing ("cancelled: " ^ string_of_cterm (cterm_of sg t')) + else () + in t' end; + +(* A simproc to cancel complementary terms in arbitrary sums. *) + +fun sum_proc sg _ t = + let val t' = cancel sg t + val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t')) + (fn _ => simp_tac cancel_ss 1) in SOME thm end handle Cancel => NONE; - val sum_conv = Simplifier.mk_simproc "cancel_sums" (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref)) @@ -133,51 +105,15 @@ (*A simproc to cancel like terms on the opposite sides of relations: (x + y - z < -z + x) = (y < 0) Works for (=) and (<=) as well as (<), if the necessary rules are supplied. - Reduces the problem to subtraction and calls the previous simproc. + Reduces the problem to subtraction. *) - (*Cancel the FIRST occurrence of a term. If it's repeated, then repeated - calls to the simproc will be needed.*) - fun cancel1 ([], u) = raise Match (*impossible: it's a common term*) - | cancel1 (t::ts, u) = if t aconv u then ts - else t :: cancel1 (ts,u); - - - val sum_cancel_ss = Data.ss addsimprocs [sum_conv] - addsimps [add_0, add_0_right]; - - val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute]; - - fun rel_proc sg _ (lhs as (rel$lt$rt)) = - let val _ = if !trace then tracing ("cancel_relations: LHS = " ^ - string_of_cterm (cterm_of sg lhs)) - else () - val ltms = terms lt - and rtms = terms rt - val ty = fastype_of lt - val common = (*inter_term miscounts repetitions, so squash them*) - gen_distinct (op aconv) (inter_term (ltms, rtms)) - val _ = if null common then raise Cancel (*nothing to do*) - else () - - fun cancelled tms = mk_sum ty (Library.foldl cancel1 (tms, common)) - - val lt' = cancelled ltms - and rt' = cancelled rtms - - val rhs = rel$lt'$rt' - val _ = if lhs aconv rhs then raise Cancel (*nothing to do*) - else () - val _ = if !trace then - tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) - else () - - val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs)) + fun rel_proc sg _ t = + let val t' = cancel sg t + val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t')) (fn _ => rtac eq_reflection 1 THEN resolve_tac eqI_rules 1 THEN - simp_tac prepare_ss 1 THEN - simp_tac sum_cancel_ss 1 THEN - IF_UNSOLVED (simp_tac add_ac_ss 1)) + simp_tac cancel_ss 1) in SOME thm end handle Cancel => NONE; @@ -186,5 +122,3 @@ (map Data.dest_eqI eqI_rules) rel_proc; end; - -