src/HOL/Power.thy
 changeset 22853 7f000a385606 parent 22624 7a6c8ed516ab child 22955 48dc37776d1e
equal inserted replaced
22852:2490d4b4671a 22853:7f000a385606
`   299    then have "b ^ Suc n < a ^ Suc n"`
`   299    then have "b ^ Suc n < a ^ Suc n"`
`   300      by (simp only: prems power_strict_mono)`
`   300      by (simp only: prems power_strict_mono)`
`   301    from le and this show "False"`
`   301    from le and this show "False"`
`   302       by (simp add: linorder_not_less [symmetric])`
`   302       by (simp add: linorder_not_less [symmetric])`
`   303  qed`
`   303  qed`
`       `
`   304 `
`       `
`   305 lemma power_less_imp_less_base:`
`       `
`   306   fixes a b :: "'a::{ordered_semidom,recpower}"`
`       `
`   307   assumes less: "a ^ n < b ^ n"`
`       `
`   308   assumes nonneg: "0 \<le> b"`
`       `
`   309   shows "a < b"`
`       `
`   310 proof (rule contrapos_pp [OF less])`
`       `
`   311   assume "~ a < b"`
`       `
`   312   hence "b \<le> a" by (simp only: linorder_not_less)`
`       `
`   313   hence "b ^ n \<le> a ^ n" using nonneg by (rule power_mono)`
`       `
`   314   thus "~ a ^ n < b ^ n" by (simp only: linorder_not_less)`
`       `
`   315 qed`
`   304 `
`   316 `
`   305 lemma power_inject_base:`
`   317 lemma power_inject_base:`
`   306      "[| 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 |]`
`   307       ==> a = (b::'a::{ordered_semidom,recpower})"`
`   319       ==> a = (b::'a::{ordered_semidom,recpower})"`
`   308 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)`