1.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Linear_Algebra
     1.5  begin
     1.6  
     1.7 -definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
     1.8 +definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"
     1.9  
    1.10  lemma norm_bound_generalize:
    1.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    1.12 @@ -67,25 +67,22 @@
    1.13    shows "norm (f x) \<le> onorm f * norm x"
    1.14      and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
    1.15  proof -
    1.16 -  let ?S = "{norm (f x) |x. norm x = 1}"
    1.17 +  let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}"
    1.18    have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
    1.19      by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
    1.20    then have Se: "?S \<noteq> {}"
    1.21      by auto
    1.22 -  from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
    1.23 -    unfolding norm_bound_generalize[OF lf, symmetric]
    1.24 -    by (auto simp add: setle_def)
    1.25 -  from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
    1.26 -  show "norm (f x) \<le> onorm f * norm x"
    1.27 +  from linear_bounded[OF lf] have b: "bdd_above ?S"
    1.28 +    unfolding norm_bound_generalize[OF lf, symmetric] by auto
    1.29 +  then show "norm (f x) \<le> onorm f * norm x"
    1.30      apply -
    1.31      apply (rule spec[where x = x])
    1.32      unfolding norm_bound_generalize[OF lf, symmetric]
    1.33 -    apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
    1.34 +    apply (auto simp: onorm_def intro!: cSUP_upper)
    1.35      done
    1.36    show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
    1.37 -    using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
    1.38      unfolding norm_bound_generalize[OF lf, symmetric]
    1.39 -    by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
    1.40 +    using Se by (auto simp: onorm_def intro!: cSUP_least b)
    1.41  qed
    1.42  
    1.43  lemma onorm_pos_le:
    1.44 @@ -107,18 +104,8 @@
    1.45    apply arith
    1.46    done
    1.47  
    1.48 -lemma onorm_const:
    1.49 -  "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
    1.50 -proof -
    1.51 -  let ?f = "\<lambda>x::'a. y::'b"
    1.52 -  have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
    1.53 -    by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
    1.54 -  show ?thesis
    1.55 -    unfolding onorm_def th
    1.56 -    apply (rule cSup_unique)
    1.57 -    apply (simp_all  add: setle_def)
    1.58 -    done
    1.59 -qed
    1.60 +lemma onorm_const: "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
    1.61 +  using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis)
    1.62  
    1.63  lemma onorm_pos_lt:
    1.64    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"