author | haftmann |

Wed Mar 21 19:39:24 2018 +0100 (14 months ago) | |

changeset 67908 | 537f891d8f14 |

parent 67907 | 02a14c1cb917 |

child 67909 | f55b07f4d1ee |

tuned proof

1.1 --- a/src/HOL/Parity.thy Wed Mar 21 19:39:23 2018 +0100 1.2 +++ b/src/HOL/Parity.thy Wed Mar 21 19:39:24 2018 +0100 1.3 @@ -371,19 +371,23 @@ 1.4 with division_segment_euclidean_size [of r] 1.5 have "of_nat (euclidean_size r) = r" 1.6 by simp 1.7 - then have "r div of_nat m = of_nat (euclidean_size r) div of_nat m" 1.8 + have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0" 1.9 + by simp 1.10 + with remainder(6) have "r div (of_nat m * of_nat n) = 0" 1.11 by simp 1.12 - also have "\<dots> = of_nat (euclidean_size r div m)" 1.13 + with \<open>of_nat (euclidean_size r) = r\<close> 1.14 + have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0" 1.15 + by simp 1.16 + then have "of_nat (euclidean_size r div (m * n)) = 0" 1.17 by (simp add: of_nat_div) 1.18 - finally have "r div of_nat m = of_nat (euclidean_size r div m)" 1.19 - . 1.20 - with remainder(1-3) have "r div of_nat m div of_nat n = 0" 1.21 - by (auto intro!: div_eqI [of _ "of_nat (euclidean_size r div m)"]) 1.22 - (simp add: division_segment_mult euclidean_size_mult ac_simps less_mult_imp_div_less ) 1.23 + then have "of_nat (euclidean_size r div m div n) = 0" 1.24 + by (simp add: div_mult2_eq) 1.25 + with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0" 1.26 + by (simp add: of_nat_div) 1.27 with remainder(1) 1.28 have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n" 1.29 by simp 1.30 - with remainder(5-7) show ?thesis 1.31 + with remainder(5) remainder(7) show ?thesis 1.32 using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r] 1.33 by (simp add: ac_simps) 1.34 next