# HG changeset patch
# User huffman
# Date 1314997032 25200
# Node ID 8670a39d44207493b9705e3fca895afd3ba7ee2b
# Parent  f64c715660c3ba4f1b3dfaedbb0df2ab533797cb
remove more duplicate lemmas

diff -r f64c715660c3 -r 8670a39d4420 NEWS
--- a/NEWS	Fri Sep 02 19:29:48 2011 +0200
+++ b/NEWS	Fri Sep 02 13:57:12 2011 -0700
@@ -248,6 +248,11 @@
   subset_interior ~> interior_mono
   subset_closure ~> closure_mono
   closure_univ ~> closure_UNIV
+  real_arch_lt ~> reals_Archimedean2
+  real_arch ~> reals_Archimedean3
+  real_abs_norm ~> abs_norm_cancel
+  real_abs_sub_norm ~> norm_triangle_ineq3
+  norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2
 
 * Complex_Main: The locale interpretations for the bounded_linear and
 bounded_bilinear locales have been removed, in order to reduce the
diff -r f64c715660c3 -r 8670a39d4420 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Sep 02 19:29:48 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Sep 02 13:57:12 2011 -0700
@@ -55,44 +55,35 @@
 
 text{* Hence derive more interesting properties of the norm. *}
 
-(* FIXME: same as norm_scaleR
-lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x"
-  by (simp add: norm_vector_def setL2_right_distrib abs_mult)
-*)
-
 lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
-  by (simp add: power2_eq_square)
+  by simp (* TODO: delete *)
 
 lemma norm_cauchy_schwarz:
+  (* TODO: move to Inner_Product.thy *)
   shows "inner x y <= norm x * norm y"
   using Cauchy_Schwarz_ineq2[of x y] by auto
 
-lemma norm_cauchy_schwarz_abs:
-  shows "\<bar>inner x y\<bar> \<le> norm x * norm y"
-  by (rule Cauchy_Schwarz_ineq2)
-
 lemma norm_triangle_sub:
   fixes x y :: "'a::real_normed_vector"
   shows "norm x \<le> norm y  + norm (x - y)"
   using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
 
-lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"
-  by (rule abs_norm_cancel)
-lemma real_abs_sub_norm: "\<bar>norm x - norm y\<bar> <= norm(x - y)"
-  by (rule norm_triangle_ineq3)
 lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
   by (simp add: norm_eq_sqrt_inner) 
+
 lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
   by (simp add: norm_eq_sqrt_inner)
+
 lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
   apply(subst order_eq_iff) unfolding norm_le by auto
+
 lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1"
-  unfolding norm_eq_sqrt_inner by auto
+  by (simp add: norm_eq_sqrt_inner)
 
 text{* Squaring equations and inequalities involving norms.  *}
 
 lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
-  by (simp add: norm_eq_sqrt_inner)
+  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
 
 lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
   by (auto simp add: norm_eq_sqrt_inner)
@@ -159,10 +150,10 @@
   unfolding dist_norm[THEN sym] .
 
 lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
-  by (metis order_trans norm_triangle_ineq)
+  by (rule norm_triangle_ineq [THEN order_trans])
 
 lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
-  by (metis basic_trans_rules(21) norm_triangle_ineq)
+  by (rule norm_triangle_ineq [THEN le_less_trans])
 
 lemma setsum_clauses:
   shows "setsum f {} = 0"
@@ -225,8 +216,8 @@
   "orthogonal x a \<Longrightarrow> orthogonal (-x) a"
   "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
   "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
-  unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
- 
+  unfolding orthogonal_def inner_add inner_diff by auto
+
 end
 
 lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
@@ -497,13 +488,10 @@
 lemma hull_redundant: "a \<in> (S hull s) ==> (S hull (insert a s) = S hull s)"
 by (metis hull_redundant_eq)
 
-text{* Archimedian properties and useful consequences. *}
+subsection {* Archimedean properties and useful consequences *}
 
 lemma real_arch_simple: "\<exists>n. x <= real (n::nat)"
-  using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto)
-lemmas real_arch_lt = reals_Archimedean2
-
-lemmas real_arch = reals_Archimedean3
+  unfolding real_of_nat_def by (rule ex_le_of_nat)
 
 lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
   using reals_Archimedean
@@ -530,7 +518,7 @@
 lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n"
 proof-
   from x have x0: "x - 1 > 0" by arith
-  from real_arch[OF x0, rule_format, of y]
+  from reals_Archimedean3[OF x0, rule_format, of y]
   obtain n::nat where n:"y < real n * (x - 1)" by metis
   from x0 have x00: "x- 1 \<ge> 0" by arith
   from real_pow_lbound[OF x00, of n] n
@@ -570,7 +558,8 @@
   shows "x = 0"
 proof-
   {assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith
-    from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x"  by blast
+    from reals_Archimedean3[OF xp, rule_format, of c]
+    obtain n::nat where n: "c < real n * x" by blast
     with xc[rule_format, of n] have "n = 0" by arith
     with n c have False by simp}
   then show ?thesis by blast
diff -r f64c715660c3 -r 8670a39d4420 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Fri Sep 02 19:29:48 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Sep 02 13:57:12 2011 -0700
@@ -509,7 +509,7 @@
     also have *: "{x::'a. a < x$$i} = (\<Union>k::nat. {(\<chi>\<chi> n. if n = i then a else -real k) <..})" using `i <DIM('a)`
     proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
       fix x
-      from real_arch_lt[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
+      from reals_Archimedean2[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
       guess k::nat .. note k = this
       { fix i assume "i < DIM('a)"
         then have "-x$$i < real k"
@@ -544,7 +544,7 @@
     also have *: "{x::'a. x$$i < a} = (\<Union>k::nat. {..< (\<chi>\<chi> n. if n = i then a else real k)})" using `i <DIM('a)`
     proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
       fix x
-      from real_arch_lt[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
+      from reals_Archimedean2[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
       guess k::nat .. note k = this
       { fix i assume "i < DIM('a)"
         then have "x$$i < real k"
@@ -1221,7 +1221,7 @@
     { fix x :: ereal assume *: "\<forall>i::nat. real i < x"
       have "x = \<infinity>"
       proof (rule ereal_top)
-        fix B from real_arch_lt[of B] guess n ..
+        fix B from reals_Archimedean2[of B] guess n ..
         then have "ereal B < real n" by auto
         with * show "B \<le> x" by (metis less_trans less_imp_le)
       qed }
diff -r f64c715660c3 -r 8670a39d4420 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Sep 02 19:29:48 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Sep 02 13:57:12 2011 -0700
@@ -392,10 +392,10 @@
       proof (cases y)
         case (real r)
         with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)
-        from real_arch_lt[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
+        from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
         then have "\<exists>p. max 0 (u x) = ereal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)
         then guess p .. note ux = this
-        obtain m :: nat where m: "p < real m" using real_arch_lt ..
+        obtain m :: nat where m: "p < real m" using reals_Archimedean2 ..
         have "p \<le> r"
         proof (rule ccontr)
           assume "\<not> p \<le> r"
diff -r f64c715660c3 -r 8670a39d4420 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Sep 02 19:29:48 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Sep 02 13:57:12 2011 -0700
@@ -41,7 +41,7 @@
 qed
 
 lemma mem_big_cube: obtains n where "x \<in> cube n"
-proof- from real_arch_lt[of "norm x"] guess n ..
+proof- from reals_Archimedean2[of "norm x"] guess n ..
   thus ?thesis apply-apply(rule that[where n=n])
     apply(rule ball_subset_cube[unfolded subset_eq,rule_format])
     by (auto simp add:dist_norm)
@@ -805,7 +805,7 @@
   have "sets ?G = sets (\<Pi>\<^isub>M i\<in>I.
        sigma \<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>)"
     by (subst sigma_product_algebra_sigma_eq[of I "\<lambda>_ i. {..<real i}" ])
-       (auto intro!: measurable_sigma_sigma incseq_SucI real_arch_lt
+       (auto intro!: measurable_sigma_sigma incseq_SucI reals_Archimedean2
              simp: product_algebra_def)
   then show ?thesis
     unfolding lborel_def borel_eq_lessThan lebesgue_def sigma_def by simp