src/HOL/Integ/IntDiv.thy
changeset 15320 dfc2654eea9f
parent 15251 bb6f072c8d10
child 15620 8ccdc8bc66a2
equal deleted inserted replaced
15319:b8da286bb9ad 15320:dfc2654eea9f
  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