# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1435075000 -3600
# Node ID b28677f33eaa7394367a54ad09622e99c89203f1
# Parent  24af00b010cf6a8c793672eb3276ddb79ccb9c16# Parent  85aed595feb486343a43cf72e4c009a9cfaaae0e
Merge

diff -r 24af00b010cf -r b28677f33eaa src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Jun 23 16:55:28 2015 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Jun 23 16:56:40 2015 +0100
@@ -502,7 +502,7 @@
   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
 
 
-(* A size for fm *)
+text \<open>A size for fm.\<close>
 fun fmsize :: "fm \<Rightarrow> nat"
 where
   "fmsize (NOT p) = 1 + fmsize p"
@@ -514,11 +514,10 @@
 | "fmsize (A p) = 4+ fmsize p"
 | "fmsize p = 1"
 
-(* several lemmas about fmsize *)
 lemma fmsize_pos[termination_simp]: "fmsize p > 0"
   by (induct p rule: fmsize.induct) simp_all
 
-  (* Semantics of formulae (fm) *)
+text \<open>Semantics of formulae (fm).\<close>
 primrec Ifm ::"'a::linordered_field list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
 where
   "Ifm vs bs T = True"
@@ -599,7 +598,7 @@
 lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)"
   by (unfold iff_def, cases "p = q", simp, cases "p = NOT q", simp) (cases "NOT p= q", auto)
 
-(* Quantifier freeness *)
+text \<open>Quantifier freeness.\<close>
 fun qfree:: "fm \<Rightarrow> bool"
 where
   "qfree (E p) = False"
@@ -611,7 +610,7 @@
 | "qfree (Iff p q) = (qfree p \<and> qfree q)"
 | "qfree p = True"
 
-(* Boundedness and substitution *)
+text \<open>Boundedness and substitution.\<close>
 primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool"
 where
   "boundslt n T = True"
@@ -628,7 +627,7 @@
 | "boundslt n (E p) = boundslt (Suc n) p"
 | "boundslt n (A p) = boundslt (Suc n) p"
 
-fun bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
+fun bound0:: "fm \<Rightarrow> bool"  -- \<open>a Formula is independent of Bound 0\<close>
 where
   "bound0 T = True"
 | "bound0 F = True"
@@ -649,7 +648,7 @@
   using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
   by (induct p rule: bound0.induct) auto
 
-primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *)
+primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool"  -- \<open>a Formula is independent of Bound n\<close>
 where
   "bound m T = True"
 | "bound m F = True"
@@ -673,23 +672,23 @@
   using bnd nb le tmbound_I[where bs=bs and vs = vs]
 proof (induct p arbitrary: bs n rule: fm.induct)
   case (E p bs n)
-  {
-    fix y
+  have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" for y
+  proof -
     from E have bnd: "boundslt (length (y#bs)) p"
       and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
-    from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .
-  }
+    from E.hyps[OF bnd nb le tmbound_I] show ?thesis .
+  qed
   then show ?case by simp
 next
   case (A p bs n)
-  {
-    fix y
+  have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" for y
+  proof -
     from A have bnd: "boundslt (length (y#bs)) p"
       and nb: "bound (Suc n) p"
       and le: "Suc n \<le> length (y#bs)"
       by simp_all
-    from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .
-  }
+    from A.hyps[OF bnd nb le tmbound_I] show ?thesis .
+  qed
   then show ?case by simp
 qed auto
 
@@ -1898,42 +1897,40 @@
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x > - ?e"
-        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
+  next
+    case 2
+    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using pos_divide_less_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
+      then show ?thesis
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x < - ?e"
-        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using neg_divide_less_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0" by simp
-      then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
+      then show ?thesis
         using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
 next
   case (4 c e)
   then have nbe: "tmbound0 e"
@@ -1944,42 +1941,40 @@
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x > - ?e"
-        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using eqs by auto
+  next
+    case 2
+    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using pos_divide_less_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
+      then show ?thesis
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x < - ?e"
-        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using neg_divide_less_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
-      then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
+      then show ?thesis
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
 next
   case (5 c e)
   then have nbe: "tmbound0 e"
@@ -1992,42 +1987,40 @@
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x > - ?e"
-        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using eqs by auto
+  next
+    case 2
+    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using pos_divide_less_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x < - ?e"
-        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs by auto
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using neg_divide_less_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
-      then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
-        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+      then show ?thesis
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> by auto
+    qed
+    then show ?thesis by auto
+  qed
 next
   case (6 c e)
   then have nbe: "tmbound0 e"
@@ -2040,42 +2033,40 @@
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x > - ?e"
-        using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using eqs by auto
+  next
+    case 2
+    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using pos_divide_less_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x > -?e / ?c"
-      then have "?c * x < - ?e"
-        using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs by auto
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
+      if "x > -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using neg_divide_less_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
-      then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> eqs by auto
+    qed
+    then show ?thesis by auto
+  qed
 qed auto
 
 lemma minusinf_nb: "islin p \<Longrightarrow> bound0 (minusinf p)"
@@ -2227,7 +2218,8 @@
   assumes lp: "islin p"
     and noS: "\<forall>t. l < t \<and> t< u \<longrightarrow> t \<notin> (\<lambda>(c,t). - Itm vs (x#bs) t / Ipoly vs c) ` set (uset p)"
       (is "\<forall>t. _ \<and> _ \<longrightarrow> t \<notin> (\<lambda>(c,t). - ?Nt x t / ?N c) ` ?U p")
-    and lx: "l < x" and xu:"x < u" and px:" Ifm vs (x#bs) p"
+    and lx: "l < x" and xu: "x < u"
+    and px: "Ifm vs (x # bs) p"
     and ly: "l < y" and yu: "y < u"
   shows "Ifm vs (y#bs) p"
   using lp px noS
@@ -2244,29 +2236,27 @@
     by auto
   have ccs: "?N c = 0 \<or> ?N c < 0 \<or> ?N c > 0"
     by dlo
-  moreover
-  {
-    assume "?N c = 0"
-    then have ?case
+  consider "?N c = 0" | "?N c > 0" | "?N c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
-  }
-  moreover
-  {
-    assume c: "?N c > 0"
-    from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"]
+  next
+    case 2
+    from px pos_less_divide_eq[OF 2, where a="x" and b="-?Nt x s"]
     have px': "x < - ?Nt x s / ?N c"
       by (auto simp add: not_less field_simps)
-    {
+    from ycs show ?thesis
+    proof
       assume y: "y < - ?Nt x s / ?N c"
       then have "y * ?N c < - ?Nt x s"
-        by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: pos_less_divide_eq[OF 2, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
-      then have ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
+      then show ?thesis using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
         by simp
-    }
-    moreover
-    {
+    next
       assume y: "y > -?Nt x s / ?N c"
       with yu have eu: "u > - ?Nt x s / ?N c"
         by auto
@@ -2274,28 +2264,23 @@
         by (cases "- ?Nt x s / ?N c > l") auto
       with lx px' have False
         by simp
-      then have ?case ..
-    }
-    ultimately have ?case
-      using ycs by blast
-  }
-  moreover
-  {
-    assume c: "?N c < 0"
-    from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"]
+      then show ?thesis ..
+    qed
+  next
+    case 3
+    from px neg_divide_less_eq[OF 3, where a="x" and b="-?Nt x s"]
     have px': "x > - ?Nt x s / ?N c"
       by (auto simp add: not_less field_simps)
-    {
+    from ycs show ?thesis
+    proof
       assume y: "y > - ?Nt x s / ?N c"
       then have "y * ?N c < - ?Nt x s"
-        by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: neg_divide_less_eq[OF 3, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
-      then have ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
+      then show ?thesis using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
         by simp
-    }
-    moreover
-    {
+    next
       assume y: "y < -?Nt x s / ?N c"
       with ly have eu: "l < - ?Nt x s / ?N c"
         by auto
@@ -2303,13 +2288,9 @@
         by (cases "- ?Nt x s / ?N c < u") auto
       with xu px' have False
         by simp
-      then have ?case ..
-    }
-    ultimately have ?case
-      using ycs by blast
-  }
-  ultimately show ?case
-    by blast
+      then show ?thesis ..
+    qed
+  qed
 next
   case (6 c s)
   from "6.prems"
@@ -2322,29 +2303,27 @@
   then have ycs: "y < - ?Nt x s / ?N c \<or> y > -?Nt x s / ?N c"
     by auto
   have ccs: "?N c = 0 \<or> ?N c < 0 \<or> ?N c > 0" by dlo
-  moreover
-  {
-    assume "?N c = 0"
-    then have ?case
+  consider "?N c = 0" | "?N c > 0" | "?N c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
-  }
-  moreover
-  {
-    assume c: "?N c > 0"
-    from px pos_le_divide_eq[OF c, where a="x" and b="-?Nt x s"]
+  next
+    case 2
+    from px pos_le_divide_eq[OF 2, where a="x" and b="-?Nt x s"]
     have px': "x \<le> - ?Nt x s / ?N c"
       by (simp add: not_less field_simps)
-    {
+    from ycs show ?thesis
+    proof
       assume y: "y < - ?Nt x s / ?N c"
       then have "y * ?N c < - ?Nt x s"
-        by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: pos_less_divide_eq[OF 2, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
-      then have ?case
+      then show ?thesis
         using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp
-    }
-    moreover
-    {
+    next
       assume y: "y > -?Nt x s / ?N c"
       with yu have eu: "u > - ?Nt x s / ?N c"
         by auto
@@ -2352,41 +2331,32 @@
         by (cases "- ?Nt x s / ?N c > l") auto
       with lx px' have False
         by simp
-      then have ?case ..
-    }
-    ultimately have ?case
-      using ycs by blast
-  }
-  moreover
-  {
-    assume c: "?N c < 0"
-    from px neg_divide_le_eq[OF c, where a="x" and b="-?Nt x s"]
+      then show ?thesis ..
+    qed
+  next
+    case 3
+    from px neg_divide_le_eq[OF 3, where a="x" and b="-?Nt x s"]
     have px': "x >= - ?Nt x s / ?N c"
       by (simp add: field_simps)
-    {
+    from ycs show ?thesis
+    proof
       assume y: "y > - ?Nt x s / ?N c"
       then have "y * ?N c < - ?Nt x s"
-        by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: neg_divide_less_eq[OF 3, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
-      then have ?case
+      then show ?thesis
         using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp
-    }
-    moreover
-    {
+    next
       assume y: "y < -?Nt x s / ?N c"
       with ly have eu: "l < - ?Nt x s / ?N c"
         by auto
       with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u"
         by (cases "- ?Nt x s / ?N c < u") auto
       with xu px' have False by simp
-      then have ?case ..
-    }
-    ultimately have ?case
-      using ycs by blast
-  }
-  ultimately show ?case
-    by blast
+      then show ?thesis ..
+    qed
+  qed
 next
   case (3 c s)
   from "3.prems"
@@ -2398,75 +2368,65 @@
     by simp
   then have ycs: "y < - ?Nt x s / ?N c \<or> y > -?Nt x s / ?N c"
     by auto
-  have ccs: "?N c = 0 \<or> ?N c < 0 \<or> ?N c > 0" by dlo
-  moreover
-  {
-    assume "?N c = 0"
-    then have ?case
+  consider "?N c = 0" | "?N c < 0" | "?N c > 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
-  }
-  moreover
-  {
-    assume c: "?N c > 0"
+  next
+    case 2
     then have cnz: "?N c \<noteq> 0"
       by simp
     from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz
     have px': "x = - ?Nt x s / ?N c"
       by (simp add: field_simps)
-    {
+    from ycs show ?thesis
+    proof
       assume y: "y < -?Nt x s / ?N c"
       with ly have eu: "l < - ?Nt x s / ?N c"
         by auto
       with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u"
         by (cases "- ?Nt x s / ?N c < u") auto
       with xu px' have False by simp
-      then have ?case ..
-    }
-    moreover
-    {
+      then show ?thesis ..
+    next
       assume y: "y > -?Nt x s / ?N c"
       with yu have eu: "u > - ?Nt x s / ?N c"
         by auto
       with noS ly yu have th: "- ?Nt x s / ?N c \<le> l"
         by (cases "- ?Nt x s / ?N c > l") auto
       with lx px' have False by simp
-      then have ?case ..
-    }
-    ultimately have ?case
-      using ycs by blast
-  }
-  moreover
-  {
-    assume c: "?N c < 0"
+      then show ?thesis ..
+    qed
+  next
+    case 3
     then have cnz: "?N c \<noteq> 0"
       by simp
     from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz
     have px': "x = - ?Nt x s / ?N c"
       by (simp add: field_simps)
-    {
+    from ycs show ?thesis
+    proof
       assume y: "y < -?Nt x s / ?N c"
       with ly have eu: "l < - ?Nt x s / ?N c"
         by auto
       with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u"
         by (cases "- ?Nt x s / ?N c < u") auto
       with xu px' have False by simp
-      then have ?case ..
-    }
-    moreover
-    {
+      then show ?thesis ..
+    next
       assume y: "y > -?Nt x s / ?N c"
       with yu have eu: "u > - ?Nt x s / ?N c"
         by auto
       with noS ly yu have th: "- ?Nt x s / ?N c \<le> l"
         by (cases "- ?Nt x s / ?N c > l") auto
       with lx px' have False by simp
-      then have ?case ..
-    }
-    ultimately have ?case using ycs by blast
-  }
-  ultimately show ?case by blast
+      then show ?thesis ..
+    qed
+  qed
 next
-    case (4 c s)
+  case (4 c s)
   from "4.prems"
   have lin: "isnpoly c" "c \<noteq> 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s"
     and px: "Ifm vs (x # bs) (NEq (CNP 0 c s))"
@@ -2476,23 +2436,19 @@
     by simp
   then have ycs: "y < - ?Nt x s / ?N c \<or> y > -?Nt x s / ?N c"
     by auto
-  have ccs: "?N c = 0 \<or> ?N c \<noteq> 0" by dlo
-  moreover
-  {
-    assume "?N c = 0"
-    then have ?case
+  show ?case
+  proof (cases "?N c = 0")
+    case True
+    then show ?thesis
       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
-  }
-  moreover
-  {
-    assume c: "?N c \<noteq> 0"
-    from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"]
-    have ?case
+  next
+    case False
+    with yne eq_divide_eq[of "y" "- ?Nt x s" "?N c"]
+    show ?thesis
       by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric])
-  }
-  ultimately show ?case
-    by blast
-qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
+  qed
+qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"]
+  bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
 
 lemma inf_uset:
   assumes lp: "islin p"
@@ -2556,49 +2512,43 @@
     then have xu: "a \<le> ?u"
       using xs by simp
     from finite_set_intervals2[where P="\<lambda>x. ?I x p",OF pa lx xu linM uinM fM lM Mu]
-    have "(\<exists>s\<in> ?M. ?I s p) \<or>
-      (\<exists>t1\<in> ?M. \<exists>t2 \<in> ?M. (\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p)" .
-    moreover {
-      fix u
-      assume um: "u\<in> ?M"
-        and pu: "?I u p"
+    consider u where "u \<in> ?M" "?I u p"
+      | t1 t2 where "t1 \<in> ?M" "t2\<in> ?M" "\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M" "t1 < a" "a < t2" "?I a p"
+      by blast
+    then show ?thesis
+    proof cases
+      case 1
       then have "\<exists>(nu,tu) \<in> ?U. u = - ?Nt a tu / ?N nu"
         by auto
-      then obtain tu nu where tuU: "(nu, tu) \<in> ?U"
-        and tuu:"u= - ?Nt a tu / ?N nu"
+      then obtain tu nu where tuU: "(nu, tu) \<in> ?U" and tuu: "u = - ?Nt a tu / ?N nu"
         by blast
-      from pu tuu have "?I (((- ?Nt a tu / ?N nu) + (- ?Nt a tu / ?N nu)) / 2) p"
-        by simp
-      with tuU have ?thesis by blast
-    }
-    moreover {
-      assume "\<exists>t1\<in> ?M. \<exists>t2 \<in> ?M. (\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p"
-      then obtain t1 t2
-        where t1M: "t1 \<in> ?M"
-          and t2M: "t2\<in> ?M"
-          and noM: "\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M"
-          and t1x: "t1 < a"
-          and xt2: "a < t2"
-          and px: "?I a p"
-        by blast
-      from t1M have "\<exists>(t1n, t1u) \<in> ?U. t1 = - ?Nt a t1u / ?N t1n"
-        by auto
+      have "?I (((- ?Nt a tu / ?N nu) + (- ?Nt a tu / ?N nu)) / 2) p"
+        using \<open>?I u p\<close> tuu by simp
+      with tuU show ?thesis by blast
+    next
+      case 2
+      have "\<exists>(t1n, t1u) \<in> ?U. t1 = - ?Nt a t1u / ?N t1n"
+        using \<open>t1 \<in> ?M\<close> by auto
       then obtain t1u t1n where t1uU: "(t1n, t1u) \<in> ?U"
         and t1u: "t1 = - ?Nt a t1u / ?N t1n"
         by blast
-      from t2M have "\<exists>(t2n, t2u) \<in> ?U. t2 = - ?Nt a t2u / ?N t2n"
-        by auto
+      have "\<exists>(t2n, t2u) \<in> ?U. t2 = - ?Nt a t2u / ?N t2n"
+        using \<open>t2 \<in> ?M\<close> by auto
       then obtain t2u t2n where t2uU: "(t2n, t2u) \<in> ?U"
         and t2u: "t2 = - ?Nt a t2u / ?N t2n"
         by blast
-      from t1x xt2 have t1t2: "t1 < t2" by simp
+      have "t1 < t2" 
+        using \<open>t1 < a\<close> \<open>a < t2\<close> by simp
       let ?u = "(t1 + t2) / 2"
-      from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2"
-        by auto
-      from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" .
-      with t1uU t2uU t1u t2u have ?thesis by blast
-    }
-    ultimately show ?thesis by blast
+      have "t1 < ?u"
+        using less_half_sum [OF \<open>t1 < t2\<close>] by auto
+      have "?u < t2"
+        using gt_half_sum [OF \<open>t1 < t2\<close>] by auto
+      have "?I ?u p"
+        using lp \<open>\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M\<close> \<open>t1 < a\<close> \<open>a < t2\<close> \<open>?I a p\<close> \<open>t1 < ?u\<close> \<open>?u < t2\<close>
+        by (rule lin_dense)
+      with t1uU t2uU t1u t2u show ?thesis by blast
+    qed
   qed
   then obtain l n s  m
     where lnU: "(n, l) \<in> ?U"
@@ -2614,7 +2564,8 @@
   with lnU smU show ?thesis by auto
 qed
 
-(* The Ferrante - Rackoff Theorem *)
+
+section \<open>The Ferrante - Rackoff Theorem\<close>
 
 theorem fr_eq:
   assumes lp: "islin p"
@@ -2623,38 +2574,37 @@
      Ifm vs (x#bs) (plusinf p) \<or>
      (\<exists>(n, t) \<in> set (uset p). \<exists>(m, s) \<in> set (uset p).
        Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) / 2)#bs) p))"
-  (is "(\<exists>x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
+  (is "(\<exists>x. ?I x p) \<longleftrightarrow> ?M \<or> ?P \<or> ?F" is "?E \<longleftrightarrow> ?D")
 proof
-  assume px: "\<exists>x. ?I x p"
-  have "?M \<or> ?P \<or> (\<not> ?M \<and> \<not> ?P)"
-    by blast
-  moreover {
-    assume "?M \<or> ?P"
-    then have "?D" by blast
-  }
-  moreover {
-    assume nmi: "\<not> ?M"
-      and npi: "\<not> ?P"
-    from inf_uset[OF lp nmi npi] have ?F
-      using px by blast
-    then have ?D by blast
-  }
-  ultimately show ?D by blast
-next
-  assume ?D
-  moreover {
-    assume m: ?M
-    from minusinf_ex[OF lp m] have ?E .
-  }
-  moreover {
-    assume p: ?P
-    from plusinf_ex[OF lp p] have ?E .
-  }
-  moreover {
-    assume f: ?F
-    then have ?E by blast
-  }
-  ultimately show ?E by blast
+  show ?D if ?E
+  proof -
+    consider "?M \<or> ?P" | "\<not> ?M" "\<not> ?P" by blast
+    then show ?thesis
+    proof cases
+      case 1
+      then show ?thesis by blast
+    next
+      case 2
+      from inf_uset[OF lp 2] have ?F
+        using \<open>?E\<close> by blast
+      then show ?thesis by blast
+    qed
+  qed
+  show ?E if ?D
+  proof -
+    from that consider ?M | ?P | ?F by blast
+    then show ?thesis
+    proof cases
+      case 1
+      from minusinf_ex[OF lp this] show ?thesis .
+    next
+      case 2
+      from plusinf_ex[OF lp this] show ?thesis .
+    next
+      case 3
+      then show ?thesis by blast
+    qed
+  qed
 qed
 
 
@@ -2701,61 +2651,51 @@
   let ?r = "?Nt x r"
   from lp have lin:"isnpoly a" "a \<noteq> 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r"
     by simp_all
-  note r= tmbound0_I[OF lin(3), of vs _ bs x]
-  have cd_cs: "?c * ?d \<noteq> 0 \<or> (?c = 0 \<and> ?d = 0) \<or> (?c = 0 \<and> ?d \<noteq> 0) \<or> (?c \<noteq> 0 \<and> ?d = 0)"
-    by auto
-  moreover
-  {
-    assume c: "?c = 0"
-      and d: "?d=0"
-    then have ?thesis
+  note r = tmbound0_I[OF lin(3), of vs _ bs x]
+  consider "?c = 0" "?d = 0" | "?c = 0" "?d \<noteq> 0" | "?c \<noteq> 0" "?d = 0" | "?c \<noteq> 0" "?d \<noteq> 0"
+    by blast
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis
       by (simp add: r[of 0] msubsteq_def Let_def evaldjf_ex)
-  }
-  moreover
-  {
-    assume c: "?c = 0"
-      and d: "?d\<noteq>0"
-    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)"
+  next
+    case 2
+    then have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)"
       by simp
     have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r = 0"
       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
     also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0"
-      using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
+      using \<open>?d \<noteq> 0\<close> mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0"
       by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
     also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0"
-      using d by simp
-    finally have ?thesis
-      using c d
+      using \<open>?d \<noteq> 0\<close> by simp
+    finally show ?thesis
+      using 2
       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubsteq_def Let_def evaldjf_ex)
-  }
-  moreover
-  {
-    assume c: "?c \<noteq> 0"
-      and d: "?d = 0"
-    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2 * ?c)"
+  next
+    case 3
+    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2 * ?c)"
       by simp
     have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r = 0"
       by (simp add: r[of "- (?t/ (2 * ?c))"])
     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0"
-      using c mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
+      using \<open>?c \<noteq> 0\<close> mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0"
       by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left)
-    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by simp
-    finally have ?thesis using c d
+    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using \<open>?c \<noteq> 0\<close> by simp
+    finally show ?thesis using 3
       by (simp add: r[of "- (?t/ (2 * ?c))"] msubsteq_def Let_def evaldjf_ex)
-  }
-  moreover
-  {
-    assume c: "?c \<noteq> 0"
-      and d: "?d \<noteq> 0"
+  next
+    case 4
     then have dc: "?c * ?d * 2 \<noteq> 0"
       by simp
-    from add_frac_eq[OF c d, of "- ?t" "- ?s"]
+    from add_frac_eq[OF 4, of "- ?t" "- ?s"]
     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)"
       by (simp add: field_simps)
     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Eq (CNP 0 a r))"
@@ -2763,17 +2703,15 @@
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r = 0"
       by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) = 0"
-      using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0]
+      using 4 mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
-      using nonzero_mult_divide_cancel_left [OF dc] c d
+      using nonzero_mult_divide_cancel_left [OF dc] 4
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally  have ?thesis using c d
+    finally show ?thesis using 4
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
           msubsteq_def Let_def evaldjf_ex field_simps)
-  }
-  ultimately show ?thesis
-    by blast
+  qed
 qed
 
 
@@ -2819,61 +2757,51 @@
   from lp have lin:"isnpoly a" "a \<noteq> 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r"
     by simp_all
   note r = tmbound0_I[OF lin(3), of vs _ bs x]
-  have cd_cs: "?c * ?d \<noteq> 0 \<or> (?c = 0 \<and> ?d = 0) \<or> (?c = 0 \<and> ?d \<noteq> 0) \<or> (?c \<noteq> 0 \<and> ?d = 0)"
-    by auto
-  moreover
-  {
-    assume c: "?c = 0"
-      and d: "?d=0"
-    then have ?thesis
+  consider "?c = 0" "?d = 0" | "?c = 0" "?d \<noteq> 0" | "?c \<noteq> 0" "?d = 0" | "?c \<noteq> 0" "?d \<noteq> 0"
+    by blast
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis
       by (simp add: r[of 0] msubstneq_def Let_def evaldjf_ex)
-  }
-  moreover
-  {
-    assume c: "?c = 0"
-      and d: "?d\<noteq>0"
-    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2 * ?d)"
+  next
+    case 2
+    from \<open>?c = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2 * ?d)"
       by simp
     have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r \<noteq> 0"
       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
     also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0"
-      using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
+      using \<open>?d \<noteq> 0\<close> mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
       by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
     also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0"
-      using d by simp
-    finally have ?thesis
-      using c d
+      using \<open>?d \<noteq> 0\<close> by simp
+    finally show ?thesis
+      using 2
       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubstneq_def Let_def evaldjf_ex)
-  }
-  moreover
-  {
-    assume c: "?c \<noteq> 0"
-      and d: "?d=0"
-    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)"
+  next
+    case 3
+    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)"
       by simp
     have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r \<noteq> 0"
       by (simp add: r[of "- (?t/ (2 * ?c))"])
     also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0"
-      using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
+      using \<open>?c \<noteq> 0\<close> mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
       by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
     also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0"
-      using c by simp
-    finally have ?thesis
-      using c d by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
-  }
-  moreover
-  {
-    assume c: "?c \<noteq> 0"
-      and d: "?d \<noteq> 0"
+      using \<open>?c \<noteq> 0\<close> by simp
+    finally show ?thesis
+      using 3 by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
+  next
+    case 4
     then have dc: "?c * ?d *2 \<noteq> 0"
       by simp
-    from add_frac_eq[OF c d, of "- ?t" "- ?s"]
+    from add_frac_eq[OF 4, of "- ?t" "- ?s"]
     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c * ?s )/ (2 * ?c * ?d)"
       by (simp add: field_simps)
     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (NEq (CNP 0 a r))"
@@ -2881,17 +2809,16 @@
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \<noteq> 0"
       by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \<noteq> 0"
-      using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
+      using 4 mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
-      using nonzero_mult_divide_cancel_left[OF dc] c d
+      using nonzero_mult_divide_cancel_left[OF dc] 4
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally have ?thesis
-      using c d
+    finally show ?thesis
+      using 4
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
           msubstneq_def Let_def evaldjf_ex field_simps)
-  }
-  ultimately show ?thesis by blast
+  qed
 qed
 
 definition "msubstlt c t d s a r =
@@ -2946,22 +2873,21 @@
   from lp have lin:"isnpoly a" "a \<noteq> 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r"
     by simp_all
   note r = tmbound0_I[OF lin(3), of vs _ bs x]
-  have cd_cs: "?c * ?d < 0 \<or> ?c * ?d > 0 \<or> (?c = 0 \<and> ?d = 0) \<or> (?c = 0 \<and> ?d < 0) \<or> (?c = 0 \<and> ?d > 0) \<or> (?c < 0 \<and> ?d = 0) \<or> (?c > 0 \<and> ?d = 0)"
-    by auto
-  moreover
-  {
-    assume c: "?c=0" and d: "?d=0"
-    then have ?thesis
+  consider "?c = 0" "?d = 0" | "?c * ?d > 0" | "?c * ?d < 0"
+    | "?c > 0" "?d = 0" | "?c < 0" "?d = 0" | "?c = 0" "?d > 0" | "?c = 0" "?d < 0"
+    by atomize_elim auto
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis
       using nc nd by (simp add: polyneg_norm lt r[of 0] msubstlt_def Let_def evaldjf_ex)
-  }
-  moreover
-  {
-    assume dc: "?c*?d > 0"
-    from dc have dc': "2*?c *?d > 0"
+  next
+    case 2
+    then have dc': "2 *?c * ?d > 0"
       by simp
-    then have c:"?c \<noteq> 0" and d: "?d \<noteq> 0"
+    from 2 have c: "?c \<noteq> 0" and d: "?d \<noteq> 0"
       by auto
-    from dc' have dc'': "\<not> 2*?c *?d < 0" by simp
+    from dc' have dc'': "\<not> 2 * ?c * ?d < 0" by simp
     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)"
       by (simp add: field_simps)
@@ -2976,19 +2902,17 @@
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
       using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally  have ?thesis using dc c d  nc nd dc'
+    finally show ?thesis using 2 c d nc nd dc'
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
           msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
-  }
-  moreover
-  {
-    assume dc: "?c * ?d < 0"
-    from dc have dc': "2*?c *?d < 0"
+  next
+    case 3
+    then have dc': "2 * ?c * ?d < 0"
       by (simp add: mult_less_0_iff field_simps)
-    then have c:"?c \<noteq> 0" and d: "?d \<noteq> 0"
+    from 3 have c: "?c \<noteq> 0" and d: "?d \<noteq> 0"
       by auto
     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
-    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)"
+    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s) / (2 * ?c * ?d)"
       by (simp add: field_simps)
     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2 * ?c * ?d) # bs) (Lt (CNP 0 a r))"
       by (simp only: th)
@@ -3001,109 +2925,100 @@
     also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
       using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally have ?thesis using dc c d nc nd
+    finally show ?thesis using 3 c d nc nd
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
           msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
-  }
-  moreover
-  {
-    assume c: "?c > 0" and d: "?d = 0"
-    from c have c'': "2*?c > 0"
+  next
+    case 4
+    from \<open>?c > 0\<close> have c'': "2 * ?c > 0"
       by (simp add: zero_less_mult_iff)
-    from c have c': "2 * ?c \<noteq> 0"
+    from \<open>?c > 0\<close> have c': "2 * ?c \<noteq> 0"
       by simp
-    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
+    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
       by (simp add: field_simps)
     have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Lt (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r < 0"
       by (simp add: r[of "- (?t / (2 * ?c))"])
     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) < 0"
-      using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
+      using \<open>?c > 0\<close> mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
         order_less_not_sym[OF c'']
       by simp
     also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
-      using nonzero_mult_divide_cancel_left[OF c'] c
+      using nonzero_mult_divide_cancel_left[OF c'] \<open>?c > 0\<close>
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
-    finally have ?thesis using c d nc nd
+    finally show ?thesis using 4 nc nd
       by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
-  }
-  moreover
-  {
-    assume c: "?c < 0" and d: "?d = 0"
-    then have c': "2 * ?c \<noteq> 0"
+  next
+    case 5
+    from \<open>?c < 0\<close> have c': "2 * ?c \<noteq> 0"
       by simp
-    from c have c'': "2 * ?c < 0"
+    from \<open>?c < 0\<close> have c'': "2 * ?c < 0"
       by (simp add: mult_less_0_iff)
-    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
+    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
       by (simp add: field_simps)
     have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r < 0"
       by (simp add: r[of "- (?t / (2*?c))"])
     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) > 0"
-      using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
+      using \<open>?c < 0\<close> order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
         mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0"
-      using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
+      using nonzero_mult_divide_cancel_left[OF c'] \<open>?c < 0\<close> order_less_not_sym[OF c'']
           less_imp_neq[OF c''] c''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally have ?thesis using c d nc nd
+    finally show ?thesis using 5 nc nd
       by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
-  }
-  moreover
-  {
-    assume c: "?c = 0" and d: "?d > 0"
-    from d have d'': "2 * ?d > 0"
+  next
+    case 6
+    from \<open>?d > 0\<close> have d'': "2 * ?d > 0"
       by (simp add: zero_less_mult_iff)
-    from d have d': "2 * ?d \<noteq> 0"
+    from \<open>?d > 0\<close> have d': "2 * ?d \<noteq> 0"
       by simp
-    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2 * ?d)"
+    from \<open>?c = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2 * ?d)"
       by (simp add: field_simps)
     have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r < 0"
       by (simp add: r[of "- (?s / (2 * ?d))"])
     also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d))+ ?r) < 0"
-      using d mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d''
+      using \<open>?d > 0\<close> mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d''
         order_less_not_sym[OF d'']
       by simp
     also have "\<dots> \<longleftrightarrow> - ?a * ?s+  2 * ?d * ?r < 0"
-      using nonzero_mult_divide_cancel_left[OF d'] d
+      using nonzero_mult_divide_cancel_left[OF d'] \<open>?d > 0\<close>
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
-    finally have ?thesis using c d nc nd
+    finally show ?thesis using 6 nc nd
       by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
-  }
-  moreover
-  {
-    assume c: "?c = 0" and d: "?d < 0"
-    then have d': "2 * ?d \<noteq> 0"
+  next
+    case 7
+    from \<open>?d < 0\<close> have d': "2 * ?d \<noteq> 0"
       by simp
-    from d have d'': "2 * ?d < 0"
+    from \<open>?d < 0\<close> have d'': "2 * ?d < 0"
       by (simp add: mult_less_0_iff)
-    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"
+    from \<open>?c = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"
       by (simp add: field_simps)
     have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
       by (simp only: th)
     also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d)) + ?r < 0"
       by (simp add: r[of "- (?s / (2 * ?d))"])
     also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) > 0"
-      using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
+      using \<open>?d < 0\<close> order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
         mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r < 0"
-      using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
+      using nonzero_mult_divide_cancel_left[OF d'] \<open>?d < 0\<close> order_less_not_sym[OF d'']
           less_imp_neq[OF d''] d''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally have ?thesis using c d nc nd
+    finally show ?thesis using 7 nc nd
       by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
-  }
-  ultimately show ?thesis by blast
+  qed
 qed
 
 definition "msubstle c t d s a r =