# HG changeset patch # User haftmann # Date 1521657564 -3600 # Node ID 537f891d8f146d5983ac7b3ac3052356d14c3dd6 # Parent 02a14c1cb9175f79818571f163c867ab34f38cca tuned proof diff -r 02a14c1cb917 -r 537f891d8f14 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Wed Mar 21 19:39:23 2018 +0100 +++ b/src/HOL/Parity.thy Wed Mar 21 19:39:24 2018 +0100 @@ -371,19 +371,23 @@ with division_segment_euclidean_size [of r] have "of_nat (euclidean_size r) = r" by simp - then have "r div of_nat m = of_nat (euclidean_size r) div of_nat m" + have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0" + by simp + with remainder(6) have "r div (of_nat m * of_nat n) = 0" by simp - also have "\ = of_nat (euclidean_size r div m)" + with \of_nat (euclidean_size r) = r\ + have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0" + by simp + then have "of_nat (euclidean_size r div (m * n)) = 0" by (simp add: of_nat_div) - finally have "r div of_nat m = of_nat (euclidean_size r div m)" - . - with remainder(1-3) have "r div of_nat m div of_nat n = 0" - by (auto intro!: div_eqI [of _ "of_nat (euclidean_size r div m)"]) - (simp add: division_segment_mult euclidean_size_mult ac_simps less_mult_imp_div_less ) + then have "of_nat (euclidean_size r div m div n) = 0" + by (simp add: div_mult2_eq) + with \of_nat (euclidean_size r) = r\ have "r div of_nat m div of_nat n = 0" + by (simp add: of_nat_div) with remainder(1) have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n" by simp - with remainder(5-7) show ?thesis + with remainder(5) remainder(7) show ?thesis using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r] by (simp add: ac_simps) next