--- a/src/HOL/Library/Primes.thy Sun Feb 22 17:32:55 2009 +0100
+++ b/src/HOL/Library/Primes.thy Sun Feb 22 17:33:16 2009 +0100
@@ -45,12 +45,14 @@
by (rule prime_dvd_square) (simp_all add: power2_eq_square)
-lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" by (induct n, auto)
+lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0"
+by (induct n, auto)
+
lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \<longleftrightarrow> x < y"
- using power_less_imp_less_base[of x "Suc n" y] power_strict_mono[of x y "Suc n"]
- by auto
+by(metis linorder_not_less not_less0 power_le_imp_le_base power_less_imp_less_base)
+
lemma exp_mono_le: "(x::nat) ^ (Suc n) \<le> y ^ (Suc n) \<longleftrightarrow> x \<le> y"
- by (simp only: linorder_not_less[symmetric] exp_mono_lt)
+by (simp only: linorder_not_less[symmetric] exp_mono_lt)
lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \<longleftrightarrow> x = y"
using power_inject_base[of x n y] by auto
--- a/src/HOL/Nat.thy Sun Feb 22 17:32:55 2009 +0100
+++ b/src/HOL/Nat.thy Sun Feb 22 17:33:16 2009 +0100
@@ -735,6 +735,11 @@
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
qed
+instance nat :: no_zero_divisors
+proof
+ fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
+qed
+
lemma nat_mult_1: "(1::nat) * n = n"
by simp
--- a/src/HOL/Parity.thy Sun Feb 22 17:32:55 2009 +0100
+++ b/src/HOL/Parity.thy Sun Feb 22 17:33:16 2009 +0100
@@ -228,20 +228,9 @@
lemma zero_le_odd_power: "odd n ==>
(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
- apply (simp add: odd_nat_equiv_def2)
- apply (erule exE)
- apply (erule ssubst)
- apply (subst power_Suc)
- apply (subst power_add)
- apply (subst zero_le_mult_iff)
- apply auto
- apply (subgoal_tac "x = 0 & y > 0")
- apply (erule conjE, assumption)
- apply (subst power_eq_0_iff [symmetric])
- apply (subgoal_tac "0 <= x^y * x^y")
- apply simp
- apply (rule zero_le_square)+
- done
+apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
+apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
+done
lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
(even n | (odd n & 0 <= x))"
--- a/src/HOL/Power.thy Sun Feb 22 17:32:55 2009 +0100
+++ b/src/HOL/Power.thy Sun Feb 22 17:33:16 2009 +0100
@@ -143,11 +143,13 @@
done
lemma power_eq_0_iff [simp]:
- "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
+ "(a^n = 0) \<longleftrightarrow>
+ (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
apply (induct "n")
-apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
+apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
done
+
lemma field_power_not_zero:
"a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
by force
@@ -370,6 +372,13 @@
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct "n", auto)
+lemma nat_power_eq_Suc_0_iff [simp]:
+ "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
+by (induct_tac m, auto)
+
+lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
+by simp
+
text{*Valid for the naturals, but what if @{text"0<i<1"}?
Premises cannot be weakened: consider the case where @{term "i=0"},
@{term "m=1"} and @{term "n=0"}.*}