src/HOL/Real_Vector_Spaces.thy
 changeset 61609 77b453bd616f parent 61531 ab2e862263e7 child 61649 268d88ec9087
```--- a/src/HOL/Real_Vector_Spaces.thy	Tue Nov 03 11:20:21 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Nov 10 14:18:41 2015 +0000
@@ -341,12 +341,6 @@
lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z"
by (cases z rule: int_diff_cases, simp)

-lemma of_real_real_of_nat_eq [simp]: "of_real (real n) = of_nat n"
-
-lemma of_real_real_of_int_eq [simp]: "of_real (real z) = of_int z"
-
lemma of_real_numeral [simp]: "of_real (numeral w) = numeral w"
using of_real_of_int_eq [of "numeral w"] by simp

@@ -997,7 +991,7 @@
also have "\<dots> \<le> (\<Sum>i<m. norm (z - w))"
by (intro norm_setprod_diff) (auto simp add: assms)
also have "\<dots> = m * norm (z - w)"
+    by simp
finally show ?thesis .
qed

@@ -1291,7 +1285,7 @@

lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
-
+
lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: real_normed_algebra_1) = of_int \<bar>m - n\<bar>"
proof -
have "dist (of_int m) (of_int n :: 'a) = dist (of_int m :: 'a) (of_int m - (of_int (m - n)))"
@@ -1300,10 +1294,10 @@
finally show ?thesis .
qed

-lemma dist_of_nat:
+lemma dist_of_nat:
"dist (of_nat m) (of_nat n :: 'a :: real_normed_algebra_1) = of_int \<bar>int m - int n\<bar>"
by (subst (1 2) of_int_of_nat_eq [symmetric]) (rule dist_of_int)
-
+
subsection \<open>Bounded Linear and Bilinear Operators\<close>

locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
@@ -1571,7 +1565,7 @@
assumes "linear f" "bij f" shows "linear (inv f)"
using assms unfolding linear_def linear_axioms_def additive_def
by (auto simp: bij_is_surj bij_is_inj surj_f_inv_f intro!:  Hilbert_Choice.inv_f_eq)
-
+
instance real_normed_algebra_1 \<subseteq> perfect_space
proof
fix x::'a
@@ -1737,7 +1731,7 @@
qed
next
assume "Cauchy f"
-  show "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
+  show "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
proof (intro allI impI)
fix e :: real assume e: "e > 0"
with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
@@ -1959,8 +1953,7 @@
using ex_le_of_nat[of x] ..
note monoD[OF mono this]
also have "f (real_of_nat n) \<le> y"
-      by (rule LIMSEQ_le_const[OF limseq])
-         (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric])
+      by (rule LIMSEQ_le_const[OF limseq]) (auto intro: exI[of _ n] monoD[OF mono])
finally have "f x \<le> y" . }
note le = this
have "eventually (\<lambda>x. real N \<le> x) at_top"```