1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 09:54:39 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 10:20:31 2012 +0200
     1.3 @@ -574,12 +574,11 @@
     1.4  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
     1.5    using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
     1.6  
     1.7 -lemma divmod_nat_zero:
     1.8 -  "divmod_nat m 0 = (0, m)"
     1.9 -proof (rule divmod_nat_unique)
    1.10 -  show "divmod_nat_rel m 0 (0, m)"
    1.11 -    unfolding divmod_nat_rel_def by simp
    1.12 -qed
    1.13 +lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
    1.14 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
    1.15 +
    1.16 +lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
    1.17 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
    1.18  
    1.19  lemma divmod_nat_base:
    1.20    assumes "m < n"
    1.21 @@ -625,40 +624,30 @@
    1.22    shows "m mod n = (m - n) mod n"
    1.23    using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
    1.24  
    1.25 -instance proof -
    1.26 -  have [simp]: "\<And>n::nat. n div 0 = 0"
    1.27 +instance proof
    1.28 +  fix m n :: nat
    1.29 +  show "m div n * n + m mod n = m"
    1.30 +    using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
    1.31 +next
    1.32 +  fix m n q :: nat
    1.33 +  assume "n \<noteq> 0"
    1.34 +  then show "(q + m * n) div n = m + q div n"
    1.35 +    by (induct m) (simp_all add: le_div_geq)
    1.36 +next
    1.37 +  fix m n q :: nat
    1.38 +  assume "m \<noteq> 0"
    1.39 +  hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
    1.40 +    unfolding divmod_nat_rel_def
    1.41 +    by (auto split: split_if_asm, simp_all add: algebra_simps)
    1.42 +  moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
    1.43 +  ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
    1.44 +  thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
    1.45 +next
    1.46 +  fix n :: nat show "n div 0 = 0"
    1.47      by (simp add: div_nat_def divmod_nat_zero)
    1.48 -  have [simp]: "\<And>n::nat. 0 div n = 0"
    1.49 -  proof -
    1.50 -    fix n :: nat
    1.51 -    show "0 div n = 0"
    1.52 -      by (cases "n = 0") simp_all
    1.53 -  qed
    1.54 -  show "OFCLASS(nat, semiring_div_class)" proof
    1.55 -    fix m n :: nat
    1.56 -    show "m div n * n + m mod n = m"
    1.57 -      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
    1.58 -  next
    1.59 -    fix m n q :: nat
    1.60 -    assume "n \<noteq> 0"
    1.61 -    then show "(q + m * n) div n = m + q div n"
    1.62 -      by (induct m) (simp_all add: le_div_geq)
    1.63 -  next
    1.64 -    fix m n q :: nat
    1.65 -    assume "m \<noteq> 0"
    1.66 -    then show "(m * n) div (m * q) = n div q"
    1.67 -    proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
    1.68 -      case False then show ?thesis by auto
    1.69 -    next
    1.70 -      case True with `m \<noteq> 0`
    1.71 -        have "m > 0" and "n > 0" and "q > 0" by auto
    1.72 -      then have "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
    1.73 -        by (auto simp add: divmod_nat_rel_def) (simp_all add: algebra_simps)
    1.74 -      moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
    1.75 -      ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
    1.76 -      then show ?thesis by (simp add: div_nat_unique)
    1.77 -    qed
    1.78 -  qed simp_all
    1.79 +next
    1.80 +  fix n :: nat show "0 div n = 0"
    1.81 +    by (simp add: div_nat_def divmod_nat_zero_left)
    1.82  qed
    1.83  
    1.84  end