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;
     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.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.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.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.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.219 -  also from vs eq have "...  = d + - b"
10.220 +  also from vs eq have "\<dots>  = d + - b"
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.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