src/HOL/Hahn_Banach/Normed_Space.thy
 changeset 44887 7ca82df6e951 parent 31795 be3e1cc5005c child 46867 0883804b67bb
```     1.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Sep 11 21:35:35 2011 +0200
1.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Sep 11 22:55:26 2011 +0200
1.3 @@ -50,8 +50,7 @@
1.4    interpret vectorspace V by fact
1.5    assume x: "x \<in> V"
1.6    then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
1.7 -  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
1.8 -    by (rule abs_homogenous)
1.9 +  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
1.10    also have "\<dots> = \<parallel>x\<parallel>" by simp
1.11    finally show ?thesis .
1.12  qed
1.13 @@ -80,13 +79,13 @@
1.14  declare normed_vectorspace.intro [intro?]
1.15
1.16  lemma (in normed_vectorspace) gt_zero [intro?]:
1.17 -  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
1.18 +  assumes x: "x \<in> V" and neq: "x \<noteq> 0"
1.19 +  shows "0 < \<parallel>x\<parallel>"
1.20  proof -
1.21 -  assume x: "x \<in> V" and neq: "x \<noteq> 0"
1.22    from x have "0 \<le> \<parallel>x\<parallel>" ..
1.23 -  also have [symmetric]: "\<dots> \<noteq> 0"
1.24 +  also have "0 \<noteq> \<parallel>x\<parallel>"
1.25    proof
1.26 -    assume "\<parallel>x\<parallel> = 0"
1.27 +    assume "0 = \<parallel>x\<parallel>"
1.28      with x have "x = 0" by simp
1.29      with neq show False by contradiction
1.30    qed
```