--- a/src/HOL/Integ/Parity.thy Thu Jun 16 18:25:54 2005 +0200
+++ b/src/HOL/Integ/Parity.thy Thu Jun 16 19:51:04 2005 +0200
@@ -28,13 +28,6 @@
even_nat_def: "even (x::nat) == even (int x)"
-subsection {* Casting a nat power to an integer *}
-
-lemma zpow_int: "int (x^y) = (int x)^y"
- apply (induct y)
- apply (simp, simp add: zmult_int [THEN sym])
- done
-
subsection {* Even and odd are mutually exclusive *}
lemma int_pos_lt_two_imp_zero_or_one:
@@ -143,7 +136,7 @@
by (simp add: even_nat_def)
lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
- by (simp add: even_nat_def zmult_int [THEN sym])
+ by (simp add: even_nat_def int_mult)
lemma even_nat_sum: "even ((x::nat) + y) =
((even x & even y) | (odd x & odd y))"
@@ -163,7 +156,7 @@
lemmas even_nat_suc = even_nat_Suc
lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
- by (simp add: even_nat_def zpow_int)
+ by (simp add: even_nat_def int_power)
lemma even_nat_zero: "even (0::nat)"
by (simp add: even_nat_def)