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;

src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy | file | annotate | diff | revisions | |

src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy | file | annotate | diff | revisions |

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.422 thus ?case by (simp add: add_cn) 2.423 -qed(simp) 2.424 +qed simp 2.425 2.426 text {* neg conserves normalizedness *} 2.427 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)" 2.428 proof (induct P) 2.429 case (Pinj i P2) 2.430 - from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2]) 2.431 - with prems show ?case by(cases P2, auto, cases i, auto) 2.432 + then have "isnorm P2" by (simp add: norm_Pinj[of i P2]) 2.433 + with Pinj show ?case by - (cases P2, auto, cases i, auto) 2.434 next 2.435 - case (PX P1 x P2) 2.436 - from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) 2.437 - with prems show ?case 2.438 - proof(cases P1) 2.439 + case (PX P1 x P2) note PX1 = this 2.440 + from PX have "isnorm P2" "isnorm P1" 2.441 + by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) 2.442 + with PX show ?case 2.443 + proof (cases P1) 2.444 case (PX p1 y p2) 2.445 - with prems show ?thesis by(cases x, auto, cases p2, auto) 2.446 + with PX1 show ?thesis by - (cases x, auto, cases p2, auto) 2.447 next 2.448 case Pinj 2.449 - with prems show ?thesis by(cases x, auto) 2.450 - qed(cases x, auto) 2.451 -qed(simp) 2.452 + with PX1 show ?thesis by (cases x) auto 2.453 + qed (cases x, auto) 2.454 +qed simp 2.455 2.456 text {* sub conserves normalizedness *} 2.457 lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)" 2.458 @@ -361,17 +377,18 @@ 2.459 2.460 text {* sqr conserves normalizizedness *} 2.461 lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)" 2.462 -proof(induct P) 2.463 +proof (induct P) 2.464 case (Pinj i Q) 2.465 - from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) 2.466 + then show ?case 2.467 + by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) 2.468 next 2.469 case (PX P1 x P2) 2.470 - from prems have "x+x~=0" "isnorm P2" "isnorm P1" by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) 2.471 - with prems have 2.472 - "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))" 2.473 - and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" 2.474 - by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) 2.475 - thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) 2.476 + then have "x + x ~= 0" "isnorm P2" "isnorm P1" 2.477 + by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) 2.478 + with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))" 2.479 + and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" 2.480 + by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) 2.481 + then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) 2.482 qed simp 2.483 2.484 text {* pow conserves normalizedness *} 2.485 @@ -379,12 +396,12 @@ 2.486 proof (induct n arbitrary: P rule: nat_less_induct) 2.487 case (1 k) 2.488 show ?case 2.489 - proof (cases "k=0") 2.490 + proof (cases "k = 0") 2.491 case False 2.492 - then have K2:"k div 2 < k" by (cases k, auto) 2.493 - from prems have "isnorm (sqr P)" by (simp add: sqr_cn) 2.494 - with prems K2 show ?thesis 2.495 - by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) 2.496 + then have K2: "k div 2 < k" by (cases k) auto 2.497 + from 1 have "isnorm (sqr P)" by (simp add: sqr_cn) 2.498 + with 1 False K2 show ?thesis 2.499 + by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) 2.500 qed simp 2.501 qed 2.502

3.1 --- a/src/HOL/Decision_Procs/Cooper.thy Mon Feb 21 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.60 by (simp add: left_distrib) 3.61 next 3.62 @@ -798,22 +798,22 @@ 3.63 let ?at = "snd (zsplit0 t)" 3.64 have abjs: "zsplit0 s = (?ns,?as)" by simp 3.65 moreover have abjt: "zsplit0 t = (?nt,?at)" by simp 3.66 - ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems 3.67 + ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6 3.68 by (simp add: Let_def split_def) 3.69 from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast 3.70 - from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto 3.71 + from 6 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto 3.72 with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 3.73 - from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 3.74 + from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 3.75 from th3[simplified] th2[simplified] th[simplified] show ?case 3.76 by (simp add: left_diff_distrib) 3.77 next 3.78 case (7 i t n a) 3.79 let ?nt = "fst (zsplit0 t)" 3.80 let ?at = "snd (zsplit0 t)" 3.81 - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems 3.82 + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 7 3.83 by (simp add: Let_def split_def) 3.84 - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 3.85 - hence " ?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp 3.86 + from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 3.87 + hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp 3.88 also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib) 3.89 finally show ?case using th th2 by simp 3.90 qed 3.91 @@ -905,9 +905,9 @@ 3.92 from zsplit0_I[OF spl, where x="i" and bs="bs"] 3.93 have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 3.94 let ?N = "\<lambda> t. Inum (i#bs) t" 3.95 - from prems Ia nb show ?case 3.96 + from 5 Ia nb show ?case 3.97 apply (auto simp add: Let_def split_def algebra_simps) 3.98 - apply (cases "?r",auto) 3.99 + apply (cases "?r", auto) 3.100 apply (case_tac nat, auto) 3.101 done 3.102 next 3.103 @@ -918,9 +918,9 @@ 3.104 from zsplit0_I[OF spl, where x="i" and bs="bs"] 3.105 have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 3.106 let ?N = "\<lambda> t. Inum (i#bs) t" 3.107 - from prems Ia nb show ?case 3.108 + from 6 Ia nb show ?case 3.109 apply (auto simp add: Let_def split_def algebra_simps) 3.110 - apply (cases "?r",auto) 3.111 + apply (cases "?r", auto) 3.112 apply (case_tac nat, auto) 3.113 done 3.114 next 3.115 @@ -931,9 +931,9 @@ 3.116 from zsplit0_I[OF spl, where x="i" and bs="bs"] 3.117 have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 3.118 let ?N = "\<lambda> t. Inum (i#bs) t" 3.119 - from prems Ia nb show ?case 3.120 + from 7 Ia nb show ?case 3.121 apply (auto simp add: Let_def split_def algebra_simps) 3.122 - apply (cases "?r",auto) 3.123 + apply (cases "?r", auto) 3.124 apply (case_tac nat, auto) 3.125 done 3.126 next 3.127 @@ -944,9 +944,9 @@ 3.128 from zsplit0_I[OF spl, where x="i" and bs="bs"] 3.129 have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 3.130 let ?N = "\<lambda> t. Inum (i#bs) t" 3.131 - from prems Ia nb show ?case 3.132 + from 8 Ia nb show ?case 3.133 apply (auto simp add: Let_def split_def algebra_simps) 3.134 - apply (cases "?r",auto) 3.135 + apply (cases "?r", auto) 3.136 apply (case_tac nat, auto) 3.137 done 3.138 next 3.139 @@ -957,9 +957,9 @@ 3.140 from zsplit0_I[OF spl, where x="i" and bs="bs"] 3.141 have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 3.142 let ?N = "\<lambda> t. Inum (i#bs) t" 3.143 - from prems Ia nb show ?case 3.144 + from 9 Ia nb show ?case 3.145 apply (auto simp add: Let_def split_def algebra_simps) 3.146 - apply (cases "?r",auto) 3.147 + apply (cases "?r", auto) 3.148 apply (case_tac nat, auto) 3.149 done 3.150 next 3.151 @@ -970,7 +970,7 @@ 3.152 from zsplit0_I[OF spl, where x="i" and bs="bs"] 3.153 have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 3.154 let ?N = "\<lambda> t. Inum (i#bs) t" 3.155 - from prems Ia nb show ?case 3.156 + from 10 Ia nb show ?case 3.157 apply (auto simp add: Let_def split_def algebra_simps) 3.158 apply (cases "?r",auto) 3.159 apply (case_tac nat, auto) 3.160 @@ -986,7 +986,7 @@ 3.161 have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith 3.162 moreover 3.163 {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 3.164 - hence ?case using prems by (simp del: zlfm.simps)} 3.165 + hence ?case using 11 `j = 0` by (simp del: zlfm.simps) } 3.166 moreover 3.167 {assume "?c=0" and "j\<noteq>0" hence ?case 3.168 using zsplit0_I[OF spl, where x="i" and bs="bs"] 3.169 @@ -1015,7 +1015,7 @@ 3.170 have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith 3.171 moreover 3.172 {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 3.173 - hence ?case using prems by (simp del: zlfm.simps)} 3.174 + hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)} 3.175 moreover 3.176 {assume "?c=0" and "j\<noteq>0" hence ?case 3.177 using zsplit0_I[OF spl, where x="i" and bs="bs"] 3.178 @@ -1100,20 +1100,20 @@ 3.179 proof (induct p rule: iszlfm.induct) 3.180 case (1 p q) 3.181 let ?d = "\<delta> (And p q)" 3.182 - from prems lcm_pos_int have dp: "?d >0" by simp 3.183 - have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 3.184 - hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps) 3.185 - have "\<delta> q dvd \<delta> (And p q)" using prems by simp 3.186 - hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) 3.187 + from 1 lcm_pos_int have dp: "?d >0" by simp 3.188 + have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp 3.189 + hence th: "d\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps) 3.190 + have "\<delta> q dvd \<delta> (And p q)" using 1 by simp 3.191 + hence th': "d\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps) 3.192 from th th' dp show ?case by simp 3.193 next 3.194 case (2 p q) 3.195 let ?d = "\<delta> (And p q)" 3.196 - from prems lcm_pos_int have dp: "?d >0" by simp 3.197 - have "\<delta> p dvd \<delta> (And p q)" using prems by simp 3.198 - hence th: "d\<delta> p ?d" using delta_mono prems by(simp only: iszlfm.simps) 3.199 - have "\<delta> q dvd \<delta> (And p q)" using prems by simp 3.200 - hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) 3.201 + from 2 lcm_pos_int have dp: "?d >0" by simp 3.202 + have "\<delta> p dvd \<delta> (And p q)" using 2 by simp 3.203 + hence th: "d\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps) 3.204 + have "\<delta> q dvd \<delta> (And p q)" using 2 by simp 3.205 + hence th': "d\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps) 3.206 from th th' dp show ?case by simp 3.207 qed simp_all 3.208 3.209 @@ -1200,7 +1200,7 @@ 3.210 "mirror p = p" 3.211 (* Lemmas for the correctness of \<sigma>\<rho> *) 3.212 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" 3.213 -by simp 3.214 + by simp 3.215 3.216 lemma minusinf_inf: 3.217 assumes linp: "iszlfm p" 3.218 @@ -1374,14 +1374,14 @@ 3.219 3.220 lemma mirror_l: "iszlfm p \<and> d\<beta> p 1 3.221 \<Longrightarrow> iszlfm (mirror p) \<and> d\<beta> (mirror p) 1" 3.222 -by (induct p rule: mirror.induct, auto) 3.223 + by (induct p rule: mirror.induct) auto 3.224 3.225 lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p" 3.226 -by (induct p rule: mirror.induct,auto) 3.227 + by (induct p rule: mirror.induct) auto 3.228 3.229 lemma \<beta>_numbound0: assumes lp: "iszlfm p" 3.230 shows "\<forall> b\<in> set (\<beta> p). numbound0 b" 3.231 - using lp by (induct p rule: \<beta>.induct,auto) 3.232 + using lp by (induct p rule: \<beta>.induct) auto 3.233 3.234 lemma d\<beta>_mono: 3.235 assumes linp: "iszlfm p" 3.236 @@ -1389,12 +1389,12 @@ 3.237 and d: "l dvd l'" 3.238 shows "d\<beta> p l'" 3.239 using dr linp dvd_trans[of _ "l" "l'", simplified d] 3.240 -by (induct p rule: iszlfm.induct) simp_all 3.241 + by (induct p rule: iszlfm.induct) simp_all 3.242 3.243 lemma \<alpha>_l: assumes lp: "iszlfm p" 3.244 shows "\<forall> b\<in> set (\<alpha> p). numbound0 b" 3.245 using lp 3.246 -by(induct p rule: \<alpha>.induct, auto) 3.247 + by(induct p rule: \<alpha>.induct) auto 3.248 3.249 lemma \<zeta>: 3.250 assumes linp: "iszlfm p" 3.251 @@ -1402,16 +1402,16 @@ 3.252 using linp 3.253 proof(induct p rule: iszlfm.induct) 3.254 case (1 p q) 3.255 - from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.256 - from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.257 - from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 3.258 + from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.259 + from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.260 + from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 3.261 d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 3.262 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) 3.263 next 3.264 case (2 p q) 3.265 - from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.266 - from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.267 - from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 3.268 + from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.269 + from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 3.270 + from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 3.271 d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 3.272 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) 3.273 qed (auto simp add: lcm_pos_int) 3.274 @@ -1585,31 +1585,31 @@ 3.275 shows "?P (x - d)" 3.276 using lp u d dp nob p 3.277 proof(induct p rule: iszlfm.induct) 3.278 - case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+ 3.279 - with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems 3.280 - show ?case by simp 3.281 + case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all 3.282 + with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5 3.283 + show ?case by simp 3.284 next 3.285 - case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+ 3.286 - with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems 3.287 - show ?case by simp 3.288 + case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all 3.289 + with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6 3.290 + show ?case by simp 3.291 next 3.292 - case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp+ 3.293 - let ?e = "Inum (x # bs) e" 3.294 - {assume "(x-d) +?e > 0" hence ?case using c1 3.295 - numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp} 3.296 - moreover 3.297 - {assume H: "\<not> (x-d) + ?e > 0" 3.298 - let ?v="Neg e" 3.299 - have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp 3.300 - from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 3.301 - have nob: "\<not> (\<exists> j\<in> {1 ..d}. x = - ?e + j)" by auto 3.302 - from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1) 3.303 - hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp 3.304 - hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp 3.305 - hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 3.306 - by (simp add: algebra_simps) 3.307 - with nob have ?case by auto} 3.308 - ultimately show ?case by blast 3.309 + case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp_all 3.310 + let ?e = "Inum (x # bs) e" 3.311 + {assume "(x-d) +?e > 0" hence ?case using c1 3.312 + numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp} 3.313 + moreover 3.314 + {assume H: "\<not> (x-d) + ?e > 0" 3.315 + let ?v="Neg e" 3.316 + have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp 3.317 + from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 3.318 + have nob: "\<not> (\<exists> j\<in> {1 ..d}. x = - ?e + j)" by auto 3.319 + from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1) 3.320 + hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp 3.321 + hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp 3.322 + hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 3.323 + by (simp add: algebra_simps) 3.324 + with nob have ?case by auto} 3.325 + ultimately show ?case by blast 3.326 next 3.327 case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" 3.328 by simp+ 3.329 @@ -1621,7 +1621,7 @@ 3.330 {assume H: "\<not> (x-d) + ?e \<ge> 0" 3.331 let ?v="Sub (C -1) e" 3.332 have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp 3.333 - from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 3.334 + from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 3.335 have nob: "\<not> (\<exists> j\<in> {1 ..d}. x = - ?e - 1 + j)" by auto 3.336 from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1) 3.337 hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" by simp 3.338 @@ -1634,7 +1634,7 @@ 3.339 let ?e = "Inum (x # bs) e" 3.340 let ?v="(Sub (C -1) e)" 3.341 have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp 3.342 - from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp 3.343 + from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp 3.344 by simp (erule ballE[where x="1"], 3.345 simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) 3.346 next 3.347 @@ -1649,12 +1649,12 @@ 3.348 hence "x = - Inum (((x -d)) # bs) e + d" by simp 3.349 hence "x = - Inum (a # bs) e + d" 3.350 by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"]) 3.351 - with prems(11) have ?case using dp by simp} 3.352 + with 4(5) have ?case using dp by simp} 3.353 ultimately show ?case by blast 3.354 next 3.355 case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+ 3.356 let ?e = "Inum (x # bs) e" 3.357 - from prems have id: "j dvd d" by simp 3.358 + from 9 have id: "j dvd d" by simp 3.359 from c1 have "?p x = (j dvd (x+ ?e))" by simp 3.360 also have "\<dots> = (j dvd x - d + ?e)" 3.361 using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp 3.362 @@ -1663,7 +1663,7 @@ 3.363 next 3.364 case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+ 3.365 let ?e = "Inum (x # bs) e" 3.366 - from prems have id: "j dvd d" by simp 3.367 + from 10 have id: "j dvd d" by simp 3.368 from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp 3.369 also have "\<dots> = (\<not> j dvd x - d + ?e)" 3.370 using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp

4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 21 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.79 proof (simp add: numgcd_def) 4.80 let ?mc = "maxcoeff t" 4.81 let ?g = "numgcdh t ?mc" 4.82 @@ -679,10 +682,10 @@ 4.83 lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0" 4.84 proof (induct t rule: maxcoeff.induct) 4.85 case (2 n c t) 4.86 - hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ 4.87 - have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) 4.88 + hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp_all 4.89 + have "max (abs c) (maxcoeff t) \<ge> abs c" by simp 4.90 with cnz have "max (abs c) (maxcoeff t) > 0" by arith 4.91 - with prems show ?case by simp 4.92 + with 2 show ?case by simp 4.93 qed auto 4.94 4.95 lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" 4.96 @@ -710,7 +713,7 @@ 4.97 {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)} 4.98 moreover 4.99 { assume nnz: "n \<noteq> 0" 4.100 - {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)} 4.101 + {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci) } 4.102 moreover 4.103 {assume g1:"?g>1" hence g0: "?g > 0" by simp 4.104 from g1 nnz have gp0: "?g' \<noteq> 0" by simp 4.105 @@ -726,45 +729,48 @@ 4.106 have gpdgp: "?g' dvd ?g'" by simp 4.107 from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 4.108 have th2:"real ?g' * ?t = Inum bs ?t'" by simp 4.109 - from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) 4.110 + from g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) 4.111 also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp 4.112 also have "\<dots> = (Inum bs ?t' / real n)" 4.113 using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp 4.114 - finally have "?lhs = Inum bs t / real n" by (simp add: simpnum_ci) 4.115 - then have ?thesis using prems by (simp add: simp_num_pair_def)} 4.116 - ultimately have ?thesis by blast} 4.117 - ultimately have ?thesis by blast} 4.118 + finally have "?lhs = Inum bs t / real n" by simp 4.119 + then have ?thesis by (simp add: simp_num_pair_def) } 4.120 + ultimately have ?thesis by blast } 4.121 + ultimately have ?thesis by blast } 4.122 ultimately show ?thesis by blast 4.123 qed 4.124 4.125 lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" 4.126 shows "numbound0 t' \<and> n' >0" 4.127 proof- 4.128 - let ?t' = "simpnum t" 4.129 + let ?t' = "simpnum t" 4.130 let ?g = "numgcd ?t'" 4.131 let ?g' = "gcd n ?g" 4.132 - {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)} 4.133 + { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) } 4.134 moreover 4.135 { assume nnz: "n \<noteq> 0" 4.136 - {assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} 4.137 + { assume "\<not> ?g > 1" hence ?thesis using assms 4.138 + by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) } 4.139 moreover 4.140 - {assume g1:"?g>1" hence g0: "?g > 0" by simp 4.141 + { assume g1:"?g>1" hence g0: "?g > 0" by simp 4.142 from g1 nnz have gp0: "?g' \<noteq> 0" by simp 4.143 hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith 4.144 hence "?g'= 1 \<or> ?g' > 1" by arith 4.145 - moreover {assume "?g'=1" hence ?thesis using prems 4.146 - by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} 4.147 - moreover {assume g'1:"?g'>1" 4.148 + moreover { 4.149 + assume "?g' = 1" hence ?thesis using assms g1 4.150 + by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) } 4.151 + moreover { 4.152 + assume g'1: "?g' > 1" 4.153 have gpdg: "?g' dvd ?g" by simp 4.154 - have gpdd: "?g' dvd n" by simp 4.155 + have gpdd: "?g' dvd n" by simp 4.156 have gpdgp: "?g' dvd ?g'" by simp 4.157 from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" . 4.158 from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] 4.159 have "n div ?g' >0" by simp 4.160 - hence ?thesis using prems 4.161 - by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)} 4.162 - ultimately have ?thesis by blast} 4.163 - ultimately have ?thesis by blast} 4.164 + hence ?thesis using assms g1 g'1 4.165 + by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0) } 4.166 + ultimately have ?thesis by blast } 4.167 + ultimately have ?thesis by blast } 4.168 ultimately show ?thesis by blast 4.169 qed 4.170 4.171 @@ -962,14 +968,14 @@ 4.172 let ?sa = "rsplit0 a" let ?sb = "rsplit0 b" 4.173 let ?ca = "fst ?sa" let ?cb = "fst ?sb" 4.174 let ?ta = "snd ?sa" let ?tb = "snd ?sb" 4.175 - from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))" 4.176 + from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))" 4.177 by (cases "rsplit0 a") (auto simp add: Let_def split_def) 4.178 have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = 4.179 Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)" 4.180 by (simp add: Let_def split_def algebra_simps) 4.181 - also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a") auto 4.182 + also have "\<dots> = Inum bs a + Inum bs b" using 2 by (cases "rsplit0 a") auto 4.183 finally show ?case using nb by simp 4.184 -qed (auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric]) 4.185 +qed (auto simp add: Let_def split_def algebra_simps, simp add: right_distrib[symmetric]) 4.186 4.187 (* Linearize a formula*) 4.188 definition 4.189 @@ -1081,8 +1087,8 @@ 4.190 case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto 4.191 next 4.192 case (3 c e) 4.193 - from prems have nb: "numbound0 e" by simp 4.194 - from prems have cp: "real c > 0" by simp 4.195 + from 3 have nb: "numbound0 e" by simp 4.196 + from 3 have cp: "real c > 0" by simp 4.197 fix a 4.198 let ?e="Inum (a#bs) e" 4.199 let ?z = "(- ?e) / real c" 4.200 @@ -1098,8 +1104,8 @@ 4.201 thus ?case by blast 4.202 next 4.203 case (4 c e) 4.204 - from prems have nb: "numbound0 e" by simp 4.205 - from prems have cp: "real c > 0" by simp 4.206 + from 4 have nb: "numbound0 e" by simp 4.207 + from 4 have cp: "real c > 0" by simp 4.208 fix a 4.209 let ?e="Inum (a#bs) e" 4.210 let ?z = "(- ?e) / real c" 4.211 @@ -1115,8 +1121,8 @@ 4.212 thus ?case by blast 4.213 next 4.214 case (5 c e) 4.215 - from prems have nb: "numbound0 e" by simp 4.216 - from prems have cp: "real c > 0" by simp 4.217 + from 5 have nb: "numbound0 e" by simp 4.218 + from 5 have cp: "real c > 0" by simp 4.219 fix a 4.220 let ?e="Inum (a#bs) e" 4.221 let ?z = "(- ?e) / real c" 4.222 @@ -1131,8 +1137,8 @@ 4.223 thus ?case by blast 4.224 next 4.225 case (6 c e) 4.226 - from prems have nb: "numbound0 e" by simp 4.227 - from prems have cp: "real c > 0" by simp 4.228 + from 6 have nb: "numbound0 e" by simp 4.229 + from lp 6 have cp: "real c > 0" by simp 4.230 fix a 4.231 let ?e="Inum (a#bs) e" 4.232 let ?z = "(- ?e) / real c" 4.233 @@ -1147,8 +1153,8 @@ 4.234 thus ?case by blast 4.235 next 4.236 case (7 c e) 4.237 - from prems have nb: "numbound0 e" by simp 4.238 - from prems have cp: "real c > 0" by simp 4.239 + from 7 have nb: "numbound0 e" by simp 4.240 + from 7 have cp: "real c > 0" by simp 4.241 fix a 4.242 let ?e="Inum (a#bs) e" 4.243 let ?z = "(- ?e) / real c" 4.244 @@ -1163,8 +1169,8 @@ 4.245 thus ?case by blast 4.246 next 4.247 case (8 c e) 4.248 - from prems have nb: "numbound0 e" by simp 4.249 - from prems have cp: "real c > 0" by simp 4.250 + from 8 have nb: "numbound0 e" by simp 4.251 + from 8 have cp: "real c > 0" by simp 4.252 fix a 4.253 let ?e="Inum (a#bs) e" 4.254 let ?z = "(- ?e) / real c" 4.255 @@ -1189,8 +1195,8 @@ 4.256 case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto 4.257 next 4.258 case (3 c e) 4.259 - from prems have nb: "numbound0 e" by simp 4.260 - from prems have cp: "real c > 0" by simp 4.261 + from 3 have nb: "numbound0 e" by simp 4.262 + from 3 have cp: "real c > 0" by simp 4.263 fix a 4.264 let ?e="Inum (a#bs) e" 4.265 let ?z = "(- ?e) / real c" 4.266 @@ -1206,8 +1212,8 @@ 4.267 thus ?case by blast 4.268 next 4.269 case (4 c e) 4.270 - from prems have nb: "numbound0 e" by simp 4.271 - from prems have cp: "real c > 0" by simp 4.272 + from 4 have nb: "numbound0 e" by simp 4.273 + from 4 have cp: "real c > 0" by simp 4.274 fix a 4.275 let ?e="Inum (a#bs) e" 4.276 let ?z = "(- ?e) / real c" 4.277 @@ -1223,8 +1229,8 @@ 4.278 thus ?case by blast 4.279 next 4.280 case (5 c e) 4.281 - from prems have nb: "numbound0 e" by simp 4.282 - from prems have cp: "real c > 0" by simp 4.283 + from 5 have nb: "numbound0 e" by simp 4.284 + from 5 have cp: "real c > 0" by simp 4.285 fix a 4.286 let ?e="Inum (a#bs) e" 4.287 let ?z = "(- ?e) / real c" 4.288 @@ -1239,8 +1245,8 @@ 4.289 thus ?case by blast 4.290 next 4.291 case (6 c e) 4.292 - from prems have nb: "numbound0 e" by simp 4.293 - from prems have cp: "real c > 0" by simp 4.294 + from 6 have nb: "numbound0 e" by simp 4.295 + from 6 have cp: "real c > 0" by simp 4.296 fix a 4.297 let ?e="Inum (a#bs) e" 4.298 let ?z = "(- ?e) / real c" 4.299 @@ -1255,8 +1261,8 @@ 4.300 thus ?case by blast 4.301 next 4.302 case (7 c e) 4.303 - from prems have nb: "numbound0 e" by simp 4.304 - from prems have cp: "real c > 0" by simp 4.305 + from 7 have nb: "numbound0 e" by simp 4.306 + from 7 have cp: "real c > 0" by simp 4.307 fix a 4.308 let ?e="Inum (a#bs) e" 4.309 let ?z = "(- ?e) / real c" 4.310 @@ -1271,8 +1277,8 @@ 4.311 thus ?case by blast 4.312 next 4.313 case (8 c e) 4.314 - from prems have nb: "numbound0 e" by simp 4.315 - from prems have cp: "real c > 0" by simp 4.316 + from 8 have nb: "numbound0 e" by simp 4.317 + from 8 have cp: "real c > 0" by simp 4.318 fix a 4.319 let ?e="Inum (a#bs) e" 4.320 let ?z = "(- ?e) / real c" 4.321 @@ -1356,7 +1362,7 @@ 4.322 shows "(Ifm (x#bs) (usubst p (t,n)) = Ifm (((Inum (x#bs) t)/(real n))#bs) p) \<and> bound0 (usubst p (t,n))" (is "(?I x (usubst p (t,n)) = ?I ?u p) \<and> ?B p" is "(_ = ?I (?t/?n) p) \<and> _" is "(_ = ?I (?N x t /_) p) \<and> _") 4.323 using lp 4.324 proof(induct p rule: usubst.induct) 4.325 - case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 4.326 + case (5 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all 4.327 have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)" 4.328 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 4.329 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" 4.330 @@ -1366,7 +1372,7 @@ 4.331 using np by simp 4.332 finally show ?case using nbt nb by (simp add: algebra_simps) 4.333 next 4.334 - case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 4.335 + case (6 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all 4.336 have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)" 4.337 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 4.338 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)" 4.339 @@ -1376,7 +1382,7 @@ 4.340 using np by simp 4.341 finally show ?case using nbt nb by (simp add: algebra_simps) 4.342 next 4.343 - case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 4.344 + case (7 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all 4.345 have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" 4.346 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 4.347 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" 4.348 @@ -1386,7 +1392,7 @@ 4.349 using np by simp 4.350 finally show ?case using nbt nb by (simp add: algebra_simps) 4.351 next 4.352 - case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 4.353 + case (8 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all 4.354 have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)" 4.355 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 4.356 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)" 4.357 @@ -1396,7 +1402,7 @@ 4.358 using np by simp 4.359 finally show ?case using nbt nb by (simp add: algebra_simps) 4.360 next 4.361 - case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 4.362 + case (3 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all 4.363 from np have np: "real n \<noteq> 0" by simp 4.364 have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)" 4.365 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 4.366 @@ -1407,7 +1413,7 @@ 4.367 using np by simp 4.368 finally show ?case using nbt nb by (simp add: algebra_simps) 4.369 next 4.370 - case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 4.371 + case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all 4.372 from np have np: "real n \<noteq> 0" by simp 4.373 have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)" 4.374 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 4.375 @@ -1467,99 +1473,99 @@ 4.376 using lp px noS 4.377 proof (induct p rule: isrlfm.induct) 4.378 case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 4.379 - from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) 4.380 - hence pxc: "x < (- ?N x e) / real c" 4.381 - by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) 4.382 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.383 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.384 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.385 - moreover {assume y: "y < (-?N x e)/ real c" 4.386 - hence "y * real c < - ?N x e" 4.387 - by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.388 - hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 4.389 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.390 - moreover {assume y: "y > (- ?N x e) / real c" 4.391 - with yu have eu: "u > (- ?N x e) / real c" by auto 4.392 - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 4.393 - with lx pxc have "False" by auto 4.394 - hence ?case by simp } 4.395 - ultimately show ?case by blast 4.396 + from 5 have "x * real c + ?N x e < 0" by (simp add: algebra_simps) 4.397 + hence pxc: "x < (- ?N x e) / real c" 4.398 + by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) 4.399 + from 5 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.400 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.401 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.402 + moreover {assume y: "y < (-?N x e)/ real c" 4.403 + hence "y * real c < - ?N x e" 4.404 + by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.405 + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 4.406 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.407 + moreover {assume y: "y > (- ?N x e) / real c" 4.408 + with yu have eu: "u > (- ?N x e) / real c" by auto 4.409 + with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 4.410 + with lx pxc have "False" by auto 4.411 + hence ?case by simp } 4.412 + ultimately show ?case by blast 4.413 next 4.414 case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + 4.415 - from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) 4.416 - hence pxc: "x \<le> (- ?N x e) / real c" 4.417 - by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) 4.418 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.419 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.420 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.421 - moreover {assume y: "y < (-?N x e)/ real c" 4.422 - hence "y * real c < - ?N x e" 4.423 - by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.424 - hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 4.425 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.426 - moreover {assume y: "y > (- ?N x e) / real c" 4.427 - with yu have eu: "u > (- ?N x e) / real c" by auto 4.428 - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 4.429 - with lx pxc have "False" by auto 4.430 - hence ?case by simp } 4.431 - ultimately show ?case by blast 4.432 + from 6 have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) 4.433 + hence pxc: "x \<le> (- ?N x e) / real c" 4.434 + by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) 4.435 + from 6 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.436 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.437 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.438 + moreover {assume y: "y < (-?N x e)/ real c" 4.439 + hence "y * real c < - ?N x e" 4.440 + by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.441 + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 4.442 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.443 + moreover {assume y: "y > (- ?N x e) / real c" 4.444 + with yu have eu: "u > (- ?N x e) / real c" by auto 4.445 + with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 4.446 + with lx pxc have "False" by auto 4.447 + hence ?case by simp } 4.448 + ultimately show ?case by blast 4.449 next 4.450 case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 4.451 - from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) 4.452 - hence pxc: "x > (- ?N x e) / real c" 4.453 - by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) 4.454 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.455 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.456 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.457 - moreover {assume y: "y > (-?N x e)/ real c" 4.458 - hence "y * real c > - ?N x e" 4.459 - by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.460 - hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 4.461 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.462 - moreover {assume y: "y < (- ?N x e) / real c" 4.463 - with ly have eu: "l < (- ?N x e) / real c" by auto 4.464 - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 4.465 - with xu pxc have "False" by auto 4.466 - hence ?case by simp } 4.467 - ultimately show ?case by blast 4.468 + from 7 have "x * real c + ?N x e > 0" by (simp add: algebra_simps) 4.469 + hence pxc: "x > (- ?N x e) / real c" 4.470 + by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) 4.471 + from 7 have noSc: "\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.472 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.473 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.474 + moreover {assume y: "y > (-?N x e)/ real c" 4.475 + hence "y * real c > - ?N x e" 4.476 + by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.477 + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 4.478 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.479 + moreover {assume y: "y < (- ?N x e) / real c" 4.480 + with ly have eu: "l < (- ?N x e) / real c" by auto 4.481 + with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 4.482 + with xu pxc have "False" by auto 4.483 + hence ?case by simp } 4.484 + ultimately show ?case by blast 4.485 next 4.486 case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 4.487 - from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) 4.488 - hence pxc: "x \<ge> (- ?N x e) / real c" 4.489 - by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) 4.490 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.491 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.492 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.493 - moreover {assume y: "y > (-?N x e)/ real c" 4.494 - hence "y * real c > - ?N x e" 4.495 - by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.496 - hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 4.497 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.498 - moreover {assume y: "y < (- ?N x e) / real c" 4.499 - with ly have eu: "l < (- ?N x e) / real c" by auto 4.500 - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 4.501 - with xu pxc have "False" by auto 4.502 - hence ?case by simp } 4.503 - ultimately show ?case by blast 4.504 + from 8 have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) 4.505 + hence pxc: "x \<ge> (- ?N x e) / real c" 4.506 + by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) 4.507 + from 8 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.508 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.509 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 4.510 + moreover {assume y: "y > (-?N x e)/ real c" 4.511 + hence "y * real c > - ?N x e" 4.512 + by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 4.513 + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 4.514 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 4.515 + moreover {assume y: "y < (- ?N x e) / real c" 4.516 + with ly have eu: "l < (- ?N x e) / real c" by auto 4.517 + with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 4.518 + with xu pxc have "False" by auto 4.519 + hence ?case by simp } 4.520 + ultimately show ?case by blast 4.521 next 4.522 case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 4.523 - from cp have cnz: "real c \<noteq> 0" by simp 4.524 - from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) 4.525 - hence pxc: "x = (- ?N x e) / real c" 4.526 - by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) 4.527 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.528 - with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto 4.529 - with pxc show ?case by simp 4.530 + from cp have cnz: "real c \<noteq> 0" by simp 4.531 + from 3 have "x * real c + ?N x e = 0" by (simp add: algebra_simps) 4.532 + hence pxc: "x = (- ?N x e) / real c" 4.533 + by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) 4.534 + from 3 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.535 + with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto 4.536 + with pxc show ?case by simp 4.537 next 4.538 case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 4.539 - from cp have cnz: "real c \<noteq> 0" by simp 4.540 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.541 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.542 - hence "y* real c \<noteq> -?N x e" 4.543 - by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp 4.544 - hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) 4.545 - thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 4.546 - by (simp add: algebra_simps) 4.547 + from cp have cnz: "real c \<noteq> 0" by simp 4.548 + from 4 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 4.549 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 4.550 + hence "y* real c \<noteq> -?N x e" 4.551 + by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp 4.552 + hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) 4.553 + thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 4.554 + by (simp add: algebra_simps) 4.555 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"]) 4.556 4.557 lemma finite_set_intervals:

5.1 --- a/src/HOL/Decision_Procs/MIR.thy Mon Feb 21 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.113 proof (simp add: numgcd_def) 5.114 let ?mc = "maxcoeff t" 5.115 let ?g = "numgcdh t ?mc" 5.116 have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff) 5.117 have th2: "?mc \<ge> 0" by (rule maxcoeff_pos) 5.118 assume H: "numgcdh t ?mc > 1" 5.119 - from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . 5.120 + from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . 5.121 qed 5.122 5.123 lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t" 5.124 @@ -911,32 +912,33 @@ 5.125 in (bv, CF c a bi))" 5.126 "split_int a = (a,C 0)" 5.127 5.128 -lemma split_int:"\<And> tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs" 5.129 +lemma split_int: "\<And>tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs" 5.130 proof (induct t rule: split_int.induct) 5.131 case (2 c n b tv ti) 5.132 let ?bv = "fst (split_int b)" 5.133 let ?bi = "snd (split_int b)" 5.134 have "split_int b = (?bv,?bi)" by simp 5.135 - with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ 5.136 - from prems(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def) 5.137 - from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def) 5.138 + with 2(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ 5.139 + from 2(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def) 5.140 + from 2(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def) 5.141 next 5.142 case (3 c a b tv ti) 5.143 let ?bv = "fst (split_int b)" 5.144 let ?bi = "snd (split_int b)" 5.145 have "split_int b = (?bv,?bi)" by simp 5.146 - with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ 5.147 - from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def) 5.148 - from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) 5.149 + with 3(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ 5.150 + from 3(2) have tibi: "ti = CF c a ?bi" 5.151 + by (simp add: Let_def split_def) 5.152 + from 3(2) b[symmetric] bii show ?case 5.153 + by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) 5.154 qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps) 5.155 5.156 lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) " 5.157 -by (induct t rule: split_int.induct, auto simp add: Let_def split_def) 5.158 - 5.159 -definition 5.160 - numfloor:: "num \<Rightarrow> num" 5.161 + by (induct t rule: split_int.induct) (auto simp add: Let_def split_def) 5.162 + 5.163 +definition numfloor:: "num \<Rightarrow> num" 5.164 where 5.165 - numfloor_def: "numfloor t = (let (tv,ti) = split_int t in 5.166 + "numfloor t = (let (tv,ti) = split_int t in 5.167 (case tv of C i \<Rightarrow> numadd (tv,ti) 5.168 | _ \<Rightarrow> numadd(CF 1 tv (C 0),ti)))" 5.169 5.170 @@ -1022,13 +1024,13 @@ 5.171 hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ 5.172 have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) 5.173 with cnz have "max (abs c) (maxcoeff t) > 0" by arith 5.174 - with prems show ?case by simp 5.175 + with 2 show ?case by simp 5.176 next 5.177 case (3 c s t) 5.178 hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ 5.179 have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) 5.180 with cnz have "max (abs c) (maxcoeff t) > 0" by arith 5.181 - with prems show ?case by simp 5.182 + with 3 show ?case by simp 5.183 qed auto 5.184 5.185 lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" 5.186 @@ -1072,34 +1074,35 @@ 5.187 have gpdgp: "?g' dvd ?g'" by simp 5.188 from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 5.189 have th2:"real ?g' * ?t = Inum bs ?t'" by simp 5.190 - from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) 5.191 + from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) 5.192 also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp 5.193 also have "\<dots> = (Inum bs ?t' / real n)" 5.194 using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp 5.195 finally have "?lhs = Inum bs t / real n" by simp 5.196 - then have ?thesis using prems by (simp add: simp_num_pair_def)} 5.197 - ultimately have ?thesis by blast} 5.198 - ultimately have ?thesis by blast} 5.199 + then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) } 5.200 + ultimately have ?thesis by blast } 5.201 + ultimately have ?thesis by blast } 5.202 ultimately show ?thesis by blast 5.203 qed 5.204 5.205 -lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" 5.206 +lemma simp_num_pair_l: 5.207 + assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" 5.208 shows "numbound0 t' \<and> n' >0" 5.209 proof- 5.210 - let ?t' = "simpnum t" 5.211 + let ?t' = "simpnum t" 5.212 let ?g = "numgcd ?t'" 5.213 let ?g' = "gcd n ?g" 5.214 - {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)} 5.215 + { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) } 5.216 moreover 5.217 { assume nnz: "n \<noteq> 0" 5.218 - {assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def)} 5.219 + {assume "\<not> ?g > 1" hence ?thesis using assms by (auto simp add: Let_def simp_num_pair_def) } 5.220 moreover 5.221 {assume g1:"?g>1" hence g0: "?g > 0" by simp 5.222 from g1 nnz have gp0: "?g' \<noteq> 0" by simp 5.223 hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith 5.224 hence "?g'= 1 \<or> ?g' > 1" by arith 5.225 - moreover {assume "?g'=1" hence ?thesis using prems 5.226 - by (auto simp add: Let_def simp_num_pair_def)} 5.227 + moreover {assume "?g'=1" hence ?thesis using assms g1 g0 5.228 + by (auto simp add: Let_def simp_num_pair_def) } 5.229 moreover {assume g'1:"?g'>1" 5.230 have gpdg: "?g' dvd ?g" by simp 5.231 have gpdd: "?g' dvd n" by simp 5.232 @@ -1107,10 +1110,10 @@ 5.233 from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" . 5.234 from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] 5.235 have "n div ?g' >0" by simp 5.236 - hence ?thesis using prems 5.237 + hence ?thesis using assms g1 g'1 5.238 by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)} 5.239 - ultimately have ?thesis by blast} 5.240 - ultimately have ?thesis by blast} 5.241 + ultimately have ?thesis by blast } 5.242 + ultimately have ?thesis by blast } 5.243 ultimately show ?thesis by blast 5.244 qed 5.245 5.246 @@ -1131,43 +1134,43 @@ 5.247 "not (Or p q) = And (not p) (not q)" 5.248 "not p = NOT p" 5.249 lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)" 5.250 -by (induct p) auto 5.251 + by (induct p) auto 5.252 lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" 5.253 -by (induct p, auto) 5.254 + by (induct p) auto 5.255 lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" 5.256 -by (induct p, auto) 5.257 + by (induct p) auto 5.258 5.259 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 5.260 "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else 5.261 if p = q then p else And p q)" 5.262 lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)" 5.263 -by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all) 5.264 + by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all) 5.265 5.266 lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)" 5.267 -using conj_def by auto 5.268 + using conj_def by auto 5.269 lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)" 5.270 -using conj_def by auto 5.271 + using conj_def by auto 5.272 5.273 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 5.274 "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p 5.275 else if p=q then p else Or p q)" 5.276 5.277 lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)" 5.278 -by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) 5.279 + by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) 5.280 lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)" 5.281 -using disj_def by auto 5.282 + using disj_def by auto 5.283 lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)" 5.284 -using disj_def by auto 5.285 + using disj_def by auto 5.286 5.287 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 5.288 "imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p 5.289 else Imp p q)" 5.290 lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)" 5.291 -by (cases "p=F \<or> q=T",simp_all add: imp_def) 5.292 + by (cases "p=F \<or> q=T",simp_all add: imp_def) 5.293 lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)" 5.294 -using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) 5.295 + using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) 5.296 lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)" 5.297 -using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 5.298 + using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 5.299 5.300 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where 5.301 "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 5.302 @@ -1245,7 +1248,8 @@ 5.303 have gpdgp: "?g' dvd ?g'" by simp 5.304 from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 5.305 have th2:"real ?g' * ?t = Inum bs t" by simp 5.306 - from prems have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" 5.307 + from assms g1 g0 g'1 5.308 + have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" 5.309 by (simp add: simpdvd_def Let_def) 5.310 also have "\<dots> = (real d rdvd (Inum bs t))" 5.311 using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] 5.312 @@ -1544,9 +1548,8 @@ 5.313 lemma qelim_ci: 5.314 assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))" 5.315 shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)" 5.316 -using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] 5.317 -by(induct p rule: qelim.induct) 5.318 -(auto simp del: simpfm.simps) 5.319 + using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] 5.320 + by (induct p rule: qelim.induct) (auto simp del: simpfm.simps) 5.321 5.322 5.323 text {* The @{text "\<int>"} Part *} 5.324 @@ -1584,7 +1587,7 @@ 5.325 case (5 t n a) 5.326 let ?nt = "fst (zsplit0 t)" 5.327 let ?at = "snd (zsplit0 t)" 5.328 - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems 5.329 + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 5 5.330 by (simp add: Let_def split_def) 5.331 from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 5.332 from th2[simplified] th[simplified] show ?case by simp

6.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 21 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"