--- 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
--- 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
--- 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
--- 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)
--- 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")
--- 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
--- 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)"