# HG changeset patch
# User haftmann
# Date 1507494501 -7200
# Node ID cc2b490f9dc4496a1414d0c75bfac7fb43e6b491
# Parent  f6a30d48aab014edeaa38b6e18dca4821103d4fb
generalized simproc

diff -r f6a30d48aab0 -r cc2b490f9dc4 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -527,25 +527,6 @@
 
 end
 
-ML \<open>
-structure Cancel_Div_Mod_Int = Cancel_Div_Mod
-(
-  val div_name = @{const_name divide};
-  val mod_name = @{const_name modulo};
-  val mk_binop = HOLogic.mk_binop;
-  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
-  val dest_sum = Arith_Data.dest_sum;
-
-  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
-
-  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
-    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
-)
-\<close>
-
-simproc_setup cancel_div_mod_int ("(k::int) + l") =
-  \<open>K Cancel_Div_Mod_Int.proc\<close>
-
 lemma is_unit_int:
   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   by auto
diff -r f6a30d48aab0 -r cc2b490f9dc4 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -9,16 +9,6 @@
   imports Nat_Transfer Lattices_Big
 begin
 
-subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
-
-lemma (in semiring_modulo) cancel_div_mod_rules:
-  "((a div b) * b + a mod b) + c = a + c"
-  "(b * (a div b) + a mod b) + c = a + c"
-  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
-
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
-
 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
   
 class euclidean_semiring = semidom_modulo + normalization_semidom + 
@@ -767,9 +757,10 @@
   val mk_binop = HOLogic.mk_binop;
   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
-  fun mk_sum [] = HOLogic.zero
-    | mk_sum [t] = t
-    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+  fun mk_sum' [] = HOLogic.zero
+    | mk_sum' [t] = t
+    | mk_sum' (t :: ts) = mk_plus (t, mk_sum' ts);
+  fun mk_sum _ = mk_sum';
   fun dest_sum tm =
     if HOLogic.is_zero tm then []
     else
diff -r f6a30d48aab0 -r cc2b490f9dc4 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -10,10 +10,6 @@
 imports Inductive Typedef Fun Rings
 begin
 
-named_theorems arith "arith facts -- only ground formulas"
-ML_file "Tools/arith_data.ML"
-
-
 subsection \<open>Type \<open>ind\<close>\<close>
 
 typedecl ind
diff -r f6a30d48aab0 -r cc2b490f9dc4 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1624,8 +1624,39 @@
   "b dvd a - a mod b"
   by (simp add: minus_mod_eq_div_mult)
 
+lemma cancel_div_mod_rules:
+  "((a div b) * b + a mod b) + c = a + c"
+  "(b * (a div b) + a mod b) + c = a + c"
+  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
 end
 
+text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
+
+named_theorems arith "arith facts -- only ground formulas"
+ML_file "Tools/arith_data.ML"
+
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
+ML \<open>
+structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
+(
+  val div_name = @{const_name divide};
+  val mod_name = @{const_name modulo};
+  val mk_binop = HOLogic.mk_binop;
+  val mk_sum = Arith_Data.mk_sum;
+  val dest_sum = Arith_Data.dest_sum;
+
+  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
+)
+\<close>
+
+simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
+  \<open>K Cancel_Div_Mod_Ring.proc\<close>
+
 class idom_modulo = idom + semidom_modulo
 begin
 
diff -r f6a30d48aab0 -r cc2b490f9dc4 src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML	Sun Oct 08 22:28:21 2017 +0200
@@ -15,7 +15,7 @@
   val div_name: string
   val mod_name: string
   val mk_binop: string -> term * term -> term
-  val mk_sum: term list -> term
+  val mk_sum: typ -> term list -> term
   val dest_sum: term -> term list
   (*logic*)
   val div_mod_eqs: thm list
@@ -34,16 +34,16 @@
 functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
 struct
 
-fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
+fun coll_div_mod (Const (@{const_name Groups.plus}, _) $ s $ t) dms =
       coll_div_mod t (coll_div_mod s dms)
-  | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n))
-                 (dms as (divs,mods)) =
-      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
-  | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m)
-                 (dms as (divs,mods)) =
-      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
-  | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
-      if m = Data.mod_name then (divs,(s,n)::mods) else dms
+  | coll_div_mod (Const (@{const_name Groups.times}, _) $ m $ (Const (d, _) $ s $ n))
+                 (dms as (divs, mods)) =
+      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
+  | coll_div_mod (Const (@{const_name Groups.times}, _) $ (Const (d, _) $ s $ n) $ m)
+                 (dms as (divs, mods)) =
+      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
+  | coll_div_mod (Const (m, _) $ s $ n) (dms as (divs, mods)) =
+      if m = Data.mod_name then (divs, (s, n) :: mods) else dms
   | coll_div_mod _ dms = dms;
 
 
@@ -58,16 +58,18 @@
 val mk_plus = Data.mk_binop @{const_name Groups.plus};
 val mk_times = Data.mk_binop @{const_name Groups.times};
 
-fun rearrange t pq =
-  let val ts = Data.dest_sum t;
-      val dpq = Data.mk_binop Data.div_name pq
-      val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
-      val d = if member (op =) ts d1 then d1 else d2
-      val m = Data.mk_binop Data.mod_name pq
-  in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
+fun rearrange T t pq =
+  let
+    val ts = Data.dest_sum t;
+    val dpq = Data.mk_binop Data.div_name pq;
+    val d1 = mk_times (snd pq, dpq) and d2 = mk_times (dpq, snd pq);
+    val d = if member (op =) ts d1 then d1 else d2;
+    val m = Data.mk_binop Data.mod_name pq;
+  in mk_plus (mk_plus (d, m), Data.mk_sum T (ts |> remove (op =) d |> remove (op =) m)) end
 
 fun cancel ctxt t pq =
-  let val teqt' = Data.prove_eq_sums ctxt (t, rearrange t pq)
+  let
+    val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq);
   in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
 
 fun proc ctxt ct =