src/HOL/Real_Vector_Spaces.thy
changeset 66793 deabce3ccf1f
parent 66422 2891f33ed4c8
child 67135 1a94352812f4
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -1469,17 +1469,14 @@
     1.4  begin
     1.5  
     1.6  lemma pos_bounded: "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
     1.7 -  apply (insert bounded)
     1.8 -  apply (erule exE)
     1.9 -  apply (rule_tac x="max 1 K" in exI)
    1.10 -  apply safe
    1.11 -   apply (rule order_less_le_trans [OF zero_less_one max.cobounded1])
    1.12 -  apply (drule spec)
    1.13 -  apply (drule spec)
    1.14 -  apply (erule order_trans)
    1.15 -  apply (rule mult_left_mono [OF max.cobounded2])
    1.16 -  apply (intro mult_nonneg_nonneg norm_ge_zero)
    1.17 -  done
    1.18 +proof -
    1.19 +  obtain K where "\<And>a b. norm (a ** b) \<le> norm a * norm b * K"
    1.20 +    using bounded by blast
    1.21 +  then have "norm (a ** b) \<le> norm a * norm b * (max 1 K)" for a b
    1.22 +    by (rule order.trans) (simp add: mult_left_mono)
    1.23 +  then show ?thesis
    1.24 +    by force
    1.25 +qed
    1.26  
    1.27  lemma nonneg_bounded: "\<exists>K\<ge>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
    1.28    using pos_bounded by (auto intro: order_less_imp_le)