src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
 changeset 27612 d3eb431db035 parent 27611 2c01c0bdb385 child 29234 60f7fb56f8cd
     1.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 16:50:09 2008 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 19:39:37 2008 +0200
1.3 @@ -5,7 +5,9 @@
1.4
1.5  header {* Extending non-maximal functions *}
1.6
1.7 -theory HahnBanachExtLemmas imports FunctionNorm begin
1.8 +theory HahnBanachExtLemmas
1.9 +imports FunctionNorm
1.10 +begin
1.11
1.12  text {*
1.13    In this section the following context is presumed.  Let @{text E} be
1.14 @@ -98,7 +100,8 @@
1.15  proof -
1.16    interpret linearform [H h] by fact
1.17    interpret vectorspace [E] by fact
1.18 -  show ?thesis proof
1.19 +  show ?thesis
1.20 +  proof
1.21      note E = vectorspace E
1.22      have H': "vectorspace H'"
1.23      proof (unfold H'_def)
1.24 @@ -116,7 +119,7 @@
1.25            x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
1.26            and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
1.27            and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
1.28 -          by (unfold H'_def sum_def lin_def) blast
1.29 +          unfolding H'_def sum_def lin_def by blast
1.30
1.31  	have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
1.32  	proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
1.33 @@ -154,9 +157,9 @@
1.34  	from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
1.35            by (rule vectorspace.mult_closed)
1.36  	with x1 obtain y a y1 a1 where
1.37 -          cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
1.38 +            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
1.39            and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
1.40 -          by (unfold H'_def sum_def lin_def) blast
1.41 +          unfolding H'_def sum_def lin_def by blast
1.42
1.43  	have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
1.44  	proof (rule decomp_H')
1.45 @@ -204,15 +207,16 @@
1.46    interpret subspace [H E] by fact
1.47    interpret seminorm [E p] by fact
1.48    interpret linearform [H h] by fact
1.49 -  show ?thesis proof
1.50 +  show ?thesis
1.51 +  proof
1.52      fix x assume x': "x \<in> H'"
1.53      show "h' x \<le> p x"
1.54      proof -
1.55        from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
1.56  	and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
1.57        from x' obtain y a where
1.58 -        x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
1.59 -	by (unfold H'_def sum_def lin_def) blast
1.60 +          x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
1.61 +	unfolding H'_def sum_def lin_def by blast
1.62        from y have y': "y \<in> E" ..
1.63        from y have ay: "inverse a \<cdot> y \<in> H" by simp
1.64
1.65 @@ -228,7 +232,7 @@
1.66        next
1.67  	txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
1.68            with @{text ya} taken as @{text "y / a"}: *}
1.69 -	assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
1.70 +	assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
1.71  	from a1 ay
1.72  	have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
1.73  	with lz have "a * xi \<le>
1.74 @@ -250,13 +254,13 @@
1.75        next
1.76  	txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
1.77            with @{text ya} taken as @{text "y / a"}: *}
1.78 -	assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
1.79 +	assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
1.80  	from a2 ay
1.81  	have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
1.82  	with gz have "a * xi \<le>
1.83            a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
1.84            by simp
1.85 -	also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
1.86 +	also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"