1.1 --- a/src/HOL/Divides.thy	Mon Mar 26 21:03:30 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 09:44:56 2012 +0200
     1.3 @@ -576,43 +576,27 @@
     1.4  
     1.5  lemma divmod_nat_zero:
     1.6    "divmod_nat m 0 = (0, m)"
     1.7 -proof -
     1.8 -  from divmod_nat_rel [of m 0] show ?thesis
     1.9 -    unfolding divmod_nat_div_mod divmod_nat_rel_def by simp
    1.10 +proof (rule divmod_nat_eq)
    1.11 +  show "divmod_nat_rel m 0 (0, m)"
    1.12 +    unfolding divmod_nat_rel_def by simp
    1.13  qed
    1.14  
    1.15  lemma divmod_nat_base:
    1.16    assumes "m < n"
    1.17    shows "divmod_nat m n = (0, m)"
    1.18 -proof -
    1.19 -  from divmod_nat_rel [of m n] show ?thesis
    1.20 -    unfolding divmod_nat_div_mod divmod_nat_rel_def
    1.21 -    using assms by (cases "m div n = 0")
    1.22 -      (auto simp add: gr0_conv_Suc [of "m div n"])
    1.23 +proof (rule divmod_nat_eq)
    1.24 +  show "divmod_nat_rel m n (0, m)"
    1.25 +    unfolding divmod_nat_rel_def using assms by simp
    1.26  qed
    1.27  
    1.28  lemma divmod_nat_step:
    1.29    assumes "0 < n" and "n \<le> m"
    1.30    shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
    1.31 -proof -
    1.32 -  from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" .
    1.33 -  with assms have m_div_n: "m div n \<ge> 1"
    1.34 -    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
    1.35 -  have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
    1.36 -  proof -
    1.37 -    from assms have
    1.38 -      "n \<noteq> 0"
    1.39 -      "\<And>k. m = Suc k * n + m mod n ==> m - n = (Suc k - Suc 0) * n + m mod n"
    1.40 -      by simp_all
    1.41 -    then show ?thesis using assms divmod_nat_m_n 
    1.42 -      by (cases "m div n")
    1.43 -         (simp_all only: divmod_nat_rel_def fst_conv snd_conv, simp_all)
    1.44 -  qed
    1.45 -  with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp
    1.46 -  moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" .
    1.47 -  ultimately have "m div n = Suc ((m - n) div n)"
    1.48 -    and "m mod n = (m - n) mod n" using m_div_n by simp_all
    1.49 -  then show ?thesis using divmod_nat_div_mod by simp
    1.50 +proof (rule divmod_nat_eq)
    1.51 +  have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
    1.52 +    by (rule divmod_nat_rel)
    1.53 +  thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
    1.54 +    unfolding divmod_nat_rel_def using assms by auto
    1.55  qed
    1.56  
    1.57  text {* The ''recursion'' equations for @{const div} and @{const mod} *}