# HG changeset patch
# User wenzelm
# Date 1435179835 -7200
# Node ID 19c277ea65aeea5a5851bfd70520eda19b812901
# Parent  d9682058f7eea0ae6817e340f67256928c3450a1
tuned proofs -- less digits;

diff -r d9682058f7ee -r 19c277ea65ae src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Jun 24 21:31:29 2015 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Jun 24 23:03:55 2015 +0200
@@ -185,30 +185,30 @@
   consider "x < y" | "x = y" | "x > y" by arith
   then show ?case
   proof cases
-    case 1
+    case xy: 1
     then obtain d where y: "y = d + x"
       by atomize_elim arith
     from 6 have *: "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    from 6 1 y have "isnorm (Pinj d Q2)"
+    from 6 xy y have "isnorm (Pinj d Q2)"
       by (cases d, simp, cases Q2, auto)
     with 6 X0 y * show ?thesis
       by (simp add: mkPinj_cn)
   next
-    case 2
+    case xy: 2
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    with 2 6 Y0 show ?thesis
+    with xy 6 Y0 show ?thesis
       by (simp add: mkPinj_cn)
   next
-    case 3
+    case xy: 3
     then obtain d where x: "x = d + y"
       by atomize_elim arith
     from 6 have *: "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    from 6 3 x have "isnorm (Pinj d P2)"
+    from 6 xy x have "isnorm (Pinj d P2)"
       by (cases d) (simp, cases P2, auto)
-    with 3 6 Y0 * x show ?thesis by (simp add: mkPinj_cn)
+    with xy 6 Y0 * x show ?thesis by (simp add: mkPinj_cn)
   qed
 next
   case (7 x P2 Q2 y R)
@@ -216,26 +216,26 @@
     by atomize_elim arith
   then show ?case
   proof cases
-    case 1
+    case x: 1
     with 7 show ?thesis
       by (auto simp add: norm_Pinj_0_False)
   next
-    case 2
+    case x: 2
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 2 have "isnorm (R \<oplus> P2)"
+    with 7 x have "isnorm (R \<oplus> P2)"
       by simp
-    with 7 2 show ?thesis
+    with 7 x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
   next
-    case 3
+    case x: 3
     with 7 have NR: "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 3 have "isnorm (Pinj (x - 1) P2)"
+    with 7 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 7 3 NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+    with 7 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
       by simp
-    with \<open>isnorm (PX Q2 y R)\<close> 3 show ?thesis
+    with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
   qed
 next
@@ -248,21 +248,21 @@
     with 8 show ?thesis
       by (auto simp add: norm_Pinj_0_False)
   next
-    case 2
+    case x: 2
     with 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 2 have "isnorm (R \<oplus> P2)"
+    with 8 x have "isnorm (R \<oplus> P2)"
       by simp
-    with 8 2 show ?thesis
+    with 8 x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
   next
-    case 3
+    case x: 3
     then obtain d where x: "x = Suc (Suc d)" by atomize_elim arith
     with 8 have NR: "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 8 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 8 3 NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+    with 8 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
       by simp
     with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
@@ -278,54 +278,54 @@
   consider "y < x" | "x = y" | "x < y" by arith
   then show ?case
   proof cases
-    case 1
+    case xy: 1
     then obtain d where x: "x = d + y"
       by atomize_elim arith
     have "isnorm (PX P1 d (Pc 0))"
     proof (cases P1)
       case (PX p1 y p2)
-      with 9 1 x show ?thesis
+      with 9 xy x show ?thesis
         by (cases d) (simp, cases p2, auto)
     next
       case Pc
-      with 9 1 x show ?thesis
+      with 9 xy x show ?thesis
         by (cases d) auto
     next
       case Pinj
-      with 9 1 x show ?thesis
+      with 9 xy x show ?thesis
         by (cases d) auto
     qed
-    with 9 NQ1 NP1 NP2 NQ2 1 x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
+    with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
       by auto
-    with Y0 1 x show ?thesis
+    with Y0 xy x show ?thesis
       by (simp add: mkPX_cn)
   next
-    case 2
+    case xy: 2
     with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
       by auto
-    with 2 Y0 show ?thesis
+    with xy Y0 show ?thesis
       by (simp add: mkPX_cn)
   next
-    case 3
+    case xy: 3
     then obtain d where y: "y = d + x"
       by atomize_elim arith
     have "isnorm (PX Q1 d (Pc 0))"
     proof (cases Q1)
       case (PX p1 y p2)
-      with 9 3 y show ?thesis
+      with 9 xy y show ?thesis
         by (cases d) (simp, cases p2, auto)
     next
       case Pc
-      with 9 3 y show ?thesis
+      with 9 xy y show ?thesis
         by (cases d) auto
     next
       case Pinj
-      with 9 3 y show ?thesis
+      with 9 xy y show ?thesis
         by (cases d) auto
     qed
-    with 9 NQ1 NP1 NP2 NQ2 3 y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
+    with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
       by auto
-    with X0 3 y show ?thesis
+    with X0 xy y show ?thesis
       by (simp add: mkPX_cn)
   qed
 qed
@@ -376,14 +376,14 @@
   consider "x < y" | "x = y" | "x > y" by arith
   then show ?case
   proof cases
-    case 1
+    case xy: 1
     then obtain d where y: "y = d + x"
       by atomize_elim arith
     from 6 have *: "x > 0"
       by (cases x) (auto simp add: norm_Pinj_0_False)
     from 6 have **: "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    from 6 1 y have "isnorm (Pinj d Q2)"
+    from 6 xy y have "isnorm (Pinj d Q2)"
       apply (cases d)
       apply simp
       apply (cases Q2)
@@ -392,28 +392,28 @@
     with 6 * ** y show ?thesis
       by (simp add: mkPinj_cn)
   next
-    case 2
+    case xy: 2
     from 6 have *: "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     from 6 have **: "y > 0"
       by (cases y) (auto simp add: norm_Pinj_0_False)
-    with 6 2 * **show ?thesis
+    with 6 xy * ** show ?thesis
       by (simp add: mkPinj_cn)
   next
-    case 3
+    case xy: 3
     then obtain d where x: "x = d + y"
       by atomize_elim arith
     from 6 have *: "y > 0"
       by (cases y) (auto simp add: norm_Pinj_0_False)
     from 6 have **: "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    from 6 3 x have "isnorm (Pinj d P2)"
+    from 6 xy x have "isnorm (Pinj d P2)"
       apply (cases d)
       apply simp
       apply (cases P2)
       apply auto
       done
-    with 6 3 * ** x show ?thesis
+    with 6 xy * ** x show ?thesis
       by (simp add: mkPinj_cn)
   qed
 next
@@ -427,22 +427,22 @@
     with 7 show ?thesis
       by (auto simp add: norm_Pinj_0_False)
   next
-    case 2
+    case x: 2
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 2 have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 7 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
-    with 7 2 Y0 show ?thesis
+    with 7 x Y0 show ?thesis
       by (simp add: mkPX_cn)
   next
-    case 3
+    case x: 3
     from 7 have *: "isnorm R" "isnorm Q2"
       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
-    from 7 3 have "isnorm (Pinj (x - 1) P2)"
+    from 7 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 7 3 * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+    with 7 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
       by auto
-    with Y0 3 show ?thesis
+    with Y0 x show ?thesis
       by (simp add: mkPX_cn)
   qed
 next
@@ -457,22 +457,22 @@
     with 8 show ?thesis
       by (auto simp add: norm_Pinj_0_False)
   next
-    case 2
+    case x: 2
     from 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 2 have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 8 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
-    with 8 2 Y0 show ?thesis
+    with 8 x Y0 show ?thesis
       by (simp add: mkPX_cn)
   next
-    case 3
+    case x: 3
     from 8 have *: "isnorm R" "isnorm Q2"
       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
-    from 8 3 have "isnorm (Pinj (x - 1) P2)"
+    from 8 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 8 3 * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+    with 8 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
       by auto
-    with Y0 3 show ?thesis
+    with Y0 x show ?thesis
       by (simp add: mkPX_cn)
   qed
 next
diff -r d9682058f7ee -r 19c277ea65ae src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 24 21:31:29 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 24 23:03:55 2015 +0200
@@ -571,10 +571,10 @@
     by blast
   then show ?thesis
   proof cases
-    case 1
+    case u: 1
     have "between u u = u" by (simp add: between_same)
-    with 1 have "P (between u u)" by simp
-    with 1 show ?thesis by blast
+    with u have "P (between u u)" by simp
+    with u show ?thesis by blast
   next
     case 2
     note t1M = \<open>t1 \<in> U\<close> and t2M = \<open>t2\<in> U\<close>
@@ -622,10 +622,10 @@
       then show ?thesis
       proof cases
         case 1
-        show ?thesis by (rule minf_ex[OF mi 1])
+        from minf_ex[OF mi this] show ?thesis .
       next
         case 2
-        show ?thesis by (rule pinf_ex[OF pi 2])
+        from pinf_ex[OF pi this] show ?thesis .
       next
         case 3
         then show ?thesis by blast
diff -r d9682058f7ee -r 19c277ea65ae src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Jun 24 21:31:29 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Jun 24 23:03:55 2015 +0200
@@ -164,11 +164,10 @@
   consider "n \<ge> ?l" | "n < ?l" by arith
   then show ?case
   proof cases
-    case 1 
-    then show ?thesis
-      using removen_same[OF 1] by simp
+    case 1
+    with removen_same[OF this] show ?thesis by simp
   next
-    case 2
+    case nl: 2
     consider "m < n" | "m \<ge> n" by arith
     then show ?thesis
     proof cases
@@ -184,17 +183,17 @@
         then show ?thesis
           using Cons by (cases m) auto
       next
-        case 2
+        case ml: 2
         have th: "length (removen n (x # xs)) = length xs"
-          using removen_length[where n = n and xs= "x # xs"] \<open>n < ?l\<close> by simp
-        with \<open>m > ?l\<close> have "m \<ge> length (removen n (x # xs))"
+          using removen_length[where n = n and xs= "x # xs"] nl by simp
+        with ml have "m \<ge> length (removen n (x # xs))"
           by auto
         from th nth_length_exceeds[OF this] have "(removen n (x # xs))!m = [] ! (m - length xs)"
            by auto
         then have "(removen n (x # xs))!m = [] ! (m - (length (x # xs) - 1))"
           by auto
         then show ?thesis
-          using \<open>n < ?l\<close> \<open>m > ?l\<close> \<open>m > ?l\<close> by auto
+          using ml nl by auto
       qed
     qed
   qed
@@ -1699,12 +1698,12 @@
     then show ?thesis
       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
   next
-    case 2
+    case c: 2
     have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x < - ?e"
-        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
+        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
@@ -1713,12 +1712,12 @@
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 3
     have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x > - ?e"
-        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
+        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
@@ -1745,12 +1744,12 @@
     then show ?thesis
       using eqs by auto
   next
-    case 2
+    case c: 2
     have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x < - ?e"
-        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
+        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
@@ -1759,12 +1758,12 @@
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 3
     have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x > - ?e"
-        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
+        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
@@ -1792,30 +1791,30 @@
     case 1
     then show ?thesis using eqs by auto
   next
-    case 2
+    case c: 2
     have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x < - ?e"
-        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
+        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0" by simp
       then show ?thesis
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs by auto
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs by auto
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 3
     have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x > - ?e"
-        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
+        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
       then show ?thesis
-        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> by auto
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] c by auto
     qed
     then show ?thesis by auto
   qed
@@ -1837,32 +1836,32 @@
     case 1
     then show ?thesis using eqs by auto
   next
-    case 2
+    case c: 2
     have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x < - ?e"
-        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
+        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
       then show ?thesis
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs
         by auto
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 3
     have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
       if "x < -?e / ?c" for x
     proof -
       from that have "?c * x > - ?e"
-        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
+        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
       then show ?thesis
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> eqs
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs
         by auto
     qed
     then show ?thesis by auto
@@ -1904,12 +1903,12 @@
     then show ?thesis
       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
   next
-    case 2
+    case c: 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"]
+        using pos_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
@@ -1918,12 +1917,12 @@
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 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"]
+        using neg_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0" by simp
       then show ?thesis
@@ -1947,12 +1946,12 @@
     case 1
     then show ?thesis using eqs by auto
   next
-    case 2
+    case c: 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"]
+        using pos_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
@@ -1961,12 +1960,12 @@
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 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"]
+        using neg_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
@@ -1993,31 +1992,31 @@
     case 1
     then show ?thesis using eqs by auto
   next
-    case 2
+    case c: 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"]
+        using pos_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
       then show ?thesis
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs by auto
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs by auto
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 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"]
+        using neg_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
       then show ?thesis
-        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> by auto
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] c by auto
     qed
     then show ?thesis by auto
   qed
@@ -2039,31 +2038,31 @@
     case 1
     then show ?thesis using eqs by auto
   next
-    case 2
+    case c: 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"]
+        using pos_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
       then show ?thesis
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs by auto
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs by auto
     qed
     then show ?thesis by auto
   next
-    case 3
+    case c: 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"]
+        using neg_divide_less_eq[OF c, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
       then show ?thesis
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> eqs by auto
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs by auto
     qed
     then show ?thesis by auto
   qed
@@ -2234,8 +2233,6 @@
     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
   consider "?N c = 0" | "?N c > 0" | "?N c < 0" by arith
   then show ?case
   proof cases
@@ -2243,15 +2240,15 @@
     then show ?thesis
       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
   next
-    case 2
-    from px pos_less_divide_eq[OF 2, where a="x" and b="-?Nt x s"]
+    case N: 2
+    from px pos_less_divide_eq[OF N, 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 2, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: pos_less_divide_eq[OF N, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
       then show ?thesis using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
@@ -2267,15 +2264,15 @@
       then show ?thesis ..
     qed
   next
-    case 3
-    from px neg_divide_less_eq[OF 3, where a="x" and b="-?Nt x s"]
+    case N: 3
+    from px neg_divide_less_eq[OF N, 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 3, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: neg_divide_less_eq[OF N, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
       then show ?thesis using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
@@ -2310,15 +2307,15 @@
     then show ?thesis
       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
   next
-    case 2
-    from px pos_le_divide_eq[OF 2, where a="x" and b="-?Nt x s"]
+    case N: 2
+    from px pos_le_divide_eq[OF N, 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 2, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: pos_less_divide_eq[OF N, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
       then show ?thesis
@@ -2334,15 +2331,15 @@
       then show ?thesis ..
     qed
   next
-    case 3
-    from px neg_divide_le_eq[OF 3, where a="x" and b="-?Nt x s"]
+    case N: 3
+    from px neg_divide_le_eq[OF N, 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 3, where a="y" and b="-?Nt x s", symmetric])
+        by (simp add: neg_divide_less_eq[OF N, where a="y" and b="-?Nt x s", symmetric])
       then have "?N c * y + ?Nt x s < 0"
         by (simp add: field_simps)
       then show ?thesis
@@ -2537,7 +2534,7 @@
       then obtain t2u t2n where t2uU: "(t2n, t2u) \<in> ?U"
         and t2u: "t2 = - ?Nt a t2u / ?N t2n"
         by blast
-      have "t1 < t2" 
+      have "t1 < t2"
         using \<open>t1 < a\<close> \<open>a < t2\<close> by simp
       let ?u = "(t1 + t2) / 2"
       have "t1 < ?u"
@@ -2585,7 +2582,7 @@
       then show ?thesis by blast
     next
       case 2
-      from inf_uset[OF lp 2] have ?F
+      from inf_uset[OF lp this] have ?F
         using \<open>?E\<close> by blast
       then show ?thesis by blast
     qed
@@ -2660,7 +2657,7 @@
     then show ?thesis
       by (simp add: r[of 0] msubsteq_def Let_def evaldjf_ex)
   next
-    case 2
+    case cd: 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))"
@@ -2668,34 +2665,35 @@
     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 \<open>?d \<noteq> 0\<close> mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
+      using cd(2) 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 \<open>?d \<noteq> 0\<close> by simp
+      using cd(2) by simp
     finally show ?thesis
-      using 2
+      using cd
       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)
   next
-    case 3
-    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2 * ?c)"
+    case cd: 3
+    from cd(2) 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 \<open>?c \<noteq> 0\<close> mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
+      using cd(1) 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 \<open>?c \<noteq> 0\<close> by simp
-    finally show ?thesis using 3
+    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0"
+      using cd(1) by simp
+    finally show ?thesis using cd
       by (simp add: r[of "- (?t/ (2 * ?c))"] msubsteq_def Let_def evaldjf_ex)
   next
-    case 4
-    then have dc: "?c * ?d * 2 \<noteq> 0"
+    case cd: 4
+    then have cd2: "?c * ?d * 2 \<noteq> 0"
       by simp
-    from add_frac_eq[OF 4, of "- ?t" "- ?s"]
+    from add_frac_eq[OF cd, 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))"
@@ -2703,12 +2701,13 @@
     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 4 mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0]
+      using cd 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] 4
+      using nonzero_mult_divide_cancel_left [OF cd2] cd
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally show ?thesis using 4
+    finally show ?thesis
+      using cd
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
           msubsteq_def Let_def evaldjf_ex field_simps)
   qed
@@ -2765,43 +2764,43 @@
     then show ?thesis
       by (simp add: r[of 0] msubstneq_def Let_def evaldjf_ex)
   next
-    case 2
-    from \<open>?c = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2 * ?d)"
+    case cd: 2
+    from cd(1) 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 \<open>?d \<noteq> 0\<close> mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
+      using cd(2) 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 \<open>?d \<noteq> 0\<close> by simp
+      using cd(2) by simp
     finally show ?thesis
-      using 2
+      using cd
       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)
   next
-    case 3
-    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)"
+    case cd: 3
+    from cd(2) 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 \<open>?c \<noteq> 0\<close> mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
+      using cd(1) 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 \<open>?c \<noteq> 0\<close> by simp
+      using cd(1) by simp
     finally show ?thesis
-      using 3 by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
+      using cd 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"
+    case cd: 4
+    then have cd2: "?c * ?d * 2 \<noteq> 0"
       by simp
-    from add_frac_eq[OF 4, of "- ?t" "- ?s"]
+    from add_frac_eq[OF cd, 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))"
@@ -2809,13 +2808,13 @@
     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 4 mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
+      using cd 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] 4
+      using nonzero_mult_divide_cancel_left[OF cd2] cd
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally show ?thesis
-      using 4
+      using cd
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
           msubstneq_def Let_def evaldjf_ex field_simps)
   qed
@@ -2882,12 +2881,12 @@
     then show ?thesis
       using nc nd by (simp add: polyneg_norm lt r[of 0] msubstlt_def Let_def evaldjf_ex)
   next
-    case 2
-    then have dc': "2 *?c * ?d > 0"
+    case cd: 2
+    then have cd2: "2 * ?c * ?d > 0"
       by simp
-    from 2 have c: "?c \<noteq> 0" and d: "?d \<noteq> 0"
+    from cd have c: "?c \<noteq> 0" and d: "?d \<noteq> 0"
       by auto
-    from dc' have dc'': "\<not> 2 * ?c * ?d < 0" by simp
+    from cd2 have cd2': "\<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)
@@ -2896,20 +2895,21 @@
     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 dc' dc''
+      using cd2 cd2'
         mult_less_cancel_left_disj[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 "2*?c*?d"] c d
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally show ?thesis using 2 c d nc nd dc'
+    finally show ?thesis
+      using cd c d nc nd cd2'
       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)
   next
-    case 3
-    then have dc': "2 * ?c * ?d < 0"
+    case cd: 3
+    then have cd2: "2 * ?c * ?d < 0"
       by (simp add: mult_less_0_iff field_simps)
-    from 3 have c: "?c \<noteq> 0" and d: "?d \<noteq> 0"
+    from cd 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)"
@@ -2919,103 +2919,108 @@
     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 dc' order_less_not_sym[OF dc']
+      using cd2 order_less_not_sym[OF cd2]
         mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
       by simp
     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 show ?thesis using 3 c d nc nd
+    finally show ?thesis
+      using cd 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)
   next
-    case 4
-    from \<open>?c > 0\<close> have c'': "2 * ?c > 0"
+    case cd: 4
+    from cd(1) have c'': "2 * ?c > 0"
       by (simp add: zero_less_mult_iff)
-    from \<open>?c > 0\<close> have c': "2 * ?c \<noteq> 0"
+    from cd(1) have c': "2 * ?c \<noteq> 0"
       by simp
-    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
+    from cd(2) 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 \<open>?c > 0\<close> mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
+      using cd(1) 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'] \<open>?c > 0\<close>
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
-    finally show ?thesis using 4 nc nd
+    finally show ?thesis
+      using cd nc nd
       by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
   next
-    case 5
-    from \<open>?c < 0\<close> have c': "2 * ?c \<noteq> 0"
+    case cd: 5
+    from cd(1) have c': "2 * ?c \<noteq> 0"
       by simp
-    from \<open>?c < 0\<close> have c'': "2 * ?c < 0"
+    from cd(1) have c'': "2 * ?c < 0"
       by (simp add: mult_less_0_iff)
-    from \<open>?d = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
+    from cd(2) 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 \<open>?c < 0\<close> order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
+      using cd(1) 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'] \<open>?c < 0\<close> order_less_not_sym[OF c'']
+      using nonzero_mult_divide_cancel_left[OF c'] cd(1) order_less_not_sym[OF c'']
           less_imp_neq[OF c''] c''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally show ?thesis using 5 nc nd
+    finally show ?thesis
+      using cd nc nd
       by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
   next
-    case 6
-    from \<open>?d > 0\<close> have d'': "2 * ?d > 0"
+    case cd: 6
+    from cd(2) have d'': "2 * ?d > 0"
       by (simp add: zero_less_mult_iff)
-    from \<open>?d > 0\<close> have d': "2 * ?d \<noteq> 0"
+    from cd(2) have d': "2 * ?d \<noteq> 0"
       by simp
-    from \<open>?c = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2 * ?d)"
+    from cd(1) 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 \<open>?d > 0\<close> mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d''
+      using cd(2) 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'] \<open>?d > 0\<close>
+      using nonzero_mult_divide_cancel_left[OF d'] cd(2)
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
-    finally show ?thesis using 6 nc nd
+    finally show ?thesis
+      using cd nc nd
       by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
   next
-    case 7
-    from \<open>?d < 0\<close> have d': "2 * ?d \<noteq> 0"
+    case cd: 7
+    from cd(2) have d': "2 * ?d \<noteq> 0"
       by simp
-    from \<open>?d < 0\<close> have d'': "2 * ?d < 0"
+    from cd(2) have d'': "2 * ?d < 0"
       by (simp add: mult_less_0_iff)
-    from \<open>?c = 0\<close> have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"
+    from cd(1) 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 \<open>?d < 0\<close> order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
+      using cd(2) 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'] \<open>?d < 0\<close> order_less_not_sym[OF d'']
+      using nonzero_mult_divide_cancel_left[OF d'] cd(2) order_less_not_sym[OF d'']
           less_imp_neq[OF d''] d''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
-    finally show ?thesis using 7 nc nd
+    finally show ?thesis
+      using cd nc nd
       by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
           lt polyneg_norm polymul_norm)
   qed
diff -r d9682058f7ee -r 19c277ea65ae src/HOL/Decision_Procs/Rat_Pair.thy
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Wed Jun 24 21:31:29 2015 +0200
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Wed Jun 24 23:03:55 2015 +0200
@@ -32,44 +32,45 @@
 lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
 proof -
   obtain a b where x: "x = (a, b)" by (cases x)
-  consider "a = 0 \<or> b = 0" | "a \<noteq> 0" "b \<noteq> 0" by blast
+  consider "a = 0 \<or> b = 0" | "a \<noteq> 0" "b \<noteq> 0"
+    by blast
   then show ?thesis
   proof cases
     case 1
     then show ?thesis
       by (simp add: x normNum_def isnormNum_def)
   next
-    case 2
+    case ab: 2
     let ?g = "gcd a b"
     let ?a' = "a div ?g"
     let ?b' = "b div ?g"
     let ?g' = "gcd ?a' ?b'"
-    from 2 have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
-    have gpos: "?g > 0" by arith
+    from ab have "?g \<noteq> 0" by simp
+    with gcd_ge_0_int[of a b] have gpos: "?g > 0" by arith
     have gdvd: "?g dvd a" "?g dvd b" by arith+
-    from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] 2
+    from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
     have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
-    from 2 have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
+    from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
     from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
-    from 2 consider "b < 0" | "b > 0" by arith
+    from ab consider "b < 0" | "b > 0" by arith
     then show ?thesis
     proof cases
-      case 1
+      case b: 1
       have False if b': "?b' \<ge> 0"
       proof -
         from gpos have th: "?g \<ge> 0" by arith
         from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)]
-        show ?thesis using 1 by arith
+        show ?thesis using b by arith
       qed
       then have b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
-      from \<open>a \<noteq> 0\<close> nz' 1 b' gp1 show ?thesis
+      from ab(1) nz' b b' gp1 show ?thesis
         by (simp add: x isnormNum_def normNum_def Let_def split_def)
     next
-      case 2
+      case b: 2
       then have "?b' \<ge> 0"
         by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
       with nz' have b': "?b' > 0" by arith
-      from 2 b' \<open>a \<noteq> 0\<close> nz' gp1 show ?thesis
+      from b b' ab(1) nz' gp1 show ?thesis
         by (simp add: x isnormNum_def normNum_def Let_def split_def)
     qed
   qed
@@ -129,11 +130,11 @@
     then show ?thesis
       using yn x y by (simp add: isnormNum_def Let_def Nmul_def split_def)
   next
-    case 3
+    case aa': 3
     then have bp: "b > 0" "b' > 0"
       using xn yn x y by (simp_all add: isnormNum_def)
     from bp have "x *\<^sub>N y = normNum (a * a', b * b')"
-      using x y 3 bp by (simp add: Nmul_def Let_def split_def normNum_def)
+      using x y aa' bp by (simp add: Nmul_def Let_def split_def normNum_def)
     then show ?thesis by simp
   qed
 qed
@@ -192,7 +193,7 @@
     case 2
     with na nb have pos: "b > 0" "b' > 0"
       by (simp_all add: x y isnormNum_def)
-    from H \<open>b \<noteq> 0\<close> \<open>b' \<noteq> 0\<close> have eq: "a * b' = a'*b"
+    from H \<open>b \<noteq> 0\<close> \<open>b' \<noteq> 0\<close> have eq: "a * b' = a' * b"
       by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
     from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
     have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
@@ -251,9 +252,9 @@
     then show ?thesis
       by (simp add: x INum_def normNum_def split_def Let_def)
   next
-    case 2
+    case ab: 2
     let ?g = "gcd a b"
-    from 2 have g: "?g \<noteq> 0"by simp
+    from ab have g: "?g \<noteq> 0"by simp
     from of_int_div[OF g, where ?'a = 'a] show ?thesis
       by (auto simp add: x INum_def normNum_def split_def Let_def)
   qed
@@ -289,7 +290,7 @@
       apply simp_all
       done
   next
-    case 2
+    case neq: 2
     show ?thesis
     proof (cases "a * b' + b * a' = 0")
       case True
@@ -299,8 +300,8 @@
           of_int b * of_int a' / (of_int b * of_int b') = ?z"
         by (simp add: add_divide_distrib)
       then have th: "of_int a / of_int b + of_int a' / of_int b' = ?z"
-        using 2 by simp
-      from True 2 show ?thesis
+        using neq by simp
+      from True neq show ?thesis
         by (simp add: x y th Nadd_def normNum_def INum_def split_def)
     next
       case False
@@ -308,7 +309,7 @@
       have gz: "?g \<noteq> 0"
         using False by simp
       show ?thesis
-        using 2 False gz
+        using neq False gz
           of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * b' + b * a'" "b * b'"]]
           of_int_div [where ?'a = 'a, OF gz gcd_dvd2 [of "a * b' + b * a'" "b * b'"]]
         by (simp add: x y Nadd_def INum_def normNum_def Let_def) (simp add: field_simps)
@@ -335,11 +336,11 @@
       apply simp_all
       done
   next
-    case 2
+    case neq: 2
     let ?g = "gcd (a * a') (b * b')"
     have gz: "?g \<noteq> 0"
-      using 2 by simp
-    from 2 of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * a'" "b * b'"]]
+      using neq by simp
+    from neq of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * a'" "b * b'"]]
       of_int_div [where ?'a = 'a , OF gz gcd_dvd2 [of "a * a'" "b * b'"]]
     show ?thesis
       by (simp add: Nmul_def x y Let_def INum_def)
diff -r d9682058f7ee -r 19c277ea65ae src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Jun 24 21:31:29 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jun 24 23:03:55 2015 +0200
@@ -494,15 +494,15 @@
     then show ?thesis
       by (cases "c = a") (simp_all add: th dist_fps_sym)
   next
-    case 3
+    case neq: 3
     def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n"
     then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m"
       by (auto dest: not_less_Least)
-    from 3 have dab: "dist a b = inverse (2 ^ n a b)"
+    from neq have dab: "dist a b = inverse (2 ^ n a b)"
       and dac: "dist a c = inverse (2 ^ n a c)"
       and dbc: "dist b c = inverse (2 ^ n b c)"
       by (simp_all add: dist_fps_def n_def fps_eq_iff)
-    from 3 have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0"
+    from neq have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0"
       unfolding th by simp_all
     from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0"
       using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c]
@@ -1073,7 +1073,7 @@
     then show ?thesis by simp
   next
     case 2
-    from startsby_zero_power[OF True 2] eq show ?thesis
+    from startsby_zero_power[OF True this] eq show ?thesis
       by (simp add: fps_inverse_def)
   qed
 next
@@ -1129,23 +1129,23 @@
     by blast
   then show ?thesis
   proof cases
-    case 1
+    case a: 1
     then have "(a * b) $ 0 = 0"
       by (simp add: fps_mult_nth)
-    with 1 have th: "inverse a = 0" "inverse (a * b) = 0"
+    with a have th: "inverse a = 0" "inverse (a * b) = 0"
       by simp_all
     show ?thesis
       unfolding th by simp
   next
-    case 2
+    case b: 2
     then have "(a * b) $ 0 = 0"
       by (simp add: fps_mult_nth)
-    with 2 have th: "inverse b = 0" "inverse (a * b) = 0"
+    with b have th: "inverse b = 0" "inverse (a * b) = 0"
       by simp_all
     show ?thesis
       unfolding th by simp
   next
-    case 3
+    case ab: 3
     then have ab0:"(a * b) $ 0 \<noteq> 0"
       by (simp add: fps_mult_nth)
     from inverse_mult_eq_1[OF ab0]
@@ -1154,7 +1154,7 @@
     then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b"
       by (simp add: field_simps)
     then show ?thesis
-      using inverse_mult_eq_1[OF \<open>a $ 0 \<noteq> 0\<close>] inverse_mult_eq_1[OF \<open>b $ 0 \<noteq> 0\<close>] by simp
+      using inverse_mult_eq_1[OF ab(1)] inverse_mult_eq_1[OF ab(2)] by simp
   qed
 qed
 
@@ -1168,7 +1168,7 @@
 
 lemma inverse_mult_eq_1':
   assumes f0: "f$0 \<noteq> (0::'a::field)"
-  shows "f * inverse f= 1"
+  shows "f * inverse f = 1"
   by (metis mult.commute inverse_mult_eq_1 f0)
 
 lemma fps_divide_deriv:
@@ -3190,7 +3190,8 @@
     from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0"
       by (rule pochhammer_neq_0_mono)
 
-    consider "k = 0 \<or> n = 0" | "n \<noteq> 0" "k \<noteq> 0" by blast
+    consider "k = 0 \<or> n = 0" | "k \<noteq> 0" "n \<noteq> 0"
+      by blast
     then have "b gchoose (n - k) =
       (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
     proof cases
@@ -3198,10 +3199,10 @@
       then show ?thesis
         using kn by (cases "k = 0") (simp_all add: gbinomial_pochhammer)
     next
-      case 2
+      case neq: 2
       then obtain m where m: "n = Suc m"
         by (cases n) auto
-      from \<open>k \<noteq> 0\<close> obtain h where h: "k = Suc h"
+      from neq(1) obtain h where h: "k = Suc h"
         by (cases k) auto
       show ?thesis
       proof (cases "k = n")
diff -r d9682058f7ee -r 19c277ea65ae src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jun 24 21:31:29 2015 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jun 24 23:03:55 2015 +0200
@@ -1005,28 +1005,28 @@
     by (cases "degree p") auto
   then show ?thesis
   proof cases
-    case 1
+    case p: 1
     then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
       by (auto simp add: poly_all_0_iff_0)
     {
       assume "p dvd (q ^ (degree p))"
       then obtain r where r: "q ^ (degree p) = p * r" ..
-      from r 1 have False by simp
+      from r p have False by simp
     }
-    with eq 1 show ?thesis by blast
+    with eq p show ?thesis by blast
   next
-    case 2
+    case dp: 2
     then obtain k where k: "p = [:k:]" "k \<noteq> 0"
       by (cases p) (simp split: if_splits)
     then have th1: "\<forall>x. poly p x \<noteq> 0"
       by simp
-    from k 2(2) have "q ^ (degree p) = p * [:1/k:]"
+    from k dp(2) have "q ^ (degree p) = p * [:1/k:]"
       by (simp add: one_poly_def)
     then have th2: "p dvd (q ^ (degree p))" ..
-    from 2(1) th1 th2 show ?thesis
+    from dp(1) th1 th2 show ?thesis
       by blast
   next
-    case 3
+    case dp: 3
     have False if dvd: "p dvd (q ^ (Suc n))" and h: "poly p x = 0" "poly q x \<noteq> 0" for x
     proof -
       from dvd obtain u where u: "q ^ (Suc n) = p * u" ..
@@ -1035,8 +1035,8 @@
       with u h(1) show ?thesis
         by (simp only: poly_mult) simp
     qed
-    with 3 nullstellensatz_lemma[of p q "degree p"]
-    show ?thesis by auto
+    with dp nullstellensatz_lemma[of p q "degree p"] show ?thesis
+      by auto
   qed
 qed
 
diff -r d9682058f7ee -r 19c277ea65ae src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 24 21:31:29 2015 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 24 23:03:55 2015 +0200
@@ -42,7 +42,7 @@
   assume "n > 0"
   then consider "n = 1" | "n > 1" "prime n" | "n > 1" "\<not> prime n"
     by arith
-  then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i::nat\<in>#M. i)"
+  then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i\<in>#M. i)"
   proof cases
     case 1
     then have "(\<forall>p\<in>set_mset {#}. prime p) \<and> n = (\<Prod>i \<in># {#}. i)"