src/Provers/Arith/cancel_factor.ML
author immler@in.tum.de
Thu, 26 Feb 2009 10:13:43 +0100
changeset 30151 629f3a92863e
parent 29269 5c25a2012975
child 35408 b48ab741683b
permissions -rw-r--r--
removed global ref dfg_format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     1
(*  Title:      Provers/Arith/cancel_factor.ML
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     3
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     4
Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     5
*)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     6
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     7
signature CANCEL_FACTOR_DATA =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     8
sig
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     9
  (*abstract syntax*)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    10
  val mk_sum: term list -> term
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    11
  val dest_sum: term -> term list
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    12
  val mk_bal: term * term -> term
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    13
  val dest_bal: term -> term * term
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    14
  (*rules*)
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19250
diff changeset
    15
  val prove_conv: tactic -> tactic -> Proof.context -> term * term -> thm
23261
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    16
  val norm_tac: tactic (*AC0 etc.*)
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    17
  val multiply_tac: integer -> tactic
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    18
    (*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    19
end;
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    20
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    21
signature CANCEL_FACTOR =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    22
sig
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19250
diff changeset
    23
  val proc: simpset -> term -> thm option
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    24
end;
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    25
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    26
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    27
functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    28
struct
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    29
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    30
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    31
(* count terms *)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    32
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    33
fun ins_term (t, []) = [(t, 1)]
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    34
  | ins_term (t, (u, k) :: uks) =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    35
      if t aconv u then (u, k + 1) :: uks
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    36
      else (t, 1) :: (u, k) :: uks;
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    37
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 24630
diff changeset
    38
fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []);
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    39
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    40
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    41
(* divide sum *)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    42
23261
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    43
fun div_sum d =
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    44
  Data.mk_sum o maps (fn (t, k) => replicate (k div d) t);
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    45
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    46
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    47
(* the simplification procedure *)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    48
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19250
diff changeset
    49
fun proc ss t =
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    50
  (case try Data.dest_bal t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 4452
diff changeset
    51
    NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 4452
diff changeset
    52
  | SOME bal =>
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    53
      (case pairself Data.dest_sum bal of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 4452
diff changeset
    54
        ([_], _) => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 4452
diff changeset
    55
      | (_, [_]) => NONE
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    56
      | ts_us =>
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    57
          let
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    58
            val (tks, uks) = pairself count_terms ts_us;
23261
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    59
            val d = 0
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    60
              |> fold (Integer.gcd o snd) tks
85f27f79232f tuned integers
haftmann
parents: 20044
diff changeset
    61
              |> fold (Integer.gcd o snd) uks;
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    62
          in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 4452
diff changeset
    63
            if d = 0 orelse d = 1 then NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 4452
diff changeset
    64
            else SOME
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19250
diff changeset
    65
              (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss)
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23261
diff changeset
    66
                (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    67
          end));
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    68
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    69
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    70
end;