- xsymbols for
authorbauerg
Mon Jul 17 13:58:18 2000 +0200 (2000-07-17)
changeset 9374153853af318b
parent 9373 78a11a353473
child 9375 cc0fd5226bb7
- xsymbols for
\<noteq> \<notin> \<in> \<exists> \<forall>
\<and> \<inter> \<union> \<Union>
- vector space type of {plus, minus, zero}, overload 0 in vector space
- syntax |.| and ||.||
src/HOL/Real/HahnBanach/Aux.thy
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
     1.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Sun Jul 16 21:00:32 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Mon Jul 17 13:58:18 2000 +0200
     1.3 @@ -17,22 +17,22 @@
     1.4  text_raw {* \medskip *}
     1.5  text{* Lemmas about sets. *}
     1.6  
     1.7 -lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v"
     1.8 +lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> B |] ==> x = v"
     1.9    by (fast elim: equalityE)
    1.10  
    1.11 -lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H"
    1.12 +lemma set_less_imp_diff_not_empty: "H < E ==> \<exists>x0 \<in> E. x0 \<notin> H"
    1.13   by (force simp add: psubset_eq)
    1.14  
    1.15  text_raw {* \medskip *}
    1.16  text{* Some lemmas about orders. *}
    1.17  
    1.18 -lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y" 
    1.19 +lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y" 
    1.20    by (rule order_less_le[RS iffD1, RS conjunct2])
    1.21  
    1.22  lemma le_noteq_imp_less: 
    1.23 -  "[| x <= (r::'a::order); x ~= r |] ==> x < r"
    1.24 +  "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r"
    1.25  proof -
    1.26 -  assume "x <= (r::'a::order)" and ne:"x ~= r"
    1.27 +  assume "x <= r" and ne:"x \<noteq> r"
    1.28    hence "x < r | x = r" by (simp add: order_le_less)
    1.29    with ne show ?thesis by simp
    1.30  qed
    1.31 @@ -116,10 +116,10 @@
    1.32    thus ?thesis; by simp;
    1.33  qed;
    1.34  
    1.35 -lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1"
    1.36 +lemma real_mult_inv_right1: "x \<noteq> #0 ==> x*rinv(x) = #1"
    1.37     by simp
    1.38  
    1.39 -lemma real_mult_inv_left1: "x ~= #0 ==> rinv(x)*x = #1"
    1.40 +lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1"
    1.41     by simp
    1.42  
    1.43  lemma real_le_mult_order1a: 
     2.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Sun Jul 16 21:00:32 2000 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Mon Jul 17 13:58:18 2000 +0200
     2.3 @@ -11,13 +11,13 @@
     2.4  
     2.5  constdefs
     2.6    is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
     2.7 -  "is_LowerBound A B == \<lambda>x. x:A & (ALL y:B. x <= y)"
     2.8 +  "is_LowerBound A B == \<lambda>x. x \<in> A \<and> (\<forall>y \<in> B. x <= y)"
     2.9     
    2.10    LowerBounds :: "('a::order) set => 'a set => 'a set"
    2.11    "LowerBounds A B == Collect (is_LowerBound A B)"
    2.12  
    2.13    is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
    2.14 -  "is_UpperBound A B == \<lambda>x. x:A & (ALL y:B. y <= x)"
    2.15 +  "is_UpperBound A B == \<lambda>x. x \<in> A \<and> (\<forall> y \<in> B. y <= x)"
    2.16   
    2.17    UpperBounds :: "('a::order) set => 'a set => 'a set"
    2.18    "UpperBounds A B == Collect (is_UpperBound A B)"
    2.19 @@ -70,7 +70,7 @@
    2.20  text {*
    2.21   A supremum\footnote{The definition of the supremum is based on one in
    2.22   \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}  of
    2.23 - an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of
    2.24 + an ordered set $B$ w.~r.~.~ $A$ is defined as a least upper bound of
    2.25   $B$, which lies in $A$.
    2.26  *}
    2.27     
    2.28 @@ -86,7 +86,7 @@
    2.29  (*<*)
    2.30  constdefs
    2.31    is_Inf :: "('a::order) set => 'a set => 'a => bool"
    2.32 -  "is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"
    2.33 +  "is_Inf A B x == x \<in> A \<and>  is_Greatest (LowerBounds A B) x"
    2.34  
    2.35    Inf :: "('a::order) set => 'a set => 'a"
    2.36    "Inf A B == Eps (is_Inf A B)"
    2.37 @@ -115,16 +115,16 @@
    2.38  
    2.39  text {* The supremum $B$ is an upper bound for $B$. *}
    2.40  
    2.41 -lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s"
    2.42 +lemma sup_ub: "y \<in> B ==> is_Sup A B s ==> y <= s"
    2.43    by (unfold is_Sup_def, rule isLubD2)
    2.44  
    2.45  text{* The supremum of a non-empty set $B$ is greater
    2.46  than a lower bound of $B$. *}
    2.47  
    2.48  lemma sup_ub1: 
    2.49 -  "[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s"
    2.50 +  "[| \<forall> y \<in> B. a <= y; is_Sup A B s; x \<in> B |] ==> a <= s"
    2.51  proof - 
    2.52 -  assume "ALL y:B. a <= y" "is_Sup A B s" "x:B"
    2.53 +  assume "\<forall> y \<in> B. a <= y" "is_Sup A B s" "x \<in> B"
    2.54    have "a <= x" by (rule bspec)
    2.55    also have "x <= s" by (rule sup_ub)
    2.56    finally show "a <= s" .
     3.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 16 21:00:32 2000 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Jul 17 13:58:18 2000 +0200
     3.3 @@ -18,16 +18,16 @@
     3.4  
     3.5  constdefs
     3.6    is_continuous ::
     3.7 -  "['a::{minus, plus} set, 'a => real, 'a => real] => bool" 
     3.8 +  "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool" 
     3.9    "is_continuous V norm f == 
    3.10 -    is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)"
    3.11 +    is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x)"
    3.12  
    3.13  lemma continuousI [intro]: 
    3.14 -  "[| is_linearform V f; !! x. x:V ==> abs (f x) <= c * norm x |] 
    3.15 +  "[| is_linearform V f; !! x. x \<in> V ==> |f x| <= c * norm x |] 
    3.16    ==> is_continuous V norm f"
    3.17  proof (unfold is_continuous_def, intro exI conjI ballI)
    3.18 -  assume r: "!! x. x:V ==> abs (f x) <= c * norm x" 
    3.19 -  fix x assume "x:V" show "abs (f x) <= c * norm x" by (rule r)
    3.20 +  assume r: "!! x. x \<in> V ==> |f x| <= c * norm x" 
    3.21 +  fix x assume "x \<in> V" show "|f x| <= c * norm x" by (rule r)
    3.22  qed
    3.23    
    3.24  lemma continuous_linearform [intro??]: 
    3.25 @@ -36,7 +36,7 @@
    3.26  
    3.27  lemma continuous_bounded [intro??]:
    3.28    "is_continuous V norm f 
    3.29 -  ==> EX c. ALL x:V. abs (f x) <= c * norm x"
    3.30 +  ==> \<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
    3.31    by (unfold is_continuous_def) force
    3.32  
    3.33  subsection{* The norm of a linear form *}
    3.34 @@ -59,14 +59,14 @@
    3.35  
    3.36  Thus we define the set $B$ the supremum is taken from as
    3.37  \[
    3.38 -\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
    3.39 +\{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
    3.40   \]
    3.41  *}
    3.42  
    3.43  constdefs
    3.44 -  B :: "[ 'a set, 'a => real, 'a => real ] => real set"
    3.45 +  B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
    3.46    "B V norm f == 
    3.47 -  {#0} Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}"
    3.48 +  {#0} \<union> {|f x| * rinv (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
    3.49  
    3.50  text{* $n$ is the function norm of $f$, iff 
    3.51  $n$ is the supremum of $B$. 
    3.52 @@ -74,17 +74,20 @@
    3.53  
    3.54  constdefs 
    3.55    is_function_norm :: 
    3.56 -  " ['a set, 'a => real, 'a => real] => real => bool"
    3.57 -  "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn"
    3.58 +  " ['a::{minus,plus,zero}  => real, 'a set, 'a => real] => real => bool"
    3.59 +  "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"
    3.60  
    3.61  text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
    3.62  if the supremum exists. Otherwise it is undefined. *}
    3.63  
    3.64  constdefs 
    3.65 -  function_norm :: " ['a set, 'a => real, 'a => real] => real"
    3.66 -  "function_norm V norm f == Sup UNIV (B V norm f)"
    3.67 +  function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"
    3.68 +  "function_norm f V norm == Sup UNIV (B V norm f)"
    3.69  
    3.70 -lemma B_not_empty: "#0 : B V norm f"
    3.71 +syntax   
    3.72 +  function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_")
    3.73 +
    3.74 +lemma B_not_empty: "#0 \<in> B V norm f"
    3.75    by (unfold B_def, force)
    3.76  
    3.77  text {* The following lemma states that every continuous linear form
    3.78 @@ -92,35 +95,35 @@
    3.79  
    3.80  lemma ex_fnorm [intro??]: 
    3.81    "[| is_normed_vectorspace V norm; is_continuous V norm f|]
    3.82 -     ==> is_function_norm V norm f (function_norm V norm f)" 
    3.83 +     ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
    3.84  proof (unfold function_norm_def is_function_norm_def 
    3.85    is_continuous_def Sup_def, elim conjE, rule selectI2EX)
    3.86    assume "is_normed_vectorspace V norm"
    3.87    assume "is_linearform V f" 
    3.88 -  and e: "EX c. ALL x:V. abs (f x) <= c * norm x"
    3.89 +  and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
    3.90  
    3.91    txt {* The existence of the supremum is shown using the 
    3.92    completeness of the reals. Completeness means, that
    3.93    every non-empty bounded set of reals has a 
    3.94    supremum. *}
    3.95 -  show  "EX a. is_Sup UNIV (B V norm f) a" 
    3.96 +  show  "\<exists>a. is_Sup UNIV (B V norm f) a" 
    3.97    proof (unfold is_Sup_def, rule reals_complete)
    3.98  
    3.99      txt {* First we have to show that $B$ is non-empty: *} 
   3.100  
   3.101 -    show "EX X. X : B V norm f" 
   3.102 +    show "\<exists>X. X \<in> B V norm f" 
   3.103      proof (intro exI)
   3.104 -      show "#0 : (B V norm f)" by (unfold B_def, force)
   3.105 +      show "#0 \<in> (B V norm f)" by (unfold B_def, force)
   3.106      qed
   3.107  
   3.108      txt {* Then we have to show that $B$ is bounded: *}
   3.109  
   3.110 -    from e show "EX Y. isUb UNIV (B V norm f) Y"
   3.111 +    from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
   3.112      proof
   3.113  
   3.114        txt {* We know that $f$ is bounded by some value $c$. *}  
   3.115    
   3.116 -      fix c assume a: "ALL x:V. abs (f x) <= c * norm x"
   3.117 +      fix c assume a: "\<forall>x \<in> V. |f x| <= c * norm x"
   3.118        def b == "max c #0"
   3.119  
   3.120        show "?thesis"
   3.121 @@ -141,7 +144,7 @@
   3.122  
   3.123        next
   3.124  	fix x y
   3.125 -        assume "x:V" "x ~= 00" (***
   3.126 +        assume "x \<in> V" "x \<noteq> 0" (***
   3.127  
   3.128           have ge: "#0 <= rinv (norm x)";
   3.129            by (rule real_less_imp_le, rule real_rinv_gt_zero, 
   3.130 @@ -152,11 +155,11 @@
   3.131                show "#0 < norm x"; ..;
   3.132              qed;
   3.133            qed; *** )
   3.134 -        have nz: "norm x ~= #0" 
   3.135 +        have nz: "norm x \<noteq> #0" 
   3.136            by (rule not_sym, rule lt_imp_not_eq, 
   3.137                rule normed_vs_norm_gt_zero) (***
   3.138            proof (rule not_sym);
   3.139 -            show "#0 ~= norm x"; 
   3.140 +            show "#0 \<noteq> norm x"; 
   3.141              proof (rule lt_imp_not_eq);
   3.142                show "#0 < norm x"; ..;
   3.143              qed;
   3.144 @@ -165,19 +168,19 @@
   3.145          txt {* The thesis follows by a short calculation using the 
   3.146          fact that $f$ is bounded. *}
   3.147      
   3.148 -        assume "y = abs (f x) * rinv (norm x)"
   3.149 +        assume "y = |f x| * rinv (norm x)"
   3.150          also have "... <= c * norm x * rinv (norm x)"
   3.151          proof (rule real_mult_le_le_mono2)
   3.152            show "#0 <= rinv (norm x)"
   3.153              by (rule real_less_imp_le, rule real_rinv_gt_zero1, 
   3.154                  rule normed_vs_norm_gt_zero)
   3.155 -          from a show "abs (f x) <= c * norm x" ..
   3.156 +          from a show "|f x| <= c * norm x" ..
   3.157          qed
   3.158          also have "... = c * (norm x * rinv (norm x))" 
   3.159            by (rule real_mult_assoc)
   3.160          also have "(norm x * rinv (norm x)) = (#1::real)" 
   3.161          proof (rule real_mult_inv_right1)
   3.162 -          show nz: "norm x ~= #0" 
   3.163 +          show nz: "norm x \<noteq> #0" 
   3.164              by (rule not_sym, rule lt_imp_not_eq, 
   3.165                rule normed_vs_norm_gt_zero)
   3.166          qed
   3.167 @@ -191,8 +194,8 @@
   3.168  text {* The norm of a continuous function is always $\geq 0$. *}
   3.169  
   3.170  lemma fnorm_ge_zero [intro??]: 
   3.171 -  "[| is_continuous V norm f; is_normed_vectorspace V norm|]
   3.172 -   ==> #0 <= function_norm V norm f"
   3.173 +  "[| is_continuous V norm f; is_normed_vectorspace V norm |]
   3.174 +   ==> #0 <= \<parallel>f\<parallel>V,norm"
   3.175  proof -
   3.176    assume c: "is_continuous V norm f" 
   3.177       and n: "is_normed_vectorspace V norm"
   3.178 @@ -203,14 +206,14 @@
   3.179  
   3.180    show ?thesis 
   3.181    proof (unfold function_norm_def, rule sup_ub1)
   3.182 -    show "ALL x:(B V norm f). #0 <= x" 
   3.183 +    show "\<forall>x \<in> (B V norm f). #0 <= x" 
   3.184      proof (intro ballI, unfold B_def,
   3.185             elim UnE singletonE CollectE exE conjE) 
   3.186        fix x r
   3.187 -      assume "x : V" "x ~= 00" 
   3.188 -        and r: "r = abs (f x) * rinv (norm x)"
   3.189 +      assume "x \<in> V" "x \<noteq> 0" 
   3.190 +        and r: "r = |f x| * rinv (norm x)"
   3.191  
   3.192 -      have ge: "#0 <= abs (f x)" by (simp! only: abs_ge_zero)
   3.193 +      have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
   3.194        have "#0 <= rinv (norm x)" 
   3.195          by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***
   3.196          proof (rule real_less_imp_le);
   3.197 @@ -225,13 +228,13 @@
   3.198  
   3.199      txt {* Since $f$ is continuous the function norm exists: *}
   3.200  
   3.201 -    have "is_function_norm V norm f (function_norm V norm f)" ..
   3.202 +    have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
   3.203      thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 
   3.204        by (unfold is_function_norm_def function_norm_def)
   3.205  
   3.206      txt {* $B$ is non-empty by construction: *}
   3.207  
   3.208 -    show "#0 : B V norm f" by (rule B_not_empty)
   3.209 +    show "#0 \<in> B V norm f" by (rule B_not_empty)
   3.210    qed
   3.211  qed
   3.212    
   3.213 @@ -242,13 +245,12 @@
   3.214  *}
   3.215  
   3.216  lemma norm_fx_le_norm_f_norm_x: 
   3.217 -  "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |] 
   3.218 -    ==> abs (f x) <= function_norm V norm f * norm x" 
   3.219 +  "[| is_continuous V norm f; is_normed_vectorspace V norm; x \<in> V |] 
   3.220 +    ==> |f x| <= \<parallel>f\<parallel>V,norm * norm x"
   3.221  proof - 
   3.222 -  assume "is_normed_vectorspace V norm" "x:V" 
   3.223 +  assume "is_normed_vectorspace V norm" "x \<in> V" 
   3.224    and c: "is_continuous V norm f"
   3.225    have v: "is_vectorspace V" ..
   3.226 -  assume "x:V"
   3.227  
   3.228   txt{* The proof is by case analysis on $x$. *}
   3.229   
   3.230 @@ -259,22 +261,22 @@
   3.231      from the linearity of $f$: for every linear function
   3.232      holds $f\ap \zero = 0$. *}
   3.233  
   3.234 -    assume "x = 00"
   3.235 -    have "abs (f x) = abs (f 00)" by (simp!)
   3.236 -    also from v continuous_linearform have "f 00 = #0" ..
   3.237 +    assume "x = 0"
   3.238 +    have "|f x| = |f 0|" by (simp!)
   3.239 +    also from v continuous_linearform have "f 0 = #0" ..
   3.240      also note abs_zero
   3.241 -    also have "#0 <= function_norm V norm f * norm x"
   3.242 +    also have "#0 <= \<parallel>f\<parallel>V,norm * norm x"
   3.243      proof (rule real_le_mult_order1a)
   3.244 -      show "#0 <= function_norm V norm f" ..
   3.245 +      show "#0 <= \<parallel>f\<parallel>V,norm" ..
   3.246        show "#0 <= norm x" ..
   3.247      qed
   3.248      finally 
   3.249 -    show "abs (f x) <= function_norm V norm f * norm x" .
   3.250 +    show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
   3.251  
   3.252    next
   3.253 -    assume "x ~= 00"
   3.254 +    assume "x \<noteq> 0"
   3.255      have n: "#0 <= norm x" ..
   3.256 -    have nz: "norm x ~= #0"
   3.257 +    have nz: "norm x \<noteq> #0"
   3.258      proof (rule lt_imp_not_eq [RS not_sym])
   3.259        show "#0 < norm x" ..
   3.260      qed
   3.261 @@ -282,28 +284,28 @@
   3.262      txt {* For the case $x\neq \zero$ we derive the following
   3.263      fact from the definition of the function norm:*}
   3.264  
   3.265 -    have l: "abs (f x) * rinv (norm x) <= function_norm V norm f"
   3.266 +    have l: "|f x| * rinv (norm x) <= \<parallel>f\<parallel>V,norm"
   3.267      proof (unfold function_norm_def, rule sup_ub)
   3.268        from ex_fnorm [OF _ c]
   3.269        show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
   3.270           by (simp! add: is_function_norm_def function_norm_def)
   3.271 -      show "abs (f x) * rinv (norm x) : B V norm f" 
   3.272 +      show "|f x| * rinv (norm x) \<in> B V norm f" 
   3.273          by (unfold B_def, intro UnI2 CollectI exI [of _ x]
   3.274              conjI, simp)
   3.275      qed
   3.276  
   3.277      txt {* The thesis now follows by a short calculation: *}
   3.278  
   3.279 -    have "abs (f x) = abs (f x) * (#1::real)" by (simp!)
   3.280 -    also from nz have "(#1::real) = rinv (norm x) * norm x" 
   3.281 +    have "|f x| = |f x| * #1" by (simp!)
   3.282 +    also from nz have "#1 = rinv (norm x) * norm x" 
   3.283        by (rule real_mult_inv_left1 [RS sym])
   3.284      also 
   3.285 -    have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x"
   3.286 -      by (simp! add: real_mult_assoc [of "abs (f x)"])
   3.287 -    also have "... <= function_norm V norm f * norm x" 
   3.288 +    have "|f x| * ... = |f x| * rinv (norm x) * norm x"
   3.289 +      by (simp! add: real_mult_assoc)
   3.290 +    also have "... <= \<parallel>f\<parallel>V,norm * norm x"
   3.291        by (rule real_mult_le_le_mono2 [OF n l])
   3.292      finally 
   3.293 -    show "abs (f x) <= function_norm V norm f * norm x" .
   3.294 +    show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
   3.295    qed
   3.296  qed
   3.297  
   3.298 @@ -315,13 +317,13 @@
   3.299  *}
   3.300  
   3.301  lemma fnorm_le_ub: 
   3.302 -  "[| is_normed_vectorspace V norm; is_continuous V norm f;
   3.303 -     ALL x:V. abs (f x) <= c * norm x; #0 <= c |]
   3.304 -  ==> function_norm V norm f <= c"
   3.305 +  "[| is_continuous V norm f; is_normed_vectorspace V norm; 
   3.306 +     \<forall>x \<in> V. |f x| <= c * norm x; #0 <= c |]
   3.307 +  ==> \<parallel>f\<parallel>V,norm <= c"
   3.308  proof (unfold function_norm_def)
   3.309    assume "is_normed_vectorspace V norm" 
   3.310    assume c: "is_continuous V norm f"
   3.311 -  assume fb: "ALL x:V. abs (f x) <= c * norm x"
   3.312 +  assume fb: "\<forall>x \<in> V. |f x| <= c * norm x"
   3.313           and "#0 <= c"
   3.314  
   3.315    txt {* Suppose the inequation holds for some $c\geq 0$.
   3.316 @@ -336,12 +338,12 @@
   3.317      show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 
   3.318        by (simp! add: is_function_norm_def function_norm_def) 
   3.319    
   3.320 -    txt {* $c$ is an upper bound of $B$, i.~e.~every
   3.321 +    txt {* $c$ is an upper bound of $B$, i.e. every
   3.322      $y\in B$ is less than $c$. *}
   3.323  
   3.324      show "isUb UNIV (B V norm f) c"  
   3.325      proof (intro isUbI setleI ballI)
   3.326 -      fix y assume "y: B V norm f"
   3.327 +      fix y assume "y \<in> B V norm f"
   3.328        thus le: "y <= c"
   3.329        proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
   3.330  
   3.331 @@ -356,14 +358,14 @@
   3.332  
   3.333        next
   3.334  	fix x 
   3.335 -        assume "x : V" "x ~= 00" 
   3.336 +        assume "x \<in> V" "x \<noteq> 0" 
   3.337  
   3.338          have lz: "#0 < norm x" 
   3.339            by (simp! add: normed_vs_norm_gt_zero)
   3.340            
   3.341 -        have nz: "norm x ~= #0" 
   3.342 +        have nz: "norm x \<noteq> #0" 
   3.343          proof (rule not_sym)
   3.344 -          from lz show "#0 ~= norm x"
   3.345 +          from lz show "#0 \<noteq> norm x"
   3.346              by (simp! add: order_less_imp_not_eq)
   3.347          qed
   3.348              
   3.349 @@ -372,10 +374,10 @@
   3.350  	hence rinv_gez: "#0 <= rinv (norm x)"
   3.351            by (rule real_less_imp_le)
   3.352  
   3.353 -	assume "y = abs (f x) * rinv (norm x)" 
   3.354 +	assume "y = |f x| * rinv (norm x)" 
   3.355  	also from rinv_gez have "... <= c * norm x * rinv (norm x)"
   3.356  	  proof (rule real_mult_le_le_mono2)
   3.357 -	    show "abs (f x) <= c * norm x" by (rule bspec)
   3.358 +	    show "|f x| <= c * norm x" by (rule bspec)
   3.359  	  qed
   3.360  	also have "... <= c" by (simp add: nz real_mult_assoc)
   3.361  	finally show ?thesis .
     4.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 16 21:00:32 2000 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Jul 17 13:58:18 2000 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  text{* We define the \emph{graph} of a (real) function $f$ with
     4.5  domain $F$ as the set 
     4.6  \[
     4.7 -\{(x, f\ap x). \ap x:F\}
     4.8 +\{(x, f\ap x). \ap x \in F\}
     4.9  \]
    4.10  So we are modeling partial functions by specifying the domain and 
    4.11  the mapping function. We use the term ``function'' also for its graph.
    4.12 @@ -22,18 +22,18 @@
    4.13  
    4.14  constdefs
    4.15    graph :: "['a set, 'a => real] => 'a graph "
    4.16 -  "graph F f == {(x, f x) | x. x:F}" 
    4.17 +  "graph F f == {(x, f x) | x. x \<in> F}" 
    4.18  
    4.19 -lemma graphI [intro??]: "x:F ==> (x, f x) : graph F f"
    4.20 +lemma graphI [intro??]: "x \<in> F ==> (x, f x) \<in> graph F f"
    4.21    by (unfold graph_def, intro CollectI exI) force
    4.22  
    4.23 -lemma graphI2 [intro??]: "x:F ==> EX t: (graph F f). t = (x, f x)"
    4.24 +lemma graphI2 [intro??]: "x \<in> F ==> \<exists>t\<in> (graph F f). t = (x, f x)"
    4.25    by (unfold graph_def, force)
    4.26  
    4.27 -lemma graphD1 [intro??]: "(x, y): graph F f ==> x:F"
    4.28 +lemma graphD1 [intro??]: "(x, y) \<in> graph F f ==> x \<in> F"
    4.29    by (unfold graph_def, elim CollectE exE) force
    4.30  
    4.31 -lemma graphD2 [intro??]: "(x, y): graph H h ==> y = h x"
    4.32 +lemma graphD2 [intro??]: "(x, y) \<in> graph H h ==> y = h x"
    4.33    by (unfold graph_def, elim CollectE exE) force 
    4.34  
    4.35  subsection {* Functions ordered by domain extension *}
    4.36 @@ -42,12 +42,12 @@
    4.37  $h$ is a subset of the graph of $h'$.*}
    4.38  
    4.39  lemma graph_extI: 
    4.40 -  "[| !! x. x: H ==> h x = h' x; H <= H'|]
    4.41 +  "[| !! x. x \<in> H ==> h x = h' x; H <= H'|]
    4.42    ==> graph H h <= graph H' h'"
    4.43    by (unfold graph_def, force)
    4.44  
    4.45  lemma graph_extD1 [intro??]: 
    4.46 -  "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x"
    4.47 +  "[| graph H h <= graph H' h'; x \<in> H |] ==> h x = h' x"
    4.48    by (unfold graph_def, force)
    4.49  
    4.50  lemma graph_extD2 [intro??]: 
    4.51 @@ -61,10 +61,10 @@
    4.52  
    4.53  constdefs
    4.54    domain :: "'a graph => 'a set" 
    4.55 -  "domain g == {x. EX y. (x, y):g}"
    4.56 +  "domain g == {x. \<exists>y. (x, y) \<in> g}"
    4.57  
    4.58    funct :: "'a graph => ('a => real)"
    4.59 -  "funct g == \<lambda>x. (SOME y. (x, y):g)"
    4.60 +  "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
    4.61  
    4.62  (*text{*  The equations 
    4.63  \begin{matharray}
    4.64 @@ -78,16 +78,16 @@
    4.65  if the relation induced by $g$ is unique. *}
    4.66  
    4.67  lemma graph_domain_funct: 
    4.68 -  "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) 
    4.69 +  "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y) 
    4.70    ==> graph (domain g) (funct g) = g"
    4.71  proof (unfold domain_def funct_def graph_def, auto)
    4.72 -  fix a b assume "(a, b) : g"
    4.73 -  show "(a, SOME y. (a, y) : g) : g" by (rule selectI2)
    4.74 -  show "EX y. (a, y) : g" ..
    4.75 -  assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y"
    4.76 -  show "b = (SOME y. (a, y) : g)"
    4.77 +  fix a b assume "(a, b) \<in> g"
    4.78 +  show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule selectI2)
    4.79 +  show "\<exists>y. (a, y) \<in> g" ..
    4.80 +  assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
    4.81 +  show "b = (SOME y. (a, y) \<in> g)"
    4.82    proof (rule select_equality [RS sym])
    4.83 -    fix y assume "(a, y):g" show "y = b" by (rule uniq)
    4.84 +    fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
    4.85    qed
    4.86  qed
    4.87  
    4.88 @@ -102,40 +102,40 @@
    4.89  
    4.90  constdefs
    4.91    norm_pres_extensions :: 
    4.92 -    "['a::{minus, plus} set, 'a  => real, 'a set, 'a => real] 
    4.93 +    "['a::{plus, minus, zero} set, 'a  => real, 'a set, 'a => real] 
    4.94      => 'a graph set"
    4.95      "norm_pres_extensions E p F f 
    4.96 -    == {g. EX H h. graph H h = g 
    4.97 -                & is_linearform H h 
    4.98 -                & is_subspace H E
    4.99 -                & is_subspace F H
   4.100 -                & graph F f <= graph H h
   4.101 -                & (ALL x:H. h x <= p x)}"
   4.102 +    == {g. \<exists>H h. graph H h = g 
   4.103 +                \<and> is_linearform H h 
   4.104 +                \<and> is_subspace H E
   4.105 +                \<and> is_subspace F H
   4.106 +                \<and> graph F f <= graph H h
   4.107 +                \<and> (\<forall>x \<in> H. h x <= p x)}"
   4.108                         
   4.109  lemma norm_pres_extension_D:  
   4.110 -  "g : norm_pres_extensions E p F f
   4.111 -  ==> EX H h. graph H h = g 
   4.112 -            & is_linearform H h 
   4.113 -            & is_subspace H E
   4.114 -            & is_subspace F H
   4.115 -            & graph F f <= graph H h
   4.116 -            & (ALL x:H. h x <= p x)"
   4.117 +  "g \<in> norm_pres_extensions E p F f
   4.118 +  ==> \<exists>H h. graph H h = g 
   4.119 +            \<and> is_linearform H h 
   4.120 +            \<and> is_subspace H E
   4.121 +            \<and> is_subspace F H
   4.122 +            \<and> graph F f <= graph H h
   4.123 +            \<and> (\<forall>x \<in> H. h x <= p x)"
   4.124    by (unfold norm_pres_extensions_def) force
   4.125  
   4.126  lemma norm_pres_extensionI2 [intro]:  
   4.127    "[| is_linearform H h; is_subspace H E; is_subspace F H;
   4.128 -  graph F f <= graph H h; ALL x:H. h x <= p x |]
   4.129 -  ==> (graph H h : norm_pres_extensions E p F f)"
   4.130 +  graph F f <= graph H h; \<forall>x \<in> H. h x <= p x |]
   4.131 +  ==> (graph H h \<in> norm_pres_extensions E p F f)"
   4.132   by (unfold norm_pres_extensions_def) force
   4.133  
   4.134  lemma norm_pres_extensionI [intro]:  
   4.135 -  "EX H h. graph H h = g 
   4.136 -         & is_linearform H h    
   4.137 -         & is_subspace H E
   4.138 -         & is_subspace F H
   4.139 -         & graph F f <= graph H h
   4.140 -         & (ALL x:H. h x <= p x)
   4.141 -  ==> g: norm_pres_extensions E p F f"
   4.142 +  "\<exists>H h. graph H h = g 
   4.143 +         \<and> is_linearform H h    
   4.144 +         \<and> is_subspace H E
   4.145 +         \<and> is_subspace F H
   4.146 +         \<and> graph F f <= graph H h
   4.147 +         \<and> (\<forall>x \<in> H. h x <= p x)
   4.148 +  ==> g\<in> norm_pres_extensions E p F f"
   4.149    by (unfold norm_pres_extensions_def) force
   4.150  
   4.151  end
   4.152 \ No newline at end of file
     5.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun Jul 16 21:00:32 2000 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Jul 17 13:58:18 2000 +0200
     5.3 @@ -1,123 +1,182 @@
     5.4 -theory HahnBanach = HahnBanachLemmas: text_raw {* \smallskip\\ *} (* from ~/Pub/TYPES99/HB/HahnBanach.thy *)
     5.5 +(*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
     5.6 +    ID:         $Id$
     5.7 +    Author:     Gertrud Bauer, TU Munich
     5.8 +*)
     5.9 +
    5.10 +header {* The Hahn-Banach Theorem *}
    5.11 +
    5.12 +theory HahnBanach = HahnBanachLemmas: 
    5.13 +
    5.14 +text {*
    5.15 +  We present the proof of two different versions of the Hahn-Banach 
    5.16 +  Theorem, closely following \cite[\S36]{Heuser:1986}.
    5.17 +*}
    5.18 +
    5.19 +subsection {* The Hahn-Banach Theorem for vector spaces *}
    5.20 +
    5.21 +text {*
    5.22 +{\bf Hahn-Banach Theorem.}\quad
    5.23 +  Let $F$ be a subspace of a real vector space $E$, let $p$ be a semi-norm on
    5.24 +  $E$, and $f$ be a linear form defined on $F$ such that $f$ is bounded by
    5.25 +  $p$, i.e. $\All {x\in F} f\ap x \leq p\ap x$.  Then $f$ can be extended to
    5.26 +  a linear form $h$ on $E$ such that $h$ is norm-preserving, i.e. $h$ is also
    5.27 +  bounded by $p$.
    5.28 +
    5.29 +\bigskip
    5.30 +{\bf Proof Sketch.}
    5.31 +\begin{enumerate}
    5.32 +\item Define $M$ as the set of norm-preserving extensions of $f$ to subspaces
    5.33 +  of $E$. The linear forms in $M$ are ordered by domain extension.
    5.34 +\item We show that every non-empty chain in $M$ has an upper bound in $M$.
    5.35 +\item With Zorn's Lemma we conclude that there is a maximal function $g$ in
    5.36 +  $M$.
    5.37 +\item The domain $H$ of $g$ is the whole space $E$, as shown by classical
    5.38 +  contradiction:
    5.39 +\begin{itemize}
    5.40 +\item Assuming $g$ is not defined on whole $E$, it can still be extended in a
    5.41 +  norm-preserving way to a super-space $H'$ of $H$.
    5.42 +\item Thus $g$ can not be maximal. Contradiction!
    5.43 +\end{itemize}
    5.44 +\end{enumerate}
    5.45 +\bigskip
    5.46 +*}
    5.47 +
    5.48 +(*
    5.49 +text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace 
    5.50 + $F$ of a real vector space $E$, such that $f$ is bounded by a seminorm 
    5.51 + $p$. 
    5.52 +
    5.53 + Then $f$ can be extended  to a linear form $h$  on $E$ that is again
    5.54 + bounded by $p$.
    5.55 +
    5.56 + \bigskip{\bf Proof Outline.}
    5.57 + First we define the set $M$ of all norm-preserving extensions of $f$.
    5.58 + We show that every chain in $M$ has an upper bound in $M$.
    5.59 + With Zorn's lemma we can conclude that $M$ has a maximal element $g$.
    5.60 + We further show by contradiction that the domain $H$ of $g$ is the whole
    5.61 + vector space $E$. 
    5.62 + If $H \neq E$, then $g$ can be extended in 
    5.63 + a norm-preserving way to a greater vector space $H_0$. 
    5.64 + So $g$ cannot be maximal in $M$.
    5.65 + \bigskip
    5.66 +*}
    5.67 +*)
    5.68  
    5.69  theorem HahnBanach:
    5.70 -  "is_vectorspace E \\<Longrightarrow> is_subspace F E \\<Longrightarrow> is_seminorm E p
    5.71 -  \\<Longrightarrow> is_linearform F f \\<Longrightarrow> \\<forall>x \\<in> F. f x \\<le> p x
    5.72 -  \\<Longrightarrow> \\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x) \\<and> (\\<forall>x \\<in> E. h x \\<le> p x)"   
    5.73 +  "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
    5.74 +  is_linearform F f; \<forall>x \<in> F. f x \<le> p x |] 
    5.75 +  ==> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"   
    5.76      -- {* Let $E$ be a vector space, $F$ a subspace of $E$, $p$ a seminorm on $E$, *}
    5.77      -- {* and $f$ a linear form on $F$ such that $f$ is bounded by $p$, *}
    5.78      -- {* then $f$ can be extended to a linear form $h$ on $E$ in a norm-preserving way. \skp *}
    5.79  proof -
    5.80    assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
    5.81 -   and "is_linearform F f" "\\<forall>x \\<in> F. f x \\<le> p x"
    5.82 +   and "is_linearform F f" "\<forall>x \<in> F. f x \<le> p x"
    5.83    -- {* Assume the context of the theorem. \skp *}
    5.84    def M == "norm_pres_extensions E p F f"
    5.85    -- {* Define $M$ as the set of all norm-preserving extensions of $F$. \skp *}
    5.86    {
    5.87 -    fix c assume "c \\<in> chain M" "\\<exists>x. x \\<in> c"
    5.88 -    have "\\<Union>c \\<in> M"
    5.89 -    txt {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
    5.90 -    txt {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
    5.91 +    fix c assume "c \<in> chain M" "\<exists>x. x \<in> c"
    5.92 +    have "\<Union> c \<in> M"
    5.93 +    -- {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
    5.94 +    -- {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
    5.95      proof (unfold M_def, rule norm_pres_extensionI)
    5.96 -      show "\\<exists> H h. graph H h = \\<Union> c
    5.97 -              & is_linearform H h 
    5.98 -              & is_subspace H E 
    5.99 -              & is_subspace F H 
   5.100 -              & graph F f \\<subseteq> graph H h
   5.101 -              & (\\<forall> x \\<in> H. h x \\<le> p x)"
   5.102 +      show "\<exists>H h. graph H h = \<Union> c
   5.103 +              \<and> is_linearform H h 
   5.104 +              \<and> is_subspace H E 
   5.105 +              \<and> is_subspace F H 
   5.106 +              \<and> graph F f \<subseteq> graph H h
   5.107 +              \<and> (\<forall>x \<in> H. h x \<le> p x)"
   5.108        proof (intro exI conjI)
   5.109 -        let ?H = "domain (\\<Union> c)"
   5.110 -        let ?h = "funct (\\<Union> c)"
   5.111 +        let ?H = "domain (\<Union> c)"
   5.112 +        let ?h = "funct (\<Union> c)"
   5.113  
   5.114 -        show a: "graph ?H ?h = \\<Union> c" 
   5.115 +        show a: "graph ?H ?h = \<Union> c" 
   5.116          proof (rule graph_domain_funct)
   5.117 -          fix x y z assume "(x, y) \\<in> \\<Union> c" "(x, z) \\<in> \\<Union> c"
   5.118 +          fix x y z assume "(x, y) \<in> \<Union> c" "(x, z) \<in> \<Union> c"
   5.119            show "z = y" by (rule sup_definite)
   5.120          qed
   5.121          show "is_linearform ?H ?h" 
   5.122            by (simp! add: sup_lf a)
   5.123 -        show "is_subspace ?H E" thm sup_subE [OF _ _ _ a]
   5.124 -          by (rule sup_subE [OF _ _ _ a]) (simp !)+
   5.125 -  (*  FIXME       by (rule sup_subE, rule a) (simp!)+; *)
   5.126 +        show "is_subspace ?H E" 
   5.127 +          by (rule sup_subE, rule a) (simp!)+
   5.128          show "is_subspace F ?H" 
   5.129 -          by (rule sup_supF [OF _ _ _ a]) (simp!)+
   5.130 -  (* FIXME        by (rule sup_supF, rule a) (simp!)+ *)
   5.131 -        show "graph F f \\<subseteq> graph ?H ?h" 
   5.132 -          by (rule sup_ext [OF _ _ _ a]) (simp!)+
   5.133 -  (*  FIXME      by (rule sup_ext, rule a) (simp!)+*)
   5.134 -        show "\\<forall>x \\<in> ?H. ?h x \\<le> p x" 
   5.135 -          by (rule sup_norm_pres [OF _ _ a]) (simp!)+
   5.136 -  (* FIXME        by (rule sup_norm_pres, rule a) (simp!)+ *)
   5.137 +          by (rule sup_supF, rule a) (simp!)+
   5.138 +        show "graph F f \<subseteq> graph ?H ?h" 
   5.139 +          by (rule sup_ext, rule a) (simp!)+
   5.140 +        show "\<forall>x \<in> ?H. ?h x \<le> p x" 
   5.141 +          by (rule sup_norm_pres, rule a) (simp!)+
   5.142        qed
   5.143      qed
   5.144  
   5.145    }
   5.146 -  hence "\\<exists>g \\<in> M. \\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x" 
   5.147 -  txt {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
   5.148 +  hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x --> g = x" 
   5.149 +  -- {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
   5.150    proof (rule Zorn's_Lemma)
   5.151 -    txt {* We show that $M$ is non-empty: *}
   5.152 -    have "graph F f \\<in> norm_pres_extensions E p F f"
   5.153 +    -- {* We show that $M$ is non-empty: *}
   5.154 +    have "graph F f \<in> norm_pres_extensions E p F f"
   5.155      proof (rule norm_pres_extensionI2)
   5.156        have "is_vectorspace F" ..
   5.157        thus "is_subspace F F" ..
   5.158      qed (blast!)+ 
   5.159 -    thus "graph F f \\<in> M" by (simp!)
   5.160 +    thus "graph F f \<in> M" by (simp!)
   5.161    qed
   5.162    thus ?thesis
   5.163    proof
   5.164 -    fix g assume "g \\<in> M" "\\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x"
   5.165 +    fix g assume "g \<in> M" "\<forall>x \<in> M. g \<subseteq> x --> g = x"
   5.166      -- {* We consider such a maximal element $g \in M$. \skp *}
   5.167      show ?thesis
   5.168        obtain H h where "graph H h = g" "is_linearform H h" 
   5.169 -        "is_subspace H E" "is_subspace F H" "graph F f \\<subseteq> graph H h" 
   5.170 -        "\\<forall>x \\<in> H. h x \\<le> p x" 
   5.171 -        txt {* $g$ is a norm-preserving extension of $f$, in other words: *}
   5.172 -        txt {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
   5.173 -        txt {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
   5.174 +        "is_subspace H E" "is_subspace F H" "graph F f \<subseteq> graph H h" 
   5.175 +        "\<forall>x \<in> H. h x \<le> p x" 
   5.176 +        -- {* $g$ is a norm-preserving extension of $f$, in other words: *}
   5.177 +        -- {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
   5.178 +        -- {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
   5.179        proof -
   5.180 -        have "\\<exists> H h. graph H h = g & is_linearform H h 
   5.181 -          & is_subspace H E & is_subspace F H
   5.182 -          & graph F f \\<subseteq> graph H h
   5.183 -          & (\\<forall>x \\<in> H. h x \\<le> p x)" by (simp! add: norm_pres_extension_D)
   5.184 +        have "\<exists> H h. graph H h = g \<and> is_linearform H h 
   5.185 +          \<and> is_subspace H E \<and> is_subspace F H
   5.186 +          \<and> graph F f \<subseteq> graph H h
   5.187 +          \<and> (\<forall>x \<in> H. h x \<le> p x)" by (simp! add: norm_pres_extension_D)
   5.188          thus ?thesis by (elim exE conjE) rule
   5.189        qed
   5.190        have h: "is_vectorspace H" ..
   5.191        have "H = E"
   5.192        -- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *} 
   5.193        proof (rule classical)
   5.194 -        assume "H \\<noteq> E"
   5.195 +        assume "H \<noteq> E"
   5.196          -- {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *}
   5.197          -- {* in a norm-preserving way to a function $h'$ with the graph $g'$. \skp *}
   5.198 -        have "\\<exists>g' \\<in> M. g \\<subseteq> g' \\<and> g \\<noteq> g'" 
   5.199 -          obtain x' where "x' \\<in> E" "x' \\<notin> H" 
   5.200 -          txt {* Pick $x' \in E \setminus H$. \skp *}
   5.201 +        have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'" 
   5.202 +          obtain x' where "x' \<in> E" "x' \<notin> H" 
   5.203 +          -- {* Pick $x' \in E \setminus H$. \skp *}
   5.204            proof -
   5.205 -            have "\\<exists>x' \\<in> E. x' \\<notin> H"
   5.206 +            have "\<exists>x' \<in> E. x' \<notin> H"
   5.207              proof (rule set_less_imp_diff_not_empty)
   5.208 -              have "H \\<subseteq> E" ..
   5.209 -              thus "H \\<subset> E" ..
   5.210 +              have "H \<subseteq> E" ..
   5.211 +              thus "H \<subset> E" ..
   5.212              qed
   5.213              thus ?thesis by blast
   5.214            qed
   5.215 -          have x': "x' \\<noteq> \<zero>"
   5.216 +          have x': "x' \<noteq> 0"
   5.217            proof (rule classical)
   5.218 -            presume "x' = \<zero>"
   5.219 -            with h have "x' \\<in> H" by simp
   5.220 +            presume "x' = 0"
   5.221 +            with h have "x' \<in> H" by simp
   5.222              thus ?thesis by contradiction
   5.223            qed blast
   5.224            def H' == "H + lin x'"
   5.225            -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
   5.226            show ?thesis
   5.227 -            obtain xi where "\\<forall>y \\<in> H. - p (y + x') - h y \\<le> xi 
   5.228 -                              \\<and> xi \\<le> p (y + x') - h y" 
   5.229 -            txt {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
   5.230 -            txt {* be used to establish that $h'$ is a norm-preserving extension of $h$. \skp *}
   5.231 +            obtain xi where "\<forall>y \<in> H. - p (y + x') - h y \<le> xi 
   5.232 +                              \<and> xi \<le> p (y + x') - h y" 
   5.233 +            -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
   5.234 +            -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. 
   5.235 +               \label{ex-xi-use}\skp *}
   5.236  
   5.237              proof -
   5.238 -	      from h have "EX xi. ALL y:H. - p (y + x') - h y <= xi 
   5.239 -                              & xi <= p (y + x') - h y" 
   5.240 +	      from h have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y <= xi 
   5.241 +                              \<and> xi <= p (y + x') - h y" 
   5.242                proof (rule ex_xi)
   5.243 -                fix u v assume "u:H" "v:H"
   5.244 +                fix u v assume "u \<in> H" "v \<in> H"
   5.245                  from h have "h v - h u = h (v - u)"
   5.246                    by (simp! add: linearform_diff)
   5.247                  also have "... <= p (v - u)"
   5.248 @@ -138,25 +197,25 @@
   5.249                thus ?thesis by rule rule
   5.250              qed
   5.251  
   5.252 -            def h' == "\\<lambda>x. let (y,a) = \\<epsilon>(y,a). x = y + a \<prod> x' \\<and> y \\<in> H
   5.253 +            def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H
   5.254                             in (h y) + a * xi"
   5.255              -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
   5.256              show ?thesis
   5.257              proof
   5.258 -              show "g \\<subseteq> graph H' h' \\<and> g \\<noteq> graph H' h'" 
   5.259 -              txt {* Show that $h'$ is an extension of $h$ \dots \skp *}
   5.260 -proof
   5.261 -		show "g \\<subseteq> graph H' h'"
   5.262 +              show "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'" 
   5.263 +              -- {* Show that $h'$ is an extension of $h$ \dots \skp *}
   5.264 +              proof
   5.265 +		show "g \<subseteq> graph H' h'"
   5.266  		proof -
   5.267 -		  have  "graph H h \\<subseteq> graph H' h'"
   5.268 +		  have  "graph H h \<subseteq> graph H' h'"
   5.269                    proof (rule graph_extI)
   5.270 -		    fix t assume "t \\<in> H" 
   5.271 -		    have "(SOME (y, a). t = y + a \<prod> x' & y \\<in> H)
   5.272 -                         = (t, #0)" 
   5.273 -		      by (rule decomp_H0_H [OF _ _ _ _ _ x'])
   5.274 +		    fix t assume "t \<in> H" 
   5.275 +		    have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H)
   5.276 +                         = (t, #0)"
   5.277 +		      by (rule decomp_H'_H) (assumption+, rule x');
   5.278  		    thus "h t = h' t" by (simp! add: Let_def)
   5.279  		  next
   5.280 -		    show "H \\<subseteq> H'"
   5.281 +		    show "H \<subseteq> H'"
   5.282  		    proof (rule subspace_subset)
   5.283  		      show "is_subspace H H'"
   5.284  		      proof (unfold H'_def, rule subspace_vs_sum1)
   5.285 @@ -167,33 +226,33 @@
   5.286  		  qed 
   5.287  		  thus ?thesis by (simp!)
   5.288  		qed
   5.289 -                show "g \\<noteq> graph H' h'"
   5.290 +                show "g \<noteq> graph H' h'"
   5.291  		proof -
   5.292 -		  have "graph H h \\<noteq> graph H' h'"
   5.293 +		  have "graph H h \<noteq> graph H' h'"
   5.294  		  proof
   5.295  		    assume e: "graph H h = graph H' h'"
   5.296 -		    have "x' \\<in> H'" 
   5.297 +		    have "x' \<in> H'" 
   5.298  		    proof (unfold H'_def, rule vs_sumI)
   5.299 -		      show "x' = \<zero> + x'" by (simp!)
   5.300 -		      from h show "\<zero> \\<in> H" ..
   5.301 -		      show "x' \\<in> lin x'" by (rule x_lin_x)
   5.302 +		      show "x' = 0 + x'" by (simp!)
   5.303 +		      from h show "0 \<in> H" ..
   5.304 +		      show "x' \<in> lin x'" by (rule x_lin_x)
   5.305  		    qed
   5.306 -		    hence "(x', h' x') \\<in> graph H' h'" ..
   5.307 -		    with e have "(x', h' x') \\<in> graph H h" by simp
   5.308 -		    hence "x' \\<in> H" ..
   5.309 +		    hence "(x', h' x') \<in> graph H' h'" ..
   5.310 +		    with e have "(x', h' x') \<in> graph H h" by simp
   5.311 +		    hence "x' \<in> H" ..
   5.312  		    thus False by contradiction
   5.313  		  qed
   5.314  		  thus ?thesis by (simp!)
   5.315  		qed
   5.316                qed
   5.317 -	      show "graph H' h' \\<in> M" 
   5.318 -              txt {* and $h'$ is norm-preserving. \skp *} 
   5.319 +	      show "graph H' h' \<in> M" 
   5.320 +              -- {* and $h'$ is norm-preserving. \skp *} 
   5.321                proof -
   5.322 -		have "graph H' h' \\<in> norm_pres_extensions E p F f"
   5.323 +		have "graph H' h' \<in> norm_pres_extensions E p F f"
   5.324  		proof (rule norm_pres_extensionI2)
   5.325  		  show "is_linearform H' h'"
   5.326 -		    by (rule h0_lf [OF _ _ _ _ _ _ x']) (simp!)+
   5.327 -		  show "is_subspace H' E"
   5.328 +		    by (rule h'_lf) (simp! add: x')+
   5.329 +                  show "is_subspace H' E" 
   5.330  		    by (unfold H'_def) (rule vs_sum_subspace [OF _ lin_subspace])
   5.331  		  have "is_subspace F H" .
   5.332  		  also from h lin_vs 
   5.333 @@ -201,49 +260,259 @@
   5.334  		  finally (subspace_trans [OF _ h]) 
   5.335  		  show f_h': "is_subspace F H'" .
   5.336  		
   5.337 -		  show "graph F f \\<subseteq> graph H' h'"
   5.338 +		  show "graph F f \<subseteq> graph H' h'"
   5.339  		  proof (rule graph_extI)
   5.340 -		    fix x assume "x \\<in> F"
   5.341 +		    fix x assume "x \<in> F"
   5.342  		    have "f x = h x" ..
   5.343  		    also have " ... = h x + #0 * xi" by simp
   5.344  		    also have "... = (let (y,a) = (x, #0) in h y + a * xi)"
   5.345  		      by (simp add: Let_def)
   5.346  		    also have 
   5.347 -		      "(x, #0) = (SOME (y, a). x = y + a (*) x' & y \\<in> H)"
   5.348 -		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x']) (simp!)+
   5.349 +		      "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
   5.350 +		      proof (rule decomp_H'_H [RS sym]) qed (simp! add: x')+
   5.351  		    also have 
   5.352 -		      "(let (y,a) = (SOME (y,a). x = y + a (*) x' & y \\<in> H)
   5.353 +		      "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
   5.354                          in h y + a * xi) 
   5.355                        = h' x" by (simp!)
   5.356  		    finally show "f x = h' x" .
   5.357  		  next
   5.358 -		    from f_h' show "F \\<subseteq> H'" ..
   5.359 +		    from f_h' show "F \<subseteq> H'" ..
   5.360  		  qed
   5.361  		
   5.362 -		  show "\\<forall>x \\<in> H'. h' x \\<le> p x"
   5.363 -		    by (rule h0_norm_pres [OF _ _ _ _ x'])
   5.364 +		  show "\<forall>x \<in> H'. h' x \<le> p x"
   5.365 +		    by (rule h'_norm_pres) (assumption+, rule x')
   5.366  		qed
   5.367 -		thus "graph H' h' \\<in> M" by (simp!)
   5.368 +		thus "graph H' h' \<in> M" by (simp!)
   5.369  	      qed
   5.370              qed
   5.371            qed
   5.372          qed
   5.373 -        hence "\\<not>(\\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x)" by simp
   5.374 +        hence "\<not> (\<forall>x \<in> M. g \<subseteq> x --> g = x)" by simp
   5.375          -- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}
   5.376          thus "H = E" by contradiction
   5.377        qed
   5.378 -      thus "\\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x) 
   5.379 -          \\<and> (\\<forall>x \\<in> E. h x \\<le> p x)" 
   5.380 +      thus "\<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) 
   5.381 +          \<and> (\<forall>x \<in> E. h x \<le> p x)" 
   5.382        proof (intro exI conjI)
   5.383          assume eq: "H = E"
   5.384  	from eq show "is_linearform E h" by (simp!)
   5.385 -	show "\\<forall>x \\<in> F. h x = f x" 
   5.386 +	show "\<forall>x \<in> F. h x = f x" 
   5.387  	proof (intro ballI, rule sym)
   5.388 -	  fix x assume "x \\<in> F" show "f x = h x " ..
   5.389 +	  fix x assume "x \<in> F" show "f x = h x " ..
   5.390  	qed
   5.391 -	from eq show "\\<forall>x \\<in> E. h x \\<le> p x" by (force!)
   5.392 +	from eq show "\<forall>x \<in> E. h x \<le> p x" by (force!)
   5.393        qed
   5.394      qed
   5.395    qed
   5.396 -qed text_raw {* \smallskip\\ *}
   5.397 +qed 
   5.398 +
   5.399 +
   5.400 +
   5.401 +subsection  {* Alternative formulation *}
   5.402 +
   5.403 +text {* The following alternative formulation of the Hahn-Banach
   5.404 +Theorem\label{abs-HahnBanach} uses the fact that for a real linear form
   5.405 +$f$ and a seminorm $p$ the
   5.406 +following inequations are equivalent:\footnote{This was shown in lemma
   5.407 +$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{abs-ineq-iff}).}
   5.408 +\begin{matharray}{ll}
   5.409 +\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
   5.410 +\forall x\in H.\ap h\ap x\leq p\ap x\\
   5.411 +\end{matharray}
   5.412 +*}
   5.413 +
   5.414 +theorem abs_HahnBanach:
   5.415 +  "[| is_vectorspace E; is_subspace F E; is_linearform F f; 
   5.416 +  is_seminorm E p; \<forall>x \<in> F. |f x| <= p x |]
   5.417 +  ==> \<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
   5.418 +   \<and> (\<forall>x \<in> E. |g x| <= p x)"
   5.419 +proof -
   5.420 +  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
   5.421 +    "is_linearform F f"  "\<forall>x \<in> F. |f x| <= p x"
   5.422 +  have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
   5.423 +  hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
   5.424 +              \<and> (\<forall>x \<in> E. g x <= p x)"
   5.425 +    by (simp! only: HahnBanach)
   5.426 +  thus ?thesis 
   5.427 +  proof (elim exE conjE)
   5.428 +    fix g assume "is_linearform E g" "\<forall>x \<in> F. g x = f x" 
   5.429 +                  "\<forall>x \<in> E. g x <= p x"
   5.430 +    hence "\<forall>x \<in> E. |g x| <= p x"
   5.431 +      by (simp! add: abs_ineq_iff [OF subspace_refl])
   5.432 +    thus ?thesis by (intro exI conjI)
   5.433 +  qed
   5.434 +qed
   5.435 +
   5.436 +subsection {* The Hahn-Banach Theorem for normed spaces *}
   5.437 +
   5.438 +text {* Every continuous linear form $f$ on a subspace $F$ of a
   5.439 +norm space $E$, can be extended to a continuous linear form $g$ on
   5.440 +$E$ such that $\fnorm{f} = \fnorm {g}$. *}
   5.441 +
   5.442 +theorem norm_HahnBanach:
   5.443 +  "[| is_normed_vectorspace E norm; is_subspace F E; 
   5.444 +  is_linearform F f; is_continuous F norm f |] 
   5.445 +  ==> \<exists>g. is_linearform E g
   5.446 +         \<and> is_continuous E norm g 
   5.447 +         \<and> (\<forall>x \<in> F. g x = f x) 
   5.448 +         \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
   5.449 +proof -
   5.450 +  assume e_norm: "is_normed_vectorspace E norm"
   5.451 +  assume f: "is_subspace F E" "is_linearform F f"
   5.452 +  assume f_cont: "is_continuous F norm f"
   5.453 +  have e: "is_vectorspace E" ..
   5.454 +  hence f_norm: "is_normed_vectorspace F norm" ..
   5.455 +
   5.456 +  txt{* We define a function $p$ on $E$ as follows:
   5.457 +  \begin{matharray}{l}
   5.458 +  p \: x = \fnorm f \cdot \norm x\\
   5.459 +  \end{matharray}
   5.460 +  *}
   5.461 +
   5.462 +  def p == "\<lambda>x. \<parallel>f\<parallel>F,norm * norm x"
   5.463 +  
   5.464 +  txt{* $p$ is a seminorm on $E$: *}
   5.465 +
   5.466 +  have q: "is_seminorm E p"
   5.467 +  proof
   5.468 +    fix x y a assume "x \<in> E" "y \<in> E"
   5.469 +
   5.470 +    txt{* $p$ is positive definite: *}
   5.471 +
   5.472 +    show "#0 <= p x"
   5.473 +    proof (unfold p_def, rule real_le_mult_order1a) thm fnorm_ge_zero
   5.474 +      from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
   5.475 +      show "#0 <= norm x" ..
   5.476 +    qed
   5.477 +
   5.478 +    txt{* $p$ is absolutely homogenous: *}
   5.479 +
   5.480 +    show "p (a \<cdot> x) = |a| * p x"
   5.481 +    proof - 
   5.482 +      have "p (a \<cdot> x) = \<parallel>f\<parallel>F,norm * norm (a \<cdot> x)"
   5.483 +        by (simp!)
   5.484 +      also have "norm (a \<cdot> x) = |a| * norm x" 
   5.485 +        by (rule normed_vs_norm_abs_homogenous)
   5.486 +      also have "\<parallel>f\<parallel>F,norm * ( |a| * norm x ) 
   5.487 +        = |a| * (\<parallel>f\<parallel>F,norm * norm x)"
   5.488 +        by (simp! only: real_mult_left_commute)
   5.489 +      also have "... = |a| * p x" by (simp!)
   5.490 +      finally show ?thesis .
   5.491 +    qed
   5.492 +
   5.493 +    txt{* Furthermore, $p$ is subadditive: *}
   5.494 +
   5.495 +    show "p (x + y) <= p x + p y"
   5.496 +    proof -
   5.497 +      have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)"
   5.498 +        by (simp!)
   5.499 +      also 
   5.500 +      have "... <= \<parallel>f\<parallel>F,norm * (norm x + norm y)"
   5.501 +      proof (rule real_mult_le_le_mono1a)
   5.502 +        from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
   5.503 +        show "norm (x + y) <= norm x + norm y" ..
   5.504 +      qed
   5.505 +      also have "... = \<parallel>f\<parallel>F,norm * norm x 
   5.506 +                        + \<parallel>f\<parallel>F,norm * norm y"
   5.507 +        by (simp! only: real_add_mult_distrib2)
   5.508 +      finally show ?thesis by (simp!)
   5.509 +    qed
   5.510 +  qed
   5.511 +
   5.512 +  txt{* $f$ is bounded by $p$. *} 
   5.513 +
   5.514 +  have "\<forall>x \<in> F. |f x| <= p x"
   5.515 +  proof
   5.516 +    fix x assume "x \<in> F"
   5.517 +     from f_norm show "|f x| <= p x" 
   5.518 +       by (simp! add: norm_fx_le_norm_f_norm_x)
   5.519 +  qed
   5.520 +
   5.521 +  txt{* Using the fact that $p$ is a seminorm and 
   5.522 +  $f$ is bounded by $p$ we can apply the Hahn-Banach Theorem 
   5.523 +  for real vector spaces. 
   5.524 +  So $f$ can be extended in a norm-preserving way to some function
   5.525 +  $g$ on the whole vector space $E$. *}
   5.526 +
   5.527 +  with e f q 
   5.528 +  have "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
   5.529 +            \<and> (\<forall>x \<in> E. |g x| <= p x)"
   5.530 +    by (simp! add: abs_HahnBanach)
   5.531 +
   5.532 +  thus ?thesis
   5.533 +  proof (elim exE conjE) 
   5.534 +    fix g
   5.535 +    assume "is_linearform E g" and a: "\<forall>x \<in> F. g x = f x" 
   5.536 +       and b: "\<forall>x \<in> E. |g x| <= p x"
   5.537 +
   5.538 +    show "\<exists>g. is_linearform E g 
   5.539 +            \<and> is_continuous E norm g 
   5.540 +            \<and> (\<forall>x \<in> F. g x = f x) 
   5.541 +            \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
   5.542 +    proof (intro exI conjI)
   5.543 +
   5.544 +    txt{* We furthermore have to show that 
   5.545 +    $g$ is also continuous: *}
   5.546 +
   5.547 +      show g_cont: "is_continuous E norm g"
   5.548 +      proof
   5.549 +        fix x assume "x \<in> E"
   5.550 +        with b show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
   5.551 +          by (simp add: p_def) 
   5.552 +      qed 
   5.553 +
   5.554 +      txt {* To complete the proof, we show that 
   5.555 +      $\fnorm g = \fnorm f$. \label{order_antisym} *}
   5.556 +
   5.557 +      show "\<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
   5.558 +        (is "?L = ?R")
   5.559 +      proof (rule order_antisym)
   5.560 +
   5.561 +        txt{* First we show $\fnorm g \leq \fnorm f$.  The function norm
   5.562 +        $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that
   5.563 +        \begin{matharray}{l}
   5.564 +        \All {x\in E} {|g\ap x| \leq c \cdot \norm x}
   5.565 +        \end{matharray}
   5.566 +        Furthermore holds
   5.567 +        \begin{matharray}{l}
   5.568 +        \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x}
   5.569 +        \end{matharray}
   5.570 +        *}
   5.571 + 
   5.572 +        have "\<forall>x \<in> E. |g x| <= \<parallel>f\<parallel>F,norm * norm x"
   5.573 +        proof
   5.574 +          fix x assume "x \<in> E" 
   5.575 +          show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
   5.576 +            by (simp!)
   5.577 +        qed
   5.578 +
   5.579 +        with g_cont e_norm show "?L <= ?R"
   5.580 +        proof (rule fnorm_le_ub)
   5.581 +          from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
   5.582 +        qed
   5.583 +
   5.584 +        txt{* The other direction is achieved by a similar 
   5.585 +        argument. *}
   5.586 +
   5.587 +        have "\<forall>x \<in> F. |f x| <= \<parallel>g\<parallel>E,norm * norm x"
   5.588 +        proof
   5.589 +          fix x assume "x \<in> F" 
   5.590 +          from a have "g x = f x" ..
   5.591 +          hence "|f x| = |g x|" by simp
   5.592 +          also from g_cont
   5.593 +          have "... <= \<parallel>g\<parallel>E,norm * norm x"
   5.594 +          proof (rule norm_fx_le_norm_f_norm_x)
   5.595 +            show "x \<in> E" ..
   5.596 +          qed
   5.597 +          finally show "|f x| <= \<parallel>g\<parallel>E,norm * norm x" .
   5.598 +        qed 
   5.599 +        thus "?R <= ?L" 
   5.600 +        proof (rule fnorm_le_ub [OF f_cont f_norm])
   5.601 +          from g_cont show "#0 <= \<parallel>g\<parallel>E,norm" ..
   5.602 +        qed
   5.603 +      qed
   5.604 +    qed
   5.605 +  qed
   5.606 +qed
   5.607 +
   5.608  end
   5.609 \ No newline at end of file
     6.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Sun Jul 16 21:00:32 2000 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Jul 17 13:58:18 2000 +0200
     6.3 @@ -35,51 +35,51 @@
     6.4  \end{matharray} *};
     6.5  
     6.6  lemma ex_xi: 
     6.7 -  "[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
     6.8 -  ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y"; 
     6.9 +  "[| is_vectorspace F; !! u v. [| u \<in> F; v \<in> F |] ==> a u <= b v |]
    6.10 +  ==> \<exists>xi::real. \<forall>y \<in> F. a y <= xi \<and> xi <= b y"; 
    6.11  proof -;
    6.12    assume vs: "is_vectorspace F";
    6.13 -  assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
    6.14 +  assume r: "(!! u v. [| u \<in> F; v \<in> F |] ==> a u <= (b v::real))";
    6.15  
    6.16    txt {* From the completeness of the reals follows:
    6.17    The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if
    6.18    it is non-empty and has an upper bound. *};
    6.19  
    6.20 -  let ?S = "{a u :: real | u. u:F}";
    6.21 +  let ?S = "{a u :: real | u. u \<in> F}";
    6.22  
    6.23 -  have "EX xi. isLub UNIV ?S xi";  
    6.24 +  have "\<exists>xi. isLub UNIV ?S xi";  
    6.25    proof (rule reals_complete);
    6.26    
    6.27      txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
    6.28  
    6.29 -    from vs; have "a \<zero> : ?S"; by force;
    6.30 -    thus "EX X. X : ?S"; ..;
    6.31 +    from vs; have "a 0 \<in> ?S"; by force;
    6.32 +    thus "\<exists>X. X \<in> ?S"; ..;
    6.33  
    6.34      txt {* $b\ap \zero$ is an upper bound of $S$: *};
    6.35  
    6.36 -    show "EX Y. isUb UNIV ?S Y"; 
    6.37 +    show "\<exists>Y. isUb UNIV ?S Y"; 
    6.38      proof; 
    6.39 -      show "isUb UNIV ?S (b \<zero>)";
    6.40 +      show "isUb UNIV ?S (b 0)";
    6.41        proof (intro isUbI setleI ballI);
    6.42 -        show "b \<zero> : UNIV"; ..;
    6.43 +        show "b 0 \<in> UNIV"; ..;
    6.44        next;
    6.45  
    6.46          txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
    6.47  
    6.48 -        fix y; assume y: "y : ?S"; 
    6.49 -        from y; have "EX u:F. y = a u"; by fast;
    6.50 -        thus "y <= b \<zero>"; 
    6.51 +        fix y; assume y: "y \<in> ?S"; 
    6.52 +        from y; have "\<exists>u \<in> F. y = a u"; by fast;
    6.53 +        thus "y <= b 0"; 
    6.54          proof;
    6.55 -          fix u; assume "u:F"; 
    6.56 +          fix u; assume "u \<in> F"; 
    6.57            assume "y = a u";
    6.58 -          also; have "a u <= b \<zero>"; by (rule r) (simp!)+;
    6.59 +          also; have "a u <= b 0"; by (rule r) (simp!)+;
    6.60            finally; show ?thesis; .;
    6.61          qed;
    6.62        qed;
    6.63      qed;
    6.64    qed;
    6.65  
    6.66 -  thus "EX xi. ALL y:F. a y <= xi & xi <= b y"; 
    6.67 +  thus "\<exists>xi. \<forall>y \<in> F. a y <= xi \<and> xi <= b y"; 
    6.68    proof (elim exE);
    6.69      fix xi; assume "isLub UNIV ?S xi"; 
    6.70      show ?thesis;
    6.71 @@ -87,7 +87,7 @@
    6.72     
    6.73        txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
    6.74       
    6.75 -      fix y; assume y: "y:F";
    6.76 +      fix y; assume y: "y \<in> F";
    6.77        show "a y <= xi";    
    6.78        proof (rule isUbD);  
    6.79          show "isUb UNIV ?S xi"; ..;
    6.80 @@ -96,17 +96,17 @@
    6.81  
    6.82        txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
    6.83  
    6.84 -      fix y; assume "y:F";
    6.85 +      fix y; assume "y \<in> F";
    6.86        show "xi <= b y";  
    6.87        proof (intro isLub_le_isUb isUbI setleI);
    6.88 -        show "b y : UNIV"; ..;
    6.89 -        show "ALL ya : ?S. ya <= b y"; 
    6.90 +        show "b y \<in> UNIV"; ..;
    6.91 +        show "\<forall>ya \<in> ?S. ya <= b y"; 
    6.92          proof;
    6.93 -          fix au; assume au: "au : ?S ";
    6.94 -          hence "EX u:F. au = a u"; by fast;
    6.95 +          fix au; assume au: "au \<in> ?S ";
    6.96 +          hence "\<exists>u \<in> F. au = a u"; by fast;
    6.97            thus "au <= b y";
    6.98            proof;
    6.99 -            fix u; assume "u:F"; assume "au = a u";  
   6.100 +            fix u; assume "u \<in> F"; assume "au = a u";  
   6.101              also; have "... <= b y"; by (rule r);
   6.102              finally; show ?thesis; .;
   6.103            qed;
   6.104 @@ -120,63 +120,63 @@
   6.105  $h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
   6.106  is a linear extension of $h$ to $H_0$. *};
   6.107  
   6.108 -lemma h0_lf: 
   6.109 -  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
   6.110 +lemma h'_lf: 
   6.111 +  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
   6.112                  in h y + a * xi);
   6.113 -  H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
   6.114 -  x0 : E; x0 ~= \<zero>; is_vectorspace E |]
   6.115 -  ==> is_linearform H0 h0";
   6.116 +  H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \<notin> H; 
   6.117 +  x0 \<in> E; x0 \<noteq> 0; is_vectorspace E |]
   6.118 +  ==> is_linearform H' h'";
   6.119  proof -;
   6.120 -  assume h0_def: 
   6.121 -    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
   6.122 +  assume h'_def: 
   6.123 +    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
   6.124                 in h y + a * xi)"
   6.125 -    and H0_def: "H0 == H + lin x0" 
   6.126 -    and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
   6.127 -      "x0 ~= \<zero>" "x0 : E" "is_vectorspace E";
   6.128 +    and H'_def: "H' == H + lin x0" 
   6.129 +    and vs: "is_subspace H E" "is_linearform H h" "x0 \<notin> H"
   6.130 +      "x0 \<noteq> 0" "x0 \<in> E" "is_vectorspace E";
   6.131  
   6.132 -  have h0: "is_vectorspace H0"; 
   6.133 -  proof (unfold H0_def, rule vs_sum_vs);
   6.134 +  have h': "is_vectorspace H'"; 
   6.135 +  proof (unfold H'_def, rule vs_sum_vs);
   6.136      show "is_subspace (lin x0) E"; ..;
   6.137    qed; 
   6.138  
   6.139    show ?thesis;
   6.140    proof;
   6.141 -    fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; 
   6.142 +    fix x1 x2; assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"; 
   6.143  
   6.144      txt{* We now have to show that $h_0$ is additive, i.~e.\
   6.145      $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
   6.146      for $x_1, x_2\in H$. *}; 
   6.147  
   6.148 -    have x1x2: "x1 + x2 : H0"; 
   6.149 -      by (rule vs_add_closed, rule h0); 
   6.150 +    have x1x2: "x1 + x2 \<in> H'"; 
   6.151 +      by (rule vs_add_closed, rule h'); 
   6.152      from x1; 
   6.153 -    have ex_x1: "EX y1 a1. x1 = y1 + a1 \<prod> x0  & y1 : H"; 
   6.154 -      by (unfold H0_def vs_sum_def lin_def) fast;
   6.155 +    have ex_x1: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0  \<and> y1 \<in> H"; 
   6.156 +      by (unfold H'_def vs_sum_def lin_def) fast;
   6.157      from x2; 
   6.158 -    have ex_x2: "EX y2 a2. x2 = y2 + a2 \<prod> x0 & y2 : H"; 
   6.159 -      by (unfold H0_def vs_sum_def lin_def) fast;
   6.160 +    have ex_x2: "\<exists> y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H"; 
   6.161 +      by (unfold H'_def vs_sum_def lin_def) fast;
   6.162      from x1x2; 
   6.163 -    have ex_x1x2: "EX y a. x1 + x2 = y + a \<prod> x0 & y : H";
   6.164 -      by (unfold H0_def vs_sum_def lin_def) fast;
   6.165 +    have ex_x1x2: "\<exists> y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H";
   6.166 +      by (unfold H'_def vs_sum_def lin_def) fast;
   6.167  
   6.168      from ex_x1 ex_x2 ex_x1x2;
   6.169 -    show "h0 (x1 + x2) = h0 x1 + h0 x2";
   6.170 +    show "h' (x1 + x2) = h' x1 + h' x2";
   6.171      proof (elim exE conjE);
   6.172        fix y1 y2 y a1 a2 a;
   6.173 -      assume y1: "x1 = y1 + a1 \<prod> x0"     and y1': "y1 : H"
   6.174 -         and y2: "x2 = y2 + a2 \<prod> x0"     and y2': "y2 : H" 
   6.175 -         and y: "x1 + x2 = y + a \<prod> x0"   and y':  "y  : H"; 
   6.176 +      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
   6.177 +         and y2: "x2 = y2 + a2 \<cdot> x0"     and y2': "y2 \<in> H" 
   6.178 +         and y: "x1 + x2 = y + a \<cdot> x0"   and y':  "y  \<in> H"; 
   6.179  
   6.180 -      have ya: "y1 + y2 = y & a1 + a2 = a"; 
   6.181 -      proof (rule decomp_H0);;
   6.182 -	txt_raw {* \label{decomp-H0-use} *};;
   6.183 -        show "y1 + y2 + (a1 + a2) \<prod> x0 = y + a \<prod> x0"; 
   6.184 +      have ya: "y1 + y2 = y \<and> a1 + a2 = a"; 
   6.185 +      proof (rule decomp_H');;
   6.186 +	txt_raw {* \label{decomp-H-use} *};;
   6.187 +        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0"; 
   6.188            by (simp! add: vs_add_mult_distrib2 [of E]);
   6.189 -        show "y1 + y2 : H"; ..;
   6.190 +        show "y1 + y2 \<in> H"; ..;
   6.191        qed;
   6.192  
   6.193 -      have "h0 (x1 + x2) = h y + a * xi";
   6.194 -	by (rule h0_definite);
   6.195 +      have "h' (x1 + x2) = h y + a * xi";
   6.196 +	by (rule h'_definite);
   6.197        also; have "... = h (y1 + y2) + (a1 + a2) * xi"; 
   6.198          by (simp add: ya);
   6.199        also; from vs y1' y2'; 
   6.200 @@ -185,10 +185,10 @@
   6.201                        real_add_mult_distrib);
   6.202        also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
   6.203          by simp;
   6.204 -      also; have "h y1 + a1 * xi = h0 x1"; 
   6.205 -        by (rule h0_definite [RS sym]);
   6.206 -      also; have "h y2 + a2 * xi = h0 x2"; 
   6.207 -        by (rule h0_definite [RS sym]);
   6.208 +      also; have "h y1 + a1 * xi = h' x1"; 
   6.209 +        by (rule h'_definite [RS sym]);
   6.210 +      also; have "h y2 + a2 * xi = h' x2"; 
   6.211 +        by (rule h'_definite [RS sym]);
   6.212        finally; show ?thesis; .;
   6.213      qed;
   6.214   
   6.215 @@ -198,39 +198,39 @@
   6.216      *}; 
   6.217  
   6.218    next;  
   6.219 -    fix c x1; assume x1: "x1 : H0";    
   6.220 -    have ax1: "c \<prod> x1 : H0";
   6.221 -      by (rule vs_mult_closed, rule h0);
   6.222 -    from x1; have ex_x: "!! x. x: H0 
   6.223 -                        ==> EX y a. x = y + a \<prod> x0 & y : H";
   6.224 -      by (unfold H0_def vs_sum_def lin_def) fast;
   6.225 +    fix c x1; assume x1: "x1 \<in> H'";    
   6.226 +    have ax1: "c \<cdot> x1 \<in> H'";
   6.227 +      by (rule vs_mult_closed, rule h');
   6.228 +    from x1; have ex_x: "!! x. x\<in> H' 
   6.229 +                        ==> \<exists> y a. x = y + a \<cdot> x0 \<and> y \<in> H";
   6.230 +      by (unfold H'_def vs_sum_def lin_def) fast;
   6.231  
   6.232 -    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 \<prod> x0 & y1 : H";
   6.233 -      by (unfold H0_def vs_sum_def lin_def) fast;
   6.234 -    with ex_x [of "c \<prod> x1", OF ax1];
   6.235 -    show "h0 (c \<prod> x1) = c * (h0 x1)";  
   6.236 +    from x1; have ex_x1: "\<exists> y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H";
   6.237 +      by (unfold H'_def vs_sum_def lin_def) fast;
   6.238 +    with ex_x [of "c \<cdot> x1", OF ax1];
   6.239 +    show "h' (c \<cdot> x1) = c * (h' x1)";  
   6.240      proof (elim exE conjE);
   6.241        fix y1 y a1 a; 
   6.242 -      assume y1: "x1 = y1 + a1 \<prod> x0"       and y1': "y1 : H"
   6.243 -        and y: "c \<prod> x1 = y  + a  \<prod> x0"   and y':  "y  : H"; 
   6.244 +      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
   6.245 +        and y: "c \<cdot> x1 = y  + a \<cdot> x0"    and y': "y \<in> H"; 
   6.246  
   6.247 -      have ya: "c \<prod> y1 = y & c * a1 = a"; 
   6.248 -      proof (rule decomp_H0); 
   6.249 -	show "c \<prod> y1 + (c * a1) \<prod> x0 = y + a \<prod> x0"; 
   6.250 -          by (simp! add: add: vs_add_mult_distrib1);
   6.251 -        show "c \<prod> y1 : H"; ..;
   6.252 +      have ya: "c \<cdot> y1 = y \<and> c * a1 = a"; 
   6.253 +      proof (rule decomp_H'); 
   6.254 +	show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0"; 
   6.255 +          by (simp! add: vs_add_mult_distrib1);
   6.256 +        show "c \<cdot> y1 \<in> H"; ..;
   6.257        qed;
   6.258  
   6.259 -      have "h0 (c \<prod> x1) = h y + a * xi"; 
   6.260 -	by (rule h0_definite);
   6.261 -      also; have "... = h (c \<prod> y1) + (c * a1) * xi";
   6.262 +      have "h' (c \<cdot> x1) = h y + a * xi"; 
   6.263 +	by (rule h'_definite);
   6.264 +      also; have "... = h (c \<cdot> y1) + (c * a1) * xi";
   6.265          by (simp add: ya);
   6.266        also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
   6.267  	by (simp add: linearform_mult [of H]);
   6.268        also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
   6.269  	by (simp add: real_add_mult_distrib2 real_mult_assoc);
   6.270 -      also; have "h y1 + a1 * xi = h0 x1"; 
   6.271 -        by (rule h0_definite [RS sym]);
   6.272 +      also; have "h y1 + a1 * xi = h' x1"; 
   6.273 +        by (rule h'_definite [RS sym]);
   6.274        finally; show ?thesis; .;
   6.275      qed;
   6.276    qed;
   6.277 @@ -239,40 +239,40 @@
   6.278  text{* \medskip The linear extension $h_0$ of $h$
   6.279  is bounded by the seminorm $p$. *};
   6.280  
   6.281 -lemma h0_norm_pres:
   6.282 -  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
   6.283 +lemma h'_norm_pres:
   6.284 +  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
   6.285                  in h y + a * xi);
   6.286 -  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= \<zero>; is_vectorspace E; 
   6.287 -  is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y; 
   6.288 -  ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
   6.289 -   ==> ALL x:H0. h0 x <= p x"; 
   6.290 +  H' == H + lin x0; x0 \<notin> H; x0 \<in> E; x0 \<noteq> 0; is_vectorspace E; 
   6.291 +  is_subspace H E; is_seminorm E p; is_linearform H h; \<forall>y \<in> H. h y <= p y; 
   6.292 +  \<forall>y \<in> H. - p (y + x0) - h y <= xi \<and> xi <= p (y + x0) - h y |]
   6.293 +   ==> \<forall> x \<in> H'. h' x <= p x"; 
   6.294  proof; 
   6.295 -  assume h0_def: 
   6.296 -    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
   6.297 +  assume h'_def: 
   6.298 +    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
   6.299                 in (h y) + a * xi)"
   6.300 -    and H0_def: "H0 == H + lin x0" 
   6.301 -    and vs: "x0 ~: H" "x0 : E" "x0 ~= \<zero>" "is_vectorspace E" 
   6.302 +    and H'_def: "H' == H + lin x0" 
   6.303 +    and vs: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" "is_vectorspace E" 
   6.304              "is_subspace H E" "is_seminorm E p" "is_linearform H h" 
   6.305 -    and a: "ALL y:H. h y <= p y";
   6.306 -  presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
   6.307 -  presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
   6.308 -  fix x; assume "x : H0"; 
   6.309 +    and a: "\<forall>y \<in> H. h y <= p y";
   6.310 +  presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya <= xi";
   6.311 +  presume a2: "\<forall>ya \<in> H. xi <= p (ya + x0) - h ya";
   6.312 +  fix x; assume "x \<in> H'"; 
   6.313    have ex_x: 
   6.314 -    "!! x. x : H0 ==> EX y a. x = y + a \<prod> x0 & y : H";
   6.315 -    by (unfold H0_def vs_sum_def lin_def) fast;
   6.316 -  have "EX y a. x = y + a \<prod> x0 & y : H";
   6.317 +    "!! x. x \<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
   6.318 +    by (unfold H'_def vs_sum_def lin_def) fast;
   6.319 +  have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
   6.320      by (rule ex_x);
   6.321 -  thus "h0 x <= p x";
   6.322 +  thus "h' x <= p x";
   6.323    proof (elim exE conjE);
   6.324 -    fix y a; assume x: "x = y + a \<prod> x0" and y: "y : H";
   6.325 -    have "h0 x = h y + a * xi";
   6.326 -      by (rule h0_definite);
   6.327 +    fix y a; assume x: "x = y + a \<cdot> x0" and y: "y \<in> H";
   6.328 +    have "h' x = h y + a * xi";
   6.329 +      by (rule h'_definite);
   6.330  
   6.331      txt{* Now we show  
   6.332      $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
   6.333      by case analysis on $a$. \label{linorder_linear_split}*};
   6.334  
   6.335 -    also; have "... <= p (y + a \<prod> x0)";
   6.336 +    also; have "... <= p (y + a \<cdot> x0)";
   6.337      proof (rule linorder_linear_split); 
   6.338  
   6.339        assume z: "a = #0"; 
   6.340 @@ -282,29 +282,29 @@
   6.341      taken as $y/a$: *};
   6.342  
   6.343      next;
   6.344 -      assume lz: "a < #0"; hence nz: "a ~= #0"; by simp;
   6.345 +      assume lz: "a < #0"; hence nz: "a \<noteq> #0"; by simp;
   6.346        from a1; 
   6.347 -      have "- p (rinv a \<prod> y + x0) - h (rinv a \<prod> y) <= xi";
   6.348 +      have "- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y) <= xi";
   6.349          by (rule bspec) (simp!);
   6.350  
   6.351        txt {* The thesis for this case now follows by a short  
   6.352        calculation. *};      
   6.353        hence "a * xi 
   6.354 -            <= a * (- p (rinv a \<prod> y + x0) - h (rinv a \<prod> y))";
   6.355 +            <= a * (- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
   6.356          by (rule real_mult_less_le_anti [OF lz]);
   6.357 -      also; have "... = - a * (p (rinv a \<prod> y + x0)) 
   6.358 -                        - a * (h (rinv a \<prod> y))";
   6.359 +      also; have "... = - a * (p (rinv a \<cdot> y + x0)) 
   6.360 +                        - a * (h (rinv a \<cdot> y))";
   6.361          by (rule real_mult_diff_distrib);
   6.362 -      also; from lz vs y; have "- a * (p (rinv a \<prod> y + x0)) 
   6.363 -                               = p (a \<prod> (rinv a \<prod> y + x0))";
   6.364 +      also; from lz vs y; have "- a * (p (rinv a \<cdot> y + x0)) 
   6.365 +                               = p (a \<cdot> (rinv a \<cdot> y + x0))";
   6.366          by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
   6.367 -      also; from nz vs y; have "... = p (y + a \<prod> x0)";
   6.368 +      also; from nz vs y; have "... = p (y + a \<cdot> x0)";
   6.369          by (simp add: vs_add_mult_distrib1);
   6.370 -      also; from nz vs y; have "a * (h (rinv a \<prod> y)) =  h y";
   6.371 +      also; from nz vs y; have "a * (h (rinv a \<cdot> y)) =  h y";
   6.372          by (simp add: linearform_mult [RS sym]);
   6.373 -      finally; have "a * xi <= p (y + a \<prod> x0) - h y"; .;
   6.374 +      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
   6.375  
   6.376 -      hence "h y + a * xi <= h y + p (y + a \<prod> x0) - h y";
   6.377 +      hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y";
   6.378          by (simp add: real_add_left_cancel_le);
   6.379        thus ?thesis; by simp;
   6.380  
   6.381 @@ -312,32 +312,32 @@
   6.382        taken as $y/a$: *};
   6.383  
   6.384      next; 
   6.385 -      assume gz: "#0 < a"; hence nz: "a ~= #0"; by simp;
   6.386 +      assume gz: "#0 < a"; hence nz: "a \<noteq> #0"; by simp;
   6.387        from a2;
   6.388 -      have "xi <= p (rinv a \<prod> y + x0) - h (rinv a \<prod> y)";
   6.389 +      have "xi <= p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y)";
   6.390          by (rule bspec) (simp!);
   6.391  
   6.392        txt {* The thesis for this case follows by a short
   6.393        calculation: *};
   6.394  
   6.395        with gz; have "a * xi 
   6.396 -            <= a * (p (rinv a \<prod> y + x0) - h (rinv a \<prod> y))";
   6.397 +            <= a * (p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
   6.398          by (rule real_mult_less_le_mono);
   6.399 -      also; have "... = a * p (rinv a \<prod> y + x0) 
   6.400 -                        - a * h (rinv a \<prod> y)";
   6.401 +      also; have "... = a * p (rinv a \<cdot> y + x0) 
   6.402 +                        - a * h (rinv a \<cdot> y)";
   6.403          by (rule real_mult_diff_distrib2); 
   6.404        also; from gz vs y; 
   6.405 -      have "a * p (rinv a \<prod> y + x0) 
   6.406 -           = p (a \<prod> (rinv a \<prod> y + x0))";
   6.407 +      have "a * p (rinv a \<cdot> y + x0) 
   6.408 +           = p (a \<cdot> (rinv a \<cdot> y + x0))";
   6.409          by (simp add: seminorm_abs_homogenous abs_eqI2);
   6.410        also; from nz vs y; 
   6.411 -      have "... = p (y + a \<prod> x0)";
   6.412 +      have "... = p (y + a \<cdot> x0)";
   6.413          by (simp add: vs_add_mult_distrib1);
   6.414 -      also; from nz vs y; have "a * h (rinv a \<prod> y) = h y";
   6.415 +      also; from nz vs y; have "a * h (rinv a \<cdot> y) = h y";
   6.416          by (simp add: linearform_mult [RS sym]); 
   6.417 -      finally; have "a * xi <= p (y + a \<prod> x0) - h y"; .;
   6.418 +      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
   6.419   
   6.420 -      hence "h y + a * xi <= h y + (p (y + a \<prod> x0) - h y)";
   6.421 +      hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)";
   6.422          by (simp add: real_add_left_cancel_le);
   6.423        thus ?thesis; by simp;
   6.424      qed;
   6.425 @@ -346,4 +346,4 @@
   6.426    qed;
   6.427  qed blast+; 
   6.428  
   6.429 -end;
   6.430 \ No newline at end of file
   6.431 +end;
     7.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sun Jul 16 21:00:32 2000 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Jul 17 13:58:18 2000 +0200
     7.3 @@ -7,8 +7,6 @@
     7.4  
     7.5  theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
     7.6  
     7.7 -
     7.8 -
     7.9  text{* This section contains some lemmas that will be used in the
    7.10  proof of the Hahn-Banach Theorem.
    7.11  In this section the following context is presumed. 
    7.12 @@ -20,7 +18,6 @@
    7.13  i.e.\ the supremum of the chain $c$.
    7.14  *} 
    7.15  
    7.16 -
    7.17  text{* Let $c$ be a chain of norm-preserving extensions of the 
    7.18  function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. 
    7.19  Every element in $H$ is member of
    7.20 @@ -28,38 +25,38 @@
    7.21  
    7.22  lemma some_H'h't:
    7.23    "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
    7.24 -  graph H h = Union c; x \\<in> H |]
    7.25 -   ==> \\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h' 
    7.26 -       & is_linearform H' h' & is_subspace H' E 
    7.27 -       & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
    7.28 -       & (\\<forall>x \\<in> H'. h' x \\<le> p x)"
    7.29 +  graph H h = \<Union> c; x \<in> H |]
    7.30 +   ==> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' 
    7.31 +       \<and> is_linearform H' h' \<and> is_subspace H' E 
    7.32 +       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
    7.33 +       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
    7.34  proof -
    7.35    assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M"
    7.36 -     and u: "graph H h = Union c" "x \\<in> H"
    7.37 +     and u: "graph H h = \<Union> c" "x \<in> H"
    7.38  
    7.39    have h: "(x, h x) \<in> graph H h" ..
    7.40 -  with u have "(x, h x) \<in> Union c" by simp
    7.41 -  hence ex1: "\<exists> g \\<in> c. (x, h x) \<in> g" 
    7.42 +  with u have "(x, h x) \<in> \<Union> c" by simp
    7.43 +  hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g" 
    7.44      by (simp only: Union_iff)
    7.45    thus ?thesis
    7.46    proof (elim bexE)
    7.47 -    fix g assume g: "g \\<in> c" "(x, h x) \\<in> g"
    7.48 -    have "c \\<subseteq> M" by (rule chainD2)
    7.49 -    hence "g \\<in> M" ..
    7.50 +    fix g assume g: "g \<in> c" "(x, h x) \<in> g"
    7.51 +    have "c \<subseteq> M" by (rule chainD2)
    7.52 +    hence "g \<in> M" ..
    7.53      hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
    7.54 -    hence "\<exists> H' h'. graph H' h' = g 
    7.55 -                  & is_linearform H' h'
    7.56 -                  & is_subspace H' E
    7.57 -                  & is_subspace F H'
    7.58 -                  & graph F f \\<subseteq> graph H' h'
    7.59 -                  & (\<forall>x \\<in> H'. h' x \\<le> p x)"
    7.60 +    hence "\<exists>H' h'. graph H' h' = g 
    7.61 +                  \<and> is_linearform H' h'
    7.62 +                  \<and> is_subspace H' E
    7.63 +                  \<and> is_subspace F H'
    7.64 +                  \<and> graph F f \<subseteq> graph H' h'
    7.65 +                  \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
    7.66        by (rule norm_pres_extension_D)
    7.67      thus ?thesis
    7.68      proof (elim exE conjE) 
    7.69        fix H' h' 
    7.70        assume "graph H' h' = g" "is_linearform H' h'" 
    7.71          "is_subspace H' E" "is_subspace F H'" 
    7.72 -        "graph F f \\<subseteq> graph H' h'" "\<forall>x \\<in> H'. h' x \\<le> p x"
    7.73 +        "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
    7.74        show ?thesis 
    7.75        proof (intro exI conjI)
    7.76          show "graph H' h' \<in> c" by (simp!)
    7.77 @@ -78,28 +75,28 @@
    7.78  
    7.79  lemma some_H'h': 
    7.80    "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
    7.81 -  graph H h = Union c; x \\<in> H |] 
    7.82 -  ==> \<exists> H' h'. x \\<in> H' & graph H' h' \\<subseteq> graph H h 
    7.83 -      & is_linearform H' h' & is_subspace H' E & is_subspace F H'
    7.84 -      & graph F f \\<subseteq> graph H' h' & (\<forall>x \\<in> H'. h' x \\<le> p x)" 
    7.85 +  graph H h = \<Union> c; x \<in> H |] 
    7.86 +  ==> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
    7.87 +      \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
    7.88 +      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 
    7.89  proof -
    7.90    assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M"
    7.91 -     and u: "graph H h = Union c" "x \\<in> H"  
    7.92 +     and u: "graph H h = \<Union> c" "x \<in> H"  
    7.93  
    7.94 -  have "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h' 
    7.95 -       & is_linearform H' h' & is_subspace H' E 
    7.96 -       & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
    7.97 -       & (\<forall> x \\<in> H'. h' x \\<le> p x)"
    7.98 +  have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' 
    7.99 +       \<and> is_linearform H' h' \<and> is_subspace H' E 
   7.100 +       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
   7.101 +       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
   7.102      by (rule some_H'h't)
   7.103    thus ?thesis 
   7.104    proof (elim exE conjE)
   7.105      fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c"
   7.106        "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
   7.107 -      "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x"
   7.108 +      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
   7.109      show ?thesis
   7.110      proof (intro exI conjI)
   7.111 -      show "x\<in>H'" by (rule graphD1)
   7.112 -      from cM u show "graph H' h' \\<subseteq> graph H h" 
   7.113 +      show "x \<in> H'" by (rule graphD1)
   7.114 +      from cM u show "graph H' h' \<subseteq> graph H h" 
   7.115          by (simp! only: chain_ball_Union_upper)
   7.116      qed
   7.117    qed
   7.118 @@ -111,48 +108,48 @@
   7.119  $h'$, such that $h$ extends $h'$. *}
   7.120  
   7.121  lemma some_H'h'2: 
   7.122 -  "[| M = norm_pres_extensions E p F f; c\<in> chain M; 
   7.123 -  graph H h = Union c;  x\<in>H; y\<in>H |] 
   7.124 -  ==> \<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h 
   7.125 -      & is_linearform H' h' & is_subspace H' E & is_subspace F H'
   7.126 -      & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)" 
   7.127 +  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
   7.128 +  graph H h = \<Union> c;  x \<in> H; y \<in> H |] 
   7.129 +  ==> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
   7.130 +      \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
   7.131 +      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 
   7.132  proof -
   7.133 -  assume "M = norm_pres_extensions E p F f" "c\<in> chain M" 
   7.134 -         "graph H h = Union c" "x\<in>H" "y\<in>H"
   7.135 +  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
   7.136 +         "graph H h = \<Union> c" "x \<in> H" "y \<in> H"
   7.137  
   7.138    txt {* $x$ is in the domain $H'$ of some function $h'$, 
   7.139    such that $h$ extends $h'$. *} 
   7.140  
   7.141 -  have e1: "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h'
   7.142 -       & is_linearform H' h' & is_subspace H' E 
   7.143 -       & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
   7.144 -       & (\<forall> x\<in>H'. h' x \\<le> p x)"
   7.145 +  have e1: "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
   7.146 +       \<and> is_linearform H' h' \<and> is_subspace H' E 
   7.147 +       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
   7.148 +       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
   7.149      by (rule some_H'h't)
   7.150  
   7.151    txt {* $y$ is in the domain $H''$ of some function $h''$,
   7.152    such that $h$ extends $h''$. *} 
   7.153  
   7.154 -  have e2: "\<exists> H'' h''. graph H'' h'' \<in> c & (y, h y) \<in> graph H'' h''
   7.155 -       & is_linearform H'' h'' & is_subspace H'' E 
   7.156 -       & is_subspace F H'' & graph F f \\<subseteq> graph H'' h'' 
   7.157 -       & (\<forall> x\<in>H''. h'' x \\<le> p x)"
   7.158 +  have e2: "\<exists>H'' h''. graph H'' h'' \<in> c \<and> (y, h y) \<in> graph H'' h''
   7.159 +       \<and> is_linearform H'' h'' \<and> is_subspace H'' E 
   7.160 +       \<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h'' 
   7.161 +       \<and> (\<forall>x \<in> H''. h'' x \<le> p x)"
   7.162      by (rule some_H'h't)
   7.163  
   7.164    from e1 e2 show ?thesis 
   7.165    proof (elim exE conjE)
   7.166 -    fix H' h' assume "(y, h y)\<in> graph H' h'" "graph H' h' \<in> c"
   7.167 +    fix H' h' assume "(y, h y) \<in> graph H' h'" "graph H' h' \<in> c"
   7.168        "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
   7.169 -      "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x"
   7.170 +      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
   7.171  
   7.172 -    fix H'' h'' assume "(x, h x)\<in> graph H'' h''" "graph H'' h'' \<in> c"
   7.173 +    fix H'' h'' assume "(x, h x) \<in> graph H'' h''" "graph H'' h'' \<in> c"
   7.174        "is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''"
   7.175 -      "graph F f \\<subseteq> graph H'' h''" "\<forall> x\<in>H''. h'' x \\<le> p x"
   7.176 +      "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"
   7.177  
   7.178     txt {* Since both $h'$ and $h''$ are elements of the chain,  
   7.179     $h''$ is an extension of $h'$ or vice versa. Thus both 
   7.180     $x$ and $y$ are contained in the greater one. \label{cases1}*}
   7.181  
   7.182 -    have "graph H'' h'' \\<subseteq> graph H' h' | graph H' h' \\<subseteq> graph H'' h''"
   7.183 +    have "graph H'' h'' \<subseteq> graph H' h' | graph H' h' \<subseteq> graph H'' h''"
   7.184        (is "?case1 | ?case2")
   7.185        by (rule chainD)
   7.186      thus ?thesis
   7.187 @@ -161,23 +158,23 @@
   7.188        show ?thesis
   7.189        proof (intro exI conjI)
   7.190          have "(x, h x) \<in> graph H'' h''" .
   7.191 -        also have "... \\<subseteq> graph H' h'" .
   7.192 -        finally have xh\<in> "(x, h x)\<in> graph H' h'" .
   7.193 -        thus x: "x\<in>H'" ..
   7.194 -        show y: "y\<in>H'" ..
   7.195 -        show "graph H' h' \\<subseteq> graph H h"
   7.196 +        also have "... \<subseteq> graph H' h'" .
   7.197 +        finally have xh:"(x, h x) \<in> graph H' h'" .
   7.198 +        thus x: "x \<in> H'" ..
   7.199 +        show y: "y \<in> H'" ..
   7.200 +        show "graph H' h' \<subseteq> graph H h"
   7.201            by (simp! only: chain_ball_Union_upper)
   7.202        qed
   7.203      next
   7.204        assume ?case2
   7.205        show ?thesis
   7.206        proof (intro exI conjI)
   7.207 -        show x: "x\<in>H''" ..
   7.208 +        show x: "x \<in> H''" ..
   7.209          have "(y, h y) \<in> graph H' h'" by (simp!)
   7.210 -        also have "... \\<subseteq> graph H'' h''" .
   7.211 -        finally have yh: "(y, h y)\<in> graph H'' h''" .
   7.212 -        thus y: "y\<in>H''" ..
   7.213 -        show "graph H'' h'' \\<subseteq> graph H h"
   7.214 +        also have "... \<subseteq> graph H'' h''" .
   7.215 +        finally have yh: "(y, h y) \<in> graph H'' h''" .
   7.216 +        thus y: "y \<in> H''" ..
   7.217 +        show "graph H'' h'' \<subseteq> graph H h"
   7.218            by (simp! only: chain_ball_Union_upper)
   7.219        qed
   7.220      qed
   7.221 @@ -187,14 +184,14 @@
   7.222  
   7.223  
   7.224  text{* \medskip The relation induced by the graph of the supremum
   7.225 -of a chain $c$ is definite, i.~e.~it is the graph of a function. *}
   7.226 +of a chain $c$ is definite, i.~e.~t is the graph of a function. *}
   7.227  
   7.228  lemma sup_definite: 
   7.229    "[| M == norm_pres_extensions E p F f; c \<in> chain M; 
   7.230 -  (x, y) \<in> Union c; (x, z) \<in> Union c |] ==> z = y"
   7.231 +  (x, y) \<in> \<Union> c; (x, z) \<in> \<Union> c |] ==> z = y"
   7.232  proof - 
   7.233 -  assume "c\<in>chain M" "M == norm_pres_extensions E p F f"
   7.234 -    "(x, y) \<in> Union c" "(x, z) \<in> Union c"
   7.235 +  assume "c \<in> chain M" "M == norm_pres_extensions E p F f"
   7.236 +    "(x, y) \<in> \<Union> c" "(x, z) \<in> \<Union> c"
   7.237    thus ?thesis
   7.238    proof (elim UnionE chainE2)
   7.239  
   7.240 @@ -203,7 +200,7 @@
   7.241      both $G_1$ and $G_2$ are members of $c$.*}
   7.242  
   7.243      fix G1 G2 assume
   7.244 -      "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \\<subseteq> M"
   7.245 +      "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \<subseteq> M"
   7.246  
   7.247      have "G1 \<in> M" ..
   7.248      hence e1: "\<exists> H1 h1. graph H1 h1 = G1"  
   7.249 @@ -219,7 +216,7 @@
   7.250        txt{* $G_1$ is contained in $G_2$ or vice versa, 
   7.251        since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*}
   7.252  
   7.253 -      have "G1 \\<subseteq> G2 | G2 \\<subseteq> G1" (is "?case1 | ?case2") ..
   7.254 +      have "G1 \<subseteq> G2 | G2 \<subseteq> G1" (is "?case1 | ?case2") ..
   7.255        thus ?thesis
   7.256        proof
   7.257          assume ?case1
   7.258 @@ -247,27 +244,27 @@
   7.259  function $h'$ is linear by construction of $M$.  *}
   7.260  
   7.261  lemma sup_lf: 
   7.262 -  "[| M = norm_pres_extensions E p F f; c\<in> chain M; 
   7.263 -  graph H h = Union c |] ==> is_linearform H h"
   7.264 +  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
   7.265 +  graph H h = \<Union> c |] ==> is_linearform H h"
   7.266  proof - 
   7.267 -  assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
   7.268 -         "graph H h = Union c"
   7.269 +  assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
   7.270 +         "graph H h = \<Union> c"
   7.271   
   7.272    show "is_linearform H h"
   7.273    proof
   7.274      fix x y assume "x \<in> H" "y \<in> H" 
   7.275 -    have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h 
   7.276 -            & is_linearform H' h' & is_subspace H' E 
   7.277 -            & is_subspace F H' & graph F f \\<subseteq> graph H' h'
   7.278 -            & (\<forall> x\<in>H'. h' x \\<le> p x)"
   7.279 +    have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
   7.280 +            \<and> is_linearform H' h' \<and> is_subspace H' E 
   7.281 +            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
   7.282 +            \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
   7.283        by (rule some_H'h'2)
   7.284  
   7.285      txt {* We have to show that $h$ is additive. *}
   7.286  
   7.287      thus "h (x + y) = h x + h y" 
   7.288      proof (elim exE conjE)
   7.289 -      fix H' h' assume "x\<in>H'" "y\<in>H'" 
   7.290 -        and b: "graph H' h' \\<subseteq> graph H h" 
   7.291 +      fix H' h' assume "x \<in> H'" "y \<in> H'" 
   7.292 +        and b: "graph H' h' \<subseteq> graph H h" 
   7.293          and "is_linearform H' h'" "is_subspace H' E"
   7.294        have "h' (x + y) = h' x + h' y" 
   7.295          by (rule linearform_add)
   7.296 @@ -279,24 +276,24 @@
   7.297      qed
   7.298    next  
   7.299      fix a x assume "x \<in> H"
   7.300 -    have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h 
   7.301 -            & is_linearform H' h' & is_subspace H' E
   7.302 -            & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
   7.303 -            & (\<forall> x\<in>H'. h' x \\<le> p x)"
   7.304 +    have "\<exists> H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
   7.305 +            \<and> is_linearform H' h' \<and> is_subspace H' E
   7.306 +            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
   7.307 +            \<and> (\<forall> x \<in> H'. h' x \<le> p x)"
   7.308        by (rule some_H'h')
   7.309  
   7.310      txt{* We have to show that $h$ is multiplicative. *}
   7.311  
   7.312 -    thus "h (a \<prod> x) = a * h x"
   7.313 +    thus "h (a \<cdot> x) = a * h x"
   7.314      proof (elim exE conjE)
   7.315 -      fix H' h' assume "x\<in>H'"
   7.316 -        and b: "graph H' h' \\<subseteq> graph H h" 
   7.317 +      fix H' h' assume "x \<in> H'"
   7.318 +        and b: "graph H' h' \<subseteq> graph H h" 
   7.319          and "is_linearform H' h'" "is_subspace H' E"
   7.320 -      have "h' (a \<prod> x) = a * h' x" 
   7.321 +      have "h' (a \<cdot> x) = a * h' x" 
   7.322          by (rule linearform_mult)
   7.323        also have "h' x = h x" ..
   7.324 -      also have "a \<prod> x \<in> H'" ..
   7.325 -      with b have "h' (a \<prod> x) = h (a \<prod> x)" ..
   7.326 +      also have "a \<cdot> x \<in> H'" ..
   7.327 +      with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
   7.328        finally show ?thesis .
   7.329      qed
   7.330    qed
   7.331 @@ -309,34 +306,34 @@
   7.332  for every element of the chain.*}
   7.333  
   7.334  lemma sup_ext:
   7.335 -  "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c; 
   7.336 -  graph H h = Union c |] ==> graph F f \\<subseteq> graph H h"
   7.337 +  "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; 
   7.338 +  c \<in> chain M; \<exists>x. x \<in> c |] ==> graph F f \<subseteq> graph H h"
   7.339  proof -
   7.340 -  assume "M = norm_pres_extensions E p F f" "c\<in> chain M" 
   7.341 -         "graph H h = Union c"
   7.342 -  assume "\<exists> x. x\<in>c"
   7.343 +  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
   7.344 +         "graph H h = \<Union> c"
   7.345 +  assume "\<exists>x. x \<in> c"
   7.346    thus ?thesis 
   7.347    proof
   7.348 -    fix x assume "x\<in>c" 
   7.349 -    have "c \\<subseteq> M" by (rule chainD2)
   7.350 -    hence "x\<in>M" ..
   7.351 +    fix x assume "x \<in> c" 
   7.352 +    have "c \<subseteq> M" by (rule chainD2)
   7.353 +    hence "x \<in> M" ..
   7.354      hence "x \<in> norm_pres_extensions E p F f" by (simp!)
   7.355  
   7.356 -    hence "\<exists> G g. graph G g = x
   7.357 -             & is_linearform G g 
   7.358 -             & is_subspace G E
   7.359 -             & is_subspace F G
   7.360 -             & graph F f \\<subseteq> graph G g 
   7.361 -             & (\<forall> x\<in>G. g x \\<le> p x)"
   7.362 +    hence "\<exists>G g. graph G g = x
   7.363 +             \<and> is_linearform G g 
   7.364 +             \<and> is_subspace G E
   7.365 +             \<and> is_subspace F G
   7.366 +             \<and> graph F f \<subseteq> graph G g 
   7.367 +             \<and> (\<forall>x \<in> G. g x \<le> p x)"
   7.368        by (simp! add: norm_pres_extension_D)
   7.369  
   7.370      thus ?thesis 
   7.371      proof (elim exE conjE) 
   7.372 -      fix G g assume "graph F f \\<subseteq> graph G g"
   7.373 +      fix G g assume "graph F f \<subseteq> graph G g"
   7.374        also assume "graph G g = x"
   7.375        also have "... \<in> c" .
   7.376 -      hence "x \\<subseteq> Union c" by fast
   7.377 -      also have [RS sym]: "graph H h = Union c" .
   7.378 +      hence "x \<subseteq> \<Union> c" by fast
   7.379 +      also have [RS sym]: "graph H h = \<Union> c" .
   7.380        finally show ?thesis .
   7.381      qed
   7.382    qed
   7.383 @@ -348,30 +345,30 @@
   7.384  vector space. *}
   7.385  
   7.386  lemma sup_supF: 
   7.387 -  "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c;
   7.388 -  graph H h = Union c; is_subspace F E; is_vectorspace E |] 
   7.389 +  "[|  graph H h = \<Union> c; M = norm_pres_extensions E p F f; 
   7.390 +  c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] 
   7.391    ==> is_subspace F H"
   7.392  proof - 
   7.393 -  assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c"
   7.394 -    "graph H h = Union c" "is_subspace F E" "is_vectorspace E"
   7.395 +  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
   7.396 +    "graph H h = \<Union> c" "is_subspace F E" "is_vectorspace E"
   7.397  
   7.398    show ?thesis 
   7.399    proof
   7.400 -    show "\<zero> \<in> F" ..
   7.401 -    show "F \\<subseteq> H" 
   7.402 +    show "0 \<in> F" ..
   7.403 +    show "F \<subseteq> H" 
   7.404      proof (rule graph_extD2)
   7.405 -      show "graph F f \\<subseteq> graph H h"
   7.406 +      show "graph F f \<subseteq> graph H h"
   7.407          by (rule sup_ext)
   7.408      qed
   7.409 -    show "\<forall> x\<in>F. \<forall> y\<in>F. x + y \<in> F" 
   7.410 +    show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F" 
   7.411      proof (intro ballI) 
   7.412 -      fix x y assume "x\<in>F" "y\<in>F"
   7.413 +      fix x y assume "x \<in> F" "y \<in> F"
   7.414        show "x + y \<in> F" by (simp!)
   7.415      qed
   7.416 -    show "\<forall> x\<in>F. \<forall> a. a \<prod> x \<in> F"
   7.417 +    show "\<forall>x \<in> F. \<forall>a. a \<cdot> x \<in> F"
   7.418      proof (intro ballI allI)
   7.419        fix x a assume "x\<in>F"
   7.420 -      show "a \<prod> x \<in> F" by (simp!)
   7.421 +      show "a \<cdot> x \<in> F" by (simp!)
   7.422      qed
   7.423    qed
   7.424  qed
   7.425 @@ -380,78 +377,78 @@
   7.426  of $E$. *}
   7.427  
   7.428  lemma sup_subE: 
   7.429 -  "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c; 
   7.430 -  graph H h = Union c; is_subspace F E; is_vectorspace E |] 
   7.431 +  "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; 
   7.432 +  c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] 
   7.433    ==> is_subspace H E"
   7.434  proof - 
   7.435 -  assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c"
   7.436 -    "graph H h = Union c" "is_subspace F E" "is_vectorspace E"
   7.437 +  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
   7.438 +    "graph H h = \<Union> c" "is_subspace F E" "is_vectorspace E"
   7.439    show ?thesis 
   7.440    proof
   7.441   
   7.442      txt {* The $\zero$ element is in $H$, as $F$ is a subset 
   7.443      of $H$: *}
   7.444  
   7.445 -    have "\<zero> \<in> F" ..
   7.446 +    have "0 \<in> F" ..
   7.447      also have "is_subspace F H" by (rule sup_supF) 
   7.448 -    hence "F \\<subseteq> H" ..
   7.449 -    finally show "\<zero> \<in> H" .
   7.450 +    hence "F \<subseteq> H" ..
   7.451 +    finally show "0 \<in> H" .
   7.452  
   7.453      txt{* $H$ is a subset of $E$: *}
   7.454  
   7.455 -    show "H \\<subseteq> E" 
   7.456 +    show "H \<subseteq> E" 
   7.457      proof
   7.458 -      fix x assume "x\<in>H"
   7.459 -      have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
   7.460 -              & is_linearform H' h' & is_subspace H' E 
   7.461 -              & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
   7.462 -              & (\<forall> x\<in>H'. h' x \\<le> p x)" 
   7.463 +      fix x assume "x \<in> H"
   7.464 +      have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
   7.465 +              \<and> is_linearform H' h' \<and> is_subspace H' E 
   7.466 +              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
   7.467 +              \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 
   7.468  	by (rule some_H'h')
   7.469 -      thus "x\<in>E" 
   7.470 +      thus "x \<in> E" 
   7.471        proof (elim exE conjE)
   7.472 -	fix H' h' assume "x\<in>H'" "is_subspace H' E"
   7.473 -        have "H' \\<subseteq> E" ..
   7.474 -	thus "x\<in>E" ..
   7.475 +	fix H' h' assume "x \<in> H'" "is_subspace H' E"
   7.476 +        have "H' \<subseteq> E" ..
   7.477 +	thus "x \<in> E" ..
   7.478        qed
   7.479      qed
   7.480  
   7.481      txt{* $H$ is closed under addition: *}
   7.482  
   7.483 -    show "\<forall> x\<in>H. \<forall> y\<in>H. x + y \<in> H" 
   7.484 +    show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H" 
   7.485      proof (intro ballI) 
   7.486 -      fix x y assume "x\<in>H" "y\<in>H"
   7.487 -      have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h 
   7.488 -              & is_linearform H' h' & is_subspace H' E 
   7.489 -              & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
   7.490 -              & (\<forall> x\<in>H'. h' x \\<le> p x)" 
   7.491 +      fix x y assume "x \<in> H" "y \<in> H"
   7.492 +      have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
   7.493 +              \<and> is_linearform H' h' \<and> is_subspace H' E 
   7.494 +              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
   7.495 +              \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 
   7.496  	by (rule some_H'h'2) 
   7.497        thus "x + y \<in> H" 
   7.498        proof (elim exE conjE) 
   7.499  	fix H' h' 
   7.500 -        assume "x\<in>H'" "y\<in>H'" "is_subspace H' E" 
   7.501 -          "graph H' h' \\<subseteq> graph H h"
   7.502 +        assume "x \<in> H'" "y \<in> H'" "is_subspace H' E" 
   7.503 +          "graph H' h' \<subseteq> graph H h"
   7.504          have "x + y \<in> H'" ..
   7.505 -	also have "H' \\<subseteq> H" ..
   7.506 +	also have "H' \<subseteq> H" ..
   7.507  	finally show ?thesis .
   7.508        qed
   7.509      qed      
   7.510  
   7.511      txt{* $H$ is closed under scalar multiplication: *}
   7.512  
   7.513 -    show "\<forall> x\<in>H. \<forall> a. a \<prod> x \<in> H" 
   7.514 +    show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H" 
   7.515      proof (intro ballI allI) 
   7.516 -      fix x a assume "x\<in>H" 
   7.517 -      have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
   7.518 -              & is_linearform H' h' & is_subspace H' E 
   7.519 -              & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
   7.520 -              & (\<forall> x\<in>H'. h' x \\<le> p x)" 
   7.521 +      fix x a assume "x \<in> H" 
   7.522 +      have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
   7.523 +              \<and> is_linearform H' h' \<and> is_subspace H' E 
   7.524 +              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
   7.525 +              \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 
   7.526  	by (rule some_H'h') 
   7.527 -      thus "a \<prod> x \<in> H" 
   7.528 +      thus "a \<cdot> x \<in> H" 
   7.529        proof (elim exE conjE)
   7.530  	fix H' h' 
   7.531 -        assume "x\<in>H'" "is_subspace H' E" "graph H' h' \\<subseteq> graph H h"
   7.532 -        have "a \<prod> x \<in> H'" ..
   7.533 -        also have "H' \\<subseteq> H" ..
   7.534 +        assume "x \<in> H'" "is_subspace H' E" "graph H' h' \<subseteq> graph H h"
   7.535 +        have "a \<cdot> x \<in> H'" ..
   7.536 +        also have "H' \<subseteq> H" ..
   7.537  	finally show ?thesis .
   7.538        qed
   7.539      qed
   7.540 @@ -463,24 +460,24 @@
   7.541  bounded by $p$.
   7.542  *}
   7.543  
   7.544 -lemma sup_norm_pres\<in> 
   7.545 -  "[| M = norm_pres_extensions E p F f; c\<in> chain M; 
   7.546 -  graph H h = Union c |] ==> \<forall> x\<in>H. h x \\<le> p x"
   7.547 +lemma sup_norm_pres:
   7.548 +  "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; c \<in> chain M |] 
   7.549 +  ==> \<forall> x \<in> H. h x \<le> p x"
   7.550  proof
   7.551 -  assume "M = norm_pres_extensions E p F f" "c\<in> chain M" 
   7.552 -         "graph H h = Union c"
   7.553 -  fix x assume "x\<in>H"
   7.554 -  have "\\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h 
   7.555 -          & is_linearform H' h' & is_subspace H' E & is_subspace F H'
   7.556 -          & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)" 
   7.557 +  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
   7.558 +         "graph H h = \<Union> c"
   7.559 +  fix x assume "x \<in> H"
   7.560 +  have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
   7.561 +          \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
   7.562 +          \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall> x \<in> H'. h' x \<le> p x)" 
   7.563      by (rule some_H'h')
   7.564 -  thus "h x \\<le> p x" 
   7.565 +  thus "h x \<le> p x" 
   7.566    proof (elim exE conjE)
   7.567      fix H' h' 
   7.568 -    assume "x\<in> H'" "graph H' h' \\<subseteq> graph H h" 
   7.569 -      and a: "\<forall> x\<in> H'. h' x \\<le> p x"
   7.570 +    assume "x \<in> H'" "graph H' h' \<subseteq> graph H h" 
   7.571 +      and a: "\<forall>x \<in> H'. h' x \<le> p x"
   7.572      have [RS sym]: "h' x = h x" ..
   7.573 -    also from a have "h' x \\<le> p x " ..
   7.574 +    also from a have "h' x \<le> p x " ..
   7.575      finally show ?thesis .  
   7.576    qed
   7.577  qed
   7.578 @@ -499,7 +496,7 @@
   7.579  lemma abs_ineq_iff: 
   7.580    "[| is_subspace H E; is_vectorspace E; is_seminorm E p; 
   7.581    is_linearform H h |] 
   7.582 -  ==> (\<forall> x\<in>H. abs (h x) \\<le> p x) = (\<forall> x\<in>H. h x \\<le> p x)" 
   7.583 +  ==> (\<forall>x \<in> H. |h x| \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" 
   7.584    (concl is "?L = ?R")
   7.585  proof -
   7.586    assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" 
   7.587 @@ -510,28 +507,28 @@
   7.588      assume l: ?L
   7.589      show ?R
   7.590      proof
   7.591 -      fix x assume x: "x\<in>H"
   7.592 -      have "h x \\<le> abs (h x)" by (rule abs_ge_self)
   7.593 -      also from l have "... \\<le> p x" ..
   7.594 -      finally show "h x \\<le> p x" .
   7.595 +      fix x assume x: "x \<in> H"
   7.596 +      have "h x \<le> |h x|" by (rule abs_ge_self)
   7.597 +      also from l have "... \<le> p x" ..
   7.598 +      finally show "h x \<le> p x" .
   7.599      qed
   7.600    next
   7.601      assume r: ?R
   7.602      show ?L
   7.603      proof 
   7.604 -      fix x assume "x\<in>H"
   7.605 -      show "!! a b \<in>: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a"
   7.606 +      fix x assume "x \<in> H"
   7.607 +      show "!! a b :: real. [| - a \<le> b; b \<le> a |] ==> |b| \<le> a"
   7.608          by arith
   7.609 -      show "- p x \\<le> h x"
   7.610 +      show "- p x \<le> h x"
   7.611        proof (rule real_minus_le)
   7.612  	from h have "- h x = h (- x)" 
   7.613            by (rule linearform_neg [RS sym])
   7.614 -	also from r have "... \\<le> p (- x)" by (simp!)
   7.615 +	also from r have "... \<le> p (- x)" by (simp!)
   7.616  	also have "... = p x" 
   7.617            by (rule seminorm_minus [OF _ subspace_subsetD])
   7.618 -	finally show "- h x \\<le> p x" . 
   7.619 +	finally show "- h x \<le> p x" . 
   7.620        qed
   7.621 -      from r show "h x \\<le> p x" .. 
   7.622 +      from r show "h x \<le> p x" .. 
   7.623      qed
   7.624    qed
   7.625  qed  
     8.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jul 16 21:00:32 2000 +0200
     8.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Jul 17 13:58:18 2000 +0200
     8.3 @@ -11,41 +11,41 @@
     8.4  space into the reals that is additive and multiplicative. *}
     8.5  
     8.6  constdefs
     8.7 -  is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
     8.8 +  is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool" 
     8.9    "is_linearform V f == 
    8.10 -      (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
    8.11 -      (ALL x: V. ALL a. f (a (*) x) = a * (f x))" 
    8.12 +      (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
    8.13 +      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))" 
    8.14  
    8.15  lemma is_linearformI [intro]: 
    8.16 -  "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
    8.17 -    !! x c. x : V ==> f (c (*) x) = c * f x |]
    8.18 +  "[| !! x y. [| x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y;
    8.19 +    !! x c. x \<in> V ==> f (c \<cdot> x) = c * f x |]
    8.20   ==> is_linearform V f"
    8.21   by (unfold is_linearform_def) force
    8.22  
    8.23  lemma linearform_add [intro??]: 
    8.24 -  "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y"
    8.25 +  "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
    8.26    by (unfold is_linearform_def) fast
    8.27  
    8.28  lemma linearform_mult [intro??]: 
    8.29 -  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)" 
    8.30 +  "[| is_linearform V f; x \<in> V |] ==>  f (a \<cdot> x) = a * (f x)" 
    8.31    by (unfold is_linearform_def) fast
    8.32  
    8.33  lemma linearform_neg [intro??]:
    8.34 -  "[|  is_vectorspace V; is_linearform V f; x:V|] 
    8.35 +  "[|  is_vectorspace V; is_linearform V f; x \<in> V|] 
    8.36    ==> f (- x) = - f x"
    8.37  proof - 
    8.38 -  assume "is_linearform V f" "is_vectorspace V" "x:V"
    8.39 -  have "f (- x) = f ((- #1) (*) x)" by (simp! add: negate_eq1)
    8.40 +  assume "is_linearform V f" "is_vectorspace V" "x \<in> V"
    8.41 +  have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
    8.42    also have "... = (- #1) * (f x)" by (rule linearform_mult)
    8.43    also have "... = - (f x)" by (simp!)
    8.44    finally show ?thesis .
    8.45  qed
    8.46  
    8.47  lemma linearform_diff [intro??]: 
    8.48 -  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
    8.49 +  "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] 
    8.50    ==> f (x - y) = f x - f y"  
    8.51  proof -
    8.52 -  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"
    8.53 +  assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V"
    8.54    have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
    8.55    also have "... = f x + f (- y)" 
    8.56      by (rule linearform_add) (simp!)+
    8.57 @@ -56,14 +56,14 @@
    8.58  text{* Every linear form yields $0$ for the $\zero$ vector.*}
    8.59  
    8.60  lemma linearform_zero [intro??, simp]: 
    8.61 -  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = #0" 
    8.62 +  "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
    8.63  proof - 
    8.64    assume "is_vectorspace V" "is_linearform V f"
    8.65 -  have "f 00 = f (00 - 00)" by (simp!)
    8.66 -  also have "... = f 00 - f 00" 
    8.67 +  have "f 0 = f (0 - 0)" by (simp!)
    8.68 +  also have "... = f 0 - f 0" 
    8.69      by (rule linearform_diff) (simp!)+
    8.70    also have "... = #0" by simp
    8.71 -  finally show "f 00 = #0" .
    8.72 +  finally show "f 0 = #0" .
    8.73  qed 
    8.74  
    8.75  end
    8.76 \ No newline at end of file
     9.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Jul 16 21:00:32 2000 +0200
     9.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Jul 17 13:58:18 2000 +0200
     9.3 @@ -7,6 +7,8 @@
     9.4  
     9.5  theory NormedSpace =  Subspace:
     9.6  
     9.7 +syntax 
     9.8 +  abs :: "real \<Rightarrow> real" ("|_|")
     9.9  
    9.10  subsection {* Quasinorms *}
    9.11  
    9.12 @@ -15,57 +17,57 @@
    9.13  definite, absolute homogenous and subadditive.  *}
    9.14  
    9.15  constdefs
    9.16 -  is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
    9.17 -  "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
    9.18 +  is_seminorm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
    9.19 +  "is_seminorm V norm == \<forall>x \<in>  V. \<forall>y \<in> V. \<forall>a. 
    9.20          #0 <= norm x 
    9.21 -      & norm (a (*) x) = (abs a) * (norm x)
    9.22 -      & norm (x + y) <= norm x + norm y"
    9.23 +      \<and> norm (a \<cdot> x) = |a| * norm x
    9.24 +      \<and> norm (x + y) <= norm x + norm y"
    9.25  
    9.26  lemma is_seminormI [intro]: 
    9.27 -  "[| !! x y a. [| x:V; y:V|] ==> #0 <= norm x;
    9.28 -  !! x a. x:V ==> norm (a (*) x) = (abs a) * (norm x);
    9.29 -  !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
    9.30 +  "[| !! x y a. [| x \<in> V; y \<in> V|] ==> #0 <= norm x;
    9.31 +  !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x;
    9.32 +  !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |] 
    9.33    ==> is_seminorm V norm"
    9.34    by (unfold is_seminorm_def, force)
    9.35  
    9.36  lemma seminorm_ge_zero [intro??]:
    9.37 -  "[| is_seminorm V norm; x:V |] ==> #0 <= norm x"
    9.38 +  "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
    9.39    by (unfold is_seminorm_def, force)
    9.40  
    9.41  lemma seminorm_abs_homogenous: 
    9.42 -  "[| is_seminorm V norm; x:V |] 
    9.43 -  ==> norm (a (*) x) = (abs a) * (norm x)"
    9.44 +  "[| is_seminorm V norm; x \<in> V |] 
    9.45 +  ==> norm (a \<cdot> x) = |a| * norm x"
    9.46    by (unfold is_seminorm_def, force)
    9.47  
    9.48  lemma seminorm_subadditive: 
    9.49 -  "[| is_seminorm V norm; x:V; y:V |] 
    9.50 +  "[| is_seminorm V norm; x \<in> V; y \<in> V |] 
    9.51    ==> norm (x + y) <= norm x + norm y"
    9.52    by (unfold is_seminorm_def, force)
    9.53  
    9.54  lemma seminorm_diff_subadditive: 
    9.55 -  "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |] 
    9.56 +  "[| is_seminorm V norm; x \<in> V; y \<in> V; is_vectorspace V |] 
    9.57    ==> norm (x - y) <= norm x + norm y"
    9.58  proof -
    9.59 -  assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V"
    9.60 -  have "norm (x - y) = norm (x + - #1 (*) y)"  
    9.61 +  assume "is_seminorm V norm" "x \<in> V" "y \<in> V" "is_vectorspace V"
    9.62 +  have "norm (x - y) = norm (x + - #1 \<cdot> y)"  
    9.63      by (simp! add: diff_eq2 negate_eq2a)
    9.64 -  also have "... <= norm x + norm  (- #1 (*) y)" 
    9.65 +  also have "... <= norm x + norm  (- #1 \<cdot> y)" 
    9.66      by (simp! add: seminorm_subadditive)
    9.67 -  also have "norm (- #1 (*) y) = abs (- #1) * norm y" 
    9.68 +  also have "norm (- #1 \<cdot> y) = |- #1| * norm y" 
    9.69      by (rule seminorm_abs_homogenous)
    9.70 -  also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
    9.71 +  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
    9.72    finally show "norm (x - y) <= norm x + norm y" by simp
    9.73  qed
    9.74  
    9.75  lemma seminorm_minus: 
    9.76 -  "[| is_seminorm V norm; x:V; is_vectorspace V |] 
    9.77 +  "[| is_seminorm V norm; x \<in> V; is_vectorspace V |] 
    9.78    ==> norm (- x) = norm x"
    9.79  proof -
    9.80 -  assume "is_seminorm V norm" "x:V" "is_vectorspace V"
    9.81 -  have "norm (- x) = norm (- #1 (*) x)" by (simp! only: negate_eq1)
    9.82 -  also have "... = abs (- #1) * norm x" 
    9.83 +  assume "is_seminorm V norm" "x \<in> V" "is_vectorspace V"
    9.84 +  have "norm (- x) = norm (- #1 \<cdot> x)" by (simp! only: negate_eq1)
    9.85 +  also have "... = |- #1| * norm x" 
    9.86      by (rule seminorm_abs_homogenous)
    9.87 -  also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
    9.88 +  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
    9.89    finally show "norm (- x) = norm x" by simp
    9.90  qed
    9.91  
    9.92 @@ -76,24 +78,24 @@
    9.93  $\zero$ vector to $0$. *}
    9.94  
    9.95  constdefs
    9.96 -  is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
    9.97 -  "is_norm V norm == ALL x: V.  is_seminorm V norm 
    9.98 -      & (norm x = #0) = (x = 00)"
    9.99 +  is_norm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
   9.100 +  "is_norm V norm == \<forall>x \<in> V.  is_seminorm V norm 
   9.101 +      \<and> (norm x = #0) = (x = 0)"
   9.102  
   9.103  lemma is_normI [intro]: 
   9.104 -  "ALL x: V.  is_seminorm V norm  & (norm x = #0) = (x = 00) 
   9.105 +  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0) 
   9.106    ==> is_norm V norm" by (simp only: is_norm_def)
   9.107  
   9.108  lemma norm_is_seminorm [intro??]: 
   9.109 -  "[| is_norm V norm; x:V |] ==> is_seminorm V norm"
   9.110 +  "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
   9.111    by (unfold is_norm_def, force)
   9.112  
   9.113  lemma norm_zero_iff: 
   9.114 -  "[| is_norm V norm; x:V |] ==> (norm x = #0) = (x = 00)"
   9.115 +  "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
   9.116    by (unfold is_norm_def, force)
   9.117  
   9.118  lemma norm_ge_zero [intro??]:
   9.119 -  "[|is_norm V norm; x:V |] ==> #0 <= norm x"
   9.120 +  "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
   9.121    by (unfold is_norm_def is_seminorm_def, force)
   9.122  
   9.123  
   9.124 @@ -104,10 +106,9 @@
   9.125  
   9.126  constdefs
   9.127    is_normed_vectorspace :: 
   9.128 -  "['a::{plus, minus} set, 'a => real] => bool"
   9.129 +  "['a::{plus, minus, zero} set, 'a => real] => bool"
   9.130    "is_normed_vectorspace V norm ==
   9.131 -      is_vectorspace V &
   9.132 -      is_norm V norm"
   9.133 +      is_vectorspace V \<and> is_norm V norm"
   9.134  
   9.135  lemma normed_vsI [intro]: 
   9.136    "[| is_vectorspace V; is_norm V norm |] 
   9.137 @@ -123,32 +124,32 @@
   9.138    by (unfold is_normed_vectorspace_def, elim conjE)
   9.139  
   9.140  lemma normed_vs_norm_ge_zero [intro??]: 
   9.141 -  "[| is_normed_vectorspace V norm; x:V |] ==> #0 <= norm x"
   9.142 +  "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
   9.143    by (unfold is_normed_vectorspace_def, rule, elim conjE)
   9.144  
   9.145  lemma normed_vs_norm_gt_zero [intro??]: 
   9.146 -  "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> #0 < norm x"
   9.147 +  "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
   9.148  proof (unfold is_normed_vectorspace_def, elim conjE)
   9.149 -  assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm"
   9.150 +  assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
   9.151    have "#0 <= norm x" ..
   9.152 -  also have "#0 ~= norm x"
   9.153 +  also have "#0 \<noteq> norm x"
   9.154    proof
   9.155      presume "norm x = #0"
   9.156 -    also have "?this = (x = 00)" by (rule norm_zero_iff)
   9.157 -    finally have "x = 00" .
   9.158 +    also have "?this = (x = 0)" by (rule norm_zero_iff)
   9.159 +    finally have "x = 0" .
   9.160      thus "False" by contradiction
   9.161    qed (rule sym)
   9.162    finally show "#0 < norm x" .
   9.163  qed
   9.164  
   9.165  lemma normed_vs_norm_abs_homogenous [intro??]: 
   9.166 -  "[| is_normed_vectorspace V norm; x:V |] 
   9.167 -  ==> norm (a (*) x) = (abs a) * (norm x)"
   9.168 +  "[| is_normed_vectorspace V norm; x \<in> V |] 
   9.169 +  ==> norm (a \<cdot> x) = |a| * norm x"
   9.170    by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 
   9.171        rule normed_vs_norm)
   9.172  
   9.173  lemma normed_vs_norm_subadditive [intro??]: 
   9.174 -  "[| is_normed_vectorspace V norm; x:V; y:V |] 
   9.175 +  "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] 
   9.176    ==> norm (x + y) <= norm x + norm y"
   9.177    by (rule seminorm_subadditive, rule norm_is_seminorm, 
   9.178       rule normed_vs_norm)
   9.179 @@ -157,7 +158,7 @@
   9.180  normed vectorspace.*}
   9.181  
   9.182  lemma subspace_normed_vs [intro??]: 
   9.183 -  "[| is_subspace F E; is_vectorspace E; 
   9.184 +  "[| is_vectorspace E; is_subspace F E;
   9.185    is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
   9.186  proof (rule normed_vsI)
   9.187    assume "is_subspace F E" "is_vectorspace E" 
   9.188 @@ -167,15 +168,15 @@
   9.189    proof (intro is_normI ballI conjI)
   9.190      show "is_seminorm F norm" 
   9.191      proof
   9.192 -      fix x y a presume "x : E"
   9.193 +      fix x y a presume "x \<in> E"
   9.194        show "#0 <= norm x" ..
   9.195 -      show "norm (a (*) x) = abs a * norm x" ..
   9.196 -      presume "y : E"
   9.197 +      show "norm (a \<cdot> x) = |a| * norm x" ..
   9.198 +      presume "y \<in> E"
   9.199        show "norm (x + y) <= norm x + norm y" ..
   9.200      qed (simp!)+
   9.201  
   9.202 -    fix x assume "x : F"
   9.203 -    show "(norm x = #0) = (x = 00)" 
   9.204 +    fix x assume "x \<in> F"
   9.205 +    show "(norm x = #0) = (x = 0)" 
   9.206      proof (rule norm_zero_iff)
   9.207        show "is_norm E norm" ..
   9.208      qed (simp!)
    10.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 16 21:00:32 2000 +0200
    10.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Jul 17 13:58:18 2000 +0200
    10.3 @@ -16,39 +16,39 @@
    10.4  scalar multiplication. *}
    10.5  
    10.6  constdefs 
    10.7 -  is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
    10.8 -  "is_subspace U V == U ~= {} & U <= V 
    10.9 -     & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)"
   10.10 +  is_subspace ::  "['a::{plus, minus, zero} set, 'a set] => bool"
   10.11 +  "is_subspace U V == U \<noteq> {} \<and> U <= V 
   10.12 +     \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x\<in> U)"
   10.13  
   10.14  lemma subspaceI [intro]: 
   10.15 -  "[| 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
   10.16 -  ALL x:U. ALL a. a (*) x : U |]
   10.17 +  "[| 0 \<in> U; U <= V; \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U); 
   10.18 +  \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U |]
   10.19    ==> is_subspace U V"
   10.20  proof (unfold is_subspace_def, intro conjI) 
   10.21 -  assume "00 : U" thus "U ~= {}" by fast
   10.22 +  assume "0 \<in> U" thus "U \<noteq> {}" by fast
   10.23  qed (simp+)
   10.24  
   10.25 -lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}"
   10.26 +lemma subspace_not_empty [intro??]: "is_subspace U V ==> U \<noteq> {}"
   10.27    by (unfold is_subspace_def) simp 
   10.28  
   10.29  lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"
   10.30    by (unfold is_subspace_def) simp
   10.31  
   10.32  lemma subspace_subsetD [simp, intro??]: 
   10.33 -  "[| is_subspace U V; x:U |] ==> x:V"
   10.34 +  "[| is_subspace U V; x \<in> U |] ==> x \<in> V"
   10.35    by (unfold is_subspace_def) force
   10.36  
   10.37  lemma subspace_add_closed [simp, intro??]: 
   10.38 -  "[| is_subspace U V; x:U; y:U |] ==> x + y : U"
   10.39 +  "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U"
   10.40    by (unfold is_subspace_def) simp
   10.41  
   10.42  lemma subspace_mult_closed [simp, intro??]: 
   10.43 -  "[| is_subspace U V; x:U |] ==> a (*) x : U"
   10.44 +  "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U"
   10.45    by (unfold is_subspace_def) simp
   10.46  
   10.47  lemma subspace_diff_closed [simp, intro??]: 
   10.48 -  "[| is_subspace U V; is_vectorspace V; x:U; y:U |] 
   10.49 -  ==> x - y : U"
   10.50 +  "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |] 
   10.51 +  ==> x - y \<in> U"
   10.52    by (simp! add: diff_eq1 negate_eq1)
   10.53  
   10.54  text {* Similar as for linear spaces, the existence of the 
   10.55 @@ -56,23 +56,23 @@
   10.56  of the carrier set and by vector space laws.*}
   10.57  
   10.58  lemma zero_in_subspace [intro??]:
   10.59 -  "[| is_subspace U V; is_vectorspace V |] ==> 00 : U"
   10.60 +  "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U"
   10.61  proof - 
   10.62    assume "is_subspace U V" and v: "is_vectorspace V"
   10.63 -  have "U ~= {}" ..
   10.64 -  hence "EX x. x:U" by force
   10.65 +  have "U \<noteq> {}" ..
   10.66 +  hence "\<exists>x. x \<in> U" by force
   10.67    thus ?thesis 
   10.68    proof 
   10.69 -    fix x assume u: "x:U" 
   10.70 -    hence "x:V" by (simp!)
   10.71 -    with v have "00 = x - x" by (simp!)
   10.72 -    also have "... : U" by (rule subspace_diff_closed)
   10.73 +    fix x assume u: "x \<in> U" 
   10.74 +    hence "x \<in> V" by (simp!)
   10.75 +    with v have "0 = x - x" by (simp!)
   10.76 +    also have "... \<in> U" by (rule subspace_diff_closed)
   10.77      finally show ?thesis .
   10.78    qed
   10.79  qed
   10.80  
   10.81  lemma subspace_neg_closed [simp, intro??]: 
   10.82 -  "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U"
   10.83 +  "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U"
   10.84    by (simp add: negate_eq1)
   10.85  
   10.86  text_raw {* \medskip *}
   10.87 @@ -84,11 +84,11 @@
   10.88    assume "is_subspace U V" "is_vectorspace V"
   10.89    show ?thesis
   10.90    proof 
   10.91 -    show "00 : U" ..
   10.92 -    show "ALL x:U. ALL a. a (*) x : U" by (simp!)
   10.93 -    show "ALL x:U. ALL y:U. x + y : U" by (simp!)
   10.94 -    show "ALL x:U. - x = -#1 (*) x" by (simp! add: negate_eq1)
   10.95 -    show "ALL x:U. ALL y:U. x - y =  x + - y" 
   10.96 +    show "0 \<in> U" ..
   10.97 +    show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!)
   10.98 +    show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!)
   10.99 +    show "\<forall>x \<in> U. - x = -#1 \<cdot> x" by (simp! add: negate_eq1)
  10.100 +    show "\<forall>x \<in> U. \<forall>y \<in> U. x - y =  x + - y" 
  10.101        by (simp! add: diff_eq1)
  10.102    qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+
  10.103  qed
  10.104 @@ -98,10 +98,10 @@
  10.105  lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"
  10.106  proof 
  10.107    assume "is_vectorspace V"
  10.108 -  show "00 : V" ..
  10.109 +  show "0 \<in> V" ..
  10.110    show "V <= V" ..
  10.111 -  show "ALL x:V. ALL y:V. x + y : V" by (simp!)
  10.112 -  show "ALL x:V. ALL a. a (*) x : V" by (simp!)
  10.113 +  show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!)
  10.114 +  show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!)
  10.115  qed
  10.116  
  10.117  text {* The subspace relation is transitive. *}
  10.118 @@ -111,22 +111,22 @@
  10.119    ==> is_subspace U W"
  10.120  proof 
  10.121    assume "is_subspace U V" "is_subspace V W" "is_vectorspace V"
  10.122 -  show "00 : U" ..
  10.123 +  show "0 \<in> U" ..
  10.124  
  10.125    have "U <= V" ..
  10.126    also have "V <= W" ..
  10.127    finally show "U <= W" .
  10.128  
  10.129 -  show "ALL x:U. ALL y:U. x + y : U" 
  10.130 +  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
  10.131    proof (intro ballI)
  10.132 -    fix x y assume "x:U" "y:U"
  10.133 -    show "x + y : U" by (simp!)
  10.134 +    fix x y assume "x \<in> U" "y \<in> U"
  10.135 +    show "x + y \<in> U" by (simp!)
  10.136    qed
  10.137  
  10.138 -  show "ALL x:U. ALL a. a (*) x : U"
  10.139 +  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
  10.140    proof (intro ballI allI)
  10.141 -    fix x a assume "x:U"
  10.142 -    show "a (*) x : U" by (simp!)
  10.143 +    fix x a assume "x \<in> U"
  10.144 +    show "a \<cdot> x \<in> U" by (simp!)
  10.145    qed
  10.146  qed
  10.147  
  10.148 @@ -138,60 +138,60 @@
  10.149  scalar multiples of $x$. *}
  10.150  
  10.151  constdefs
  10.152 -  lin :: "'a => 'a set"
  10.153 -  "lin x == {a (*) x | a. True}" 
  10.154 +  lin :: "('a::{minus,plus,zero}) => 'a set"
  10.155 +  "lin x == {a \<cdot> x | a. True}" 
  10.156  
  10.157 -lemma linD: "x : lin v = (EX a::real. x = a (*) v)"
  10.158 +lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
  10.159    by (unfold lin_def) fast
  10.160  
  10.161 -lemma linI [intro??]: "a (*) x0 : lin x0"
  10.162 +lemma linI [intro??]: "a \<cdot> x0 \<in> lin x0"
  10.163    by (unfold lin_def) fast
  10.164  
  10.165  text {* Every vector is contained in its linear closure. *}
  10.166  
  10.167 -lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x"
  10.168 +lemma x_lin_x: "[| is_vectorspace V; x \<in> V |] ==> x \<in> lin x"
  10.169  proof (unfold lin_def, intro CollectI exI conjI)
  10.170 -  assume "is_vectorspace V" "x:V"
  10.171 -  show "x = #1 (*) x" by (simp!)
  10.172 +  assume "is_vectorspace V" "x \<in> V"
  10.173 +  show "x = #1 \<cdot> x" by (simp!)
  10.174  qed simp
  10.175  
  10.176  text {* Any linear closure is a subspace. *}
  10.177  
  10.178  lemma lin_subspace [intro??]: 
  10.179 -  "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"
  10.180 +  "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V"
  10.181  proof
  10.182 -  assume "is_vectorspace V" "x:V"
  10.183 -  show "00 : lin x" 
  10.184 +  assume "is_vectorspace V" "x \<in> V"
  10.185 +  show "0 \<in> lin x" 
  10.186    proof (unfold lin_def, intro CollectI exI conjI)
  10.187 -    show "00 = (#0::real) (*) x" by (simp!)
  10.188 +    show "0 = (#0::real) \<cdot> x" by (simp!)
  10.189    qed simp
  10.190  
  10.191    show "lin x <= V"
  10.192    proof (unfold lin_def, intro subsetI, elim CollectE exE conjE) 
  10.193 -    fix xa a assume "xa = a (*) x" 
  10.194 -    show "xa:V" by (simp!)
  10.195 +    fix xa a assume "xa = a \<cdot> x" 
  10.196 +    show "xa \<in> V" by (simp!)
  10.197    qed
  10.198  
  10.199 -  show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x" 
  10.200 +  show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x" 
  10.201    proof (intro ballI)
  10.202 -    fix x1 x2 assume "x1 : lin x" "x2 : lin x" 
  10.203 -    thus "x1 + x2 : lin x"
  10.204 +    fix x1 x2 assume "x1 \<in> lin x" "x2 \<in> lin x" 
  10.205 +    thus "x1 + x2 \<in> lin x"
  10.206      proof (unfold lin_def, elim CollectE exE conjE, 
  10.207        intro CollectI exI conjI)
  10.208 -      fix a1 a2 assume "x1 = a1 (*) x" "x2 = a2 (*) x"
  10.209 -      show "x1 + x2 = (a1 + a2) (*) x" 
  10.210 +      fix a1 a2 assume "x1 = a1 \<cdot> x" "x2 = a2 \<cdot> x"
  10.211 +      show "x1 + x2 = (a1 + a2) \<cdot> x" 
  10.212          by (simp! add: vs_add_mult_distrib2)
  10.213      qed simp
  10.214    qed
  10.215  
  10.216 -  show "ALL xa:lin x. ALL a. a (*) xa : lin x" 
  10.217 +  show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x" 
  10.218    proof (intro ballI allI)
  10.219 -    fix x1 a assume "x1 : lin x" 
  10.220 -    thus "a (*) x1 : lin x"
  10.221 +    fix x1 a assume "x1 \<in> lin x" 
  10.222 +    thus "a \<cdot> x1 \<in> lin x"
  10.223      proof (unfold lin_def, elim CollectE exE conjE,
  10.224        intro CollectI exI conjI)
  10.225 -      fix a1 assume "x1 = a1 (*) x"
  10.226 -      show "a (*) x1 = (a * a1) (*) x" by (simp!)
  10.227 +      fix a1 assume "x1 = a1 \<cdot> x"
  10.228 +      show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!)
  10.229      qed simp
  10.230    qed 
  10.231  qed
  10.232 @@ -199,9 +199,9 @@
  10.233  text {* Any linear closure is a vector space. *}
  10.234  
  10.235  lemma lin_vs [intro??]: 
  10.236 -  "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"
  10.237 +  "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)"
  10.238  proof (rule subspace_vs)
  10.239 -  assume "is_vectorspace V" "x:V"
  10.240 +  assume "is_vectorspace V" "x \<in> V"
  10.241    show "is_subspace (lin x) V" ..
  10.242  qed
  10.243  
  10.244 @@ -215,22 +215,22 @@
  10.245  instance set :: (plus) plus by intro_classes
  10.246  
  10.247  defs vs_sum_def:
  10.248 -  "U + V == {u + v | u v. u:U & v:V}" (***
  10.249 +  "U + V == {u + v | u v. u \<in> U \<and> v \<in> V}" (***
  10.250  
  10.251  constdefs 
  10.252    vs_sum :: 
  10.253 -  "['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
  10.254 -  "vs_sum U V == {x. EX u:U. EX v:V. x = u + v}";
  10.255 +  "['a::{plus, minus, zero} set, 'a set] => 'a set"         (infixl "+" 65)
  10.256 +  "vs_sum U V == {x. \<exists>u \<in> U. \<exists>v \<in> V. x = u + v}";
  10.257  ***)
  10.258  
  10.259  lemma vs_sumD: 
  10.260 -  "x: U + V = (EX u:U. EX v:V. x = u + v)"
  10.261 +  "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
  10.262      by (unfold vs_sum_def) fast
  10.263  
  10.264  lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
  10.265  
  10.266  lemma vs_sumI [intro??]: 
  10.267 -  "[| x:U; y:V; t= x + y |] ==> t : U + V"
  10.268 +  "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
  10.269    by (unfold vs_sum_def) fast
  10.270  
  10.271  text{* $U$ is a subspace of $U + V$. *}
  10.272 @@ -240,20 +240,20 @@
  10.273    ==> is_subspace U (U + V)"
  10.274  proof 
  10.275    assume "is_vectorspace U" "is_vectorspace V"
  10.276 -  show "00 : U" ..
  10.277 +  show "0 \<in> U" ..
  10.278    show "U <= U + V"
  10.279    proof (intro subsetI vs_sumI)
  10.280 -  fix x assume "x:U"
  10.281 -    show "x = x + 00" by (simp!)
  10.282 -    show "00 : V" by (simp!)
  10.283 +  fix x assume "x \<in> U"
  10.284 +    show "x = x + 0" by (simp!)
  10.285 +    show "0 \<in> V" by (simp!)
  10.286    qed
  10.287 -  show "ALL x:U. ALL y:U. x + y : U" 
  10.288 +  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
  10.289    proof (intro ballI)
  10.290 -    fix x y assume "x:U" "y:U" show "x + y : U" by (simp!)
  10.291 +    fix x y assume "x \<in> U" "y \<in> U" show "x + y \<in> U" by (simp!)
  10.292    qed
  10.293 -  show "ALL x:U. ALL a. a (*) x : U" 
  10.294 +  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" 
  10.295    proof (intro ballI allI)
  10.296 -    fix x a assume "x:U" show "a (*) x : U" by (simp!)
  10.297 +    fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!)
  10.298    qed
  10.299  qed
  10.300  
  10.301 @@ -264,38 +264,38 @@
  10.302    ==> is_subspace (U + V) E"
  10.303  proof 
  10.304    assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"
  10.305 -  show "00 : U + V"
  10.306 +  show "0 \<in> U + V"
  10.307    proof (intro vs_sumI)
  10.308 -    show "00 : U" ..
  10.309 -    show "00 : V" ..
  10.310 -    show "(00::'a) = 00 + 00" by (simp!)
  10.311 +    show "0 \<in> U" ..
  10.312 +    show "0 \<in> V" ..
  10.313 +    show "(0::'a) = 0 + 0" by (simp!)
  10.314    qed
  10.315    
  10.316    show "U + V <= E"
  10.317    proof (intro subsetI, elim vs_sumE bexE)
  10.318 -    fix x u v assume "u : U" "v : V" "x = u + v"
  10.319 -    show "x:E" by (simp!)
  10.320 +    fix x u v assume "u \<in> U" "v \<in> V" "x = u + v"
  10.321 +    show "x \<in> E" by (simp!)
  10.322    qed
  10.323    
  10.324 -  show "ALL x: U + V. ALL y: U + V. x + y : U + V"
  10.325 +  show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V"
  10.326    proof (intro ballI)
  10.327 -    fix x y assume "x : U + V" "y : U + V"
  10.328 -    thus "x + y : U + V"
  10.329 +    fix x y assume "x \<in> U + V" "y \<in> U + V"
  10.330 +    thus "x + y \<in> U + V"
  10.331      proof (elim vs_sumE bexE, intro vs_sumI)
  10.332        fix ux vx uy vy 
  10.333 -      assume "ux : U" "vx : V" "x = ux + vx" 
  10.334 -	and "uy : U" "vy : V" "y = uy + vy"
  10.335 +      assume "ux \<in> U" "vx \<in> V" "x = ux + vx" 
  10.336 +	and "uy \<in> U" "vy \<in> V" "y = uy + vy"
  10.337        show "x + y = (ux + uy) + (vx + vy)" by (simp!)
  10.338      qed (simp!)+
  10.339    qed
  10.340  
  10.341 -  show "ALL x : U + V. ALL a. a (*) x : U + V"
  10.342 +  show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V"
  10.343    proof (intro ballI allI)
  10.344 -    fix x a assume "x : U + V"
  10.345 -    thus "a (*) x : U + V"
  10.346 +    fix x a assume "x \<in> U + V"
  10.347 +    thus "a \<cdot> x \<in> U + V"
  10.348      proof (elim vs_sumE bexE, intro vs_sumI)
  10.349 -      fix a x u v assume "u : U" "v : V" "x = u + v"
  10.350 -      show "a (*) x = (a (*) u) + (a (*) v)" 
  10.351 +      fix a x u v assume "u \<in> U" "v \<in> V" "x = u + v"
  10.352 +      show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" 
  10.353          by (simp! add: vs_add_mult_distrib1)
  10.354      qed (simp!)+
  10.355    qed
  10.356 @@ -323,154 +323,154 @@
  10.357  
  10.358  lemma decomp: 
  10.359    "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
  10.360 -  U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
  10.361 -  ==> u1 = u2 & v1 = v2" 
  10.362 +  U \<inter> V = {0}; u1 \<in> U; u2 \<in> U; v1 \<in> V; v2 \<in> V; u1 + v1 = u2 + v2 |] 
  10.363 +  ==> u1 = u2 \<and> v1 = v2" 
  10.364  proof 
  10.365    assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
  10.366 -    "U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V" 
  10.367 +    "U \<inter> V = {0}" "u1 \<in> U" "u2 \<in> U" "v1 \<in> V" "v2 \<in> V" 
  10.368      "u1 + v1 = u2 + v2" 
  10.369    have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap)
  10.370 -  have u: "u1 - u2 : U" by (simp!) 
  10.371 -  with eq have v': "v2 - v1 : U" by simp 
  10.372 -  have v: "v2 - v1 : V" by (simp!) 
  10.373 -  with eq have u': "u1 - u2 : V" by simp
  10.374 +  have u: "u1 - u2 \<in> U" by (simp!) 
  10.375 +  with eq have v': "v2 - v1 \<in> U" by simp 
  10.376 +  have v: "v2 - v1 \<in> V" by (simp!) 
  10.377 +  with eq have u': "u1 - u2 \<in> V" by simp
  10.378    
  10.379    show "u1 = u2"
  10.380    proof (rule vs_add_minus_eq)
  10.381 -    show "u1 - u2 = 00" by (rule Int_singletonD [OF _ u u']) 
  10.382 -    show "u1 : E" ..
  10.383 -    show "u2 : E" ..
  10.384 +    show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u']) 
  10.385 +    show "u1 \<in> E" ..
  10.386 +    show "u2 \<in> E" ..
  10.387    qed
  10.388  
  10.389    show "v1 = v2"
  10.390    proof (rule vs_add_minus_eq [RS sym])
  10.391 -    show "v2 - v1 = 00" by (rule Int_singletonD [OF _ v' v])
  10.392 -    show "v1 : E" ..
  10.393 -    show "v2 : E" ..
  10.394 +    show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
  10.395 +    show "v1 \<in> E" ..
  10.396 +    show "v2 \<in> E" ..
  10.397    qed
  10.398  qed
  10.399  
  10.400  text {* An application of the previous lemma will be used in the proof
  10.401 -of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any
  10.402 +of the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
  10.403  element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
  10.404  the linear closure of $x_0$ the components $y \in H$ and $a$ are
  10.405  uniquely determined. *}
  10.406  
  10.407 -lemma decomp_H0: 
  10.408 -  "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
  10.409 -  x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |]
  10.410 -  ==> y1 = y2 & a1 = a2"
  10.411 +lemma decomp_H': 
  10.412 +  "[| is_vectorspace E; is_subspace H E; y1 \<in> H; y2 \<in> H; 
  10.413 +  x' \<notin> H; x' \<in> E; x' \<noteq> 0; y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x' |]
  10.414 +  ==> y1 = y2 \<and> a1 = a2"
  10.415  proof
  10.416    assume "is_vectorspace E" and h: "is_subspace H E"
  10.417 -     and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00" 
  10.418 -         "y1 + a1 (*) x0 = y2 + a2 (*) x0"
  10.419 +     and "y1 \<in> H" "y2 \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 
  10.420 +         "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
  10.421  
  10.422 -  have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0"
  10.423 +  have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
  10.424    proof (rule decomp) 
  10.425 -    show "a1 (*) x0 : lin x0" .. 
  10.426 -    show "a2 (*) x0 : lin x0" ..
  10.427 -    show "H Int (lin x0) = {00}" 
  10.428 +    show "a1 \<cdot> x' \<in> lin x'" .. 
  10.429 +    show "a2 \<cdot> x' \<in> lin x'" ..
  10.430 +    show "H \<inter> (lin x') = {0}" 
  10.431      proof
  10.432 -      show "H Int lin x0 <= {00}" 
  10.433 +      show "H \<inter> lin x' <= {0}" 
  10.434        proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2])
  10.435 -        fix x assume "x:H" "x : lin x0" 
  10.436 -        thus "x = 00"
  10.437 +        fix x assume "x \<in> H" "x \<in> lin x'" 
  10.438 +        thus "x = 0"
  10.439          proof (unfold lin_def, elim CollectE exE conjE)
  10.440 -          fix a assume "x = a (*) x0"
  10.441 +          fix a assume "x = a \<cdot> x'"
  10.442            show ?thesis
  10.443            proof cases
  10.444              assume "a = (#0::real)" show ?thesis by (simp!)
  10.445            next
  10.446 -            assume "a ~= (#0::real)" 
  10.447 -            from h have "rinv a (*) a (*) x0 : H" 
  10.448 +            assume "a \<noteq> (#0::real)" 
  10.449 +            from h have "rinv a \<cdot> a \<cdot> x' \<in> H" 
  10.450                by (rule subspace_mult_closed) (simp!)
  10.451 -            also have "rinv a (*) a (*) x0 = x0" by (simp!)
  10.452 -            finally have "x0 : H" .
  10.453 +            also have "rinv a \<cdot> a \<cdot> x' = x'" by (simp!)
  10.454 +            finally have "x' \<in> H" .
  10.455              thus ?thesis by contradiction
  10.456            qed
  10.457         qed
  10.458        qed
  10.459 -      show "{00} <= H Int lin x0"
  10.460 +      show "{0} <= H \<inter> lin x'"
  10.461        proof -
  10.462 -	have "00: H Int lin x0"
  10.463 +	have "0 \<in> H \<inter> lin x'"
  10.464  	proof (rule IntI)
  10.465 -	  show "00:H" ..
  10.466 -	  from lin_vs show "00 : lin x0" ..
  10.467 +	  show "0 \<in> H" ..
  10.468 +	  from lin_vs show "0 \<in> lin x'" ..
  10.469  	qed
  10.470  	thus ?thesis by simp
  10.471        qed
  10.472      qed
  10.473 -    show "is_subspace (lin x0) E" ..
  10.474 +    show "is_subspace (lin x') E" ..
  10.475    qed
  10.476    
  10.477    from c show "y1 = y2" by simp
  10.478    
  10.479    show  "a1 = a2" 
  10.480    proof (rule vs_mult_right_cancel [RS iffD1])
  10.481 -    from c show "a1 (*) x0 = a2 (*) x0" by simp
  10.482 +    from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
  10.483    qed
  10.484  qed
  10.485  
  10.486 -text {* Since for any element $y + a \mult x_0$ of the direct sum 
  10.487 -of a vectorspace $H$ and the linear closure of $x_0$ the components
  10.488 +text {* Since for any element $y + a \mult x'$ of the direct sum 
  10.489 +of a vectorspace $H$ and the linear closure of $x'$ the components
  10.490  $y\in H$ and $a$ are unique, it follows from $y\in H$ that 
  10.491  $a = 0$.*} 
  10.492  
  10.493 -lemma decomp_H0_H: 
  10.494 -  "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
  10.495 -  x0 ~= 00 |] 
  10.496 -  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))"
  10.497 +lemma decomp_H'_H: 
  10.498 +  "[| is_vectorspace E; is_subspace H E; t \<in> H; x' \<notin> H; x' \<in> E;
  10.499 +  x' \<noteq> 0 |] 
  10.500 +  ==> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))"
  10.501  proof (rule, unfold split_tupled_all)
  10.502 -  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
  10.503 -    "x0 ~= 00"
  10.504 +  assume "is_vectorspace E" "is_subspace H E" "t \<in> H" "x' \<notin> H" "x' \<in> E"
  10.505 +    "x' \<noteq> 0"
  10.506    have h: "is_vectorspace H" ..
  10.507 -  fix y a presume t1: "t = y + a (*) x0" and "y:H"
  10.508 -  have "y = t & a = (#0::real)" 
  10.509 -    by (rule decomp_H0) (assumption | (simp!))+
  10.510 +  fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H"
  10.511 +  have "y = t \<and> a = (#0::real)" 
  10.512 +    by (rule decomp_H') (assumption | (simp!))+
  10.513    thus "(y, a) = (t, (#0::real))" by (simp!)
  10.514  qed (simp!)+
  10.515  
  10.516 -text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
  10.517 -are unique, so the function $h_0$ defined by 
  10.518 -$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *}
  10.519 +text {* The components $y\in H$ and $a$ in $y \plus a \mult x'$ 
  10.520 +are unique, so the function $h'$ defined by 
  10.521 +$h' (y \plus a \mult x') = h y + a \cdot \xi$ is definite. *}
  10.522  
  10.523 -lemma h0_definite:
  10.524 -  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
  10.525 +lemma h'_definite:
  10.526 +  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
  10.527                  in (h y) + a * xi);
  10.528 -  x = y + a (*) x0; is_vectorspace E; is_subspace H E;
  10.529 -  y:H; x0 ~: H; x0:E; x0 ~= 00 |]
  10.530 -  ==> h0 x = h y + a * xi"
  10.531 +  x = y + a \<cdot> x'; is_vectorspace E; is_subspace H E;
  10.532 +  y \<in> H; x' \<notin> H; x' \<in> E; x' \<noteq> 0 |]
  10.533 +  ==> h' x = h y + a * xi"
  10.534  proof -  
  10.535    assume 
  10.536 -    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
  10.537 +    "h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
  10.538                 in (h y) + a * xi)"
  10.539 -    "x = y + a (*) x0" "is_vectorspace E" "is_subspace H E"
  10.540 -    "y:H" "x0 ~: H" "x0:E" "x0 ~= 00"
  10.541 -  have "x : H + (lin x0)" 
  10.542 +    "x = y + a \<cdot> x'" "is_vectorspace E" "is_subspace H E"
  10.543 +    "y \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
  10.544 +  have "x \<in> H + (lin x')" 
  10.545      by (simp! add: vs_sum_def lin_def) force+
  10.546 -  have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)" 
  10.547 +  have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" 
  10.548    proof
  10.549 -    show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"
  10.550 +    show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
  10.551        by (force!)
  10.552    next
  10.553      fix xa ya
  10.554 -    assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa"
  10.555 -           "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya"
  10.556 +    assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa"
  10.557 +           "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya"
  10.558      show "xa = ya" 
  10.559      proof -
  10.560 -      show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" 
  10.561 +      show "fst xa = fst ya \<and> snd xa = snd ya ==> xa = ya" 
  10.562          by (simp add: Pair_fst_snd_eq)
  10.563 -      have x: "x = fst xa + snd xa (*) x0 & fst xa : H" 
  10.564 +      have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H" 
  10.565          by (force!)
  10.566 -      have y: "x = fst ya + snd ya (*) x0 & fst ya : H" 
  10.567 +      have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H" 
  10.568          by (force!)
  10.569 -      from x y show "fst xa = fst ya & snd xa = snd ya" 
  10.570 -        by (elim conjE) (rule decomp_H0, (simp!)+)
  10.571 +      from x y show "fst xa = fst ya \<and> snd xa = snd ya" 
  10.572 +        by (elim conjE) (rule decomp_H', (simp!)+)
  10.573      qed
  10.574    qed
  10.575 -  hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)" 
  10.576 +  hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
  10.577      by (rule select1_equality) (force!)
  10.578 -  thus "h0 x = h y + a * xi" by (simp! add: Let_def)
  10.579 +  thus "h' x = h y + a * xi" by (simp! add: Let_def)
  10.580  qed
  10.581  
  10.582  end
  10.583 \ No newline at end of file
    11.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Jul 16 21:00:32 2000 +0200
    11.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Jul 17 13:58:18 2000 +0200
    11.3 @@ -15,24 +15,11 @@
    11.4  element $\zero$ is defined. *}
    11.5  
    11.6  consts
    11.7 -  prod  :: "[real, 'a] => 'a"                       (infixr "'(*')" 70)
    11.8 -  zero  :: 'a                                       ("00")
    11.9 +  prod  :: "[real, 'a::{plus, minus, zero}] => 'a"        (infixr "'(*')" 70)
   11.10  
   11.11  syntax (symbols)
   11.12 -  prod  :: "[real, 'a] => 'a"                       (infixr "\<prod>" 70)
   11.13 -  zero  :: 'a                                       ("\<zero>")
   11.14 -
   11.15 -(* text {* The unary and binary minus can be considered as 
   11.16 -abbreviations: *}
   11.17 -*)
   11.18 +  prod  :: "[real, 'a] => 'a"                       (infixr "\<cdot>" 70)
   11.19  
   11.20 -(***
   11.21 -constdefs 
   11.22 -  negate :: "'a => 'a"                           ("- _" [100] 100)
   11.23 -  "- x == (- #1) ( * ) x"
   11.24 -  diff :: "'a => 'a => 'a"                       (infixl "-" 68)
   11.25 -  "x - y == x + - y";
   11.26 -***)
   11.27  
   11.28  subsection {* Vector space laws *}
   11.29  
   11.30 @@ -47,43 +34,43 @@
   11.31  *}
   11.32  
   11.33  constdefs
   11.34 -  is_vectorspace :: "('a::{plus,minus}) set => bool"
   11.35 -  "is_vectorspace V == V ~= {} 
   11.36 -   & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
   11.37 -        x + y : V                                 
   11.38 -      & a (*) x : V                                 
   11.39 -      & (x + y) + z = x + (y + z)             
   11.40 -      & x + y = y + x                           
   11.41 -      & x - x = 00                               
   11.42 -      & 00 + x = x                               
   11.43 -      & a (*) (x + y) = a (*) x + a (*) y       
   11.44 -      & (a + b) (*) x = a (*) x + b (*) x         
   11.45 -      & (a * b) (*) x = a (*) b (*) x               
   11.46 -      & #1 (*) x = x
   11.47 -      & - x = (- #1) (*) x
   11.48 -      & x - y = x + - y)"                             
   11.49 +  is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
   11.50 +  "is_vectorspace V == V \<noteq> {}
   11.51 +   \<and> (\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. \<forall>a b.
   11.52 +        x + y \<in> V                                 
   11.53 +      \<and> a \<cdot> x \<in> V                                 
   11.54 +      \<and> (x + y) + z = x + (y + z)             
   11.55 +      \<and> x + y = y + x                           
   11.56 +      \<and> x - x = 0                               
   11.57 +      \<and> 0 + x = x                               
   11.58 +      \<and> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y       
   11.59 +      \<and> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x         
   11.60 +      \<and> (a * b) \<cdot> x = a \<cdot> b \<cdot> x               
   11.61 +      \<and> #1 \<cdot> x = x
   11.62 +      \<and> - x = (- #1) \<cdot> x
   11.63 +      \<and> x - y = x + - y)"                             
   11.64  
   11.65  text_raw {* \medskip *}
   11.66  text {* The corresponding introduction rule is:*}
   11.67  
   11.68  lemma vsI [intro]:
   11.69 -  "[| 00:V; 
   11.70 -  ALL x:V. ALL y:V. x + y : V; 
   11.71 -  ALL x:V. ALL a. a (*) x : V;  
   11.72 -  ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
   11.73 -  ALL x:V. ALL y:V. x + y = y + x;
   11.74 -  ALL x:V. x - x = 00;
   11.75 -  ALL x:V. 00 + x = x;
   11.76 -  ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
   11.77 -  ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
   11.78 -  ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x; 
   11.79 -  ALL x:V. #1 (*) x = x; 
   11.80 -  ALL x:V. - x = (- #1) (*) x; 
   11.81 -  ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V"
   11.82 +  "[| 0 \<in> V; 
   11.83 +  \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V; 
   11.84 +  \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V;  
   11.85 +  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z);
   11.86 +  \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x;
   11.87 +  \<forall>x \<in> V. x - x = 0;
   11.88 +  \<forall>x \<in> V. 0 + x = x;
   11.89 +  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y;
   11.90 +  \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x;
   11.91 +  \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x; 
   11.92 +  \<forall>x \<in> V. #1 \<cdot> x = x; 
   11.93 +  \<forall>x \<in> V. - x = (- #1) \<cdot> x; 
   11.94 +  \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y |] ==> is_vectorspace V"
   11.95  proof (unfold is_vectorspace_def, intro conjI ballI allI)
   11.96    fix x y z 
   11.97 -  assume "x:V" "y:V" "z:V"
   11.98 -    "ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)"
   11.99 +  assume "x \<in> V" "y \<in> V" "z \<in> V"
  11.100 +    "\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. x + y + z = x + (y + z)"
  11.101    thus "x + y + z =  x + (y + z)" by (elim bspec[elimify])
  11.102  qed force+
  11.103  
  11.104 @@ -91,58 +78,58 @@
  11.105  text {* The corresponding destruction rules are: *}
  11.106  
  11.107  lemma negate_eq1: 
  11.108 -  "[| is_vectorspace V; x:V |] ==> - x = (- #1) (*) x"
  11.109 +  "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
  11.110    by (unfold is_vectorspace_def) simp
  11.111  
  11.112  lemma diff_eq1: 
  11.113 -  "[| is_vectorspace V; x:V; y:V |] ==> x - y = x + - y"
  11.114 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y = x + - y"
  11.115    by (unfold is_vectorspace_def) simp 
  11.116  
  11.117  lemma negate_eq2: 
  11.118 -  "[| is_vectorspace V; x:V |] ==> (- #1) (*) x = - x"
  11.119 +  "[| is_vectorspace V; x \<in> V |] ==> (- #1) \<cdot> x = - x"
  11.120    by (unfold is_vectorspace_def) simp
  11.121  
  11.122  lemma negate_eq2a: 
  11.123 -  "[| is_vectorspace V; x:V |] ==> #-1 (*) x = - x"
  11.124 +  "[| is_vectorspace V; x \<in> V |] ==> #-1 \<cdot> x = - x"
  11.125    by (unfold is_vectorspace_def) simp
  11.126  
  11.127  lemma diff_eq2: 
  11.128 -  "[| is_vectorspace V; x:V; y:V |] ==> x + - y = x - y"
  11.129 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + - y = x - y"
  11.130    by (unfold is_vectorspace_def) simp  
  11.131  
  11.132 -lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V ~= {})" 
  11.133 +lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \<noteq> {})" 
  11.134    by (unfold is_vectorspace_def) simp
  11.135   
  11.136  lemma vs_add_closed [simp, intro??]: 
  11.137 -  "[| is_vectorspace V; x:V; y:V |] ==> x + y : V" 
  11.138 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + y \<in> V" 
  11.139    by (unfold is_vectorspace_def) simp
  11.140  
  11.141  lemma vs_mult_closed [simp, intro??]: 
  11.142 -  "[| is_vectorspace V; x:V |] ==> a (*) x : V" 
  11.143 +  "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> x \<in> V" 
  11.144    by (unfold is_vectorspace_def) simp
  11.145  
  11.146  lemma vs_diff_closed [simp, intro??]: 
  11.147 - "[| is_vectorspace V; x:V; y:V |] ==> x - y : V"
  11.148 + "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y \<in> V"
  11.149    by (simp add: diff_eq1 negate_eq1)
  11.150  
  11.151  lemma vs_neg_closed  [simp, intro??]: 
  11.152 -  "[| is_vectorspace V; x:V |] ==> - x : V"
  11.153 +  "[| is_vectorspace V; x \<in> V |] ==> - x \<in> V"
  11.154    by (simp add: negate_eq1)
  11.155  
  11.156  lemma vs_add_assoc [simp]:  
  11.157 -  "[| is_vectorspace V; x:V; y:V; z:V |]
  11.158 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
  11.159     ==> (x + y) + z = x + (y + z)"
  11.160    by (unfold is_vectorspace_def) fast
  11.161  
  11.162  lemma vs_add_commute [simp]: 
  11.163 -  "[| is_vectorspace V; x:V; y:V |] ==> y + x = x + y"
  11.164 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> y + x = x + y"
  11.165    by (unfold is_vectorspace_def) simp
  11.166  
  11.167  lemma vs_add_left_commute [simp]:
  11.168 -  "[| is_vectorspace V; x:V; y:V; z:V |] 
  11.169 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  11.170    ==> x + (y + z) = y + (x + z)"
  11.171  proof -
  11.172 -  assume "is_vectorspace V" "x:V" "y:V" "z:V"
  11.173 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
  11.174    hence "x + (y + z) = (x + y) + z" 
  11.175      by (simp only: vs_add_assoc)
  11.176    also have "... = (y + x) + z" by (simp! only: vs_add_commute)
  11.177 @@ -153,78 +140,78 @@
  11.178  theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
  11.179  
  11.180  lemma vs_diff_self [simp]: 
  11.181 -  "[| is_vectorspace V; x:V |] ==>  x - x = 00" 
  11.182 +  "[| is_vectorspace V; x \<in> V |] ==>  x - x = 0" 
  11.183    by (unfold is_vectorspace_def) simp
  11.184  
  11.185  text {* The existence of the zero element of a vector space
  11.186  follows from the non-emptiness of carrier set. *}
  11.187  
  11.188 -lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V"
  11.189 +lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \<in> V"
  11.190  proof - 
  11.191    assume "is_vectorspace V"
  11.192 -  have "V ~= {}" ..
  11.193 -  hence "EX x. x:V" by force
  11.194 +  have "V \<noteq> {}" ..
  11.195 +  hence "\<exists>x. x \<in> V" by force
  11.196    thus ?thesis 
  11.197    proof 
  11.198 -    fix x assume "x:V" 
  11.199 -    have "00 = x - x" by (simp!)
  11.200 -    also have "... : V" by (simp! only: vs_diff_closed)
  11.201 +    fix x assume "x \<in> V" 
  11.202 +    have "0 = x - x" by (simp!)
  11.203 +    also have "... \<in> V" by (simp! only: vs_diff_closed)
  11.204      finally show ?thesis .
  11.205    qed
  11.206  qed
  11.207  
  11.208  lemma vs_add_zero_left [simp]: 
  11.209 -  "[| is_vectorspace V; x:V |] ==>  00 + x = x"
  11.210 +  "[| is_vectorspace V; x \<in> V |] ==>  0 + x = x"
  11.211    by (unfold is_vectorspace_def) simp
  11.212  
  11.213  lemma vs_add_zero_right [simp]: 
  11.214 -  "[| is_vectorspace V; x:V |] ==>  x + 00 = x"
  11.215 +  "[| is_vectorspace V; x \<in> V |] ==>  x + 0 = x"
  11.216  proof -
  11.217 -  assume "is_vectorspace V" "x:V"
  11.218 -  hence "x + 00 = 00 + x" by simp
  11.219 +  assume "is_vectorspace V" "x \<in> V"
  11.220 +  hence "x + 0 = 0 + x" by simp
  11.221    also have "... = x" by (simp!)
  11.222    finally show ?thesis .
  11.223  qed
  11.224  
  11.225  lemma vs_add_mult_distrib1: 
  11.226 -  "[| is_vectorspace V; x:V; y:V |] 
  11.227 -  ==> a (*) (x + y) = a (*) x + a (*) y"
  11.228 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
  11.229 +  ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
  11.230    by (unfold is_vectorspace_def) simp
  11.231  
  11.232  lemma vs_add_mult_distrib2: 
  11.233 -  "[| is_vectorspace V; x:V |] 
  11.234 -  ==> (a + b) (*) x = a (*) x + b (*) x" 
  11.235 +  "[| is_vectorspace V; x \<in> V |] 
  11.236 +  ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" 
  11.237    by (unfold is_vectorspace_def) simp
  11.238  
  11.239  lemma vs_mult_assoc: 
  11.240 -  "[| is_vectorspace V; x:V |] ==> (a * b) (*) x = a (*) (b (*) x)"
  11.241 +  "[| is_vectorspace V; x \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
  11.242    by (unfold is_vectorspace_def) simp
  11.243  
  11.244  lemma vs_mult_assoc2 [simp]: 
  11.245 - "[| is_vectorspace V; x:V |] ==> a (*) b (*) x = (a * b) (*) x"
  11.246 + "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
  11.247    by (simp only: vs_mult_assoc)
  11.248  
  11.249  lemma vs_mult_1 [simp]: 
  11.250 -  "[| is_vectorspace V; x:V |] ==> #1 (*) x = x" 
  11.251 +  "[| is_vectorspace V; x \<in> V |] ==> #1 \<cdot> x = x" 
  11.252    by (unfold is_vectorspace_def) simp
  11.253  
  11.254  lemma vs_diff_mult_distrib1: 
  11.255 -  "[| is_vectorspace V; x:V; y:V |] 
  11.256 -  ==> a (*) (x - y) = a (*) x - a (*) y"
  11.257 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
  11.258 +  ==> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
  11.259    by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1)
  11.260  
  11.261  lemma vs_diff_mult_distrib2: 
  11.262 -  "[| is_vectorspace V; x:V |] 
  11.263 -  ==> (a - b) (*) x = a (*) x - (b (*) x)"
  11.264 +  "[| is_vectorspace V; x \<in> V |] 
  11.265 +  ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
  11.266  proof -
  11.267 -  assume "is_vectorspace V" "x:V"
  11.268 -  have " (a - b) (*) x = (a + - b) (*) x" 
  11.269 +  assume "is_vectorspace V" "x \<in> V"
  11.270 +  have " (a - b) \<cdot> x = (a + - b) \<cdot> x" 
  11.271      by (unfold real_diff_def, simp)
  11.272 -  also have "... = a (*) x + (- b) (*) x" 
  11.273 +  also have "... = a \<cdot> x + (- b) \<cdot> x" 
  11.274      by (rule vs_add_mult_distrib2)
  11.275 -  also have "... = a (*) x + - (b (*) x)" 
  11.276 +  also have "... = a \<cdot> x + - (b \<cdot> x)" 
  11.277      by (simp! add: negate_eq1)
  11.278 -  also have "... = a (*) x - (b (*) x)" 
  11.279 +  also have "... = a \<cdot> x - (b \<cdot> x)" 
  11.280      by (simp! add: diff_eq1)
  11.281    finally show ?thesis .
  11.282  qed
  11.283 @@ -234,40 +221,40 @@
  11.284  text{* Further derived laws: *}
  11.285  
  11.286  lemma vs_mult_zero_left [simp]: 
  11.287 -  "[| is_vectorspace V; x:V |] ==> #0 (*) x = 00"
  11.288 +  "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
  11.289  proof -
  11.290 -  assume "is_vectorspace V" "x:V"
  11.291 -  have  "#0 (*) x = (#1 - #1) (*) x" by simp
  11.292 -  also have "... = (#1 + - #1) (*) x" by simp
  11.293 -  also have "... =  #1 (*) x + (- #1) (*) x" 
  11.294 +  assume "is_vectorspace V" "x \<in> V"
  11.295 +  have  "#0 \<cdot> x = (#1 - #1) \<cdot> x" by simp
  11.296 +  also have "... = (#1 + - #1) \<cdot> x" by simp
  11.297 +  also have "... =  #1 \<cdot> x + (- #1) \<cdot> x" 
  11.298      by (rule vs_add_mult_distrib2)
  11.299 -  also have "... = x + (- #1) (*) x" by (simp!)
  11.300 +  also have "... = x + (- #1) \<cdot> x" by (simp!)
  11.301    also have "... = x + - x" by (simp! add: negate_eq2a)
  11.302    also have "... = x - x" by (simp! add: diff_eq2)
  11.303 -  also have "... = 00" by (simp!)
  11.304 +  also have "... = 0" by (simp!)
  11.305    finally show ?thesis .
  11.306  qed
  11.307  
  11.308  lemma vs_mult_zero_right [simp]: 
  11.309 -  "[| is_vectorspace (V:: 'a::{plus, minus} set) |] 
  11.310 -  ==> a (*) 00 = (00::'a)"
  11.311 +  "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |] 
  11.312 +  ==> a \<cdot> 0 = (0::'a)"
  11.313  proof -
  11.314    assume "is_vectorspace V"
  11.315 -  have "a (*) 00 = a (*) (00 - (00::'a))" by (simp!)
  11.316 -  also have "... =  a (*) 00 - a (*) 00"
  11.317 +  have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
  11.318 +  also have "... =  a \<cdot> 0 - a \<cdot> 0"
  11.319       by (rule vs_diff_mult_distrib1) (simp!)+
  11.320 -  also have "... = 00" by (simp!)
  11.321 +  also have "... = 0" by (simp!)
  11.322    finally show ?thesis .
  11.323  qed
  11.324  
  11.325  lemma vs_minus_mult_cancel [simp]:  
  11.326 -  "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) x"
  11.327 +  "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> x"
  11.328    by (simp add: negate_eq1)
  11.329  
  11.330  lemma vs_add_minus_left_eq_diff: 
  11.331 -  "[| is_vectorspace V; x:V; y:V |] ==> - x + y = y - x"
  11.332 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + y = y - x"
  11.333  proof - 
  11.334 -  assume "is_vectorspace V" "x:V" "y:V"
  11.335 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V"
  11.336    have "- x + y = y + - x" 
  11.337      by (simp! add: vs_add_commute [RS sym, of V "- x"])
  11.338    also have "... = y - x" by (simp! add: diff_eq1)
  11.339 @@ -275,63 +262,63 @@
  11.340  qed
  11.341  
  11.342  lemma vs_add_minus [simp]: 
  11.343 -  "[| is_vectorspace V; x:V |] ==> x + - x = 00"
  11.344 +  "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
  11.345    by (simp! add: diff_eq2)
  11.346  
  11.347  lemma vs_add_minus_left [simp]: 
  11.348 -  "[| is_vectorspace V; x:V |] ==> - x + x = 00"
  11.349 +  "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
  11.350    by (simp! add: diff_eq2)
  11.351  
  11.352  lemma vs_minus_minus [simp]: 
  11.353 -  "[| is_vectorspace V; x:V |] ==> - (- x) = x"
  11.354 +  "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
  11.355    by (simp add: negate_eq1)
  11.356  
  11.357  lemma vs_minus_zero [simp]: 
  11.358 -  "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00" 
  11.359 +  "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0" 
  11.360    by (simp add: negate_eq1)
  11.361  
  11.362  lemma vs_minus_zero_iff [simp]:
  11.363 -  "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)" 
  11.364 +  "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)" 
  11.365    (concl is "?L = ?R")
  11.366  proof -
  11.367 -  assume "is_vectorspace V" "x:V"
  11.368 +  assume "is_vectorspace V" "x \<in> V"
  11.369    show "?L = ?R"
  11.370    proof
  11.371      have "x = - (- x)" by (rule vs_minus_minus [RS sym])
  11.372      also assume ?L
  11.373 -    also have "- ... = 00" by (rule vs_minus_zero)
  11.374 +    also have "- ... = 0" by (rule vs_minus_zero)
  11.375      finally show ?R .
  11.376    qed (simp!)
  11.377  qed
  11.378  
  11.379  lemma vs_add_minus_cancel [simp]:  
  11.380 -  "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y" 
  11.381 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y" 
  11.382    by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
  11.383  
  11.384  lemma vs_minus_add_cancel [simp]: 
  11.385 -  "[| is_vectorspace V; x:V; y:V |] ==> - x + (x + y) = y" 
  11.386 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y" 
  11.387    by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
  11.388  
  11.389  lemma vs_minus_add_distrib [simp]:  
  11.390 -  "[| is_vectorspace V; x:V; y:V |] 
  11.391 +  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
  11.392    ==> - (x + y) = - x + - y"
  11.393    by (simp add: negate_eq1 vs_add_mult_distrib1)
  11.394  
  11.395  lemma vs_diff_zero [simp]: 
  11.396 -  "[| is_vectorspace V; x:V |] ==> x - 00 = x"
  11.397 +  "[| is_vectorspace V; x \<in> V |] ==> x - 0 = x"
  11.398    by (simp add: diff_eq1)  
  11.399  
  11.400  lemma vs_diff_zero_right [simp]: 
  11.401 -  "[| is_vectorspace V; x:V |] ==> 00 - x = - x"
  11.402 +  "[| is_vectorspace V; x \<in> V |] ==> 0 - x = - x"
  11.403    by (simp add:diff_eq1)
  11.404  
  11.405  lemma vs_add_left_cancel:
  11.406 -  "[| is_vectorspace V; x:V; y:V; z:V |] 
  11.407 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  11.408     ==> (x + y = x + z) = (y = z)"  
  11.409    (concl is "?L = ?R")
  11.410  proof
  11.411 -  assume "is_vectorspace V" "x:V" "y:V" "z:V"
  11.412 -  have "y = 00 + y" by (simp!)
  11.413 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
  11.414 +  have "y = 0 + y" by (simp!)
  11.415    also have "... = - x + x + y" by (simp!)
  11.416    also have "... = - x + (x + y)" 
  11.417      by (simp! only: vs_add_assoc vs_neg_closed)
  11.418 @@ -343,68 +330,67 @@
  11.419  qed force
  11.420  
  11.421  lemma vs_add_right_cancel: 
  11.422 -  "[| is_vectorspace V; x:V; y:V; z:V |] 
  11.423 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  11.424    ==> (y + x = z + x) = (y = z)"  
  11.425    by (simp only: vs_add_commute vs_add_left_cancel)
  11.426  
  11.427  lemma vs_add_assoc_cong: 
  11.428 -  "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] 
  11.429 +  "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |] 
  11.430    ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
  11.431    by (simp only: vs_add_assoc [RS sym]) 
  11.432  
  11.433  lemma vs_mult_left_commute: 
  11.434 -  "[| is_vectorspace V; x:V; y:V; z:V |] 
  11.435 -  ==> x (*) y (*) z = y (*) x (*) z"  
  11.436 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  11.437 +  ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"  
  11.438    by (simp add: real_mult_commute)
  11.439  
  11.440 -lemma vs_mult_zero_uniq :
  11.441 -  "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = #0"
  11.442 +lemma vs_mult_zero_uniq:
  11.443 +  "[| is_vectorspace V; x \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
  11.444  proof (rule classical)
  11.445 -  assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00"
  11.446 -  assume "a ~= #0"
  11.447 -  have "x = (rinv a * a) (*) x" by (simp!)
  11.448 -  also have "... = rinv a (*) (a (*) x)" by (rule vs_mult_assoc)
  11.449 -  also have "... = rinv a (*) 00" by (simp!)
  11.450 -  also have "... = 00" by (simp!)
  11.451 -  finally have "x = 00" .
  11.452 +  assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
  11.453 +  assume "a \<noteq> #0"
  11.454 +  have "x = (rinv a * a) \<cdot> x" by (simp!)
  11.455 +  also have "... = rinv a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
  11.456 +  also have "... = rinv a \<cdot> 0" by (simp!)
  11.457 +  also have "... = 0" by (simp!)
  11.458 +  finally have "x = 0" .
  11.459    thus "a = #0" by contradiction 
  11.460  qed
  11.461  
  11.462  lemma vs_mult_left_cancel: 
  11.463 -  "[| is_vectorspace V; x:V; y:V; a ~= #0 |] ==> 
  11.464 -  (a (*) x = a (*) y) = (x = y)"
  11.465 +  "[| is_vectorspace V; x \<in> V; y \<in> V; a \<noteq> #0 |] ==> 
  11.466 +  (a \<cdot> x = a \<cdot> y) = (x = y)"
  11.467    (concl is "?L = ?R")
  11.468  proof
  11.469 -  assume "is_vectorspace V" "x:V" "y:V" "a ~= #0"
  11.470 -  have "x = #1 (*) x" by (simp!)
  11.471 -  also have "... = (rinv a * a) (*) x" by (simp!)
  11.472 -  also have "... = rinv a (*) (a (*) x)" 
  11.473 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "a \<noteq> #0"
  11.474 +  have "x = #1 \<cdot> x" by (simp!)
  11.475 +  also have "... = (rinv a * a) \<cdot> x" by (simp!)
  11.476 +  also have "... = rinv a \<cdot> (a \<cdot> x)" 
  11.477      by (simp! only: vs_mult_assoc)
  11.478    also assume ?L
  11.479 -  also have "rinv a (*) ... = y" by (simp!)
  11.480 +  also have "rinv a \<cdot> ... = y" by (simp!)
  11.481    finally show ?R .
  11.482  qed simp
  11.483  
  11.484  lemma vs_mult_right_cancel: (*** forward ***)
  11.485 -  "[| is_vectorspace V; x:V; x ~= 00 |] 
  11.486 -  ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R")
  11.487 +  "[| is_vectorspace V; x \<in> V; x \<noteq> 0 |] 
  11.488 +  ==> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
  11.489  proof
  11.490 -  assume "is_vectorspace V" "x:V" "x ~= 00"
  11.491 -  have "(a - b) (*) x = a (*) x - b (*) x" 
  11.492 +  assume "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
  11.493 +  have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x" 
  11.494      by (simp! add: vs_diff_mult_distrib2)
  11.495 -  also assume ?L hence "a (*) x - b (*) x = 00" by (simp!)
  11.496 -  finally have "(a - b) (*) x = 00" . 
  11.497 +  also assume ?L hence "a \<cdot> x - b \<cdot> x = 0" by (simp!)
  11.498 +  finally have "(a - b) \<cdot> x = 0" . 
  11.499    hence "a - b = #0" by (simp! add: vs_mult_zero_uniq)
  11.500    thus "a = b" by (rule real_add_minus_eq)
  11.501  qed simp (*** 
  11.502  
  11.503 -backward :
  11.504  lemma vs_mult_right_cancel: 
  11.505 -  "[| is_vectorspace V; x:V; x ~= 00 |] ==>  
  11.506 +  "[| is_vectorspace V; x:V; x \<noteq> 0 |] ==>  
  11.507    (a ( * ) x = b ( * ) x) = (a = b)"
  11.508    (concl is "?L = ?R");
  11.509  proof;
  11.510 -  assume "is_vectorspace V" "x:V" "x ~= 00";
  11.511 +  assume "is_vectorspace V" "x:V" "x \<noteq> 0";
  11.512    assume l: ?L; 
  11.513    show "a = b"; 
  11.514    proof (rule real_add_minus_eq);
  11.515 @@ -412,8 +398,8 @@
  11.516      proof (rule vs_mult_zero_uniq);
  11.517        have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
  11.518          by (simp! add: vs_diff_mult_distrib2);
  11.519 -      also; from l; have "a ( * ) x - b ( * ) x = 00"; by (simp!);
  11.520 -      finally; show "(a - b) ( * ) x  = 00"; .; 
  11.521 +      also; from l; have "a ( * ) x - b ( * ) x = 0"; by (simp!);
  11.522 +      finally; show "(a - b) ( * ) x  = 0"; .; 
  11.523      qed;
  11.524    qed;
  11.525  next;
  11.526 @@ -423,11 +409,11 @@
  11.527  **)
  11.528  
  11.529  lemma vs_eq_diff_eq: 
  11.530 -  "[| is_vectorspace V; x:V; y:V; z:V |] ==> 
  11.531 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] ==> 
  11.532    (x = z - y) = (x + y = z)"
  11.533    (concl is "?L = ?R" )  
  11.534  proof -
  11.535 -  assume vs: "is_vectorspace V" "x:V" "y:V" "z:V"
  11.536 +  assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
  11.537    show "?L = ?R"   
  11.538    proof
  11.539      assume ?L
  11.540 @@ -435,7 +421,7 @@
  11.541      also have "... = z + - y + y" by (simp! add: diff_eq1)
  11.542      also have "... = z + (- y + y)" 
  11.543        by (rule vs_add_assoc) (simp!)+
  11.544 -    also from vs have "... = z + 00" 
  11.545 +    also from vs have "... = z + 0" 
  11.546        by (simp only: vs_add_minus_left)
  11.547      also from vs have "... = z" by (simp only: vs_add_zero_right)
  11.548      finally show ?R .
  11.549 @@ -452,32 +438,32 @@
  11.550  qed
  11.551  
  11.552  lemma vs_add_minus_eq_minus: 
  11.553 -  "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y" 
  11.554 +  "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y" 
  11.555  proof -
  11.556 -  assume "is_vectorspace V" "x:V" "y:V" 
  11.557 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V" 
  11.558    have "x = (- y + y) + x" by (simp!)
  11.559    also have "... = - y + (x + y)" by (simp!)
  11.560 -  also assume "x + y = 00"
  11.561 -  also have "- y + 00 = - y" by (simp!)
  11.562 +  also assume "x + y = 0"
  11.563 +  also have "- y + 0 = - y" by (simp!)
  11.564    finally show "x = - y" .
  11.565  qed
  11.566  
  11.567  lemma vs_add_minus_eq: 
  11.568 -  "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y" 
  11.569 +  "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y" 
  11.570  proof -
  11.571 -  assume "is_vectorspace V" "x:V" "y:V" "x - y = 00"
  11.572 -  assume "x - y = 00"
  11.573 -  hence e: "x + - y = 00" by (simp! add: diff_eq1)
  11.574 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "x - y = 0"
  11.575 +  assume "x - y = 0"
  11.576 +  hence e: "x + - y = 0" by (simp! add: diff_eq1)
  11.577    with _ _ _ have "x = - (- y)" 
  11.578      by (rule vs_add_minus_eq_minus) (simp!)+
  11.579    thus "x = y" by (simp!)
  11.580  qed
  11.581  
  11.582  lemma vs_add_diff_swap:
  11.583 -  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d |] 
  11.584 +  "[| is_vectorspace V; a \<in> V; b \<in> V; c \<in> V; d \<in> V; a + b = c + d |] 
  11.585    ==> a - c = d - b"
  11.586  proof - 
  11.587 -  assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" 
  11.588 +  assume vs: "is_vectorspace V" "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V" 
  11.589      and eq: "a + b = c + d"
  11.590    have "- c + (a + b) = - c + (c + d)" 
  11.591      by (simp! add: vs_add_left_cancel)
  11.592 @@ -487,16 +473,16 @@
  11.593      by (simp add: vs_add_ac diff_eq1)
  11.594    also from eq have "...  = d + - b" 
  11.595      by (simp! add: vs_add_right_cancel)
  11.596 -  also have "... = d - b" by (simp! add : diff_eq2)
  11.597 +  also have "... = d - b" by (simp! add: diff_eq2)
  11.598    finally show "a - c = d - b" .
  11.599  qed
  11.600  
  11.601  lemma vs_add_cancel_21: 
  11.602 -  "[| is_vectorspace V; x:V; y:V; z:V; u:V |] 
  11.603 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V; u \<in> V |] 
  11.604    ==> (x + (y + z) = y + u) = ((x + z) = u)"
  11.605    (concl is "?L = ?R") 
  11.606  proof - 
  11.607 -  assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V"
  11.608 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
  11.609    show "?L = ?R"
  11.610    proof
  11.611      have "x + z = - y + y + (x + z)" by (simp!)
  11.612 @@ -510,20 +496,20 @@
  11.613  qed
  11.614  
  11.615  lemma vs_add_cancel_end: 
  11.616 -  "[| is_vectorspace V;  x:V; y:V; z:V |] 
  11.617 +  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  11.618    ==> (x + (y + z) = y) = (x = - z)"
  11.619    (concl is "?L = ?R" )
  11.620  proof -
  11.621 -  assume "is_vectorspace V" "x:V" "y:V" "z:V"
  11.622 +  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
  11.623    show "?L = ?R"
  11.624    proof
  11.625      assume l: ?L
  11.626 -    have "x + z = 00" 
  11.627 +    have "x + z = 0" 
  11.628      proof (rule vs_add_left_cancel [RS iffD1])
  11.629        have "y + (x + z) = x + (y + z)" by (simp!)
  11.630        also note l
  11.631 -      also have "y = y + 00" by (simp!)
  11.632 -      finally show "y + (x + z) = y + 00" .
  11.633 +      also have "y = y + 0" by (simp!)
  11.634 +      finally show "y + (x + z) = y + 0" .
  11.635      qed (simp!)+
  11.636      thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
  11.637    next