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)
```