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.84                by (simp add: Let_def)
    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