tuned proofs: avoid implicit prems;
authorwenzelm
Thu Jun 14 00:22:45 2007 +0200 (2007-06-14)
changeset 233781d138d6bb461
parent 23377 197b6a39592c
child 23379 d0e3f790bd73
tuned proofs: avoid implicit prems;
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/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/HahnBanach/ZornLemma.thy
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Wed Jun 13 19:14:51 2007 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Jun 14 00:22:45 2007 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4    assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
     1.5    shows "continuous V norm f"
     1.6  proof
     1.7 -  show "linearform V f" .
     1.8 +  show "linearform V f" by fact
     1.9    from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
    1.10    then show "continuous_axioms V norm f" ..
    1.11  qed
    1.12 @@ -138,7 +138,7 @@
    1.13            note y_rep
    1.14            also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
    1.15            proof (rule mult_right_mono)
    1.16 -            from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
    1.17 +            from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
    1.18              from gt have "0 < inverse \<parallel>x\<parallel>" 
    1.19                by (rule positive_imp_inverse_positive)
    1.20              thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
    1.21 @@ -164,7 +164,8 @@
    1.22    shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
    1.23  proof -
    1.24    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    1.25 -    by (unfold B_def fn_norm_def) (rule fn_norm_works)
    1.26 +    unfolding B_def fn_norm_def
    1.27 +    using `continuous V norm f` by (rule fn_norm_works)
    1.28    from this and b show ?thesis ..
    1.29  qed
    1.30  
    1.31 @@ -174,7 +175,8 @@
    1.32    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
    1.33  proof -
    1.34    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    1.35 -    by (unfold B_def fn_norm_def) (rule fn_norm_works)
    1.36 +    unfolding B_def fn_norm_def
    1.37 +    using `continuous V norm f` by (rule fn_norm_works)
    1.38    from this and b show ?thesis ..
    1.39  qed
    1.40  
    1.41 @@ -188,7 +190,8 @@
    1.42      So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
    1.43      0"}, provided the supremum exists and @{text B} is not empty. *}
    1.44    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    1.45 -    by (unfold B_def fn_norm_def) (rule fn_norm_works)
    1.46 +    unfolding B_def fn_norm_def
    1.47 +    using `continuous V norm f` by (rule fn_norm_works)
    1.48    moreover have "0 \<in> B V f" ..
    1.49    ultimately show ?thesis ..
    1.50  qed
    1.51 @@ -210,8 +213,9 @@
    1.52    also have "f 0 = 0" by rule unfold_locales
    1.53    also have "\<bar>\<dots>\<bar> = 0" by simp
    1.54    also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
    1.55 -      by (unfold B_def fn_norm_def) (rule fn_norm_ge_zero)
    1.56 -    have "0 \<le> norm x" ..
    1.57 +    unfolding B_def fn_norm_def
    1.58 +    using `continuous V norm f` by (rule fn_norm_ge_zero)
    1.59 +  from x have "0 \<le> norm x" ..
    1.60    with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
    1.61    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
    1.62  next
    1.63 @@ -223,8 +227,8 @@
    1.64      from x show "0 \<le> \<parallel>x\<parallel>" ..
    1.65      from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
    1.66        by (auto simp add: B_def real_divide_def)
    1.67 -    then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
    1.68 -      by (unfold B_def fn_norm_def) (rule fn_norm_ub)
    1.69 +    with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
    1.70 +      unfolding B_def fn_norm_def by (rule fn_norm_ub)
    1.71    qed
    1.72    finally show ?thesis .
    1.73  qed
    1.74 @@ -255,7 +259,7 @@
    1.75      note b_rep
    1.76      also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
    1.77      proof (rule mult_right_mono)
    1.78 -      have "0 < \<parallel>x\<parallel>" ..
    1.79 +      have "0 < \<parallel>x\<parallel>" using x x_neq ..
    1.80        then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
    1.81        from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
    1.82      qed
     2.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Wed Jun 13 19:14:51 2007 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Jun 14 00:22:45 2007 +0200
     2.3 @@ -82,13 +82,13 @@
     2.4    assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
     2.5    shows "graph (domain g) (funct g) = g"
     2.6  proof (unfold domain_def funct_def graph_def, auto)  (* FIXME !? *)
     2.7 -  fix a b assume "(a, b) \<in> g"
     2.8 -  show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
     2.9 -  show "\<exists>y. (a, y) \<in> g" ..
    2.10 -  show "b = (SOME y. (a, y) \<in> g)"
    2.11 +  fix a b assume g: "(a, b) \<in> g"
    2.12 +  from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
    2.13 +  from g show "\<exists>y. (a, y) \<in> g" ..
    2.14 +  from g show "b = (SOME y. (a, y) \<in> g)"
    2.15    proof (rule some_equality [symmetric])
    2.16      fix y assume "(a, y) \<in> g"
    2.17 -    show "y = b" by (rule uniq)
    2.18 +    with g show "y = b" by (rule uniq)
    2.19    qed
    2.20  qed
    2.21  
     3.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jun 13 19:14:51 2007 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jun 14 00:22:45 2007 +0200
     3.3 @@ -62,8 +62,9 @@
     3.4  proof -
     3.5    def M \<equiv> "norm_pres_extensions E p F f"
     3.6    hence M: "M = \<dots>" by (simp only:)
     3.7 -  have E: "vectorspace E" .
     3.8 -  have F: "vectorspace F" ..
     3.9 +  note E = `vectorspace E`
    3.10 +  then have F: "vectorspace F" ..
    3.11 +  note FE = `F \<unlhd> E`
    3.12    {
    3.13      fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
    3.14      have "\<Union>c \<in> M"
    3.15 @@ -80,9 +81,9 @@
    3.16        qed
    3.17        moreover from M cM a have "linearform ?H ?h"
    3.18          by (rule sup_lf)
    3.19 -      moreover from a M cM ex have "?H \<unlhd> E"
    3.20 +      moreover from a M cM ex FE E have "?H \<unlhd> E"
    3.21          by (rule sup_subE)
    3.22 -      moreover from a M cM ex have "F \<unlhd> ?H"
    3.23 +      moreover from a M cM ex FE have "F \<unlhd> ?H"
    3.24          by (rule sup_supF)
    3.25        moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h"
    3.26          by (rule sup_ext)
    3.27 @@ -102,14 +103,14 @@
    3.28        -- {* We show that @{text M} is non-empty: *}
    3.29      show "graph F f \<in> M"
    3.30      proof (unfold M_def, rule norm_pres_extensionI2)
    3.31 -      show "linearform F f" .
    3.32 -      show "F \<unlhd> E" .
    3.33 +      show "linearform F f" by fact
    3.34 +      show "F \<unlhd> E" by fact
    3.35        from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl)
    3.36        show "graph F f \<subseteq> graph F f" ..
    3.37 -      show "\<forall>x\<in>F. f x \<le> p x" .
    3.38 +      show "\<forall>x\<in>F. f x \<le> p x" by fact
    3.39      qed
    3.40    qed
    3.41 -  then obtain g where gM: "g \<in> M" and "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
    3.42 +  then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
    3.43      by blast
    3.44    from gM [unfolded M_def] obtain H h where
    3.45        g_rep: "g = graph H h"
    3.46 @@ -120,7 +121,7 @@
    3.47        -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *}
    3.48        -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
    3.49        -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
    3.50 -  from HE have H: "vectorspace H"
    3.51 +  from HE E have H: "vectorspace H"
    3.52      by (rule subspace.vectorspace)
    3.53  
    3.54    have HE_eq: "H = E"
    3.55 @@ -139,7 +140,7 @@
    3.56          proof
    3.57            assume "x' = 0"
    3.58            with H have "x' \<in> H" by (simp only: vectorspace.zero)
    3.59 -          then show False by contradiction
    3.60 +          with `x' \<notin> H` show False by contradiction
    3.61          qed
    3.62        qed
    3.63  
    3.64 @@ -147,12 +148,12 @@
    3.65          -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *}
    3.66        have HH': "H \<unlhd> H'"
    3.67        proof (unfold H'_def)
    3.68 -        have "vectorspace (lin x')" ..
    3.69 +        from x'E have "vectorspace (lin x')" ..
    3.70          with H show "H \<unlhd> H + lin x'" ..
    3.71        qed
    3.72  
    3.73        obtain xi where
    3.74 -        "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
    3.75 +        xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
    3.76            \<and> xi \<le> p (y + x') - h y"
    3.77          -- {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *}
    3.78          -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
    3.79 @@ -178,7 +179,7 @@
    3.80            finally have "h v - h u \<le> p (v + x') + p (u + x')" .
    3.81            then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp
    3.82          qed
    3.83 -        then show ?thesis ..
    3.84 +        then show thesis by (blast intro: that)
    3.85        qed
    3.86  
    3.87        def h' \<equiv> "\<lambda>x. let (y, a) =
    3.88 @@ -193,8 +194,8 @@
    3.89            have  "graph H h \<subseteq> graph H' h'"
    3.90            proof (rule graph_extI)
    3.91              fix t assume t: "t \<in> H"
    3.92 -            have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
    3.93 -              by (rule decomp_H'_H)
    3.94 +            from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
    3.95 +	      using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` by (rule decomp_H'_H)
    3.96              with h'_def show "h t = h' t" by (simp add: Let_def)
    3.97            next
    3.98              from HH' show "H \<subseteq> H'" ..
    3.99 @@ -216,7 +217,7 @@
   3.100              hence "(x', h' x') \<in> graph H' h'" ..
   3.101              with eq have "(x', h' x') \<in> graph H h" by (simp only:)
   3.102              hence "x' \<in> H" ..
   3.103 -            thus False by contradiction
   3.104 +            with `x' \<notin> H` show False by contradiction
   3.105            qed
   3.106            with g_rep show ?thesis by simp
   3.107          qed
   3.108 @@ -226,15 +227,17 @@
   3.109        proof (unfold M_def)
   3.110          show "graph H' h' \<in> norm_pres_extensions E p F f"
   3.111          proof (rule norm_pres_extensionI2)
   3.112 -          show "linearform H' h'" by (rule h'_lf)
   3.113 +          show "linearform H' h'"
   3.114 +	    using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E
   3.115 +	    by (rule h'_lf)
   3.116            show "H' \<unlhd> E"
   3.117 -          proof (unfold H'_def, rule)
   3.118 -            show "H \<unlhd> E" .
   3.119 -            show "vectorspace E" .
   3.120 +	  unfolding H'_def
   3.121 +          proof
   3.122 +            show "H \<unlhd> E" by fact
   3.123 +            show "vectorspace E" by fact
   3.124              from x'E show "lin x' \<unlhd> E" ..
   3.125            qed
   3.126 -          have "F \<unlhd> H" .
   3.127 -          from H this HH' show FH': "F \<unlhd> H'"
   3.128 +          from H `F \<unlhd> H` HH' show FH': "F \<unlhd> H'"
   3.129              by (rule vectorspace.subspace_trans)
   3.130            show "graph F f \<subseteq> graph H' h'"
   3.131            proof (rule graph_extI)
   3.132 @@ -245,9 +248,12 @@
   3.133                by (simp add: Let_def)
   3.134              also have "(x, 0) =
   3.135                  (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
   3.136 +	    using E HE
   3.137              proof (rule decomp_H'_H [symmetric])
   3.138                from FH x show "x \<in> H" ..
   3.139                from x' show "x' \<noteq> 0" .
   3.140 +	      show "x' \<notin> H" by fact
   3.141 +	      show "x' \<in> E" by fact
   3.142              qed
   3.143              also have
   3.144                "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
   3.145 @@ -256,14 +262,17 @@
   3.146            next
   3.147              from FH' show "F \<subseteq> H'" ..
   3.148            qed
   3.149 -          show "\<forall>x \<in> H'. h' x \<le> p x" by (rule h'_norm_pres)
   3.150 +          show "\<forall>x \<in> H'. h' x \<le> p x"
   3.151 +	    using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE
   3.152 +	      `seminorm E p` linearform and hp xi
   3.153 +	    by (rule h'_norm_pres)
   3.154          qed
   3.155        qed
   3.156        ultimately show ?thesis ..
   3.157      qed
   3.158      hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
   3.159        -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *}
   3.160 -    then show "H = E" by contradiction
   3.161 +    with gx show "H = E" by contradiction
   3.162    qed
   3.163  
   3.164    from HE_eq and linearform have "linearform E h"
   3.165 @@ -303,19 +312,24 @@
   3.166      \<and> (\<forall>x \<in> F. g x = f x)
   3.167      \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
   3.168  proof -
   3.169 -  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x)
   3.170 -    \<and> (\<forall>x \<in> E. g x \<le> p x)"
   3.171 +  note E = `vectorspace E`
   3.172 +  note FE = `subspace F E`
   3.173 +  note sn = `seminorm E p`
   3.174 +  note lf = `linearform F f`
   3.175 +  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)"
   3.176 +  using E FE sn lf
   3.177    proof (rule HahnBanach)
   3.178      show "\<forall>x \<in> F. f x \<le> p x"
   3.179 -      by (rule abs_ineq_iff [THEN iffD1])
   3.180 +      using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
   3.181    qed
   3.182 -  then obtain g where * : "linearform E g"  "\<forall>x \<in> F. g x = f x"
   3.183 -      and "\<forall>x \<in> E. g x \<le> p x" by blast
   3.184 +  then obtain g where lg: "linearform E g" and *: "\<forall>x \<in> F. g x = f x"
   3.185 +      and **: "\<forall>x \<in> E. g x \<le> p x" by blast
   3.186    have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
   3.187 +  using _ E sn lg **
   3.188    proof (rule abs_ineq_iff [THEN iffD2])
   3.189      show "E \<unlhd> E" ..
   3.190    qed
   3.191 -  with * show ?thesis by blast
   3.192 +  with lg * show ?thesis by blast
   3.193  qed
   3.194  
   3.195  
   3.196 @@ -336,14 +350,14 @@
   3.197  proof -
   3.198    have E: "vectorspace E" by unfold_locales
   3.199    have E_norm: "normed_vectorspace E norm" by rule unfold_locales
   3.200 -  have FE: "F \<unlhd> E" .
   3.201 +  note FE = `F \<unlhd> E`
   3.202    have F: "vectorspace F" by rule unfold_locales
   3.203 -  have linearform: "linearform F f" .
   3.204 +  note linearform = `linearform F f`
   3.205    have F_norm: "normed_vectorspace F norm"
   3.206 -    by (rule subspace_normed_vs)
   3.207 +    using FE E_norm by (rule subspace_normed_vs)
   3.208    have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
   3.209      by (rule normed_vectorspace.fn_norm_ge_zero
   3.210 -      [OF F_norm (* continuous.intro*), folded B_def fn_norm_def])
   3.211 +      [OF F_norm `continuous F norm f`, folded B_def fn_norm_def])
   3.212    txt {* We define a function @{text p} on @{text E} as follows:
   3.213      @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
   3.214    def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
   3.215 @@ -390,6 +404,7 @@
   3.216    have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   3.217    proof
   3.218      fix x assume "x \<in> F"
   3.219 +    from this and `continuous F norm f`
   3.220      show "\<bar>f x\<bar> \<le> p x"
   3.221        by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
   3.222          [OF F_norm, folded B_def fn_norm_def])
   3.223 @@ -452,7 +467,7 @@
   3.224        show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
   3.225        proof
   3.226  	fix x assume x: "x \<in> F"
   3.227 -	from a have "g x = f x" ..
   3.228 +	from a x have "g x = f x" ..
   3.229  	hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
   3.230  	also from g_cont
   3.231  	have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
   3.232 @@ -465,7 +480,7 @@
   3.233  	using g_cont
   3.234  	by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
   3.235      next
   3.236 -      show "continuous F norm f" .
   3.237 +      show "continuous F norm f" by fact
   3.238      qed
   3.239    qed
   3.240    with linearformE a g_cont show ?thesis by blast
     4.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Wed Jun 13 19:14:51 2007 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Jun 14 00:22:45 2007 +0200
     4.3 @@ -96,11 +96,12 @@
     4.4    includes vectorspace E
     4.5    shows "linearform H' h'"
     4.6  proof
     4.7 +  note E = `vectorspace E`
     4.8    have H': "vectorspace H'"
     4.9    proof (unfold H'_def)
    4.10 -    have "x0 \<in> E" .
    4.11 -    then have "lin x0 \<unlhd> E" ..
    4.12 -    with HE show "vectorspace (H + lin x0)" ..
    4.13 +    from `x0 \<in> E`
    4.14 +    have "lin x0 \<unlhd> E" ..
    4.15 +    with HE show "vectorspace (H + lin x0)" using E ..
    4.16    qed
    4.17    {
    4.18      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
    4.19 @@ -114,7 +115,7 @@
    4.20            and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
    4.21          by (unfold H'_def sum_def lin_def) blast
    4.22  
    4.23 -      have ya: "y1 + y2 = y \<and> a1 + a2 = a" using _ HE _ y x0
    4.24 +      have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
    4.25        proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
    4.26          from HE y1 y2 show "y1 + y2 \<in> H"
    4.27            by (rule subspace.add_closed)
    4.28 @@ -126,7 +127,7 @@
    4.29          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
    4.30        qed
    4.31  
    4.32 -      from h'_def x1x2 _ HE y x0
    4.33 +      from h'_def x1x2 E HE y x0
    4.34        have "h' (x1 + x2) = h y + a * xi"
    4.35          by (rule h'_definite)
    4.36        also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
    4.37 @@ -135,10 +136,10 @@
    4.38          by simp
    4.39        also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
    4.40          by (simp add: left_distrib)
    4.41 -      also from h'_def x1_rep _ HE y1 x0
    4.42 +      also from h'_def x1_rep E HE y1 x0
    4.43        have "h y1 + a1 * xi = h' x1"
    4.44          by (rule h'_definite [symmetric])
    4.45 -      also from h'_def x2_rep _ HE y2 x0
    4.46 +      also from h'_def x2_rep E HE y2 x0
    4.47        have "h y2 + a2 * xi = h' x2"
    4.48          by (rule h'_definite [symmetric])
    4.49        finally show ?thesis .
    4.50 @@ -154,7 +155,7 @@
    4.51            and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
    4.52          by (unfold H'_def sum_def lin_def) blast
    4.53  
    4.54 -      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using _ HE _ y x0
    4.55 +      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
    4.56        proof (rule decomp_H')
    4.57          from HE y1 show "c \<cdot> y1 \<in> H"
    4.58            by (rule subspace.mult_closed)
    4.59 @@ -166,7 +167,7 @@
    4.60          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
    4.61        qed
    4.62  
    4.63 -      from h'_def cx1_rep _ HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
    4.64 +      from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
    4.65          by (rule h'_definite)
    4.66        also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
    4.67          by (simp only: ya)
    4.68 @@ -174,7 +175,7 @@
    4.69          by simp
    4.70        also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
    4.71          by (simp only: right_distrib)
    4.72 -      also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1"
    4.73 +      also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
    4.74          by (rule h'_definite [symmetric])
    4.75        finally show ?thesis .
    4.76      qed
    4.77 @@ -195,6 +196,8 @@
    4.78      and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
    4.79    shows "\<forall>x \<in> H'. h' x \<le> p x"
    4.80  proof
    4.81 +  note E = `vectorspace E`
    4.82 +  note HE = `subspace H E`
    4.83    fix x assume x': "x \<in> H'"
    4.84    show "h' x \<le> p x"
    4.85    proof -
    4.86 @@ -206,7 +209,7 @@
    4.87      from y have y': "y \<in> E" ..
    4.88      from y have ay: "inverse a \<cdot> y \<in> H" by simp
    4.89  
    4.90 -    from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi"
    4.91 +    from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
    4.92        by (rule h'_definite)
    4.93      also have "\<dots> \<le> p (y + a \<cdot> x0)"
    4.94      proof (rule linorder_cases)
     5.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Wed Jun 13 19:14:51 2007 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Jun 14 00:22:45 2007 +0200
     5.3 @@ -126,13 +126,13 @@
     5.4      @{text x} and @{text y} are contained in the greater
     5.5      one. \label{cases1}*}
     5.6  
     5.7 -  from cM have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
     5.8 +  from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
     5.9      (is "?case1 \<or> ?case2") ..
    5.10    then show ?thesis
    5.11    proof
    5.12      assume ?case1
    5.13 -    have "(x, h x) \<in> graph H'' h''" .
    5.14 -    also have "... \<subseteq> graph H' h'" .
    5.15 +    have "(x, h x) \<in> graph H'' h''" by fact
    5.16 +    also have "... \<subseteq> graph H' h'" by fact
    5.17      finally have xh:"(x, h x) \<in> graph H' h'" .
    5.18      then have "x \<in> H'" ..
    5.19      moreover from y_hy have "y \<in> H'" ..
    5.20 @@ -143,8 +143,8 @@
    5.21      assume ?case2
    5.22      from x_hx have "x \<in> H''" ..
    5.23      moreover {
    5.24 -      from y_hy have "(y, h y) \<in> graph H' h'" .
    5.25 -      also have "\<dots> \<subseteq> graph H'' h''" .
    5.26 +      have "(y, h y) \<in> graph H' h'" by (rule y_hy)
    5.27 +      also have "\<dots> \<subseteq> graph H'' h''" by fact
    5.28        finally have "(y, h y) \<in> graph H'' h''" .
    5.29      } then have "y \<in> H''" ..
    5.30      moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
    5.31 @@ -402,7 +402,7 @@
    5.32    includes subspace H E + vectorspace E + seminorm E p + linearform H h
    5.33    shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
    5.34  proof
    5.35 -  have H: "vectorspace H" ..
    5.36 +  have H: "vectorspace H" using `vectorspace E` ..
    5.37    {
    5.38      assume l: ?L
    5.39      show ?R
    5.40 @@ -419,12 +419,13 @@
    5.41        fix x assume x: "x \<in> H"
    5.42        show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
    5.43          by arith
    5.44 -      have "linearform H h" .
    5.45 -      from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric])
    5.46 +      from `linearform H h` and H x
    5.47 +      have "- h x = h (- x)" by (rule linearform.neg [symmetric])
    5.48        also
    5.49        from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
    5.50        with r have "h (- x) \<le> p (- x)" ..
    5.51        also have "\<dots> = p x"
    5.52 +	using `seminorm E p` `vectorspace E`
    5.53        proof (rule seminorm.minus)
    5.54          from x show "x \<in> E" ..
    5.55        qed
     6.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Wed Jun 13 19:14:51 2007 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Jun 14 00:22:45 2007 +0200
     6.3 @@ -36,7 +36,7 @@
     6.4    assume x: "x \<in> V" and y: "y \<in> V"
     6.5    hence "x - y = x + - y" by (rule diff_eq1)
     6.6    also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
     6.7 -  also from _ y have "f (- y) = - f y" by (rule neg)
     6.8 +  also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
     6.9    finally show ?thesis by simp
    6.10  qed
    6.11  
    6.12 @@ -47,7 +47,7 @@
    6.13    shows "f 0 = 0"
    6.14  proof -
    6.15    have "f 0 = f (0 - 0)" by simp
    6.16 -  also have "\<dots> = f 0 - f 0" by (rule diff) simp_all
    6.17 +  also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
    6.18    also have "\<dots> = 0" by simp
    6.19    finally show ?thesis .
    6.20  qed
     7.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Jun 13 19:14:51 2007 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Jun 14 00:22:45 2007 +0200
     7.3 @@ -58,7 +58,7 @@
     7.4    have "U \<noteq> {}" by (rule U_V.non_empty)
     7.5    then obtain x where x: "x \<in> U" by blast
     7.6    hence "x \<in> V" .. hence "0 = x - x" by simp
     7.7 -  also have "... \<in> U" by (rule U_V.diff_closed)
     7.8 +  also from `vectorspace V` x x have "... \<in> U" by (rule U_V.diff_closed)
     7.9    finally show ?thesis .
    7.10  qed
    7.11  
    7.12 @@ -198,8 +198,14 @@
    7.13  text {* Any linear closure is a vector space. *}
    7.14  
    7.15  lemma (in vectorspace) lin_vectorspace [intro]:
    7.16 -    "x \<in> V \<Longrightarrow> vectorspace (lin x)"
    7.17 -  by (rule subspace.vectorspace) (rule lin_subspace)
    7.18 +  assumes "x \<in> V"
    7.19 +  shows "vectorspace (lin x)"
    7.20 +proof -
    7.21 +  from `x \<in> V` have "subspace (lin x) V"
    7.22 +    by (rule lin_subspace)
    7.23 +  from this and `vectorspace V` show ?thesis
    7.24 +    by (rule subspace.vectorspace)
    7.25 +qed
    7.26  
    7.27  
    7.28  subsection {* Sum of two vectorspaces *}
    7.29 @@ -253,19 +259,17 @@
    7.30  proof
    7.31    have "0 \<in> U + V"
    7.32    proof
    7.33 -    show "0 \<in> U" ..
    7.34 -    show "0 \<in> V" ..
    7.35 +    show "0 \<in> U" using `vectorspace E` ..
    7.36 +    show "0 \<in> V" using `vectorspace E` ..
    7.37      show "(0::'a) = 0 + 0" by simp
    7.38    qed
    7.39    thus "U + V \<noteq> {}" by blast
    7.40    show "U + V \<subseteq> E"
    7.41    proof
    7.42      fix x assume "x \<in> U + V"
    7.43 -    then obtain u v where x: "x = u + v" and
    7.44 -      u: "u \<in> U" and v: "v \<in> V" ..
    7.45 -    have "U \<unlhd> E" . with u have "u \<in> E" ..
    7.46 -    moreover have "V \<unlhd> E" . with v have "v \<in> E" ..
    7.47 -    ultimately show "x \<in> E" using x by simp
    7.48 +    then obtain u v where "x = u + v" and
    7.49 +      "u \<in> U" and "v \<in> V" ..
    7.50 +    then show "x \<in> E" by simp
    7.51    qed
    7.52    fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
    7.53    show "x + y \<in> U + V"
    7.54 @@ -314,8 +318,10 @@
    7.55      and sum: "u1 + v1 = u2 + v2"
    7.56    shows "u1 = u2 \<and> v1 = v2"
    7.57  proof
    7.58 -  have U: "vectorspace U" by (rule subspace.vectorspace)
    7.59 -  have V: "vectorspace V" by (rule subspace.vectorspace)
    7.60 +  have U: "vectorspace U"
    7.61 +    using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
    7.62 +  have V: "vectorspace V"
    7.63 +    using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
    7.64    from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
    7.65      by (simp add: add_diff_swap)
    7.66    from u1 u2 have u: "u1 - u2 \<in> U"
    7.67 @@ -327,15 +333,15 @@
    7.68  
    7.69    show "u1 = u2"
    7.70    proof (rule add_minus_eq)
    7.71 -    show "u1 \<in> E" ..
    7.72 -    show "u2 \<in> E" ..
    7.73 -    from u u' and direct show "u1 - u2 = 0" by force
    7.74 +    from u1 show "u1 \<in> E" ..
    7.75 +    from u2 show "u2 \<in> E" ..
    7.76 +    from u u' and direct show "u1 - u2 = 0" by blast
    7.77    qed
    7.78    show "v1 = v2"
    7.79    proof (rule add_minus_eq [symmetric])
    7.80 -    show "v1 \<in> E" ..
    7.81 -    show "v2 \<in> E" ..
    7.82 -    from v v' and direct show "v2 - v1 = 0" by force
    7.83 +    from v1 show "v1 \<in> E" ..
    7.84 +    from v2 show "v2 \<in> E" ..
    7.85 +    from v v' and direct show "v2 - v1 = 0" by blast
    7.86    qed
    7.87  qed
    7.88  
    7.89 @@ -375,19 +381,19 @@
    7.90            from x have "x \<in> H" ..
    7.91            with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
    7.92            with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
    7.93 -          thus ?thesis by contradiction
    7.94 +          with `x' \<notin> H` show ?thesis by contradiction
    7.95          qed
    7.96          thus "x \<in> {0}" ..
    7.97        qed
    7.98        show "{0} \<subseteq> H \<inter> lin x'"
    7.99        proof -
   7.100 -        have "0 \<in> H" ..
   7.101 -        moreover have "0 \<in> lin x'" ..
   7.102 +        have "0 \<in> H" using `vectorspace E` ..
   7.103 +        moreover have "0 \<in> lin x'" using `x' \<in> E` ..
   7.104          ultimately show ?thesis by blast
   7.105        qed
   7.106      qed
   7.107 -    show "lin x' \<unlhd> E" ..
   7.108 -  qed
   7.109 +    show "lin x' \<unlhd> E" using `x' \<in> E` ..
   7.110 +  qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
   7.111    thus "y1 = y2" ..
   7.112    from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
   7.113    with x' show "a1 = a2" by (simp add: mult_right_cancel)
   7.114 @@ -412,7 +418,7 @@
   7.115    proof (rule decomp_H')
   7.116      from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
   7.117      from ya show "y \<in> H" ..
   7.118 -  qed
   7.119 +  qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
   7.120    with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
   7.121  qed
   7.122  
   7.123 @@ -450,7 +456,7 @@
   7.124          from xq show "fst q \<in> H" ..
   7.125          from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
   7.126            by simp
   7.127 -      qed
   7.128 +      qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+)
   7.129        thus ?thesis by (cases p, cases q) simp
   7.130      qed
   7.131    qed
     8.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Jun 13 19:14:51 2007 +0200
     8.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Jun 14 00:22:45 2007 +0200
     8.3 @@ -89,7 +89,7 @@
     8.4  proof -
     8.5    from non_empty obtain x where x: "x \<in> V" by blast
     8.6    then have "0 = x - x" by (rule diff_self [symmetric])
     8.7 -  also from x have "... \<in> V" by (rule diff_closed)
     8.8 +  also from x x have "... \<in> V" by (rule diff_closed)
     8.9    finally show ?thesis .
    8.10  qed
    8.11  
    8.12 @@ -116,7 +116,7 @@
    8.13    assume x: "x \<in> V"
    8.14    have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
    8.15      by (simp add: real_diff_def)
    8.16 -  also have "... = a \<cdot> x + (- b) \<cdot> x"
    8.17 +  also from x have "... = a \<cdot> x + (- b) \<cdot> x"
    8.18      by (rule add_mult_distrib2)
    8.19    also from x have "... = a \<cdot> x + - (b \<cdot> x)"
    8.20      by (simp add: negate_eq1 mult_assoc2)
    8.21 @@ -138,7 +138,7 @@
    8.22    assume x: "x \<in> V"
    8.23    have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
    8.24    also have "... = (1 + - 1) \<cdot> x" by simp
    8.25 -  also have "... =  1 \<cdot> x + (- 1) \<cdot> x"
    8.26 +  also from x have "... =  1 \<cdot> x + (- 1) \<cdot> x"
    8.27      by (rule add_mult_distrib2)
    8.28    also from x have "... = x + (- 1) \<cdot> x" by simp
    8.29    also from x have "... = x + - x" by (simp add: negate_eq2a)
    8.30 @@ -260,11 +260,11 @@
    8.31    assume a: "a \<noteq> 0"
    8.32    assume x: "x \<in> V"  "x \<noteq> 0" and ax: "a \<cdot> x = 0"
    8.33    from x a have "x = (inverse a * a) \<cdot> x" by simp
    8.34 -  also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
    8.35 +  also from `x \<in> V` have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
    8.36    also from ax have "... = inverse a \<cdot> 0" by simp
    8.37    also have "... = 0" by simp
    8.38    finally have "x = 0" .
    8.39 -  thus "a = 0" by contradiction
    8.40 +  with `x \<noteq> 0` show "a = 0" by contradiction
    8.41  qed
    8.42  
    8.43  lemma (in vectorspace) mult_left_cancel:
    8.44 @@ -360,7 +360,7 @@
    8.45      and eq: "a + b = c + d"
    8.46    then have "- c + (a + b) = - c + (c + d)"
    8.47      by (simp add: add_left_cancel)
    8.48 -  also have "... = d" by (rule minus_add_cancel)
    8.49 +  also have "... = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)
    8.50    finally have eq: "- c + (a + b) = d" .
    8.51    from vs have "a - c = (- c + (a + b)) + - b"
    8.52      by (simp add: add_ac diff_eq1)
     9.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Wed Jun 13 19:14:51 2007 +0200
     9.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Thu Jun 14 00:22:45 2007 +0200
     9.3 @@ -48,6 +48,7 @@
     9.4          show "\<Union>c \<in> S"
     9.5          proof (rule r)
     9.6            from c show "\<exists>x. x \<in> c" by fast
     9.7 +	  show "c \<in> chain S" by fact
     9.8          qed
     9.9        qed
    9.10      qed