src/HOL/Real/HahnBanach/HahnBanach.thy
 changeset 27612 d3eb431db035 parent 27611 2c01c0bdb385 child 28823 dcbef866c9e2
```     1.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 15 16:50:09 2008 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 15 19:39:37 2008 +0200
1.3 @@ -5,7 +5,9 @@
1.4
1.5  header {* The Hahn-Banach Theorem *}
1.6
1.7 -theory HahnBanach imports HahnBanachLemmas begin
1.8 +theory HahnBanach
1.9 +imports HahnBanachLemmas
1.10 +begin
1.11
1.12  text {*
1.13    We present the proof of two different versions of the Hahn-Banach
1.14 @@ -66,7 +68,7 @@
1.15    interpret seminorm [E p] by fact
1.16    interpret linearform [F f] by fact
1.17    def M \<equiv> "norm_pres_extensions E p F f"
1.18 -  hence M: "M = \<dots>" by (simp only:)
1.19 +  then have M: "M = \<dots>" by (simp only:)
1.20    from E have F: "vectorspace F" ..
1.21    note FE = `F \<unlhd> E`
1.22    {
1.23 @@ -74,7 +76,8 @@
1.24      have "\<Union>c \<in> M"
1.25        -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *}
1.26        -- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *}
1.27 -    proof (unfold M_def, rule norm_pres_extensionI)
1.28 +      unfolding M_def
1.29 +    proof (rule norm_pres_extensionI)
1.30        let ?H = "domain (\<Union>c)"
1.31        let ?h = "funct (\<Union>c)"
1.32
1.33 @@ -101,12 +104,13 @@
1.34            \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
1.35      qed
1.36    }
1.37 -  hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
1.38 +  then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
1.39    -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *}
1.40    proof (rule Zorn's_Lemma)
1.41        -- {* We show that @{text M} is non-empty: *}
1.42      show "graph F f \<in> M"
1.43 -    proof (unfold M_def, rule norm_pres_extensionI2)
1.44 +      unfolding M_def
1.45 +    proof (rule norm_pres_extensionI2)
1.46        show "linearform F f" by fact
1.47        show "F \<unlhd> E" by fact
1.48        from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl)
1.49 @@ -116,12 +120,12 @@
1.50    qed
1.51    then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
1.52      by blast
1.53 -  from gM [unfolded M_def] obtain H h where
1.54 +  from gM obtain H h where
1.55        g_rep: "g = graph H h"
1.56      and linearform: "linearform H h"
1.57      and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
1.58      and graphs: "graph F f \<subseteq> graph H h"
1.59 -    and hp: "\<forall>x \<in> H. h x \<le> p x" ..
1.60 +    and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
1.61        -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *}
1.62        -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
1.63        -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
1.64 @@ -213,14 +217,15 @@
1.65            proof
1.66              assume eq: "graph H h = graph H' h'"
1.67              have "x' \<in> H'"
1.68 -            proof (unfold H'_def, rule)
1.69 +	      unfolding H'_def
1.70 +            proof
1.71                from H show "0 \<in> H" by (rule vectorspace.zero)
1.72                from x'E show "x' \<in> lin x'" by (rule x_lin_x)
1.73                from x'E show "x' = 0 + x'" by simp
1.74              qed
1.75 -            hence "(x', h' x') \<in> graph H' h'" ..
1.76 +            then have "(x', h' x') \<in> graph H' h'" ..
1.77              with eq have "(x', h' x') \<in> graph H h" by (simp only:)
1.78 -            hence "x' \<in> H" ..
1.79 +            then have "x' \<in> H" ..
1.80              with `x' \<notin> H` show False by contradiction
1.81            qed
1.82            with g_rep show ?thesis by simp
1.83 @@ -252,7 +257,7 @@
1.85              also have "(x, 0) =
1.86                  (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
1.87 -	    using E HE
1.88 +	      using E HE
1.89              proof (rule decomp_H'_H [symmetric])
1.90                from FH x show "x \<in> H" ..
1.91                from x' show "x' \<noteq> 0" .
1.92 @@ -274,7 +279,7 @@
1.93        qed
1.94        ultimately show ?thesis ..
1.95      qed
1.96 -    hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
1.97 +    then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
1.98        -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *}
1.99      with gx show "H = E" by contradiction
1.100    qed
1.101 @@ -321,12 +326,8 @@
1.102    interpret subspace [F E] by fact
1.103    interpret linearform [F f] by fact
1.104    interpret seminorm [E p] by fact
1.105 -(*  note E = `vectorspace E`
1.106 -  note FE = `subspace F E`
1.107 -  note sn = `seminorm E p`
1.108 -  note lf = `linearform F f`
1.109 -*)  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
1.110 -  using E FE sn lf
1.111 +  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
1.112 +    using E FE sn lf
1.113    proof (rule HahnBanach)
1.114      show "\<forall>x \<in> F. f x \<le> p x"
1.115        using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
1.116 @@ -334,7 +335,7 @@
1.117    then obtain g where lg: "linearform E g" and *: "\<forall>x \<in> F. g x = f x"
1.118        and **: "\<forall>x \<in> E. g x \<le> p x" by blast
1.119    have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
1.120 -  using _ E sn lg **
1.121 +    using _ E sn lg **
1.122    proof (rule abs_ineq_iff [THEN iffD2])
1.123      show "E \<unlhd> E" ..
1.124    qed
1.125 @@ -384,10 +385,10 @@
1.126    have q: "seminorm E p"
1.127    proof
1.128      fix x y a assume x: "x \<in> E" and y: "y \<in> E"
1.129 -
1.130 +
1.131      txt {* @{text p} is positive definite: *}
1.132 -      have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
1.133 -      moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
1.134 +    have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
1.135 +    moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
1.136      ultimately show "0 \<le> p x"
1.137        by (simp add: p_def zero_le_mult_iff)
1.138
1.139 @@ -422,9 +423,9 @@
1.140    have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
1.141    proof
1.142      fix x assume "x \<in> F"
1.143 -    from this and `continuous F norm f`
1.144 +    with `continuous F norm f` and linearform
1.145      show "\<bar>f x\<bar> \<le> p x"
1.146 -      by (unfold p_def) (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
1.147 +      unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
1.148          [OF normed_vectorspace_with_fn_norm.intro,
1.149           OF F_norm, folded B_def fn_norm_def])
1.150    qed
1.151 @@ -435,9 +436,9 @@
1.152      some function @{text g} on the whole vector space @{text E}. *}
1.153
1.154    with E FE linearform q obtain g where
1.155 -        linearformE: "linearform E g"
1.156 -      and a: "\<forall>x \<in> F. g x = f x"
1.157 -      and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
1.158 +      linearformE: "linearform E g"
1.159 +    and a: "\<forall>x \<in> F. g x = f x"
1.160 +    and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
1.161      by (rule abs_HahnBanach [elim_format]) iprover
1.162
1.163    txt {* We furthermore have to show that @{text g} is also continuous: *}
1.164 @@ -489,7 +490,7 @@
1.165        proof
1.166  	fix x assume x: "x \<in> F"
1.167  	from a x have "g x = f x" ..
1.168 -	hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
1.169 +	then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
1.170  	also from g_cont
1.171  	have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
1.172  	proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
1.173 @@ -500,7 +501,6 @@
1.174        show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
1.175  	using g_cont
1.176  	by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
1.177 -    next
1.178        show "continuous F norm f" by fact
1.179      qed
1.180    qed
```