src/HOL/Power.thy
 changeset 14353 79f9fbef9106 parent 14348 744c868ee0b7 child 14438 6b41e98931f8
equal inserted replaced
14352:a8b1a44d8264 14353:79f9fbef9106
`   151 done`
`   151 done`
`   152 `
`   152 `
`   153 lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"`
`   153 lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"`
`   154 by force`
`   154 by force`
`   155 `
`   155 `
`       `
`   156 lemma nonzero_power_inverse:`
`       `
`   157   "a \<noteq> 0 ==> inverse ((a::'a::{field,ringpower}) ^ n) = (inverse a) ^ n"`
`       `
`   158 apply (induct_tac "n")`
`       `
`   159 apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)`
`       `
`   160 done`
`       `
`   161 `
`   156 text{*Perhaps these should be simprules.*}`
`   162 text{*Perhaps these should be simprules.*}`
`   157 lemma power_inverse:`
`   163 lemma power_inverse:`
`   158   "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"`
`   164   "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"`
`   159 apply (induct_tac "n")`
`   165 apply (induct_tac "n")`
`   160 apply (auto simp add: power_Suc inverse_mult_distrib)`
`   166 apply (auto simp add: power_Suc inverse_mult_distrib)`
`   161 done`
`   167 done`
`   162 `
`   168 `
`       `
`   169 lemma nonzero_power_divide: `
`       `
`   170     "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"`
`       `
`   171 by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)`
`       `
`   172 `
`       `
`   173 lemma power_divide: `
`       `
`   174     "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"`
`       `
`   175 apply (case_tac "b=0", simp add: power_0_left)`
`       `
`   176 apply (rule nonzero_power_divide) `
`       `
`   177 apply assumption `
`       `
`   178 done`
`       `
`   179 `
`   163 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"`
`   180 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"`
`   164 apply (induct_tac "n")`
`   181 apply (induct_tac "n")`
`   165 apply (auto simp add: power_Suc abs_mult)`
`   182 apply (auto simp add: power_Suc abs_mult)`
`       `
`   183 done`
`       `
`   184 `
`       `
`   185 lemma zero_less_power_abs_iff [simp]:`
`       `
`   186      "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" `
`       `
`   187 proof (induct "n")`
`       `
`   188   case 0`
`       `
`   189     show ?case by (simp add: zero_less_one)`
`       `
`   190 next`
`       `
`   191   case (Suc n)`
`       `
`   192     show ?case by (force simp add: prems power_Suc zero_less_mult_iff)`
`       `
`   193 qed`
`       `
`   194 `
`       `
`   195 lemma zero_le_power_abs [simp]:`
`       `
`   196      "(0::'a::{ordered_ring,ringpower}) \<le> (abs a)^n"`
`       `
`   197 apply (induct_tac "n")`
`       `
`   198 apply (auto simp add: zero_le_one zero_le_power)`
`   166 done`
`   199 done`
`   167 `
`   200 `
`   168 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"`
`   201 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"`
`   169 proof -`
`   202 proof -`
`   170   have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])`
`   203   have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])`
`   411 val power_strict_mono = thm"power_strict_mono";`
`   444 val power_strict_mono = thm"power_strict_mono";`
`   412 val power_eq_0_iff = thm"power_eq_0_iff";`
`   445 val power_eq_0_iff = thm"power_eq_0_iff";`
`   413 val field_power_eq_0_iff = thm"field_power_eq_0_iff";`
`   446 val field_power_eq_0_iff = thm"field_power_eq_0_iff";`
`   414 val field_power_not_zero = thm"field_power_not_zero";`
`   447 val field_power_not_zero = thm"field_power_not_zero";`
`   415 val power_inverse = thm"power_inverse";`
`   448 val power_inverse = thm"power_inverse";`
`       `
`   449 val nonzero_power_divide = thm"nonzero_power_divide";`
`       `
`   450 val power_divide = thm"power_divide";`
`   416 val power_abs = thm"power_abs";`
`   451 val power_abs = thm"power_abs";`
`       `
`   452 val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";`
`       `
`   453 val zero_le_power_abs = thm "zero_le_power_abs";`
`   417 val power_minus = thm"power_minus";`
`   454 val power_minus = thm"power_minus";`
`   418 val power_Suc_less = thm"power_Suc_less";`
`   455 val power_Suc_less = thm"power_Suc_less";`
`   419 val power_strict_decreasing = thm"power_strict_decreasing";`
`   456 val power_strict_decreasing = thm"power_strict_decreasing";`
`   420 val power_decreasing = thm"power_decreasing";`
`   457 val power_decreasing = thm"power_decreasing";`
`   421 val power_Suc_less_one = thm"power_Suc_less_one";`
`   458 val power_Suc_less_one = thm"power_Suc_less_one";`