Fix another bug in Omega d.p.

Thanks to someplaceguy for reporting these.

Progress of sorts with github issue #1207

src/integer/OmegaShell.sml

@@ -85,7 +85,7 @@ end
 fun callsimple t =
     (OmegaSimple.simple_CONV ORELSEC
      (OmegaSymbolic.eliminate_an_existential THENC
-      EVERY_DISJ_CONV callsimple)) t
+      EVERY_DISJ_CONV (IS_NOT_EXISTS_CONV ORELSEC callsimple))) t
 
 val simple =
   TRY_CONV (STRIP_QUANT_CONV OmegaMath.cond_removal) THENC

src/integer/OmegaSymbolic.sml

@@ -23,14 +23,6 @@ val lhand = rand o rator
 
 val REWRITE_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV bool_rewrites
 
-fun EVERY_CONJ_CONV c t =
-    if is_conj t then BINOP_CONV (EVERY_CONJ_CONV c) t
-    else c t
-
-fun EVERY_DISJ_CONV c t =
-    if is_disj t then BINOP_CONV (EVERY_DISJ_CONV c) t
-    else c t
-
 fun ERR f msg = HOL_ERR { origin_structure = "OmegaSymbolic",
                           origin_function = f,
                           message = msg}
@@ -262,11 +254,7 @@ end
 
     tm is of the form   ?x. (c * x = e) /\ c1 /\ c2 /\ c3
     where each ci is either of the form  d * x <= U  or  L <= e * x.
-    If e contains any variables that appear in ctxt, then
-    leaf_normalise all of the ci's and the equality term and then rename
-    x to be v (which is its correct name).
-
-    Otherwise, multiply the ci's through so as to make them include
+    Multiply the ci's through so as to make them include
     c * x as a subterm, then rewrite with the first conjunct, and then
     leaf normalise.  The variable x will have been eliminated from all
     but the first conjunct.  Then push the ?x inwards, and turn that
@@ -322,11 +310,11 @@ fun do_divisibility_analysis v ctxt tm = let
   val (x, body) = dest_exists tm
   val (eqterm, rest) = dest_conj body
 in
-  if not (null (op_intersect aconv (free_vars (rand eqterm)) ctxt)) then
+  (*if not (null (op_intersect aconv (free_vars (rand eqterm)) ctxt)) then
     (* leave it as an equality *)
     BINDER_CONV (EVERY_CONJ_CONV OmegaMath.leaf_normalise) THENC
     RAND_CONV (ALPHA_CONV v)
-  else let
+  else*) let
       val c = lhand (lhand eqterm)
       val c_i = int_of_term c
       fun ctxt_rwt tm = let
@@ -468,8 +456,9 @@ fun apply_fmve ctype = let
         RAND_CONV (calculate_nightmare ctxt)
       end
   end t
-  fun elim_rT tm = (if Teq (rand tm) then REWR_CONV CooperThms.T_and_r
-                    else ALL_CONV) tm
+  fun elim_rT tm =
+      (if Teq (rand tm) then REWR_CONV CooperThms.T_and_r
+       else PURE_REWRITE_CONV [RIGHT_AND_OVER_OR, OR_CLAUSES, AND_CLAUSES]) tm
 in
   initially THENC LAND_CONV finisher THENC elim_rT
 end

src/integer/testing/selftest.sml

@@ -71,4 +71,13 @@ val _ = convtest ("decide_closed_presburger w/genvar % 4",
                       $var$(%%genvar%%801) + r = 0”,
                   boolSyntax.F);
 
+val _ = convtest ("decide_closed_presburger gh1207c",
+                  OmegaShell.decide_closed_presburger,
+                  “∀x q r:int.
+                    41 * x = q * 42 + r ∧ 0 ≤ r ∧ r < 42 ⇒
+                    ∀k r'.
+                       41 * x = k * 42 + r' ∧ 0 ≤ r' ∧ r' < 42 ⇒
+                       x ≤ -42 ∨ 1 < r ∨ -21 < k”,
+                  boolSyntax.T);
+
 val _ = exit_count0 erc

src/integer/testing/test_cases.sml

@@ -262,6 +262,7 @@ val terms_to_test =
   ("Github1203d", “0n = Num 0i”, true),
   ("Github1207a", “&(x - x:num) = 0i”, true),
   ("Github1207b", “&(x - a:num) <= &x:int”, true),
+  ("Github1207c", “x <= -42 \/ 1 < (41 * x) % 42 \/ -21 < (41 * x) / 42”, true),
   ("Github1209a",
    “! $var$(_ _) q r:int.
           0 = q * 5 + r /\ 0 <= r /\ r < 5 ==>