equal
deleted
inserted
replaced
1165 let ?e="Inum (a#bs) e" |
1165 let ?e="Inum (a#bs) e" |
1166 let ?z = "(- ?e) / real c" |
1166 let ?z = "(- ?e) / real c" |
1167 {fix x |
1167 {fix x |
1168 assume xz: "x > ?z" |
1168 assume xz: "x > ?z" |
1169 with mult_strict_right_mono [OF xz cp] cp |
1169 with mult_strict_right_mono [OF xz cp] cp |
1170 have "(real c * x > - ?e)" by (simp add: mult_ac) |
1170 have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac) |
1171 hence "real c * x + ?e > 0" by arith |
1171 hence "real c * x + ?e > 0" by arith |
1172 hence "real c * x + ?e \<noteq> 0" by simp |
1172 hence "real c * x + ?e \<noteq> 0" by simp |
1173 with xz have "?P ?z x (Eq (CN 0 c e))" |
1173 with xz have "?P ?z x (Eq (CN 0 c e))" |
1174 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1174 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1175 hence "\<forall> x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp |
1175 hence "\<forall> x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp |
1182 let ?e="Inum (a#bs) e" |
1182 let ?e="Inum (a#bs) e" |
1183 let ?z = "(- ?e) / real c" |
1183 let ?z = "(- ?e) / real c" |
1184 {fix x |
1184 {fix x |
1185 assume xz: "x > ?z" |
1185 assume xz: "x > ?z" |
1186 with mult_strict_right_mono [OF xz cp] cp |
1186 with mult_strict_right_mono [OF xz cp] cp |
1187 have "(real c * x > - ?e)" by (simp add: mult_ac) |
1187 have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac) |
1188 hence "real c * x + ?e > 0" by arith |
1188 hence "real c * x + ?e > 0" by arith |
1189 hence "real c * x + ?e \<noteq> 0" by simp |
1189 hence "real c * x + ?e \<noteq> 0" by simp |
1190 with xz have "?P ?z x (NEq (CN 0 c e))" |
1190 with xz have "?P ?z x (NEq (CN 0 c e))" |
1191 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1191 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1192 hence "\<forall> x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp |
1192 hence "\<forall> x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp |
1199 let ?e="Inum (a#bs) e" |
1199 let ?e="Inum (a#bs) e" |
1200 let ?z = "(- ?e) / real c" |
1200 let ?z = "(- ?e) / real c" |
1201 {fix x |
1201 {fix x |
1202 assume xz: "x > ?z" |
1202 assume xz: "x > ?z" |
1203 with mult_strict_right_mono [OF xz cp] cp |
1203 with mult_strict_right_mono [OF xz cp] cp |
1204 have "(real c * x > - ?e)" by (simp add: mult_ac) |
1204 have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac) |
1205 hence "real c * x + ?e > 0" by arith |
1205 hence "real c * x + ?e > 0" by arith |
1206 with xz have "?P ?z x (Lt (CN 0 c e))" |
1206 with xz have "?P ?z x (Lt (CN 0 c e))" |
1207 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1207 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1208 hence "\<forall> x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp |
1208 hence "\<forall> x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp |
1209 thus ?case by blast |
1209 thus ?case by blast |
1215 let ?e="Inum (a#bs) e" |
1215 let ?e="Inum (a#bs) e" |
1216 let ?z = "(- ?e) / real c" |
1216 let ?z = "(- ?e) / real c" |
1217 {fix x |
1217 {fix x |
1218 assume xz: "x > ?z" |
1218 assume xz: "x > ?z" |
1219 with mult_strict_right_mono [OF xz cp] cp |
1219 with mult_strict_right_mono [OF xz cp] cp |
1220 have "(real c * x > - ?e)" by (simp add: mult_ac) |
1220 have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac) |
1221 hence "real c * x + ?e > 0" by arith |
1221 hence "real c * x + ?e > 0" by arith |
1222 with xz have "?P ?z x (Le (CN 0 c e))" |
1222 with xz have "?P ?z x (Le (CN 0 c e))" |
1223 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1223 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1224 hence "\<forall> x > ?z. ?P ?z x (Le (CN 0 c e))" by simp |
1224 hence "\<forall> x > ?z. ?P ?z x (Le (CN 0 c e))" by simp |
1225 thus ?case by blast |
1225 thus ?case by blast |
1231 let ?e="Inum (a#bs) e" |
1231 let ?e="Inum (a#bs) e" |
1232 let ?z = "(- ?e) / real c" |
1232 let ?z = "(- ?e) / real c" |
1233 {fix x |
1233 {fix x |
1234 assume xz: "x > ?z" |
1234 assume xz: "x > ?z" |
1235 with mult_strict_right_mono [OF xz cp] cp |
1235 with mult_strict_right_mono [OF xz cp] cp |
1236 have "(real c * x > - ?e)" by (simp add: mult_ac) |
1236 have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac) |
1237 hence "real c * x + ?e > 0" by arith |
1237 hence "real c * x + ?e > 0" by arith |
1238 with xz have "?P ?z x (Gt (CN 0 c e))" |
1238 with xz have "?P ?z x (Gt (CN 0 c e))" |
1239 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1239 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1240 hence "\<forall> x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp |
1240 hence "\<forall> x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp |
1241 thus ?case by blast |
1241 thus ?case by blast |
1247 let ?e="Inum (a#bs) e" |
1247 let ?e="Inum (a#bs) e" |
1248 let ?z = "(- ?e) / real c" |
1248 let ?z = "(- ?e) / real c" |
1249 {fix x |
1249 {fix x |
1250 assume xz: "x > ?z" |
1250 assume xz: "x > ?z" |
1251 with mult_strict_right_mono [OF xz cp] cp |
1251 with mult_strict_right_mono [OF xz cp] cp |
1252 have "(real c * x > - ?e)" by (simp add: mult_ac) |
1252 have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac) |
1253 hence "real c * x + ?e > 0" by arith |
1253 hence "real c * x + ?e > 0" by arith |
1254 with xz have "?P ?z x (Ge (CN 0 c e))" |
1254 with xz have "?P ?z x (Ge (CN 0 c e))" |
1255 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1255 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
1256 hence "\<forall> x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp |
1256 hence "\<forall> x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp |
1257 thus ?case by blast |
1257 thus ?case by blast |