move everything related to 'norm' method into new theory file Norm_Arith.thy
authorhuffman
Wed Aug 24 15:06:13 2011 -0700 (2011-08-24)
changeset 44516d9a496ae5d9d
parent 44515 fcaacc214a36
child 44517 68e8eb0ce8aa
move everything related to 'norm' method into new theory file Norm_Arith.thy
src/HOL/IsaMakefile
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Norm_Arith.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Aug 24 12:39:42 2011 -0700
     1.2 +++ b/src/HOL/IsaMakefile	Wed Aug 24 15:06:13 2011 -0700
     1.3 @@ -1175,6 +1175,7 @@
     1.4    Multivariate_Analysis/L2_Norm.thy					\
     1.5    Multivariate_Analysis/Linear_Algebra.thy				\
     1.6    Multivariate_Analysis/Multivariate_Analysis.thy			\
     1.7 +  Multivariate_Analysis/Norm_Arith.thy					\
     1.8    Multivariate_Analysis/Operator_Norm.thy				\
     1.9    Multivariate_Analysis/Path_Connected.thy				\
    1.10    Multivariate_Analysis/ROOT.ML						\
     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 12:39:42 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 15:06:13 2011 -0700
     2.3 @@ -10,9 +10,6 @@
     2.4    "~~/src/HOL/Library/Infinite_Set"
     2.5    L2_Norm
     2.6    "~~/src/HOL/Library/Convex"
     2.7 -  "~~/src/HOL/Library/Sum_of_Squares"
     2.8 -uses
     2.9 -  ("normarith.ML")
    2.10  begin
    2.11  
    2.12  lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
    2.13 @@ -154,111 +151,6 @@
    2.14    then show "x = y" by (simp)
    2.15  qed
    2.16  
    2.17 -subsection{* General linear decision procedure for normed spaces. *}
    2.18 -
    2.19 -lemma norm_cmul_rule_thm:
    2.20 -  fixes x :: "'a::real_normed_vector"
    2.21 -  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
    2.22 -  unfolding norm_scaleR
    2.23 -  apply (erule mult_left_mono)
    2.24 -  apply simp
    2.25 -  done
    2.26 -
    2.27 -  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
    2.28 -lemma norm_add_rule_thm:
    2.29 -  fixes x1 x2 :: "'a::real_normed_vector"
    2.30 -  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
    2.31 -  by (rule order_trans [OF norm_triangle_ineq add_mono])
    2.32 -
    2.33 -lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
    2.34 -  by (simp add: field_simps)
    2.35 -
    2.36 -lemma pth_1:
    2.37 -  fixes x :: "'a::real_normed_vector"
    2.38 -  shows "x == scaleR 1 x" by simp
    2.39 -
    2.40 -lemma pth_2:
    2.41 -  fixes x :: "'a::real_normed_vector"
    2.42 -  shows "x - y == x + -y" by (atomize (full)) simp
    2.43 -
    2.44 -lemma pth_3:
    2.45 -  fixes x :: "'a::real_normed_vector"
    2.46 -  shows "- x == scaleR (-1) x" by simp
    2.47 -
    2.48 -lemma pth_4:
    2.49 -  fixes x :: "'a::real_normed_vector"
    2.50 -  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
    2.51 -
    2.52 -lemma pth_5:
    2.53 -  fixes x :: "'a::real_normed_vector"
    2.54 -  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
    2.55 -
    2.56 -lemma pth_6:
    2.57 -  fixes x :: "'a::real_normed_vector"
    2.58 -  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
    2.59 -  by (simp add: scaleR_right_distrib)
    2.60 -
    2.61 -lemma pth_7:
    2.62 -  fixes x :: "'a::real_normed_vector"
    2.63 -  shows "0 + x == x" and "x + 0 == x" by simp_all
    2.64 -
    2.65 -lemma pth_8:
    2.66 -  fixes x :: "'a::real_normed_vector"
    2.67 -  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
    2.68 -  by (simp add: scaleR_left_distrib)
    2.69 -
    2.70 -lemma pth_9:
    2.71 -  fixes x :: "'a::real_normed_vector" shows
    2.72 -  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
    2.73 -  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
    2.74 -  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
    2.75 -  by (simp_all add: algebra_simps)
    2.76 -
    2.77 -lemma pth_a:
    2.78 -  fixes x :: "'a::real_normed_vector"
    2.79 -  shows "scaleR 0 x + y == y" by simp
    2.80 -
    2.81 -lemma pth_b:
    2.82 -  fixes x :: "'a::real_normed_vector" shows
    2.83 -  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
    2.84 -  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
    2.85 -  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
    2.86 -  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
    2.87 -  by (simp_all add: algebra_simps)
    2.88 -
    2.89 -lemma pth_c:
    2.90 -  fixes x :: "'a::real_normed_vector" shows
    2.91 -  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
    2.92 -  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
    2.93 -  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
    2.94 -  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
    2.95 -  by (simp_all add: algebra_simps)
    2.96 -
    2.97 -lemma pth_d:
    2.98 -  fixes x :: "'a::real_normed_vector"
    2.99 -  shows "x + 0 == x" by simp
   2.100 -
   2.101 -lemma norm_imp_pos_and_ge:
   2.102 -  fixes x :: "'a::real_normed_vector"
   2.103 -  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
   2.104 -  by atomize auto
   2.105 -
   2.106 -lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
   2.107 -
   2.108 -lemma norm_pths:
   2.109 -  fixes x :: "'a::real_normed_vector" shows
   2.110 -  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
   2.111 -  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   2.112 -  using norm_ge_zero[of "x - y"] by auto
   2.113 -
   2.114 -use "normarith.ML"
   2.115 -
   2.116 -method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   2.117 -*} "prove simple linear statements about vector norms"
   2.118 -
   2.119 -
   2.120 -text{* Hence more metric properties. *}
   2.121 -
   2.122  lemma norm_triangle_half_r:
   2.123    shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
   2.124    using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
   2.125 @@ -274,16 +166,6 @@
   2.126  lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
   2.127    by (metis basic_trans_rules(21) norm_triangle_ineq)
   2.128  
   2.129 -lemma dist_triangle_add:
   2.130 -  fixes x y x' y' :: "'a::real_normed_vector"
   2.131 -  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
   2.132 -  by norm
   2.133 -
   2.134 -lemma dist_triangle_add_half:
   2.135 -  fixes x x' y y' :: "'a::real_normed_vector"
   2.136 -  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
   2.137 -  by norm
   2.138 -
   2.139  lemma setsum_clauses:
   2.140    shows "setsum f {} = 0"
   2.141    and "finite S \<Longrightarrow> setsum f (insert x S) =
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Wed Aug 24 15:06:13 2011 -0700
     3.3 @@ -0,0 +1,124 @@
     3.4 +(*  Title:      HOL/Multivariate_Analysis/Norm_Arith.thy
     3.5 +    Author:     Amine Chaieb, University of Cambridge
     3.6 +*)
     3.7 +
     3.8 +header {* General linear decision procedure for normed spaces *}
     3.9 +
    3.10 +theory Norm_Arith
    3.11 +imports "~~/src/HOL/Library/Sum_of_Squares"
    3.12 +uses ("normarith.ML")
    3.13 +begin
    3.14 +
    3.15 +lemma norm_cmul_rule_thm:
    3.16 +  fixes x :: "'a::real_normed_vector"
    3.17 +  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
    3.18 +  unfolding norm_scaleR
    3.19 +  apply (erule mult_left_mono)
    3.20 +  apply simp
    3.21 +  done
    3.22 +
    3.23 +  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
    3.24 +lemma norm_add_rule_thm:
    3.25 +  fixes x1 x2 :: "'a::real_normed_vector"
    3.26 +  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
    3.27 +  by (rule order_trans [OF norm_triangle_ineq add_mono])
    3.28 +
    3.29 +lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
    3.30 +  by (simp add: field_simps)
    3.31 +
    3.32 +lemma pth_1:
    3.33 +  fixes x :: "'a::real_normed_vector"
    3.34 +  shows "x == scaleR 1 x" by simp
    3.35 +
    3.36 +lemma pth_2:
    3.37 +  fixes x :: "'a::real_normed_vector"
    3.38 +  shows "x - y == x + -y" by (atomize (full)) simp
    3.39 +
    3.40 +lemma pth_3:
    3.41 +  fixes x :: "'a::real_normed_vector"
    3.42 +  shows "- x == scaleR (-1) x" by simp
    3.43 +
    3.44 +lemma pth_4:
    3.45 +  fixes x :: "'a::real_normed_vector"
    3.46 +  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
    3.47 +
    3.48 +lemma pth_5:
    3.49 +  fixes x :: "'a::real_normed_vector"
    3.50 +  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
    3.51 +
    3.52 +lemma pth_6:
    3.53 +  fixes x :: "'a::real_normed_vector"
    3.54 +  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
    3.55 +  by (simp add: scaleR_right_distrib)
    3.56 +
    3.57 +lemma pth_7:
    3.58 +  fixes x :: "'a::real_normed_vector"
    3.59 +  shows "0 + x == x" and "x + 0 == x" by simp_all
    3.60 +
    3.61 +lemma pth_8:
    3.62 +  fixes x :: "'a::real_normed_vector"
    3.63 +  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
    3.64 +  by (simp add: scaleR_left_distrib)
    3.65 +
    3.66 +lemma pth_9:
    3.67 +  fixes x :: "'a::real_normed_vector" shows
    3.68 +  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
    3.69 +  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
    3.70 +  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
    3.71 +  by (simp_all add: algebra_simps)
    3.72 +
    3.73 +lemma pth_a:
    3.74 +  fixes x :: "'a::real_normed_vector"
    3.75 +  shows "scaleR 0 x + y == y" by simp
    3.76 +
    3.77 +lemma pth_b:
    3.78 +  fixes x :: "'a::real_normed_vector" shows
    3.79 +  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
    3.80 +  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
    3.81 +  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
    3.82 +  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
    3.83 +  by (simp_all add: algebra_simps)
    3.84 +
    3.85 +lemma pth_c:
    3.86 +  fixes x :: "'a::real_normed_vector" shows
    3.87 +  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
    3.88 +  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
    3.89 +  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
    3.90 +  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
    3.91 +  by (simp_all add: algebra_simps)
    3.92 +
    3.93 +lemma pth_d:
    3.94 +  fixes x :: "'a::real_normed_vector"
    3.95 +  shows "x + 0 == x" by simp
    3.96 +
    3.97 +lemma norm_imp_pos_and_ge:
    3.98 +  fixes x :: "'a::real_normed_vector"
    3.99 +  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
   3.100 +  by atomize auto
   3.101 +
   3.102 +lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
   3.103 +
   3.104 +lemma norm_pths:
   3.105 +  fixes x :: "'a::real_normed_vector" shows
   3.106 +  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
   3.107 +  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   3.108 +  using norm_ge_zero[of "x - y"] by auto
   3.109 +
   3.110 +use "normarith.ML"
   3.111 +
   3.112 +method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   3.113 +*} "prove simple linear statements about vector norms"
   3.114 +
   3.115 +text{* Hence more metric properties. *}
   3.116 +
   3.117 +lemma dist_triangle_add:
   3.118 +  fixes x y x' y' :: "'a::real_normed_vector"
   3.119 +  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
   3.120 +  by norm
   3.121 +
   3.122 +lemma dist_triangle_add_half:
   3.123 +  fixes x x' y y' :: "'a::real_normed_vector"
   3.124 +  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
   3.125 +  by norm
   3.126 +
   3.127 +end
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 12:39:42 2011 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 15:06:13 2011 -0700
     4.3 @@ -7,7 +7,7 @@
     4.4  header {* Elementary topology in Euclidean space. *}
     4.5  
     4.6  theory Topology_Euclidean_Space
     4.7 -imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
     4.8 +imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
     4.9  begin
    4.10  
    4.11  (* to be moved elsewhere *)
    4.12 @@ -5763,15 +5763,13 @@
    4.13    { fix y assume "m > 0"  "m *\<^sub>R a + c \<le> y"  "y \<le> m *\<^sub>R b + c"
    4.14      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
    4.15        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
    4.16 -      apply(auto simp add: pth_3[symmetric] 
    4.17 -        intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"]) 
    4.18 +      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
    4.19        by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
    4.20    } moreover
    4.21    { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
    4.22      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
    4.23        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
    4.24 -      apply(auto simp add: pth_3[symmetric]
    4.25 -        intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
    4.26 +      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
    4.27        by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
    4.28    }
    4.29    ultimately show ?thesis using False by auto