# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1430312662 -3600
# Node ID 91477b3a2d6b6656fb54fc6e89c2234259787faa
# Parent  7478de1f5b5914b285f81bcdd9f1c88cc7e5ed14
Tidying. Improved simplification for numerals, esp in exponents.

diff -r 7478de1f5b59 -r 91477b3a2d6b src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Apr 28 22:57:07 2015 +0200
+++ b/src/HOL/Power.thy	Wed Apr 29 14:04:22 2015 +0100
@@ -131,9 +131,25 @@
 
 end
 
+text{*Extract constant factors from powers*}
 declare power_mult_distrib [where a = "numeral w" for w, simp]
 declare power_mult_distrib [where b = "numeral w" for w, simp]
 
+lemma power_add_numeral [simp]:
+  fixes a :: "'a :: monoid_mult"
+  shows "a^numeral m * a^numeral n = a^numeral (m + n)"
+  by (simp add: power_add [symmetric])
+
+lemma power_add_numeral2 [simp]:
+  fixes a :: "'a :: monoid_mult"
+  shows "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b"
+  by (simp add: mult.assoc [symmetric])
+
+lemma power_mult_numeral [simp]:
+  fixes a :: "'a :: monoid_mult"
+  shows"(a^numeral m)^numeral n = a^numeral (m * n)"
+  by (simp only: numeral_mult power_mult)
+
 context semiring_numeral
 begin
 
diff -r 7478de1f5b59 -r 91477b3a2d6b src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Apr 28 22:57:07 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Apr 29 14:04:22 2015 +0100
@@ -316,10 +316,10 @@
 lemma of_real_real_of_int_eq [simp]: "of_real (real z) = of_int z"
   by (simp add: real_of_int_def)
 
-lemma of_real_numeral: "of_real (numeral w) = numeral w"
+lemma of_real_numeral [simp]: "of_real (numeral w) = numeral w"
 using of_real_of_int_eq [of "numeral w"] by simp
 
-lemma of_real_neg_numeral: "of_real (- numeral w) = - numeral w"
+lemma of_real_neg_numeral [simp]: "of_real (- numeral w) = - numeral w"
 using of_real_of_int_eq [of "- numeral w"] by simp
 
 text{*Every real algebra has characteristic zero*}
diff -r 7478de1f5b59 -r 91477b3a2d6b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Apr 28 22:57:07 2015 +0200
+++ b/src/HOL/Transcendental.thy	Wed Apr 29 14:04:22 2015 +0100
@@ -10,6 +10,12 @@
 imports Binomial Series Deriv NthRoot
 begin
 
+lemma reals_Archimedean4:
+  assumes "0 < y" "0 \<le> x" 
+  obtains n where "real n * y \<le> x" "x < real (Suc n) * y"
+  using floor_correct [of "x/y"] assms
+  by (auto simp: Real.real_of_nat_Suc field_simps intro: that [of "nat (floor (x/y))"])
+
 lemma of_real_fact [simp]: "of_real (fact n) = fact n"
   by (metis of_nat_fact of_real_of_nat_eq)
 
@@ -222,6 +228,16 @@
 using powser_times_n_limit_0 [of "inverse x"]
 by (simp add: norm_divide divide_simps)
 
+lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) ---> (0::'a\<Colon>real_normed_field)) sequentially"
+  apply (clarsimp simp: lim_sequentially norm_divide dist_norm divide_simps)
+  apply (auto simp: mult_ac dest!: ex_less_of_nat_mult [of _ 1])
+  by (metis le_eq_less_or_eq less_trans linordered_comm_semiring_strict_class.comm_mult_strict_left_mono 
+          of_nat_less_0_iff of_nat_less_iff zero_less_mult_iff zero_less_one)
+
+lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) ---> (0::'a\<Colon>real_normed_field)) sequentially"
+  using lim_1_over_n
+  by (simp add: inverse_eq_divide)
+
 lemma sum_split_even_odd:
   fixes f :: "nat \<Rightarrow> real"
   shows
@@ -1127,7 +1143,7 @@
   obtain r :: real where r0: "0 < r" and r1: "r < 1"
     using dense [OF zero_less_one] by fast
   obtain N :: nat where N: "norm x < real N * r"
-    using reals_Archimedean3 [OF r0] by fast
+    using ex_less_of_nat_mult r0 real_of_nat_def by auto
   from r1 show ?thesis
   proof (rule summable_ratio_test [rule_format])
     fix n :: nat
@@ -3535,22 +3551,18 @@
     done
 qed
 
-lemma reals_Archimedean4:
-     "\<lbrakk>0 < y; 0 \<le> x\<rbrakk> \<Longrightarrow> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
-apply (auto dest!: reals_Archimedean3)
-apply (drule_tac x = x in spec, clarify)
-apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
- prefer 2 apply (erule LeastI)
-apply (case_tac "LEAST m::nat. x < real m * y", simp)
-apply (rename_tac m)
-apply (subgoal_tac "~ x < real m * y")
- prefer 2 apply (rule not_less_Least, simp, force)
+lemma reals_Archimedean4':
+     "\<lbrakk>0 < y; 0 \<le> x\<rbrakk> \<Longrightarrow> \<exists>n. real n * y \<le> x \<and> x < real (Suc n) * y"
+apply (rule_tac x="nat (floor (x/y))" in exI)
+using floor_correct [of "x/y"]
+apply (auto simp: Real.real_of_nat_Suc field_simps)
 done
 
 lemma cos_zero_lemma:
      "\<lbrakk>0 \<le> x; cos x = 0\<rbrakk> \<Longrightarrow>
       \<exists>n::nat. odd n & x = real n * (pi/2)"
-apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
+apply (erule reals_Archimedean4 [OF pi_gt_zero])
+apply (auto simp: )
 apply (subgoal_tac "0 \<le> x - real n * pi &
                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
 apply (auto simp: algebra_simps real_of_nat_Suc)