src/Provers/Arith/cancel_factor.ML
author wenzelm
Mon, 16 Nov 1998 13:54:35 +0100
changeset 5897 b3548f939dd2
parent 4452 b2ee34200dab
child 15531 08c8dad8e399
permissions -rw-r--r--
removed genelim.ML;
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
    ID:         $Id$
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     4
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     5
Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
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
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     8
signature CANCEL_FACTOR_DATA =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
     9
sig
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    10
  (*abstract syntax*)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    11
  val mk_sum: term list -> term
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    12
  val dest_sum: term -> term list
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    13
  val mk_bal: term * term -> term
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    14
  val dest_bal: term -> term * term
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    15
  (*rules*)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    16
  val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    17
  val norm_tac: tactic			(*AC0 etc.*)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    18
  val multiply_tac: int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
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
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    23
  val proc: Sign.sg -> thm list -> term -> thm option
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
(* greatest common divisor *)
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 gcd (0, n) = n
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    34
  | gcd (m, n) = gcd (n mod m, m);
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    35
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    36
val gcds = foldl gcd;
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    37
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    38
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    39
(* count terms *)
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
fun ins_term (t, []) = [(t, 1)]
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    42
  | ins_term (t, (u, k) :: uks) =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    43
      if t aconv u then (u, k + 1) :: uks
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    44
      else (t, 1) :: (u, k) :: uks;
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    45
4452
b2ee34200dab adapted to new sort function;
wenzelm
parents: 4292
diff changeset
    46
fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);
4292
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    47
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    48
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    49
(* divide sum *)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    50
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    51
fun div_sum d tks =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    52
  Data.mk_sum (flat (map (fn (t, k) => replicate (k div d) t) tks));
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    53
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    54
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    55
(* the simplification procedure *)
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    56
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    57
fun proc sg _ t =
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    58
  (case try Data.dest_bal t of
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    59
    None => None
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    60
  | Some bal =>
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    61
      (case pairself Data.dest_sum bal of
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    62
        ([_], _) => None
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    63
      | (_, [_]) => None
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    64
      | ts_us =>
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    65
          let
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    66
            val (tks, uks) = pairself count_terms ts_us;
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    67
            val d = gcds (gcds (0, map snd tks), map snd uks);
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    68
          in
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    69
            if d = 0 orelse d = 1 then None
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    70
            else Some
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    71
              (Data.prove_conv (Data.multiply_tac d) Data.norm_tac sg
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    72
                (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    73
          end));
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    74
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    75
014771692751 Cancel common constant factor from balanced exression.
wenzelm
parents:
diff changeset
    76
end;