# HG changeset patch
# User huffman
# Date 1332836431 -7200
# Node ID 5b6c5641498a4f3ff4d5ea3d2866b66b1ffb4450
# Parent  fb67b596067ff244fa4978f81dce126f25c975c2
simplify some proofs

diff -r fb67b596067f -r 5b6c5641498a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 09:54:39 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 10:20:31 2012 +0200
@@ -574,12 +574,11 @@
 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
 
-lemma divmod_nat_zero:
-  "divmod_nat m 0 = (0, m)"
-proof (rule divmod_nat_unique)
-  show "divmod_nat_rel m 0 (0, m)"
-    unfolding divmod_nat_rel_def by simp
-qed
+lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
+
+lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
 
 lemma divmod_nat_base:
   assumes "m < n"
@@ -625,40 +624,30 @@
   shows "m mod n = (m - n) mod n"
   using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
 
-instance proof -
-  have [simp]: "\<And>n::nat. n div 0 = 0"
+instance proof
+  fix m n :: nat
+  show "m div n * n + m mod n = m"
+    using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
+next
+  fix m n q :: nat
+  assume "n \<noteq> 0"
+  then show "(q + m * n) div n = m + q div n"
+    by (induct m) (simp_all add: le_div_geq)
+next
+  fix m n q :: nat
+  assume "m \<noteq> 0"
+  hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
+    unfolding divmod_nat_rel_def
+    by (auto split: split_if_asm, simp_all add: algebra_simps)
+  moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
+  ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
+  thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
+next
+  fix n :: nat show "n div 0 = 0"
     by (simp add: div_nat_def divmod_nat_zero)
-  have [simp]: "\<And>n::nat. 0 div n = 0"
-  proof -
-    fix n :: nat
-    show "0 div n = 0"
-      by (cases "n = 0") simp_all
-  qed
-  show "OFCLASS(nat, semiring_div_class)" proof
-    fix m n :: nat
-    show "m div n * n + m mod n = m"
-      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
-  next
-    fix m n q :: nat
-    assume "n \<noteq> 0"
-    then show "(q + m * n) div n = m + q div n"
-      by (induct m) (simp_all add: le_div_geq)
-  next
-    fix m n q :: nat
-    assume "m \<noteq> 0"
-    then show "(m * n) div (m * q) = n div q"
-    proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
-      case False then show ?thesis by auto
-    next
-      case True with `m \<noteq> 0`
-        have "m > 0" and "n > 0" and "q > 0" by auto
-      then have "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
-        by (auto simp add: divmod_nat_rel_def) (simp_all add: algebra_simps)
-      moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
-      ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
-      then show ?thesis by (simp add: div_nat_unique)
-    qed
-  qed simp_all
+next
+  fix n :: nat show "0 div n = 0"
+    by (simp add: div_nat_def divmod_nat_zero_left)
 qed
 
 end