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