# HG changeset patch
# User huffman
# Date 1272321894 25200
# Node ID 6e5bfa8daa88dc6e627f3e37c9d0a61fbf8373d0
# Parent  1ad1cfeaec2dd360958b3465e167508ec7a360ba
move more lemmas into Vec1.thy

diff -r 1ad1cfeaec2d -r 6e5bfa8daa88 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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)"
diff -r 1ad1cfeaec2d -r 6e5bfa8daa88 src/HOL/Multivariate_Analysis/Vec1.thy
--- 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