src/Provers/Arith/assoc_fold.ML
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 9419 e46de4af70e4
child 12262 11ff5f47df6e
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     1
(*  Title:      Provers/Arith/assoc_fold.ML
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     2
    ID:         $Id$
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     5
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     6
Simplification procedure for associative operators + and * on numeric types
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     7
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     8
Performs constant folding when the literals are separated, as in 3+n+4.
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
     9
*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    10
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    11
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    12
signature ASSOC_FOLD_DATA =
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    13
sig
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    14
  val ss		: simpset	(*basic simpset of object-logtic*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    15
  val eq_reflection	: thm		(*object-equality to meta-equality*)
9419
e46de4af70e4 do not pass theory values, but sg_ref;
wenzelm
parents: 8999
diff changeset
    16
  val sg_ref 		: Sign.sg_ref	(*the operator's signature*)
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    17
  val T			: typ		(*the operator's numeric type*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    18
  val plus		: term		(*the operator being folded*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    19
  val add_ac		: thm list      (*AC-rewrites for plus*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    20
end;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    21
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    22
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    23
functor Assoc_Fold (Data: ASSOC_FOLD_DATA) =
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    24
struct
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    25
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    26
 val assoc_ss = Data.ss addsimps Data.add_ac;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    27
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    28
 (*prove while suppressing timing information*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    29
 fun prove name ct tacf = 
8999
ad8260dc6e4a global timing flag;
wenzelm
parents: 8857
diff changeset
    30
     setmp Library.timing false (prove_goalw_cterm [] ct) tacf
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    31
     handle ERROR =>
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    32
	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    33
                
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    34
 exception Assoc_fail;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    35
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    36
 fun mk_sum []  = raise Assoc_fail
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    37
   | mk_sum tms = foldr1 (fn (x,y) => Data.plus $ x $ y) tms;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    38
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    39
 (*Separate the literals from the other terms being combined*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    40
 fun sift_terms (t, (lits,others)) =
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    41
     case t of
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    42
	  Const("Numeral.number_of", _) $ _ =>
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    43
	      (t::lits, others)         (*new literal*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    44
	| (f as Const _) $ x $ y =>
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    45
	      if f = Data.plus 
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    46
              then sift_terms (x, sift_terms (y, (lits,others)))
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    47
	      else (lits, t::others)    (*arbitrary summand*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    48
	| _ => (lits, t::others);
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    49
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    50
 val trace = ref false;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    51
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    52
 (*Make a simproc to combine all literals in a associative nest*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    53
 fun proc sg _ lhs =
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    54
   let fun show t = string_of_cterm (Thm.cterm_of sg t)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    55
       val _ = if !trace then writeln ("assoc_fold simproc: LHS = " ^ show lhs)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    56
	       else ()
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    57
       val (lits,others) = sift_terms (lhs, ([],[]))
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    58
       val _ = if length lits < 2
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    59
               then raise Assoc_fail (*we can't reduce the number of terms*)
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    60
               else ()  
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    61
       val rhs = Data.plus $ mk_sum lits $ mk_sum others
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    62
       val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    63
       val th = prove "assoc_fold" 
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    64
	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    65
		   (fn _ => [rtac Data.eq_reflection 1,
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    66
			     simp_tac assoc_ss 1])
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    67
   in Some th end
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    68
   handle Assoc_fail => None;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    69
 
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    70
 val conv = 
8857
7ec405405dd7 improved name of simproc;
wenzelm
parents: 7072
diff changeset
    71
     Simplifier.mk_simproc "assoc_fold"
9419
e46de4af70e4 do not pass theory values, but sg_ref;
wenzelm
parents: 8999
diff changeset
    72
       [Thm.cterm_of (Sign.deref Data.sg_ref)
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    73
	             (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    74
       proc;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    75
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    76
end;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    77
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    78
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    79
(*test data:
8999
ad8260dc6e4a global timing flag;
wenzelm
parents: 8857
diff changeset
    80
set timing;
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    81
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    82
Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)";
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    83
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    84
Goal "a + b + c + d + e + f + g + h + i + j + k + l + m + n + oo + p + q + r + s + t + u + v + (w + x + y + z + a + #2 + b + #2 + c + #2 + d + #2 + e) + #2 + f + (#2 + g + #2 + h + #2 + i) + #2 + (j + #2 + k + #2 + l + #2 + m + #2) + n + #2 + (oo + #2 + p + #2 + q + #2 + r) + #2 + s + #2 + t + #2 + u + #2 + v + #2 + w + #2 + x + #2 + y + #2 + z + #2 = (uu::nat)";
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    85
*)