merged

--- a/Admin/isatest/isatest-settings	Mon Feb 16 13:42:15 2009 -0800
+++ b/Admin/isatest/isatest-settings	Mon Feb 16 13:42:45 2009 -0800
@@ -11,7 +11,7 @@
 HOME=/home/isatest
 
 ## send email on failure to
-MAILTO="[e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail]"
+MAILTO="[e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail]"
 
 LOGPREFIX=$HOME/log
 MASTERLOG=$LOGPREFIX/isatest.log

--- a/src/HOL/Extraction.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Extraction.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -16,28 +16,19 @@
 let
 fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
       (Const ("op :", _) $ x $ S)) = (case strip_comb S of
-        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @
-           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
-      | (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @
-           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x]))
+        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, U), ts @ [x]))
+      | (Free (s, U), ts) => SOME (list_comb (Free (s, U), ts @ [x]))
       | _ => NONE)
   | realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
       (Const ("op :", _) $ x $ S)) = (case strip_comb S of
-        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T :: binder_types U @
-           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
-      | (Free (s, U), ts) => SOME (list_comb (Free (s, T :: binder_types U @
-           [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), r :: ts @ [x]))
+        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts @ [x]))
+      | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts @ [x]))
       | _ => NONE)
   | realizes_set_proc _ = NONE;
 
-fun mk_realizes_set r rT s (setT as Type ("set", [elT])) =
-  Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $
-    incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
-      Bound 0 $ incr_boundvars 1 s));
 in
   Extraction.add_types
-      [("bool", ([], NONE)),
-       ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
+      [("bool", ([], NONE))] #>
   Extraction.set_preprocessor (fn thy =>
       Proofterm.rewrite_proof_notypes
         ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o

--- a/src/HOL/IntDiv.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/IntDiv.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -377,6 +377,11 @@
 apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
 done
 
+lemma zmod_zminus1_not_zero:
+  fixes k l :: int
+  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  unfolding zmod_zminus1_eq_if by auto
+
 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
 by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
 
@@ -393,6 +398,11 @@
      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
 by (simp add: zmod_zminus1_eq_if zmod_zminus2)
 
+lemma zmod_zminus2_not_zero:
+  fixes k l :: int
+  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  unfolding zmod_zminus2_eq_if by auto 
+
 
 subsection{*Division of a Number by Itself*}
 
@@ -1523,6 +1533,40 @@
   thus  ?lhs by simp
 qed
 
+
+subsection {* Code generation *}
+
+definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
+  "pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
+
+lemma pdivmod_posDivAlg [code]:
+  "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
+by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
+
+lemma divmod_pdivmod: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+  apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
+    then pdivmod k l
+    else (let (r, s) = pdivmod k l in
+      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+proof -
+  have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
+  show ?thesis
+    by (simp add: divmod_mod_div pdivmod_def)
+      (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
+      zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
+qed
+
+lemma divmod_code [code]: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+  apsnd ((op *) (sgn l)) (if sgn k = sgn l
+    then pdivmod k l
+    else (let (r, s) = pdivmod k l in
+      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+proof -
+  have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l"
+    by (auto simp add: not_less sgn_if)
+  then show ?thesis by (simp add: divmod_pdivmod)
+qed
+
 code_modulename SML
   IntDiv Integer
 

--- a/src/HOL/Library/Binomial.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Library/Binomial.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Binomial.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Amine Chaieb
     Copyright   1997  University of Cambridge
 *)
@@ -13,11 +12,9 @@
 text {* This development is based on the work of Andy Gordon and
   Florian Kammueller. *}
 
-consts
-  binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"      (infixl "choose" 65)
-primrec
+primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) where
   binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)"
-  binomial_Suc: "(Suc n choose k) =
+  | binomial_Suc: "(Suc n choose k) =
                  (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 lemma binomial_n_0 [simp]: "(n choose 0) = 1"

--- a/src/HOL/Library/Code_Integer.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Library/Code_Integer.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Code_Integer.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
@@ -72,6 +71,11 @@
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
+code_const pdivmod
+  (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
+  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
+  (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
+
 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")

--- a/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -105,12 +105,18 @@
   This can be accomplished by applying the following transformation rules:
 *}
 
-lemma Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
+lemma Suc_if_eq': "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
   f n = (if n = 0 then g else h (n - 1))"
-  by (case_tac n) simp_all
+  by (cases n) simp_all
+
+lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
+  f n \<equiv> if n = 0 then g else h (n - 1)"
+  by (rule eq_reflection, rule Suc_if_eq')
+    (rule meta_eq_to_obj_eq, assumption,
+     rule meta_eq_to_obj_eq, assumption)
 
 lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
-  by (case_tac n) simp_all
+  by (cases n) simp_all
 
 text {*
   The rules above are built into a preprocessor that is plugged into
@@ -123,16 +129,16 @@
 setup {*
 let
 
-fun remove_suc thy thms =
+fun gen_remove_suc Suc_if_eq dest_judgement thy thms =
   let
     val vname = Name.variant (map fst
-      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
+      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
     val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
     fun lhs_of th = snd (Thm.dest_comb
-      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
-    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
+      (fst (Thm.dest_comb (dest_judgement (cprop_of th)))));
+    fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th)));
     fun find_vars ct = (case term_of ct of
-        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
+        (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
       | _ $ _ =>
         let val (ct1, ct2) = Thm.dest_comb ct
         in 
@@ -150,7 +156,7 @@
              (Drule.instantiate'
                [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
                  SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
-               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
+               Suc_if_eq)) (Thm.forall_intr cv' th)
       in
         case map_filter (fn th'' =>
             SOME (th'', singleton
@@ -161,20 +167,26 @@
               let val (ths1, ths2) = split_list thps
               in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
       end
-  in case get_first mk_thms eqs of
-      NONE => thms
-    | SOME x => remove_suc thy x
+  in get_first mk_thms eqs end;
+
+fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms =
+  let
+    val dest = dest_lhs o prop_of;
+    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
+  in
+    if forall (can dest) thms andalso exists (contains_suc o dest) thms
+      then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms
+       else NONE
   end;
 
-fun eqn_suc_preproc thy ths =
-  let
-    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
-    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
-  in
-    if forall (can dest) ths andalso
-      exists (contains_suc o dest) ths
-    then remove_suc thy ths else ths
-  end;
+fun eqn_suc_preproc thy = map fst
+  #> gen_eqn_suc_preproc
+      @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
+  #> (Option.map o map) (Code_Unit.mk_eqn thy);
+
+fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
+  @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
+  |> the_default thms;
 
 fun remove_suc_clause thy thms =
   let
@@ -215,28 +227,11 @@
         (map_filter (try dest) (concl_of th :: prems_of th))) ths
     then remove_suc_clause thy ths else ths
   end;
-
-fun lift f thy eqns1 =
-  let
-    val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
-    val thms3 = try (map fst
-      #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
-      #> f thy
-      #> map (fn thm => thm RS @{thm eq_reflection})
-      #> map (Conv.fconv_rule Drule.beta_eta_conversion)) eqns2;
-    val thms4 = Option.map Drule.zero_var_indexes_list thms3;
-  in case thms4
-   of NONE => NONE
-    | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
-        then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
-  end
-
 in
 
-  Codegen.add_preprocessor eqn_suc_preproc
+  Codegen.add_preprocessor eqn_suc_preproc'
   #> Codegen.add_preprocessor clause_suc_preproc
-  #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
-  #> Code.add_functrans ("clause_Suc", lift clause_suc_preproc)
+  #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
 
 end;
 *}

--- a/src/HOL/List.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/List.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -257,7 +257,7 @@
 \caption{Characteristic examples}
 \label{fig:Characteristic}
 \end{figure}
-Figure~\ref{fig:Characteristic} shows charachteristic examples
+Figure~\ref{fig:Characteristic} shows characteristic examples
 that should give an intuitive understanding of the above functions.
 *}
 

--- a/src/HOL/Rational.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Rational.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -886,14 +886,13 @@
   finally show ?thesis using assms by simp
 qed
 
-lemma rat_less_eq_code [code]:
-  "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
-       then sgn c * sgn d \<ge> 0
-     else if d = 0
-       then sgn a * sgn b \<le> 0
-     else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
-by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
-  (auto simp add: sgn_times sgn_0_0 le_less sgn_1_pos [symmetric] sgn_1_neg [symmetric])
+lemma (in ordered_idom) sgn_greater [simp]:
+  "0 < sgn a \<longleftrightarrow> 0 < a"
+  unfolding sgn_if by auto
+
+lemma (in ordered_idom) sgn_less [simp]:
+  "sgn a < 0 \<longleftrightarrow> a < 0"
+  unfolding sgn_if by auto
 
 lemma rat_le_eq_code [code]:
   "Fract a b < Fract c d \<longleftrightarrow> (if b = 0
@@ -901,9 +900,17 @@
      else if d = 0
        then sgn a * sgn b < 0
      else a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d)"
-by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
-   (auto simp add: sgn_times sgn_0_0 sgn_1_pos [symmetric] sgn_1_neg [symmetric],
-     auto simp add: sgn_1_pos)
+  by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
+
+lemma rat_less_eq_code [code]:
+  "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
+       then sgn c * sgn d \<ge> 0
+     else if d = 0
+       then sgn a * sgn b \<le> 0
+     else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
+  by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
+    (auto simp add: le_less not_less sgn_0_0)
+
 
 lemma rat_plus_code [code]:
   "Fract a b + Fract c d = (if b = 0

--- a/src/HOL/Ring_and_Field.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:   HOL/Ring_and_Field.thy
-    ID:      $Id$
     Author:  Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
              with contributions by Jeremy Avigad
 *)
@@ -1078,6 +1077,14 @@
   "sgn a = - 1 \<longleftrightarrow> a < 0"
 unfolding sgn_if by (auto simp add: equal_neg_zero)
 
+lemma sgn_pos [simp]:
+  "0 < a \<Longrightarrow> sgn a = 1"
+unfolding sgn_1_pos .
+
+lemma sgn_neg [simp]:
+  "a < 0 \<Longrightarrow> sgn a = - 1"
+unfolding sgn_1_neg .
+
 lemma sgn_times:
   "sgn (a * b) = sgn a * sgn b"
 by (auto simp add: sgn_if zero_less_mult_iff)
@@ -1085,6 +1092,14 @@
 lemma abs_sgn: "abs k = k * sgn k"
 unfolding sgn_if abs_if by auto
 
+lemma sgn_greater [simp]:
+  "0 < sgn a \<longleftrightarrow> 0 < a"
+  unfolding sgn_if by auto
+
+lemma sgn_less [simp]:
+  "sgn a < 0 \<longleftrightarrow> a < 0"
+  unfolding sgn_if by auto
+
 (* The int instances are proved, these generic ones are tedious to prove here.
 And not very useful, as int seems to be the only instance.
 If needed, they should be proved later, when metis is available.

--- a/src/HOL/Tools/Qelim/generated_cooper.ML	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Tools/Qelim/generated_cooper.ML	Mon Feb 16 13:42:45 2009 -0800
@@ -15,13 +15,13 @@
 
 fun divmod n m = (if eqop eq_nat m 0 then (0, n) else IntInf.divMod (n, m));
 
-fun snd (a, y) = y;
+fun snd (a, b) = b;
 
 fun mod_nat m n = snd (divmod m n);
 
 fun gcd m n = (if eqop eq_nat n 0 then m else gcd n (mod_nat m n));
 
-fun fst (y, b) = y;
+fun fst (a, b) = a;
 
 fun div_nat m n = fst (divmod m n);
 
@@ -48,7 +48,7 @@
 fun map f [] = []
   | map f (x :: xs) = f x :: map f xs;
 
-fun append [] y = y
+fun append [] ys = ys
   | append (x :: xs) ys = x :: append xs ys;
 
 fun disjuncts (Or (p, q)) = append (disjuncts p) (disjuncts q)
@@ -105,53 +105,53 @@
     (Le num) = f4 num
   | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19
     (Lt num) = f3 num
-  | fm_case f1 y f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
-    = y
-  | fm_case y f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
-    = y;
+  | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
+    = f2
+  | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
+    = f1;
 
-fun eq_num (Mul (cb, dc)) (Sub (ae, be)) = false
-  | eq_num (Mul (cb, dc)) (Add (ae, be)) = false
-  | eq_num (Sub (cc, dc)) (Add (ae, be)) = false
-  | eq_num (Mul (bd, cc)) (Neg ae) = false
-  | eq_num (Sub (be, cc)) (Neg ae) = false
-  | eq_num (Add (be, cc)) (Neg ae) = false
-  | eq_num (Mul (db, ea)) (Cn (ac, bd, cc)) = false
-  | eq_num (Sub (dc, ea)) (Cn (ac, bd, cc)) = false
-  | eq_num (Add (dc, ea)) (Cn (ac, bd, cc)) = false
-  | eq_num (Neg dc) (Cn (ac, bd, cc)) = false
-  | eq_num (Mul (bd, cc)) (Bound ac) = false
-  | eq_num (Sub (be, cc)) (Bound ac) = false
-  | eq_num (Add (be, cc)) (Bound ac) = false
-  | eq_num (Neg be) (Bound ac) = false
-  | eq_num (Cn (bc, cb, dc)) (Bound ac) = false
-  | eq_num (Mul (bd, cc)) (C ad) = false
-  | eq_num (Sub (be, cc)) (C ad) = false
-  | eq_num (Add (be, cc)) (C ad) = false
-  | eq_num (Neg be) (C ad) = false
-  | eq_num (Cn (bc, cb, dc)) (C ad) = false
-  | eq_num (Bound bc) (C ad) = false
-  | eq_num (Sub (ab, bb)) (Mul (c, da)) = false
-  | eq_num (Add (ab, bb)) (Mul (c, da)) = false
-  | eq_num (Add (ab, bb)) (Sub (ca, da)) = false
-  | eq_num (Neg ab) (Mul (ba, ca)) = false
-  | eq_num (Neg ab) (Sub (bb, ca)) = false
-  | eq_num (Neg ab) (Add (bb, ca)) = false
-  | eq_num (Cn (a, ba, ca)) (Mul (d, e)) = false
-  | eq_num (Cn (a, ba, ca)) (Sub (da, e)) = false
-  | eq_num (Cn (a, ba, ca)) (Add (da, e)) = false
-  | eq_num (Cn (a, ba, ca)) (Neg da) = false
-  | eq_num (Bound a) (Mul (ba, ca)) = false
-  | eq_num (Bound a) (Sub (bb, ca)) = false
-  | eq_num (Bound a) (Add (bb, ca)) = false
-  | eq_num (Bound a) (Neg bb) = false
-  | eq_num (Bound a) (Cn (b, c, da)) = false
-  | eq_num (C aa) (Mul (ba, ca)) = false
-  | eq_num (C aa) (Sub (bb, ca)) = false
-  | eq_num (C aa) (Add (bb, ca)) = false
-  | eq_num (C aa) (Neg bb) = false
-  | eq_num (C aa) (Cn (b, c, da)) = false
-  | eq_num (C aa) (Bound b) = false
+fun eq_num (Mul (c, d)) (Sub (a, b)) = false
+  | eq_num (Mul (c, d)) (Add (a, b)) = false
+  | eq_num (Sub (c, d)) (Add (a, b)) = false
+  | eq_num (Mul (b, c)) (Neg a) = false
+  | eq_num (Sub (b, c)) (Neg a) = false
+  | eq_num (Add (b, c)) (Neg a) = false
+  | eq_num (Mul (d, e)) (Cn (a, b, c)) = false
+  | eq_num (Sub (d, e)) (Cn (a, b, c)) = false
+  | eq_num (Add (d, e)) (Cn (a, b, c)) = false
+  | eq_num (Neg d) (Cn (a, b, c)) = false
+  | eq_num (Mul (b, c)) (Bound a) = false
+  | eq_num (Sub (b, c)) (Bound a) = false
+  | eq_num (Add (b, c)) (Bound a) = false
+  | eq_num (Neg b) (Bound a) = false
+  | eq_num (Cn (b, c, d)) (Bound a) = false
+  | eq_num (Mul (b, c)) (C a) = false
+  | eq_num (Sub (b, c)) (C a) = false
+  | eq_num (Add (b, c)) (C a) = false
+  | eq_num (Neg b) (C a) = false
+  | eq_num (Cn (b, c, d)) (C a) = false
+  | eq_num (Bound b) (C a) = false
+  | eq_num (Sub (a, b)) (Mul (c, d)) = false
+  | eq_num (Add (a, b)) (Mul (c, d)) = false
+  | eq_num (Add (a, b)) (Sub (c, d)) = false
+  | eq_num (Neg a) (Mul (b, c)) = false
+  | eq_num (Neg a) (Sub (b, c)) = false
+  | eq_num (Neg a) (Add (b, c)) = false
+  | eq_num (Cn (a, b, c)) (Mul (d, e)) = false
+  | eq_num (Cn (a, b, c)) (Sub (d, e)) = false
+  | eq_num (Cn (a, b, c)) (Add (d, e)) = false
+  | eq_num (Cn (a, b, c)) (Neg d) = false
+  | eq_num (Bound a) (Mul (b, c)) = false
+  | eq_num (Bound a) (Sub (b, c)) = false
+  | eq_num (Bound a) (Add (b, c)) = false
+  | eq_num (Bound a) (Neg b) = false
+  | eq_num (Bound a) (Cn (b, c, d)) = false
+  | eq_num (C a) (Mul (b, c)) = false
+  | eq_num (C a) (Sub (b, c)) = false
+  | eq_num (C a) (Add (b, c)) = false
+  | eq_num (C a) (Neg b) = false
+  | eq_num (C a) (Cn (b, c, d)) = false
+  | eq_num (C a) (Bound b) = false
   | eq_num (Mul (inta, num)) (Mul (int', num')) =
     ((inta : IntInf.int) = int') andalso eq_num num num'
   | eq_num (Sub (num1, num2)) (Sub (num1', num2')) =
@@ -165,347 +165,347 @@
   | eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat')
   | eq_num (C inta) (C int') = ((inta : IntInf.int) = int');
 
-fun eq_fm (NClosed bd) (Closed ad) = false
-  | eq_fm (NClosed bd) (A af) = false
-  | eq_fm (Closed bd) (A af) = false
-  | eq_fm (NClosed bd) (E af) = false
-  | eq_fm (Closed bd) (E af) = false
-  | eq_fm (A bf) (E af) = false
-  | eq_fm (NClosed cd) (Iff (af, bf)) = false
-  | eq_fm (Closed cd) (Iff (af, bf)) = false
-  | eq_fm (A cf) (Iff (af, bf)) = false
-  | eq_fm (E cf) (Iff (af, bf)) = false
-  | eq_fm (NClosed cd) (Imp (af, bf)) = false
-  | eq_fm (Closed cd) (Imp (af, bf)) = false
-  | eq_fm (A cf) (Imp (af, bf)) = false
-  | eq_fm (E cf) (Imp (af, bf)) = false
-  | eq_fm (Iff (cf, db)) (Imp (af, bf)) = false
-  | eq_fm (NClosed cd) (Or (af, bf)) = false
-  | eq_fm (Closed cd) (Or (af, bf)) = false
-  | eq_fm (A cf) (Or (af, bf)) = false
-  | eq_fm (E cf) (Or (af, bf)) = false
-  | eq_fm (Iff (cf, db)) (Or (af, bf)) = false
-  | eq_fm (Imp (cf, db)) (Or (af, bf)) = false
-  | eq_fm (NClosed cd) (And (af, bf)) = false
-  | eq_fm (Closed cd) (And (af, bf)) = false
-  | eq_fm (A cf) (And (af, bf)) = false
-  | eq_fm (E cf) (And (af, bf)) = false
-  | eq_fm (Iff (cf, db)) (And (af, bf)) = false
-  | eq_fm (Imp (cf, db)) (And (af, bf)) = false
-  | eq_fm (Or (cf, db)) (And (af, bf)) = false
-  | eq_fm (NClosed bd) (Not af) = false
-  | eq_fm (Closed bd) (Not af) = false
-  | eq_fm (A bf) (Not af) = false
-  | eq_fm (E bf) (Not af) = false
-  | eq_fm (Iff (bf, cf)) (Not af) = false
-  | eq_fm (Imp (bf, cf)) (Not af) = false
-  | eq_fm (Or (bf, cf)) (Not af) = false
-  | eq_fm (And (bf, cf)) (Not af) = false
-  | eq_fm (NClosed cd) (NDvd (ae, bg)) = false
-  | eq_fm (Closed cd) (NDvd (ae, bg)) = false
-  | eq_fm (A cf) (NDvd (ae, bg)) = false
-  | eq_fm (E cf) (NDvd (ae, bg)) = false
-  | eq_fm (Iff (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (Imp (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (Or (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (And (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (Not cf) (NDvd (ae, bg)) = false
-  | eq_fm (NClosed cd) (Dvd (ae, bg)) = false
-  | eq_fm (Closed cd) (Dvd (ae, bg)) = false
-  | eq_fm (A cf) (Dvd (ae, bg)) = false
-  | eq_fm (E cf) (Dvd (ae, bg)) = false
-  | eq_fm (Iff (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (Imp (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (Or (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (And (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (Not cf) (Dvd (ae, bg)) = false
-  | eq_fm (NDvd (ce, dc)) (Dvd (ae, bg)) = false
-  | eq_fm (NClosed bd) (NEq ag) = false
-  | eq_fm (Closed bd) (NEq ag) = false
-  | eq_fm (A bf) (NEq ag) = false
-  | eq_fm (E bf) (NEq ag) = false
-  | eq_fm (Iff (bf, cf)) (NEq ag) = false
-  | eq_fm (Imp (bf, cf)) (NEq ag) = false
-  | eq_fm (Or (bf, cf)) (NEq ag) = false
-  | eq_fm (And (bf, cf)) (NEq ag) = false
-  | eq_fm (Not bf) (NEq ag) = false
-  | eq_fm (NDvd (be, cg)) (NEq ag) = false
-  | eq_fm (Dvd (be, cg)) (NEq ag) = false
-  | eq_fm (NClosed bd) (Eq ag) = false
-  | eq_fm (Closed bd) (Eq ag) = false
-  | eq_fm (A bf) (Eq ag) = false
-  | eq_fm (E bf) (Eq ag) = false
-  | eq_fm (Iff (bf, cf)) (Eq ag) = false
-  | eq_fm (Imp (bf, cf)) (Eq ag) = false
-  | eq_fm (Or (bf, cf)) (Eq ag) = false
-  | eq_fm (And (bf, cf)) (Eq ag) = false
-  | eq_fm (Not bf) (Eq ag) = false
-  | eq_fm (NDvd (be, cg)) (Eq ag) = false
-  | eq_fm (Dvd (be, cg)) (Eq ag) = false
-  | eq_fm (NEq bg) (Eq ag) = false
-  | eq_fm (NClosed bd) (Ge ag) = false
-  | eq_fm (Closed bd) (Ge ag) = false
-  | eq_fm (A bf) (Ge ag) = false
-  | eq_fm (E bf) (Ge ag) = false
-  | eq_fm (Iff (bf, cf)) (Ge ag) = false
-  | eq_fm (Imp (bf, cf)) (Ge ag) = false
-  | eq_fm (Or (bf, cf)) (Ge ag) = false
-  | eq_fm (And (bf, cf)) (Ge ag) = false
-  | eq_fm (Not bf) (Ge ag) = false
-  | eq_fm (NDvd (be, cg)) (Ge ag) = false
-  | eq_fm (Dvd (be, cg)) (Ge ag) = false
-  | eq_fm (NEq bg) (Ge ag) = false
-  | eq_fm (Eq bg) (Ge ag) = false
-  | eq_fm (NClosed bd) (Gt ag) = false
-  | eq_fm (Closed bd) (Gt ag) = false
-  | eq_fm (A bf) (Gt ag) = false
-  | eq_fm (E bf) (Gt ag) = false
-  | eq_fm (Iff (bf, cf)) (Gt ag) = false
-  | eq_fm (Imp (bf, cf)) (Gt ag) = false
-  | eq_fm (Or (bf, cf)) (Gt ag) = false
-  | eq_fm (And (bf, cf)) (Gt ag) = false
-  | eq_fm (Not bf) (Gt ag) = false
-  | eq_fm (NDvd (be, cg)) (Gt ag) = false
-  | eq_fm (Dvd (be, cg)) (Gt ag) = false
-  | eq_fm (NEq bg) (Gt ag) = false
-  | eq_fm (Eq bg) (Gt ag) = false
-  | eq_fm (Ge bg) (Gt ag) = false
-  | eq_fm (NClosed bd) (Le ag) = false
-  | eq_fm (Closed bd) (Le ag) = false
-  | eq_fm (A bf) (Le ag) = false
-  | eq_fm (E bf) (Le ag) = false
-  | eq_fm (Iff (bf, cf)) (Le ag) = false
-  | eq_fm (Imp (bf, cf)) (Le ag) = false
-  | eq_fm (Or (bf, cf)) (Le ag) = false
-  | eq_fm (And (bf, cf)) (Le ag) = false
-  | eq_fm (Not bf) (Le ag) = false
-  | eq_fm (NDvd (be, cg)) (Le ag) = false
-  | eq_fm (Dvd (be, cg)) (Le ag) = false
-  | eq_fm (NEq bg) (Le ag) = false
-  | eq_fm (Eq bg) (Le ag) = false
-  | eq_fm (Ge bg) (Le ag) = false
-  | eq_fm (Gt bg) (Le ag) = false
-  | eq_fm (NClosed bd) (Lt ag) = false
-  | eq_fm (Closed bd) (Lt ag) = false
-  | eq_fm (A bf) (Lt ag) = false
-  | eq_fm (E bf) (Lt ag) = false
-  | eq_fm (Iff (bf, cf)) (Lt ag) = false
-  | eq_fm (Imp (bf, cf)) (Lt ag) = false
-  | eq_fm (Or (bf, cf)) (Lt ag) = false
-  | eq_fm (And (bf, cf)) (Lt ag) = false
-  | eq_fm (Not bf) (Lt ag) = false
-  | eq_fm (NDvd (be, cg)) (Lt ag) = false
-  | eq_fm (Dvd (be, cg)) (Lt ag) = false
-  | eq_fm (NEq bg) (Lt ag) = false
-  | eq_fm (Eq bg) (Lt ag) = false
-  | eq_fm (Ge bg) (Lt ag) = false
-  | eq_fm (Gt bg) (Lt ag) = false
-  | eq_fm (Le bg) (Lt ag) = false
-  | eq_fm (NClosed ad) F = false
-  | eq_fm (Closed ad) F = false
-  | eq_fm (A af) F = false
-  | eq_fm (E af) F = false
-  | eq_fm (Iff (af, bf)) F = false
-  | eq_fm (Imp (af, bf)) F = false
-  | eq_fm (Or (af, bf)) F = false
-  | eq_fm (And (af, bf)) F = false
-  | eq_fm (Not af) F = false
-  | eq_fm (NDvd (ae, bg)) F = false
-  | eq_fm (Dvd (ae, bg)) F = false
-  | eq_fm (NEq ag) F = false
-  | eq_fm (Eq ag) F = false
-  | eq_fm (Ge ag) F = false
-  | eq_fm (Gt ag) F = false
-  | eq_fm (Le ag) F = false
-  | eq_fm (Lt ag) F = false
-  | eq_fm (NClosed ad) T = false
-  | eq_fm (Closed ad) T = false
-  | eq_fm (A af) T = false
-  | eq_fm (E af) T = false
-  | eq_fm (Iff (af, bf)) T = false
-  | eq_fm (Imp (af, bf)) T = false
-  | eq_fm (Or (af, bf)) T = false
-  | eq_fm (And (af, bf)) T = false
-  | eq_fm (Not af) T = false
-  | eq_fm (NDvd (ae, bg)) T = false
-  | eq_fm (Dvd (ae, bg)) T = false
-  | eq_fm (NEq ag) T = false
-  | eq_fm (Eq ag) T = false
-  | eq_fm (Ge ag) T = false
-  | eq_fm (Gt ag) T = false
-  | eq_fm (Le ag) T = false
-  | eq_fm (Lt ag) T = false
+fun eq_fm (NClosed b) (Closed a) = false
+  | eq_fm (NClosed b) (A a) = false
+  | eq_fm (Closed b) (A a) = false
+  | eq_fm (NClosed b) (E a) = false
+  | eq_fm (Closed b) (E a) = false
+  | eq_fm (A b) (E a) = false
+  | eq_fm (NClosed c) (Iff (a, b)) = false
+  | eq_fm (Closed c) (Iff (a, b)) = false
+  | eq_fm (A c) (Iff (a, b)) = false
+  | eq_fm (E c) (Iff (a, b)) = false
+  | eq_fm (NClosed c) (Imp (a, b)) = false
+  | eq_fm (Closed c) (Imp (a, b)) = false
+  | eq_fm (A c) (Imp (a, b)) = false
+  | eq_fm (E c) (Imp (a, b)) = false
+  | eq_fm (Iff (c, d)) (Imp (a, b)) = false
+  | eq_fm (NClosed c) (Or (a, b)) = false
+  | eq_fm (Closed c) (Or (a, b)) = false
+  | eq_fm (A c) (Or (a, b)) = false
+  | eq_fm (E c) (Or (a, b)) = false
+  | eq_fm (Iff (c, d)) (Or (a, b)) = false
+  | eq_fm (Imp (c, d)) (Or (a, b)) = false
+  | eq_fm (NClosed c) (And (a, b)) = false
+  | eq_fm (Closed c) (And (a, b)) = false
+  | eq_fm (A c) (And (a, b)) = false
+  | eq_fm (E c) (And (a, b)) = false
+  | eq_fm (Iff (c, d)) (And (a, b)) = false
+  | eq_fm (Imp (c, d)) (And (a, b)) = false
+  | eq_fm (Or (c, d)) (And (a, b)) = false
+  | eq_fm (NClosed b) (Not a) = false
+  | eq_fm (Closed b) (Not a) = false
+  | eq_fm (A b) (Not a) = false
+  | eq_fm (E b) (Not a) = false
+  | eq_fm (Iff (b, c)) (Not a) = false
+  | eq_fm (Imp (b, c)) (Not a) = false
+  | eq_fm (Or (b, c)) (Not a) = false
+  | eq_fm (And (b, c)) (Not a) = false
+  | eq_fm (NClosed c) (NDvd (a, b)) = false
+  | eq_fm (Closed c) (NDvd (a, b)) = false
+  | eq_fm (A c) (NDvd (a, b)) = false
+  | eq_fm (E c) (NDvd (a, b)) = false
+  | eq_fm (Iff (c, d)) (NDvd (a, b)) = false
+  | eq_fm (Imp (c, d)) (NDvd (a, b)) = false
+  | eq_fm (Or (c, d)) (NDvd (a, b)) = false
+  | eq_fm (And (c, d)) (NDvd (a, b)) = false
+  | eq_fm (Not c) (NDvd (a, b)) = false
+  | eq_fm (NClosed c) (Dvd (a, b)) = false
+  | eq_fm (Closed c) (Dvd (a, b)) = false
+  | eq_fm (A c) (Dvd (a, b)) = false
+  | eq_fm (E c) (Dvd (a, b)) = false
+  | eq_fm (Iff (c, d)) (Dvd (a, b)) = false
+  | eq_fm (Imp (c, d)) (Dvd (a, b)) = false
+  | eq_fm (Or (c, d)) (Dvd (a, b)) = false
+  | eq_fm (And (c, d)) (Dvd (a, b)) = false
+  | eq_fm (Not c) (Dvd (a, b)) = false
+  | eq_fm (NDvd (c, d)) (Dvd (a, b)) = false
+  | eq_fm (NClosed b) (NEq a) = false
+  | eq_fm (Closed b) (NEq a) = false
+  | eq_fm (A b) (NEq a) = false
+  | eq_fm (E b) (NEq a) = false
+  | eq_fm (Iff (b, c)) (NEq a) = false
+  | eq_fm (Imp (b, c)) (NEq a) = false
+  | eq_fm (Or (b, c)) (NEq a) = false
+  | eq_fm (And (b, c)) (NEq a) = false
+  | eq_fm (Not b) (NEq a) = false
+  | eq_fm (NDvd (b, c)) (NEq a) = false
+  | eq_fm (Dvd (b, c)) (NEq a) = false
+  | eq_fm (NClosed b) (Eq a) = false
+  | eq_fm (Closed b) (Eq a) = false
+  | eq_fm (A b) (Eq a) = false
+  | eq_fm (E b) (Eq a) = false
+  | eq_fm (Iff (b, c)) (Eq a) = false
+  | eq_fm (Imp (b, c)) (Eq a) = false
+  | eq_fm (Or (b, c)) (Eq a) = false
+  | eq_fm (And (b, c)) (Eq a) = false
+  | eq_fm (Not b) (Eq a) = false
+  | eq_fm (NDvd (b, c)) (Eq a) = false
+  | eq_fm (Dvd (b, c)) (Eq a) = false
+  | eq_fm (NEq b) (Eq a) = false
+  | eq_fm (NClosed b) (Ge a) = false
+  | eq_fm (Closed b) (Ge a) = false
+  | eq_fm (A b) (Ge a) = false
+  | eq_fm (E b) (Ge a) = false
+  | eq_fm (Iff (b, c)) (Ge a) = false
+  | eq_fm (Imp (b, c)) (Ge a) = false
+  | eq_fm (Or (b, c)) (Ge a) = false
+  | eq_fm (And (b, c)) (Ge a) = false
+  | eq_fm (Not b) (Ge a) = false
+  | eq_fm (NDvd (b, c)) (Ge a) = false
+  | eq_fm (Dvd (b, c)) (Ge a) = false
+  | eq_fm (NEq b) (Ge a) = false
+  | eq_fm (Eq b) (Ge a) = false
+  | eq_fm (NClosed b) (Gt a) = false
+  | eq_fm (Closed b) (Gt a) = false
+  | eq_fm (A b) (Gt a) = false
+  | eq_fm (E b) (Gt a) = false
+  | eq_fm (Iff (b, c)) (Gt a) = false
+  | eq_fm (Imp (b, c)) (Gt a) = false
+  | eq_fm (Or (b, c)) (Gt a) = false
+  | eq_fm (And (b, c)) (Gt a) = false
+  | eq_fm (Not b) (Gt a) = false
+  | eq_fm (NDvd (b, c)) (Gt a) = false
+  | eq_fm (Dvd (b, c)) (Gt a) = false
+  | eq_fm (NEq b) (Gt a) = false
+  | eq_fm (Eq b) (Gt a) = false
+  | eq_fm (Ge b) (Gt a) = false
+  | eq_fm (NClosed b) (Le a) = false
+  | eq_fm (Closed b) (Le a) = false
+  | eq_fm (A b) (Le a) = false
+  | eq_fm (E b) (Le a) = false
+  | eq_fm (Iff (b, c)) (Le a) = false
+  | eq_fm (Imp (b, c)) (Le a) = false
+  | eq_fm (Or (b, c)) (Le a) = false
+  | eq_fm (And (b, c)) (Le a) = false
+  | eq_fm (Not b) (Le a) = false
+  | eq_fm (NDvd (b, c)) (Le a) = false
+  | eq_fm (Dvd (b, c)) (Le a) = false
+  | eq_fm (NEq b) (Le a) = false
+  | eq_fm (Eq b) (Le a) = false
+  | eq_fm (Ge b) (Le a) = false
+  | eq_fm (Gt b) (Le a) = false
+  | eq_fm (NClosed b) (Lt a) = false
+  | eq_fm (Closed b) (Lt a) = false
+  | eq_fm (A b) (Lt a) = false
+  | eq_fm (E b) (Lt a) = false
+  | eq_fm (Iff (b, c)) (Lt a) = false
+  | eq_fm (Imp (b, c)) (Lt a) = false
+  | eq_fm (Or (b, c)) (Lt a) = false
+  | eq_fm (And (b, c)) (Lt a) = false
+  | eq_fm (Not b) (Lt a) = false
+  | eq_fm (NDvd (b, c)) (Lt a) = false
+  | eq_fm (Dvd (b, c)) (Lt a) = false
+  | eq_fm (NEq b) (Lt a) = false
+  | eq_fm (Eq b) (Lt a) = false
+  | eq_fm (Ge b) (Lt a) = false
+  | eq_fm (Gt b) (Lt a) = false
+  | eq_fm (Le b) (Lt a) = false
+  | eq_fm (NClosed a) F = false
+  | eq_fm (Closed a) F = false
+  | eq_fm (A a) F = false
+  | eq_fm (E a) F = false
+  | eq_fm (Iff (a, b)) F = false
+  | eq_fm (Imp (a, b)) F = false
+  | eq_fm (Or (a, b)) F = false
+  | eq_fm (And (a, b)) F = false
+  | eq_fm (Not a) F = false
+  | eq_fm (NDvd (a, b)) F = false
+  | eq_fm (Dvd (a, b)) F = false
+  | eq_fm (NEq a) F = false
+  | eq_fm (Eq a) F = false
+  | eq_fm (Ge a) F = false
+  | eq_fm (Gt a) F = false
+  | eq_fm (Le a) F = false
+  | eq_fm (Lt a) F = false
+  | eq_fm (NClosed a) T = false
+  | eq_fm (Closed a) T = false
+  | eq_fm (A a) T = false
+  | eq_fm (E a) T = false
+  | eq_fm (Iff (a, b)) T = false
+  | eq_fm (Imp (a, b)) T = false
+  | eq_fm (Or (a, b)) T = false
+  | eq_fm (And (a, b)) T = false
+  | eq_fm (Not a) T = false
+  | eq_fm (NDvd (a, b)) T = false
+  | eq_fm (Dvd (a, b)) T = false
+  | eq_fm (NEq a) T = false
+  | eq_fm (Eq a) T = false
+  | eq_fm (Ge a) T = false
+  | eq_fm (Gt a) T = false
+  | eq_fm (Le a) T = false
+  | eq_fm (Lt a) T = false
   | eq_fm F T = false
   | eq_fm (Closed a) (NClosed b) = false
-  | eq_fm (A ab) (NClosed b) = false
-  | eq_fm (A ab) (Closed b) = false
-  | eq_fm (E ab) (NClosed b) = false
-  | eq_fm (E ab) (Closed b) = false
-  | eq_fm (E ab) (A bb) = false
-  | eq_fm (Iff (ab, bb)) (NClosed c) = false
-  | eq_fm (Iff (ab, bb)) (Closed c) = false
-  | eq_fm (Iff (ab, bb)) (A cb) = false
-  | eq_fm (Iff (ab, bb)) (E cb) = false
-  | eq_fm (Imp (ab, bb)) (NClosed c) = false
-  | eq_fm (Imp (ab, bb)) (Closed c) = false
-  | eq_fm (Imp (ab, bb)) (A cb) = false
-  | eq_fm (Imp (ab, bb)) (E cb) = false
-  | eq_fm (Imp (ab, bb)) (Iff (cb, d)) = false
-  | eq_fm (Or (ab, bb)) (NClosed c) = false
-  | eq_fm (Or (ab, bb)) (Closed c) = false
-  | eq_fm (Or (ab, bb)) (A cb) = false
-  | eq_fm (Or (ab, bb)) (E cb) = false
-  | eq_fm (Or (ab, bb)) (Iff (cb, d)) = false
-  | eq_fm (Or (ab, bb)) (Imp (cb, d)) = false
-  | eq_fm (And (ab, bb)) (NClosed c) = false
-  | eq_fm (And (ab, bb)) (Closed c) = false
-  | eq_fm (And (ab, bb)) (A cb) = false
-  | eq_fm (And (ab, bb)) (E cb) = false
-  | eq_fm (And (ab, bb)) (Iff (cb, d)) = false
-  | eq_fm (And (ab, bb)) (Imp (cb, d)) = false
-  | eq_fm (And (ab, bb)) (Or (cb, d)) = false
-  | eq_fm (Not ab) (NClosed b) = false
-  | eq_fm (Not ab) (Closed b) = false
-  | eq_fm (Not ab) (A bb) = false
-  | eq_fm (Not ab) (E bb) = false
-  | eq_fm (Not ab) (Iff (bb, cb)) = false
-  | eq_fm (Not ab) (Imp (bb, cb)) = false
-  | eq_fm (Not ab) (Or (bb, cb)) = false
-  | eq_fm (Not ab) (And (bb, cb)) = false
-  | eq_fm (NDvd (aa, bc)) (NClosed c) = false
-  | eq_fm (NDvd (aa, bc)) (Closed c) = false
-  | eq_fm (NDvd (aa, bc)) (A cb) = false
-  | eq_fm (NDvd (aa, bc)) (E cb) = false
-  | eq_fm (NDvd (aa, bc)) (Iff (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (Imp (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (Or (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (And (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (Not cb) = false
-  | eq_fm (Dvd (aa, bc)) (NClosed c) = false
-  | eq_fm (Dvd (aa, bc)) (Closed c) = false
-  | eq_fm (Dvd (aa, bc)) (A cb) = false
-  | eq_fm (Dvd (aa, bc)) (E cb) = false
-  | eq_fm (Dvd (aa, bc)) (Iff (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (Imp (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (Or (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (And (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (Not cb) = false
-  | eq_fm (Dvd (aa, bc)) (NDvd (ca, da)) = false
-  | eq_fm (NEq ac) (NClosed b) = false
-  | eq_fm (NEq ac) (Closed b) = false
-  | eq_fm (NEq ac) (A bb) = false
-  | eq_fm (NEq ac) (E bb) = false
-  | eq_fm (NEq ac) (Iff (bb, cb)) = false
-  | eq_fm (NEq ac) (Imp (bb, cb)) = false
-  | eq_fm (NEq ac) (Or (bb, cb)) = false
-  | eq_fm (NEq ac) (And (bb, cb)) = false
-  | eq_fm (NEq ac) (Not bb) = false
-  | eq_fm (NEq ac) (NDvd (ba, cc)) = false
-  | eq_fm (NEq ac) (Dvd (ba, cc)) = false
-  | eq_fm (Eq ac) (NClosed b) = false
-  | eq_fm (Eq ac) (Closed b) = false
-  | eq_fm (Eq ac) (A bb) = false
-  | eq_fm (Eq ac) (E bb) = false
-  | eq_fm (Eq ac) (Iff (bb, cb)) = false
-  | eq_fm (Eq ac) (Imp (bb, cb)) = false
-  | eq_fm (Eq ac) (Or (bb, cb)) = false
-  | eq_fm (Eq ac) (And (bb, cb)) = false
-  | eq_fm (Eq ac) (Not bb) = false
-  | eq_fm (Eq ac) (NDvd (ba, cc)) = false
-  | eq_fm (Eq ac) (Dvd (ba, cc)) = false
-  | eq_fm (Eq ac) (NEq bc) = false
-  | eq_fm (Ge ac) (NClosed b) = false
-  | eq_fm (Ge ac) (Closed b) = false
-  | eq_fm (Ge ac) (A bb) = false
-  | eq_fm (Ge ac) (E bb) = false
-  | eq_fm (Ge ac) (Iff (bb, cb)) = false
-  | eq_fm (Ge ac) (Imp (bb, cb)) = false
-  | eq_fm (Ge ac) (Or (bb, cb)) = false
-  | eq_fm (Ge ac) (And (bb, cb)) = false
-  | eq_fm (Ge ac) (Not bb) = false
-  | eq_fm (Ge ac) (NDvd (ba, cc)) = false
-  | eq_fm (Ge ac) (Dvd (ba, cc)) = false
-  | eq_fm (Ge ac) (NEq bc) = false
-  | eq_fm (Ge ac) (Eq bc) = false
-  | eq_fm (Gt ac) (NClosed b) = false
-  | eq_fm (Gt ac) (Closed b) = false
-  | eq_fm (Gt ac) (A bb) = false
-  | eq_fm (Gt ac) (E bb) = false
-  | eq_fm (Gt ac) (Iff (bb, cb)) = false
-  | eq_fm (Gt ac) (Imp (bb, cb)) = false
-  | eq_fm (Gt ac) (Or (bb, cb)) = false
-  | eq_fm (Gt ac) (And (bb, cb)) = false
-  | eq_fm (Gt ac) (Not bb) = false
-  | eq_fm (Gt ac) (NDvd (ba, cc)) = false
-  | eq_fm (Gt ac) (Dvd (ba, cc)) = false
-  | eq_fm (Gt ac) (NEq bc) = false
-  | eq_fm (Gt ac) (Eq bc) = false
-  | eq_fm (Gt ac) (Ge bc) = false
-  | eq_fm (Le ac) (NClosed b) = false
-  | eq_fm (Le ac) (Closed b) = false
-  | eq_fm (Le ac) (A bb) = false
-  | eq_fm (Le ac) (E bb) = false
-  | eq_fm (Le ac) (Iff (bb, cb)) = false
-  | eq_fm (Le ac) (Imp (bb, cb)) = false
-  | eq_fm (Le ac) (Or (bb, cb)) = false
-  | eq_fm (Le ac) (And (bb, cb)) = false
-  | eq_fm (Le ac) (Not bb) = false
-  | eq_fm (Le ac) (NDvd (ba, cc)) = false
-  | eq_fm (Le ac) (Dvd (ba, cc)) = false
-  | eq_fm (Le ac) (NEq bc) = false
-  | eq_fm (Le ac) (Eq bc) = false
-  | eq_fm (Le ac) (Ge bc) = false
-  | eq_fm (Le ac) (Gt bc) = false
-  | eq_fm (Lt ac) (NClosed b) = false
-  | eq_fm (Lt ac) (Closed b) = false
-  | eq_fm (Lt ac) (A bb) = false
-  | eq_fm (Lt ac) (E bb) = false
-  | eq_fm (Lt ac) (Iff (bb, cb)) = false
-  | eq_fm (Lt ac) (Imp (bb, cb)) = false
-  | eq_fm (Lt ac) (Or (bb, cb)) = false
-  | eq_fm (Lt ac) (And (bb, cb)) = false
-  | eq_fm (Lt ac) (Not bb) = false
-  | eq_fm (Lt ac) (NDvd (ba, cc)) = false
-  | eq_fm (Lt ac) (Dvd (ba, cc)) = false
-  | eq_fm (Lt ac) (NEq bc) = false
-  | eq_fm (Lt ac) (Eq bc) = false
-  | eq_fm (Lt ac) (Ge bc) = false
-  | eq_fm (Lt ac) (Gt bc) = false
-  | eq_fm (Lt ac) (Le bc) = false
+  | eq_fm (A a) (NClosed b) = false
+  | eq_fm (A a) (Closed b) = false
+  | eq_fm (E a) (NClosed b) = false
+  | eq_fm (E a) (Closed b) = false
+  | eq_fm (E a) (A b) = false
+  | eq_fm (Iff (a, b)) (NClosed c) = false
+  | eq_fm (Iff (a, b)) (Closed c) = false
+  | eq_fm (Iff (a, b)) (A c) = false
+  | eq_fm (Iff (a, b)) (E c) = false
+  | eq_fm (Imp (a, b)) (NClosed c) = false
+  | eq_fm (Imp (a, b)) (Closed c) = false
+  | eq_fm (Imp (a, b)) (A c) = false
+  | eq_fm (Imp (a, b)) (E c) = false
+  | eq_fm (Imp (a, b)) (Iff (c, d)) = false
+  | eq_fm (Or (a, b)) (NClosed c) = false
+  | eq_fm (Or (a, b)) (Closed c) = false
+  | eq_fm (Or (a, b)) (A c) = false
+  | eq_fm (Or (a, b)) (E c) = false
+  | eq_fm (Or (a, b)) (Iff (c, d)) = false
+  | eq_fm (Or (a, b)) (Imp (c, d)) = false
+  | eq_fm (And (a, b)) (NClosed c) = false
+  | eq_fm (And (a, b)) (Closed c) = false
+  | eq_fm (And (a, b)) (A c) = false
+  | eq_fm (And (a, b)) (E c) = false
+  | eq_fm (And (a, b)) (Iff (c, d)) = false
+  | eq_fm (And (a, b)) (Imp (c, d)) = false
+  | eq_fm (And (a, b)) (Or (c, d)) = false
+  | eq_fm (Not a) (NClosed b) = false
+  | eq_fm (Not a) (Closed b) = false
+  | eq_fm (Not a) (A b) = false
+  | eq_fm (Not a) (E b) = false
+  | eq_fm (Not a) (Iff (b, c)) = false
+  | eq_fm (Not a) (Imp (b, c)) = false
+  | eq_fm (Not a) (Or (b, c)) = false
+  | eq_fm (Not a) (And (b, c)) = false
+  | eq_fm (NDvd (a, b)) (NClosed c) = false
+  | eq_fm (NDvd (a, b)) (Closed c) = false
+  | eq_fm (NDvd (a, b)) (A c) = false
+  | eq_fm (NDvd (a, b)) (E c) = false
+  | eq_fm (NDvd (a, b)) (Iff (c, d)) = false
+  | eq_fm (NDvd (a, b)) (Imp (c, d)) = false
+  | eq_fm (NDvd (a, b)) (Or (c, d)) = false
+  | eq_fm (NDvd (a, b)) (And (c, d)) = false
+  | eq_fm (NDvd (a, b)) (Not c) = false
+  | eq_fm (Dvd (a, b)) (NClosed c) = false
+  | eq_fm (Dvd (a, b)) (Closed c) = false
+  | eq_fm (Dvd (a, b)) (A c) = false
+  | eq_fm (Dvd (a, b)) (E c) = false
+  | eq_fm (Dvd (a, b)) (Iff (c, d)) = false
+  | eq_fm (Dvd (a, b)) (Imp (c, d)) = false
+  | eq_fm (Dvd (a, b)) (Or (c, d)) = false
+  | eq_fm (Dvd (a, b)) (And (c, d)) = false
+  | eq_fm (Dvd (a, b)) (Not c) = false
+  | eq_fm (Dvd (a, b)) (NDvd (c, d)) = false
+  | eq_fm (NEq a) (NClosed b) = false
+  | eq_fm (NEq a) (Closed b) = false
+  | eq_fm (NEq a) (A b) = false
+  | eq_fm (NEq a) (E b) = false
+  | eq_fm (NEq a) (Iff (b, c)) = false
+  | eq_fm (NEq a) (Imp (b, c)) = false
+  | eq_fm (NEq a) (Or (b, c)) = false
+  | eq_fm (NEq a) (And (b, c)) = false
+  | eq_fm (NEq a) (Not b) = false
+  | eq_fm (NEq a) (NDvd (b, c)) = false
+  | eq_fm (NEq a) (Dvd (b, c)) = false
+  | eq_fm (Eq a) (NClosed b) = false
+  | eq_fm (Eq a) (Closed b) = false
+  | eq_fm (Eq a) (A b) = false
+  | eq_fm (Eq a) (E b) = false
+  | eq_fm (Eq a) (Iff (b, c)) = false
+  | eq_fm (Eq a) (Imp (b, c)) = false
+  | eq_fm (Eq a) (Or (b, c)) = false
+  | eq_fm (Eq a) (And (b, c)) = false
+  | eq_fm (Eq a) (Not b) = false
+  | eq_fm (Eq a) (NDvd (b, c)) = false
+  | eq_fm (Eq a) (Dvd (b, c)) = false
+  | eq_fm (Eq a) (NEq b) = false
+  | eq_fm (Ge a) (NClosed b) = false
+  | eq_fm (Ge a) (Closed b) = false
+  | eq_fm (Ge a) (A b) = false
+  | eq_fm (Ge a) (E b) = false
+  | eq_fm (Ge a) (Iff (b, c)) = false
+  | eq_fm (Ge a) (Imp (b, c)) = false
+  | eq_fm (Ge a) (Or (b, c)) = false
+  | eq_fm (Ge a) (And (b, c)) = false
+  | eq_fm (Ge a) (Not b) = false
+  | eq_fm (Ge a) (NDvd (b, c)) = false
+  | eq_fm (Ge a) (Dvd (b, c)) = false
+  | eq_fm (Ge a) (NEq b) = false
+  | eq_fm (Ge a) (Eq b) = false
+  | eq_fm (Gt a) (NClosed b) = false
+  | eq_fm (Gt a) (Closed b) = false
+  | eq_fm (Gt a) (A b) = false
+  | eq_fm (Gt a) (E b) = false
+  | eq_fm (Gt a) (Iff (b, c)) = false
+  | eq_fm (Gt a) (Imp (b, c)) = false
+  | eq_fm (Gt a) (Or (b, c)) = false
+  | eq_fm (Gt a) (And (b, c)) = false
+  | eq_fm (Gt a) (Not b) = false
+  | eq_fm (Gt a) (NDvd (b, c)) = false
+  | eq_fm (Gt a) (Dvd (b, c)) = false
+  | eq_fm (Gt a) (NEq b) = false
+  | eq_fm (Gt a) (Eq b) = false
+  | eq_fm (Gt a) (Ge b) = false
+  | eq_fm (Le a) (NClosed b) = false
+  | eq_fm (Le a) (Closed b) = false
+  | eq_fm (Le a) (A b) = false
+  | eq_fm (Le a) (E b) = false
+  | eq_fm (Le a) (Iff (b, c)) = false
+  | eq_fm (Le a) (Imp (b, c)) = false
+  | eq_fm (Le a) (Or (b, c)) = false
+  | eq_fm (Le a) (And (b, c)) = false
+  | eq_fm (Le a) (Not b) = false
+  | eq_fm (Le a) (NDvd (b, c)) = false
+  | eq_fm (Le a) (Dvd (b, c)) = false
+  | eq_fm (Le a) (NEq b) = false
+  | eq_fm (Le a) (Eq b) = false
+  | eq_fm (Le a) (Ge b) = false
+  | eq_fm (Le a) (Gt b) = false
+  | eq_fm (Lt a) (NClosed b) = false
+  | eq_fm (Lt a) (Closed b) = false
+  | eq_fm (Lt a) (A b) = false
+  | eq_fm (Lt a) (E b) = false
+  | eq_fm (Lt a) (Iff (b, c)) = false
+  | eq_fm (Lt a) (Imp (b, c)) = false
+  | eq_fm (Lt a) (Or (b, c)) = false
+  | eq_fm (Lt a) (And (b, c)) = false
+  | eq_fm (Lt a) (Not b) = false
+  | eq_fm (Lt a) (NDvd (b, c)) = false
+  | eq_fm (Lt a) (Dvd (b, c)) = false
+  | eq_fm (Lt a) (NEq b) = false
+  | eq_fm (Lt a) (Eq b) = false
+  | eq_fm (Lt a) (Ge b) = false
+  | eq_fm (Lt a) (Gt b) = false
+  | eq_fm (Lt a) (Le b) = false
   | eq_fm F (NClosed a) = false
   | eq_fm F (Closed a) = false
-  | eq_fm F (A ab) = false
-  | eq_fm F (E ab) = false
-  | eq_fm F (Iff (ab, bb)) = false
-  | eq_fm F (Imp (ab, bb)) = false
-  | eq_fm F (Or (ab, bb)) = false
-  | eq_fm F (And (ab, bb)) = false
-  | eq_fm F (Not ab) = false
-  | eq_fm F (NDvd (aa, bc)) = false
-  | eq_fm F (Dvd (aa, bc)) = false
-  | eq_fm F (NEq ac) = false
-  | eq_fm F (Eq ac) = false
-  | eq_fm F (Ge ac) = false
-  | eq_fm F (Gt ac) = false
-  | eq_fm F (Le ac) = false
-  | eq_fm F (Lt ac) = false
+  | eq_fm F (A a) = false
+  | eq_fm F (E a) = false
+  | eq_fm F (Iff (a, b)) = false
+  | eq_fm F (Imp (a, b)) = false
+  | eq_fm F (Or (a, b)) = false
+  | eq_fm F (And (a, b)) = false
+  | eq_fm F (Not a) = false
+  | eq_fm F (NDvd (a, b)) = false
+  | eq_fm F (Dvd (a, b)) = false
+  | eq_fm F (NEq a) = false
+  | eq_fm F (Eq a) = false
+  | eq_fm F (Ge a) = false
+  | eq_fm F (Gt a) = false
+  | eq_fm F (Le a) = false
+  | eq_fm F (Lt a) = false
   | eq_fm T (NClosed a) = false
   | eq_fm T (Closed a) = false
-  | eq_fm T (A ab) = false
-  | eq_fm T (E ab) = false
-  | eq_fm T (Iff (ab, bb)) = false
-  | eq_fm T (Imp (ab, bb)) = false
-  | eq_fm T (Or (ab, bb)) = false
-  | eq_fm T (And (ab, bb)) = false
-  | eq_fm T (Not ab) = false
-  | eq_fm T (NDvd (aa, bc)) = false
-  | eq_fm T (Dvd (aa, bc)) = false
-  | eq_fm T (NEq ac) = false
-  | eq_fm T (Eq ac) = false
-  | eq_fm T (Ge ac) = false
-  | eq_fm T (Gt ac) = false
-  | eq_fm T (Le ac) = false
-  | eq_fm T (Lt ac) = false
+  | eq_fm T (A a) = false
+  | eq_fm T (E a) = false
+  | eq_fm T (Iff (a, b)) = false
+  | eq_fm T (Imp (a, b)) = false
+  | eq_fm T (Or (a, b)) = false
+  | eq_fm T (And (a, b)) = false
+  | eq_fm T (Not a) = false
+  | eq_fm T (NDvd (a, b)) = false
+  | eq_fm T (Dvd (a, b)) = false
+  | eq_fm T (NEq a) = false
+  | eq_fm T (Eq a) = false
+  | eq_fm T (Ge a) = false
+  | eq_fm T (Gt a) = false
+  | eq_fm T (Le a) = false
+  | eq_fm T (Lt a) = false
   | eq_fm T F = false
   | eq_fm (NClosed nat) (NClosed nat') = ((nat : IntInf.int) = nat')
   | eq_fm (Closed nat) (Closed nat') = ((nat : IntInf.int) = nat')
@@ -554,7 +554,7 @@
                      | NClosed nat => Or (f p, q))
                 end));
 
-fun foldr f [] y = y
+fun foldr f [] a = a
   | foldr f (x :: xs) a = f x (foldr f xs a);
 
 fun evaldjf f ps = foldr (djf f) ps F;
@@ -607,9 +607,9 @@
   | numsubst0 t (Add (a, b)) = Add (numsubst0 t a, numsubst0 t b)
   | numsubst0 t (Sub (a, b)) = Sub (numsubst0 t a, numsubst0 t b)
   | numsubst0 t (Mul (i, a)) = Mul (i, numsubst0 t a)
-  | numsubst0 ta (Cn (v, ia, aa)) =
-    (if eqop eq_nat v 0 then Add (Mul (ia, ta), numsubst0 ta aa)
-      else Cn (suc (minus_nat v 1), ia, numsubst0 ta aa));
+  | numsubst0 t (Cn (v, i, a)) =
+    (if eqop eq_nat v 0 then Add (Mul (i, t), numsubst0 t a)
+      else Cn (suc (minus_nat v 1), i, numsubst0 t a));
 
 fun subst0 t T = T
   | subst0 t F = F
@@ -691,36 +691,35 @@
   | minusinf (NEq (Cn (hm, c, e))) =
     (if eqop eq_nat hm 0 then T else NEq (Cn (suc (minus_nat hm 1), c, e)));
 
-fun adjust b =
-  (fn a as (q, r) =>
-    (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
-      then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
-             IntInf.- (r, b))
-      else (IntInf.* ((2 : IntInf.int), q), r)));
+val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
 
-fun negDivAlg a b =
-  (if IntInf.<= ((0 : IntInf.int), IntInf.+ (a, b)) orelse
-        IntInf.<= (b, (0 : IntInf.int))
-    then ((~1 : IntInf.int), IntInf.+ (a, b))
-    else adjust b (negDivAlg a (IntInf.* ((2 : IntInf.int), b))));
+fun sgn_int i =
+  (if eqop eq_int i (0 : IntInf.int) then (0 : IntInf.int)
+    else (if IntInf.< ((0 : IntInf.int), i) then (1 : IntInf.int)
+           else IntInf.~ (1 : IntInf.int)));
 
 fun apsnd f (x, y) = (x, f y);
 
-val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
-
-fun posDivAlg a b =
-  (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
-    then ((0 : IntInf.int), a)
-    else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
-
-fun divmoda a b =
-  (if IntInf.<= ((0 : IntInf.int), a)
-    then (if IntInf.<= ((0 : IntInf.int), b) then posDivAlg a b
-           else (if eqop eq_int a (0 : IntInf.int)
-                  then ((0 : IntInf.int), (0 : IntInf.int))
-                  else apsnd IntInf.~ (negDivAlg (IntInf.~ a) (IntInf.~ b))))
-    else (if IntInf.< ((0 : IntInf.int), b) then negDivAlg a b
-           else apsnd IntInf.~ (posDivAlg (IntInf.~ a) (IntInf.~ b))));
+fun divmoda k l =
+  (if eqop eq_int k (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int))
+    else (if eqop eq_int l (0 : IntInf.int) then ((0 : IntInf.int), k)
+           else apsnd (fn a => IntInf.* (sgn_int l, a))
+                  (if eqop eq_int (sgn_int k) (sgn_int l)
+                    then (fn k => fn l => IntInf.divMod (IntInf.abs k,
+                           IntInf.abs l))
+                           k l
+                    else let
+                           val a =
+                             (fn k => fn l => IntInf.divMod (IntInf.abs k,
+                               IntInf.abs l))
+                               k l;
+                           val (r, s) = a;
+                         in
+                           (if eqop eq_int s (0 : IntInf.int)
+                             then (IntInf.~ r, (0 : IntInf.int))
+                             else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
+                                    IntInf.- (abs_int l, s)))
+                         end)));
 
 fun mod_int a b = snd (divmoda a b);
 
@@ -823,23 +822,23 @@
       else nummul i (simpnum t))
   | simpnum (Cn (v, va, vb)) = Cn (v, va, vb);
 
-fun nota (Not y) = y
+fun nota (Not p) = p
   | nota T = F
   | nota F = T
-  | nota (Lt vc) = Not (Lt vc)
-  | nota (Le vc) = Not (Le vc)
-  | nota (Gt vc) = Not (Gt vc)
-  | nota (Ge vc) = Not (Ge vc)
-  | nota (Eq vc) = Not (Eq vc)
-  | nota (NEq vc) = Not (NEq vc)
-  | nota (Dvd (va, vab)) = Not (Dvd (va, vab))
-  | nota (NDvd (va, vab)) = Not (NDvd (va, vab))
-  | nota (And (vb, vaa)) = Not (And (vb, vaa))
-  | nota (Or (vb, vaa)) = Not (Or (vb, vaa))
-  | nota (Imp (vb, vaa)) = Not (Imp (vb, vaa))
-  | nota (Iff (vb, vaa)) = Not (Iff (vb, vaa))
-  | nota (E vb) = Not (E vb)
-  | nota (A vb) = Not (A vb)
+  | nota (Lt v) = Not (Lt v)
+  | nota (Le v) = Not (Le v)
+  | nota (Gt v) = Not (Gt v)
+  | nota (Ge v) = Not (Ge v)
+  | nota (Eq v) = Not (Eq v)
+  | nota (NEq v) = Not (NEq v)
+  | nota (Dvd (v, va)) = Not (Dvd (v, va))
+  | nota (NDvd (v, va)) = Not (NDvd (v, va))
+  | nota (And (v, va)) = Not (And (v, va))
+  | nota (Or (v, va)) = Not (Or (v, va))
+  | nota (Imp (v, va)) = Not (Imp (v, va))
+  | nota (Iff (v, va)) = Not (Iff (v, va))
+  | nota (E v) = Not (E v)
+  | nota (A v) = Not (A v)
   | nota (Closed v) = Not (Closed v)
   | nota (NClosed v) = Not (NClosed v);
 
@@ -1184,7 +1183,7 @@
   | delta (Le v) = (1 : IntInf.int)
   | delta (Gt w) = (1 : IntInf.int)
   | delta (Ge x) = (1 : IntInf.int)
-  | delta (Eq ya) = (1 : IntInf.int)
+  | delta (Eq y) = (1 : IntInf.int)
   | delta (NEq z) = (1 : IntInf.int)
   | delta (Dvd (aa, C bo)) = (1 : IntInf.int)
   | delta (Dvd (aa, Bound bp)) = (1 : IntInf.int)
@@ -1205,10 +1204,10 @@
   | delta (A ao) = (1 : IntInf.int)
   | delta (Closed ap) = (1 : IntInf.int)
   | delta (NClosed aq) = (1 : IntInf.int)
-  | delta (Dvd (b, Cn (cm, c, e))) =
-    (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
-  | delta (NDvd (b, Cn (dm, c, e))) =
-    (if eqop eq_nat dm 0 then b else (1 : IntInf.int));
+  | delta (Dvd (i, Cn (cm, c, e))) =
+    (if eqop eq_nat cm 0 then i else (1 : IntInf.int))
+  | delta (NDvd (i, Cn (dm, c, e))) =
+    (if eqop eq_nat dm 0 then i else (1 : IntInf.int));
 
 fun div_int a b = fst (divmoda a b);
 
@@ -1367,22 +1366,22 @@
   | zeta (A ao) = (1 : IntInf.int)
   | zeta (Closed ap) = (1 : IntInf.int)
   | zeta (NClosed aq) = (1 : IntInf.int)
-  | zeta (Lt (Cn (cm, b, e))) =
-    (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
-  | zeta (Le (Cn (dm, b, e))) =
-    (if eqop eq_nat dm 0 then b else (1 : IntInf.int))
-  | zeta (Gt (Cn (em, b, e))) =
-    (if eqop eq_nat em 0 then b else (1 : IntInf.int))
-  | zeta (Ge (Cn (fm, b, e))) =
-    (if eqop eq_nat fm 0 then b else (1 : IntInf.int))
-  | zeta (Eq (Cn (gm, b, e))) =
-    (if eqop eq_nat gm 0 then b else (1 : IntInf.int))
-  | zeta (NEq (Cn (hm, b, e))) =
-    (if eqop eq_nat hm 0 then b else (1 : IntInf.int))
-  | zeta (Dvd (i, Cn (im, b, e))) =
-    (if eqop eq_nat im 0 then b else (1 : IntInf.int))
-  | zeta (NDvd (i, Cn (jm, b, e))) =
-    (if eqop eq_nat jm 0 then b else (1 : IntInf.int));
+  | zeta (Lt (Cn (cm, c, e))) =
+    (if eqop eq_nat cm 0 then c else (1 : IntInf.int))
+  | zeta (Le (Cn (dm, c, e))) =
+    (if eqop eq_nat dm 0 then c else (1 : IntInf.int))
+  | zeta (Gt (Cn (em, c, e))) =
+    (if eqop eq_nat em 0 then c else (1 : IntInf.int))
+  | zeta (Ge (Cn (fm, c, e))) =
+    (if eqop eq_nat fm 0 then c else (1 : IntInf.int))
+  | zeta (Eq (Cn (gm, c, e))) =
+    (if eqop eq_nat gm 0 then c else (1 : IntInf.int))
+  | zeta (NEq (Cn (hm, c, e))) =
+    (if eqop eq_nat hm 0 then c else (1 : IntInf.int))
+  | zeta (Dvd (i, Cn (im, c, e))) =
+    (if eqop eq_nat im 0 then c else (1 : IntInf.int))
+  | zeta (NDvd (i, Cn (jm, c, e))) =
+    (if eqop eq_nat jm 0 then c else (1 : IntInf.int));
 
 fun zsplit0 (C c) = ((0 : IntInf.int), C c)
   | zsplit0 (Bound n) =
@@ -1691,4 +1690,16 @@
   (if IntInf.<= (i, (0 : IntInf.int)) then n
     else nat_aux (IntInf.- (i, (1 : IntInf.int))) (suc n));
 
+fun adjust b =
+  (fn a as (q, r) =>
+    (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
+      then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
+             IntInf.- (r, b))
+      else (IntInf.* ((2 : IntInf.int), q), r)));
+
+fun posDivAlg a b =
+  (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
+    then ((0 : IntInf.int), a)
+    else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
+
 end; (*struct GeneratedCooper*)

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 16 13:42:45 2009 -0800
@@ -262,7 +262,8 @@
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
-    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])]
+    |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
+         [Nitpick_Const_Simp_Thms.add])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
     |-> (fn thms => pair (reccomb_names, Library.flat thms))

--- a/src/HOL/ex/Codegenerator_Pretty.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Codegenerator_Pretty.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 

--- a/src/HOL/ex/Efficient_Nat_examples.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/ex/Efficient_Nat_examples.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -1,12 +1,11 @@
 (*  Title:      HOL/ex/Efficient_Nat_examples.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Simple examples for Efficient\_Nat theory. *}
 
 theory Efficient_Nat_examples
-imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat
+imports Complex_Main Efficient_Nat
 begin
 
 fun to_n :: "nat \<Rightarrow> nat list" where

--- a/src/HOL/ex/Numeral.thy	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/HOL/ex/Numeral.thy	Mon Feb 16 13:42:45 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Numeral.thy
-    ID:         $Id$
     Author:     Florian Haftmann
 
 An experimental alternative numeral representation.
@@ -216,7 +215,7 @@
 
 text {*
   We embed binary representations into a generic algebraic
-  structure using @{text of_num}
+  structure using @{text of_num}.
 *}
 
 class semiring_numeral = semiring + monoid_mult
@@ -764,7 +763,7 @@
 
 subsection {* Numeral equations as default simplification rules *}
 
-text {* TODO.  Be more precise here with respect to subsumed facts. *}
+text {* TODO.  Be more precise here with respect to subsumed facts.  Or use named theorems anyway. *}
 declare (in semiring_numeral) numeral [simp]
 declare (in semiring_1) numeral [simp]
 declare (in semiring_char_0) numeral [simp]

--- a/src/Pure/ProofGeneral/ROOT.ML	Mon Feb 16 13:42:15 2009 -0800
+++ b/src/Pure/ProofGeneral/ROOT.ML	Mon Feb 16 13:42:45 2009 -0800
@@ -18,7 +18,7 @@
   |> setmp Proofterm.proofs 1
   |> setmp quick_and_dirty true
   |> setmp auto_quickcheck true
-  |> setmp auto_solve false) "preferences.ML";
+  |> setmp auto_solve true) "preferences.ML";
 
 use "pgip_parser.ML";