src/Provers/Arith/cancel_div_mod.ML
author wenzelm
Sat, 08 Jul 2006 12:54:30 +0200
changeset 20044 92cc2f4c7335
parent 19233 77ca20b0ed77
child 22997 d4f3b015b50b
permissions -rw-r--r--
simprocs: no theory argument -- use simpset context instead;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     1
(*  Title:      Provers/Arith/cancel_div_mod.ML
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow, TU Muenchen
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     4
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     5
Cancel div and mod terms:
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     6
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     7
  A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     8
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 17613
diff changeset
     9
FIXME: Is parameterized but assumes for simplicity that + and * are called
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 17613
diff changeset
    10
"HOL.plus" and "HOL.minus"
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    11
*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    12
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    13
signature CANCEL_DIV_MOD_DATA =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    14
sig
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    15
  (*abstract syntax*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    16
  val div_name: string
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    17
  val mod_name: string
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    18
  val mk_binop: string -> term * term -> term
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    19
  val mk_sum: term list -> term
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    20
  val dest_sum: term -> term list
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    21
  (*logic*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    22
  val div_mod_eqs: thm list
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    23
  (* (n*(m div n) + m mod n) + k == m + k and
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    24
     ((m div n)*n + m mod n) + k == m + k *)
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    25
  val prove_eq_sums: simpset -> term * term -> thm
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    26
  (* must prove ac0-equivalence of sums *)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    27
end;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    28
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    29
signature CANCEL_DIV_MOD =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    30
sig
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    31
  val proc: simpset -> term -> thm option
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    32
end;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    33
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    34
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    35
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    36
struct
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    37
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 17613
diff changeset
    38
fun coll_div_mod (Const("HOL.plus",_) $ s $ t) dms =
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    39
      coll_div_mod t (coll_div_mod s dms)
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 17613
diff changeset
    40
  | coll_div_mod (Const("HOL.times",_) $ m $ (Const(d,_) $ s $ n))
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    41
                 (dms as (divs,mods)) =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    42
      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 17613
diff changeset
    43
  | coll_div_mod (Const("HOL.times",_) $ (Const(d,_) $ s $ n) $ m)
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    44
                 (dms as (divs,mods)) =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    45
      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    46
  | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    47
      if m = Data.mod_name then (divs,(s,n)::mods) else dms
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    48
  | coll_div_mod _ dms = dms;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    49
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    50
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    51
(* Proof principle:
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    52
   1. (...div...)+(...mod...) == (div + mod) + rest
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    53
      in function rearrange
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    54
   2. (div + mod) + ?x = d + ?x
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    55
      Data.div_mod_eq
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    56
   ==> thesis by transitivity
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    57
*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    58
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 17613
diff changeset
    59
val mk_plus = Data.mk_binop "HOL.plus"
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 17613
diff changeset
    60
val mk_times = Data.mk_binop "HOL.times"
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    61
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    62
fun rearrange t pq =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    63
  let val ts = Data.dest_sum t;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    64
      val dpq = Data.mk_binop Data.div_name pq
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    65
      val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    66
      val d = if d1 mem ts then d1 else d2
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    67
      val m = Data.mk_binop Data.mod_name pq
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    68
  in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    69
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    70
fun cancel ss t pq =
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    71
  let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    72
  in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    73
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    74
fun proc ss t =
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    75
  let val (divs,mods) = coll_div_mod t ([],[])
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    76
  in if null divs orelse null mods then NONE
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    77
     else case divs inter mods of
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    78
            pq :: _ => SOME (cancel ss t pq)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    79
          | [] => NONE
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    80
  end
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    81
17613
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    82
end