src/Provers/Arith/assoc_fold.ML
author immler@in.tum.de
Thu, 26 Feb 2009 10:13:43 +0100
changeset 30151 629f3a92863e
parent 25919 8b1c0d434824
child 30732 afca5be252d6
permissions -rw-r--r--
removed global ref dfg_format
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
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
     6
Simplification procedure for associative operators + and * on numeric
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
     7
types.  Performs constant folding when the literals are separated, as
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
     8
in 3+n+4.
7072
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
signature ASSOC_FOLD_DATA =
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    12
sig
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    13
  val assoc_ss: simpset
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    14
  val eq_reflection: thm
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    15
end;
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    16
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    17
signature ASSOC_FOLD =
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    18
sig
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    19
  val proc: simpset -> term -> thm option
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    20
end;
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    21
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    22
functor Assoc_Fold(Data: ASSOC_FOLD_DATA): ASSOC_FOLD =
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    23
struct
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    24
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    25
exception Assoc_fail;
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    26
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    27
fun mk_sum plus []  = raise Assoc_fail
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    28
  | mk_sum plus tms = foldr1 (fn (x, y) => plus $ x $ y) tms;
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    29
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    30
(*Separate the literals from the other terms being combined*)
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    31
fun sift_terms plus (t, (lits,others)) =
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    32
  (case t of
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 22997
diff changeset
    33
    Const (@{const_name Int.number_of}, _) $ _ =>       (* FIXME logic dependent *)
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    34
      (t::lits, others)         (*new literal*)
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    35
  | (f as Const _) $ x $ y =>
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    36
      if f = plus
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    37
      then sift_terms plus (x, sift_terms plus (y, (lits,others)))
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    38
      else (lits, t::others)    (*arbitrary summand*)
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    39
  | _ => (lits, t::others));
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    40
20055
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    41
(*A simproc to combine all literals in a associative nest*)
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    42
fun proc ss lhs =
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    43
  let
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    44
    val plus = (case lhs of f $ _ $ _ => f | _ => error "Assoc_fold: bad pattern")
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    45
    val (lits, others) = sift_terms plus (lhs, ([],[]))
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    46
    val _ = length lits < 2 andalso raise Assoc_fail (*we can't reduce the number of terms*)
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    47
    val rhs = plus $ mk_sum plus lits $ mk_sum plus others
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    48
    val th = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (lhs, rhs))
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    49
      (fn _ => rtac Data.eq_reflection 1 THEN
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    50
          simp_tac (Simplifier.inherit_context ss Data.assoc_ss) 1)
24c127b97ab5 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17956
diff changeset
    51
  in SOME th end handle Assoc_fail => NONE;
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12262
diff changeset
    52
7072
c3f3fd86e11c new simprocs assoc_fold and combine_coeff
paulson
parents:
diff changeset
    53
end;