tuned proof
authorhaftmann
Wed Mar 21 19:39:24 2018 +0100 (14 months ago)
changeset 67908537f891d8f14
parent 67907 02a14c1cb917
child 67909 f55b07f4d1ee
tuned proof
src/HOL/Parity.thy
     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