# HG changeset patch
# User wenzelm
# Date 1394037400 -3600
# Node ID 22e9fc998d65770ef64c4f96d8674f5784640a93
# Parent  f376f18fd0b7b141532f8177c0a239cd0b34f72b
tuned proofs;

diff -r f376f18fd0b7 -r 22e9fc998d65 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Mar 05 16:16:36 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Mar 05 17:36:40 2014 +0100
@@ -405,10 +405,10 @@
 fun bnds :: "num \<Rightarrow> nat list"
 where
   "bnds (Bound n) = [n]"
-| "bnds (CN n c a) = n#(bnds a)"
+| "bnds (CN n c a) = n # bnds a"
 | "bnds (Neg a) = bnds a"
-| "bnds (Add a b) = (bnds a)@(bnds b)"
-| "bnds (Sub a b) = (bnds a)@(bnds b)"
+| "bnds (Add a b) = bnds a @ bnds b"
+| "bnds (Sub a b) =  bnds a @ bnds b"
 | "bnds (Mul i a) = bnds a"
 | "bnds a = []"
 
@@ -422,12 +422,12 @@
   where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
 
 consts numadd:: "num \<times> num \<Rightarrow> num"
-recdef numadd "measure (\<lambda>(t,s). num_size t + num_size s)"
+recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
   "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
     (if n1 = n2 then
       (let c = c1 + c2
-       in if c=0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2)))
-     else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2))
+       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2)))
+     else if n1 \<le> 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, t) = CN n1 c1 (numadd (r1, t))"
   "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
@@ -608,20 +608,20 @@
 | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
 | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
 | "simpfm (NOT p) = not (simpfm p)"
-| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F | _ \<Rightarrow> Lt a')"
-| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le a')"
-| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"
-| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge a')"
-| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
-| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq a')"
+| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v < 0 then T else F | _ \<Rightarrow> Lt a')"
+| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<le> 0 then T else F | _ \<Rightarrow> Le a')"
+| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v > 0 then T else F | _ \<Rightarrow> Gt a')"
+| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<ge> 0 then T else F | _ \<Rightarrow> Ge a')"
+| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v = 0 then T else F | _ \<Rightarrow> Eq a')"
+| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<noteq> 0 then T else F | _ \<Rightarrow> NEq a')"
 | "simpfm (Dvd i a) =
     (if i = 0 then simpfm (Eq a)
      else if abs i = 1 then T
-     else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"
+     else let a' = simpnum a in case a' of C v \<Rightarrow> if i dvd v then T else F | _ \<Rightarrow> Dvd i a')"
 | "simpfm (NDvd i a) =
     (if i = 0 then simpfm (NEq a)
      else if abs i = 1 then F
-     else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')"
+     else let a' = simpnum a in case a' of C v \<Rightarrow> if \<not>( i dvd v) then T else F | _ \<Rightarrow> NDvd i a')"
 | "simpfm p = p"
   by pat_completeness auto
 termination by (relation "measure fmsize") auto
@@ -823,7 +823,8 @@
 | "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"
 
 lemma zsplit0_I:
-  shows "\<And>n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a"
+  shows "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
+    (Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t) \<and> numbound0 a"
   (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
 proof (induct t rule: zsplit0.induct)
   case (1 c n a)
@@ -1308,7 +1309,7 @@
 qed simp_all
 
 
-consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- {* adjust the coeffitients of a formula *}
+consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- {* adjust the coefficients of a formula *}
 recdef a_\<beta> "measure size"
   "a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
   "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
@@ -1428,110 +1429,147 @@
     by simp_all
   fix a
   from 4 have "\<forall>x < (- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
-  proof(clarsimp)
-    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
+  proof clarsimp
+    fix x
+    assume "x < (- Inum (a#bs) e)" and"x + Inum (x # bs) e = 0"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "False" by simp
   qed
   then show ?case by auto
 next
-  case (5 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (5 c e)
+  then have c1: "c = 1" and nb: "numbound0 e"
+    by simp_all
   fix a
   from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
-  proof(clarsimp)
-    fix x assume "x < (- Inum (a#bs) e)"
+  proof clarsimp
+    fix x
+    assume "x < (- Inum (a#bs) e)"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
-    show "x + Inum (x#bs) e < 0" by simp
+    show "x + Inum (x # bs) e < 0"
+      by simp
   qed
   then show ?case by auto
 next
-  case (6 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (6 c e)
+  then have c1: "c = 1" and nb: "numbound0 e"
+    by simp_all
   fix a
   from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
-  proof(clarsimp)
-    fix x assume "x < (- Inum (a#bs) e)"
+  proof clarsimp
+    fix x
+    assume "x < (- Inum (a#bs) e)"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "x + Inum (x#bs) e \<le> 0" by simp
   qed
   then show ?case by auto
 next
-  case (7 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (7 c e)
+  then have c1: "c = 1" and nb: "numbound0 e"
+    by simp_all
   fix a
   from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
-  proof(clarsimp)
-    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
+  proof clarsimp
+    fix x
+    assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
-    show "False" by simp
+    show False by simp
   qed
   then show ?case by auto
 next
-  case (8 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (8 c e)
+  then have c1: "c = 1" and nb: "numbound0 e"
+    by simp_all
   fix a
   from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
-  proof(clarsimp)
-    fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0"
+  proof clarsimp
+    fix x
+    assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e \<ge> 0"
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
-    show "False" by simp
+    show False by simp
   qed
   then show ?case by auto
 qed auto
 
 lemma minusinf_repeats:
-  assumes d: "d_\<delta> p d" and linp: "iszlfm p"
-  shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)"
+  assumes d: "d_\<delta> p d"
+    and linp: "iszlfm p"
+  shows "Ifm bbs ((x - k * d) # bs) (minusinf p) = Ifm bbs (x # bs) (minusinf p)"
   using linp d
 proof (induct p rule: iszlfm.induct)
   case (9 i c e)
-  then have nbe: "numbound0 e" and id: "i dvd d" by simp_all
-  then have "\<exists>k. d=i*k" by (simp add: dvd_def)
-  then obtain "di" where di_def: "d=i*di" by blast
+  then have nbe: "numbound0 e" and id: "i dvd d"
+    by simp_all
+  then have "\<exists>k. d = i * k"
+    by (simp add: dvd_def)
+  then obtain "di" where di_def: "d = i * di"
+    by blast
   show ?case
   proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
       rule iffI)
-    assume "i dvd c * x - c*(k*d) + Inum (x # bs) e"
+    assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
       (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
-    then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
-    then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
+    then have "\<exists>l::int. ?rt = i * l"
+      by (simp add: dvd_def)
+    then have "\<exists>l::int. c*x+ ?I x e = i * l + c * (k * i * di)"
       by (simp add: algebra_simps di_def)
-    then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
+    then have "\<exists>l::int. c*x+ ?I x e = i*(l + c * k * di)"
       by (simp add: algebra_simps)
-    then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
-    then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
+    then have "\<exists>l::int. c * x + ?I x e = i * l"
+      by blast
+    then show "i dvd c * x + Inum (x # bs) e"
+      by (simp add: dvd_def)
   next
-    assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
-    then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
-    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
-    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
-    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
-    then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast
-    then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
+    assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
+    then have "\<exists>l::int. c * x + ?e = i * l"
+      by (simp add: dvd_def)
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
+      by simp
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
+      by (simp add: di_def)
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
+      by (simp add: algebra_simps)
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
+      by blast
+    then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
+      by (simp add: dvd_def)
   qed
 next
   case (10 i c e)
-  then have nbe: "numbound0 e"  and id: "i dvd d" by simp_all
-  then have "\<exists>k. d=i*k" by (simp add: dvd_def)
-  then obtain "di" where di_def: "d=i*di" by blast
+  then have nbe: "numbound0 e" and id: "i dvd d"
+    by simp_all
+  then have "\<exists>k. d = i * k"
+    by (simp add: dvd_def)
+  then obtain di where di_def: "d = i * di"
+    by blast
   show ?case
-  proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
-    assume "i dvd c * x - c*(k*d) + Inum (x # bs) e"
+  proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
+    assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
       (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
-    then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
-    then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
+    then have "\<exists>l::int. ?rt = i * l"
+      by (simp add: dvd_def)
+    then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
       by (simp add: algebra_simps di_def)
-    then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
+    then have "\<exists>l::int. c * x+ ?I x e = i * (l + c * k * di)"
       by (simp add: algebra_simps)
-    then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
-    then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
+    then have "\<exists>l::int. c * x + ?I x e = i * l"
+      by blast
+    then show "i dvd c * x + Inum (x # bs) e"
+      by (simp add: dvd_def)
   next
-    assume
-      "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
-    then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
-    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
-    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
-    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
-    then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l"
+    assume "i dvd c * x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
+    then have "\<exists>l::int. c * x + ?e = i * l"
+      by (simp add: dvd_def)
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
+      by simp
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
+      by (simp add: di_def)
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
+      by (simp add: algebra_simps)
+    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
       by blast
-    then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
+    then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
+      by (simp add: dvd_def)
   qed
 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
 
@@ -1542,7 +1580,7 @@
 
 lemma mirror:
   assumes lp: "iszlfm p"
-  shows "Ifm bbs (x#bs) (mirror p) = Ifm bbs ((- x)#bs) p"
+  shows "Ifm bbs (x # bs) (mirror p) = Ifm bbs ((- x) # bs) p"
   using lp
 proof (induct p rule: iszlfm.induct)
   case (9 j c e)
@@ -1616,22 +1654,27 @@
 qed (auto simp add: lcm_pos_int)
 
 lemma a_\<beta>:
-  assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0"
+  assumes linp: "iszlfm p"
+    and d: "d_\<beta> p l"
+    and lp: "l > 0"
   shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)"
   using linp d
 proof (induct p rule: iszlfm.induct)
   case (5 c e)
-  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
-  from cp have cnz: "c \<noteq> 0" by simp
-  have "c div c\<le> l div c"
+  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
+  from cp have cnz: "c \<noteq> 0"
+    by simp
+  have "c div c \<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
-    by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
-    by simp
+  have "c * (l div c) = c * (l div c) + l mod c"
+    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
+  then have cl: "c * (l div c) =l"
+    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
   then have "(l*x + (l div c) * Inum (x # bs) e < 0) =
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
     by simp
@@ -1643,19 +1686,23 @@
     using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
 next
   case (6 c e)
-  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
-  from cp have cnz: "c \<noteq> 0" by simp
+  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
+  from cp have cnz: "c \<noteq> 0"
+    by simp
   have "c div c\<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
+  have "c * (l div c) = c* (l div c) + l mod c"
+    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
+  then have cl: "c * (l div c) = l"
+    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+  then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
+      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
     by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
-    by simp
-  then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
-      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp
   also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)"
     by (simp add: algebra_simps)
   also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
@@ -1664,10 +1711,68 @@
     using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
 next
   case (7 c e)
-  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
-  from cp have cnz: "c \<noteq> 0" by simp
-  have "c div c\<le> l div c"
+  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
+  from cp have cnz: "c \<noteq> 0"
+    by simp
+  have "c div c \<le> l div c"
+    by (simp add: zdiv_mono1[OF clel cp])
+  then have ldcp:"0 < l div c"
+    by (simp add: div_self[OF cnz])
+  have "c * (l div c) = c* (l div c) + l mod c"
+    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
+  then have cl:"c * (l div c) = l"
+    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+  then have "(l * x + (l div c) * Inum (x # bs) e > 0) =
+      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
+    by simp
+  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)"
+    by (simp add: algebra_simps)
+  also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
+    using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
+    by simp
+  finally show ?case
+    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
+    by simp
+next
+  case (8 c e)
+  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
+  from cp have cnz: "c \<noteq> 0"
+    by simp
+  have "c div c \<le> l div c"
+    by (simp add: zdiv_mono1[OF clel cp])
+  then have ldcp: "0 < l div c"
+    by (simp add: div_self[OF cnz])
+  have "c * (l div c) = c* (l div c) + l mod c"
+    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
+  then have cl: "c * (l div c) =l"
+    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    by simp
+  then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
+      ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
+    by simp
+  also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
+    by (simp add: algebra_simps)
+  also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)"
+    using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"]
+    by simp
+  finally show ?case
+    using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]
+    by simp
+next
+  case (3 c e)
+  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
+  from cp have cnz: "c \<noteq> 0"
+    by simp
+  have "c div c \<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
@@ -1675,105 +1780,50 @@
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  then have "(l*x + (l div c)* Inum (x # bs) e > 0) =
-      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp
-  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)"
-    by (simp add: algebra_simps)
-  also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
-    using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
-  finally show ?case
-    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
-next
-  case (8 c e)
-  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
-  from cp have cnz: "c \<noteq> 0" by simp
-  have "c div c\<le> l div c"
-    by (simp add: zdiv_mono1[OF clel cp])
-  then have ldcp:"0 < l div c"
-    by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
-    by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have "(l * x + (l div c) * Inum (x # bs) e = 0) =
+      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
     by simp
-  then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
-      ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" by simp
-  also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
-    by (simp add: algebra_simps)
-  also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)"
-    using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp
-  finally show ?case
-    using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by simp
-next
-  case (3 c e)
-  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
-  from cp have cnz: "c \<noteq> 0" by simp
-  have "c div c\<le> l div c"
-    by (simp add: zdiv_mono1[OF clel cp])
-  then have ldcp:"0 < l div c"
-    by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
-    by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
-    by simp
-  then have "(l * x + (l div c) * Inum (x # bs) e = 0) =
-      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp
   also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)"
     by (simp add: algebra_simps)
   also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
-    using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
+    using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
+    by simp
   finally show ?case
-    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
+    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
+    by simp
 next
   case (4 c e)
-  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
-  from cp have cnz: "c \<noteq> 0" by simp
-  have "c div c\<le> l div c"
+  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
+  from cp have cnz: "c \<noteq> 0"
+    by simp
+  have "c div c \<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
-    by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  have "c * (l div c) = c* (l div c) + l mod c"
+    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
+  then have cl: "c * (l div c) = l"
+    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+  then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) \<longleftrightarrow>
+      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
     by simp
-  then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
-      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" by simp
-  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)"
+  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0"
     by (simp add: algebra_simps)
-  also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)"
-    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
+  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<noteq> 0"
+    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
+    by simp
   finally show ?case
-    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
+    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
+    by simp
 next
   case (9 j c e)
-  then have cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
-  from cp have cnz: "c \<noteq> 0" by simp
-  have "c div c\<le> l div c"
-    by (simp add: zdiv_mono1[OF clel cp])
-  then have ldcp:"0 < l div c"
-    by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
-    by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
-    by simp
-  then have "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) =
-    (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
-  also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)"
-    by (simp add: algebra_simps)
-  also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)"
-    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
-    by simp
-  also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp
-  finally show ?case
-    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ]
-    by (simp add: dvd_def)
-next
-  case (10 j c e)
-  then have cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
-  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
+  then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
@@ -1781,25 +1831,70 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-  then have cl:"c * (l div c) =l"
+  then have cl: "c * (l div c) = l"
     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
-  then have "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e =
-      ((l div c) * j) * k) = (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
+  then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
+      (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
+    by simp
+  also have "\<dots> \<longleftrightarrow> (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
+    by (simp add: algebra_simps)
+  also
+  fix k
+  have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
+    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
+    by simp
+  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
+    by simp
+  finally show ?case
+    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]
+      be mult_strict_mono[OF ldcp jp ldcp ]
+    by (simp add: dvd_def)
+next
+  case (10 j c e)
+  then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l"
+    by simp_all
+  from lp cp have clel: "c \<le> l"
+    by (simp add: zdvd_imp_le [OF d' lp])
+  from cp have cnz: "c \<noteq> 0"
     by simp
-  also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps)
-  also fix k have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)"
-    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
-  also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp
-  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be  mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def)
+  have "c div c \<le> l div c"
+    by (simp add: zdiv_mono1[OF clel cp])
+  then have ldcp: "0 < l div c"
+    by (simp add: div_self[OF cnz])
+  have "c * (l div c) = c* (l div c) + l mod c"
+    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
+  then have cl:"c * (l div c) =l"
+    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    by simp
+  then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
+      (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
+    by simp
+  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
+    by (simp add: algebra_simps)
+  also
+  fix k
+  have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
+    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
+    by simp
+  also have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
+    by simp
+  finally show ?case
+    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
+      mult_strict_mono[OF ldcp jp ldcp ]
+    by (simp add: dvd_def)
 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
 
-lemma a_\<beta>_ex: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l>0"
-  shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists>(x::int). Ifm bbs (x#bs) p)"
-  (is "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>x. ?P' x)")
+lemma a_\<beta>_ex:
+  assumes linp: "iszlfm p"
+    and d: "d_\<beta> p l"
+    and lp: "l > 0"
+  shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) \<longleftrightarrow> (\<exists>x::int. Ifm bbs (x#bs) p)"
+  (is "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>x. ?P' x)")
 proof-
-  have "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>(x::int). ?P (l*x))"
+  have "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>(x::int). ?P (l*x))"
     using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
-  also have "\<dots> = (\<exists>(x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
+  also have "\<dots> = (\<exists>x::int. ?P' x)"
+    using a_\<beta>[OF linp d lp] by simp
   finally show ?thesis  .
 qed
 
@@ -2157,7 +2252,7 @@
     lq: "iszlfm ?q" and
     Bn: "\<forall>b\<in> set ?B. numbound0 b" by auto
   from zlin_qfree[OF lq] have qfq: "qfree ?q" .
-  from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq".
+  from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" .
   have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp
   then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
     by (auto simp only: subst0_bound0[OF qfmq])
@@ -2174,10 +2269,13 @@
     by auto
   from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
   from mdb qdb
-  have mdqdb: "bound0 (disj ?md ?qd)" unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all
+  have mdqdb: "bound0 (disj ?md ?qd)"
+    unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all
   from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
-  have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))" by auto
-  also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))" by simp
+  have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))"
+    by auto
+  also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))"
+    by simp
   also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?mq ) \<or>
       (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
     by (simp only: Inum.simps) blast
@@ -2195,27 +2293,38 @@
   also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
     by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"])
       (auto simp add: split_def)
-  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp
-  also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj)
-  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb])
+  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)"
+    by simp
+  also have "\<dots> = (?I i (disj ?md ?qd))"
+    by (simp add: disj)
+  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))"
+    by (simp only: decr [OF mdqdb])
   finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" .
-  { assume mdT: "?md = T"
-    then have cT:"cooper p = T"
+  {
+    assume mdT: "?md = T"
+    then have cT: "cooper p = T"
       by (simp only: cooper_def unit_def split_def Let_def if_True) simp
-    from mdT have lhs:"?lhs" using mdqd by simp
-    from mdT have "?rhs" by (simp add: cooper_def unit_def split_def)
-    with lhs cT have ?thesis by simp }
+    from mdT have lhs: "?lhs"
+      using mdqd by simp
+    from mdT have "?rhs"
+      by (simp add: cooper_def unit_def split_def)
+    with lhs cT have ?thesis by simp
+  }
   moreover
-  { assume mdT: "?md \<noteq> T" then have "cooper p = decr (disj ?md ?qd)"
+  {
+    assume mdT: "?md \<noteq> T"
+    then have "cooper p = decr (disj ?md ?qd)"
       by (simp only: cooper_def unit_def split_def Let_def if_False)
-    with mdqd2 decr_qf[OF mdqdb] have ?thesis by simp }
+    with mdqd2 decr_qf[OF mdqdb] have ?thesis
+      by simp
+  }
   ultimately show ?thesis by blast
 qed
 
-definition pa :: "fm \<Rightarrow> fm" where
-  "pa p = qelim (prep p) cooper"
+definition pa :: "fm \<Rightarrow> fm"
+  where "pa p = qelim (prep p) cooper"
 
-theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
+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"
@@ -2436,7 +2545,7 @@
   by cooper
 
 lemma "\<not> (\<forall>(x::int).
-    (2 dvd x \<longleftrightarrow> (ALL(y::int). x \<noteq> 2*y+1) \<or>
+    (2 dvd x \<longleftrightarrow> (\<forall>(y::int). x \<noteq> 2*y+1) \<or>
       (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17) \<longrightarrow> 0 < x \<or> (\<not> 3 dvd x \<and> x + 8 = 0)))"
   by cooper