src/HOL/Power.thy
changeset 22955 48dc37776d1e
parent 22853 7f000a385606
child 22957 82a799ae7579
equal deleted 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 ..