src/Provers/Arith/cancel_div_mod.ML
changeset 20044 92cc2f4c7335
parent 19233 77ca20b0ed77
child 22997 d4f3b015b50b
     1.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Sat Jul 08 12:54:29 2006 +0200
     1.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Sat Jul 08 12:54:30 2006 +0200
     1.3 @@ -22,13 +22,13 @@
     1.4    val div_mod_eqs: thm list
     1.5    (* (n*(m div n) + m mod n) + k == m + k and
     1.6       ((m div n)*n + m mod n) + k == m + k *)
     1.7 -  val prove_eq_sums: theory -> simpset -> term * term -> thm
     1.8 +  val prove_eq_sums: simpset -> term * term -> thm
     1.9    (* must prove ac0-equivalence of sums *)
    1.10  end;
    1.11  
    1.12  signature CANCEL_DIV_MOD =
    1.13  sig
    1.14 -  val proc: theory -> simpset -> term -> thm option
    1.15 +  val proc: simpset -> term -> thm option
    1.16  end;
    1.17  
    1.18  
    1.19 @@ -67,15 +67,15 @@
    1.20        val m = Data.mk_binop Data.mod_name pq
    1.21    in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
    1.22  
    1.23 -fun cancel thy ss t pq =
    1.24 -  let val teqt' = Data.prove_eq_sums thy ss (t, rearrange t pq)
    1.25 +fun cancel ss t pq =
    1.26 +  let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
    1.27    in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
    1.28  
    1.29 -fun proc thy ss t =
    1.30 +fun proc ss t =
    1.31    let val (divs,mods) = coll_div_mod t ([],[])
    1.32    in if null divs orelse null mods then NONE
    1.33       else case divs inter mods of
    1.34 -            pq :: _ => SOME(cancel thy ss t pq)
    1.35 +            pq :: _ => SOME (cancel ss t pq)
    1.36            | [] => NONE
    1.37    end
    1.38