author nipkow Fri Nov 13 22:01:01 2009 +0100 (2009-11-13) changeset 33676 802f5e233e48 parent 33674 5241785055bc child 33677 ade8e136efb4
moved lemma from Algebra/IntRing to Ring_and_Field
 src/HOL/Algebra/IntRing.thy file | annotate | diff | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Nov 13 19:49:13 2009 +0100
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Nov 13 22:01:01 2009 +0100
1.3 @@ -12,32 +12,11 @@
1.4
1.5  subsection {* Some properties of @{typ int} *}
1.6
1.7 -lemma abseq_imp_dvd:
1.8 -  assumes a_lk: "abs l = abs (k::int)"
1.9 -  shows "l dvd k"
1.10 -proof -
1.11 -  from a_lk
1.12 -      have "nat (abs l) = nat (abs k)" by simp
1.13 -  hence "nat (abs l) dvd nat (abs k)" by simp
1.14 -  hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
1.15 -  hence "abs l dvd k" by simp
1.16 -  thus "l dvd k"
1.17 -  apply (unfold dvd_def, cases "l<0")
1.18 -   defer 1 apply clarsimp
1.19 -  proof (clarsimp)
1.20 -    fix k
1.21 -    assume l0: "l < 0"
1.22 -    have "- (l * k) = l * (-k)" by simp
1.23 -    thus "\<exists>ka. - (l * k) = l * ka" by fast
1.24 -  qed
1.25 -qed
1.26 -
1.27  lemma dvds_eq_abseq:
1.28    "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
1.29  apply rule
1.30   apply (simp add: zdvd_antisym_abs)
1.31 -apply (rule conjI)
1.32 - apply (simp add: abseq_imp_dvd)+
1.33 +apply (simp add: dvd_if_abs_eq)
1.34  done
1.35
1.36
```
```     2.1 --- a/src/HOL/Ring_and_Field.thy	Fri Nov 13 19:49:13 2009 +0100
2.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Nov 13 22:01:01 2009 +0100
2.3 @@ -1301,6 +1301,10 @@
2.4  lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
2.5    by (simp add: abs_if)
2.6
2.7 +lemma dvd_if_abs_eq:
2.8 +  "abs l = abs (k) \<Longrightarrow> l dvd k"
2.9 +by(subst abs_dvd_iff[symmetric]) simp
2.10 +
2.11  end
2.12
2.13  class ordered_field = field + ordered_idom
```