author | ballarin |
Wed, 17 Dec 2008 17:53:41 +0100 | |
changeset 29239 | 0a64c3418347 |
parent 27250 | 7eef2b183032 |
child 34974 | 18b41bba42b5 |
permissions | -rw-r--r-- |
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 (*object-equality to meta-equality*) |
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; |