tuned proofs -- eliminated prems;
authorwenzelm
Mon Feb 21 23:47:19 2011 +0100 (2011-02-21)
changeset 41807ab5d2d81f9fb
parent 41806 173e1b50d5c5
child 41816 7a55699805dc
tuned proofs -- eliminated prems;
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Feb 21 18:29:47 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Feb 21 23:47:19 2011 +0100
     1.3 @@ -308,7 +308,7 @@
     1.4    assumes "norm P1 = norm P2"
     1.5    shows "Ipolex l P1 = Ipolex l P2"
     1.6  proof -
     1.7 -  from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
     1.8 +  from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
     1.9    then show ?thesis by (simp only: norm_ci)
    1.10  qed
    1.11  
     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Mon Feb 21 18:29:47 2011 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Mon Feb 21 23:47:19 2011 +0100
     2.3 @@ -50,23 +50,25 @@
     2.4    assumes A:"isnorm (PX P x Q)" and "isnorm Q2" 
     2.5    shows "isnorm (PX P x Q2)"
     2.6  proof(cases P)
     2.7 -  case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto)
     2.8 +  case (PX p1 y p2) with assms show ?thesis by(cases x, auto, cases p2, auto)
     2.9  next
    2.10 -  case Pc from prems show ?thesis by(cases x, auto)
    2.11 +  case Pc with assms show ?thesis by (cases x) auto
    2.12  next
    2.13 -  case Pinj from prems show ?thesis by(cases x, auto)
    2.14 +  case Pinj with assms show ?thesis by (cases x) auto
    2.15  qed
    2.16   
    2.17 -lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)"
    2.18 -proof(cases P)
    2.19 +lemma norm_PXtrans2:
    2.20 +  assumes "isnorm (PX P x Q)" and "isnorm Q2"
    2.21 +  shows "isnorm (PX P (Suc (n+x)) Q2)"
    2.22 +proof (cases P)
    2.23    case (PX p1 y p2)
    2.24 -  from prems show ?thesis by(cases x, auto, cases p2, auto)
    2.25 +  with assms show ?thesis by (cases x, auto, cases p2, auto)
    2.26  next
    2.27    case Pc
    2.28 -  from prems show ?thesis by(cases x, auto)
    2.29 +  with assms show ?thesis by (cases x) auto
    2.30  next
    2.31    case Pinj
    2.32 -  from prems show ?thesis by(cases x, auto)
    2.33 +  with assms show ?thesis by (cases x) auto
    2.34  qed
    2.35  
    2.36  text {* mkPX conserves normalizedness (@{text "_cn"}) *}
    2.37 @@ -75,15 +77,17 @@
    2.38    shows "isnorm (mkPX P x Q)"
    2.39  proof(cases P)
    2.40    case (Pc c)
    2.41 -  from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    2.42 +  with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    2.43  next
    2.44    case (Pinj i Q)
    2.45 -  from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    2.46 +  with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    2.47  next
    2.48    case (PX P1 y P2)
    2.49 -  from prems have Y0:"y>0" by(cases y, auto)
    2.50 -  from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
    2.51 -  with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
    2.52 +  with assms have Y0: "y>0" by (cases y) auto
    2.53 +  from assms PX have "isnorm P1" "isnorm P2"
    2.54 +    by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
    2.55 +  from assms PX Y0 show ?thesis
    2.56 +    by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
    2.57  qed
    2.58  
    2.59  text {* add conserves normalizedness *}
    2.60 @@ -94,118 +98,127 @@
    2.61    case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
    2.62  next
    2.63    case (4 c P2 i Q2)
    2.64 -  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
    2.65 -  with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
    2.66 +  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
    2.67 +  with 4 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
    2.68  next
    2.69    case (5 P2 i Q2 c)
    2.70 -  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
    2.71 -  with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
    2.72 +  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
    2.73 +  with 5 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
    2.74  next
    2.75    case (6 x P2 y Q2)
    2.76 -  from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False) 
    2.77 -  from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False) 
    2.78 +  then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
    2.79 +  with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False)
    2.80    have "x < y \<or> x = y \<or> x > y" by arith
    2.81    moreover
    2.82 -  { assume "x<y" hence "EX d. y=d+x" by arith
    2.83 -    then obtain d where "y=d+x"..
    2.84 +  { assume "x<y" hence "EX d. y =d + x" by arith
    2.85 +    then obtain d where y: "y = d + x" ..
    2.86      moreover
    2.87 -    note prems X0
    2.88 +    note 6 X0
    2.89      moreover
    2.90 -    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
    2.91 +    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
    2.92      moreover
    2.93 -    with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
    2.94 -    ultimately have ?case by (simp add: mkPinj_cn)}
    2.95 +    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
    2.96 +    ultimately have ?case by (simp add: mkPinj_cn) }
    2.97    moreover
    2.98    { assume "x=y"
    2.99      moreover
   2.100 -    from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.101 +    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.102      moreover
   2.103 -    note prems Y0
   2.104 +    note 6 Y0
   2.105      moreover
   2.106      ultimately have ?case by (simp add: mkPinj_cn) }
   2.107    moreover
   2.108 -  { assume "x>y" hence "EX d. x=d+y" by arith
   2.109 -    then obtain d where "x=d+y"..
   2.110 +  { assume "x>y" hence "EX d. x = d + y" by arith
   2.111 +    then obtain d where x: "x = d + y"..
   2.112      moreover
   2.113 -    note prems Y0
   2.114 +    note 6 Y0
   2.115      moreover
   2.116 -    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.117 +    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.118      moreover
   2.119 -    with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
   2.120 +    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
   2.121      ultimately have ?case by (simp add: mkPinj_cn)}
   2.122    ultimately show ?case by blast
   2.123  next
   2.124    case (7 x P2 Q2 y R)
   2.125    have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
   2.126    moreover
   2.127 -  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
   2.128 +  { assume "x = 0"
   2.129 +    with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
   2.130    moreover
   2.131 -  { assume "x=1"
   2.132 -    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.133 -    with prems have "isnorm (R \<oplus> P2)" by simp
   2.134 -    with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.135 +  { assume "x = 1"
   2.136 +    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.137 +    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
   2.138 +    with 7 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.139    moreover
   2.140    { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
   2.141      then obtain d where X:"x=Suc (Suc d)" ..
   2.142 -    from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.143 -    with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
   2.144 -    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
   2.145 -    with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.146 +    with 7 have NR: "isnorm R" "isnorm P2"
   2.147 +      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.148 +    with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   2.149 +    with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
   2.150 +    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.151    ultimately show ?case by blast
   2.152  next
   2.153    case (8 Q2 y R x P2)
   2.154    have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   2.155    moreover
   2.156 -  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
   2.157 +  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
   2.158    moreover
   2.159 -  { assume "x=1"
   2.160 -    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.161 -    with prems have "isnorm (R \<oplus> P2)" by simp
   2.162 -    with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.163 +  { assume "x = 1"
   2.164 +    with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.165 +    with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp
   2.166 +    with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.167    moreover
   2.168    { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
   2.169 -    then obtain d where X:"x=Suc (Suc d)" ..
   2.170 -    from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.171 -    with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
   2.172 -    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
   2.173 -    with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.174 +    then obtain d where X: "x = Suc (Suc d)" ..
   2.175 +    with 8 have NR: "isnorm R" "isnorm P2"
   2.176 +      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.177 +    with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   2.178 +    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
   2.179 +    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   2.180    ultimately show ?case by blast
   2.181  next
   2.182    case (9 P1 x P2 Q1 y Q2)
   2.183 -  from prems have Y0:"y>0" by(cases y, auto)
   2.184 -  from prems have X0:"x>0" by(cases x, auto)
   2.185 -  from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
   2.186 -  from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
   2.187 +  then have Y0: "y>0" by (cases y) auto
   2.188 +  with 9 have X0: "x>0" by (cases x) auto
   2.189 +  with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
   2.190 +    by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
   2.191 +  with 9 have NQ1:"isnorm Q1" and NQ2: "isnorm Q2"
   2.192 +    by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
   2.193    have "y < x \<or> x = y \<or> x < y" by arith
   2.194    moreover
   2.195 -  {assume sm1:"y < x" hence "EX d. x=d+y" by arith
   2.196 -    then obtain d where sm2:"x=d+y"..
   2.197 -    note prems NQ1 NP1 NP2 NQ2 sm1 sm2
   2.198 +  { assume sm1: "y < x" hence "EX d. x = d + y" by arith
   2.199 +    then obtain d where sm2: "x = d + y" ..
   2.200 +    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
   2.201      moreover
   2.202      have "isnorm (PX P1 d (Pc 0))" 
   2.203 -    proof(cases P1)
   2.204 +    proof (cases P1)
   2.205        case (PX p1 y p2)
   2.206 -      with prems show ?thesis by(cases d, simp,cases p2, auto)
   2.207 -    next case Pc   from prems show ?thesis by(cases d, auto)
   2.208 -    next case Pinj from prems show ?thesis by(cases d, auto)
   2.209 +      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
   2.210 +    next
   2.211 +      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
   2.212 +    next
   2.213 +      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
   2.214      qed
   2.215      ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
   2.216 -    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
   2.217 +    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
   2.218    moreover
   2.219 -  {assume "x=y"
   2.220 -    from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
   2.221 -    with Y0 prems have ?case by (simp add: mkPX_cn) }
   2.222 +  { assume "x = y"
   2.223 +    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
   2.224 +    with `x = y` Y0 have ?case by (simp add: mkPX_cn) }
   2.225    moreover
   2.226 -  {assume sm1:"x<y" hence "EX d. y=d+x" by arith
   2.227 -    then obtain d where sm2:"y=d+x"..
   2.228 -    note prems NQ1 NP1 NP2 NQ2 sm1 sm2
   2.229 +  { assume sm1: "x < y" hence "EX d. y = d + x" by arith
   2.230 +    then obtain d where sm2: "y = d + x" ..
   2.231 +    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
   2.232      moreover
   2.233      have "isnorm (PX Q1 d (Pc 0))" 
   2.234 -    proof(cases Q1)
   2.235 +    proof (cases Q1)
   2.236        case (PX p1 y p2)
   2.237 -      with prems show ?thesis by(cases d, simp,cases p2, auto)
   2.238 -    next case Pc   from prems show ?thesis by(cases d, auto)
   2.239 -    next case Pinj from prems show ?thesis by(cases d, auto)
   2.240 +      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
   2.241 +    next
   2.242 +      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
   2.243 +    next
   2.244 +      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
   2.245      qed
   2.246      ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
   2.247      with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
   2.248 @@ -222,138 +235,141 @@
   2.249      by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
   2.250  next
   2.251    case (4 c P2 i Q2)
   2.252 -  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   2.253 -  with prems show ?case 
   2.254 -    by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
   2.255 +  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   2.256 +  with 4 show ?case 
   2.257 +    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
   2.258  next
   2.259    case (5 P2 i Q2 c)
   2.260 -  from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   2.261 -  with prems show ?case
   2.262 -    by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
   2.263 +  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   2.264 +  with 5 show ?case
   2.265 +    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
   2.266  next
   2.267    case (6 x P2 y Q2)
   2.268    have "x < y \<or> x = y \<or> x > y" by arith
   2.269    moreover
   2.270 -  { assume "x<y" hence "EX d. y=d+x" by arith
   2.271 -    then obtain d where "y=d+x"..
   2.272 +  { assume "x < y" hence "EX d. y = d + x" by arith
   2.273 +    then obtain d where y: "y = d + x" ..
   2.274      moreover
   2.275 -    note prems
   2.276 +    note 6
   2.277      moreover
   2.278 -    from prems have "x>0" by (cases x, auto simp add: norm_Pinj_0_False) 
   2.279 +    from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False)
   2.280      moreover
   2.281 -    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.282 +    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.283      moreover
   2.284 -    with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto) 
   2.285 -    ultimately have ?case by (simp add: mkPinj_cn)}
   2.286 +    from 6 `x < y` y have "isnorm (Pinj d Q2)" by - (cases d, simp, cases Q2, auto) 
   2.287 +    ultimately have ?case by (simp add: mkPinj_cn) }
   2.288    moreover
   2.289 -  { assume "x=y"
   2.290 +  { assume "x = y"
   2.291      moreover
   2.292 -    from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.293 +    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.294      moreover
   2.295 -    with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
   2.296 +    from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
   2.297      moreover
   2.298 -    note prems
   2.299 +    note 6
   2.300      moreover
   2.301      ultimately have ?case by (simp add: mkPinj_cn) }
   2.302    moreover
   2.303 -  { assume "x>y" hence "EX d. x=d+y" by arith
   2.304 -    then obtain d where "x=d+y"..
   2.305 +  { assume "x > y" hence "EX d. x = d + y" by arith
   2.306 +    then obtain d where x: "x = d + y" ..
   2.307      moreover
   2.308 -    note prems
   2.309 +    note 6
   2.310      moreover
   2.311 -    from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False) 
   2.312 +    from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)
   2.313      moreover
   2.314 -    from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.315 +    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   2.316      moreover
   2.317 -    with prems have "isnorm (Pinj d P2)"  by (cases d, simp, cases P2, auto)
   2.318 +    from 6 `x > y` x have "isnorm (Pinj d P2)" by - (cases d, simp, cases P2, auto)
   2.319      ultimately have ?case by (simp add: mkPinj_cn) }
   2.320    ultimately show ?case by blast
   2.321  next
   2.322    case (7 x P2 Q2 y R)
   2.323 -  from prems have Y0:"y>0" by(cases y, auto)
   2.324 -  have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
   2.325 +  then have Y0: "y > 0" by (cases y) auto
   2.326 +  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   2.327    moreover
   2.328 -  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
   2.329 +  { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
   2.330    moreover
   2.331 -  { assume "x=1"
   2.332 -    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.333 -    with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
   2.334 -    with Y0 prems have ?case by (simp add: mkPX_cn)}
   2.335 +  { assume "x = 1"
   2.336 +    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.337 +    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
   2.338 +    with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
   2.339    moreover
   2.340 -  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
   2.341 -    then obtain d where X:"x=Suc (Suc d)" ..
   2.342 -    from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
   2.343 -    moreover
   2.344 -    from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
   2.345 +  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
   2.346 +    then obtain d where X: "x = Suc (Suc d)" ..
   2.347 +    from 7 have NR: "isnorm R" "isnorm Q2"
   2.348 +      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
   2.349      moreover
   2.350 -    from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
   2.351 +    from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   2.352 +    moreover
   2.353 +    from 7 have "isnorm (Pinj x P2)" by (cases P2) auto
   2.354      moreover
   2.355 -    note prems
   2.356 +    note 7 X
   2.357      ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
   2.358 -    with Y0 X have ?case by (simp add: mkPX_cn)}
   2.359 +    with Y0 X have ?case by (simp add: mkPX_cn) }
   2.360    ultimately show ?case by blast
   2.361  next
   2.362    case (8 Q2 y R x P2)
   2.363 -  from prems have Y0:"y>0" by(cases y, auto)
   2.364 -  have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
   2.365 +  then have Y0: "y>0" by (cases y) auto
   2.366 +  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   2.367    moreover
   2.368 -  { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
   2.369 +  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
   2.370    moreover
   2.371 -  { assume "x=1"
   2.372 -    from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.373 -    with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
   2.374 -    with Y0 prems have ?case by (simp add: mkPX_cn) }
   2.375 +  { assume "x = 1"
   2.376 +    from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   2.377 +    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
   2.378 +    with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
   2.379    moreover
   2.380 -  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
   2.381 -    then obtain d where X:"x=Suc (Suc d)" ..
   2.382 -    from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
   2.383 +  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
   2.384 +    then obtain d where X: "x = Suc (Suc d)" ..
   2.385 +    from 8 have NR: "isnorm R" "isnorm Q2"
   2.386 +      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
   2.387      moreover
   2.388 -    from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
   2.389 +    from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   2.390      moreover
   2.391 -    from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
   2.392 +    from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
   2.393      moreover
   2.394 -    note prems
   2.395 +    note 8 X
   2.396      ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
   2.397      with Y0 X have ?case by (simp add: mkPX_cn) }
   2.398    ultimately show ?case by blast
   2.399  next
   2.400    case (9 P1 x P2 Q1 y Q2)
   2.401 -  from prems have X0:"x>0" by(cases x, auto)
   2.402 -  from prems have Y0:"y>0" by(cases y, auto)
   2.403 -  note prems
   2.404 +  from 9 have X0: "x > 0" by (cases x) auto
   2.405 +  from 9 have Y0: "y > 0" by (cases y) auto
   2.406 +  note 9
   2.407    moreover
   2.408 -  from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   2.409 +  from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   2.410    moreover 
   2.411 -  from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
   2.412 +  from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
   2.413    ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
   2.414      "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" 
   2.415      by (auto simp add: mkPinj_cn)
   2.416 -  with prems X0 Y0 have
   2.417 +  with 9 X0 Y0 have
   2.418      "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
   2.419      "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"  
   2.420      "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" 
   2.421      by (auto simp add: mkPX_cn)
   2.422    thus ?case by (simp add: add_cn)
   2.423 -qed(simp)
   2.424 +qed simp
   2.425  
   2.426  text {* neg conserves normalizedness *}
   2.427  lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
   2.428  proof (induct P)
   2.429    case (Pinj i P2)
   2.430 -  from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2])
   2.431 -  with prems show ?case by(cases P2, auto, cases i, auto)
   2.432 +  then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
   2.433 +  with Pinj show ?case by - (cases P2, auto, cases i, auto)
   2.434  next
   2.435 -  case (PX P1 x P2)
   2.436 -  from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   2.437 -  with prems show ?case
   2.438 -  proof(cases P1)
   2.439 +  case (PX P1 x P2) note PX1 = this
   2.440 +  from PX have "isnorm P2" "isnorm P1"
   2.441 +    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   2.442 +  with PX show ?case
   2.443 +  proof (cases P1)
   2.444      case (PX p1 y p2)
   2.445 -    with prems show ?thesis by(cases x, auto, cases p2, auto)
   2.446 +    with PX1 show ?thesis by - (cases x, auto, cases p2, auto)
   2.447    next
   2.448      case Pinj
   2.449 -    with prems show ?thesis by(cases x, auto)
   2.450 -  qed(cases x, auto)
   2.451 -qed(simp)
   2.452 +    with PX1 show ?thesis by (cases x) auto
   2.453 +  qed (cases x, auto)
   2.454 +qed simp
   2.455  
   2.456  text {* sub conserves normalizedness *}
   2.457  lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
   2.458 @@ -361,17 +377,18 @@
   2.459  
   2.460  text {* sqr conserves normalizizedness *}
   2.461  lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
   2.462 -proof(induct P)
   2.463 +proof (induct P)
   2.464    case (Pinj i Q)
   2.465 -  from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
   2.466 +  then show ?case
   2.467 +    by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
   2.468  next 
   2.469    case (PX P1 x P2)
   2.470 -  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])
   2.471 -  with prems have
   2.472 -    "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
   2.473 -    and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
   2.474 -   by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   2.475 -  thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   2.476 +  then have "x + x ~= 0" "isnorm P2" "isnorm P1"
   2.477 +    by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   2.478 +  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
   2.479 +      and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
   2.480 +    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   2.481 +  then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   2.482  qed simp
   2.483  
   2.484  text {* pow conserves normalizedness *}
   2.485 @@ -379,12 +396,12 @@
   2.486  proof (induct n arbitrary: P rule: nat_less_induct)
   2.487    case (1 k)
   2.488    show ?case 
   2.489 -  proof (cases "k=0")
   2.490 +  proof (cases "k = 0")
   2.491      case False
   2.492 -    then have K2:"k div 2 < k" by (cases k, auto)
   2.493 -    from prems have "isnorm (sqr P)" by (simp add: sqr_cn)
   2.494 -    with prems K2 show ?thesis
   2.495 -    by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
   2.496 +    then have K2: "k div 2 < k" by (cases k) auto
   2.497 +    from 1 have "isnorm (sqr P)" by (simp add: sqr_cn)
   2.498 +    with 1 False K2 show ?thesis
   2.499 +      by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
   2.500    qed simp
   2.501  qed
   2.502  
     3.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 21 18:29:47 2011 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 21 23:47:19 2011 +0100
     3.3 @@ -495,11 +495,11 @@
     3.4    | "not F = T"
     3.5    | "not p = NOT p"
     3.6  lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
     3.7 -by (cases p) auto
     3.8 +  by (cases p) auto
     3.9  lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
    3.10 -by (cases p, auto)
    3.11 +  by (cases p) auto
    3.12  lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
    3.13 -by (cases p, auto)
    3.14 +  by (cases p) auto
    3.15  
    3.16  definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
    3.17    "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)"
    3.18 @@ -755,12 +755,12 @@
    3.19    let ?b = "snd (zsplit0 a)"
    3.20    have abj: "zsplit0 a = (?j,?b)" by simp 
    3.21    {assume "m\<noteq>0" 
    3.22 -    with prems(1)[OF abj] prems(2) have ?case by (auto simp add: Let_def split_def)}
    3.23 +    with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)}
    3.24    moreover
    3.25    {assume m0: "m =0"
    3.26 -    from abj have th: "a'=?b \<and> n=i+?j" using prems 
    3.27 +    with abj have th: "a'=?b \<and> n=i+?j" using 3 
    3.28        by (simp add: Let_def split_def)
    3.29 -    from abj prems  have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
    3.30 +    from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
    3.31      from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
    3.32      also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
    3.33    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
    3.34 @@ -770,9 +770,9 @@
    3.35    case (4 t n a)
    3.36    let ?nt = "fst (zsplit0 t)"
    3.37    let ?at = "snd (zsplit0 t)"
    3.38 -  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems 
    3.39 +  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 4
    3.40      by (simp add: Let_def split_def)
    3.41 -  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    3.42 +  from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    3.43    from th2[simplified] th[simplified] show ?case by simp
    3.44  next
    3.45    case (5 s t n a)
    3.46 @@ -782,12 +782,12 @@
    3.47    let ?at = "snd (zsplit0 t)"
    3.48    have abjs: "zsplit0 s = (?ns,?as)" by simp 
    3.49    moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
    3.50 -  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems 
    3.51 +  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 5
    3.52      by (simp add: Let_def split_def)
    3.53    from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
    3.54 -  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
    3.55 +  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
    3.56    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    3.57 -  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
    3.58 +  from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
    3.59    from th3[simplified] th2[simplified] th[simplified] show ?case 
    3.60      by (simp add: left_distrib)
    3.61  next
    3.62 @@ -798,22 +798,22 @@
    3.63    let ?at = "snd (zsplit0 t)"
    3.64    have abjs: "zsplit0 s = (?ns,?as)" by simp 
    3.65    moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
    3.66 -  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems 
    3.67 +  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6
    3.68      by (simp add: Let_def split_def)
    3.69    from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
    3.70 -  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
    3.71 +  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
    3.72    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    3.73 -  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
    3.74 +  from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
    3.75    from th3[simplified] th2[simplified] th[simplified] show ?case 
    3.76      by (simp add: left_diff_distrib)
    3.77  next
    3.78    case (7 i t n a)
    3.79    let ?nt = "fst (zsplit0 t)"
    3.80    let ?at = "snd (zsplit0 t)"
    3.81 -  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems 
    3.82 +  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 7
    3.83      by (simp add: Let_def split_def)
    3.84 -  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    3.85 -  hence " ?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
    3.86 +  from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    3.87 +  hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
    3.88    also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
    3.89    finally show ?case using th th2 by simp
    3.90  qed
    3.91 @@ -905,9 +905,9 @@
    3.92    from zsplit0_I[OF spl, where x="i" and bs="bs"] 
    3.93    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
    3.94    let ?N = "\<lambda> t. Inum (i#bs) t"
    3.95 -  from prems Ia nb  show ?case 
    3.96 +  from 5 Ia nb  show ?case 
    3.97      apply (auto simp add: Let_def split_def algebra_simps) 
    3.98 -    apply (cases "?r",auto)
    3.99 +    apply (cases "?r", auto)
   3.100      apply (case_tac nat, auto)
   3.101      done
   3.102  next
   3.103 @@ -918,9 +918,9 @@
   3.104    from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   3.105    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   3.106    let ?N = "\<lambda> t. Inum (i#bs) t"
   3.107 -  from prems Ia nb  show ?case 
   3.108 +  from 6 Ia nb show ?case 
   3.109      apply (auto simp add: Let_def split_def algebra_simps) 
   3.110 -    apply (cases "?r",auto)
   3.111 +    apply (cases "?r", auto)
   3.112      apply (case_tac nat, auto)
   3.113      done
   3.114  next
   3.115 @@ -931,9 +931,9 @@
   3.116    from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   3.117    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   3.118    let ?N = "\<lambda> t. Inum (i#bs) t"
   3.119 -  from prems Ia nb  show ?case 
   3.120 +  from 7 Ia nb show ?case 
   3.121      apply (auto simp add: Let_def split_def algebra_simps) 
   3.122 -    apply (cases "?r",auto)
   3.123 +    apply (cases "?r", auto)
   3.124      apply (case_tac nat, auto)
   3.125      done
   3.126  next
   3.127 @@ -944,9 +944,9 @@
   3.128    from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   3.129    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   3.130    let ?N = "\<lambda> t. Inum (i#bs) t"
   3.131 -  from prems Ia nb  show ?case 
   3.132 +  from 8 Ia nb  show ?case
   3.133      apply (auto simp add: Let_def split_def algebra_simps) 
   3.134 -    apply (cases "?r",auto)
   3.135 +    apply (cases "?r", auto)
   3.136      apply (case_tac nat, auto)
   3.137      done
   3.138  next
   3.139 @@ -957,9 +957,9 @@
   3.140    from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   3.141    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   3.142    let ?N = "\<lambda> t. Inum (i#bs) t"
   3.143 -  from prems Ia nb  show ?case 
   3.144 +  from 9 Ia nb  show ?case
   3.145      apply (auto simp add: Let_def split_def algebra_simps) 
   3.146 -    apply (cases "?r",auto)
   3.147 +    apply (cases "?r", auto)
   3.148      apply (case_tac nat, auto)
   3.149      done
   3.150  next
   3.151 @@ -970,7 +970,7 @@
   3.152    from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   3.153    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   3.154    let ?N = "\<lambda> t. Inum (i#bs) t"
   3.155 -  from prems Ia nb  show ?case 
   3.156 +  from 10 Ia nb  show ?case
   3.157      apply (auto simp add: Let_def split_def algebra_simps) 
   3.158      apply (cases "?r",auto)
   3.159      apply (case_tac nat, auto)
   3.160 @@ -986,7 +986,7 @@
   3.161    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
   3.162    moreover
   3.163    {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
   3.164 -    hence ?case using prems by (simp del: zlfm.simps)}
   3.165 +    hence ?case using 11 `j = 0` by (simp del: zlfm.simps) }
   3.166    moreover
   3.167    {assume "?c=0" and "j\<noteq>0" hence ?case 
   3.168        using zsplit0_I[OF spl, where x="i" and bs="bs"]
   3.169 @@ -1015,7 +1015,7 @@
   3.170    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
   3.171    moreover
   3.172    {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
   3.173 -    hence ?case using prems by (simp del: zlfm.simps)}
   3.174 +    hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)}
   3.175    moreover
   3.176    {assume "?c=0" and "j\<noteq>0" hence ?case 
   3.177        using zsplit0_I[OF spl, where x="i" and bs="bs"]
   3.178 @@ -1100,20 +1100,20 @@
   3.179  proof (induct p rule: iszlfm.induct)
   3.180    case (1 p q) 
   3.181    let ?d = "\<delta> (And p q)"
   3.182 -  from prems lcm_pos_int have dp: "?d >0" by simp
   3.183 -  have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
   3.184 -  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps)
   3.185 -  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
   3.186 -  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
   3.187 +  from 1 lcm_pos_int have dp: "?d >0" by simp
   3.188 +  have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
   3.189 +  hence th: "d\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
   3.190 +  have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
   3.191 +  hence th': "d\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
   3.192    from th th' dp show ?case by simp
   3.193  next
   3.194    case (2 p q)  
   3.195    let ?d = "\<delta> (And p q)"
   3.196 -  from prems lcm_pos_int have dp: "?d >0" by simp
   3.197 -  have "\<delta> p dvd \<delta> (And p q)" using prems by simp
   3.198 -  hence th: "d\<delta> p ?d" using delta_mono prems by(simp only: iszlfm.simps)
   3.199 -  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
   3.200 -  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
   3.201 +  from 2 lcm_pos_int have dp: "?d >0" by simp
   3.202 +  have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
   3.203 +  hence th: "d\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
   3.204 +  have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
   3.205 +  hence th': "d\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
   3.206    from th th' dp show ?case by simp
   3.207  qed simp_all
   3.208  
   3.209 @@ -1200,7 +1200,7 @@
   3.210    "mirror p = p"
   3.211      (* Lemmas for the correctness of \<sigma>\<rho> *)
   3.212  lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
   3.213 -by simp
   3.214 +  by simp
   3.215  
   3.216  lemma minusinf_inf:
   3.217    assumes linp: "iszlfm p"
   3.218 @@ -1374,14 +1374,14 @@
   3.219  
   3.220  lemma mirror_l: "iszlfm p \<and> d\<beta> p 1 
   3.221    \<Longrightarrow> iszlfm (mirror p) \<and> d\<beta> (mirror p) 1"
   3.222 -by (induct p rule: mirror.induct, auto)
   3.223 +  by (induct p rule: mirror.induct) auto
   3.224  
   3.225  lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
   3.226 -by (induct p rule: mirror.induct,auto)
   3.227 +  by (induct p rule: mirror.induct) auto
   3.228  
   3.229  lemma \<beta>_numbound0: assumes lp: "iszlfm p"
   3.230    shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
   3.231 -  using lp by (induct p rule: \<beta>.induct,auto)
   3.232 +  using lp by (induct p rule: \<beta>.induct) auto
   3.233  
   3.234  lemma d\<beta>_mono: 
   3.235    assumes linp: "iszlfm p"
   3.236 @@ -1389,12 +1389,12 @@
   3.237    and d: "l dvd l'"
   3.238    shows "d\<beta> p l'"
   3.239  using dr linp dvd_trans[of _ "l" "l'", simplified d]
   3.240 -by (induct p rule: iszlfm.induct) simp_all
   3.241 +  by (induct p rule: iszlfm.induct) simp_all
   3.242  
   3.243  lemma \<alpha>_l: assumes lp: "iszlfm p"
   3.244    shows "\<forall> b\<in> set (\<alpha> p). numbound0 b"
   3.245  using lp
   3.246 -by(induct p rule: \<alpha>.induct, auto)
   3.247 +  by(induct p rule: \<alpha>.induct) auto
   3.248  
   3.249  lemma \<zeta>: 
   3.250    assumes linp: "iszlfm p"
   3.251 @@ -1402,16 +1402,16 @@
   3.252  using linp
   3.253  proof(induct p rule: iszlfm.induct)
   3.254    case (1 p q)
   3.255 -  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   3.256 -  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"  by simp
   3.257 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   3.258 +  from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   3.259 +  from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   3.260 +  from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   3.261      d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   3.262      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
   3.263  next
   3.264    case (2 p q)
   3.265 -  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   3.266 -  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   3.267 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   3.268 +  from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   3.269 +  from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   3.270 +  from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   3.271      d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   3.272      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
   3.273  qed (auto simp add: lcm_pos_int)
   3.274 @@ -1585,31 +1585,31 @@
   3.275    shows "?P (x - d)"
   3.276  using lp u d dp nob p
   3.277  proof(induct p rule: iszlfm.induct)
   3.278 -  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp+
   3.279 -    with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
   3.280 -    show ?case by simp
   3.281 +  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp_all
   3.282 +  with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5
   3.283 +  show ?case by simp
   3.284  next
   3.285 -  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp+
   3.286 -    with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
   3.287 -    show ?case by simp
   3.288 +  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp_all
   3.289 +  with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6
   3.290 +  show ?case by simp
   3.291  next
   3.292 -  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+
   3.293 -    let ?e = "Inum (x # bs) e"
   3.294 -    {assume "(x-d) +?e > 0" hence ?case using c1 
   3.295 -      numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
   3.296 -    moreover
   3.297 -    {assume H: "\<not> (x-d) + ?e > 0" 
   3.298 -      let ?v="Neg e"
   3.299 -      have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
   3.300 -      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"]] 
   3.301 -      have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto 
   3.302 -      from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
   3.303 -      hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
   3.304 -      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
   3.305 -      hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 
   3.306 -        by (simp add: algebra_simps)
   3.307 -      with nob have ?case by auto}
   3.308 -    ultimately show ?case by blast
   3.309 +  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
   3.310 +  let ?e = "Inum (x # bs) e"
   3.311 +  {assume "(x-d) +?e > 0" hence ?case using c1 
   3.312 +    numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
   3.313 +  moreover
   3.314 +  {assume H: "\<not> (x-d) + ?e > 0" 
   3.315 +    let ?v="Neg e"
   3.316 +    have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
   3.317 +    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"]] 
   3.318 +    have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto 
   3.319 +    from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
   3.320 +    hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
   3.321 +    hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
   3.322 +    hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 
   3.323 +      by (simp add: algebra_simps)
   3.324 +    with nob have ?case by auto}
   3.325 +  ultimately show ?case by blast
   3.326  next
   3.327    case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" 
   3.328      by simp+
   3.329 @@ -1621,7 +1621,7 @@
   3.330      {assume H: "\<not> (x-d) + ?e \<ge> 0" 
   3.331        let ?v="Sub (C -1) e"
   3.332        have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
   3.333 -      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"]] 
   3.334 +      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"]] 
   3.335        have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto 
   3.336        from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
   3.337        hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
   3.338 @@ -1634,7 +1634,7 @@
   3.339      let ?e = "Inum (x # bs) e"
   3.340      let ?v="(Sub (C -1) e)"
   3.341      have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
   3.342 -    from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
   3.343 +    from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
   3.344        by simp (erule ballE[where x="1"],
   3.345          simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
   3.346  next
   3.347 @@ -1649,12 +1649,12 @@
   3.348        hence "x = - Inum (((x -d)) # bs) e + d" by simp
   3.349        hence "x = - Inum (a # bs) e + d"
   3.350          by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
   3.351 -       with prems(11) have ?case using dp by simp}
   3.352 +       with 4(5) have ?case using dp by simp}
   3.353    ultimately show ?case by blast
   3.354  next 
   3.355    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+
   3.356      let ?e = "Inum (x # bs) e"
   3.357 -    from prems have id: "j dvd d" by simp
   3.358 +    from 9 have id: "j dvd d" by simp
   3.359      from c1 have "?p x = (j dvd (x+ ?e))" by simp
   3.360      also have "\<dots> = (j dvd x - d + ?e)" 
   3.361        using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
   3.362 @@ -1663,7 +1663,7 @@
   3.363  next
   3.364    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+
   3.365      let ?e = "Inum (x # bs) e"
   3.366 -    from prems have id: "j dvd d" by simp
   3.367 +    from 10 have id: "j dvd d" by simp
   3.368      from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
   3.369      also have "\<dots> = (\<not> j dvd x - d + ?e)" 
   3.370        using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
     4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 21 18:29:47 2011 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 21 23:47:19 2011 +0100
     4.3 @@ -495,14 +495,16 @@
     4.4    assumes gt: "dvdnumcoeff t g" and gp: "g > 0" 
     4.5    shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t"
     4.6    using gt
     4.7 -proof(induct t rule: reducecoeffh.induct) 
     4.8 -  case (1 i) hence gd: "g dvd i" by simp
     4.9 +proof (induct t rule: reducecoeffh.induct) 
    4.10 +  case (1 i)
    4.11 +  hence gd: "g dvd i" by simp
    4.12    from gp have gnz: "g \<noteq> 0" by simp
    4.13 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd])
    4.14 +  with assms show ?case by (simp add: real_of_int_div[OF gnz gd])
    4.15  next
    4.16 -  case (2 n c t)  hence gd: "g dvd c" by simp
    4.17 +  case (2 n c t)
    4.18 +  hence gd: "g dvd c" by simp
    4.19    from gp have gnz: "g \<noteq> 0" by simp
    4.20 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
    4.21 +  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
    4.22  qed (auto simp add: numgcd_def gp)
    4.23  
    4.24  fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
    4.25 @@ -511,14 +513,14 @@
    4.26  | "ismaxcoeff t = (\<lambda>x. True)"
    4.27  
    4.28  lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
    4.29 -by (induct t rule: ismaxcoeff.induct, auto)
    4.30 +  by (induct t rule: ismaxcoeff.induct) auto
    4.31  
    4.32  lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)"
    4.33  proof (induct t rule: maxcoeff.induct)
    4.34    case (2 n c t)
    4.35    hence H:"ismaxcoeff t (maxcoeff t)" .
    4.36 -  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2)
    4.37 -  from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
    4.38 +  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp
    4.39 +  from ismaxcoeff_mono[OF H thh] show ?case by simp
    4.40  qed simp_all
    4.41  
    4.42  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))"
    4.43 @@ -534,30 +536,31 @@
    4.44  lemma dvdnumcoeff_aux:
    4.45    assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
    4.46    shows "dvdnumcoeff t (numgcdh t m)"
    4.47 -using prems
    4.48 +using assms
    4.49  proof(induct t rule: numgcdh.induct)
    4.50    case (2 n c t) 
    4.51    let ?g = "numgcdh t m"
    4.52 -  from prems have th:"gcd c ?g > 1" by simp
    4.53 +  from 2 have th:"gcd c ?g > 1" by simp
    4.54    from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    4.55    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    4.56 -  moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    4.57 +  moreover {assume "abs c > 1" and gp: "?g > 1" with 2
    4.58      have th: "dvdnumcoeff t ?g" by simp
    4.59      have th': "gcd c ?g dvd ?g" by simp
    4.60      from dvdnumcoeff_trans[OF th' th] have ?case by simp }
    4.61    moreover {assume "abs c = 0 \<and> ?g > 1"
    4.62 -    with prems have th: "dvdnumcoeff t ?g" by simp
    4.63 +    with 2 have th: "dvdnumcoeff t ?g" by simp
    4.64      have th': "gcd c ?g dvd ?g" by simp
    4.65      from dvdnumcoeff_trans[OF th' th] have ?case by simp
    4.66      hence ?case by simp }
    4.67    moreover {assume "abs c > 1" and g0:"?g = 0" 
    4.68 -    from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
    4.69 +    from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp }
    4.70    ultimately show ?case by blast
    4.71  qed auto
    4.72  
    4.73  lemma dvdnumcoeff_aux2:
    4.74 -  assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
    4.75 -  using prems 
    4.76 +  assumes "numgcd t > 1"
    4.77 +  shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
    4.78 +  using assms
    4.79  proof (simp add: numgcd_def)
    4.80    let ?mc = "maxcoeff t"
    4.81    let ?g = "numgcdh t ?mc"
    4.82 @@ -679,10 +682,10 @@
    4.83  lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
    4.84  proof (induct t rule: maxcoeff.induct)
    4.85    case (2 n c t)
    4.86 -  hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
    4.87 -  have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)
    4.88 +  hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp_all
    4.89 +  have "max (abs c) (maxcoeff t) \<ge> abs c" by simp
    4.90    with cnz have "max (abs c) (maxcoeff t) > 0" by arith
    4.91 -  with prems show ?case by simp
    4.92 +  with 2 show ?case by simp
    4.93  qed auto
    4.94  
    4.95  lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0"
    4.96 @@ -710,7 +713,7 @@
    4.97    {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
    4.98    moreover
    4.99    { assume nnz: "n \<noteq> 0"
   4.100 -    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
   4.101 +    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci) }
   4.102      moreover
   4.103      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   4.104        from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   4.105 @@ -726,45 +729,48 @@
   4.106          have gpdgp: "?g' dvd ?g'" by simp
   4.107          from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   4.108          have th2:"real ?g' * ?t = Inum bs ?t'" by simp
   4.109 -        from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
   4.110 +        from g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
   4.111          also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
   4.112          also have "\<dots> = (Inum bs ?t' / real n)"
   4.113            using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
   4.114 -        finally have "?lhs = Inum bs t / real n" by (simp add: simpnum_ci)
   4.115 -        then have ?thesis using prems by (simp add: simp_num_pair_def)}
   4.116 -      ultimately have ?thesis by blast}
   4.117 -    ultimately have ?thesis by blast} 
   4.118 +        finally have "?lhs = Inum bs t / real n" by simp
   4.119 +        then have ?thesis by (simp add: simp_num_pair_def) }
   4.120 +      ultimately have ?thesis by blast }
   4.121 +    ultimately have ?thesis by blast }
   4.122    ultimately show ?thesis by blast
   4.123  qed
   4.124  
   4.125  lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')"
   4.126    shows "numbound0 t' \<and> n' >0"
   4.127  proof-
   4.128 -    let ?t' = "simpnum t"
   4.129 +  let ?t' = "simpnum t"
   4.130    let ?g = "numgcd ?t'"
   4.131    let ?g' = "gcd n ?g"
   4.132 -  {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   4.133 +  { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) }
   4.134    moreover
   4.135    { assume nnz: "n \<noteq> 0"
   4.136 -    {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
   4.137 +    { assume "\<not> ?g > 1" hence ?thesis using assms
   4.138 +        by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) }
   4.139      moreover
   4.140 -    {assume g1:"?g>1" hence g0: "?g > 0" by simp
   4.141 +    { assume g1:"?g>1" hence g0: "?g > 0" by simp
   4.142        from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   4.143        hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith
   4.144        hence "?g'= 1 \<or> ?g' > 1" by arith
   4.145 -      moreover {assume "?g'=1" hence ?thesis using prems 
   4.146 -          by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
   4.147 -      moreover {assume g'1:"?g'>1"
   4.148 +      moreover {
   4.149 +        assume "?g' = 1" hence ?thesis using assms g1
   4.150 +          by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) }
   4.151 +      moreover {
   4.152 +        assume g'1: "?g' > 1"
   4.153          have gpdg: "?g' dvd ?g" by simp
   4.154 -        have gpdd: "?g' dvd n" by simp 
   4.155 +        have gpdd: "?g' dvd n" by simp
   4.156          have gpdgp: "?g' dvd ?g'" by simp
   4.157          from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
   4.158          from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
   4.159          have "n div ?g' >0" by simp
   4.160 -        hence ?thesis using prems 
   4.161 -          by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)}
   4.162 -      ultimately have ?thesis by blast}
   4.163 -    ultimately have ?thesis by blast} 
   4.164 +        hence ?thesis using assms g1 g'1
   4.165 +          by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0) }
   4.166 +      ultimately have ?thesis by blast }
   4.167 +    ultimately have ?thesis by blast }
   4.168    ultimately show ?thesis by blast
   4.169  qed
   4.170  
   4.171 @@ -962,14 +968,14 @@
   4.172    let ?sa = "rsplit0 a" let ?sb = "rsplit0 b"
   4.173    let ?ca = "fst ?sa" let ?cb = "fst ?sb"
   4.174    let ?ta = "snd ?sa" let ?tb = "snd ?sb"
   4.175 -  from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))" 
   4.176 +  from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))" 
   4.177      by (cases "rsplit0 a") (auto simp add: Let_def split_def)
   4.178    have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = 
   4.179      Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
   4.180      by (simp add: Let_def split_def algebra_simps)
   4.181 -  also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a") auto
   4.182 +  also have "\<dots> = Inum bs a + Inum bs b" using 2 by (cases "rsplit0 a") auto
   4.183    finally show ?case using nb by simp 
   4.184 -qed (auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric])
   4.185 +qed (auto simp add: Let_def split_def algebra_simps, simp add: right_distrib[symmetric])
   4.186  
   4.187      (* Linearize a formula*)
   4.188  definition
   4.189 @@ -1081,8 +1087,8 @@
   4.190    case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
   4.191  next
   4.192    case (3 c e) 
   4.193 -  from prems have nb: "numbound0 e" by simp
   4.194 -  from prems have cp: "real c > 0" by simp
   4.195 +  from 3 have nb: "numbound0 e" by simp
   4.196 +  from 3 have cp: "real c > 0" by simp
   4.197    fix a
   4.198    let ?e="Inum (a#bs) e"
   4.199    let ?z = "(- ?e) / real c"
   4.200 @@ -1098,8 +1104,8 @@
   4.201    thus ?case by blast
   4.202  next
   4.203    case (4 c e)   
   4.204 -  from prems have nb: "numbound0 e" by simp
   4.205 -  from prems have cp: "real c > 0" by simp
   4.206 +  from 4 have nb: "numbound0 e" by simp
   4.207 +  from 4 have cp: "real c > 0" by simp
   4.208    fix a
   4.209    let ?e="Inum (a#bs) e"
   4.210    let ?z = "(- ?e) / real c"
   4.211 @@ -1115,8 +1121,8 @@
   4.212    thus ?case by blast
   4.213  next
   4.214    case (5 c e) 
   4.215 -    from prems have nb: "numbound0 e" by simp
   4.216 -  from prems have cp: "real c > 0" by simp
   4.217 +  from 5 have nb: "numbound0 e" by simp
   4.218 +  from 5 have cp: "real c > 0" by simp
   4.219    fix a
   4.220    let ?e="Inum (a#bs) e"
   4.221    let ?z = "(- ?e) / real c"
   4.222 @@ -1131,8 +1137,8 @@
   4.223    thus ?case by blast
   4.224  next
   4.225    case (6 c e)  
   4.226 -    from prems have nb: "numbound0 e" by simp
   4.227 -  from prems have cp: "real c > 0" by simp
   4.228 +  from 6 have nb: "numbound0 e" by simp
   4.229 +  from lp 6 have cp: "real c > 0" by simp
   4.230    fix a
   4.231    let ?e="Inum (a#bs) e"
   4.232    let ?z = "(- ?e) / real c"
   4.233 @@ -1147,8 +1153,8 @@
   4.234    thus ?case by blast
   4.235  next
   4.236    case (7 c e)  
   4.237 -    from prems have nb: "numbound0 e" by simp
   4.238 -  from prems have cp: "real c > 0" by simp
   4.239 +  from 7 have nb: "numbound0 e" by simp
   4.240 +  from 7 have cp: "real c > 0" by simp
   4.241    fix a
   4.242    let ?e="Inum (a#bs) e"
   4.243    let ?z = "(- ?e) / real c"
   4.244 @@ -1163,8 +1169,8 @@
   4.245    thus ?case by blast
   4.246  next
   4.247    case (8 c e)  
   4.248 -    from prems have nb: "numbound0 e" by simp
   4.249 -  from prems have cp: "real c > 0" by simp
   4.250 +  from 8 have nb: "numbound0 e" by simp
   4.251 +  from 8 have cp: "real c > 0" by simp
   4.252    fix a
   4.253    let ?e="Inum (a#bs) e"
   4.254    let ?z = "(- ?e) / real c"
   4.255 @@ -1189,8 +1195,8 @@
   4.256    case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto
   4.257  next
   4.258    case (3 c e) 
   4.259 -  from prems have nb: "numbound0 e" by simp
   4.260 -  from prems have cp: "real c > 0" by simp
   4.261 +  from 3 have nb: "numbound0 e" by simp
   4.262 +  from 3 have cp: "real c > 0" by simp
   4.263    fix a
   4.264    let ?e="Inum (a#bs) e"
   4.265    let ?z = "(- ?e) / real c"
   4.266 @@ -1206,8 +1212,8 @@
   4.267    thus ?case by blast
   4.268  next
   4.269    case (4 c e) 
   4.270 -  from prems have nb: "numbound0 e" by simp
   4.271 -  from prems have cp: "real c > 0" by simp
   4.272 +  from 4 have nb: "numbound0 e" by simp
   4.273 +  from 4 have cp: "real c > 0" by simp
   4.274    fix a
   4.275    let ?e="Inum (a#bs) e"
   4.276    let ?z = "(- ?e) / real c"
   4.277 @@ -1223,8 +1229,8 @@
   4.278    thus ?case by blast
   4.279  next
   4.280    case (5 c e) 
   4.281 -  from prems have nb: "numbound0 e" by simp
   4.282 -  from prems have cp: "real c > 0" by simp
   4.283 +  from 5 have nb: "numbound0 e" by simp
   4.284 +  from 5 have cp: "real c > 0" by simp
   4.285    fix a
   4.286    let ?e="Inum (a#bs) e"
   4.287    let ?z = "(- ?e) / real c"
   4.288 @@ -1239,8 +1245,8 @@
   4.289    thus ?case by blast
   4.290  next
   4.291    case (6 c e) 
   4.292 -  from prems have nb: "numbound0 e" by simp
   4.293 -  from prems have cp: "real c > 0" by simp
   4.294 +  from 6 have nb: "numbound0 e" by simp
   4.295 +  from 6 have cp: "real c > 0" by simp
   4.296    fix a
   4.297    let ?e="Inum (a#bs) e"
   4.298    let ?z = "(- ?e) / real c"
   4.299 @@ -1255,8 +1261,8 @@
   4.300    thus ?case by blast
   4.301  next
   4.302    case (7 c e) 
   4.303 -  from prems have nb: "numbound0 e" by simp
   4.304 -  from prems have cp: "real c > 0" by simp
   4.305 +  from 7 have nb: "numbound0 e" by simp
   4.306 +  from 7 have cp: "real c > 0" by simp
   4.307    fix a
   4.308    let ?e="Inum (a#bs) e"
   4.309    let ?z = "(- ?e) / real c"
   4.310 @@ -1271,8 +1277,8 @@
   4.311    thus ?case by blast
   4.312  next
   4.313    case (8 c e) 
   4.314 -  from prems have nb: "numbound0 e" by simp
   4.315 -  from prems have cp: "real c > 0" by simp
   4.316 +  from 8 have nb: "numbound0 e" by simp
   4.317 +  from 8 have cp: "real c > 0" by simp
   4.318    fix a
   4.319    let ?e="Inum (a#bs) e"
   4.320    let ?z = "(- ?e) / real c"
   4.321 @@ -1356,7 +1362,7 @@
   4.322    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> _")
   4.323    using lp
   4.324  proof(induct p rule: usubst.induct)
   4.325 -  case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.326 +  case (5 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
   4.327    have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)"
   4.328      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.329    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)"
   4.330 @@ -1366,7 +1372,7 @@
   4.331      using np by simp 
   4.332    finally show ?case using nbt nb by (simp add: algebra_simps)
   4.333  next
   4.334 -  case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.335 +  case (6 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
   4.336    have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)"
   4.337      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.338    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
   4.339 @@ -1376,7 +1382,7 @@
   4.340      using np by simp 
   4.341    finally show ?case using nbt nb by (simp add: algebra_simps)
   4.342  next
   4.343 -  case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.344 +  case (7 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
   4.345    have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)"
   4.346      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.347    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)"
   4.348 @@ -1386,7 +1392,7 @@
   4.349      using np by simp 
   4.350    finally show ?case using nbt nb by (simp add: algebra_simps)
   4.351  next
   4.352 -  case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.353 +  case (8 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
   4.354    have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)"
   4.355      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.356    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
   4.357 @@ -1396,7 +1402,7 @@
   4.358      using np by simp 
   4.359    finally show ?case using nbt nb by (simp add: algebra_simps)
   4.360  next
   4.361 -  case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.362 +  case (3 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
   4.363    from np have np: "real n \<noteq> 0" by simp
   4.364    have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)"
   4.365      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.366 @@ -1407,7 +1413,7 @@
   4.367      using np by simp 
   4.368    finally show ?case using nbt nb by (simp add: algebra_simps)
   4.369  next
   4.370 -  case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.371 +  case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
   4.372    from np have np: "real n \<noteq> 0" by simp
   4.373    have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)"
   4.374      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.375 @@ -1467,99 +1473,99 @@
   4.376  using lp px noS
   4.377  proof (induct p rule: isrlfm.induct)
   4.378    case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.379 -    from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps)
   4.380 -    hence pxc: "x < (- ?N x e) / real c" 
   4.381 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
   4.382 -    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.383 -    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.384 -    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.385 -    moreover {assume y: "y < (-?N x e)/ real c"
   4.386 -      hence "y * real c < - ?N x e"
   4.387 -        by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.388 -      hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
   4.389 -      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.390 -    moreover {assume y: "y > (- ?N x e) / real c" 
   4.391 -      with yu have eu: "u > (- ?N x e) / real c" by auto
   4.392 -      with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
   4.393 -      with lx pxc have "False" by auto
   4.394 -      hence ?case by simp }
   4.395 -    ultimately show ?case by blast
   4.396 +  from 5 have "x * real c + ?N x e < 0" by (simp add: algebra_simps)
   4.397 +  hence pxc: "x < (- ?N x e) / real c" 
   4.398 +    by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
   4.399 +  from 5 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.400 +  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.401 +  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.402 +  moreover {assume y: "y < (-?N x e)/ real c"
   4.403 +    hence "y * real c < - ?N x e"
   4.404 +      by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.405 +    hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
   4.406 +    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.407 +  moreover {assume y: "y > (- ?N x e) / real c" 
   4.408 +    with yu have eu: "u > (- ?N x e) / real c" by auto
   4.409 +    with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
   4.410 +    with lx pxc have "False" by auto
   4.411 +    hence ?case by simp }
   4.412 +  ultimately show ?case by blast
   4.413  next
   4.414    case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp +
   4.415 -    from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps)
   4.416 -    hence pxc: "x \<le> (- ?N x e) / real c" 
   4.417 -      by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
   4.418 -    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.419 -    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.420 -    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.421 -    moreover {assume y: "y < (-?N x e)/ real c"
   4.422 -      hence "y * real c < - ?N x e"
   4.423 -        by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.424 -      hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
   4.425 -      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.426 -    moreover {assume y: "y > (- ?N x e) / real c" 
   4.427 -      with yu have eu: "u > (- ?N x e) / real c" by auto
   4.428 -      with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
   4.429 -      with lx pxc have "False" by auto
   4.430 -      hence ?case by simp }
   4.431 -    ultimately show ?case by blast
   4.432 +  from 6 have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps)
   4.433 +  hence pxc: "x \<le> (- ?N x e) / real c" 
   4.434 +    by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
   4.435 +  from 6 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.436 +  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.437 +  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.438 +  moreover {assume y: "y < (-?N x e)/ real c"
   4.439 +    hence "y * real c < - ?N x e"
   4.440 +      by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.441 +    hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
   4.442 +    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.443 +  moreover {assume y: "y > (- ?N x e) / real c" 
   4.444 +    with yu have eu: "u > (- ?N x e) / real c" by auto
   4.445 +    with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
   4.446 +    with lx pxc have "False" by auto
   4.447 +    hence ?case by simp }
   4.448 +  ultimately show ?case by blast
   4.449  next
   4.450    case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.451 -    from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps)
   4.452 -    hence pxc: "x > (- ?N x e) / real c" 
   4.453 -      by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
   4.454 -    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.455 -    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.456 -    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.457 -    moreover {assume y: "y > (-?N x e)/ real c"
   4.458 -      hence "y * real c > - ?N x e"
   4.459 -        by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.460 -      hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
   4.461 -      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.462 -    moreover {assume y: "y < (- ?N x e) / real c" 
   4.463 -      with ly have eu: "l < (- ?N x e) / real c" by auto
   4.464 -      with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
   4.465 -      with xu pxc have "False" by auto
   4.466 -      hence ?case by simp }
   4.467 -    ultimately show ?case by blast
   4.468 +  from 7 have "x * real c + ?N x e > 0" by (simp add: algebra_simps)
   4.469 +  hence pxc: "x > (- ?N x e) / real c" 
   4.470 +    by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
   4.471 +  from 7 have noSc: "\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.472 +  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.473 +  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.474 +  moreover {assume y: "y > (-?N x e)/ real c"
   4.475 +    hence "y * real c > - ?N x e"
   4.476 +      by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.477 +    hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
   4.478 +    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.479 +  moreover {assume y: "y < (- ?N x e) / real c" 
   4.480 +    with ly have eu: "l < (- ?N x e) / real c" by auto
   4.481 +    with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
   4.482 +    with xu pxc have "False" by auto
   4.483 +    hence ?case by simp }
   4.484 +  ultimately show ?case by blast
   4.485  next
   4.486    case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.487 -    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps)
   4.488 -    hence pxc: "x \<ge> (- ?N x e) / real c" 
   4.489 -      by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
   4.490 -    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.491 -    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.492 -    hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.493 -    moreover {assume y: "y > (-?N x e)/ real c"
   4.494 -      hence "y * real c > - ?N x e"
   4.495 -        by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.496 -      hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
   4.497 -      hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.498 -    moreover {assume y: "y < (- ?N x e) / real c" 
   4.499 -      with ly have eu: "l < (- ?N x e) / real c" by auto
   4.500 -      with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
   4.501 -      with xu pxc have "False" by auto
   4.502 -      hence ?case by simp }
   4.503 -    ultimately show ?case by blast
   4.504 +  from 8 have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps)
   4.505 +  hence pxc: "x \<ge> (- ?N x e) / real c" 
   4.506 +    by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
   4.507 +  from 8 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.508 +  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.509 +  hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
   4.510 +  moreover {assume y: "y > (-?N x e)/ real c"
   4.511 +    hence "y * real c > - ?N x e"
   4.512 +      by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.513 +    hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
   4.514 +    hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.515 +  moreover {assume y: "y < (- ?N x e) / real c" 
   4.516 +    with ly have eu: "l < (- ?N x e) / real c" by auto
   4.517 +    with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
   4.518 +    with xu pxc have "False" by auto
   4.519 +    hence ?case by simp }
   4.520 +  ultimately show ?case by blast
   4.521  next
   4.522    case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.523 -    from cp have cnz: "real c \<noteq> 0" by simp
   4.524 -    from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps)
   4.525 -    hence pxc: "x = (- ?N x e) / real c" 
   4.526 -      by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
   4.527 -    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.528 -    with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto
   4.529 -    with pxc show ?case by simp
   4.530 +  from cp have cnz: "real c \<noteq> 0" by simp
   4.531 +  from 3 have "x * real c + ?N x e = 0" by (simp add: algebra_simps)
   4.532 +  hence pxc: "x = (- ?N x e) / real c" 
   4.533 +    by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
   4.534 +  from 3 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.535 +  with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto
   4.536 +  with pxc show ?case by simp
   4.537  next
   4.538    case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.539 -    from cp have cnz: "real c \<noteq> 0" by simp
   4.540 -    from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.541 -    with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.542 -    hence "y* real c \<noteq> -?N x e"      
   4.543 -      by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
   4.544 -    hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
   4.545 -    thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
   4.546 -      by (simp add: algebra_simps)
   4.547 +  from cp have cnz: "real c \<noteq> 0" by simp
   4.548 +  from 4 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.549 +  with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.550 +  hence "y* real c \<noteq> -?N x e"      
   4.551 +    by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
   4.552 +  hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
   4.553 +  thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
   4.554 +    by (simp add: algebra_simps)
   4.555  qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
   4.556  
   4.557  lemma finite_set_intervals:
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Mon Feb 21 18:29:47 2011 +0100
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Mon Feb 21 23:47:19 2011 +0100
     5.3 @@ -46,7 +46,7 @@
     5.4  proof(induct rule: iupt.induct)
     5.5    case (1 a b)
     5.6    show ?case
     5.7 -    using prems by (simp add: simp_from_to)
     5.8 +    using 1 by (simp add: simp_from_to)
     5.9  qed
    5.10  
    5.11  lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
    5.12 @@ -119,7 +119,7 @@
    5.13    assume "?r" hence "(i\<Colon>int) dvd \<lfloor>x\<Colon>real\<rfloor>" ..
    5.14    hence "\<exists> k. real (floor x) = real (i*k)" 
    5.15      by (simp only: real_of_int_inject) (simp add: dvd_def)
    5.16 -  thus ?l using prems by (simp add: rdvd_def)
    5.17 +  thus ?l using `?r` by (simp add: rdvd_def)
    5.18  qed
    5.19  
    5.20  lemma int_rdvd_iff: "(real (i::int) rdvd real t) = (i dvd t)"
    5.21 @@ -705,16 +705,17 @@
    5.22  proof(induct t rule: reducecoeffh.induct) 
    5.23    case (1 i) hence gd: "g dvd i" by simp
    5.24    from gp have gnz: "g \<noteq> 0" by simp
    5.25 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd])
    5.26 +  from assms 1 show ?case by (simp add: real_of_int_div[OF gnz gd])
    5.27  next
    5.28    case (2 n c t)  hence gd: "g dvd c" by simp
    5.29    from gp have gnz: "g \<noteq> 0" by simp
    5.30 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
    5.31 +  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
    5.32  next
    5.33    case (3 c s t)  hence gd: "g dvd c" by simp
    5.34    from gp have gnz: "g \<noteq> 0" by simp
    5.35 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
    5.36 +  from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
    5.37  qed (auto simp add: numgcd_def gp)
    5.38 +
    5.39  consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
    5.40  recdef ismaxcoeff "measure size"
    5.41    "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"
    5.42 @@ -729,7 +730,7 @@
    5.43  proof (induct t rule: maxcoeff.induct)
    5.44    case (2 n c t)
    5.45    hence H:"ismaxcoeff t (maxcoeff t)" .
    5.46 -  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2)
    5.47 +  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp
    5.48    from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
    5.49  next
    5.50    case (3 c t s) 
    5.51 @@ -747,60 +748,60 @@
    5.52    apply auto
    5.53    done
    5.54  lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
    5.55 -  by (induct t rule: numgcdh.induct, auto)
    5.56 +  by (induct t rule: numgcdh.induct) auto
    5.57  
    5.58  lemma dvdnumcoeff_aux:
    5.59    assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
    5.60    shows "dvdnumcoeff t (numgcdh t m)"
    5.61 -using prems
    5.62 +using assms
    5.63  proof(induct t rule: numgcdh.induct)
    5.64    case (2 n c t) 
    5.65    let ?g = "numgcdh t m"
    5.66 -  from prems have th:"gcd c ?g > 1" by simp
    5.67 +  from 2 have th:"gcd c ?g > 1" by simp
    5.68    from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    5.69    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    5.70 -  moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    5.71 +  moreover {assume "abs c > 1" and gp: "?g > 1" with 2
    5.72      have th: "dvdnumcoeff t ?g" by simp
    5.73      have th': "gcd c ?g dvd ?g" by simp
    5.74      from dvdnumcoeff_trans[OF th' th] have ?case by simp }
    5.75    moreover {assume "abs c = 0 \<and> ?g > 1"
    5.76 -    with prems have th: "dvdnumcoeff t ?g" by simp
    5.77 +    with 2 have th: "dvdnumcoeff t ?g" by simp
    5.78      have th': "gcd c ?g dvd ?g" by simp
    5.79      from dvdnumcoeff_trans[OF th' th] have ?case by simp
    5.80      hence ?case by simp }
    5.81    moreover {assume "abs c > 1" and g0:"?g = 0" 
    5.82 -    from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
    5.83 +    from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp }
    5.84    ultimately show ?case by blast
    5.85  next
    5.86    case (3 c s t) 
    5.87    let ?g = "numgcdh t m"
    5.88 -  from prems have th:"gcd c ?g > 1" by simp
    5.89 +  from 3 have th:"gcd c ?g > 1" by simp
    5.90    from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    5.91    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    5.92 -  moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    5.93 +  moreover {assume "abs c > 1" and gp: "?g > 1" with 3
    5.94      have th: "dvdnumcoeff t ?g" by simp
    5.95      have th': "gcd c ?g dvd ?g" by simp
    5.96      from dvdnumcoeff_trans[OF th' th] have ?case by simp }
    5.97    moreover {assume "abs c = 0 \<and> ?g > 1"
    5.98 -    with prems have th: "dvdnumcoeff t ?g" by simp
    5.99 +    with 3 have th: "dvdnumcoeff t ?g" by simp
   5.100      have th': "gcd c ?g dvd ?g" by simp
   5.101      from dvdnumcoeff_trans[OF th' th] have ?case by simp
   5.102      hence ?case by simp }
   5.103    moreover {assume "abs c > 1" and g0:"?g = 0" 
   5.104 -    from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
   5.105 +    from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp }
   5.106    ultimately show ?case by blast
   5.107  qed auto
   5.108  
   5.109  lemma dvdnumcoeff_aux2:
   5.110    assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
   5.111 -  using prems 
   5.112 +  using assms 
   5.113  proof (simp add: numgcd_def)
   5.114    let ?mc = "maxcoeff t"
   5.115    let ?g = "numgcdh t ?mc"
   5.116    have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff)
   5.117    have th2: "?mc \<ge> 0" by (rule maxcoeff_pos)
   5.118    assume H: "numgcdh t ?mc > 1"
   5.119 -  from dvdnumcoeff_aux[OF th1 th2 H]  show "dvdnumcoeff t ?g" .
   5.120 +  from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" .
   5.121  qed
   5.122  
   5.123  lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t"
   5.124 @@ -911,32 +912,33 @@
   5.125         in (bv, CF c a bi))"
   5.126    "split_int a = (a,C 0)"
   5.127  
   5.128 -lemma split_int:"\<And> tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs"
   5.129 +lemma split_int: "\<And>tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs"
   5.130  proof (induct t rule: split_int.induct)
   5.131    case (2 c n b tv ti)
   5.132    let ?bv = "fst (split_int b)"
   5.133    let ?bi = "snd (split_int b)"
   5.134    have "split_int b = (?bv,?bi)" by simp
   5.135 -  with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
   5.136 -  from prems(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def)
   5.137 -  from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def)
   5.138 +  with 2(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
   5.139 +  from 2(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def)
   5.140 +  from 2(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def)
   5.141  next
   5.142    case (3 c a b tv ti) 
   5.143    let ?bv = "fst (split_int b)"
   5.144    let ?bi = "snd (split_int b)"
   5.145    have "split_int b = (?bv,?bi)" by simp
   5.146 -  with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
   5.147 -  from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def)
   5.148 -  from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF)
   5.149 +  with 3(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
   5.150 +  from 3(2) have tibi: "ti = CF c a ?bi"
   5.151 +    by (simp add: Let_def split_def)
   5.152 +  from 3(2) b[symmetric] bii show ?case
   5.153 +    by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF)
   5.154  qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps)
   5.155  
   5.156  lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) "
   5.157 -by (induct t rule: split_int.induct, auto simp add: Let_def split_def)
   5.158 -
   5.159 -definition
   5.160 -  numfloor:: "num \<Rightarrow> num"
   5.161 +  by (induct t rule: split_int.induct) (auto simp add: Let_def split_def)
   5.162 +
   5.163 +definition numfloor:: "num \<Rightarrow> num"
   5.164  where
   5.165 -  numfloor_def: "numfloor t = (let (tv,ti) = split_int t in 
   5.166 +  "numfloor t = (let (tv,ti) = split_int t in 
   5.167    (case tv of C i \<Rightarrow> numadd (tv,ti) 
   5.168    | _ \<Rightarrow> numadd(CF 1 tv (C 0),ti)))"
   5.169  
   5.170 @@ -1022,13 +1024,13 @@
   5.171    hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
   5.172    have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)
   5.173    with cnz have "max (abs c) (maxcoeff t) > 0" by arith
   5.174 -  with prems show ?case by simp
   5.175 +  with 2 show ?case by simp
   5.176  next
   5.177    case (3 c s t) 
   5.178    hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
   5.179    have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)
   5.180    with cnz have "max (abs c) (maxcoeff t) > 0" by arith
   5.181 -  with prems show ?case by simp
   5.182 +  with 3 show ?case by simp
   5.183  qed auto
   5.184  
   5.185  lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0"
   5.186 @@ -1072,34 +1074,35 @@
   5.187          have gpdgp: "?g' dvd ?g'" by simp
   5.188          from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   5.189          have th2:"real ?g' * ?t = Inum bs ?t'" by simp
   5.190 -        from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
   5.191 +        from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
   5.192          also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
   5.193          also have "\<dots> = (Inum bs ?t' / real n)"
   5.194            using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
   5.195          finally have "?lhs = Inum bs t / real n" by simp
   5.196 -        then have ?thesis using prems by (simp add: simp_num_pair_def)}
   5.197 -      ultimately have ?thesis by blast}
   5.198 -    ultimately have ?thesis by blast} 
   5.199 +        then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
   5.200 +      ultimately have ?thesis by blast }
   5.201 +    ultimately have ?thesis by blast }
   5.202    ultimately show ?thesis by blast
   5.203  qed
   5.204  
   5.205 -lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')"
   5.206 +lemma simp_num_pair_l:
   5.207 +  assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')"
   5.208    shows "numbound0 t' \<and> n' >0"
   5.209  proof-
   5.210 -    let ?t' = "simpnum t"
   5.211 +  let ?t' = "simpnum t"
   5.212    let ?g = "numgcd ?t'"
   5.213    let ?g' = "gcd n ?g"
   5.214 -  {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   5.215 +  { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) }
   5.216    moreover
   5.217    { assume nnz: "n \<noteq> 0"
   5.218 -    {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def)}
   5.219 +    {assume "\<not> ?g > 1" hence ?thesis using assms by (auto simp add: Let_def simp_num_pair_def) }
   5.220      moreover
   5.221      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   5.222        from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   5.223        hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith
   5.224        hence "?g'= 1 \<or> ?g' > 1" by arith
   5.225 -      moreover {assume "?g'=1" hence ?thesis using prems 
   5.226 -          by (auto simp add: Let_def simp_num_pair_def)}
   5.227 +      moreover {assume "?g'=1" hence ?thesis using assms g1 g0
   5.228 +          by (auto simp add: Let_def simp_num_pair_def) }
   5.229        moreover {assume g'1:"?g'>1"
   5.230          have gpdg: "?g' dvd ?g" by simp
   5.231          have gpdd: "?g' dvd n" by simp
   5.232 @@ -1107,10 +1110,10 @@
   5.233          from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
   5.234          from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
   5.235          have "n div ?g' >0" by simp
   5.236 -        hence ?thesis using prems 
   5.237 +        hence ?thesis using assms g1 g'1
   5.238            by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
   5.239 -      ultimately have ?thesis by blast}
   5.240 -    ultimately have ?thesis by blast} 
   5.241 +      ultimately have ?thesis by blast }
   5.242 +    ultimately have ?thesis by blast } 
   5.243    ultimately show ?thesis by blast
   5.244  qed
   5.245  
   5.246 @@ -1131,43 +1134,43 @@
   5.247    "not (Or p q) = And (not p) (not q)"
   5.248    "not p = NOT p"
   5.249  lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"
   5.250 -by (induct p) auto
   5.251 +  by (induct p) auto
   5.252  lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
   5.253 -by (induct p, auto)
   5.254 +  by (induct p) auto
   5.255  lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"
   5.256 -by (induct p, auto)
   5.257 +  by (induct p) auto
   5.258  
   5.259  definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   5.260    "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 
   5.261     if p = q then p else And p q)"
   5.262  lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"
   5.263 -by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
   5.264 +  by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)
   5.265  
   5.266  lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"
   5.267 -using conj_def by auto 
   5.268 +  using conj_def by auto 
   5.269  lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"
   5.270 -using conj_def by auto 
   5.271 +  using conj_def by auto 
   5.272  
   5.273  definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   5.274    "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p 
   5.275         else if p=q then p else Or p q)"
   5.276  
   5.277  lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"
   5.278 -by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
   5.279 +  by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
   5.280  lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
   5.281 -using disj_def by auto 
   5.282 +  using disj_def by auto 
   5.283  lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
   5.284 -using disj_def by auto 
   5.285 +  using disj_def by auto 
   5.286  
   5.287  definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   5.288    "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 
   5.289      else Imp p q)"
   5.290  lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
   5.291 -by (cases "p=F \<or> q=T",simp_all add: imp_def)
   5.292 +  by (cases "p=F \<or> q=T",simp_all add: imp_def)
   5.293  lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
   5.294 -using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
   5.295 +  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
   5.296  lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
   5.297 -using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 
   5.298 +  using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 
   5.299  
   5.300  definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   5.301    "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
   5.302 @@ -1245,7 +1248,8 @@
   5.303        have gpdgp: "?g' dvd ?g'" by simp
   5.304        from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   5.305        have th2:"real ?g' * ?t = Inum bs t" by simp
   5.306 -      from prems have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"
   5.307 +      from assms g1 g0 g'1
   5.308 +      have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"
   5.309          by (simp add: simpdvd_def Let_def)
   5.310        also have "\<dots> = (real d rdvd (Inum bs t))"
   5.311          using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] 
   5.312 @@ -1544,9 +1548,8 @@
   5.313  lemma qelim_ci:
   5.314    assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
   5.315    shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)"
   5.316 -using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] 
   5.317 -by(induct p rule: qelim.induct) 
   5.318 -(auto simp del: simpfm.simps)
   5.319 +  using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] 
   5.320 +  by (induct p rule: qelim.induct) (auto simp del: simpfm.simps)
   5.321  
   5.322  
   5.323  text {* The @{text "\<int>"} Part *}
   5.324 @@ -1584,7 +1587,7 @@
   5.325    case (5 t n a)
   5.326    let ?nt = "fst (zsplit0 t)"
   5.327    let ?at = "snd (zsplit0 t)"
   5.328 -  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems 
   5.329 +  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 5 
   5.330      by (simp add: Let_def split_def)
   5.331    from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   5.332    from th2[simplified] th[simplified] show ?case by simp
     6.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 18:29:47 2011 +0100
     6.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:47:19 2011 +0100
     6.3 @@ -144,11 +144,10 @@
     6.4    {assume nxs: "n \<ge> length (x#xs)" hence ?case using removen_same[OF nxs] by simp}
     6.5    moreover
     6.6    {assume nxs: "\<not> (n \<ge> length (x#xs))" 
     6.7 -    {assume mln: "m < n" hence ?case using prems by (cases m, auto)}
     6.8 +    {assume mln: "m < n" hence ?case using Cons by (cases m, auto)}
     6.9      moreover
    6.10      {assume mln: "\<not> (m < n)" 
    6.11 -      
    6.12 -      {assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)}
    6.13 +      {assume mxs: "m \<le> length (x#xs)" hence ?case using Cons by (cases m, auto)}
    6.14        moreover
    6.15        {assume mxs: "\<not> (m \<le> length (x#xs))" 
    6.16          have th: "length (removen n (x#xs)) = length xs" 
    6.17 @@ -162,15 +161,13 @@
    6.18        ultimately have ?case by blast
    6.19      }
    6.20      ultimately have ?case by blast
    6.21 -    
    6.22 -  }      ultimately show ?case by blast
    6.23 +  } ultimately show ?case by blast
    6.24  qed
    6.25  
    6.26  lemma decrtm: assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound m t" 
    6.27    and nle: "m \<le> length bs" 
    6.28    shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
    6.29 -  using bnd nb nle
    6.30 -  by (induct t rule: tm.induct, auto simp add: removen_nth)
    6.31 +  using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)
    6.32  
    6.33  primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
    6.34    "tmsubst0 t (CP c) = CP c"
    6.35 @@ -182,10 +179,10 @@
    6.36  | "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
    6.37  lemma tmsubst0:
    6.38    shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
    6.39 -by (induct a rule: tm.induct,auto simp add: nth_pos2)
    6.40 +  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
    6.41  
    6.42  lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
    6.43 -by (induct a rule: tm.induct,auto simp add: nth_pos2)
    6.44 +  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
    6.45  
    6.46  primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
    6.47    "tmsubst n t (CP c) = CP c"
    6.48 @@ -569,13 +566,13 @@
    6.49  proof(induct p arbitrary: bs n rule: fm.induct)
    6.50    case (E p bs n) 
    6.51    {fix y
    6.52 -    from prems have bnd: "boundslt (length (y#bs)) p" 
    6.53 +    from E have bnd: "boundslt (length (y#bs)) p" 
    6.54        and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
    6.55      from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
    6.56    thus ?case by simp 
    6.57  next
    6.58    case (A p bs n) {fix y
    6.59 -    from prems have bnd: "boundslt (length (y#bs)) p" 
    6.60 +    from A have bnd: "boundslt (length (y#bs)) p" 
    6.61        and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
    6.62      from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
    6.63    thus ?case by simp 
    6.64 @@ -620,16 +617,16 @@
    6.65  proof(induct p arbitrary: bs m rule: fm.induct)
    6.66    case (E p bs m) 
    6.67    {fix x
    6.68 -    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    6.69 +    from E have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    6.70    and nle: "Suc m < length (x#bs)" by auto
    6.71 -    from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    6.72 +    from E(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    6.73    } thus ?case by auto 
    6.74  next
    6.75    case (A p bs m)  
    6.76    {fix x
    6.77 -    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    6.78 +    from A have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
    6.79    and nle: "Suc m < length (x#bs)" by auto
    6.80 -    from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    6.81 +    from A(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
    6.82    } thus ?case by auto
    6.83  qed (auto simp add: decrtm removen_nth)
    6.84  
    6.85 @@ -680,18 +677,18 @@
    6.86  proof (induct p arbitrary: bs n t rule: fm.induct)
    6.87    case (E p bs n) 
    6.88    {fix x 
    6.89 -    from prems have bn: "boundslt (length (x#bs)) p" by simp 
    6.90 -      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
    6.91 -    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 
    6.92 +    from E have bn: "boundslt (length (x#bs)) p" by simp 
    6.93 +    from E have nlm: "Suc n \<le> length (x#bs)" by simp
    6.94 +    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 
    6.95      hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
    6.96      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  
    6.97  thus ?case by simp 
    6.98  next
    6.99    case (A p bs n)   
   6.100    {fix x 
   6.101 -    from prems have bn: "boundslt (length (x#bs)) p" by simp 
   6.102 -      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
   6.103 -    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 
   6.104 +    from A have bn: "boundslt (length (x#bs)) p" by simp 
   6.105 +    from A have nlm: "Suc n \<le> length (x#bs)" by simp
   6.106 +    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 
   6.107      hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
   6.108      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  
   6.109  thus ?case by simp 
   6.110 @@ -1371,7 +1368,7 @@
   6.111    case 2 thus ?case by (auto,rule_tac x="min z za" in exI, auto)
   6.112  next
   6.113    case (3 c e) hence nbe: "tmbound0 e" by simp
   6.114 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.115 +  from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.116    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   6.117    let ?c = "Ipoly vs c"
   6.118    let ?e = "Itm vs (y#bs) e"
   6.119 @@ -1393,7 +1390,7 @@
   6.120    ultimately show ?case by blast
   6.121  next
   6.122    case (4 c e)  hence nbe: "tmbound0 e" by simp
   6.123 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.124 +  from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.125    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   6.126    let ?c = "Ipoly vs c"
   6.127    let ?e = "Itm vs (y#bs) e"
   6.128 @@ -1414,7 +1411,7 @@
   6.129    ultimately show ?case by blast
   6.130  next
   6.131    case (5 c e)  hence nbe: "tmbound0 e" by simp
   6.132 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.133 +  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.134    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   6.135    note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
   6.136    let ?c = "Ipoly vs c"
   6.137 @@ -1436,7 +1433,7 @@
   6.138    ultimately show ?case by blast
   6.139  next
   6.140    case (6 c e)  hence nbe: "tmbound0 e" by simp
   6.141 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.142 +  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.143    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   6.144    note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
   6.145    let ?c = "Ipoly vs c"
   6.146 @@ -1467,7 +1464,7 @@
   6.147    case 2 thus ?case by (auto,rule_tac x="max z za" in exI, auto)
   6.148  next
   6.149    case (3 c e) hence nbe: "tmbound0 e" by simp
   6.150 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.151 +  from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.152    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   6.153    let ?c = "Ipoly vs c"
   6.154    let ?e = "Itm vs (y#bs) e"
   6.155 @@ -1488,8 +1485,8 @@
   6.156          using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   6.157    ultimately show ?case by blast
   6.158  next
   6.159 -  case (4 c e)  hence nbe: "tmbound0 e" by simp
   6.160 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.161 +  case (4 c e) hence nbe: "tmbound0 e" by simp
   6.162 +  from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.163    note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   6.164    let ?c = "Ipoly vs c"
   6.165    let ?e = "Itm vs (y#bs) e"
   6.166 @@ -1509,8 +1506,8 @@
   6.167          using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   6.168    ultimately show ?case by blast
   6.169  next
   6.170 -  case (5 c e)  hence nbe: "tmbound0 e" by simp
   6.171 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.172 +  case (5 c e) hence nbe: "tmbound0 e" by simp
   6.173 +  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.174    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   6.175    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]
   6.176    let ?c = "Ipoly vs c"
   6.177 @@ -1532,7 +1529,7 @@
   6.178    ultimately show ?case by blast
   6.179  next
   6.180    case (6 c e)  hence nbe: "tmbound0 e" by simp
   6.181 -  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.182 +  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   6.183    hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   6.184    note eqs = lt[OF nc(1), where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
   6.185    let ?c = "Ipoly vs c"
     7.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 18:29:47 2011 +0100
     7.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:47:19 2011 +0100
     7.3 @@ -253,53 +253,53 @@
     7.4        \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
     7.5  proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
     7.6    case (2 a b c' n' p' n0 n1)
     7.7 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
     7.8 -  from prems(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
     7.9 +  from 2 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
    7.10 +  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    7.11    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
    7.12 -  with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
    7.13 +  with 2(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
    7.14    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
    7.15 -  thus ?case using prems th3 by simp
    7.16 +  thus ?case using 2 th3 by simp
    7.17  next
    7.18    case (3 c' n' p' a b n1 n0)
    7.19 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
    7.20 -  from prems(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    7.21 +  from 3 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
    7.22 +  from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    7.23    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
    7.24 -  with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
    7.25 +  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
    7.26    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
    7.27 -  thus ?case using prems th3 by simp
    7.28 +  thus ?case using 3 th3 by simp
    7.29  next
    7.30    case (4 c n p c' n' p' n0 n1)
    7.31    hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
    7.32 -  from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 
    7.33 -  from prems have ngen0: "n \<ge> n0" by simp
    7.34 -  from prems have n'gen1: "n' \<ge> n1" by simp 
    7.35 +  from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 
    7.36 +  from 4 have ngen0: "n \<ge> n0" by simp
    7.37 +  from 4 have n'gen1: "n' \<ge> n1" by simp 
    7.38    have "n < n' \<or> n' < n \<or> n = n'" by auto
    7.39    moreover {assume eq: "n = n'"
    7.40 -    with prems(2)[OF nc nc'] 
    7.41 +    with 4(2)[OF nc nc'] 
    7.42      have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
    7.43      hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
    7.44        using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
    7.45 -    from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    7.46 +    from eq 4(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    7.47      have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
    7.48 -    from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
    7.49 +    from minle npp' ncc'n01 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
    7.50    moreover {assume lt: "n < n'"
    7.51      have "min n0 n1 \<le> n0" by simp
    7.52 -    with prems have th1:"min n0 n1 \<le> n" by auto 
    7.53 -    from prems have th21: "isnpolyh c (Suc n)" by simp
    7.54 -    from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
    7.55 +    with 4 have th1:"min n0 n1 \<le> n" by auto 
    7.56 +    from 4 have th21: "isnpolyh c (Suc n)" by simp
    7.57 +    from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp
    7.58      from lt have th23: "min (Suc n) n' = Suc n" by arith
    7.59 -    from prems(4)[OF th21 th22]
    7.60 +    from 4(4)[OF th21 th22]
    7.61      have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
    7.62 -    with prems th1 have ?case by simp } 
    7.63 +    with 4 lt th1 have ?case by simp }
    7.64    moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
    7.65      have "min n0 n1 \<le> n1"  by simp
    7.66 -    with prems have th1:"min n0 n1 \<le> n'" by auto
    7.67 -    from prems have th21: "isnpolyh c' (Suc n')" by simp_all
    7.68 -    from prems have th22: "isnpolyh (CN c n p) n" by simp
    7.69 +    with 4 have th1:"min n0 n1 \<le> n'" by auto
    7.70 +    from 4 have th21: "isnpolyh c' (Suc n')" by simp_all
    7.71 +    from 4 have th22: "isnpolyh (CN c n p) n" by simp
    7.72      from gt have th23: "min n (Suc n') = Suc n'" by arith
    7.73 -    from prems(3)[OF th22 th21]
    7.74 +    from 4(3)[OF th22 th21]
    7.75      have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
    7.76 -    with prems th1 have ?case by simp}
    7.77 +    with 4 gt th1 have ?case by simp}
    7.78        ultimately show ?case by blast
    7.79  qed auto
    7.80  
    7.81 @@ -370,14 +370,15 @@
    7.82    \<Longrightarrow> degreen p m = degreen q m"
    7.83  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
    7.84    case (4 c n p c' n' p' m n0 n1 x) 
    7.85 -  {assume nn': "n' < n" hence ?case using prems by simp}
    7.86 +  {assume nn': "n' < n" hence ?case using 4 by simp}
    7.87    moreover 
    7.88    {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
    7.89 -    moreover {assume "n < n'" with prems have ?case by simp }
    7.90 -    moreover {assume eq: "n = n'" hence ?case using prems 
    7.91 +    moreover {assume "n < n'" with 4 have ?case by simp }
    7.92 +    moreover {assume eq: "n = n'" hence ?case using 4 
    7.93          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
    7.94          apply (auto simp add: Let_def)
    7.95 -        by blast
    7.96 +        apply blast
    7.97 +        done
    7.98        }
    7.99      ultimately have ?case by blast}
   7.100    ultimately show ?case by blast
   7.101 @@ -664,13 +665,13 @@
   7.102  qed
   7.103  
   7.104  lemma polypow_normh: 
   7.105 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.106 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.107    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   7.108  proof (induct k arbitrary: n rule: polypow.induct)
   7.109    case (2 k n)
   7.110    let ?q = "polypow (Suc k div 2) p"
   7.111    let ?d = "polymul (?q,?q)"
   7.112 -  from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
   7.113 +  from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
   7.114    from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
   7.115    from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp
   7.116    from dn on show ?case by (simp add: Let_def)
   7.117 @@ -695,7 +696,7 @@
   7.118  
   7.119  
   7.120  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
   7.121 -by (simp add: shift1_def polymul)
   7.122 +  by (simp add: shift1_def)
   7.123  
   7.124  lemma shift1_isnpoly: 
   7.125    assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "
   7.126 @@ -713,7 +714,7 @@
   7.127    using f np by (induct k arbitrary: p, auto)
   7.128  
   7.129  lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
   7.130 -  by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
   7.131 +  by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   7.132  
   7.133  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   7.134    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   7.135 @@ -731,10 +732,10 @@
   7.136    using np
   7.137  proof (induct p arbitrary: n rule: behead.induct)
   7.138    case (1 c p n) hence pn: "isnpolyh p n" by simp
   7.139 -  from prems(2)[OF pn] 
   7.140 +  from 1(1)[OF pn] 
   7.141    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 
   7.142    then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   7.143 -    by (simp_all add: th[symmetric] field_simps power_Suc)
   7.144 +    by (simp_all add: th[symmetric] field_simps)
   7.145  qed (auto simp add: Let_def)
   7.146  
   7.147  lemma behead_isnpolyh:
   7.148 @@ -747,7 +748,7 @@
   7.149    case (goal1 c n p n')
   7.150    hence "n = Suc (n - 1)" by simp
   7.151    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   7.152 -  with prems(2) show ?case by simp
   7.153 +  with goal1(2) show ?case by simp
   7.154  qed
   7.155  
   7.156  lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
   7.157 @@ -838,7 +839,7 @@
   7.158  qed
   7.159  
   7.160  lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
   7.161 -  by (induct p, auto)
   7.162 +  by (induct p) auto
   7.163  
   7.164  lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
   7.165    unfolding wf_bs_def by simp
   7.166 @@ -1033,7 +1034,7 @@
   7.167      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   7.168  
   7.169  lemma polymul_1[simp]: 
   7.170 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.171 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.172    and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
   7.173    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
   7.174      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   7.175 @@ -1101,17 +1102,17 @@
   7.176  next
   7.177    case (2 a b c' n' p') 
   7.178    let ?c = "(a,b)"
   7.179 -  from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
   7.180 +  from 2 have "degree (C ?c) = degree (CN c' n' p')" by simp
   7.181    hence nz:"n' > 0" by (cases n', auto)
   7.182    hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   7.183 -  with prems show ?case by simp
   7.184 +  with 2 show ?case by simp
   7.185  next
   7.186    case (3 c n p a' b') 
   7.187    let ?c' = "(a',b')"
   7.188 -  from prems have "degree (C ?c') = degree (CN c n p)" by simp
   7.189 +  from 3 have "degree (C ?c') = degree (CN c n p)" by simp
   7.190    hence nz:"n > 0" by (cases n, auto)
   7.191    hence "head (CN c n p) = CN c n p" by (cases n, auto)
   7.192 -  with prems show ?case by simp
   7.193 +  with 3 show ?case by simp
   7.194  next
   7.195    case (4 c n p c' n' p')
   7.196    hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 
   7.197 @@ -1126,36 +1127,40 @@
   7.198    moreover
   7.199    {assume nn': "n = n'"
   7.200      have "n = 0 \<or> n >0" by arith
   7.201 -    moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}
   7.202 +    moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
   7.203      moreover {assume nz: "n > 0"
   7.204 -      with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
   7.205 -      hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def split_def fst_conv snd_conv] using nn' prems by (simp add: Let_def)}
   7.206 +      with nn' H(3) have  cc': "c = c'" and pp': "p = p'" by (cases n, auto)+
   7.207 +      hence ?case
   7.208 +        using polysub_same_0 [OF p'nh, simplified polysub_def split_def fst_conv snd_conv]
   7.209 +          polysub_same_0 [OF c'nh, simplified polysub_def split_def fst_conv snd_conv]
   7.210 +        using 4 nn' by (simp add: Let_def) }
   7.211      ultimately have ?case by blast}
   7.212    moreover
   7.213    {assume nn': "n < n'" hence n'p: "n' > 0" by simp 
   7.214      hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
   7.215 -    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using prems by (cases n', simp_all)
   7.216 -    hence "n > 0" by (cases n, simp_all)
   7.217 -    hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
   7.218 -    from H(3) headcnp headcnp' nn' have ?case by auto}
   7.219 +    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
   7.220 +      using 4 nn' by (cases n', simp_all)
   7.221 +    hence "n > 0" by (cases n) simp_all
   7.222 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto
   7.223 +    from H(3) headcnp headcnp' nn' have ?case by auto }
   7.224    moreover
   7.225    {assume nn': "n > n'"  hence np: "n > 0" by simp 
   7.226 -    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
   7.227 -    from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   7.228 -    from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
   7.229 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) simp_all
   7.230 +    from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   7.231 +    from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all
   7.232      with degcnpeq have "n' > 0" by (cases n', simp_all)
   7.233 -    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   7.234 -    from H(3) headcnp headcnp' nn' have ?case by auto}
   7.235 +    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
   7.236 +    from H(3) headcnp headcnp' nn' have ?case by auto }
   7.237    ultimately show ?case  by blast
   7.238  qed auto 
   7.239   
   7.240  lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
   7.241 -by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
   7.242 +  by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def)
   7.243  
   7.244  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
   7.245  proof(induct k arbitrary: n0 p)
   7.246    case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   7.247 -  with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   7.248 +  with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   7.249      and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
   7.250    thus ?case by (simp add: funpow_swap1)
   7.251  qed auto  
   7.252 @@ -1194,19 +1199,20 @@
   7.253  apply (metis head_nz)
   7.254  apply (metis head_nz)
   7.255  apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
   7.256 -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   7.257 +apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   7.258 +done
   7.259  
   7.260  lemma polymul_head_polyeq: 
   7.261 -   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.262 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.263    shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
   7.264  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   7.265    case (2 a b c' n' p' n0 n1)
   7.266    hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)"  by (simp_all add: head_isnpolyh)
   7.267 -  thus ?case using prems by (cases n', auto) 
   7.268 +  thus ?case using 2 by (cases n') auto
   7.269  next 
   7.270    case (3 c n p a' b' n0 n1) 
   7.271    hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')"  by (simp_all add: head_isnpolyh)
   7.272 -  thus ?case using prems by (cases n, auto)
   7.273 +  thus ?case using 3 by (cases n) auto
   7.274  next
   7.275    case (4 c n p c' n' p' n0 n1)
   7.276    hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
   7.277 @@ -1215,15 +1221,14 @@
   7.278    have "n < n' \<or> n' < n \<or> n = n'" by arith
   7.279    moreover 
   7.280    {assume nn': "n < n'" hence ?case 
   7.281 -      thm prems
   7.282 -      using norm 
   7.283 -    prems(6)[rule_format, OF nn' norm(1,6)]
   7.284 -    prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
   7.285 +    using norm 
   7.286 +    4(5)[rule_format, OF nn' norm(1,6)]
   7.287 +    4(6)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all) }
   7.288    moreover {assume nn': "n'< n"
   7.289      hence stupid: "n' < n \<and> \<not> n < n'" by simp
   7.290 -    hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]
   7.291 -      prems(5)[rule_format, OF stupid norm(5,4)] 
   7.292 -      by (simp,cases n',simp,cases n,auto)}
   7.293 +    hence ?case using norm 4(3) [rule_format, OF stupid norm(5,3)]
   7.294 +      4(4)[rule_format, OF stupid norm(5,4)] 
   7.295 +      by (simp,cases n',simp,cases n,auto) }
   7.296    moreover {assume nn': "n' = n"
   7.297      hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp
   7.298      from nn' polymul_normh[OF norm(5,4)] 
   7.299 @@ -1247,8 +1252,8 @@
   7.300      have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
   7.301      hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
   7.302      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
   7.303 -    have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
   7.304 -        prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
   7.305 +    have ?case using norm 4(1)[rule_format, OF stupid norm(5,3)]
   7.306 +        4(2)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
   7.307      ultimately have ?case by (cases n) auto} 
   7.308    ultimately show ?case by blast
   7.309  qed simp_all
   7.310 @@ -1603,12 +1608,13 @@
   7.311  
   7.312  definition "swapnorm n m t = polynate (swap n m t)"
   7.313  
   7.314 -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
   7.315 +lemma swapnorm:
   7.316 +  assumes nbs: "n < length bs" and mbs: "m < length bs"
   7.317    shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   7.318 -  using swap[OF prems] swapnorm_def by simp
   7.319 +  using swap[OF assms] swapnorm_def by simp
   7.320  
   7.321  lemma swapnorm_isnpoly[simp]: 
   7.322 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.323 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   7.324    shows "isnpoly (swapnorm n m p)"
   7.325    unfolding swapnorm_def by simp
   7.326  
   7.327 @@ -1625,9 +1631,9 @@
   7.328    "isweaknpoly p = False"       
   7.329  
   7.330  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
   7.331 -  by (induct p arbitrary: n0, auto)
   7.332 +  by (induct p arbitrary: n0) auto
   7.333  
   7.334  lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" 
   7.335 -  by (induct p, auto)
   7.336 +  by (induct p) auto
   7.337  
   7.338  end
   7.339 \ No newline at end of file