src/HOL/Integ/IntDiv.thy
 changeset 22091 d13ad9a479f9 parent 22026 cc60e54aa7cb child 22744 5cbe966d67a2
equal inserted replaced
`  1241   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])`
`  1241   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])`
`  1242   apply assumption`
`  1242   apply assumption`
`  1243   apply (simp add: mult_ac)`
`  1243   apply (simp add: mult_ac)`
`  1244   done`
`  1244   done`
`  1245 `
`  1245 `
`  1246 lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"`
`  1246 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"`
`  1247 proof`
`  1247 proof`
`  1248   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)`
`  1248   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)`
`  1249   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)`
`  1249   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)`
`  1250   hence "nat \<bar>x\<bar> = 1"  by simp`
`  1250   hence "nat \<bar>x\<bar> = 1"  by simp`
`  1251   thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)`
`  1251   thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)`