author  immler@in.tum.de 
Thu, 26 Feb 2009 10:13:43 +0100  
changeset 30151  629f3a92863e 
parent 27250  7eef2b183032 
child 34974  18b41bba42b5 
permissions  rwrr 
24584  1 
(* Title: Provers/Arith/abel_cancel.ML 
5589  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

6 
Simplification procedures for abelian groups (e.g. integers, reals, 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

7 
polymorphic types). 
5589  8 

13462  9 
 Cancel complementary terms in sums 
5589  10 
 Cancel like terms on opposite sides of relations 
11 
*) 

12 

13 
signature ABEL_CANCEL = 

14 
sig 

27250  15 
val eq_reflection : thm (*objectequality to metaequality*) 
16 
val T : typ (*the type of group elements*) 

16569  17 
val cancel_ss : simpset (*abelian group cancel simpset*) 
27250  18 
val sum_pats : cterm list 
16569  19 
val eqI_rules : thm list 
20 
val dest_eqI : thm > term 

5589  21 
end; 
22 

23 

24 
functor Abel_Cancel (Data: ABEL_CANCEL) = 

25 
struct 

26 

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

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

28 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

29 
(* FIXME dependent on abstract syntax *) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

30 

22997  31 
fun zero t = Const (@{const_name HOL.zero}, t); 
32 
fun minus t = Const (@{const_name HOL.uminus}, t > t); 

5589  33 

22997  34 
fun add_terms pos (Const (@{const_name HOL.plus}, _) $ x $ y, ts) = 
20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

35 
add_terms pos (x, add_terms pos (y, ts)) 
22997  36 
 add_terms pos (Const (@{const_name HOL.minus}, _) $ x $ y, ts) = 
20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

37 
add_terms pos (x, add_terms (not pos) (y, ts)) 
22997  38 
 add_terms pos (Const (@{const_name HOL.uminus}, _) $ x, ts) = 
20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

39 
add_terms (not pos) (x, ts) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

40 
 add_terms pos (x, ts) = (pos,x) :: ts; 
5589  41 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

42 
fun terms fml = add_terms true (fml, []); 
5589  43 

22997  44 
fun zero1 pt (u as (c as Const(@{const_name HOL.plus},_)) $ x $ y) = 
16569  45 
(case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE 
46 
 SOME z => SOME(c $ x $ z)) 

47 
 SOME z => SOME(c $ z $ y)) 

22997  48 
 zero1 (pos,t) (u as (c as Const(@{const_name HOL.minus},_)) $ x $ y) = 
16569  49 
(case zero1 (pos,t) x of 
50 
NONE => (case zero1 (not pos,t) y of NONE => NONE 

51 
 SOME z => SOME(c $ x $ z)) 

52 
 SOME z => SOME(c $ z $ y)) 

22997  53 
 zero1 (pos,t) (u as (c as Const(@{const_name HOL.uminus},_)) $ x) = 
16569  54 
(case zero1 (not pos,t) x of NONE => NONE 
55 
 SOME z => SOME(c $ z)) 

56 
 zero1 (pos,t) u = 

57 
if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE 

5589  58 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

59 
exception Cancel; 
5589  60 

16569  61 
fun find_common _ [] _ = raise Cancel 
62 
 find_common opp ((p,l)::ls) rs = 

63 
let val pr = if opp then not p else p 

64 
in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l) 

65 
else find_common opp ls rs 

66 
end 

5589  67 

16569  68 
(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, , =, etc. 
69 
If OP = +, it must be t2(t) rather than t2(t) 

70 
*) 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

71 
fun cancel t = 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

72 
let 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

73 
val c $ lhs $ rhs = t 
22997  74 
val opp = case c of Const(@{const_name HOL.plus},_) => true  _ => false; 
20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

75 
val (pos,l) = find_common opp (terms lhs) (terms rhs) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

76 
val posr = if opp then not pos else pos 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

77 
val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs)) 
16569  78 
in t' end; 
79 

80 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

81 
(*A simproc to cancel complementary terms in arbitrary sums.*) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

82 
fun sum_proc ss t = 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

83 
let 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

84 
val t' = cancel t 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

85 
val thm = 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

86 
Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t')) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

87 
(fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

88 
in SOME thm end handle Cancel => NONE; 
5589  89 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

90 
val sum_conv = 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

91 
Simplifier.mk_simproc "cancel_sums" 
27250  92 
(map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc); 
5589  93 

94 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

95 
(*A simproc to cancel like terms on the opposite sides of relations: 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

96 
(x + y  z < z + x) = (y < 0) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

97 
Works for (=) and (<=) as well as (<), if the necessary rules are supplied. 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

98 
Reduces the problem to subtraction.*) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

99 
fun rel_proc ss t = 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

100 
let 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

101 
val t' = cancel t 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

102 
val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t')) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

103 
(fn _ => rtac eq_reflection 1 THEN 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

104 
resolve_tac eqI_rules 1 THEN 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

105 
simp_tac (Simplifier.inherit_context ss cancel_ss) 1) 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

106 
in SOME thm end handle Cancel => NONE; 
5589  107 

20055
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

108 
val rel_conv = 
24c127b97ab5
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19798
diff
changeset

109 
Simplifier.mk_simproc "cancel_relations" 
27250  110 
(map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc); 
5589  111 

112 
end; 