src/Provers/Arith/cancel_div_mod.ML
author blanchet
Tue, 07 Dec 2010 11:56:01 +0100
changeset 41051 2ed1b971fc20
parent 36692 54b64d4ad524
child 43594 ef1ddc59b825
permissions -rw-r--r--
give the inner timeout mechanism a chance, since it gives more precise information to the user
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
    Author:     Tobias Nipkow, TU Muenchen
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     3
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     4
Cancel div and mod terms:
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     5
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     6
  A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
     7
22997
d4f3b015b50b canonical prefixing of class constants
haftmann
parents: 20044
diff changeset
     8
FIXME: Is parameterized but assumes for simplicity that + and * are named
34974
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 33049
diff changeset
     9
as in HOL
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    10
*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    11
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    12
signature CANCEL_DIV_MOD_DATA =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    13
sig
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    14
  (*abstract syntax*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    15
  val div_name: string
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    16
  val mod_name: string
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    17
  val mk_binop: string -> term * term -> term
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    18
  val mk_sum: term list -> term
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    19
  val dest_sum: term -> term list
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    20
  (*logic*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    21
  val div_mod_eqs: thm list
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    22
  (* (n*(m div n) + m mod n) + k == m + k and
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    23
     ((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
    24
  val prove_eq_sums: simpset -> term * term -> thm
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    25
  (* must prove ac0-equivalence of sums *)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    26
end;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    27
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    28
signature CANCEL_DIV_MOD =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    29
sig
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    30
  val proc: simpset -> term -> thm option
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    31
end;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    32
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    33
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    34
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    35
struct
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    36
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 34974
diff changeset
    37
fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    38
      coll_div_mod t (coll_div_mod s dms)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 34974
diff changeset
    39
  | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n))
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    40
                 (dms as (divs,mods)) =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    41
      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 34974
diff changeset
    42
  | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m)
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    43
                 (dms as (divs,mods)) =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    44
      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    45
  | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    46
      if m = Data.mod_name then (divs,(s,n)::mods) else dms
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    47
  | coll_div_mod _ dms = dms;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    48
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    49
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    50
(* Proof principle:
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    51
   1. (...div...)+(...mod...) == (div + mod) + rest
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    52
      in function rearrange
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    53
   2. (div + mod) + ?x = d + ?x
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    54
      Data.div_mod_eq
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    55
   ==> thesis by transitivity
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    56
*)
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    57
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 34974
diff changeset
    58
val mk_plus = Data.mk_binop @{const_name Groups.plus};
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 34974
diff changeset
    59
val mk_times = Data.mk_binop @{const_name Groups.times};
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    60
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    61
fun rearrange t pq =
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    62
  let val ts = Data.dest_sum t;
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    63
      val dpq = Data.mk_binop Data.div_name pq
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    64
      val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 35267
diff changeset
    65
      val d = if member (op =) ts d1 then d1 else d2
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    66
      val m = Data.mk_binop Data.mod_name pq
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33038
diff changeset
    67
  in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    68
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    69
fun cancel ss t pq =
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    70
  let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
30937
1fe5a573b552 whitespace tuning
haftmann
parents: 22997
diff changeset
    71
  in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    72
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    73
fun proc ss t =
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    74
  let val (divs,mods) = coll_div_mod t ([],[])
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    75
  in if null divs orelse null mods then NONE
33049
c38f02fdf35d curried inter as canonical list operation (beware of argument order)
haftmann
parents: 33040
diff changeset
    76
     else case inter (op =) mods divs of
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19233
diff changeset
    77
            pq :: _ => SOME (cancel ss t pq)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    78
          | [] => NONE
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    79
  end
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    80
17613
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    81
end