author wenzelm Thu Jun 14 00:22:45 2007 +0200 (2007-06-14) changeset 23378 1d138d6bb461 parent 23377 197b6a39592c child 23379 d0e3f790bd73
tuned proofs: avoid implicit prems;
     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.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.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"

     9.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Wed Jun 13 19:14:51 2007 +0200