--- a/src/HOL/IsaMakefile Wed Aug 24 12:39:42 2011 -0700
+++ b/src/HOL/IsaMakefile Wed Aug 24 15:06:13 2011 -0700
@@ -1175,6 +1175,7 @@
Multivariate_Analysis/L2_Norm.thy \
Multivariate_Analysis/Linear_Algebra.thy \
Multivariate_Analysis/Multivariate_Analysis.thy \
+ Multivariate_Analysis/Norm_Arith.thy \
Multivariate_Analysis/Operator_Norm.thy \
Multivariate_Analysis/Path_Connected.thy \
Multivariate_Analysis/ROOT.ML \
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 24 12:39:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 24 15:06:13 2011 -0700
@@ -10,9 +10,6 @@
"~~/src/HOL/Library/Infinite_Set"
L2_Norm
"~~/src/HOL/Library/Convex"
- "~~/src/HOL/Library/Sum_of_Squares"
-uses
- ("normarith.ML")
begin
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -154,111 +151,6 @@
then show "x = y" by (simp)
qed
-subsection{* General linear decision procedure for normed spaces. *}
-
-lemma norm_cmul_rule_thm:
- fixes x :: "'a::real_normed_vector"
- shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
- unfolding norm_scaleR
- apply (erule mult_left_mono)
- apply simp
- done
-
- (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
-lemma norm_add_rule_thm:
- fixes x1 x2 :: "'a::real_normed_vector"
- shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
- by (rule order_trans [OF norm_triangle_ineq add_mono])
-
-lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
- by (simp add: field_simps)
-
-lemma pth_1:
- fixes x :: "'a::real_normed_vector"
- shows "x == scaleR 1 x" by simp
-
-lemma pth_2:
- fixes x :: "'a::real_normed_vector"
- shows "x - y == x + -y" by (atomize (full)) simp
-
-lemma pth_3:
- fixes x :: "'a::real_normed_vector"
- shows "- x == scaleR (-1) x" by simp
-
-lemma pth_4:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
-
-lemma pth_5:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
-
-lemma pth_6:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c (x + y) == scaleR c x + scaleR c y"
- by (simp add: scaleR_right_distrib)
-
-lemma pth_7:
- fixes x :: "'a::real_normed_vector"
- shows "0 + x == x" and "x + 0 == x" by simp_all
-
-lemma pth_8:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c x + scaleR d x == scaleR (c + d) x"
- by (simp add: scaleR_left_distrib)
-
-lemma pth_9:
- fixes x :: "'a::real_normed_vector" shows
- "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
- "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
- "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
- by (simp_all add: algebra_simps)
-
-lemma pth_a:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x + y == y" by simp
-
-lemma pth_b:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
- "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
- "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
- by (simp_all add: algebra_simps)
-
-lemma pth_c:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
- "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
- "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
- by (simp_all add: algebra_simps)
-
-lemma pth_d:
- fixes x :: "'a::real_normed_vector"
- shows "x + 0 == x" by simp
-
-lemma norm_imp_pos_and_ge:
- fixes x :: "'a::real_normed_vector"
- shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
- by atomize auto
-
-lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
-
-lemma norm_pths:
- fixes x :: "'a::real_normed_vector" shows
- "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
- "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
- using norm_ge_zero[of "x - y"] by auto
-
-use "normarith.ML"
-
-method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
-*} "prove simple linear statements about vector norms"
-
-
-text{* Hence more metric properties. *}
-
lemma norm_triangle_half_r:
shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
@@ -274,16 +166,6 @@
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
by (metis basic_trans_rules(21) norm_triangle_ineq)
-lemma dist_triangle_add:
- fixes x y x' y' :: "'a::real_normed_vector"
- shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
- by norm
-
-lemma dist_triangle_add_half:
- fixes x x' y y' :: "'a::real_normed_vector"
- shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
- by norm
-
lemma setsum_clauses:
shows "setsum f {} = 0"
and "finite S \<Longrightarrow> setsum f (insert x S) =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy Wed Aug 24 15:06:13 2011 -0700
@@ -0,0 +1,124 @@
+(* Title: HOL/Multivariate_Analysis/Norm_Arith.thy
+ Author: Amine Chaieb, University of Cambridge
+*)
+
+header {* General linear decision procedure for normed spaces *}
+
+theory Norm_Arith
+imports "~~/src/HOL/Library/Sum_of_Squares"
+uses ("normarith.ML")
+begin
+
+lemma norm_cmul_rule_thm:
+ fixes x :: "'a::real_normed_vector"
+ shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+ unfolding norm_scaleR
+ apply (erule mult_left_mono)
+ apply simp
+ done
+
+ (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
+lemma norm_add_rule_thm:
+ fixes x1 x2 :: "'a::real_normed_vector"
+ shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
+ by (rule order_trans [OF norm_triangle_ineq add_mono])
+
+lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
+ by (simp add: field_simps)
+
+lemma pth_1:
+ fixes x :: "'a::real_normed_vector"
+ shows "x == scaleR 1 x" by simp
+
+lemma pth_2:
+ fixes x :: "'a::real_normed_vector"
+ shows "x - y == x + -y" by (atomize (full)) simp
+
+lemma pth_3:
+ fixes x :: "'a::real_normed_vector"
+ shows "- x == scaleR (-1) x" by simp
+
+lemma pth_4:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+
+lemma pth_5:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+
+lemma pth_6:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+ by (simp add: scaleR_right_distrib)
+
+lemma pth_7:
+ fixes x :: "'a::real_normed_vector"
+ shows "0 + x == x" and "x + 0 == x" by simp_all
+
+lemma pth_8:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+ by (simp add: scaleR_left_distrib)
+
+lemma pth_9:
+ fixes x :: "'a::real_normed_vector" shows
+ "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
+ "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
+ "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_a:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR 0 x + y == y" by simp
+
+lemma pth_b:
+ fixes x :: "'a::real_normed_vector" shows
+ "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
+ "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
+ "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
+ "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+ by (simp_all add: algebra_simps)
+
+lemma pth_c:
+ fixes x :: "'a::real_normed_vector" shows
+ "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
+ "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
+ "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
+ "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_d:
+ fixes x :: "'a::real_normed_vector"
+ shows "x + 0 == x" by simp
+
+lemma norm_imp_pos_and_ge:
+ fixes x :: "'a::real_normed_vector"
+ shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+ by atomize auto
+
+lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
+
+lemma norm_pths:
+ fixes x :: "'a::real_normed_vector" shows
+ "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
+ "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
+ using norm_ge_zero[of "x - y"] by auto
+
+use "normarith.ML"
+
+method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+*} "prove simple linear statements about vector norms"
+
+text{* Hence more metric properties. *}
+
+lemma dist_triangle_add:
+ fixes x y x' y' :: "'a::real_normed_vector"
+ shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+ by norm
+
+lemma dist_triangle_add_half:
+ fixes x x' y y' :: "'a::real_normed_vector"
+ shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
+ by norm
+
+end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 24 12:39:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 24 15:06:13 2011 -0700
@@ -7,7 +7,7 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
begin
(* to be moved elsewhere *)
@@ -5763,15 +5763,13 @@
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
}
ultimately show ?thesis using False by auto