--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 15:22:03 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 15:44:54 2010 -0700
@@ -13,9 +13,6 @@
(* Because I do not want to type this all the time *)
lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
-(** move this **)
-declare norm_vec1[simp]
-
subsection {* Derivatives *}
text {* The definition is slightly tricky since we make it work over
@@ -94,16 +91,6 @@
subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}
-lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
-
-lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
- shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
- { assume ?l guess K using linear_bounded[OF `?l`] ..
- hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
- unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
- thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
- unfolding vec1_dest_vec1_simps by auto qed
-
lemma has_derivative_within_vec1_dest_vec1: fixes f::"real\<Rightarrow>real" shows
"((vec1 \<circ> f \<circ> dest_vec1) has_derivative (vec1 \<circ> f' \<circ> dest_vec1)) (at (vec1 x) within vec1 ` s)
= (f has_derivative f') (at x within s)"
--- a/src/HOL/Multivariate_Analysis/Vec1.thy Mon Apr 26 15:22:03 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Vec1.thy Mon Apr 26 15:44:54 2010 -0700
@@ -188,7 +188,7 @@
apply auto
done
-lemma norm_vec1: "norm(vec1 x) = abs(x)"
+lemma norm_vec1 [simp]: "norm(vec1 x) = abs(x)"
by (simp add: vec_def norm_real)
lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
@@ -386,4 +386,14 @@
apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule
apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
+lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
+
+lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
+ shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
+ { assume ?l guess K using linear_bounded[OF `?l`] ..
+ hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
+ unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
+ thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
+ unfolding vec1_dest_vec1_simps by auto qed
+
end