src/HOL/Power.thy
changeset 66936 cf8d8fc23891
parent 66912 a99a7cbf0fb5
child 67226 ec32cdaab97b
     1.1 --- a/src/HOL/Power.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Power.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -306,6 +306,20 @@
     1.4  
     1.5  end
     1.6  
     1.7 +context semidom_divide
     1.8 +begin
     1.9 +
    1.10 +lemma power_diff:
    1.11 +  "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \<noteq> 0" and "n \<le> m"
    1.12 +proof -
    1.13 +  define q where "q = m - n"
    1.14 +  with \<open>n \<le> m\<close> have "m = q + n" by simp
    1.15 +  with \<open>a \<noteq> 0\<close> q_def show ?thesis
    1.16 +    by (simp add: power_add)
    1.17 +qed
    1.18 +
    1.19 +end
    1.20 +
    1.21  context algebraic_semidom
    1.22  begin
    1.23  
    1.24 @@ -370,11 +384,6 @@
    1.25  context field
    1.26  begin
    1.27  
    1.28 -lemma power_diff:
    1.29 -  assumes "a \<noteq> 0"
    1.30 -  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
    1.31 -  by (induct m n rule: diff_induct) (simp_all add: assms power_not_zero)
    1.32 -
    1.33  lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
    1.34    by (induct n) simp_all
    1.35