src/HOL/Power.thy
changeset 14353 79f9fbef9106
parent 14348 744c868ee0b7
child 14438 6b41e98931f8
--- a/src/HOL/Power.thy	Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Power.thy	Mon Jan 12 16:51:45 2004 +0100
@@ -153,6 +153,12 @@
 lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
 by force
 
+lemma nonzero_power_inverse:
+  "a \<noteq> 0 ==> inverse ((a::'a::{field,ringpower}) ^ n) = (inverse a) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
+done
+
 text{*Perhaps these should be simprules.*}
 lemma power_inverse:
   "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
@@ -160,11 +166,38 @@
 apply (auto simp add: power_Suc inverse_mult_distrib)
 done
 
+lemma nonzero_power_divide: 
+    "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
+by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+
+lemma power_divide: 
+    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"
+apply (case_tac "b=0", simp add: power_0_left)
+apply (rule nonzero_power_divide) 
+apply assumption 
+done
+
 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
 apply (induct_tac "n")
 apply (auto simp add: power_Suc abs_mult)
 done
 
+lemma zero_less_power_abs_iff [simp]:
+     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" 
+proof (induct "n")
+  case 0
+    show ?case by (simp add: zero_less_one)
+next
+  case (Suc n)
+    show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
+qed
+
+lemma zero_le_power_abs [simp]:
+     "(0::'a::{ordered_ring,ringpower}) \<le> (abs a)^n"
+apply (induct_tac "n")
+apply (auto simp add: zero_le_one zero_le_power)
+done
+
 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
 proof -
   have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
@@ -413,7 +446,11 @@
 val field_power_eq_0_iff = thm"field_power_eq_0_iff";
 val field_power_not_zero = thm"field_power_not_zero";
 val power_inverse = thm"power_inverse";
+val nonzero_power_divide = thm"nonzero_power_divide";
+val power_divide = thm"power_divide";
 val power_abs = thm"power_abs";
+val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";
+val zero_le_power_abs = thm "zero_le_power_abs";
 val power_minus = thm"power_minus";
 val power_Suc_less = thm"power_Suc_less";
 val power_strict_decreasing = thm"power_strict_decreasing";