author | wenzelm |

Tue Jul 15 19:39:37 2008 +0200 (2008-07-15) | |

changeset 27612 | d3eb431db035 |

parent 27611 | 2c01c0bdb385 |

child 27613 | 0e03b957c649 |

modernized specifications and proofs;

tuned document;

tuned document;

1.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 16:50:09 2008 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 19:39:37 2008 +0200 1.3 @@ -28,7 +28,8 @@ 1.4 shows "\<Squnion>A = (x::'a::order)" 1.5 proof - 1.6 interpret lub [A x] by fact 1.7 - show ?thesis proof (unfold the_lub_def) 1.8 + show ?thesis 1.9 + proof (unfold the_lub_def) 1.10 from `lub A x` show "The (lub A) = x" 1.11 proof 1.12 fix x' assume lub': "lub A x'" 1.13 @@ -73,7 +74,7 @@ 1.14 shows "\<exists>x. lub A x" 1.15 proof - 1.16 from ex_upper have "\<exists>y. isUb UNIV A y" 1.17 - by (unfold isUb_def setle_def) blast 1.18 + unfolding isUb_def setle_def by blast 1.19 with nonempty have "\<exists>x. isLub UNIV A x" 1.20 by (rule reals_complete) 1.21 then show ?thesis by (simp only: lub_compat)

2.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 16:50:09 2008 +0200 2.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 19:39:37 2008 +0200 2.3 @@ -5,7 +5,9 @@ 2.4 2.5 header {* The norm of a function *} 2.6 2.7 -theory FunctionNorm imports NormedSpace FunctionOrder begin 2.8 +theory FunctionNorm 2.9 +imports NormedSpace FunctionOrder 2.10 +begin 2.11 2.12 subsection {* Continuous linear forms*} 2.13 2.14 @@ -97,7 +99,7 @@ 2.15 proof (rule real_complete) 2.16 txt {* First we have to show that @{text B} is non-empty: *} 2.17 have "0 \<in> B V f" .. 2.18 - thus "\<exists>x. x \<in> B V f" .. 2.19 + then show "\<exists>x. x \<in> B V f" .. 2.20 2.21 txt {* Then we have to show that @{text B} is bounded: *} 2.22 show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" 2.23 @@ -116,7 +118,7 @@ 2.24 show "y \<le> b" 2.25 proof cases 2.26 assume "y = 0" 2.27 - thus ?thesis by (unfold b_def) arith 2.28 + then show ?thesis unfolding b_def by arith 2.29 next 2.30 txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some 2.31 @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} 2.32 @@ -135,21 +137,21 @@ 2.33 from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 2.34 from gt have "0 < inverse \<parallel>x\<parallel>" 2.35 by (rule positive_imp_inverse_positive) 2.36 - thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) 2.37 + then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) 2.38 qed 2.39 also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" 2.40 by (rule real_mult_assoc) 2.41 also 2.42 from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp 2.43 - hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 2.44 + then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 2.45 also have "c * 1 \<le> b" by (simp add: b_def le_maxI1) 2.46 finally show "y \<le> b" . 2.47 qed 2.48 qed 2.49 - thus ?thesis .. 2.50 + then show ?thesis .. 2.51 qed 2.52 qed 2.53 - then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex) 2.54 + then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) 2.55 qed 2.56 2.57 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: 2.58 @@ -185,7 +187,6 @@ 2.59 So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> 2.60 0"}, provided the supremum exists and @{text B} is not empty. *} 2.61 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 2.62 -(* unfolding B_def fn_norm_def *) 2.63 using `continuous V norm f` by (rule fn_norm_works) 2.64 moreover have "0 \<in> B V f" .. 2.65 ultimately show ?thesis .. 2.66 @@ -205,7 +206,8 @@ 2.67 proof - 2.68 interpret continuous [V norm f] by fact 2.69 interpret linearform [V f] . 2.70 - show ?thesis proof cases 2.71 + show ?thesis 2.72 + proof cases 2.73 assume "x = 0" 2.74 then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp 2.75 also have "f 0 = 0" by rule unfold_locales 2.76 @@ -245,7 +247,8 @@ 2.77 shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" 2.78 proof - 2.79 interpret continuous [V norm f] by fact 2.80 - show ?thesis proof (rule fn_norm_leastB [folded B_def fn_norm_def]) 2.81 + show ?thesis 2.82 + proof (rule fn_norm_leastB [folded B_def fn_norm_def]) 2.83 fix b assume b: "b \<in> B V f" 2.84 show "b \<le> c" 2.85 proof cases

3.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Jul 15 16:50:09 2008 +0200 3.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Jul 15 19:39:37 2008 +0200 3.3 @@ -5,7 +5,9 @@ 3.4 3.5 header {* An order on functions *} 3.6 3.7 -theory FunctionOrder imports Subspace Linearform begin 3.8 +theory FunctionOrder 3.9 +imports Subspace Linearform 3.10 +begin 3.11 3.12 subsection {* The graph of a function *} 3.13 3.14 @@ -27,14 +29,14 @@ 3.15 "graph F f = {(x, f x) | x. x \<in> F}" 3.16 3.17 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f" 3.18 - by (unfold graph_def) blast 3.19 + unfolding graph_def by blast 3.20 3.21 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)" 3.22 - by (unfold graph_def) blast 3.23 + unfolding graph_def by blast 3.24 3.25 lemma graphE [elim?]: 3.26 "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C" 3.27 - by (unfold graph_def) blast 3.28 + unfolding graph_def by blast 3.29 3.30 3.31 subsection {* Functions ordered by domain extension *} 3.32 @@ -47,15 +49,15 @@ 3.33 lemma graph_extI: 3.34 "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H' 3.35 \<Longrightarrow> graph H h \<subseteq> graph H' h'" 3.36 - by (unfold graph_def) blast 3.37 + unfolding graph_def by blast 3.38 3.39 lemma graph_extD1 [dest?]: 3.40 "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x" 3.41 - by (unfold graph_def) blast 3.42 + unfolding graph_def by blast 3.43 3.44 lemma graph_extD2 [dest?]: 3.45 "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'" 3.46 - by (unfold graph_def) blast 3.47 + unfolding graph_def by blast 3.48 3.49 3.50 subsection {* Domain and function of a graph *} 3.51 @@ -81,7 +83,8 @@ 3.52 lemma graph_domain_funct: 3.53 assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y" 3.54 shows "graph (domain g) (funct g) = g" 3.55 -proof (unfold domain_def funct_def graph_def, auto) (* FIXME !? *) 3.56 + unfolding domain_def funct_def graph_def 3.57 +proof auto (* FIXME !? *) 3.58 fix a b assume g: "(a, b) \<in> g" 3.59 from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) 3.60 from g show "\<exists>y. (a, y) \<in> g" .. 3.61 @@ -119,13 +122,13 @@ 3.62 \<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h 3.63 \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h 3.64 \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C" 3.65 - by (unfold norm_pres_extensions_def) blast 3.66 + unfolding norm_pres_extensions_def by blast 3.67 3.68 lemma norm_pres_extensionI2 [intro]: 3.69 "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H 3.70 \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x 3.71 \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f" 3.72 - by (unfold norm_pres_extensions_def) blast 3.73 + unfolding norm_pres_extensions_def by blast 3.74 3.75 lemma norm_pres_extensionI: (* FIXME ? *) 3.76 "\<exists>H h. g = graph H h 3.77 @@ -134,6 +137,6 @@ 3.78 \<and> F \<unlhd> H 3.79 \<and> graph F f \<subseteq> graph H h 3.80 \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f" 3.81 - by (unfold norm_pres_extensions_def) blast 3.82 + unfolding norm_pres_extensions_def by blast 3.83 3.84 end

4.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 16:50:09 2008 +0200 4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 19:39:37 2008 +0200 4.3 @@ -5,7 +5,9 @@ 4.4 4.5 header {* The Hahn-Banach Theorem *} 4.6 4.7 -theory HahnBanach imports HahnBanachLemmas begin 4.8 +theory HahnBanach 4.9 +imports HahnBanachLemmas 4.10 +begin 4.11 4.12 text {* 4.13 We present the proof of two different versions of the Hahn-Banach 4.14 @@ -66,7 +68,7 @@ 4.15 interpret seminorm [E p] by fact 4.16 interpret linearform [F f] by fact 4.17 def M \<equiv> "norm_pres_extensions E p F f" 4.18 - hence M: "M = \<dots>" by (simp only:) 4.19 + then have M: "M = \<dots>" by (simp only:) 4.20 from E have F: "vectorspace F" .. 4.21 note FE = `F \<unlhd> E` 4.22 { 4.23 @@ -74,7 +76,8 @@ 4.24 have "\<Union>c \<in> M" 4.25 -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *} 4.26 -- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *} 4.27 - proof (unfold M_def, rule norm_pres_extensionI) 4.28 + unfolding M_def 4.29 + proof (rule norm_pres_extensionI) 4.30 let ?H = "domain (\<Union>c)" 4.31 let ?h = "funct (\<Union>c)" 4.32 4.33 @@ -101,12 +104,13 @@ 4.34 \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast 4.35 qed 4.36 } 4.37 - hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" 4.38 + then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" 4.39 -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *} 4.40 proof (rule Zorn's_Lemma) 4.41 -- {* We show that @{text M} is non-empty: *} 4.42 show "graph F f \<in> M" 4.43 - proof (unfold M_def, rule norm_pres_extensionI2) 4.44 + unfolding M_def 4.45 + proof (rule norm_pres_extensionI2) 4.46 show "linearform F f" by fact 4.47 show "F \<unlhd> E" by fact 4.48 from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl) 4.49 @@ -116,12 +120,12 @@ 4.50 qed 4.51 then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" 4.52 by blast 4.53 - from gM [unfolded M_def] obtain H h where 4.54 + from gM obtain H h where 4.55 g_rep: "g = graph H h" 4.56 and linearform: "linearform H h" 4.57 and HE: "H \<unlhd> E" and FH: "F \<unlhd> H" 4.58 and graphs: "graph F f \<subseteq> graph H h" 4.59 - and hp: "\<forall>x \<in> H. h x \<le> p x" .. 4.60 + and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def .. 4.61 -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *} 4.62 -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} 4.63 -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} 4.64 @@ -213,14 +217,15 @@ 4.65 proof 4.66 assume eq: "graph H h = graph H' h'" 4.67 have "x' \<in> H'" 4.68 - proof (unfold H'_def, rule) 4.69 + unfolding H'_def 4.70 + proof 4.71 from H show "0 \<in> H" by (rule vectorspace.zero) 4.72 from x'E show "x' \<in> lin x'" by (rule x_lin_x) 4.73 from x'E show "x' = 0 + x'" by simp 4.74 qed 4.75 - hence "(x', h' x') \<in> graph H' h'" .. 4.76 + then have "(x', h' x') \<in> graph H' h'" .. 4.77 with eq have "(x', h' x') \<in> graph H h" by (simp only:) 4.78 - hence "x' \<in> H" .. 4.79 + then have "x' \<in> H" .. 4.80 with `x' \<notin> H` show False by contradiction 4.81 qed 4.82 with g_rep show ?thesis by simp 4.83 @@ -252,7 +257,7 @@ 4.84 by (simp add: Let_def) 4.85 also have "(x, 0) = 4.86 (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)" 4.87 - using E HE 4.88 + using E HE 4.89 proof (rule decomp_H'_H [symmetric]) 4.90 from FH x show "x \<in> H" .. 4.91 from x' show "x' \<noteq> 0" . 4.92 @@ -274,7 +279,7 @@ 4.93 qed 4.94 ultimately show ?thesis .. 4.95 qed 4.96 - hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp 4.97 + then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp 4.98 -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} 4.99 with gx show "H = E" by contradiction 4.100 qed 4.101 @@ -321,12 +326,8 @@ 4.102 interpret subspace [F E] by fact 4.103 interpret linearform [F f] by fact 4.104 interpret seminorm [E p] by fact 4.105 -(* note E = `vectorspace E` 4.106 - note FE = `subspace F E` 4.107 - note sn = `seminorm E p` 4.108 - note lf = `linearform F f` 4.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)" 4.110 - using E FE sn lf 4.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)" 4.112 + using E FE sn lf 4.113 proof (rule HahnBanach) 4.114 show "\<forall>x \<in> F. f x \<le> p x" 4.115 using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1]) 4.116 @@ -334,7 +335,7 @@ 4.117 then obtain g where lg: "linearform E g" and *: "\<forall>x \<in> F. g x = f x" 4.118 and **: "\<forall>x \<in> E. g x \<le> p x" by blast 4.119 have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x" 4.120 - using _ E sn lg ** 4.121 + using _ E sn lg ** 4.122 proof (rule abs_ineq_iff [THEN iffD2]) 4.123 show "E \<unlhd> E" .. 4.124 qed 4.125 @@ -384,10 +385,10 @@ 4.126 have q: "seminorm E p" 4.127 proof 4.128 fix x y a assume x: "x \<in> E" and y: "y \<in> E" 4.129 - 4.130 + 4.131 txt {* @{text p} is positive definite: *} 4.132 - have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) 4.133 - moreover from x have "0 \<le> \<parallel>x\<parallel>" .. 4.134 + have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) 4.135 + moreover from x have "0 \<le> \<parallel>x\<parallel>" .. 4.136 ultimately show "0 \<le> p x" 4.137 by (simp add: p_def zero_le_mult_iff) 4.138 4.139 @@ -422,9 +423,9 @@ 4.140 have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x" 4.141 proof 4.142 fix x assume "x \<in> F" 4.143 - from this and `continuous F norm f` 4.144 + with `continuous F norm f` and linearform 4.145 show "\<bar>f x\<bar> \<le> p x" 4.146 - by (unfold p_def) (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong 4.147 + unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong 4.148 [OF normed_vectorspace_with_fn_norm.intro, 4.149 OF F_norm, folded B_def fn_norm_def]) 4.150 qed 4.151 @@ -435,9 +436,9 @@ 4.152 some function @{text g} on the whole vector space @{text E}. *} 4.153 4.154 with E FE linearform q obtain g where 4.155 - linearformE: "linearform E g" 4.156 - and a: "\<forall>x \<in> F. g x = f x" 4.157 - and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x" 4.158 + linearformE: "linearform E g" 4.159 + and a: "\<forall>x \<in> F. g x = f x" 4.160 + and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x" 4.161 by (rule abs_HahnBanach [elim_format]) iprover 4.162 4.163 txt {* We furthermore have to show that @{text g} is also continuous: *} 4.164 @@ -489,7 +490,7 @@ 4.165 proof 4.166 fix x assume x: "x \<in> F" 4.167 from a x have "g x = f x" .. 4.168 - hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:) 4.169 + then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:) 4.170 also from g_cont 4.171 have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" 4.172 proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def]) 4.173 @@ -500,7 +501,6 @@ 4.174 show "0 \<le> \<parallel>g\<parallel>\<hyphen>E" 4.175 using g_cont 4.176 by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) 4.177 - next 4.178 show "continuous F norm f" by fact 4.179 qed 4.180 qed

5.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 16:50:09 2008 +0200 5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 19:39:37 2008 +0200 5.3 @@ -5,7 +5,9 @@ 5.4 5.5 header {* Extending non-maximal functions *} 5.6 5.7 -theory HahnBanachExtLemmas imports FunctionNorm begin 5.8 +theory HahnBanachExtLemmas 5.9 +imports FunctionNorm 5.10 +begin 5.11 5.12 text {* 5.13 In this section the following context is presumed. Let @{text E} be 5.14 @@ -98,7 +100,8 @@ 5.15 proof - 5.16 interpret linearform [H h] by fact 5.17 interpret vectorspace [E] by fact 5.18 - show ?thesis proof 5.19 + show ?thesis 5.20 + proof 5.21 note E = `vectorspace E` 5.22 have H': "vectorspace H'" 5.23 proof (unfold H'_def) 5.24 @@ -116,7 +119,7 @@ 5.25 x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H" 5.26 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 5.27 and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H" 5.28 - by (unfold H'_def sum_def lin_def) blast 5.29 + unfolding H'_def sum_def lin_def by blast 5.30 5.31 have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0 5.32 proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} 5.33 @@ -154,9 +157,9 @@ 5.34 from H' x1 have ax1: "c \<cdot> x1 \<in> H'" 5.35 by (rule vectorspace.mult_closed) 5.36 with x1 obtain y a y1 a1 where 5.37 - cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" 5.38 + cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" 5.39 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 5.40 - by (unfold H'_def sum_def lin_def) blast 5.41 + unfolding H'_def sum_def lin_def by blast 5.42 5.43 have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0 5.44 proof (rule decomp_H') 5.45 @@ -204,15 +207,16 @@ 5.46 interpret subspace [H E] by fact 5.47 interpret seminorm [E p] by fact 5.48 interpret linearform [H h] by fact 5.49 - show ?thesis proof 5.50 + show ?thesis 5.51 + proof 5.52 fix x assume x': "x \<in> H'" 5.53 show "h' x \<le> p x" 5.54 proof - 5.55 from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi" 5.56 and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto 5.57 from x' obtain y a where 5.58 - x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H" 5.59 - by (unfold H'_def sum_def lin_def) blast 5.60 + x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H" 5.61 + unfolding H'_def sum_def lin_def by blast 5.62 from y have y': "y \<in> E" .. 5.63 from y have ay: "inverse a \<cdot> y \<in> H" by simp 5.64 5.65 @@ -228,7 +232,7 @@ 5.66 next 5.67 txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} 5.68 with @{text ya} taken as @{text "y / a"}: *} 5.69 - assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp 5.70 + assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp 5.71 from a1 ay 5.72 have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" .. 5.73 with lz have "a * xi \<le> 5.74 @@ -250,13 +254,13 @@ 5.75 next 5.76 txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} 5.77 with @{text ya} taken as @{text "y / a"}: *} 5.78 - assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp 5.79 + assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp 5.80 from a2 ay 5.81 have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" .. 5.82 with gz have "a * xi \<le> 5.83 a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))" 5.84 by simp 5.85 - also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)" 5.86 + also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)" 5.87 by (simp add: right_diff_distrib) 5.88 also from gz x0 y' 5.89 have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"

6.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 16:50:09 2008 +0200 6.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 19:39:37 2008 +0200 6.3 @@ -5,7 +5,9 @@ 6.4 6.5 header {* The supremum w.r.t.~the function order *} 6.6 6.7 -theory HahnBanachSupLemmas imports FunctionNorm ZornLemma begin 6.8 +theory HahnBanachSupLemmas 6.9 +imports FunctionNorm ZornLemma 6.10 +begin 6.11 6.12 text {* 6.13 This section contains some lemmas that will be used in the proof of 6.14 @@ -132,7 +134,7 @@ 6.15 proof 6.16 assume ?case1 6.17 have "(x, h x) \<in> graph H'' h''" by fact 6.18 - also have "... \<subseteq> graph H' h'" by fact 6.19 + also have "\<dots> \<subseteq> graph H' h'" by fact 6.20 finally have xh:"(x, h x) \<in> graph H' h'" . 6.21 then have "x \<in> H'" .. 6.22 moreover from y_hy have "y \<in> H'" .. 6.23 @@ -171,11 +173,11 @@ 6.24 6.25 from G1 c have "G1 \<in> M" .. 6.26 then obtain H1 h1 where G1_rep: "G1 = graph H1 h1" 6.27 - by (unfold M_def) blast 6.28 + unfolding M_def by blast 6.29 6.30 from G2 c have "G2 \<in> M" .. 6.31 then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" 6.32 - by (unfold M_def) blast 6.33 + unfolding M_def by blast 6.34 6.35 txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"} 6.36 or vice versa, since both @{text "G\<^sub>1"} and @{text 6.37 @@ -186,18 +188,18 @@ 6.38 proof 6.39 assume ?case1 6.40 with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast 6.41 - hence "y = h2 x" .. 6.42 + then have "y = h2 x" .. 6.43 also 6.44 from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:) 6.45 - hence "z = h2 x" .. 6.46 + then have "z = h2 x" .. 6.47 finally show ?thesis . 6.48 next 6.49 assume ?case2 6.50 with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast 6.51 - hence "z = h1 x" .. 6.52 + then have "z = h1 x" .. 6.53 also 6.54 from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:) 6.55 - hence "y = h1 x" .. 6.56 + then have "y = h1 x" .. 6.57 finally show ?thesis .. 6.58 qed 6.59 qed

7.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:50:09 2008 +0200 7.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 19:39:37 2008 +0200 7.3 @@ -5,7 +5,9 @@ 7.4 7.5 header {* Linearforms *} 7.6 7.7 -theory Linearform imports VectorSpace begin 7.8 +theory Linearform 7.9 +imports VectorSpace 7.10 +begin 7.11 7.12 text {* 7.13 A \emph{linear form} is a function on a vector space into the reals 7.14 @@ -25,9 +27,9 @@ 7.15 proof - 7.16 interpret vectorspace [V] by fact 7.17 assume x: "x \<in> V" 7.18 - hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1) 7.19 - also from x have "... = (- 1) * (f x)" by (rule mult) 7.20 - also from x have "... = - (f x)" by simp 7.21 + then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1) 7.22 + also from x have "\<dots> = (- 1) * (f x)" by (rule mult) 7.23 + also from x have "\<dots> = - (f x)" by simp 7.24 finally show ?thesis . 7.25 qed 7.26 7.27 @@ -37,8 +39,8 @@ 7.28 proof - 7.29 interpret vectorspace [V] by fact 7.30 assume x: "x \<in> V" and y: "y \<in> V" 7.31 - hence "x - y = x + - y" by (rule diff_eq1) 7.32 - also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y) 7.33 + then have "x - y = x + - y" by (rule diff_eq1) 7.34 + also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y) 7.35 also have "f (- y) = - f y" using `vectorspace V` y by (rule neg) 7.36 finally show ?thesis by simp 7.37 qed

8.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 16:50:09 2008 +0200 8.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 19:39:37 2008 +0200 8.3 @@ -5,7 +5,9 @@ 8.4 8.5 header {* Normed vector spaces *} 8.6 8.7 -theory NormedSpace imports Subspace begin 8.8 +theory NormedSpace 8.9 +imports Subspace 8.10 +begin 8.11 8.12 subsection {* Quasinorms *} 8.13 8.14 @@ -32,7 +34,7 @@ 8.15 proof - 8.16 interpret vectorspace [V] by fact 8.17 assume x: "x \<in> V" and y: "y \<in> V" 8.18 - hence "x - y = x + - 1 \<cdot> y" 8.19 + then have "x - y = x + - 1 \<cdot> y" 8.20 by (simp add: diff_eq2 negate_eq2a) 8.21 also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>" 8.22 by (simp add: subadditive) 8.23 @@ -48,7 +50,7 @@ 8.24 proof - 8.25 interpret vectorspace [V] by fact 8.26 assume x: "x \<in> V" 8.27 - hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1) 8.28 + then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1) 8.29 also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" 8.30 by (rule abs_homogenous) 8.31 also have "\<dots> = \<parallel>x\<parallel>" by simp 8.32 @@ -103,7 +105,8 @@ 8.33 proof - 8.34 interpret subspace [F E] by fact 8.35 interpret normed_vectorspace [E norm] by fact 8.36 - show ?thesis proof 8.37 + show ?thesis 8.38 + proof 8.39 show "vectorspace F" by (rule vectorspace) unfold_locales 8.40 next 8.41 have "NormedSpace.norm E norm" by unfold_locales

9.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy Tue Jul 15 16:50:09 2008 +0200 9.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Tue Jul 15 19:39:37 2008 +0200 9.3 @@ -5,8 +5,9 @@ 9.4 9.5 header {* Subspaces *} 9.6 9.7 -theory Subspace imports VectorSpace begin 9.8 - 9.9 +theory Subspace 9.10 +imports VectorSpace 9.11 +begin 9.12 9.13 subsection {* Definition *} 9.14 9.15 @@ -42,10 +43,11 @@ 9.16 9.17 lemma (in subspace) diff_closed [iff]: 9.18 assumes "vectorspace V" 9.19 - shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U" (is "PROP ?P") 9.20 + assumes x: "x \<in> U" and y: "y \<in> U" 9.21 + shows "x - y \<in> U" 9.22 proof - 9.23 interpret vectorspace [V] by fact 9.24 - show "PROP ?P" by (simp add: diff_eq1 negate_eq1) 9.25 + from x y show ?thesis by (simp add: diff_eq1 negate_eq1) 9.26 qed 9.27 9.28 text {* 9.29 @@ -61,17 +63,18 @@ 9.30 interpret vectorspace [V] by fact 9.31 have "U \<noteq> {}" by (rule U_V.non_empty) 9.32 then obtain x where x: "x \<in> U" by blast 9.33 - hence "x \<in> V" .. hence "0 = x - x" by simp 9.34 - also from `vectorspace V` x x have "... \<in> U" by (rule U_V.diff_closed) 9.35 + then have "x \<in> V" .. then have "0 = x - x" by simp 9.36 + also from `vectorspace V` x x have "\<dots> \<in> U" by (rule U_V.diff_closed) 9.37 finally show ?thesis . 9.38 qed 9.39 9.40 lemma (in subspace) neg_closed [iff]: 9.41 assumes "vectorspace V" 9.42 - shows "x \<in> U \<Longrightarrow> - x \<in> U" (is "PROP ?P") 9.43 + assumes x: "x \<in> U" 9.44 + shows "- x \<in> U" 9.45 proof - 9.46 interpret vectorspace [V] by fact 9.47 - show "PROP ?P" by (simp add: negate_eq1) 9.48 + from x show ?thesis by (simp add: negate_eq1) 9.49 qed 9.50 9.51 text {* \medskip Further derived laws: every subspace is a vector space. *} 9.52 @@ -81,7 +84,8 @@ 9.53 shows "vectorspace U" 9.54 proof - 9.55 interpret vectorspace [V] by fact 9.56 - show ?thesis proof 9.57 + show ?thesis 9.58 + proof 9.59 show "U \<noteq> {}" .. 9.60 fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U" 9.61 fix a b :: real 9.62 @@ -144,14 +148,13 @@ 9.63 "lin x = {a \<cdot> x | a. True}" 9.64 9.65 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x" 9.66 - by (unfold lin_def) blast 9.67 + unfolding lin_def by blast 9.68 9.69 lemma linI' [iff]: "a \<cdot> x \<in> lin x" 9.70 - by (unfold lin_def) blast 9.71 + unfolding lin_def by blast 9.72 9.73 -lemma linE [elim]: 9.74 - "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C" 9.75 - by (unfold lin_def) blast 9.76 +lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C" 9.77 + unfolding lin_def by blast 9.78 9.79 9.80 text {* Every vector is contained in its linear closure. *} 9.81 @@ -159,7 +162,7 @@ 9.82 lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x" 9.83 proof - 9.84 assume "x \<in> V" 9.85 - hence "x = 1 \<cdot> x" by simp 9.86 + then have "x = 1 \<cdot> x" by simp 9.87 also have "\<dots> \<in> lin x" .. 9.88 finally show ?thesis . 9.89 qed 9.90 @@ -167,7 +170,7 @@ 9.91 lemma (in vectorspace) "0_lin_x" [iff]: "x \<in> V \<Longrightarrow> 0 \<in> lin x" 9.92 proof 9.93 assume "x \<in> V" 9.94 - thus "0 = 0 \<cdot> x" by simp 9.95 + then show "0 = 0 \<cdot> x" by simp 9.96 qed 9.97 9.98 text {* Any linear closure is a subspace. *} 9.99 @@ -176,7 +179,7 @@ 9.100 "x \<in> V \<Longrightarrow> lin x \<unlhd> V" 9.101 proof 9.102 assume x: "x \<in> V" 9.103 - thus "lin x \<noteq> {}" by (auto simp add: x_lin_x) 9.104 + then show "lin x \<noteq> {}" by (auto simp add: x_lin_x) 9.105 show "lin x \<subseteq> V" 9.106 proof 9.107 fix x' assume "x' \<in> lin x" 9.108 @@ -224,22 +227,27 @@ 9.109 set of all sums of elements from @{text U} and @{text V}. 9.110 *} 9.111 9.112 -instance "fun" :: (type, type) plus .. 9.113 +instantiation "fun" :: (type, type) plus 9.114 +begin 9.115 9.116 -defs (overloaded) 9.117 - sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}" 9.118 +definition 9.119 + sum_def: "plus_fun U V = {u + v | u v. u \<in> U \<and> v \<in> V}" (* FIXME not fully general!? *) 9.120 + 9.121 +instance .. 9.122 + 9.123 +end 9.124 9.125 lemma sumE [elim]: 9.126 "x \<in> U + V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C" 9.127 - by (unfold sum_def) blast 9.128 + unfolding sum_def by blast 9.129 9.130 lemma sumI [intro]: 9.131 "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V" 9.132 - by (unfold sum_def) blast 9.133 + unfolding sum_def by blast 9.134 9.135 lemma sumI' [intro]: 9.136 "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V" 9.137 - by (unfold sum_def) blast 9.138 + unfolding sum_def by blast 9.139 9.140 text {* @{text U} is a subspace of @{text "U + V"}. *} 9.141 9.142 @@ -249,7 +257,8 @@ 9.143 proof - 9.144 interpret vectorspace [U] by fact 9.145 interpret vectorspace [V] by fact 9.146 - show ?thesis proof 9.147 + show ?thesis 9.148 + proof 9.149 show "U \<noteq> {}" .. 9.150 show "U \<subseteq> U + V" 9.151 proof 9.152 @@ -259,7 +268,7 @@ 9.153 with x show "x \<in> U + V" by simp 9.154 qed 9.155 fix x y assume x: "x \<in> U" and "y \<in> U" 9.156 - thus "x + y \<in> U" by simp 9.157 + then show "x + y \<in> U" by simp 9.158 from x show "\<And>a. a \<cdot> x \<in> U" by simp 9.159 qed 9.160 qed 9.161 @@ -273,14 +282,15 @@ 9.162 interpret subspace [U E] by fact 9.163 interpret vectorspace [E] by fact 9.164 interpret subspace [V E] by fact 9.165 - show ?thesis proof 9.166 + show ?thesis 9.167 + proof 9.168 have "0 \<in> U + V" 9.169 proof 9.170 show "0 \<in> U" using `vectorspace E` .. 9.171 show "0 \<in> V" using `vectorspace E` .. 9.172 show "(0::'a) = 0 + 0" by simp 9.173 qed 9.174 - thus "U + V \<noteq> {}" by blast 9.175 + then show "U + V \<noteq> {}" by blast 9.176 show "U + V \<subseteq> E" 9.177 proof 9.178 fix x assume "x \<in> U + V" 9.179 @@ -299,14 +309,14 @@ 9.180 and "vx + vy \<in> V" 9.181 and "x + y = (ux + uy) + (vx + vy)" 9.182 using x y by (simp_all add: add_ac) 9.183 - thus ?thesis .. 9.184 + then show ?thesis .. 9.185 qed 9.186 fix a show "a \<cdot> x \<in> U + V" 9.187 proof - 9.188 from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" .. 9.189 - hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V" 9.190 + then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V" 9.191 and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib) 9.192 - thus ?thesis .. 9.193 + then show ?thesis .. 9.194 qed 9.195 qed 9.196 qed 9.197 @@ -339,7 +349,8 @@ 9.198 interpret vectorspace [E] by fact 9.199 interpret subspace [U E] by fact 9.200 interpret subspace [V E] by fact 9.201 - show ?thesis proof 9.202 + show ?thesis 9.203 + proof 9.204 have U: "vectorspace U" (* FIXME: use interpret *) 9.205 using `subspace U E` `vectorspace E` by (rule subspace.vectorspace) 9.206 have V: "vectorspace V" 9.207 @@ -386,7 +397,8 @@ 9.208 proof - 9.209 interpret vectorspace [E] by fact 9.210 interpret subspace [H E] by fact 9.211 - show ?thesis proof 9.212 + show ?thesis 9.213 + proof 9.214 have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'" 9.215 proof (rule decomp) 9.216 show "a1 \<cdot> x' \<in> lin x'" .. 9.217 @@ -409,7 +421,7 @@ 9.218 with a and x' have "x' \<in> H" by (simp add: mult_assoc2) 9.219 with `x' \<notin> H` show ?thesis by contradiction 9.220 qed 9.221 - thus "x \<in> {0}" .. 9.222 + then show "x \<in> {0}" .. 9.223 qed 9.224 show "{0} \<subseteq> H \<inter> lin x'" 9.225 proof - 9.226 @@ -420,7 +432,7 @@ 9.227 qed 9.228 show "lin x' \<unlhd> E" using `x' \<in> E` .. 9.229 qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) 9.230 - thus "y1 = y2" .. 9.231 + then show "y1 = y2" .. 9.232 from c have "a1 \<cdot> x' = a2 \<cdot> x'" .. 9.233 with x' show "a1 = a2" by (simp add: mult_right_cancel) 9.234 qed 9.235 @@ -441,7 +453,8 @@ 9.236 proof - 9.237 interpret vectorspace [E] by fact 9.238 interpret subspace [H E] by fact 9.239 - show ?thesis proof (rule, simp_all only: split_paired_all split_conv) 9.240 + show ?thesis 9.241 + proof (rule, simp_all only: split_paired_all split_conv) 9.242 from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp 9.243 fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H" 9.244 have "y = t \<and> a = 0" 9.245 @@ -490,10 +503,10 @@ 9.246 from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'" 9.247 by simp 9.248 qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+) 9.249 - thus ?thesis by (cases p, cases q) simp 9.250 + then show ?thesis by (cases p, cases q) simp 9.251 qed 9.252 qed 9.253 - hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 9.254 + then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 9.255 by (rule some1_equality) (simp add: x y) 9.256 with h'_def show "h' x = h y + a * xi" by (simp add: Let_def) 9.257 qed

10.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Jul 15 16:50:09 2008 +0200 10.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Jul 15 19:39:37 2008 +0200 10.3 @@ -5,7 +5,9 @@ 10.4 10.5 header {* Vector spaces *} 10.6 10.7 -theory VectorSpace imports Real Bounds Zorn begin 10.8 +theory VectorSpace 10.9 +imports Real Bounds Zorn 10.10 +begin 10.11 10.12 subsection {* Signature *} 10.13 10.14 @@ -71,10 +73,10 @@ 10.15 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" 10.16 proof - 10.17 assume xyz: "x \<in> V" "y \<in> V" "z \<in> V" 10.18 - hence "x + (y + z) = (x + y) + z" 10.19 + then have "x + (y + z) = (x + y) + z" 10.20 by (simp only: add_assoc) 10.21 - also from xyz have "... = (y + x) + z" by (simp only: add_commute) 10.22 - also from xyz have "... = y + (x + z)" by (simp only: add_assoc) 10.23 + also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute) 10.24 + also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc) 10.25 finally show ?thesis . 10.26 qed 10.27 10.28 @@ -89,7 +91,7 @@ 10.29 proof - 10.30 from non_empty obtain x where x: "x \<in> V" by blast 10.31 then have "0 = x - x" by (rule diff_self [symmetric]) 10.32 - also from x x have "... \<in> V" by (rule diff_closed) 10.33 + also from x x have "\<dots> \<in> V" by (rule diff_closed) 10.34 finally show ?thesis . 10.35 qed 10.36 10.37 @@ -98,7 +100,7 @@ 10.38 proof - 10.39 assume x: "x \<in> V" 10.40 from this and zero have "x + 0 = 0 + x" by (rule add_commute) 10.41 - also from x have "... = x" by (rule add_zero_left) 10.42 + also from x have "\<dots> = x" by (rule add_zero_left) 10.43 finally show ?thesis . 10.44 qed 10.45 10.46 @@ -116,11 +118,11 @@ 10.47 assume x: "x \<in> V" 10.48 have " (a - b) \<cdot> x = (a + - b) \<cdot> x" 10.49 by (simp add: real_diff_def) 10.50 - also from x have "... = a \<cdot> x + (- b) \<cdot> x" 10.51 + also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x" 10.52 by (rule add_mult_distrib2) 10.53 - also from x have "... = a \<cdot> x + - (b \<cdot> x)" 10.54 + also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)" 10.55 by (simp add: negate_eq1 mult_assoc2) 10.56 - also from x have "... = a \<cdot> x - (b \<cdot> x)" 10.57 + also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)" 10.58 by (simp add: diff_eq1) 10.59 finally show ?thesis . 10.60 qed 10.61 @@ -137,13 +139,13 @@ 10.62 proof - 10.63 assume x: "x \<in> V" 10.64 have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp 10.65 - also have "... = (1 + - 1) \<cdot> x" by simp 10.66 - also from x have "... = 1 \<cdot> x + (- 1) \<cdot> x" 10.67 + also have "\<dots> = (1 + - 1) \<cdot> x" by simp 10.68 + also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x" 10.69 by (rule add_mult_distrib2) 10.70 - also from x have "... = x + (- 1) \<cdot> x" by simp 10.71 - also from x have "... = x + - x" by (simp add: negate_eq2a) 10.72 - also from x have "... = x - x" by (simp add: diff_eq2) 10.73 - also from x have "... = 0" by simp 10.74 + also from x have "\<dots> = x + (- 1) \<cdot> x" by simp 10.75 + also from x have "\<dots> = x + - x" by (simp add: negate_eq2a) 10.76 + also from x have "\<dots> = x - x" by (simp add: diff_eq2) 10.77 + also from x have "\<dots> = 0" by simp 10.78 finally show ?thesis . 10.79 qed 10.80 10.81 @@ -151,9 +153,9 @@ 10.82 "a \<cdot> 0 = (0::'a)" 10.83 proof - 10.84 have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp 10.85 - also have "... = a \<cdot> 0 - a \<cdot> 0" 10.86 + also have "\<dots> = a \<cdot> 0 - a \<cdot> 0" 10.87 by (rule diff_mult_distrib1) simp_all 10.88 - also have "... = 0" by simp 10.89 + also have "\<dots> = 0" by simp 10.90 finally show ?thesis . 10.91 qed 10.92 10.93 @@ -165,8 +167,8 @@ 10.94 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x" 10.95 proof - 10.96 assume xy: "x \<in> V" "y \<in> V" 10.97 - hence "- x + y = y + - x" by (simp add: add_commute) 10.98 - also from xy have "... = y - x" by (simp add: diff_eq1) 10.99 + then have "- x + y = y + - x" by (simp add: add_commute) 10.100 + also from xy have "\<dots> = y - x" by (simp add: diff_eq1) 10.101 finally show ?thesis . 10.102 qed 10.103 10.104 @@ -193,7 +195,7 @@ 10.105 { 10.106 from x have "x = - (- x)" by (simp add: minus_minus) 10.107 also assume "- x = 0" 10.108 - also have "- ... = 0" by (rule minus_zero) 10.109 + also have "- \<dots> = 0" by (rule minus_zero) 10.110 finally show "x = 0" . 10.111 next 10.112 assume "x = 0" 10.113 @@ -227,13 +229,13 @@ 10.114 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" 10.115 { 10.116 from y have "y = 0 + y" by simp 10.117 - also from x y have "... = (- x + x) + y" by simp 10.118 - also from x y have "... = - x + (x + y)" 10.119 + also from x y have "\<dots> = (- x + x) + y" by simp 10.120 + also from x y have "\<dots> = - x + (x + y)" 10.121 by (simp add: add_assoc neg_closed) 10.122 also assume "x + y = x + z" 10.123 also from x z have "- x + (x + z) = - x + x + z" 10.124 by (simp add: add_assoc [symmetric] neg_closed) 10.125 - also from x z have "... = z" by simp 10.126 + also from x z have "\<dots> = z" by simp 10.127 finally show "y = z" . 10.128 next 10.129 assume "y = z" 10.130 @@ -260,9 +262,9 @@ 10.131 assume a: "a \<noteq> 0" 10.132 assume x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0" 10.133 from x a have "x = (inverse a * a) \<cdot> x" by simp 10.134 - also from `x \<in> V` have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) 10.135 - also from ax have "... = inverse a \<cdot> 0" by simp 10.136 - also have "... = 0" by simp 10.137 + also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) 10.138 + also from ax have "\<dots> = inverse a \<cdot> 0" by simp 10.139 + also have "\<dots> = 0" by simp 10.140 finally have "x = 0" . 10.141 with `x \<noteq> 0` show "a = 0" by contradiction 10.142 qed 10.143 @@ -272,11 +274,11 @@ 10.144 proof 10.145 assume x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0" 10.146 from x have "x = 1 \<cdot> x" by simp 10.147 - also from a have "... = (inverse a * a) \<cdot> x" by simp 10.148 - also from x have "... = inverse a \<cdot> (a \<cdot> x)" 10.149 + also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp 10.150 + also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)" 10.151 by (simp only: mult_assoc) 10.152 also assume "a \<cdot> x = a \<cdot> y" 10.153 - also from a y have "inverse a \<cdot> ... = y" 10.154 + also from a y have "inverse a \<cdot> \<dots> = y" 10.155 by (simp add: mult_assoc2) 10.156 finally show "x = y" . 10.157 next 10.158 @@ -295,7 +297,7 @@ 10.159 with x have "a \<cdot> x - b \<cdot> x = 0" by simp 10.160 finally have "(a - b) \<cdot> x = 0" . 10.161 with x neq have "a - b = 0" by (rule mult_zero_uniq) 10.162 - thus "a = b" by simp 10.163 + then show "a = b" by simp 10.164 next 10.165 assume "a = b" 10.166 then show "a \<cdot> x = b \<cdot> x" by (simp only:) 10.167 @@ -308,24 +310,24 @@ 10.168 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" 10.169 { 10.170 assume "x = z - y" 10.171 - hence "x + y = z - y + y" by simp 10.172 - also from y z have "... = z + - y + y" 10.173 + then have "x + y = z - y + y" by simp 10.174 + also from y z have "\<dots> = z + - y + y" 10.175 by (simp add: diff_eq1) 10.176 - also have "... = z + (- y + y)" 10.177 + also have "\<dots> = z + (- y + y)" 10.178 by (rule add_assoc) (simp_all add: y z) 10.179 - also from y z have "... = z + 0" 10.180 + also from y z have "\<dots> = z + 0" 10.181 by (simp only: add_minus_left) 10.182 - also from z have "... = z" 10.183 + also from z have "\<dots> = z" 10.184 by (simp only: add_zero_right) 10.185 finally show "x + y = z" . 10.186 next 10.187 assume "x + y = z" 10.188 - hence "z - y = (x + y) - y" by simp 10.189 - also from x y have "... = x + y + - y" 10.190 + then have "z - y = (x + y) - y" by simp 10.191 + also from x y have "\<dots> = x + y + - y" 10.192 by (simp add: diff_eq1) 10.193 - also have "... = x + (y + - y)" 10.194 + also have "\<dots> = x + (y + - y)" 10.195 by (rule add_assoc) (simp_all add: x y) 10.196 - also from x y have "... = x" by simp 10.197 + also from x y have "\<dots> = x" by simp 10.198 finally show "x = z - y" .. 10.199 } 10.200 qed 10.201 @@ -335,7 +337,7 @@ 10.202 proof - 10.203 assume x: "x \<in> V" and y: "y \<in> V" 10.204 from x y have "x = (- y + y) + x" by simp 10.205 - also from x y have "... = - y + (x + y)" by (simp add: add_ac) 10.206 + also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac) 10.207 also assume "x + y = 0" 10.208 also from y have "- y + 0 = - y" by simp 10.209 finally show "x = - y" . 10.210 @@ -360,13 +362,13 @@ 10.211 and eq: "a + b = c + d" 10.212 then have "- c + (a + b) = - c + (c + d)" 10.213 by (simp add: add_left_cancel) 10.214 - also have "... = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel) 10.215 + also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel) 10.216 finally have eq: "- c + (a + b) = d" . 10.217 from vs have "a - c = (- c + (a + b)) + - b" 10.218 by (simp add: add_ac diff_eq1) 10.219 - also from vs eq have "... = d + - b" 10.220 + also from vs eq have "\<dots> = d + - b" 10.221 by (simp add: add_right_cancel) 10.222 - also from vs have "... = d - b" by (simp add: diff_eq2) 10.223 + also from vs have "\<dots> = d - b" by (simp add: diff_eq2) 10.224 finally show "a - c = d - b" . 10.225 qed 10.226 10.227 @@ -377,7 +379,7 @@ 10.228 assume vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V" 10.229 { 10.230 from vs have "x + z = - y + y + (x + z)" by simp 10.231 - also have "... = - y + (y + (x + z))" 10.232 + also have "\<dots> = - y + (y + (x + z))" 10.233 by (rule add_assoc) (simp_all add: vs) 10.234 also from vs have "y + (x + z) = x + (y + z)" 10.235 by (simp add: add_ac) 10.236 @@ -404,10 +406,10 @@ 10.237 with vs show "x = - z" by (simp add: add_minus_eq_minus) 10.238 next 10.239 assume eq: "x = - z" 10.240 - hence "x + (y + z) = - z + (y + z)" by simp 10.241 - also have "... = y + (- z + z)" 10.242 + then have "x + (y + z) = - z + (y + z)" by simp 10.243 + also have "\<dots> = y + (- z + z)" 10.244 by (rule add_left_commute) (simp_all add: vs) 10.245 - also from vs have "... = y" by simp 10.246 + also from vs have "\<dots> = y" by simp 10.247 finally show "x + (y + z) = y" . 10.248 } 10.249 qed

11.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy Tue Jul 15 16:50:09 2008 +0200 11.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Tue Jul 15 19:39:37 2008 +0200 11.3 @@ -5,7 +5,9 @@ 11.4 11.5 header {* Zorn's Lemma *} 11.6 11.7 -theory ZornLemma imports Zorn begin 11.8 +theory ZornLemma 11.9 +imports Zorn 11.10 +begin 11.11 11.12 text {* 11.13 Zorn's Lemmas states: if every linear ordered subset of an ordered 11.14 @@ -23,8 +25,6 @@ 11.15 and aS: "a \<in> S" 11.16 shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z" 11.17 proof (rule Zorn_Lemma2) 11.18 - txt_raw {* \footnote{See 11.19 - \url{http://isabelle.in.tum.de/library/HOL/HOL-Complex/Zorn.html}} \isanewline *} 11.20 show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" 11.21 proof 11.22 fix c assume "c \<in> chain S" 11.23 @@ -32,22 +32,22 @@ 11.24 proof cases 11.25 11.26 txt {* If @{text c} is an empty chain, then every element in 11.27 - @{text S} is an upper bound of @{text c}. *} 11.28 + @{text S} is an upper bound of @{text c}. *} 11.29 11.30 assume "c = {}" 11.31 with aS show ?thesis by fast 11.32 11.33 txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper 11.34 - bound of @{text c}, lying in @{text S}. *} 11.35 + bound of @{text c}, lying in @{text S}. *} 11.36 11.37 next 11.38 - assume c: "c \<noteq> {}" 11.39 + assume "c \<noteq> {}" 11.40 show ?thesis 11.41 proof 11.42 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast 11.43 show "\<Union>c \<in> S" 11.44 proof (rule r) 11.45 - from c show "\<exists>x. x \<in> c" by fast 11.46 + from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast 11.47 show "c \<in> chain S" by fact 11.48 qed 11.49 qed