author | wenzelm |
Fri, 21 Oct 2005 18:14:34 +0200 | |
changeset 17956 | 369e2af8ee45 |
parent 17877 | 67d5ab1cb0d8 |
child 19233 | 77ca20b0ed77 |
permissions | -rw-r--r-- |
14756 | 1 |
(* Title: HOL/OrderedGroup.ML |
5589 | 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 |
||
13462 | 8 |
- Cancel complementary terms in sums |
5589 | 9 |
- Cancel like terms on opposite sides of relations |
14756 | 10 |
|
16569 | 11 |
Modification in May 2004 by Steven Obua: polymorphic types work also now |
12 |
Modification in June 2005 by Tobias Nipkow: cancel_sums works in general now |
|
13 |
(using Clemens Ballarin's code for ordered rewriting in abelian groups) |
|
14 |
and the whole file is reduced to a fraction of its former size. |
|
5589 | 15 |
*) |
16 |
||
17 |
signature ABEL_CANCEL = |
|
18 |
sig |
|
16569 | 19 |
val cancel_ss : simpset (*abelian group cancel simpset*) |
20 |
val thy_ref : theory_ref (*signature of the theory of the group*) |
|
21 |
val T : typ (*the type of group elements*) |
|
22 |
val eq_reflection : thm (*object-equality to meta-equality*) |
|
23 |
val eqI_rules : thm list |
|
24 |
val dest_eqI : thm -> term |
|
5589 | 25 |
end; |
26 |
||
27 |
||
28 |
functor Abel_Cancel (Data: ABEL_CANCEL) = |
|
29 |
struct |
|
30 |
||
5728
1d1175ef2d56
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents:
5610
diff
changeset
|
31 |
open Data; |
1d1175ef2d56
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents:
5610
diff
changeset
|
32 |
|
14756 | 33 |
fun zero t = Const ("0", t); |
34 |
fun minus t = Const ("uminus", t --> t); |
|
5589 | 35 |
|
16569 | 36 |
fun add_terms pos (Const ("op +", _) $ x $ y, ts) = |
37 |
add_terms pos (x, add_terms pos (y, ts)) |
|
38 |
| add_terms pos (Const ("op -", _) $ x $ y, ts) = |
|
39 |
add_terms pos (x, add_terms (not pos) (y, ts)) |
|
40 |
| add_terms pos (Const ("uminus", _) $ x, ts) = |
|
41 |
add_terms (not pos) (x, ts) |
|
42 |
| add_terms pos (x, ts) = (pos,x) :: ts; |
|
5589 | 43 |
|
16569 | 44 |
fun terms fml = add_terms true (fml, []); |
5589 | 45 |
|
16569 | 46 |
fun zero1 pt (u as (c as Const("op +",_)) $ x $ y) = |
47 |
(case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE |
|
48 |
| SOME z => SOME(c $ x $ z)) |
|
49 |
| SOME z => SOME(c $ z $ y)) |
|
50 |
| zero1 (pos,t) (u as (c as Const("op -",_)) $ x $ y) = |
|
51 |
(case zero1 (pos,t) x of |
|
52 |
NONE => (case zero1 (not pos,t) y of NONE => NONE |
|
53 |
| SOME z => SOME(c $ x $ z)) |
|
54 |
| SOME z => SOME(c $ z $ y)) |
|
55 |
| zero1 (pos,t) (u as (c as Const("uminus",_)) $ x) = |
|
56 |
(case zero1 (not pos,t) x of NONE => NONE |
|
57 |
| SOME z => SOME(c $ z)) |
|
58 |
| zero1 (pos,t) u = |
|
59 |
if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE |
|
5589 | 60 |
|
61 |
exception Cancel; |
|
62 |
||
63 |
val trace = ref false; |
|
64 |
||
16569 | 65 |
fun find_common _ [] _ = raise Cancel |
66 |
| find_common opp ((p,l)::ls) rs = |
|
67 |
let val pr = if opp then not p else p |
|
68 |
in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l) |
|
69 |
else find_common opp ls rs |
|
70 |
end |
|
5589 | 71 |
|
16569 | 72 |
(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc. |
73 |
If OP = +, it must be t2(-t) rather than t2(t) |
|
74 |
*) |
|
75 |
fun cancel sg t = |
|
76 |
let val _ = if !trace |
|
77 |
then tracing ("Abel cancel: " ^ string_of_cterm (cterm_of sg t)) |
|
78 |
else () |
|
79 |
val c $ lhs $ rhs = t |
|
80 |
val opp = case c of Const("op +",_) => true | _ => false; |
|
81 |
val (pos,l) = find_common opp (terms lhs) (terms rhs) |
|
82 |
val posr = if opp then not pos else pos |
|
83 |
val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs)) |
|
84 |
val _ = if !trace |
|
85 |
then tracing ("cancelled: " ^ string_of_cterm (cterm_of sg t')) |
|
86 |
else () |
|
87 |
in t' end; |
|
88 |
||
89 |
(* A simproc to cancel complementary terms in arbitrary sums. *) |
|
90 |
||
16973 | 91 |
fun sum_proc sg ss t = |
16569 | 92 |
let val t' = cancel sg t |
17956 | 93 |
val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t')) |
17877
67d5ab1cb0d8
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
wenzelm
parents:
16973
diff
changeset
|
94 |
(fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
15531 | 95 |
in SOME thm end |
96 |
handle Cancel => NONE; |
|
5589 | 97 |
|
13462 | 98 |
val sum_conv = |
5589 | 99 |
Simplifier.mk_simproc "cancel_sums" |
16423 | 100 |
(map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref)) |
13462 | 101 |
[("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax !???!!??! *) |
5589 | 102 |
sum_proc; |
103 |
||
104 |
||
105 |
(*A simproc to cancel like terms on the opposite sides of relations: |
|
106 |
(x + y - z < -z + x) = (y < 0) |
|
107 |
Works for (=) and (<=) as well as (<), if the necessary rules are supplied. |
|
16569 | 108 |
Reduces the problem to subtraction. |
5589 | 109 |
*) |
110 |
||
16973 | 111 |
fun rel_proc sg ss t = |
16569 | 112 |
let val t' = cancel sg t |
17956 | 113 |
val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t')) |
13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
114 |
(fn _ => rtac eq_reflection 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
115 |
resolve_tac eqI_rules 1 THEN |
17877
67d5ab1cb0d8
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
wenzelm
parents:
16973
diff
changeset
|
116 |
simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
15531 | 117 |
in SOME thm end |
118 |
handle Cancel => NONE; |
|
5589 | 119 |
|
13462 | 120 |
val rel_conv = |
16423 | 121 |
Simplifier.simproc_i (Theory.deref thy_ref) "cancel_relations" |
13462 | 122 |
(map Data.dest_eqI eqI_rules) rel_proc; |
5589 | 123 |
|
124 |
end; |