author wenzelm Mon, 21 Feb 2011 23:54:53 +0100 changeset 41816 7a55699805dc parent 41815 9a0cacbcd825 (current diff) parent 41807 ab5d2d81f9fb (diff) child 41817 c7be23634728 child 41829 455cbcbba8c2
merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
```--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Feb 21 23:54:53 2011 +0100
@@ -308,7 +308,7 @@
assumes "norm P1 = norm P2"
shows "Ipolex l P1 = Ipolex l P2"
proof -
-  from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
+  from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
then show ?thesis by (simp only: norm_ci)
qed
```
```--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Mon Feb 21 23:54:53 2011 +0100
@@ -50,23 +50,25 @@
assumes A:"isnorm (PX P x Q)" and "isnorm Q2"
shows "isnorm (PX P x Q2)"
proof(cases P)
-  case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto)
+  case (PX p1 y p2) with assms show ?thesis by(cases x, auto, cases p2, auto)
next
-  case Pc from prems show ?thesis by(cases x, auto)
+  case Pc with assms show ?thesis by (cases x) auto
next
-  case Pinj from prems show ?thesis by(cases x, auto)
+  case Pinj with assms show ?thesis by (cases x) auto
qed

-lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)"
-proof(cases P)
+lemma norm_PXtrans2:
+  assumes "isnorm (PX P x Q)" and "isnorm Q2"
+  shows "isnorm (PX P (Suc (n+x)) Q2)"
+proof (cases P)
case (PX p1 y p2)
-  from prems show ?thesis by(cases x, auto, cases p2, auto)
+  with assms show ?thesis by (cases x, auto, cases p2, auto)
next
case Pc
-  from prems show ?thesis by(cases x, auto)
+  with assms show ?thesis by (cases x) auto
next
case Pinj
-  from prems show ?thesis by(cases x, auto)
+  with assms show ?thesis by (cases x) auto
qed

text {* mkPX conserves normalizedness (@{text "_cn"}) *}
@@ -75,15 +77,17 @@
shows "isnorm (mkPX P x Q)"
proof(cases P)
case (Pc c)
-  from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
+  with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
next
case (Pinj i Q)
-  from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
+  with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
next
case (PX P1 y P2)
-  from prems have Y0:"y>0" by(cases y, auto)
-  from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
-  with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
+  with assms have Y0: "y>0" by (cases y) auto
+  from assms PX have "isnorm P1" "isnorm P2"
+    by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
+  from assms PX Y0 show ?thesis
+    by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
qed

text {* add conserves normalizedness *}
@@ -94,118 +98,127 @@
case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
next
case (4 c P2 i Q2)
-  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
-  with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
+  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+  with 4 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
next
case (5 P2 i Q2 c)
-  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
-  with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
+  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+  with 5 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
next
case (6 x P2 y Q2)
-  from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False)
-  from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False)
+  then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
+  with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False)
have "x < y \<or> x = y \<or> x > y" by arith
moreover
-  { assume "x<y" hence "EX d. y=d+x" by arith
-    then obtain d where "y=d+x"..
+  { assume "x<y" hence "EX d. y =d + x" by arith
+    then obtain d where y: "y = d + x" ..
moreover
-    note prems X0
+    note 6 X0
moreover
-    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
-    with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn)}
+    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
+    ultimately have ?case by (simp add: mkPinj_cn) }
moreover
{ assume "x=y"
moreover
-    from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
-    note prems Y0
+    note 6 Y0
moreover
ultimately have ?case by (simp add: mkPinj_cn) }
moreover
-  { assume "x>y" hence "EX d. x=d+y" by arith
-    then obtain d where "x=d+y"..
+  { assume "x>y" hence "EX d. x = d + y" by arith
+    then obtain d where x: "x = d + y"..
moreover
-    note prems Y0
+    note 6 Y0
moreover
-    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
-    with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
+    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
ultimately have ?case by (simp add: mkPinj_cn)}
ultimately show ?case by blast
next
case (7 x P2 Q2 y R)
have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
moreover
-  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
+  { assume "x = 0"
+    with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
moreover
-  { assume "x=1"
-    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with prems have "isnorm (R \<oplus> P2)" by simp
-    with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
+  { assume "x = 1"
+    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
+    with 7 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
moreover
{ assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
then obtain d where X:"x=Suc (Suc d)" ..
-    from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
-    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
-    with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
+    with 7 have NR: "isnorm R" "isnorm P2"
+      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
+    with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
+    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
ultimately show ?case by blast
next
case (8 Q2 y R x P2)
have "x = 0 \<or> x = 1 \<or> x > 1" by arith
moreover
-  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
+  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
moreover
-  { assume "x=1"
-    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with prems have "isnorm (R \<oplus> P2)" by simp
-    with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
+  { assume "x = 1"
+    with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp
+    with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
moreover
{ assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
-    then obtain d where X:"x=Suc (Suc d)" ..
-    from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
-    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
-    with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
+    then obtain d where X: "x = Suc (Suc d)" ..
+    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 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
+    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
ultimately show ?case by blast
next
case (9 P1 x P2 Q1 y Q2)
-  from prems have Y0:"y>0" by(cases y, auto)
-  from prems have X0:"x>0" by(cases x, auto)
-  from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
-  from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
+  then have Y0: "y>0" by (cases y) auto
+  with 9 have X0: "x>0" by (cases x) auto
+  with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
+    by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
+  with 9 have NQ1:"isnorm Q1" and NQ2: "isnorm Q2"
+    by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
have "y < x \<or> x = y \<or> x < y" by arith
moreover
-  {assume sm1:"y < x" hence "EX d. x=d+y" by arith
-    then obtain d where sm2:"x=d+y"..
-    note prems NQ1 NP1 NP2 NQ2 sm1 sm2
+  { assume sm1: "y < x" hence "EX d. x = d + y" by arith
+    then obtain d where sm2: "x = d + y" ..
+    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
moreover
have "isnorm (PX P1 d (Pc 0))"
-    proof(cases P1)
+    proof (cases P1)
case (PX p1 y p2)
-      with prems show ?thesis by(cases d, simp,cases p2, auto)
-    next case Pc   from prems show ?thesis by(cases d, auto)
-    next case Pinj from prems show ?thesis by(cases d, auto)
+      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
+    next
+      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
+    next
+      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
qed
ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
-    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
+    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
moreover
-  {assume "x=y"
-    from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
-    with Y0 prems have ?case by (simp add: mkPX_cn) }
+  { assume "x = y"
+    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
+    with `x = y` Y0 have ?case by (simp add: mkPX_cn) }
moreover
-  {assume sm1:"x<y" hence "EX d. y=d+x" by arith
-    then obtain d where sm2:"y=d+x"..
-    note prems NQ1 NP1 NP2 NQ2 sm1 sm2
+  { assume sm1: "x < y" hence "EX d. y = d + x" by arith
+    then obtain d where sm2: "y = d + x" ..
+    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
moreover
have "isnorm (PX Q1 d (Pc 0))"
-    proof(cases Q1)
+    proof (cases Q1)
case (PX p1 y p2)
-      with prems show ?thesis by(cases d, simp,cases p2, auto)
-    next case Pc   from prems show ?thesis by(cases d, auto)
-    next case Pinj from prems show ?thesis by(cases d, auto)
+      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
+    next
+      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
+    next
+      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
qed
ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
@@ -222,138 +235,141 @@
by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
next
case (4 c P2 i Q2)
-  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
-  with prems show ?case
-    by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
+  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+  with 4 show ?case
+    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
next
case (5 P2 i Q2 c)
-  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
-  with prems show ?case
-    by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
+  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
+  with 5 show ?case
+    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
next
case (6 x P2 y Q2)
have "x < y \<or> x = y \<or> x > y" by arith
moreover
-  { assume "x<y" hence "EX d. y=d+x" by arith
-    then obtain d where "y=d+x"..
+  { assume "x < y" hence "EX d. y = d + x" by arith
+    then obtain d where y: "y = d + x" ..
moreover
-    note prems
+    note 6
moreover
-    from prems have "x>0" by (cases x, auto simp add: norm_Pinj_0_False)
+    from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False)
moreover
-    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
-    with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn)}
+    from 6 `x < y` y have "isnorm (Pinj d Q2)" by - (cases d, simp, cases Q2, auto)
+    ultimately have ?case by (simp add: mkPinj_cn) }
moreover
-  { assume "x=y"
+  { assume "x = y"
moreover
-    from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
-    with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
+    from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
moreover
-    note prems
+    note 6
moreover
ultimately have ?case by (simp add: mkPinj_cn) }
moreover
-  { assume "x>y" hence "EX d. x=d+y" by arith
-    then obtain d where "x=d+y"..
+  { assume "x > y" hence "EX d. x = d + y" by arith
+    then obtain d where x: "x = d + y" ..
moreover
-    note prems
+    note 6
moreover
-    from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
+    from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)
moreover
-    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
-    with prems have "isnorm (Pinj d P2)"  by (cases d, simp, cases P2, auto)
+    from 6 `x > y` x have "isnorm (Pinj d P2)" by - (cases d, simp, cases P2, auto)
ultimately have ?case by (simp add: mkPinj_cn) }
ultimately show ?case by blast
next
case (7 x P2 Q2 y R)
-  from prems have Y0:"y>0" by(cases y, auto)
-  have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
+  then have Y0: "y > 0" by (cases y) auto
+  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
moreover
-  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
+  { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
moreover
-  { assume "x=1"
-    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
-    with Y0 prems have ?case by (simp add: mkPX_cn)}
+  { assume "x = 1"
+    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
+    with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
moreover
-  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
-    then obtain d where X:"x=Suc (Suc d)" ..
-    from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
-    moreover
-    from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
+  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
+    then obtain d where X: "x = Suc (Suc d)" ..
+    from 7 have NR: "isnorm R" "isnorm Q2"
+      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
moreover
-    from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
+    from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
+    moreover
+    from 7 have "isnorm (Pinj x P2)" by (cases P2) auto
moreover
-    note prems
+    note 7 X
ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
-    with Y0 X have ?case by (simp add: mkPX_cn)}
+    with Y0 X have ?case by (simp add: mkPX_cn) }
ultimately show ?case by blast
next
case (8 Q2 y R x P2)
-  from prems have Y0:"y>0" by(cases y, auto)
-  have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
+  then have Y0: "y>0" by (cases y) auto
+  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
moreover
-  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
+  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
moreover
-  { assume "x=1"
-    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
-    with Y0 prems have ?case by (simp add: mkPX_cn) }
+  { assume "x = 1"
+    from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
+    with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
moreover
-  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
-    then obtain d where X:"x=Suc (Suc d)" ..
-    from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
+  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
+    then obtain d where X: "x = Suc (Suc d)" ..
+    from 8 have NR: "isnorm R" "isnorm Q2"
+      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
moreover
-    from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
+    from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
moreover
-    from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
+    from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
moreover
-    note prems
+    note 8 X
ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
with Y0 X have ?case by (simp add: mkPX_cn) }
ultimately show ?case by blast
next
case (9 P1 x P2 Q1 y Q2)
-  from prems have X0:"x>0" by(cases x, auto)
-  from prems have Y0:"y>0" by(cases y, auto)
-  note prems
+  from 9 have X0: "x > 0" by (cases x) auto
+  from 9 have Y0: "y > 0" by (cases y) auto
+  note 9
moreover
-  from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
+  from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
moreover
-  from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
+  from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
"isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
by (auto simp add: mkPinj_cn)
-  with prems X0 Y0 have
+  with 9 X0 Y0 have
"isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
"isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
"isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
by (auto simp add: mkPX_cn)
thus ?case by (simp add: add_cn)
-qed(simp)
+qed simp

text {* neg conserves normalizedness *}
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
proof (induct P)
case (Pinj i P2)
-  from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2])
-  with prems show ?case by(cases P2, auto, cases i, auto)
+  then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
+  with Pinj show ?case by - (cases P2, auto, cases i, auto)
next
-  case (PX P1 x P2)
-  from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
-  with prems show ?case
-  proof(cases P1)
+  case (PX P1 x P2) note PX1 = this
+  from PX have "isnorm P2" "isnorm P1"
+    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
+  with PX show ?case
+  proof (cases P1)
case (PX p1 y p2)
-    with prems show ?thesis by(cases x, auto, cases p2, auto)
+    with PX1 show ?thesis by - (cases x, auto, cases p2, auto)
next
case Pinj
-    with prems show ?thesis by(cases x, auto)
-  qed(cases x, auto)
-qed(simp)
+    with PX1 show ?thesis by (cases x) auto
+  qed (cases x, auto)
+qed simp

text {* sub conserves normalizedness *}
lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
@@ -361,17 +377,18 @@

text {* sqr conserves normalizizedness *}
lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
-proof(induct P)
+proof (induct P)
case (Pinj i Q)
-  from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
+  then show ?case
+    by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
next
case (PX P1 x P2)
-  from prems have "x+x~=0" "isnorm P2" "isnorm P1" by (cases x,  auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
-  with prems have
-    "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
-    and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
-   by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
-  thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
+  then have "x + x ~= 0" "isnorm P2" "isnorm P1"
+    by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
+  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
+      and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
+    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
+  then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
qed simp

text {* pow conserves normalizedness *}
@@ -379,12 +396,12 @@
proof (induct n arbitrary: P rule: nat_less_induct)
case (1 k)
show ?case
-  proof (cases "k=0")
+  proof (cases "k = 0")
case False
-    then have K2:"k div 2 < k" by (cases k, auto)
-    from prems have "isnorm (sqr P)" by (simp add: sqr_cn)
-    with prems K2 show ?thesis
-    by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
+    then have K2: "k div 2 < k" by (cases k) auto
+    from 1 have "isnorm (sqr P)" by (simp add: sqr_cn)
+    with 1 False K2 show ?thesis
+      by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
qed simp
qed
```
```--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 21 23:54:53 2011 +0100
@@ -495,11 +495,11 @@
| "not F = T"
| "not p = NOT p"
lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
-by (cases p) auto
+  by (cases p) auto
lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
-by (cases p, auto)
+  by (cases p) auto
lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
-by (cases p, auto)
+  by (cases p) auto

definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
"conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"
@@ -755,12 +755,12 @@
let ?b = "snd (zsplit0 a)"
have abj: "zsplit0 a = (?j,?b)" by simp
{assume "m\<noteq>0"
-    with prems(1)[OF abj] prems(2) have ?case by (auto simp add: Let_def split_def)}
+    with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)}
moreover
{assume m0: "m =0"
-    from abj have th: "a'=?b \<and> n=i+?j" using prems
+    with abj have th: "a'=?b \<and> n=i+?j" using 3
by (simp add: Let_def split_def)
-    from abj prems  have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
+    from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
@@ -770,9 +770,9 @@
case (4 t n a)
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
-  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems
+  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 4
by (simp add: Let_def split_def)
-  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
+  from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
from th2[simplified] th[simplified] show ?case by simp
next
case (5 s t n a)
@@ -782,12 +782,12 @@
let ?at = "snd (zsplit0 t)"
have abjs: "zsplit0 s = (?ns,?as)" by simp
moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp
-  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems
+  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 5
by (simp add: Let_def split_def)
from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
-  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
+  from 5 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+  from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
by (simp add: left_distrib)
next
@@ -798,22 +798,22 @@
let ?at = "snd (zsplit0 t)"
have abjs: "zsplit0 s = (?ns,?as)" by simp
moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp
-  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems
+  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6
by (simp add: Let_def split_def)
from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
-  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
+  from 6 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+  from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
by (simp add: left_diff_distrib)
next
case (7 i t n a)
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
-  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems
+  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 7
by (simp add: Let_def split_def)
-  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  hence " ?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
+  from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
+  hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
finally show ?case using th th2 by simp
qed
@@ -905,9 +905,9 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
-  from prems Ia nb  show ?case
+  from 5 Ia nb  show ?case
apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
+    apply (cases "?r", auto)
apply (case_tac nat, auto)
done
next
@@ -918,9 +918,9 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
-  from prems Ia nb  show ?case
+  from 6 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
+    apply (cases "?r", auto)
apply (case_tac nat, auto)
done
next
@@ -931,9 +931,9 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
-  from prems Ia nb  show ?case
+  from 7 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
+    apply (cases "?r", auto)
apply (case_tac nat, auto)
done
next
@@ -944,9 +944,9 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
-  from prems Ia nb  show ?case
+  from 8 Ia nb  show ?case
apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
+    apply (cases "?r", auto)
apply (case_tac nat, auto)
done
next
@@ -957,9 +957,9 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
-  from prems Ia nb  show ?case
+  from 9 Ia nb  show ?case
apply (auto simp add: Let_def split_def algebra_simps)
-    apply (cases "?r",auto)
+    apply (cases "?r", auto)
apply (case_tac nat, auto)
done
next
@@ -970,7 +970,7 @@
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
-  from prems Ia nb  show ?case
+  from 10 Ia nb  show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
@@ -986,7 +986,7 @@
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
{assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def)
-    hence ?case using prems by (simp del: zlfm.simps)}
+    hence ?case using 11 `j = 0` by (simp del: zlfm.simps) }
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
@@ -1015,7 +1015,7 @@
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
{assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def)
-    hence ?case using prems by (simp del: zlfm.simps)}
+    hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
@@ -1100,20 +1100,20 @@
proof (induct p rule: iszlfm.induct)
case (1 p q)
let ?d = "\<delta> (And p q)"
-  from prems lcm_pos_int have dp: "?d >0" by simp
-  have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
-  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps)
-  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
-  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
+  from 1 lcm_pos_int have dp: "?d >0" by simp
+  have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
+  hence th: "d\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
+  have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
+  hence th': "d\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
from th th' dp show ?case by simp
next
case (2 p q)
let ?d = "\<delta> (And p q)"
-  from prems lcm_pos_int have dp: "?d >0" by simp
-  have "\<delta> p dvd \<delta> (And p q)" using prems by simp
-  hence th: "d\<delta> p ?d" using delta_mono prems by(simp only: iszlfm.simps)
-  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
-  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
+  from 2 lcm_pos_int have dp: "?d >0" by simp
+  have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
+  hence th: "d\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
+  have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
+  hence th': "d\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
from th th' dp show ?case by simp
qed simp_all

@@ -1200,7 +1200,7 @@
"mirror p = p"
(* Lemmas for the correctness of \<sigma>\<rho> *)
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
-by simp
+  by simp

lemma minusinf_inf:
assumes linp: "iszlfm p"
@@ -1374,14 +1374,14 @@

lemma mirror_l: "iszlfm p \<and> d\<beta> p 1
\<Longrightarrow> iszlfm (mirror p) \<and> d\<beta> (mirror p) 1"
-by (induct p rule: mirror.induct, auto)
+  by (induct p rule: mirror.induct) auto

lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
-by (induct p rule: mirror.induct,auto)
+  by (induct p rule: mirror.induct) auto

lemma \<beta>_numbound0: assumes lp: "iszlfm p"
shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
-  using lp by (induct p rule: \<beta>.induct,auto)
+  using lp by (induct p rule: \<beta>.induct) auto

lemma d\<beta>_mono:
assumes linp: "iszlfm p"
@@ -1389,12 +1389,12 @@
and d: "l dvd l'"
shows "d\<beta> p l'"
using dr linp dvd_trans[of _ "l" "l'", simplified d]
-by (induct p rule: iszlfm.induct) simp_all
+  by (induct p rule: iszlfm.induct) simp_all

lemma \<alpha>_l: assumes lp: "iszlfm p"
shows "\<forall> b\<in> set (\<alpha> p). numbound0 b"
using lp
-by(induct p rule: \<alpha>.induct, auto)
+  by(induct p rule: \<alpha>.induct) auto

lemma \<zeta>:
assumes linp: "iszlfm p"
@@ -1402,16 +1402,16 @@
using linp
proof(induct p rule: iszlfm.induct)
case (1 p q)
-  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"  by simp
-  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+  from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
next
case (2 p q)
-  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+  from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
qed (auto simp add: lcm_pos_int)
@@ -1585,31 +1585,31 @@
shows "?P (x - d)"
using lp u d dp nob p
proof(induct p rule: iszlfm.induct)
-  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp+
-    with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
-    show ?case by simp
+  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp_all
+  with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5
+  show ?case by simp
next
-  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp+
-    with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
-    show ?case by simp
+  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp_all
+  with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6
+  show ?case by simp
next
-  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp+
-    let ?e = "Inum (x # bs) e"
-    {assume "(x-d) +?e > 0" hence ?case using c1
-      numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
-    moreover
-    {assume H: "\<not> (x-d) + ?e > 0"
-      let ?v="Neg e"
-      have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
-      from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
-      have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto
-      from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
-      hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
-      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
-      hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)"
-        by (simp add: algebra_simps)
-      with nob have ?case by auto}
-    ultimately show ?case by blast
+  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp_all
+  let ?e = "Inum (x # bs) e"
+  {assume "(x-d) +?e > 0" hence ?case using c1
+    numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
+  moreover
+  {assume H: "\<not> (x-d) + ?e > 0"
+    let ?v="Neg e"
+    have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
+    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
+    have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto
+    from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
+    hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
+    hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
+    hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)"
+      by (simp add: algebra_simps)
+    with nob have ?case by auto}
+  ultimately show ?case by blast
next
case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
by simp+
@@ -1621,7 +1621,7 @@
{assume H: "\<not> (x-d) + ?e \<ge> 0"
let ?v="Sub (C -1) e"
have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
-      from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
+      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto
from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
@@ -1634,7 +1634,7 @@
let ?e = "Inum (x # bs) e"
let ?v="(Sub (C -1) e)"
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
-    from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
+    from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
by simp (erule ballE[where x="1"],
simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
next
@@ -1649,12 +1649,12 @@
hence "x = - Inum (((x -d)) # bs) e + d" by simp
hence "x = - Inum (a # bs) e + d"
by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
-       with prems(11) have ?case using dp by simp}
+       with 4(5) have ?case using dp by simp}
ultimately show ?case by blast
next
case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
let ?e = "Inum (x # bs) e"
-    from prems have id: "j dvd d" by simp
+    from 9 have id: "j dvd d" by simp
from c1 have "?p x = (j dvd (x+ ?e))" by simp
also have "\<dots> = (j dvd x - d + ?e)"
using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
@@ -1663,7 +1663,7 @@
next
case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
let ?e = "Inum (x # bs) e"
-    from prems have id: "j dvd d" by simp
+    from 10 have id: "j dvd d" by simp
from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
also have "\<dots> = (\<not> j dvd x - d + ?e)"
using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp```
```--- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 21 23:54:53 2011 +0100
@@ -495,14 +495,16 @@
assumes gt: "dvdnumcoeff t g" and gp: "g > 0"
shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t"
using gt
-proof(induct t rule: reducecoeffh.induct)
-  case (1 i) hence gd: "g dvd i" by simp
+proof (induct t rule: reducecoeffh.induct)
+  case (1 i)
+  hence gd: "g dvd i" by simp
from gp have gnz: "g \<noteq> 0" by simp
-  from prems show ?case by (simp add: real_of_int_div[OF gnz gd])
+  with assms show ?case by (simp add: real_of_int_div[OF gnz gd])
next
-  case (2 n c t)  hence gd: "g dvd c" by simp
+  case (2 n c t)
+  hence gd: "g dvd c" by simp
from gp have gnz: "g \<noteq> 0" by simp
-  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
+  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
qed (auto simp add: numgcd_def gp)

fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
@@ -511,14 +513,14 @@
| "ismaxcoeff t = (\<lambda>x. True)"

lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
-by (induct t rule: ismaxcoeff.induct, auto)
+  by (induct t rule: ismaxcoeff.induct) auto

lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)"
proof (induct t rule: maxcoeff.induct)
case (2 n c t)
hence H:"ismaxcoeff t (maxcoeff t)" .
-  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2)
-  from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
+  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp
+  from ismaxcoeff_mono[OF H thh] show ?case by simp
qed simp_all

lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
@@ -534,30 +536,31 @@
lemma dvdnumcoeff_aux:
assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
shows "dvdnumcoeff t (numgcdh t m)"
-using prems
+using assms
proof(induct t rule: numgcdh.induct)
case (2 n c t)
let ?g = "numgcdh t m"
-  from prems have th:"gcd c ?g > 1" by simp
+  from 2 have th:"gcd c ?g > 1" by simp
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
-  moreover {assume "abs c > 1" and gp: "?g > 1" with prems
+  moreover {assume "abs c > 1" and gp: "?g > 1" with 2
have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp }
moreover {assume "abs c = 0 \<and> ?g > 1"
-    with prems have th: "dvdnumcoeff t ?g" by simp
+    with 2 have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
-    from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
+    from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp }
ultimately show ?case by blast
qed auto

lemma dvdnumcoeff_aux2:
-  assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
-  using prems
+  assumes "numgcd t > 1"
+  shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
+  using assms
proof (simp add: numgcd_def)
let ?mc = "maxcoeff t"
let ?g = "numgcdh t ?mc"
@@ -679,10 +682,10 @@
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
proof (induct t rule: maxcoeff.induct)
case (2 n c t)
-  hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
-  have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)
+  hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp_all
+  have "max (abs c) (maxcoeff t) \<ge> abs c" by simp
with cnz have "max (abs c) (maxcoeff t) > 0" by arith
-  with prems show ?case by simp
+  with 2 show ?case by simp
qed auto

lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0"
@@ -710,7 +713,7 @@
{assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
moreover
{ assume nnz: "n \<noteq> 0"
-    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
+    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci) }
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
from g1 nnz have gp0: "?g' \<noteq> 0" by simp
@@ -726,45 +729,48 @@
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs ?t'" by simp
-        from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
+        from g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
also have "\<dots> = (Inum bs ?t' / real n)"
using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
-        finally have "?lhs = Inum bs t / real n" by (simp add: simpnum_ci)
-        then have ?thesis using prems by (simp add: simp_num_pair_def)}
-      ultimately have ?thesis by blast}
-    ultimately have ?thesis by blast}
+        finally have "?lhs = Inum bs t / real n" by simp
+        then have ?thesis by (simp add: simp_num_pair_def) }
+      ultimately have ?thesis by blast }
+    ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed

lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')"
shows "numbound0 t' \<and> n' >0"
proof-
-    let ?t' = "simpnum t"
+  let ?t' = "simpnum t"
let ?g = "numgcd ?t'"
let ?g' = "gcd n ?g"
-  {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
+  { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) }
moreover
{ assume nnz: "n \<noteq> 0"
-    {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
+    { assume "\<not> ?g > 1" hence ?thesis using assms
+        by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) }
moreover
-    {assume g1:"?g>1" hence g0: "?g > 0" by simp
+    { assume g1:"?g>1" hence g0: "?g > 0" by simp
from g1 nnz have gp0: "?g' \<noteq> 0" by simp
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
-      moreover {assume "?g'=1" hence ?thesis using prems
-          by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
-      moreover {assume g'1:"?g'>1"
+      moreover {
+        assume "?g' = 1" hence ?thesis using assms g1
+          by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) }
+      moreover {
+        assume g'1: "?g' > 1"
have gpdg: "?g' dvd ?g" by simp
-        have gpdd: "?g' dvd n" by simp
+        have gpdd: "?g' dvd n" by simp
have gpdgp: "?g' dvd ?g'" by simp
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
have "n div ?g' >0" by simp
-        hence ?thesis using prems
-          by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)}
-      ultimately have ?thesis by blast}
-    ultimately have ?thesis by blast}
+        hence ?thesis using assms g1 g'1
+          by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0) }
+      ultimately have ?thesis by blast }
+    ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed

@@ -962,14 +968,14 @@
let ?sa = "rsplit0 a" let ?sb = "rsplit0 b"
let ?ca = "fst ?sa" let ?cb = "fst ?sb"
let ?ta = "snd ?sa" let ?tb = "snd ?sb"
-  from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))"
+  from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))"
by (cases "rsplit0 a") (auto simp add: Let_def split_def)
have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) =
Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
by (simp add: Let_def split_def algebra_simps)
-  also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a") auto
+  also have "\<dots> = Inum bs a + Inum bs b" using 2 by (cases "rsplit0 a") auto
finally show ?case using nb by simp
-qed (auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric])
+qed (auto simp add: Let_def split_def algebra_simps, simp add: right_distrib[symmetric])

(* Linearize a formula*)
definition
@@ -1081,8 +1087,8 @@
case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
next
case (3 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 3 have nb: "numbound0 e" by simp
+  from 3 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1098,8 +1104,8 @@
thus ?case by blast
next
case (4 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 4 have nb: "numbound0 e" by simp
+  from 4 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1115,8 +1121,8 @@
thus ?case by blast
next
case (5 c e)
-    from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 5 have nb: "numbound0 e" by simp
+  from 5 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1131,8 +1137,8 @@
thus ?case by blast
next
case (6 c e)
-    from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 6 have nb: "numbound0 e" by simp
+  from lp 6 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1147,8 +1153,8 @@
thus ?case by blast
next
case (7 c e)
-    from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 7 have nb: "numbound0 e" by simp
+  from 7 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1163,8 +1169,8 @@
thus ?case by blast
next
case (8 c e)
-    from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 8 have nb: "numbound0 e" by simp
+  from 8 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1189,8 +1195,8 @@
case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto
next
case (3 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 3 have nb: "numbound0 e" by simp
+  from 3 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1206,8 +1212,8 @@
thus ?case by blast
next
case (4 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 4 have nb: "numbound0 e" by simp
+  from 4 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1223,8 +1229,8 @@
thus ?case by blast
next
case (5 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 5 have nb: "numbound0 e" by simp
+  from 5 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1239,8 +1245,8 @@
thus ?case by blast
next
case (6 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 6 have nb: "numbound0 e" by simp
+  from 6 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1255,8 +1261,8 @@
thus ?case by blast
next
case (7 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 7 have nb: "numbound0 e" by simp
+  from 7 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1271,8 +1277,8 @@
thus ?case by blast
next
case (8 c e)
-  from prems have nb: "numbound0 e" by simp
-  from prems have cp: "real c > 0" by simp
+  from 8 have nb: "numbound0 e" by simp
+  from 8 have cp: "real c > 0" by simp
fix a
let ?e="Inum (a#bs) e"
let ?z = "(- ?e) / real c"
@@ -1356,7 +1362,7 @@
shows "(Ifm (x#bs) (usubst p (t,n)) = Ifm (((Inum (x#bs) t)/(real n))#bs) p) \<and> bound0 (usubst p (t,n))" (is "(?I x (usubst p (t,n)) = ?I ?u p) \<and> ?B p" is "(_ = ?I (?t/?n) p) \<and> _" is "(_ = ?I (?N x t /_) p) \<and> _")
using lp
proof(induct p rule: usubst.induct)
-  case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
+  case (5 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)"
@@ -1366,7 +1372,7 @@
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
-  case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
+  case (6 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
@@ -1376,7 +1382,7 @@
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
-  case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
+  case (7 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)"
@@ -1386,7 +1392,7 @@
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
-  case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
+  case (8 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
@@ -1396,7 +1402,7 @@
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
-  case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
+  case (3 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
from np have np: "real n \<noteq> 0" by simp
have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
@@ -1407,7 +1413,7 @@
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
-  case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
+  case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
from np have np: "real n \<noteq> 0" by simp
have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)"
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
@@ -1467,99 +1473,99 @@
using lp px noS
proof (induct p rule: isrlfm.induct)
case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps)
-    hence pxc: "x < (- ?N x e) / real c"
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
-    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
-    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
-    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
-    moreover {assume y: "y < (-?N x e)/ real c"
-      hence "y * real c < - ?N x e"
-        by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
-      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
-    moreover {assume y: "y > (- ?N x e) / real c"
-      with yu have eu: "u > (- ?N x e) / real c" by auto
-      with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
-      with lx pxc have "False" by auto
-      hence ?case by simp }
-    ultimately show ?case by blast
+  from 5 have "x * real c + ?N x e < 0" by (simp add: algebra_simps)
+  hence pxc: "x < (- ?N x e) / real c"
+    by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
+  from 5 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
+  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
+  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
+  moreover {assume y: "y < (-?N x e)/ real c"
+    hence "y * real c < - ?N x e"
+      by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
+    hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
+    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
+  moreover {assume y: "y > (- ?N x e) / real c"
+    with yu have eu: "u > (- ?N x e) / real c" by auto
+    with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
+    with lx pxc have "False" by auto
+    hence ?case by simp }
+  ultimately show ?case by blast
next
case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp +
-    from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps)
-    hence pxc: "x \<le> (- ?N x e) / real c"
-      by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
-    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
-    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
-    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
-    moreover {assume y: "y < (-?N x e)/ real c"
-      hence "y * real c < - ?N x e"
-        by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
-      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
-    moreover {assume y: "y > (- ?N x e) / real c"
-      with yu have eu: "u > (- ?N x e) / real c" by auto
-      with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
-      with lx pxc have "False" by auto
-      hence ?case by simp }
-    ultimately show ?case by blast
+  from 6 have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps)
+  hence pxc: "x \<le> (- ?N x e) / real c"
+    by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
+  from 6 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
+  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
+  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
+  moreover {assume y: "y < (-?N x e)/ real c"
+    hence "y * real c < - ?N x e"
+      by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
+    hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
+    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
+  moreover {assume y: "y > (- ?N x e) / real c"
+    with yu have eu: "u > (- ?N x e) / real c" by auto
+    with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
+    with lx pxc have "False" by auto
+    hence ?case by simp }
+  ultimately show ?case by blast
next
case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps)
-    hence pxc: "x > (- ?N x e) / real c"
-      by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
-    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
-    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
-    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
-    moreover {assume y: "y > (-?N x e)/ real c"
-      hence "y * real c > - ?N x e"
-        by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
-      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
-    moreover {assume y: "y < (- ?N x e) / real c"
-      with ly have eu: "l < (- ?N x e) / real c" by auto
-      with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
-      with xu pxc have "False" by auto
-      hence ?case by simp }
-    ultimately show ?case by blast
+  from 7 have "x * real c + ?N x e > 0" by (simp add: algebra_simps)
+  hence pxc: "x > (- ?N x e) / real c"
+    by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
+  from 7 have noSc: "\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
+  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
+  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
+  moreover {assume y: "y > (-?N x e)/ real c"
+    hence "y * real c > - ?N x e"
+      by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
+    hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
+    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
+  moreover {assume y: "y < (- ?N x e) / real c"
+    with ly have eu: "l < (- ?N x e) / real c" by auto
+    with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
+    with xu pxc have "False" by auto
+    hence ?case by simp }
+  ultimately show ?case by blast
next
case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps)
-    hence pxc: "x \<ge> (- ?N x e) / real c"
-      by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
-    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
-    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
-    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
-    moreover {assume y: "y > (-?N x e)/ real c"
-      hence "y * real c > - ?N x e"
-        by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
-      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
-    moreover {assume y: "y < (- ?N x e) / real c"
-      with ly have eu: "l < (- ?N x e) / real c" by auto
-      with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
-      with xu pxc have "False" by auto
-      hence ?case by simp }
-    ultimately show ?case by blast
+  from 8 have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps)
+  hence pxc: "x \<ge> (- ?N x e) / real c"
+    by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
+  from 8 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
+  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
+  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
+  moreover {assume y: "y > (-?N x e)/ real c"
+    hence "y * real c > - ?N x e"
+      by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
+    hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
+    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
+  moreover {assume y: "y < (- ?N x e) / real c"
+    with ly have eu: "l < (- ?N x e) / real c" by auto
+    with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
+    with xu pxc have "False" by auto
+    hence ?case by simp }
+  ultimately show ?case by blast
next
case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from cp have cnz: "real c \<noteq> 0" by simp
-    from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps)
-    hence pxc: "x = (- ?N x e) / real c"
-      by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
-    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
-    with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto
-    with pxc show ?case by simp
+  from cp have cnz: "real c \<noteq> 0" by simp
+  from 3 have "x * real c + ?N x e = 0" by (simp add: algebra_simps)
+  hence pxc: "x = (- ?N x e) / real c"
+    by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
+  from 3 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
+  with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto
+  with pxc show ?case by simp
next
case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from cp have cnz: "real c \<noteq> 0" by simp
-    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
-    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
-    hence "y* real c \<noteq> -?N x e"
-      by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
-    hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
-    thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
-      by (simp add: algebra_simps)
+  from cp have cnz: "real c \<noteq> 0" by simp
+  from 4 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
+  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
+  hence "y* real c \<noteq> -?N x e"
+    by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
+  hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
+  thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
+    by (simp add: algebra_simps)
qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])

lemma finite_set_intervals:```
```--- a/src/HOL/Decision_Procs/MIR.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Feb 21 23:54:53 2011 +0100
@@ -46,7 +46,7 @@
proof(induct rule: iupt.induct)
case (1 a b)
show ?case
-    using prems by (simp add: simp_from_to)
+    using 1 by (simp add: simp_from_to)
qed

lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
@@ -119,7 +119,7 @@
assume "?r" hence "(i\<Colon>int) dvd \<lfloor>x\<Colon>real\<rfloor>" ..
hence "\<exists> k. real (floor x) = real (i*k)"
by (simp only: real_of_int_inject) (simp add: dvd_def)
-  thus ?l using prems by (simp add: rdvd_def)
+  thus ?l using `?r` by (simp add: rdvd_def)
qed

lemma int_rdvd_iff: "(real (i::int) rdvd real t) = (i dvd t)"
@@ -705,16 +705,17 @@
proof(induct t rule: reducecoeffh.induct)
case (1 i) hence gd: "g dvd i" by simp
from gp have gnz: "g \<noteq> 0" by simp
-  from prems show ?case by (simp add: real_of_int_div[OF gnz gd])
+  from assms 1 show ?case by (simp add: real_of_int_div[OF gnz gd])
next
case (2 n c t)  hence gd: "g dvd c" by simp
from gp have gnz: "g \<noteq> 0" by simp
-  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
+  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
next
case (3 c s t)  hence gd: "g dvd c" by simp
from gp have gnz: "g \<noteq> 0" by simp
-  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
+  from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
qed (auto simp add: numgcd_def gp)
+
consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
recdef ismaxcoeff "measure size"
"ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"
@@ -729,7 +730,7 @@
proof (induct t rule: maxcoeff.induct)
case (2 n c t)
hence H:"ismaxcoeff t (maxcoeff t)" .
-  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2)
+  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp
from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
next
case (3 c t s)
@@ -747,60 +748,60 @@
apply auto
done
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
-  by (induct t rule: numgcdh.induct, auto)
+  by (induct t rule: numgcdh.induct) auto

lemma dvdnumcoeff_aux:
assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
shows "dvdnumcoeff t (numgcdh t m)"
-using prems
+using assms
proof(induct t rule: numgcdh.induct)
case (2 n c t)
let ?g = "numgcdh t m"
-  from prems have th:"gcd c ?g > 1" by simp
+  from 2 have th:"gcd c ?g > 1" by simp
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
-  moreover {assume "abs c > 1" and gp: "?g > 1" with prems
+  moreover {assume "abs c > 1" and gp: "?g > 1" with 2
have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp }
moreover {assume "abs c = 0 \<and> ?g > 1"
-    with prems have th: "dvdnumcoeff t ?g" by simp
+    with 2 have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
-    from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
+    from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp }
ultimately show ?case by blast
next
case (3 c s t)
let ?g = "numgcdh t m"
-  from prems have th:"gcd c ?g > 1" by simp
+  from 3 have th:"gcd c ?g > 1" by simp
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
-  moreover {assume "abs c > 1" and gp: "?g > 1" with prems
+  moreover {assume "abs c > 1" and gp: "?g > 1" with 3
have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp }
moreover {assume "abs c = 0 \<and> ?g > 1"
-    with prems have th: "dvdnumcoeff t ?g" by simp
+    with 3 have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
-    from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
+    from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp }
ultimately show ?case by blast
qed auto

lemma dvdnumcoeff_aux2:
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
-  using prems
+  using assms
proof (simp add: numgcd_def)
let ?mc = "maxcoeff t"
let ?g = "numgcdh t ?mc"
have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff)
have th2: "?mc \<ge> 0" by (rule maxcoeff_pos)
assume H: "numgcdh t ?mc > 1"
-  from dvdnumcoeff_aux[OF th1 th2 H]  show "dvdnumcoeff t ?g" .
+  from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" .
qed

lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t"
@@ -911,32 +912,33 @@
in (bv, CF c a bi))"
"split_int a = (a,C 0)"

-lemma split_int:"\<And> tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs"
+lemma split_int: "\<And>tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs"
proof (induct t rule: split_int.induct)
case (2 c n b tv ti)
let ?bv = "fst (split_int b)"
let ?bi = "snd (split_int b)"
have "split_int b = (?bv,?bi)" by simp
-  with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
-  from prems(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def)
-  from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def)
+  with 2(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
+  from 2(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def)
+  from 2(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def)
next
case (3 c a b tv ti)
let ?bv = "fst (split_int b)"
let ?bi = "snd (split_int b)"
have "split_int b = (?bv,?bi)" by simp
-  with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
-  from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def)
-  from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF)
+  with 3(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
+  from 3(2) have tibi: "ti = CF c a ?bi"
+    by (simp add: Let_def split_def)
+  from 3(2) b[symmetric] bii show ?case
+    by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF)
qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps)

lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) "
-by (induct t rule: split_int.induct, auto simp add: Let_def split_def)
-
-definition
-  numfloor:: "num \<Rightarrow> num"
+  by (induct t rule: split_int.induct) (auto simp add: Let_def split_def)
+
+definition numfloor:: "num \<Rightarrow> num"
where
-  numfloor_def: "numfloor t = (let (tv,ti) = split_int t in
+  "numfloor t = (let (tv,ti) = split_int t in
(case tv of C i \<Rightarrow> numadd (tv,ti)
| _ \<Rightarrow> numadd(CF 1 tv (C 0),ti)))"

@@ -1022,13 +1024,13 @@
hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)
with cnz have "max (abs c) (maxcoeff t) > 0" by arith
-  with prems show ?case by simp
+  with 2 show ?case by simp
next
case (3 c s t)
hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)
with cnz have "max (abs c) (maxcoeff t) > 0" by arith
-  with prems show ?case by simp
+  with 3 show ?case by simp
qed auto

lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0"
@@ -1072,34 +1074,35 @@
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs ?t'" by simp
-        from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
+        from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
also have "\<dots> = (Inum bs ?t' / real n)"
using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
finally have "?lhs = Inum bs t / real n" by simp
-        then have ?thesis using prems by (simp add: simp_num_pair_def)}
-      ultimately have ?thesis by blast}
-    ultimately have ?thesis by blast}
+        then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
+      ultimately have ?thesis by blast }
+    ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed

-lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')"
+lemma simp_num_pair_l:
+  assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')"
shows "numbound0 t' \<and> n' >0"
proof-
-    let ?t' = "simpnum t"
+  let ?t' = "simpnum t"
let ?g = "numgcd ?t'"
let ?g' = "gcd n ?g"
-  {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
+  { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) }
moreover
{ assume nnz: "n \<noteq> 0"
-    {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def)}
+    {assume "\<not> ?g > 1" hence ?thesis using assms by (auto simp add: Let_def simp_num_pair_def) }
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
from g1 nnz have gp0: "?g' \<noteq> 0" by simp
hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
-      moreover {assume "?g'=1" hence ?thesis using prems
-          by (auto simp add: Let_def simp_num_pair_def)}
+      moreover {assume "?g'=1" hence ?thesis using assms g1 g0
+          by (auto simp add: Let_def simp_num_pair_def) }
moreover {assume g'1:"?g'>1"
have gpdg: "?g' dvd ?g" by simp
have gpdd: "?g' dvd n" by simp
@@ -1107,10 +1110,10 @@
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
have "n div ?g' >0" by simp
-        hence ?thesis using prems
+        hence ?thesis using assms g1 g'1
by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
-      ultimately have ?thesis by blast}
-    ultimately have ?thesis by blast}
+      ultimately have ?thesis by blast }
+    ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed

@@ -1131,43 +1134,43 @@
"not (Or p q) = And (not p) (not q)"
"not p = NOT p"
lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"
-by (induct p) auto
+  by (induct p) auto
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
-by (induct p, auto)
+  by (induct p) auto
lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"
-by (induct p, auto)
+  by (induct p) auto

definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
"conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else
if p = q then p else And p q)"
lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"
-by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
+  by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)

lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"
-using conj_def by auto
+  using conj_def by auto
lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"
-using conj_def by auto
+  using conj_def by auto

definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
"disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p
else if p=q then p else Or p q)"

lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"
-by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
+  by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
-using disj_def by auto
+  using disj_def by auto
lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
-using disj_def by auto
+  using disj_def by auto

definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
"imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p
else Imp p q)"
lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
-by (cases "p=F \<or> q=T",simp_all add: imp_def)
+  by (cases "p=F \<or> q=T",simp_all add: imp_def)
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
-using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
+  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
-using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def)
+  using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def)

definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
"iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else
@@ -1245,7 +1248,8 @@
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs t" by simp
-      from prems have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"
+      from assms g1 g0 g'1
+      have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"
by (simp add: simpdvd_def Let_def)
also have "\<dots> = (real d rdvd (Inum bs t))"
using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]]
@@ -1544,9 +1548,8 @@
lemma qelim_ci:
assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)"
-using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]]
-by(induct p rule: qelim.induct)
-(auto simp del: simpfm.simps)
+  using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]]
+  by (induct p rule: qelim.induct) (auto simp del: simpfm.simps)

text {* The @{text "\<int>"} Part *}
@@ -1584,7 +1587,7 @@
case (5 t n a)
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
-  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems
+  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 5
by (simp add: Let_def split_def)
from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
from th2[simplified] th[simplified] show ?case by simp```
```--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:54:53 2011 +0100
@@ -144,11 +144,10 @@
{assume nxs: "n \<ge> length (x#xs)" hence ?case using removen_same[OF nxs] by simp}
moreover
{assume nxs: "\<not> (n \<ge> length (x#xs))"
-    {assume mln: "m < n" hence ?case using prems by (cases m, auto)}
+    {assume mln: "m < n" hence ?case using Cons by (cases m, auto)}
moreover
{assume mln: "\<not> (m < n)"
-
-      {assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)}
+      {assume mxs: "m \<le> length (x#xs)" hence ?case using Cons by (cases m, auto)}
moreover
{assume mxs: "\<not> (m \<le> length (x#xs))"
have th: "length (removen n (x#xs)) = length xs"
@@ -162,15 +161,13 @@
ultimately have ?case by blast
}
ultimately have ?case by blast
-
-  }      ultimately show ?case by blast
+  } ultimately show ?case by blast
qed

lemma decrtm: assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound m t"
and nle: "m \<le> length bs"
shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
-  using bnd nb nle
-  by (induct t rule: tm.induct, auto simp add: removen_nth)
+  using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)

primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
"tmsubst0 t (CP c) = CP c"
@@ -182,10 +179,10 @@
| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
lemma tmsubst0:
shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+  by (induct a rule: tm.induct) (auto simp add: nth_pos2)

lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+  by (induct a rule: tm.induct) (auto simp add: nth_pos2)

primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
"tmsubst n t (CP c) = CP c"
@@ -569,13 +566,13 @@
proof(induct p arbitrary: bs n rule: fm.induct)
case (E p bs n)
{fix y
-    from prems have bnd: "boundslt (length (y#bs)) p"
+    from E have bnd: "boundslt (length (y#bs)) p"
and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
thus ?case by simp
next
case (A p bs n) {fix y
-    from prems have bnd: "boundslt (length (y#bs)) p"
+    from A have bnd: "boundslt (length (y#bs)) p"
and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
thus ?case by simp
@@ -620,16 +617,16 @@
proof(induct p arbitrary: bs m rule: fm.induct)
case (E p bs m)
{fix x
-    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p"
+    from E have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p"
and nle: "Suc m < length (x#bs)" by auto
-    from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
+    from E(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
} thus ?case by auto
next
case (A p bs m)
{fix x
-    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p"
+    from A have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p"
and nle: "Suc m < length (x#bs)" by auto
-    from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
+    from A(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
} thus ?case by auto
qed (auto simp add: decrtm removen_nth)

@@ -680,18 +677,18 @@
proof (induct p arbitrary: bs n t rule: fm.induct)
case (E p bs n)
{fix x
-    from prems have bn: "boundslt (length (x#bs)) p" by simp
-      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
-    from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp
+    from E have bn: "boundslt (length (x#bs)) p" by simp
+    from E have nlm: "Suc n \<le> length (x#bs)" by simp
+    from E(1)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp
hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }
thus ?case by simp
next
case (A p bs n)
{fix x
-    from prems have bn: "boundslt (length (x#bs)) p" by simp
-      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
-    from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp
+    from A have bn: "boundslt (length (x#bs)) p" by simp
+    from A have nlm: "Suc n \<le> length (x#bs)" by simp
+    from A(1)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp
hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }
thus ?case by simp
@@ -1371,7 +1368,7 @@
case 2 thus ?case by (auto,rule_tac x="min z za" in exI, auto)
next
case (3 c e) hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"
let ?e = "Itm vs (y#bs) e"
@@ -1393,7 +1390,7 @@
ultimately show ?case by blast
next
case (4 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"
let ?e = "Itm vs (y#bs) e"
@@ -1414,7 +1411,7 @@
ultimately show ?case by blast
next
case (5 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"
@@ -1436,7 +1433,7 @@
ultimately show ?case by blast
next
case (6 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"
@@ -1467,7 +1464,7 @@
case 2 thus ?case by (auto,rule_tac x="max z za" in exI, auto)
next
case (3 c e) hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"
let ?e = "Itm vs (y#bs) e"
@@ -1488,8 +1485,8 @@
using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
ultimately show ?case by blast
next
-  case (4 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  case (4 c e) hence nbe: "tmbound0 e" by simp
+  from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"
let ?e = "Itm vs (y#bs) e"
@@ -1509,8 +1506,8 @@
using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
ultimately show ?case by blast
next
-  case (5 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  case (5 c e) hence nbe: "tmbound0 e" by simp
+  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
note eqs = lt[OF nc(1), where ?'a = 'a] lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"
@@ -1532,7 +1529,7 @@
ultimately show ?case by blast
next
case (6 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
note eqs = lt[OF nc(1), where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
let ?c = "Ipoly vs c"```