1398 have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" |
1398 have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" |
1399 (is "_ = (j dvd c*x - ?e)") by simp |
1399 (is "_ = (j dvd c*x - ?e)") by simp |
1400 also have "\<dots> = (j dvd (- (c*x - ?e)))" |
1400 also have "\<dots> = (j dvd (- (c*x - ?e)))" |
1401 by (simp only: dvd_minus_iff) |
1401 by (simp only: dvd_minus_iff) |
1402 also have "\<dots> = (j dvd (c* (- x)) + ?e)" |
1402 also have "\<dots> = (j dvd (c* (- x)) + ?e)" |
1403 apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib) |
1403 by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib) |
1404 apply (simp add: algebra_simps) |
1404 (simp add: algebra_simps) |
1405 done |
|
1406 also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" |
1405 also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" |
1407 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp |
1406 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp |
1408 finally show ?case . |
1407 finally show ?case . |
1409 next |
1408 next |
1410 case (10 j c e) hence nb: "numbound0 e" by simp |
1409 case (10 j c e) hence nb: "numbound0 e" by simp |
1411 have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" |
1410 have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" |
1412 (is "_ = (j dvd c*x - ?e)") by simp |
1411 (is "_ = (j dvd c*x - ?e)") by simp |
1413 also have "\<dots> = (j dvd (- (c*x - ?e)))" |
1412 also have "\<dots> = (j dvd (- (c*x - ?e)))" |
1414 by (simp only: dvd_minus_iff) |
1413 by (simp only: dvd_minus_iff) |
1415 also have "\<dots> = (j dvd (c* (- x)) + ?e)" |
1414 also have "\<dots> = (j dvd (c* (- x)) + ?e)" |
1416 apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib) |
1415 by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib) |
1417 apply (simp add: algebra_simps) |
1416 (simp add: algebra_simps) |
1418 done |
|
1419 also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" |
1417 also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" |
1420 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp |
1418 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp |
1421 finally show ?case by simp |
1419 finally show ?case by simp |
1422 qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc) |
1420 qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc) |
1423 |
1421 |