src/Provers/Arith/abel_cancel.ML
author paulson
Thu, 01 Oct 1998 18:19:34 +0200
changeset 5589 94c05305fb29
child 5610 377acd99d74c
permissions -rw-r--r--
new simproc functor
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
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    15
  val ss	: simpset		(*basic simpset of object-logtic*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    16
  val mk_eq     : term * term -> term	(*create an equality proposition*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    17
  val mk_meta_eq: thm -> thm		(*object-equality to meta-equality*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    18
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    19
  val thy	: theory		(*the theory of the group*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    20
  val T		: typ			(*the type of group elements*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    21
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    22
  val zero	: term
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
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    26
  val add_assoc	: thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    27
  val add_commute : thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    28
  val add_left_commute : thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    29
  val add_0 : thm
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    30
  val add_0_right : thm
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
let open Data in
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    48
struct
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
    49
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 ()
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   116
       val ct = Thm.cterm_of sg (Data.mk_eq (lhs, rhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   117
       val thm = prove ct 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   118
		   (fn _ => [simp_tac prepare_ss 1,
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   119
			     IF_UNSOLVED (simp_tac cancel_ss 1),
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   120
			     IF_UNSOLVED (simp_tac inverse_ss 1)])
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   121
	 handle ERROR =>
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   122
	 error("cancel_sums simproc:\nfailed to prove " ^
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   123
	       string_of_cterm ct)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   124
   in Some (Data.mk_meta_eq thm) end
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   125
   handle Cancel => None;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   126
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   127
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   128
 val sum_conv = 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   129
     Simplifier.mk_simproc "cancel_sums"
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   130
       (map (Thm.read_cterm (sign_of Data.thy)) 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   131
	[("x + y", Data.T), ("x - y", Data.T)])
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   132
       sum_proc;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   133
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   134
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   135
 (*A simproc to cancel like terms on the opposite sides of relations:
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   136
     (x + y - z < -z + x) = (y < 0)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   137
   Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   138
   Reduces the problem to subtraction and calls the previous simproc.
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   139
 *)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   140
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   141
 (*Cancel the FIRST occurrence of a term.  If it's repeated, then repeated
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   142
   calls to the simproc will be needed.*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   143
 fun cancel1 ([], u)    = raise Match (*impossible: it's a common term*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   144
   | cancel1 (t::ts, u) = if t aconv u then ts
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   145
			  else t :: cancel1 (ts,u);
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   146
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   147
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   148
 val sum_cancel_ss = Data.ss addsimprocs [sum_conv]
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   149
			     addsimps    [add_0, add_0_right];
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   150
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   151
 val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   152
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   153
 fun rel_proc sg _ (lhs as (rel$lt$rt)) =
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   154
   let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   155
				       string_of_cterm (cterm_of sg lhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   156
	       else ()
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   157
       val ltms = terms lt
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   158
       and rtms = terms rt
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   159
       val common = (*inter_term miscounts repetitions, so squash them*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   160
		    gen_distinct (op aconv) (inter_term (ltms, rtms))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   161
       val _ = if null common then raise Cancel  (*nothing to do*)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   162
				   else ()
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   163
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   164
       fun cancelled tms = mk_sum (foldl cancel1 (tms, common))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   165
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   166
       val lt' = cancelled ltms
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   167
       and rt' = cancelled rtms
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   168
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   169
       val rhs = rel$lt'$rt'
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   170
       val _ = if !trace then 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   171
		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   172
	       else ()
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   173
       val ct = Thm.cterm_of sg (Data.mk_eq (lhs,rhs))
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   174
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   175
       val thm = prove ct 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   176
		   (fn _ => [resolve_tac eqI_rules 1,
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   177
			     simp_tac prepare_ss 1,
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   178
			     simp_tac sum_cancel_ss 1,
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   179
			     IF_UNSOLVED (simp_tac add_ac_ss 1)])
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   180
	 handle ERROR =>
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   181
	 error("cancel_relations simproc:\nfailed to prove " ^
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   182
	       string_of_cterm ct)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   183
   in Some (Data.mk_meta_eq thm) end
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   184
   handle Cancel => None;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   185
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   186
 val rel_conv = 
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   187
     Simplifier.mk_simproc "cancel_relations"
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   188
       (map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   189
       rel_proc;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   190
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   191
 end
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   192
end;
94c05305fb29 new simproc functor
paulson
parents:
diff changeset
   193