src/HOL/Integ/IntDiv.thy
 changeset 15320 dfc2654eea9f parent 15251 bb6f072c8d10 child 15620 8ccdc8bc66a2
equal inserted replaced
`  1192 `
`  1192 `
`  1193 lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"`
`  1193 lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"`
`  1194 apply (induct "n")`
`  1194 apply (induct "n")`
`  1195 apply (auto simp add: zero_le_mult_iff)`
`  1195 apply (auto simp add: zero_le_mult_iff)`
`  1196 done`
`  1196 done`
`       `
`  1197 `
`       `
`  1198 theorem zpower_int: "(int m)^n = int (m^n)"`
`       `
`  1199   by (induct n) (simp_all add: zmult_int)`
`  1197 `
`  1200 `
`  1198 lemma zdiv_int: "int (a div b) = (int a) div (int b)"`
`  1201 lemma zdiv_int: "int (a div b) = (int a) div (int b)"`
`  1199 apply (subst split_div, auto)`
`  1202 apply (subst split_div, auto)`
`  1200 apply (subst split_zdiv, auto)`
`  1203 apply (subst split_zdiv, auto)`
`  1201 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)`
`  1204 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)`
`  1315 val zpower_zmod = thm "zpower_zmod";`
`  1318 val zpower_zmod = thm "zpower_zmod";`
`  1316 val zpower_zadd_distrib = thm "zpower_zadd_distrib";`
`  1319 val zpower_zadd_distrib = thm "zpower_zadd_distrib";`
`  1317 val zpower_zpower = thm "zpower_zpower";`
`  1320 val zpower_zpower = thm "zpower_zpower";`
`  1318 val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";`
`  1321 val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";`
`  1319 val zero_le_zpower_abs = thm "zero_le_zpower_abs";`
`  1322 val zero_le_zpower_abs = thm "zero_le_zpower_abs";`
`       `
`  1323 val zpower_int = thm "zpower_int";`
`  1320 *}`
`  1324 *}`
`  1321 `
`  1325 `
`  1322 end`
`  1326 end`