src/HOL/Multivariate_Analysis/Linear_Algebra.thy

 
 
 subsection \<open>Archimedean properties and useful consequences\<close>
 
 lemma real_arch_simple: "\<exists>n::nat. x \<le> real n"
-  unfolding real_of_nat_def by (rule ex_le_of_nat)
+  by (rule ex_le_of_nat)
 
 lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
   using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
-  by (auto simp add: field_simps cong: conj_cong simp del: real_of_nat_Suc)
+  by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)
 
 text\<open>Bernoulli's inequality\<close>
 lemma Bernoulli_inequality:
   fixes x :: real
   assumes "-1 \<le> x"

 next
   case (Suc n)
   have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
     by (simp add: algebra_simps)
   also have "... = (1 + x) * (1 + n*x)"
-    by (auto simp: power2_eq_square algebra_simps  real_of_nat_Suc)
+    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
   also have "... \<le> (1 + x) ^ Suc n"
     using Suc.hyps assms mult_left_mono by fastforce
   finally show ?case .
 qed
 

 lemma forall_pos_mono_1:
   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
     (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
   apply (rule forall_pos_mono)
   apply auto
-  apply (metis Suc_pred real_of_nat_Suc)
+  apply (metis Suc_pred of_nat_Suc)
   done
 
 lemma real_archimedian_rdiv_eq_0:
   assumes x0: "x \<ge> 0"
     and c: "c \<ge> 0"

     also have "\<dots> \<le> e + e"
       unfolding real_norm_def
       by (intro add_mono norm_bound_Basis_le i fPs) auto
     finally show "(\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le> 2*e" by simp
   qed
-  also have "\<dots> = 2 * real DIM('n) * e"
-    by (simp add: real_of_nat_def)
+  also have "\<dots> = 2 * real DIM('n) * e" by simp
   finally show ?thesis .
 qed
 
 
 subsection \<open>Linearity and Bilinearity continued\<close>

 lemma independent_bound:
   fixes S :: "'a::euclidean_space set"
   shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
   using independent_span_bound[OF finite_Basis, of S] by auto
 
-corollary 
+corollary
   fixes S :: "'a::euclidean_space set"
   assumes "independent S"
   shows independent_imp_finite: "finite S" and independent_card_le:"card S \<le> DIM('a)"
 using assms independent_bound by auto
-  
+
 lemma dependent_biggerset:
   fixes S :: "'a::euclidean_space set"
   shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
   by (metis independent_bound not_less)
 

     by (auto intro: real_sqrt_pow2)
   have th: "sqrt (real ?d) * infnorm x \<ge> 0"
     by (simp add: zero_le_mult_iff infnorm_pos_le)
   have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
     unfolding power_mult_distrib d2
-    unfolding real_of_nat_def
     apply (subst euclidean_inner)
     apply (subst power2_abs[symmetric])
     apply (rule order_trans[OF setsum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
     apply (auto simp add: power2_eq_square[symmetric])
     apply (subst power2_abs[symmetric])