# HG changeset patch
# User paulson
# Date 1554840348 -3600
# Node ID c4f2cac288d27da17567dbc75ef8b96504695efe
# Parent  a93e6472ac9c3b050c966f29bc951aee44f1c4e4# Parent  e8f4ce87012b82dc229541ff0da60b6981f60593
merged

diff -r e8f4ce87012b -r c4f2cac288d2 Admin/lib/Tools/regenerate_cooper
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/regenerate_cooper	Tue Apr 09 21:05:48 2019 +0100
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+#
+# Author: Florian Haftmann, TU Muenchen
+#
+# DESCRIPTION: regenerate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML from ~~/src/HOL/Decision_Proc/Cooper.thy
+
+session=HOL-Decision_Procs
+src='HOL-Decision_Procs.Cooper:code/cooper_procedure.ML'
+dst='~~/src/HOL/Tools/Qelim/'
+
+"${ISABELLE_TOOL}" build "${session}"
+"${ISABELLE_TOOL}" export -x "${src}" -p 2 -O "${dst}" "${session}"
diff -r e8f4ce87012b -r c4f2cac288d2 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Tue Apr 09 21:05:32 2019 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Apr 09 21:05:48 2019 +0100
@@ -2,15 +2,15 @@
     Author:     Amine Chaieb
 *)
 
+section \<open>Presburger arithmetic based on Cooper's algorithm\<close>
+
 theory Cooper
 imports
   Complex_Main
   "HOL-Library.Code_Target_Numeral"
 begin
 
-section \<open>Periodicity of \<open>dvd\<close>\<close>
-
-subsection \<open>Shadow syntax and semantics\<close>
+subsection \<open>Basic formulae\<close>
 
 datatype (plugins del: size) num = C int | Bound nat | CN nat int num
   | Neg num | Add num num | Sub num num
@@ -146,7 +146,7 @@
   | "qfree p \<longleftrightarrow> True"
 
 
-text \<open>Boundedness and substitution\<close>
+subsection \<open>Boundedness and substitution\<close>
 
 primrec numbound0 :: "num \<Rightarrow> bool"  \<comment> \<open>a \<open>num\<close> is \<^emph>\<open>independent\<close> of Bound 0\<close>
   where
@@ -418,7 +418,7 @@
 qed
 
 
-text \<open>Simplification\<close>
+subsection \<open>Simplification\<close>
 
 text \<open>Algebraic simplifications for nums\<close>
 
@@ -819,7 +819,9 @@
   apply (case_tac "simpnum a", auto)+
   done
 
-text \<open>Generic quantifier elimination\<close>
+
+subsection \<open>Generic quantifier elimination\<close>
+
 fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   where
     "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
@@ -2249,7 +2251,7 @@
 qed
 
 
-text \<open>Cooper's Algorithm\<close>
+subsection \<open>Cooper's Algorithm\<close>
 
 definition cooper :: "fm \<Rightarrow> fm"
 where
@@ -2371,16 +2373,8 @@
 theorem mirqe: "Ifm bbs bs (pa p) = Ifm bbs bs p \<and> qfree (pa p)"
   using qelim_ci cooper prep by (auto simp add: pa_def)
 
-definition cooper_test :: "unit \<Rightarrow> fm"
-  where "cooper_test u =
-    pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
-      (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
 
-ML_val \<open>@{code cooper_test} ()\<close>
-
-(*code_reflect Cooper_Procedure
-  functions pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int
-  file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*)
+subsection \<open>Setup\<close>
 
 oracle linzqe_oracle = \<open>
 let
@@ -2535,7 +2529,7 @@
 \<close> "decision procedure for linear integer arithmetic"
 
 
-text \<open>Tests\<close>
+subsection \<open>Tests\<close>
 
 lemma "\<exists>(j::int). \<forall>x\<ge>j. \<exists>a b. x = 3*a+5*b"
   by cooper
@@ -2666,4 +2660,10 @@
 theorem "(\<exists>m::nat. n = 2 * m) \<longrightarrow> (n + 1) div 2 = n div 2"
   by cooper
 
+
+subsection \<open>Variant for HOL-Main\<close>
+
+export_code pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int
+  in Eval module_name Cooper_Procedure file_prefix cooper_procedure
+
 end
diff -r e8f4ce87012b -r c4f2cac288d2 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Tue Apr 09 21:05:32 2019 +0100
+++ b/src/HOL/Euclidean_Division.thy	Tue Apr 09 21:05:48 2019 +0100
@@ -165,25 +165,31 @@
 
 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
 
-class euclidean_semiring_cancel = euclidean_semiring +
-  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
-  and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
+class euclidean_semiring_cancel = euclidean_semiring + semidom_divide_cancel
 begin
 
+context
+  fixes b
+  assumes "b \<noteq> 0"
+begin
+
+lemma div_mult_self1 [simp]:
+  "(a + c * b) div b = c + a div b"
+  using \<open>b \<noteq> 0\<close> by (rule div_mult_self1)
+
 lemma div_mult_self2 [simp]:
-  assumes "b \<noteq> 0"
-  shows "(a + b * c) div b = c + a div b"
-  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
+  "(a + b * c) div b = c + a div b"
+  using \<open>b \<noteq> 0\<close> by (rule div_mult_self2)
 
 lemma div_mult_self3 [simp]:
-  assumes "b \<noteq> 0"
-  shows "(c * b + a) div b = c + a div b"
-  using assms by (simp add: add.commute)
+  "(c * b + a) div b = c + a div b"
+  using \<open>b \<noteq> 0\<close> by (rule div_mult_self3)
 
 lemma div_mult_self4 [simp]:
-  assumes "b \<noteq> 0"
-  shows "(b * c + a) div b = c + a div b"
-  using assms by (simp add: add.commute)
+  "(b * c + a) div b = c + a div b"
+  using \<open>b \<noteq> 0\<close> by (rule div_mult_self4)
+
+end
 
 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
 proof (cases "b = 0")
@@ -194,7 +200,7 @@
     by (simp add: div_mult_mod_eq)
   also from False div_mult_self1 [of b a c] have
     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
-      by (simp add: algebra_simps)
+    by (simp add: algebra_simps)
   finally have "a = a div b * b + (a + c * b) mod b"
     by (simp add: add.commute [of a] add.assoc distrib_right)
   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
@@ -222,16 +228,6 @@
   "a * b mod b = 0"
   using mod_mult_self1 [of 0 a b] by simp
 
-lemma div_add_self1:
-  assumes "b \<noteq> 0"
-  shows "(b + a) div b = a div b + 1"
-  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
-
-lemma div_add_self2:
-  assumes "b \<noteq> 0"
-  shows "(a + b) div b = a div b + 1"
-  using assms div_add_self1 [of b a] by (simp add: add.commute)
-
 lemma mod_add_self1 [simp]:
   "(b + a) mod b = a mod b"
   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
@@ -284,14 +280,6 @@
   finally show ?thesis .
 qed
 
-lemma div_mult_mult2 [simp]:
-  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
-  by (drule div_mult_mult1) (simp add: mult.commute)
-
-lemma div_mult_mult1_if [simp]:
-  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
-  by simp_all
-
 lemma mod_mult_mult1:
   "(c * a) mod (c * b) = c * (a mod b)"
 proof (cases "c = 0")
@@ -448,23 +436,14 @@
 class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
 begin
 
-subclass idom_divide ..
-
-lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
-  using div_mult_mult1 [of "- 1" a b] by simp
+subclass idom_divide_cancel ..
 
 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   using mod_mult_mult1 [of "- 1" a b] by simp
 
-lemma div_minus_right: "a div (- b) = (- a) div b"
-  using div_minus_minus [of "- a" b] by simp
-
 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   using mod_minus_minus [of "- a" b] by simp
 
-lemma div_minus1_right [simp]: "a div (- 1) = - a"
-  using div_minus_right [of a 1] by simp
-
 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   using mod_minus_right [of a 1] by simp
 
diff -r e8f4ce87012b -r c4f2cac288d2 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Apr 09 21:05:32 2019 +0100
+++ b/src/HOL/Fields.thy	Tue Apr 09 21:05:48 2019 +0100
@@ -378,30 +378,42 @@
     by (simp add: divide_inverse)
 qed
 
+subclass idom_divide_cancel
+proof
+  fix a b c
+  assume [simp]: "c \<noteq> 0"
+  show "(c * a) / (c * b) = a / b"
+  proof (cases "b = 0")
+    case True then show ?thesis
+      by simp
+  next
+    case False
+    then have "(c * a) / (c * b) = c * a * (inverse b * inverse c)"
+      by (simp add: divide_inverse nonzero_inverse_mult_distrib)
+    also have "... =  a * inverse b * (inverse c * c)"
+      by (simp only: ac_simps)
+    also have "... =  a * inverse b" by simp
+    finally show ?thesis by (simp add: divide_inverse)
+  qed
+next
+  fix a b c
+  assume "b \<noteq> 0"
+  have "((a * inverse b) * b + c * b) = (c + a * inverse b) * b"
+    using distrib [of c "a * inverse b" b] by (simp add: ac_simps)
+  also have "(a * inverse b) * b = a"
+    using \<open>b \<noteq> 0\<close> by (simp add: ac_simps)
+  finally show "(a + c * b) / b = c + a / b"
+    using \<open>b \<noteq> 0\<close> by (simp add: ac_simps divide_inverse [symmetric])
+qed
+
+lemmas nonzero_mult_divide_mult_cancel_left = div_mult_mult1 \<comment> \<open>duplicate\<close>
+lemmas nonzero_mult_divide_mult_cancel_right = div_mult_mult2 \<comment> \<open>duplicate\<close>
+
 text\<open>There is no slick version using division by zero.\<close>
 lemma inverse_add:
   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
   by (simp add: division_ring_inverse_add ac_simps)
 
-lemma nonzero_mult_divide_mult_cancel_left [simp]:
-  assumes [simp]: "c \<noteq> 0"
-  shows "(c * a) / (c * b) = a / b"
-proof (cases "b = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
-    by (simp add: divide_inverse nonzero_inverse_mult_distrib)
-  also have "... =  a * inverse b * (inverse c * c)"
-    by (simp only: ac_simps)
-  also have "... =  a * inverse b" by simp
-    finally show ?thesis by (simp add: divide_inverse)
-qed
-
-lemma nonzero_mult_divide_mult_cancel_right [simp]:
-  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
-  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
-
 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   by (simp add: divide_inverse ac_simps)
 
diff -r e8f4ce87012b -r c4f2cac288d2 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Apr 09 21:05:32 2019 +0100
+++ b/src/HOL/Rings.thy	Tue Apr 09 21:05:48 2019 +0100
@@ -1699,6 +1699,69 @@
 end
 
 
+text \<open>Integral (semi)domains with cancellation rules\<close>
+
+class semidom_divide_cancel = semidom_divide +
+  assumes div_mult_self1: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+    and div_mult_mult1: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
+begin
+
+context
+  fixes b
+  assumes "b \<noteq> 0"
+begin
+
+lemma div_mult_self2:
+  "(a + b * c) div b = c + a div b"
+  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
+
+lemma div_mult_self3:
+  "(c * b + a) div b = c + a div b"
+  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
+
+lemma div_mult_self4:
+  "(b * c + a) div b = c + a div b"
+  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
+
+lemma div_add_self1:
+  "(b + a) div b = a div b + 1"
+  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a 1] by (simp add: ac_simps)
+
+lemma div_add_self2:
+  "(a + b) div b = a div b + 1"
+  using \<open>b \<noteq> 0\<close> div_add_self1 [of a] by (simp add: ac_simps)
+
+end
+
+lemma div_mult_mult2:
+  "(a * c) div (b * c) = a div b" if "c \<noteq> 0"
+  using that div_mult_mult1 [of c a b] by (simp add: ac_simps)
+
+lemma div_mult_mult1_if [simp]:
+  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
+  by (simp add: div_mult_mult1)
+
+lemma div_mult_mult2_if [simp]:
+  "(a * c) div (b * c) = (if c = 0 then 0 else a div b)"
+  using div_mult_mult1_if [of c a b] by (simp add: ac_simps)
+
+end
+
+class idom_divide_cancel = idom_divide + semidom_divide_cancel
+begin
+
+lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
+  using div_mult_mult1 [of "- 1" a b] by simp
+
+lemma div_minus_right: "a div (- b) = (- a) div b"
+  using div_minus_minus [of "- a" b] by simp
+
+lemma div_minus1_right [simp]: "a div (- 1) = - a"
+  using div_minus_right [of a 1] by simp
+
+end
+
+
 text \<open>Quotient and remainder in integral domains\<close>
 
 class semidom_modulo = algebraic_semidom + semiring_modulo
diff -r e8f4ce87012b -r c4f2cac288d2 src/HOL/Tools/Qelim/cooper_procedure.ML
--- a/src/HOL/Tools/Qelim/cooper_procedure.ML	Tue Apr 09 21:05:32 2019 +0100
+++ b/src/HOL/Tools/Qelim/cooper_procedure.ML	Tue Apr 09 21:05:48 2019 +0100
@@ -1,5 +1,3 @@
-(* Generated from Cooper.thy; DO NOT EDIT! *)
-
 structure Cooper_Procedure : sig
   datatype inta = Int_of_integer of int
   val integer_of_int : inta -> int
@@ -89,25 +87,29 @@
 
 val minus_int = {minus = minus_inta} : inta minus;
 
-fun sgn_integer k =
-  (if k = (0 : IntInf.int) then (0 : IntInf.int)
-    else (if k < (0 : IntInf.int) then (~1 : IntInf.int)
-           else (1 : IntInf.int)));
-
 fun apsnd f (x, y) = (x, f y);
 
 fun divmod_integer k l =
   (if k = (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int))
-    else (if l = (0 : IntInf.int) then ((0 : IntInf.int), k)
-           else (apsnd o (fn a => fn b => a * b) o sgn_integer) l
-                  (if sgn_integer k = sgn_integer l
-                    then Integer.div_mod (abs k) (abs l)
-                    else let
-                           val (r, s) = Integer.div_mod (abs k) (abs l);
-                         in
-                           (if s = (0 : IntInf.int) then (~ r, (0 : IntInf.int))
-                             else (~ r - (1 : IntInf.int), abs l - s))
-                         end)));
+    else (if (0 : IntInf.int) < l
+           then (if (0 : IntInf.int) < k then Integer.div_mod (abs k) (abs l)
+                  else let
+                         val (r, s) = Integer.div_mod (abs k) (abs l);
+                       in
+                         (if s = (0 : IntInf.int) then (~ r, (0 : IntInf.int))
+                           else (~ r - (1 : IntInf.int), l - s))
+                       end)
+           else (if l = (0 : IntInf.int) then ((0 : IntInf.int), k)
+                  else apsnd (fn a => ~ a)
+                         (if k < (0 : IntInf.int)
+                           then Integer.div_mod (abs k) (abs l)
+                           else let
+                                  val (r, s) = Integer.div_mod (abs k) (abs l);
+                                in
+                                  (if s = (0 : IntInf.int)
+                                    then (~ r, (0 : IntInf.int))
+                                    else (~ r - (1 : IntInf.int), ~ l - s))
+                                end))));
 
 fun fst (x1, x2) = x1;
 
@@ -506,6 +508,11 @@
       semiring_no_zero_divisors_cancel_int}
   : inta semidom_divide;
 
+type 'a algebraic_semidom =
+  {semidom_divide_algebraic_semidom : 'a semidom_divide};
+val semidom_divide_algebraic_semidom = #semidom_divide_algebraic_semidom :
+  'a algebraic_semidom -> 'a semidom_divide;
+
 type 'a semiring_modulo =
   {comm_semiring_1_cancel_semiring_modulo : 'a comm_semiring_1_cancel,
     modulo_semiring_modulo : 'a modulo};
@@ -515,20 +522,6 @@
 val modulo_semiring_modulo = #modulo_semiring_modulo :
   'a semiring_modulo -> 'a modulo;
 
-val semiring_modulo_int =
-  {comm_semiring_1_cancel_semiring_modulo = comm_semiring_1_cancel_int,
-    modulo_semiring_modulo = modulo_int}
-  : inta semiring_modulo;
-
-type 'a algebraic_semidom =
-  {semidom_divide_algebraic_semidom : 'a semidom_divide};
-val semidom_divide_algebraic_semidom = #semidom_divide_algebraic_semidom :
-  'a algebraic_semidom -> 'a semidom_divide;
-
-val algebraic_semidom_int =
-  {semidom_divide_algebraic_semidom = semidom_divide_int} :
-  inta algebraic_semidom;
-
 type 'a semidom_modulo =
   {algebraic_semidom_semidom_modulo : 'a algebraic_semidom,
     semiring_modulo_semidom_modulo : 'a semiring_modulo};
@@ -537,6 +530,15 @@
 val semiring_modulo_semidom_modulo = #semiring_modulo_semidom_modulo :
   'a semidom_modulo -> 'a semiring_modulo;
 
+val algebraic_semidom_int =
+  {semidom_divide_algebraic_semidom = semidom_divide_int} :
+  inta algebraic_semidom;
+
+val semiring_modulo_int =
+  {comm_semiring_1_cancel_semiring_modulo = comm_semiring_1_cancel_int,
+    modulo_semiring_modulo = modulo_int}
+  : inta semiring_modulo;
+
 val semidom_modulo_int =
   {algebraic_semidom_semidom_modulo = algebraic_semidom_int,
     semiring_modulo_semidom_modulo = semiring_modulo_int}
@@ -1153,15 +1155,15 @@
 fun abs_int i = (if less_int i zero_inta then uminus_int i else i);
 
 fun dvd (A1_, A2_) a b =
-  eq A2_
-    (modulo ((modulo_semiring_modulo o semiring_modulo_semidom_modulo) A1_) b a)
+  eq A1_
+    (modulo ((modulo_semiring_modulo o semiring_modulo_semidom_modulo) A2_) b a)
     (zero ((zero_mult_zero o mult_zero_semiring_0 o semiring_0_semiring_1 o
              semiring_1_comm_semiring_1 o
              comm_semiring_1_comm_semiring_1_cancel o
              comm_semiring_1_cancel_semidom o semidom_semidom_divide o
              semidom_divide_algebraic_semidom o
              algebraic_semidom_semidom_modulo)
-            A1_));
+            A2_));
 
 fun nummul i (C j) = C (times_inta i j)
   | nummul i (CN (n, c, t)) = CN (n, times_inta c i, nummul i t)
@@ -1175,78 +1177,78 @@
 
 fun less_eq_nat m n = integer_of_nat m <= integer_of_nat n;
 
-fun numadd (CN (n1, c1, r1), CN (n2, c2, r2)) =
+fun numadd (CN (n1, c1, r1)) (CN (n2, c2, r2)) =
   (if equal_nat n1 n2
     then let
            val c = plus_inta c1 c2;
          in
-           (if equal_inta c zero_inta then numadd (r1, r2)
-             else CN (n1, c, numadd (r1, r2)))
+           (if equal_inta c zero_inta then numadd r1 r2
+             else CN (n1, c, numadd r1 r2))
          end
     else (if less_eq_nat n1 n2
-           then CN (n1, c1, numadd (r1, Add (Mul (c2, Bound n2), r2)))
-           else CN (n2, c2, numadd (Add (Mul (c1, Bound n1), r1), r2))))
-  | numadd (CN (n1, c1, r1), C dd) = CN (n1, c1, numadd (r1, C dd))
-  | numadd (CN (n1, c1, r1), Bound de) = CN (n1, c1, numadd (r1, Bound de))
-  | numadd (CN (n1, c1, r1), Neg di) = CN (n1, c1, numadd (r1, Neg di))
-  | numadd (CN (n1, c1, r1), Add (dj, dk)) =
-    CN (n1, c1, numadd (r1, Add (dj, dk)))
-  | numadd (CN (n1, c1, r1), Sub (dl, dm)) =
-    CN (n1, c1, numadd (r1, Sub (dl, dm)))
-  | numadd (CN (n1, c1, r1), Mul (dn, doa)) =
-    CN (n1, c1, numadd (r1, Mul (dn, doa)))
-  | numadd (C w, CN (n2, c2, r2)) = CN (n2, c2, numadd (C w, r2))
-  | numadd (Bound x, CN (n2, c2, r2)) = CN (n2, c2, numadd (Bound x, r2))
-  | numadd (Neg ac, CN (n2, c2, r2)) = CN (n2, c2, numadd (Neg ac, r2))
-  | numadd (Add (ad, ae), CN (n2, c2, r2)) =
-    CN (n2, c2, numadd (Add (ad, ae), r2))
-  | numadd (Sub (af, ag), CN (n2, c2, r2)) =
-    CN (n2, c2, numadd (Sub (af, ag), r2))
-  | numadd (Mul (ah, ai), CN (n2, c2, r2)) =
-    CN (n2, c2, numadd (Mul (ah, ai), r2))
-  | numadd (C b1, C b2) = C (plus_inta b1 b2)
-  | numadd (C aj, Bound bi) = Add (C aj, Bound bi)
-  | numadd (C aj, Neg bm) = Add (C aj, Neg bm)
-  | numadd (C aj, Add (bn, bo)) = Add (C aj, Add (bn, bo))
-  | numadd (C aj, Sub (bp, bq)) = Add (C aj, Sub (bp, bq))
-  | numadd (C aj, Mul (br, bs)) = Add (C aj, Mul (br, bs))
-  | numadd (Bound ak, C cf) = Add (Bound ak, C cf)
-  | numadd (Bound ak, Bound cg) = Add (Bound ak, Bound cg)
-  | numadd (Bound ak, Neg ck) = Add (Bound ak, Neg ck)
-  | numadd (Bound ak, Add (cl, cm)) = Add (Bound ak, Add (cl, cm))
-  | numadd (Bound ak, Sub (cn, co)) = Add (Bound ak, Sub (cn, co))
-  | numadd (Bound ak, Mul (cp, cq)) = Add (Bound ak, Mul (cp, cq))
-  | numadd (Neg ao, C en) = Add (Neg ao, C en)
-  | numadd (Neg ao, Bound eo) = Add (Neg ao, Bound eo)
-  | numadd (Neg ao, Neg et) = Add (Neg ao, Neg et)
-  | numadd (Neg ao, Add (eu, ev)) = Add (Neg ao, Add (eu, ev))
-  | numadd (Neg ao, Sub (ew, ex)) = Add (Neg ao, Sub (ew, ex))
-  | numadd (Neg ao, Mul (ey, ez)) = Add (Neg ao, Mul (ey, ez))
-  | numadd (Add (ap, aq), C fm) = Add (Add (ap, aq), C fm)
-  | numadd (Add (ap, aq), Bound fna) = Add (Add (ap, aq), Bound fna)
-  | numadd (Add (ap, aq), Neg fr) = Add (Add (ap, aq), Neg fr)
-  | numadd (Add (ap, aq), Add (fs, ft)) = Add (Add (ap, aq), Add (fs, ft))
-  | numadd (Add (ap, aq), Sub (fu, fv)) = Add (Add (ap, aq), Sub (fu, fv))
-  | numadd (Add (ap, aq), Mul (fw, fx)) = Add (Add (ap, aq), Mul (fw, fx))
-  | numadd (Sub (ar, asa), C gk) = Add (Sub (ar, asa), C gk)
-  | numadd (Sub (ar, asa), Bound gl) = Add (Sub (ar, asa), Bound gl)
-  | numadd (Sub (ar, asa), Neg gp) = Add (Sub (ar, asa), Neg gp)
-  | numadd (Sub (ar, asa), Add (gq, gr)) = Add (Sub (ar, asa), Add (gq, gr))
-  | numadd (Sub (ar, asa), Sub (gs, gt)) = Add (Sub (ar, asa), Sub (gs, gt))
-  | numadd (Sub (ar, asa), Mul (gu, gv)) = Add (Sub (ar, asa), Mul (gu, gv))
-  | numadd (Mul (at, au), C hi) = Add (Mul (at, au), C hi)
-  | numadd (Mul (at, au), Bound hj) = Add (Mul (at, au), Bound hj)
-  | numadd (Mul (at, au), Neg hn) = Add (Mul (at, au), Neg hn)
-  | numadd (Mul (at, au), Add (ho, hp)) = Add (Mul (at, au), Add (ho, hp))
-  | numadd (Mul (at, au), Sub (hq, hr)) = Add (Mul (at, au), Sub (hq, hr))
-  | numadd (Mul (at, au), Mul (hs, ht)) = Add (Mul (at, au), Mul (hs, ht));
+           then CN (n1, c1, numadd r1 (Add (Mul (c2, Bound n2), r2)))
+           else CN (n2, c2, numadd (Add (Mul (c1, Bound n1), r1)) r2)))
+  | numadd (CN (n1, c1, r1)) (C v) = CN (n1, c1, numadd r1 (C v))
+  | numadd (CN (n1, c1, r1)) (Bound v) = CN (n1, c1, numadd r1 (Bound v))
+  | numadd (CN (n1, c1, r1)) (Neg v) = CN (n1, c1, numadd r1 (Neg v))
+  | numadd (CN (n1, c1, r1)) (Add (v, va)) =
+    CN (n1, c1, numadd r1 (Add (v, va)))
+  | numadd (CN (n1, c1, r1)) (Sub (v, va)) =
+    CN (n1, c1, numadd r1 (Sub (v, va)))
+  | numadd (CN (n1, c1, r1)) (Mul (v, va)) =
+    CN (n1, c1, numadd r1 (Mul (v, va)))
+  | numadd (C v) (CN (n2, c2, r2)) = CN (n2, c2, numadd (C v) r2)
+  | numadd (Bound v) (CN (n2, c2, r2)) = CN (n2, c2, numadd (Bound v) r2)
+  | numadd (Neg v) (CN (n2, c2, r2)) = CN (n2, c2, numadd (Neg v) r2)
+  | numadd (Add (v, va)) (CN (n2, c2, r2)) =
+    CN (n2, c2, numadd (Add (v, va)) r2)
+  | numadd (Sub (v, va)) (CN (n2, c2, r2)) =
+    CN (n2, c2, numadd (Sub (v, va)) r2)
+  | numadd (Mul (v, va)) (CN (n2, c2, r2)) =
+    CN (n2, c2, numadd (Mul (v, va)) r2)
+  | numadd (C b1) (C b2) = C (plus_inta b1 b2)
+  | numadd (C v) (Bound va) = Add (C v, Bound va)
+  | numadd (C v) (Neg va) = Add (C v, Neg va)
+  | numadd (C v) (Add (va, vb)) = Add (C v, Add (va, vb))
+  | numadd (C v) (Sub (va, vb)) = Add (C v, Sub (va, vb))
+  | numadd (C v) (Mul (va, vb)) = Add (C v, Mul (va, vb))
+  | numadd (Bound v) (C va) = Add (Bound v, C va)
+  | numadd (Bound v) (Bound va) = Add (Bound v, Bound va)
+  | numadd (Bound v) (Neg va) = Add (Bound v, Neg va)
+  | numadd (Bound v) (Add (va, vb)) = Add (Bound v, Add (va, vb))
+  | numadd (Bound v) (Sub (va, vb)) = Add (Bound v, Sub (va, vb))
+  | numadd (Bound v) (Mul (va, vb)) = Add (Bound v, Mul (va, vb))
+  | numadd (Neg v) (C va) = Add (Neg v, C va)
+  | numadd (Neg v) (Bound va) = Add (Neg v, Bound va)
+  | numadd (Neg v) (Neg va) = Add (Neg v, Neg va)
+  | numadd (Neg v) (Add (va, vb)) = Add (Neg v, Add (va, vb))
+  | numadd (Neg v) (Sub (va, vb)) = Add (Neg v, Sub (va, vb))
+  | numadd (Neg v) (Mul (va, vb)) = Add (Neg v, Mul (va, vb))
+  | numadd (Add (v, va)) (C vb) = Add (Add (v, va), C vb)
+  | numadd (Add (v, va)) (Bound vb) = Add (Add (v, va), Bound vb)
+  | numadd (Add (v, va)) (Neg vb) = Add (Add (v, va), Neg vb)
+  | numadd (Add (v, va)) (Add (vb, vc)) = Add (Add (v, va), Add (vb, vc))
+  | numadd (Add (v, va)) (Sub (vb, vc)) = Add (Add (v, va), Sub (vb, vc))
+  | numadd (Add (v, va)) (Mul (vb, vc)) = Add (Add (v, va), Mul (vb, vc))
+  | numadd (Sub (v, va)) (C vb) = Add (Sub (v, va), C vb)
+  | numadd (Sub (v, va)) (Bound vb) = Add (Sub (v, va), Bound vb)
+  | numadd (Sub (v, va)) (Neg vb) = Add (Sub (v, va), Neg vb)
+  | numadd (Sub (v, va)) (Add (vb, vc)) = Add (Sub (v, va), Add (vb, vc))
+  | numadd (Sub (v, va)) (Sub (vb, vc)) = Add (Sub (v, va), Sub (vb, vc))
+  | numadd (Sub (v, va)) (Mul (vb, vc)) = Add (Sub (v, va), Mul (vb, vc))
+  | numadd (Mul (v, va)) (C vb) = Add (Mul (v, va), C vb)
+  | numadd (Mul (v, va)) (Bound vb) = Add (Mul (v, va), Bound vb)
+  | numadd (Mul (v, va)) (Neg vb) = Add (Mul (v, va), Neg vb)
+  | numadd (Mul (v, va)) (Add (vb, vc)) = Add (Mul (v, va), Add (vb, vc))
+  | numadd (Mul (v, va)) (Sub (vb, vc)) = Add (Mul (v, va), Sub (vb, vc))
+  | numadd (Mul (v, va)) (Mul (vb, vc)) = Add (Mul (v, va), Mul (vb, vc));
 
-fun numsub s t = (if equal_numa s t then C zero_inta else numadd (s, numneg t));
+fun numsub s t = (if equal_numa s t then C zero_inta else numadd s (numneg t));
 
 fun simpnum (C j) = C j
   | simpnum (Bound n) = CN (n, one_inta, C zero_inta)
   | simpnum (Neg t) = numneg (simpnum t)
-  | simpnum (Add (t, s)) = numadd (simpnum t, simpnum s)
+  | simpnum (Add (t, s)) = numadd (simpnum t) (simpnum s)
   | simpnum (Sub (t, s)) = numsub (simpnum t) (simpnum s)
   | simpnum (Mul (i, t)) =
     (if equal_inta i zero_inta then C zero_inta else nummul i (simpnum t))
@@ -1356,7 +1358,7 @@
                   in
                     (case aa
                       of C v =>
-                        (if dvd (semidom_modulo_int, equal_int) i v then T
+                        (if dvd (equal_int, semidom_modulo_int) i v then T
                           else F)
                       | Bound _ => Dvd (i, aa) | CN (_, _, _) => Dvd (i, aa)
                       | Neg _ => Dvd (i, aa) | Add (_, _) => Dvd (i, aa)
@@ -1370,7 +1372,7 @@
                   in
                     (case aa
                       of C v =>
-                        (if not (dvd (semidom_modulo_int, equal_int) i v) then T
+                        (if not (dvd (equal_int, semidom_modulo_int) i v) then T
                           else F)
                       | Bound _ => NDvd (i, aa) | CN (_, _, _) => NDvd (i, aa)
                       | Neg _ => NDvd (i, aa) | Add (_, _) => NDvd (i, aa)