src/Provers/Arith/cancel_div_mod.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 51717 9e7d1c139569
child 59582 0fbed69ff081
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
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 *)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 43594
diff changeset
    24
  val prove_eq_sums: Proof.context -> 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
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 43594
diff changeset
    30
  val proc: Proof.context -> cterm -> 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
43594
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    34
functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
13516
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
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 43594
diff changeset
    69
fun cancel ctxt t pq =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 43594
diff changeset
    70
  let val teqt' = Data.prove_eq_sums ctxt (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
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 43594
diff changeset
    73
fun proc ctxt ct =
43594
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    74
  let
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    75
    val t = term_of ct;
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    76
    val (divs, mods) = coll_div_mod t ([], []);
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    77
  in
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    78
    if null divs orelse null mods then NONE
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    79
    else
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    80
      (case inter (op =) mods divs of
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 43594
diff changeset
    81
        pq :: _ => SOME (cancel ctxt t pq)
43594
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    82
      | [] => NONE)
ef1ddc59b825 modernized some simproc setup;
wenzelm
parents: 36692
diff changeset
    83
  end;
13516
13a6103b9ac4 for cancelling div + mod.
nipkow
parents:
diff changeset
    84
17613
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    85
end