src/HOL/Power.thy
 changeset 22955 48dc37776d1e parent 22853 7f000a385606 child 22957 82a799ae7579
equal inserted replaced
22954:372e3471fca2 22955:48dc37776d1e
`   316 `
`   316 `
`   317 lemma power_inject_base:`
`   317 lemma power_inject_base:`
`   318      "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]`
`   318      "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]`
`   319       ==> a = (b::'a::{ordered_semidom,recpower})"`
`   319       ==> a = (b::'a::{ordered_semidom,recpower})"`
`   320 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)`
`   320 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)`
`       `
`   321 `
`       `
`   322 lemma power_eq_imp_eq_base:`
`       `
`   323   fixes a b :: "'a::{ordered_semidom,recpower}"`
`       `
`   324   shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"`
`       `
`   325 by (cases n, simp_all, rule power_inject_base)`
`   321 `
`   326 `
`   322 `
`   327 `
`   323 subsection{*Exponentiation for the Natural Numbers*}`
`   328 subsection{*Exponentiation for the Natural Numbers*}`
`   324 `
`   329 `
`   325 instance nat :: power ..`
`   330 instance nat :: power ..`