# HG changeset patch
# User haftmann
# Date 1235320396 -3600
# Node ID c53242ef274ed2b97882f033e05e2f30c29e084c
# Parent  f84c2412e87056941cca8bb2a14f29277d3dd9fc# Parent  bf6b35c5c0fc9c736a9912683feae63157ded443
merged

diff -r f84c2412e870 -r c53242ef274e src/HOL/Library/Primes.thy
--- 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
diff -r f84c2412e870 -r c53242ef274e src/HOL/Nat.thy
--- 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
 
diff -r f84c2412e870 -r c53242ef274e src/HOL/Parity.thy
--- 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))"
diff -r f84c2412e870 -r c53242ef274e src/HOL/Power.thy
--- 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"}.*}