equal
deleted
inserted
replaced
1390 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1390 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1391 from cp have cnz: "c \<noteq> 0" by simp |
1391 from cp have cnz: "c \<noteq> 0" by simp |
1392 have "c div c\<le> l div c" |
1392 have "c div c\<le> l div c" |
1393 by (simp add: zdiv_mono1[OF clel cp]) |
1393 by (simp add: zdiv_mono1[OF clel cp]) |
1394 then have ldcp:"0 < l div c" |
1394 then have ldcp:"0 < l div c" |
1395 by (simp add: zdiv_self[OF cnz]) |
1395 by (simp add: div_self[OF cnz]) |
1396 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1396 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1397 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1397 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1398 by simp |
1398 by simp |
1399 hence "(l*x + (l div c) * Inum (x # bs) e < 0) = |
1399 hence "(l*x + (l div c) * Inum (x # bs) e < 0) = |
1400 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)" |
1400 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)" |
1408 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1408 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1409 from cp have cnz: "c \<noteq> 0" by simp |
1409 from cp have cnz: "c \<noteq> 0" by simp |
1410 have "c div c\<le> l div c" |
1410 have "c div c\<le> l div c" |
1411 by (simp add: zdiv_mono1[OF clel cp]) |
1411 by (simp add: zdiv_mono1[OF clel cp]) |
1412 then have ldcp:"0 < l div c" |
1412 then have ldcp:"0 < l div c" |
1413 by (simp add: zdiv_self[OF cnz]) |
1413 by (simp add: div_self[OF cnz]) |
1414 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1414 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1415 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1415 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1416 by simp |
1416 by simp |
1417 hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) = |
1417 hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) = |
1418 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" |
1418 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" |
1426 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1426 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1427 from cp have cnz: "c \<noteq> 0" by simp |
1427 from cp have cnz: "c \<noteq> 0" by simp |
1428 have "c div c\<le> l div c" |
1428 have "c div c\<le> l div c" |
1429 by (simp add: zdiv_mono1[OF clel cp]) |
1429 by (simp add: zdiv_mono1[OF clel cp]) |
1430 then have ldcp:"0 < l div c" |
1430 then have ldcp:"0 < l div c" |
1431 by (simp add: zdiv_self[OF cnz]) |
1431 by (simp add: div_self[OF cnz]) |
1432 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1432 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1433 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1433 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1434 by simp |
1434 by simp |
1435 hence "(l*x + (l div c)* Inum (x # bs) e > 0) = |
1435 hence "(l*x + (l div c)* Inum (x # bs) e > 0) = |
1436 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" |
1436 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" |
1444 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1444 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1445 from cp have cnz: "c \<noteq> 0" by simp |
1445 from cp have cnz: "c \<noteq> 0" by simp |
1446 have "c div c\<le> l div c" |
1446 have "c div c\<le> l div c" |
1447 by (simp add: zdiv_mono1[OF clel cp]) |
1447 by (simp add: zdiv_mono1[OF clel cp]) |
1448 then have ldcp:"0 < l div c" |
1448 then have ldcp:"0 < l div c" |
1449 by (simp add: zdiv_self[OF cnz]) |
1449 by (simp add: div_self[OF cnz]) |
1450 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1450 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1451 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1451 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1452 by simp |
1452 by simp |
1453 hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) = |
1453 hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) = |
1454 ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" |
1454 ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" |
1464 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1464 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1465 from cp have cnz: "c \<noteq> 0" by simp |
1465 from cp have cnz: "c \<noteq> 0" by simp |
1466 have "c div c\<le> l div c" |
1466 have "c div c\<le> l div c" |
1467 by (simp add: zdiv_mono1[OF clel cp]) |
1467 by (simp add: zdiv_mono1[OF clel cp]) |
1468 then have ldcp:"0 < l div c" |
1468 then have ldcp:"0 < l div c" |
1469 by (simp add: zdiv_self[OF cnz]) |
1469 by (simp add: div_self[OF cnz]) |
1470 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1470 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1471 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1471 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1472 by simp |
1472 by simp |
1473 hence "(l * x + (l div c) * Inum (x # bs) e = 0) = |
1473 hence "(l * x + (l div c) * Inum (x # bs) e = 0) = |
1474 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" |
1474 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" |
1482 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1482 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1483 from cp have cnz: "c \<noteq> 0" by simp |
1483 from cp have cnz: "c \<noteq> 0" by simp |
1484 have "c div c\<le> l div c" |
1484 have "c div c\<le> l div c" |
1485 by (simp add: zdiv_mono1[OF clel cp]) |
1485 by (simp add: zdiv_mono1[OF clel cp]) |
1486 then have ldcp:"0 < l div c" |
1486 then have ldcp:"0 < l div c" |
1487 by (simp add: zdiv_self[OF cnz]) |
1487 by (simp add: div_self[OF cnz]) |
1488 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1488 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1489 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1489 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1490 by simp |
1490 by simp |
1491 hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) = |
1491 hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) = |
1492 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" |
1492 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" |
1500 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1500 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1501 from cp have cnz: "c \<noteq> 0" by simp |
1501 from cp have cnz: "c \<noteq> 0" by simp |
1502 have "c div c\<le> l div c" |
1502 have "c div c\<le> l div c" |
1503 by (simp add: zdiv_mono1[OF clel cp]) |
1503 by (simp add: zdiv_mono1[OF clel cp]) |
1504 then have ldcp:"0 < l div c" |
1504 then have ldcp:"0 < l div c" |
1505 by (simp add: zdiv_self[OF cnz]) |
1505 by (simp add: div_self[OF cnz]) |
1506 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1506 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1507 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1507 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1508 by simp |
1508 by simp |
1509 hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
1509 hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
1510 also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) |
1510 also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) |
1517 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1517 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1518 from cp have cnz: "c \<noteq> 0" by simp |
1518 from cp have cnz: "c \<noteq> 0" by simp |
1519 have "c div c\<le> l div c" |
1519 have "c div c\<le> l div c" |
1520 by (simp add: zdiv_mono1[OF clel cp]) |
1520 by (simp add: zdiv_mono1[OF clel cp]) |
1521 then have ldcp:"0 < l div c" |
1521 then have ldcp:"0 < l div c" |
1522 by (simp add: zdiv_self[OF cnz]) |
1522 by (simp add: div_self[OF cnz]) |
1523 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1523 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1524 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1524 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1525 by simp |
1525 by simp |
1526 hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
1526 hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
1527 also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) |
1527 also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) |