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)"
    1.87  	  by (simp add: right_diff_distrib)
    1.88  	also from gz x0 y'
    1.89  	have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"