author huffman Wed Aug 24 15:06:13 2011 -0700 (2011-08-24) changeset 44516 d9a496ae5d9d parent 44515 fcaacc214a36 child 44517 68e8eb0ce8aa
move everything related to 'norm' method into new theory file Norm_Arith.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.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.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.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.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.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.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
```