src/Provers/Arith/abel_cancel.ML
author paulson
Thu, 23 Sep 1999 13:09:39 +0200
changeset 7586 ae28545cd104
parent 6391 0da748358eff
child 8999 ad8260dc6e4a
permissions -rw-r--r--
The restrict_to_left rule fixes some bugs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     1
(*  Title:      Provers/Arith/abel_cancel.ML
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     2
    ID:         $Id$
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     5
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     6
Simplification procedures for abelian groups (e.g. integers, reals)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     7
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     8
- Cancel complementary terms in sums 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
     9
- Cancel like terms on opposite sides of relations
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    10
*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    11
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    12
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    13
signature ABEL_CANCEL =
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    14
sig
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    15
  val ss		: simpset	(*basic simpset of object-logtic*)
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    16
  val eq_reflection	: thm		(*object-equality to meta-equality*)
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    17
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    18
  val thy		: theory	(*the theory of the group*)
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    19
  val T			: typ		(*the type of group elements*)
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    20
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    21
  val zero		: term
7586
ae28545cd104 The restrict_to_left rule fixes some bugs
paulson
parents: 6391
diff changeset
    22
  val restrict_to_left  : thm
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    23
  val add_cancel_21	: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    24
  val add_cancel_end	: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    25
  val add_left_cancel	: thm
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    26
  val add_assoc		: thm
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    27
  val add_commute 	: thm
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    28
  val add_left_commute 	: thm
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    29
  val add_0 		: thm
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
    30
  val add_0_right 	: thm
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    31
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    32
  val eq_diff_eq 	: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    33
  val eqI_rules		: thm list
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    34
  val dest_eqI		: thm -> term
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    35
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    36
  val diff_def		: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    37
  val minus_add_distrib	: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    38
  val minus_minus	: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    39
  val minus_0		: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    40
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    41
  val add_inverses	: thm list
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    42
  val cancel_simps	: thm list
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    43
end;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    44
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    45
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    46
functor Abel_Cancel (Data: ABEL_CANCEL) =
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    47
struct
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    48
5728
1d1175ef2d56 eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents: 5610
diff changeset
    49
open Data;
1d1175ef2d56 eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents: 5610
diff changeset
    50
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    51
 val prepare_ss = Data.ss addsimps [add_assoc, diff_def, 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    52
				    minus_add_distrib, minus_minus,
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    53
				    minus_0, add_0, add_0_right];
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    54
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    55
 (*prove while suppressing timing information*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    56
 fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    57
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    58
 val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    59
 val minus = Const ("uminus", Data.T --> Data.T);
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    60
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    61
 (*Cancel corresponding terms on the two sides of the equation, NOT on
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    62
   the same side!*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    63
 val cancel_ss = 
7586
ae28545cd104 The restrict_to_left rule fixes some bugs
paulson
parents: 6391
diff changeset
    64
   Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ 
ae28545cd104 The restrict_to_left rule fixes some bugs
paulson
parents: 6391
diff changeset
    65
                    (map (fn th => th RS restrict_to_left) Data.cancel_simps);
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    66
7586
ae28545cd104 The restrict_to_left rule fixes some bugs
paulson
parents: 6391
diff changeset
    67
 val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps;
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    68
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    69
 fun mk_sum []  = Data.zero
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    70
   | mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    71
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    72
 (*We map -t to t and (in other cases) t to -t.  No need to check the type of
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    73
   uminus, since the simproc is only called on sums of type T.*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    74
 fun negate (Const("uminus",_) $ t) = t
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    75
   | negate t                       = minus $ t;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    76
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    77
 (*Flatten a formula built from +, binary - and unary -.
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    78
   No need to check types PROVIDED they are checked upon entry!*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    79
 fun add_terms neg (Const ("op +", _) $ x $ y, ts) =
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    80
	 add_terms neg (x, add_terms neg (y, ts))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    81
   | add_terms neg (Const ("op -", _) $ x $ y, ts) =
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    82
	 add_terms neg (x, add_terms (not neg) (y, ts))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    83
   | add_terms neg (Const ("uminus", _) $ x, ts) = 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    84
	 add_terms (not neg) (x, ts)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    85
   | add_terms neg (x, ts) = 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    86
	 (if neg then negate x else x) :: ts;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    87
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    88
 fun terms fml = add_terms false (fml, []);
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    89
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    90
 exception Cancel;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    91
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    92
 (*Cancels just the first occurrence of u, leaving the rest unchanged*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    93
 fun cancelled (u, t::ts) = if u aconv t then ts else t :: cancelled(u,ts)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    94
   | cancelled _          = raise Cancel;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    95
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    96
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    97
 val trace = ref false;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    98
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    99
 (*Make a simproc to cancel complementary terms in sums.  Examples:
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   100
    x-x = 0    x+(y-x) = y   -x+(y+(x+z)) = y+z
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   101
   It will unfold the definition of diff and associate to the right if 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   102
   necessary.  Rewriting is faster if the formula is already
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   103
   in that form.
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   104
 *)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   105
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   106
 fun sum_proc sg _ lhs =
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   107
   let val _ = if !trace then writeln ("cancel_sums: LHS = " ^ 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   108
				       string_of_cterm (cterm_of sg lhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   109
	       else ()
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   110
       val (head::tail) = terms lhs
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   111
       val head' = negate head
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   112
       val rhs = mk_sum (cancelled (head',tail))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   113
       and chead' = Thm.cterm_of sg head'
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   114
       val _ = if !trace then 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   115
		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   116
	       else ()
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   117
       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   118
       val thm = prove ct 
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   119
		   (fn _ => [rtac eq_reflection 1,
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   120
			     simp_tac prepare_ss 1,
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   121
			     IF_UNSOLVED (simp_tac cancel_ss 1),
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   122
			     IF_UNSOLVED (simp_tac inverse_ss 1)])
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   123
	 handle ERROR =>
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   124
	 error("cancel_sums simproc:\nfailed to prove " ^
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   125
	       string_of_cterm ct)
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   126
   in Some thm end
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   127
   handle Cancel => None;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   128
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   129
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   130
 val sum_conv = 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   131
     Simplifier.mk_simproc "cancel_sums"
6391
0da748358eff Theory.sign_of;
wenzelm
parents: 5728
diff changeset
   132
       (map (Thm.read_cterm (Theory.sign_of Data.thy)) 
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   133
	[("x + y", Data.T), ("x - y", Data.T)])
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   134
       sum_proc;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   135
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   136
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   137
 (*A simproc to cancel like terms on the opposite sides of relations:
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   138
     (x + y - z < -z + x) = (y < 0)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   139
   Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   140
   Reduces the problem to subtraction and calls the previous simproc.
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   141
 *)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   142
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   143
 (*Cancel the FIRST occurrence of a term.  If it's repeated, then repeated
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   144
   calls to the simproc will be needed.*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   145
 fun cancel1 ([], u)    = raise Match (*impossible: it's a common term*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   146
   | cancel1 (t::ts, u) = if t aconv u then ts
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   147
			  else t :: cancel1 (ts,u);
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   148
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   149
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   150
 val sum_cancel_ss = Data.ss addsimprocs [sum_conv]
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   151
			     addsimps    [add_0, add_0_right];
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   152
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   153
 val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   154
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   155
 fun rel_proc sg _ (lhs as (rel$lt$rt)) =
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   156
   let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   157
				       string_of_cterm (cterm_of sg lhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   158
	       else ()
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   159
       val ltms = terms lt
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   160
       and rtms = terms rt
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   161
       val common = (*inter_term miscounts repetitions, so squash them*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   162
		    gen_distinct (op aconv) (inter_term (ltms, rtms))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   163
       val _ = if null common then raise Cancel  (*nothing to do*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   164
				   else ()
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   165
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   166
       fun cancelled tms = mk_sum (foldl cancel1 (tms, common))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   167
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   168
       val lt' = cancelled ltms
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   169
       and rt' = cancelled rtms
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   170
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   171
       val rhs = rel$lt'$rt'
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   172
       val _ = if !trace then 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   173
		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   174
	       else ()
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   175
       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   176
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   177
       val thm = prove ct 
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   178
		   (fn _ => [rtac eq_reflection 1,
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   179
			     resolve_tac eqI_rules 1,
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   180
			     simp_tac prepare_ss 1,
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   181
			     simp_tac sum_cancel_ss 1,
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   182
			     IF_UNSOLVED (simp_tac add_ac_ss 1)])
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   183
	 handle ERROR =>
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   184
	 error("cancel_relations simproc:\nfailed to prove " ^
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   185
	       string_of_cterm ct)
5610
377acd99d74c simpler interface for Abel_Cancel
paulson
parents: 5589
diff changeset
   186
   in Some thm end
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   187
   handle Cancel => None;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   188
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   189
 val rel_conv = 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   190
     Simplifier.mk_simproc "cancel_relations"
6391
0da748358eff Theory.sign_of;
wenzelm
parents: 5728
diff changeset
   191
       (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI) eqI_rules)
5589
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   192
       rel_proc;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   193
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   194
end;