modernized specifications and proofs;
authorwenzelm
Tue Jul 15 19:39:37 2008 +0200 (2008-07-15)
changeset 27612d3eb431db035
parent 27611 2c01c0bdb385
child 27613 0e03b957c649
modernized specifications and proofs;
tuned document;
src/HOL/Real/HahnBanach/Bounds.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/FunctionOrder.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/HahnBanach/ZornLemma.thy
     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