remove more duplicate lemmas
authorhuffman
Fri Sep 02 13:57:12 2011 -0700 (2011-09-02 ago)
changeset 446668670a39d4420
parent 44664 f64c715660c3
child 44667 ee5772ca7d16
remove more duplicate lemmas
NEWS
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
     1.1 --- a/NEWS	Fri Sep 02 19:29:48 2011 +0200
     1.2 +++ b/NEWS	Fri Sep 02 13:57:12 2011 -0700
     1.3 @@ -248,6 +248,11 @@
     1.4    subset_interior ~> interior_mono
     1.5    subset_closure ~> closure_mono
     1.6    closure_univ ~> closure_UNIV
     1.7 +  real_arch_lt ~> reals_Archimedean2
     1.8 +  real_arch ~> reals_Archimedean3
     1.9 +  real_abs_norm ~> abs_norm_cancel
    1.10 +  real_abs_sub_norm ~> norm_triangle_ineq3
    1.11 +  norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2
    1.12  
    1.13  * Complex_Main: The locale interpretations for the bounded_linear and
    1.14  bounded_bilinear locales have been removed, in order to reduce the
     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Sep 02 19:29:48 2011 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Sep 02 13:57:12 2011 -0700
     2.3 @@ -55,44 +55,35 @@
     2.4  
     2.5  text{* Hence derive more interesting properties of the norm. *}
     2.6  
     2.7 -(* FIXME: same as norm_scaleR
     2.8 -lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x"
     2.9 -  by (simp add: norm_vector_def setL2_right_distrib abs_mult)
    2.10 -*)
    2.11 -
    2.12  lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
    2.13 -  by (simp add: power2_eq_square)
    2.14 +  by simp (* TODO: delete *)
    2.15  
    2.16  lemma norm_cauchy_schwarz:
    2.17 +  (* TODO: move to Inner_Product.thy *)
    2.18    shows "inner x y <= norm x * norm y"
    2.19    using Cauchy_Schwarz_ineq2[of x y] by auto
    2.20  
    2.21 -lemma norm_cauchy_schwarz_abs:
    2.22 -  shows "\<bar>inner x y\<bar> \<le> norm x * norm y"
    2.23 -  by (rule Cauchy_Schwarz_ineq2)
    2.24 -
    2.25  lemma norm_triangle_sub:
    2.26    fixes x y :: "'a::real_normed_vector"
    2.27    shows "norm x \<le> norm y  + norm (x - y)"
    2.28    using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
    2.29  
    2.30 -lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"
    2.31 -  by (rule abs_norm_cancel)
    2.32 -lemma real_abs_sub_norm: "\<bar>norm x - norm y\<bar> <= norm(x - y)"
    2.33 -  by (rule norm_triangle_ineq3)
    2.34  lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
    2.35    by (simp add: norm_eq_sqrt_inner) 
    2.36 +
    2.37  lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
    2.38    by (simp add: norm_eq_sqrt_inner)
    2.39 +
    2.40  lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
    2.41    apply(subst order_eq_iff) unfolding norm_le by auto
    2.42 +
    2.43  lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1"
    2.44 -  unfolding norm_eq_sqrt_inner by auto
    2.45 +  by (simp add: norm_eq_sqrt_inner)
    2.46  
    2.47  text{* Squaring equations and inequalities involving norms.  *}
    2.48  
    2.49  lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
    2.50 -  by (simp add: norm_eq_sqrt_inner)
    2.51 +  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
    2.52  
    2.53  lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
    2.54    by (auto simp add: norm_eq_sqrt_inner)
    2.55 @@ -159,10 +150,10 @@
    2.56    unfolding dist_norm[THEN sym] .
    2.57  
    2.58  lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
    2.59 -  by (metis order_trans norm_triangle_ineq)
    2.60 +  by (rule norm_triangle_ineq [THEN order_trans])
    2.61  
    2.62  lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
    2.63 -  by (metis basic_trans_rules(21) norm_triangle_ineq)
    2.64 +  by (rule norm_triangle_ineq [THEN le_less_trans])
    2.65  
    2.66  lemma setsum_clauses:
    2.67    shows "setsum f {} = 0"
    2.68 @@ -225,8 +216,8 @@
    2.69    "orthogonal x a \<Longrightarrow> orthogonal (-x) a"
    2.70    "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
    2.71    "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
    2.72 -  unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
    2.73 - 
    2.74 +  unfolding orthogonal_def inner_add inner_diff by auto
    2.75 +
    2.76  end
    2.77  
    2.78  lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
    2.79 @@ -497,13 +488,10 @@
    2.80  lemma hull_redundant: "a \<in> (S hull s) ==> (S hull (insert a s) = S hull s)"
    2.81  by (metis hull_redundant_eq)
    2.82  
    2.83 -text{* Archimedian properties and useful consequences. *}
    2.84 +subsection {* Archimedean properties and useful consequences *}
    2.85  
    2.86  lemma real_arch_simple: "\<exists>n. x <= real (n::nat)"
    2.87 -  using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto)
    2.88 -lemmas real_arch_lt = reals_Archimedean2
    2.89 -
    2.90 -lemmas real_arch = reals_Archimedean3
    2.91 +  unfolding real_of_nat_def by (rule ex_le_of_nat)
    2.92  
    2.93  lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
    2.94    using reals_Archimedean
    2.95 @@ -530,7 +518,7 @@
    2.96  lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n"
    2.97  proof-
    2.98    from x have x0: "x - 1 > 0" by arith
    2.99 -  from real_arch[OF x0, rule_format, of y]
   2.100 +  from reals_Archimedean3[OF x0, rule_format, of y]
   2.101    obtain n::nat where n:"y < real n * (x - 1)" by metis
   2.102    from x0 have x00: "x- 1 \<ge> 0" by arith
   2.103    from real_pow_lbound[OF x00, of n] n
   2.104 @@ -570,7 +558,8 @@
   2.105    shows "x = 0"
   2.106  proof-
   2.107    {assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith
   2.108 -    from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x"  by blast
   2.109 +    from reals_Archimedean3[OF xp, rule_format, of c]
   2.110 +    obtain n::nat where n: "c < real n * x" by blast
   2.111      with xc[rule_format, of n] have "n = 0" by arith
   2.112      with n c have False by simp}
   2.113    then show ?thesis by blast
     3.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Sep 02 19:29:48 2011 +0200
     3.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Sep 02 13:57:12 2011 -0700
     3.3 @@ -509,7 +509,7 @@
     3.4      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)`
     3.5      proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
     3.6        fix x
     3.7 -      from real_arch_lt[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
     3.8 +      from reals_Archimedean2[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
     3.9        guess k::nat .. note k = this
    3.10        { fix i assume "i < DIM('a)"
    3.11          then have "-x$$i < real k"
    3.12 @@ -544,7 +544,7 @@
    3.13      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)`
    3.14      proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
    3.15        fix x
    3.16 -      from real_arch_lt[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
    3.17 +      from reals_Archimedean2[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
    3.18        guess k::nat .. note k = this
    3.19        { fix i assume "i < DIM('a)"
    3.20          then have "x$$i < real k"
    3.21 @@ -1221,7 +1221,7 @@
    3.22      { fix x :: ereal assume *: "\<forall>i::nat. real i < x"
    3.23        have "x = \<infinity>"
    3.24        proof (rule ereal_top)
    3.25 -        fix B from real_arch_lt[of B] guess n ..
    3.26 +        fix B from reals_Archimedean2[of B] guess n ..
    3.27          then have "ereal B < real n" by auto
    3.28          with * show "B \<le> x" by (metis less_trans less_imp_le)
    3.29        qed }
     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Sep 02 19:29:48 2011 +0200
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Sep 02 13:57:12 2011 -0700
     4.3 @@ -392,10 +392,10 @@
     4.4        proof (cases y)
     4.5          case (real r)
     4.6          with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)
     4.7 -        from real_arch_lt[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
     4.8 +        from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
     4.9          then have "\<exists>p. max 0 (u x) = ereal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)
    4.10          then guess p .. note ux = this
    4.11 -        obtain m :: nat where m: "p < real m" using real_arch_lt ..
    4.12 +        obtain m :: nat where m: "p < real m" using reals_Archimedean2 ..
    4.13          have "p \<le> r"
    4.14          proof (rule ccontr)
    4.15            assume "\<not> p \<le> r"
     5.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Sep 02 19:29:48 2011 +0200
     5.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Sep 02 13:57:12 2011 -0700
     5.3 @@ -41,7 +41,7 @@
     5.4  qed
     5.5  
     5.6  lemma mem_big_cube: obtains n where "x \<in> cube n"
     5.7 -proof- from real_arch_lt[of "norm x"] guess n ..
     5.8 +proof- from reals_Archimedean2[of "norm x"] guess n ..
     5.9    thus ?thesis apply-apply(rule that[where n=n])
    5.10      apply(rule ball_subset_cube[unfolded subset_eq,rule_format])
    5.11      by (auto simp add:dist_norm)
    5.12 @@ -805,7 +805,7 @@
    5.13    have "sets ?G = sets (\<Pi>\<^isub>M i\<in>I.
    5.14         sigma \<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>)"
    5.15      by (subst sigma_product_algebra_sigma_eq[of I "\<lambda>_ i. {..<real i}" ])
    5.16 -       (auto intro!: measurable_sigma_sigma incseq_SucI real_arch_lt
    5.17 +       (auto intro!: measurable_sigma_sigma incseq_SucI reals_Archimedean2
    5.18               simp: product_algebra_def)
    5.19    then show ?thesis
    5.20      unfolding lborel_def borel_eq_lessThan lebesgue_def sigma_def by simp