author wenzelm Mon Feb 21 23:54:53 2011 +0100 (2011-02-21) changeset 41816 7a55699805dc parent 41815 9a0cacbcd825 parent 41807 ab5d2d81f9fb child 41817 c7be23634728 child 41829 455cbcbba8c2
merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
```     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Feb 21 23:14:36 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Feb 21 23:54:53 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 23:14:36 2011 +0100
2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Mon Feb 21 23:54:53 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.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.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.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 23:14:36 2011 +0100
3.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 21 23:54:53 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.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.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 23:14:36 2011 +0100
4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 21 23:54:53 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.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.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 23:14:36 2011 +0100
5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Mon Feb 21 23:54:53 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.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 23:14:36 2011 +0100
6.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:54:53 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"
```