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} *}