author huffman Tue Mar 27 10:20:31 2012 +0200 (2012-03-27) changeset 47136 5b6c5641498a parent 47135 fb67b596067f child 47137 7f5f0531cae6
simplify some proofs
 src/HOL/Divides.thy file | annotate | diff | revisions
```     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)"