The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
authorwenzelm
Fri Sep 10 17:28:51 1999 +0200 (1999-09-10)
changeset 7535599d3414b51d
parent 7534 30344dde83ab
child 7536 5c094aec523d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);
src/HOL/IsaMakefile
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/HahnBanach_h0_lemmas.thy
src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy
src/HOL/Real/HahnBanach/LinearSpace.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/ROOT.ML
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/Zorn_Lemma.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 09 19:01:37 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 10 17:28:51 1999 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
     1.5    HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.6    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
     1.7 -  TLA-Inc TLA-Buffer TLA-Memory
     1.8 +  HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
     1.9  
    1.10  all: images test
    1.11  
    1.12 @@ -94,6 +94,21 @@
    1.13  	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
    1.14  
    1.15  
    1.16 +## HOL-Real-HahnBanach
    1.17 +
    1.18 +HOL-Real-HahnBanach: HOL-Real $(LOG)/HOL-Real-HahnBanach.gz
    1.19 +
    1.20 +$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy	\
    1.21 +  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
    1.22 +  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
    1.23 +  Real/HahnBanach/HahnBanach_h0_lemmas.thy				\
    1.24 +  Real/HahnBanach/HahnBanach_lemmas.thy					\
    1.25 +  Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy	\
    1.26 +  Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML		\
    1.27 +  Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy
    1.28 +	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
    1.29 +
    1.30 +
    1.31  ## HOL-Subst
    1.32  
    1.33  HOL-Subst: HOL $(LOG)/HOL-Subst.gz
    1.34 @@ -406,4 +421,5 @@
    1.35  	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
    1.36  	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
    1.37  	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
    1.38 -	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz
    1.39 +	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz \
    1.40 +	  $(LOG)/HOL-Real-HahnBanach.gz
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Fri Sep 10 17:28:51 1999 +0200
     2.3 @@ -0,0 +1,134 @@
     2.4 +
     2.5 +theory Aux = Main + Real:;
     2.6 +
     2.7 +
     2.8 +theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y";	    (*  <=  ~=  < *)
     2.9 +  by (asm_simp add: order_less_le);
    2.10 +
    2.11 +lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; 
    2.12 +  by (rule order_less_le[RS iffD1, RS conjunct2]);
    2.13 +
    2.14 +lemma Int_singeltonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
    2.15 +  by (fast elim: equalityE);
    2.16 +
    2.17 +lemma real_add_minus_eq: "x - y = 0r ==> x = y";
    2.18 +proof -;
    2.19 +  assume "x - y = 0r";
    2.20 +  have "x + - y = x - y"; by simp;
    2.21 +  also; have "... = 0r"; .;
    2.22 +  finally; have "x + - y = 0r"; .;
    2.23 +  hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
    2.24 +  also; have "... = y"; by asm_simp;
    2.25 +  finally; show "x = y"; .;
    2.26 +qed;
    2.27 +
    2.28 +lemma rabs_minus_one: "rabs (- 1r) = 1r"; 
    2.29 +proof -; 
    2.30 +  have "rabs (- 1r) = - (- 1r)"; 
    2.31 +  proof (rule rabs_minus_eqI2);
    2.32 +    show "-1r < 0r";
    2.33 +      by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
    2.34 +  qed;
    2.35 +  also; have "... = 1r"; by asm_simp; 
    2.36 +  finally; show ?thesis; by asm_simp;
    2.37 +qed;
    2.38 +
    2.39 +axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
    2.40 +
    2.41 +axioms real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x";
    2.42 +
    2.43 +axioms real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
    2.44 +
    2.45 +axioms real_mult_diff_distrib: "a * (- x - y) = - a * x - a * y";
    2.46 +
    2.47 +axioms real_mult_diff_distrib2: "a * (x - y) = a * x - a * y";
    2.48 +
    2.49 +lemma less_imp_le: "(x::real) < y ==> x <= y";
    2.50 +  by (asm_simp only: real_less_imp_le);
    2.51 +
    2.52 +lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
    2.53 +proof -;
    2.54 +  assume "x <= (r::'a::order)";
    2.55 +  assume "x ~= r";
    2.56 +  then; have "x < r | x = r";
    2.57 +    by (asm_simp add: order_le_less);
    2.58 +  then; show ?thesis;
    2.59 +    by asm_simp;
    2.60 +qed;
    2.61 +
    2.62 +lemma minus_le: "- (x::real) <= y ==> - y <= x";
    2.63 +proof -; 
    2.64 +  assume "- x <= y";
    2.65 +  hence "- x < y | - x = y"; by (rule order_le_less [RS iffD1]);
    2.66 +  thus "-y <= x";
    2.67 +  proof;
    2.68 +     assume "- x < y"; show ?thesis; 
    2.69 +     proof -; 
    2.70 +       have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]); 
    2.71 +       hence "- y < x"; by asm_simp;
    2.72 +       thus ?thesis; by (rule real_less_imp_le);
    2.73 +    qed;
    2.74 +  next; 
    2.75 +     assume "- x = y"; show ?thesis; by force;
    2.76 +  qed;
    2.77 +qed;
    2.78 +
    2.79 +lemma rabs_interval_iff_1: "(rabs (x::real) <= r) = (-r <= x & x <= r)";
    2.80 +proof (rule case [of "rabs x = r"]);
    2.81 +  assume  a: "rabs x = r";
    2.82 +  show ?thesis; 
    2.83 +  proof;
    2.84 +    assume "rabs x <= r";
    2.85 +    show "- r <= x & x <= r";
    2.86 +    proof;
    2.87 +      have "- x <= rabs x"; by (rule rabs_ge_minus_self);
    2.88 +      hence "- x <= r"; by asm_simp;
    2.89 +      thus "- r <= x"; by (asm_simp add : minus_le [of "x" "r"]);
    2.90 +      have "x <= rabs x"; by (rule rabs_ge_self); 
    2.91 +      thus "x <= r"; by asm_simp; 
    2.92 +    qed;
    2.93 +  next; 
    2.94 +    assume "- r <= x & x <= r";
    2.95 +    show "rabs x <= r";  by fast;  
    2.96 +  qed;
    2.97 +next;   
    2.98 +  assume "rabs x ~= r";
    2.99 +  show ?thesis; 
   2.100 +  proof;
   2.101 +    assume "rabs x <= r"; 
   2.102 +    have "rabs x < r"; by (rule conjI [RS real_less_le [RS iffD2]]);
   2.103 +    hence "- r < x & x < r"; by (rule rabs_interval_iff [RS iffD1]);
   2.104 +    thus "- r <= x & x <= r";
   2.105 +    proof(elim conjE, intro conjI); 
   2.106 +      assume "- r < x";
   2.107 +      show "- r <= x"; by (rule real_less_imp_le); 
   2.108 +      assume "x < r";
   2.109 +      show "x <= r"; by (rule real_less_imp_le); 
   2.110 +    qed;
   2.111 +  next;
   2.112 +    assume "- r <= x & x <= r";
   2.113 +    thus "rabs x <= r";
   2.114 +    proof; 
   2.115 +      assume "- r <= x" "x <= r";
   2.116 +      show ?thesis; 
   2.117 +      proof (rule rabs_disj [RS disjE, of x]);
   2.118 +        assume  "rabs x = x";
   2.119 +        show ?thesis; by asm_simp; 
   2.120 +      next; 
   2.121 +        assume "rabs x = - x";
   2.122 +        from minus_le [of r x]; show ?thesis; by asm_simp;
   2.123 +      qed;
   2.124 +    qed;
   2.125 +  qed;
   2.126 +qed;
   2.127 +
   2.128 +lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
   2.129 +proof- ;
   2.130 +  assume "H < E ";
   2.131 +  have le: "H <= E"; by (rule conjunct1 [OF psubset_eq[RS iffD1]]);
   2.132 +  have ne: "H ~= E";  by (rule conjunct2 [OF psubset_eq[RS iffD1]]);
   2.133 +  with le; show ?thesis; by force;
   2.134 +qed;
   2.135 +
   2.136 +
   2.137 +end;
   2.138 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Fri Sep 10 17:28:51 1999 +0200
     3.3 @@ -0,0 +1,105 @@
     3.4 +
     3.5 +theory Bounds = Main + Real:;
     3.6 +
     3.7 +
     3.8 +section {* The sets of lower and upper bounds *};
     3.9 +
    3.10 +constdefs
    3.11 +  is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
    3.12 +  "is_LowerBound A B == %x. x:A & (ALL y:B. x <= y)"
    3.13 +   
    3.14 +  LowerBounds :: "('a::order) set => 'a set => 'a set"
    3.15 +  "LowerBounds A B == Collect (is_LowerBound A B)"
    3.16 +
    3.17 +  is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
    3.18 +  "is_UpperBound A B == %x. x:A & (ALL y:B. y <= x)"
    3.19 + 
    3.20 +  UpperBounds :: "('a::order) set => 'a set => 'a set"
    3.21 +  "UpperBounds A B == Collect (is_UpperBound A B)";
    3.22 +
    3.23 +syntax
    3.24 +  "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3UPPER'_BOUNDS _:_./ _)" 10)
    3.25 +  "_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3UPPER'_BOUNDS _./ _)" 10)
    3.26 +  "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3LOWER'_BOUNDS _:_./ _)" 10)
    3.27 +  "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3LOWER'_BOUNDS _./ _)" 10);
    3.28 +
    3.29 +translations
    3.30 +  "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (%x. P))"
    3.31 +  "UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
    3.32 +  "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (%x. P))"
    3.33 +  "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P";
    3.34 +
    3.35 +
    3.36 +section {* Least and greatest elements *};
    3.37 +
    3.38 +constdefs
    3.39 +  is_Least :: "('a::order) set => 'a => bool"
    3.40 +  "is_Least B == is_LowerBound B B"
    3.41 +
    3.42 +  Least :: "('a::order) set => 'a"
    3.43 +  "Least B == Eps (is_Least B)"
    3.44 +
    3.45 +  is_Greatest :: "('a::order) set => 'a => bool"
    3.46 +  "is_Greatest B == is_UpperBound B B"
    3.47 +
    3.48 +  Greatest :: "('a::order) set => 'a" 
    3.49 +  "Greatest B == Eps (is_Greatest B)";
    3.50 +
    3.51 +syntax
    3.52 +  "_LEAST"    :: "[pttrn, 'a => bool] => 'a"   ("(3LLEAST _./ _)" 10)
    3.53 +  "_GREATEST" :: "[pttrn, 'a => bool] => 'a"   ("(3GREATEST _./ _)" 10);
    3.54 +
    3.55 +translations
    3.56 +  "LLEAST x. P" == "Least {x. P}"
    3.57 +  "GREATEST x. P" == "Greatest {x. P}";
    3.58 +
    3.59 +
    3.60 +section {* Inf and Sup *};
    3.61 +
    3.62 +constdefs
    3.63 +  is_Sup :: "('a::order) set => 'a set => 'a => bool"
    3.64 +  "is_Sup A B x == isLub A B x"
    3.65 +   
    3.66 +  (* was:  x:A & is_Least (UpperBounds A B) x" *)
    3.67 +
    3.68 +  Sup :: "('a::order) set => 'a set => 'a"
    3.69 +  "Sup A B == Eps (is_Sup A B)"
    3.70 +
    3.71 +  is_Inf :: "('a::order) set => 'a set => 'a => bool"  
    3.72 +  "is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"
    3.73 +
    3.74 +  Inf :: "('a::order) set => 'a set => 'a"
    3.75 +  "Inf A B == Eps (is_Inf A B)";
    3.76 +
    3.77 +syntax
    3.78 +  "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3SUP _:_./ _)" 10)
    3.79 +  "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3SUP _./ _)" 10)
    3.80 +  "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3INF _:_./ _)" 10)
    3.81 +  "_INF_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3INF _./ _)" 10);
    3.82 +
    3.83 +translations
    3.84 +  "SUP x:A. P" == "Sup A (Collect (%x. P))"
    3.85 +  "SUP x. P" == "SUP x:UNIV. P"
    3.86 +  "INF x:A. P" == "Inf A (Collect (%x. P))"
    3.87 +  "INF x. P" == "INF x:UNIV. P";
    3.88 +
    3.89 +
    3.90 +lemma [intro]: "[| x:A; !!y. y:B ==> y <= x |] ==> x: UpperBounds A B";
    3.91 +  by (unfold UpperBounds_def is_UpperBound_def) force;
    3.92 +
    3.93 +lemma ub_ge_sup: "isUb A B y ==> is_Sup A B s ==> s <= y";
    3.94 +  by (unfold is_Sup_def, rule isLub_le_isUb);
    3.95 +
    3.96 +lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
    3.97 +  by (unfold is_Sup_def, rule isLubD2);
    3.98 +
    3.99 +lemma sup_ub1: "ALL y:B. a <= y ==> is_Sup A B s ==> x:B ==> a <= s";
   3.100 +proof -; 
   3.101 +  assume "ALL y:B. a <= y" "is_Sup A B s" "x:B";
   3.102 +  have "a <= x"; by (rule bspec);
   3.103 +  also; have "x <= s"; by (rule sup_ub);
   3.104 +  finally; show "a <= s"; .;
   3.105 +qed;
   3.106 +  
   3.107 +
   3.108 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 10 17:28:51 1999 +0200
     4.3 @@ -0,0 +1,222 @@
     4.4 +
     4.5 +theory FunctionNorm = NormedSpace + FunctionOrder:;
     4.6 +
     4.7 +
     4.8 +theorems [elim!!] = bspec;
     4.9 +
    4.10 +constdefs
    4.11 +  is_continous :: "['a set, 'a => real, 'a => real] => bool" 
    4.12 +  "is_continous V norm f == (is_linearform V f
    4.13 +                           & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
    4.14 +
    4.15 +lemma lipschitz_continous_I: 
    4.16 +  "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] 
    4.17 +  ==> is_continous V norm f";
    4.18 +proof (unfold is_continous_def, intro exI conjI ballI);
    4.19 +  assume r: "!! x. x:V ==> rabs (f x) <= c * norm x"; 
    4.20 +  fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
    4.21 +qed;
    4.22 +  
    4.23 +lemma continous_linearform: "is_continous V norm f ==> is_linearform V f";
    4.24 +  by (unfold is_continous_def) force;
    4.25 +
    4.26 +lemma continous_bounded: "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
    4.27 +  by (unfold is_continous_def) force;
    4.28 +
    4.29 +constdefs
    4.30 +  B:: "[ 'a set, 'a => real, 'a => real ] => real set"
    4.31 +  "B V norm f == {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm (x)))}";
    4.32 +
    4.33 +constdefs 
    4.34 +  function_norm :: " ['a set, 'a => real, 'a => real] => real"
    4.35 +  "function_norm V norm f == 
    4.36 +     Sup UNIV (B V norm f)";
    4.37 +
    4.38 +constdefs 
    4.39 +  is_function_norm :: " ['a set, 'a => real, 'a => real] => real => bool"
    4.40 +  "is_function_norm V norm f fn == 
    4.41 +     is_Sup UNIV (B V norm f) fn";
    4.42 +
    4.43 +lemma B_not_empty: "0r : B V norm f";
    4.44 +  by (unfold B_def, force);
    4.45 +
    4.46 +lemma le_max1: "x <= max x (y::'a::linorder)";
    4.47 +  by (simp add: le_max_iff_disj[of x x y]);
    4.48 +
    4.49 +lemma le_max2: "y <= max x (y::'a::linorder)"; 
    4.50 +  by (simp add: le_max_iff_disj[of y x y]);
    4.51 +
    4.52 +lemma ex_fnorm: 
    4.53 +  "[| is_normed_vectorspace V norm; is_continous V norm f|]
    4.54 +     ==> is_function_norm V norm f (function_norm V norm f)"; 
    4.55 +proof (unfold function_norm_def is_function_norm_def is_continous_def Sup_def, elim conjE, 
    4.56 +    rule selectI2EX);
    4.57 +  assume "is_normed_vectorspace V norm";
    4.58 +  assume "is_linearform V f" and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
    4.59 +  show  "EX a. is_Sup UNIV (B V norm f) a"; 
    4.60 +  proof (unfold is_Sup_def, rule reals_complete);
    4.61 +    show "EX X. X : B V norm f"; 
    4.62 +    proof (intro exI);
    4.63 +      show "0r : (B V norm f)"; by (unfold B_def, force);
    4.64 +    qed;
    4.65 +
    4.66 +    from e; show "EX Y. isUb UNIV (B V norm f) Y";
    4.67 +    proof;
    4.68 +      fix c; assume a: "ALL x:V. rabs (f x) <= c * norm x";
    4.69 +      def b == "max c 0r";
    4.70 +
    4.71 +      show "EX Y. isUb UNIV (B V norm f) Y";
    4.72 +      proof (intro exI isUbI setleI ballI, unfold B_def, 
    4.73 +	elim CollectD [elimify] disjE bexE conjE);
    4.74 +	fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)";
    4.75 +        from a; have le: "rabs (f x) <= c * norm x"; ..;
    4.76 +        have "y = rabs (f x) * rinv (norm x)";.;
    4.77 +        also; from _  le; have "... <= c * norm x * rinv (norm x)";
    4.78 +        proof (rule real_mult_le_le_mono2);
    4.79 +          show "0r <= rinv (norm x)";
    4.80 +            by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero);
    4.81 +        qed;
    4.82 +        also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
    4.83 +        also; have "(norm x * rinv (norm x)) = 1r"; 
    4.84 +        proof (rule real_mult_inv_right);
    4.85 +          show "norm x ~= 0r"; 
    4.86 +            by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero);
    4.87 +        qed;
    4.88 +        also; have "c * ... = c"; by asm_simp;
    4.89 +        also; have "... <= b"; by (asm_simp add: le_max1);
    4.90 +	finally; show "y <= b"; .;
    4.91 +      next; 
    4.92 +	fix y; assume "y = 0r"; show "y <= b"; by (asm_simp add: le_max2);
    4.93 +      qed simp;
    4.94 +    qed;
    4.95 +  qed;
    4.96 +qed;
    4.97 +
    4.98 +lemma fnorm_ge_zero: "[| is_continous V norm f; is_normed_vectorspace V norm|]
    4.99 +   ==> 0r <= function_norm V norm f";
   4.100 +proof -;
   4.101 +  assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
   4.102 +  have "is_function_norm V norm f (function_norm V norm f)"; by (rule ex_fnorm);
   4.103 +  hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)"; 
   4.104 +    by (simp add: is_function_norm_def);
   4.105 +  show ?thesis; 
   4.106 +  proof (unfold function_norm_def, rule sup_ub1);
   4.107 +    show "ALL x:(B V norm f). 0r <= x"; 
   4.108 +    proof (intro ballI, unfold B_def, elim CollectD [elimify] bexE conjE disjE);
   4.109 +      fix x r; assume "is_normed_vectorspace V norm" "x : V" "x ~= <0>" 
   4.110 +        "r = rabs (f x) * rinv (norm x)"; 
   4.111 +      show  "0r <= r";
   4.112 +      proof (asm_simp, rule real_le_mult_order);
   4.113 +        show "0r <= rabs (f x)"; by (asm_simp only: rabs_ge_zero);
   4.114 +        show "0r <= rinv (norm x)";
   4.115 +        proof (rule less_imp_le);
   4.116 +          show "0r < rinv (norm x)"; 
   4.117 +            by (rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero [of V norm]);
   4.118 +        qed;
   4.119 +      qed;
   4.120 +    qed asm_simp;
   4.121 +    from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
   4.122 +      by (asm_simp add: is_function_norm_def function_norm_def); 
   4.123 +    show "0r : B V norm f"; by (rule B_not_empty);
   4.124 +  qed;
   4.125 +qed;
   4.126 +  
   4.127 +
   4.128 +lemma norm_fx_le_norm_f_norm_x: 
   4.129 +  "[| is_normed_vectorspace V norm; x:V; is_continous V norm f |] 
   4.130 +    ==> rabs (f x) <= (function_norm V norm f) * norm x"; 
   4.131 +proof -; 
   4.132 +  assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
   4.133 +  have v: "is_vectorspace V"; by (rule normed_vs_vs);
   4.134 +  assume "x:V";
   4.135 +  show "?thesis";
   4.136 +  proof (rule case [of "x = <0>"]);
   4.137 +    assume "x ~= <0>";
   4.138 +    show "?thesis";
   4.139 +    proof -;
   4.140 +      have n: "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
   4.141 +      have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f"; 
   4.142 +        proof (unfold function_norm_def, rule sup_ub);
   4.143 +          from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
   4.144 +             by (asm_simp add: is_function_norm_def function_norm_def); 
   4.145 +          show "rabs (f x) * rinv (norm x) : B V norm f"; 
   4.146 +            by (unfold B_def, intro CollectI disjI2 bexI [of _ x] conjI, simp);
   4.147 +        qed;
   4.148 +      have "rabs (f x) = rabs (f x) * 1r"; by asm_simp;
   4.149 +      also; have "1r = rinv (norm x) * norm x"; 
   4.150 +        by (rule real_mult_inv_left [RS sym], rule lt_imp_not_eq[RS not_sym], 
   4.151 +              rule normed_vs_norm_gt_zero[of V norm]);
   4.152 +      also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x"; 
   4.153 +        by (asm_simp add: real_mult_assoc [of "rabs (f x)"]);
   4.154 +      also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x"; 
   4.155 +        by (rule real_mult_le_le_mono2 [OF n le]);
   4.156 +      finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
   4.157 +    qed;
   4.158 +  next; 
   4.159 +    assume "x = <0>";
   4.160 +    then; show "?thesis";
   4.161 +    proof -;
   4.162 +      have "rabs (f x) = rabs (f <0>)"; by asm_simp;
   4.163 +      also; have "f <0> = 0r"; by (rule linearform_zero [OF v continous_linearform]); 
   4.164 +      also; note rabs_zero;
   4.165 +      also; have" 0r <= function_norm V norm f * norm x";
   4.166 +      proof (rule real_le_mult_order);
   4.167 +        show "0r <= function_norm V norm f"; by (rule fnorm_ge_zero);
   4.168 +        show "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
   4.169 +      qed;
   4.170 +      finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
   4.171 +    qed;
   4.172 +  qed;
   4.173 +qed;
   4.174 +
   4.175 +
   4.176 +
   4.177 +
   4.178 +lemma fnorm_le_ub: 
   4.179 +  "[| is_normed_vectorspace V norm; is_continous V norm f;
   4.180 +     ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
   4.181 +  ==> function_norm V norm f <= c";
   4.182 +proof (unfold function_norm_def);
   4.183 +  assume "is_normed_vectorspace V norm"; 
   4.184 +  assume c: "is_continous V norm f";
   4.185 +  assume fb: "ALL x:V. rabs (f x) <= c * norm x"
   4.186 +         and "0r <= c";
   4.187 +  show "Sup UNIV (B V norm f) <= c"; 
   4.188 +  proof (rule ub_ge_sup);
   4.189 +    from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
   4.190 +      by (asm_simp add: is_function_norm_def function_norm_def); 
   4.191 +    show "isUb UNIV (B V norm f) c";  
   4.192 +    proof (intro isUbI setleI ballI);
   4.193 +      fix y; assume "y: B V norm f";
   4.194 +      show le: "y <= c";
   4.195 +      proof (unfold B_def, elim CollectD [elimify] disjE bexE);
   4.196 +	fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
   4.197 +	assume x: "x : V";
   4.198 +	have lt: "0r < norm x";
   4.199 +	  by (asm_simp add: normed_vs_norm_gt_zero);
   4.200 +	hence "0r ~= norm x"; by (asm_simp add: order_less_imp_not_eq);
   4.201 +	hence neq: "norm x ~= 0r"; by (rule not_sym);
   4.202 +
   4.203 +	from lt; have "0r < rinv (norm x)";
   4.204 +	  by (asm_simp add: real_rinv_gt_zero);
   4.205 +	then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le);
   4.206 +
   4.207 +	from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
   4.208 +	also; from inv_leq; have "... <= c * norm x * rinv (norm x)";
   4.209 +	  proof (rule real_mult_le_le_mono2);
   4.210 +	    from fb x; show "rabs (f x) <= c * norm x"; ..;
   4.211 +	  qed;
   4.212 +	also; have "... <= c";
   4.213 +	  by (simp add: neq real_mult_assoc);
   4.214 +	finally; show ?thesis; .;
   4.215 +      next;
   4.216 +        assume "y = 0r";
   4.217 +        show "y <= c"; by force;
   4.218 +      qed;
   4.219 +    qed force;
   4.220 +  qed;
   4.221 +qed;
   4.222 +
   4.223 +
   4.224 +end;
   4.225 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Sep 10 17:28:51 1999 +0200
     5.3 @@ -0,0 +1,95 @@
     5.4 +
     5.5 +theory FunctionOrder = Subspace + Linearform:;
     5.6 +
     5.7 +
     5.8 +section {* Order on functions *};
     5.9 +
    5.10 +types 'a graph = "('a * real) set";
    5.11 +
    5.12 +constdefs
    5.13 +  graph :: "['a set, 'a => real] => 'a graph "
    5.14 +  "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* == {(x, f x). x:F} *)
    5.15 +
    5.16 +constdefs
    5.17 +  domain :: "'a graph => 'a set" 
    5.18 +  "domain g == {x. EX y. (x, y):g}";
    5.19 +
    5.20 +constdefs
    5.21 +  funct :: "'a graph => ('a => real)"
    5.22 +  "funct g == %x. (@ y. (x, y):g)";
    5.23 +
    5.24 +lemma graph_I: "x:F ==> (x, f x) : graph F f";
    5.25 +  by (unfold graph_def, intro CollectI exI) force;
    5.26 +
    5.27 +lemma graphD1: "(x, y): graph F f ==> x:F";
    5.28 +  by (unfold graph_def, elim CollectD [elimify] exE) force;
    5.29 +
    5.30 +lemma graph_domain_funct: "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
    5.31 +proof ( unfold domain_def, unfold funct_def, unfold graph_def, auto);
    5.32 +  fix a b; assume "(a, b) : g";
    5.33 +  show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
    5.34 +  show "EX y. (a, y) : g"; ..;
    5.35 +  assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y";
    5.36 +  show "b = (SOME y. (a, y) : g)";
    5.37 +  proof (rule select_equality [RS sym]);
    5.38 +    fix y; assume "(a, y):g"; show "y = b"; by (rule uniq);
    5.39 +  qed;
    5.40 +qed;
    5.41 +
    5.42 +lemma graph_lemma1: "x:F ==> EX t: (graph F f). t = (x, f x)";
    5.43 +  by (unfold graph_def, force);
    5.44 +
    5.45 +lemma graph_lemma2: "(x, y): graph H h ==> y = h x";
    5.46 +  by (unfold graph_def, elim CollectD [elimify] exE) force; 
    5.47 +
    5.48 +lemma graph_lemma3: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
    5.49 +  by (unfold graph_def, force);
    5.50 +
    5.51 +lemma graph_lemma4: "[| graph H h <= graph H' h' |] ==> H <= H'";
    5.52 +  by (unfold graph_def, force);
    5.53 +
    5.54 +lemma graph_lemma5: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
    5.55 +  by (unfold graph_def, force);
    5.56 +
    5.57 +
    5.58 +constdefs
    5.59 +  norm_prev_extensions :: 
    5.60 +   "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
    5.61 +  "norm_prev_extensions E p F f == {g. EX H h. graph H h = g 
    5.62 +                                             & is_linearform H h 
    5.63 +                                             & is_subspace H E
    5.64 +                                             & is_subspace F H
    5.65 +                                             & (graph F f <= graph H h)
    5.66 +                                             & (ALL x:H. h x <= p x)}";
    5.67 +                       
    5.68 +lemma norm_prev_extension_D:  
    5.69 +  "(g: norm_prev_extensions E p F f) ==> (EX H h. graph H h = g 
    5.70 +                                              & is_linearform H h 
    5.71 +                                              & is_subspace H E
    5.72 +                                              & is_subspace F H
    5.73 +                                              & (graph F f <= graph H h)
    5.74 +                                              & (ALL x:H. h x <= p x))";
    5.75 + by (unfold norm_prev_extensions_def) force;
    5.76 +
    5.77 +lemma norm_prev_extension_I2 [intro]:  
    5.78 +   "[| is_linearform H h;    
    5.79 +       is_subspace H E;
    5.80 +       is_subspace F H;
    5.81 +       (graph F f <= graph H h);
    5.82 +       (ALL x:H. h x <= p x) |]
    5.83 +   ==> (graph H h : norm_prev_extensions E p F f)";
    5.84 + by (unfold norm_prev_extensions_def) force;
    5.85 +
    5.86 +lemma norm_prev_extension_I [intro]:  
    5.87 +   "(EX H h. graph H h = g 
    5.88 +             & is_linearform H h    
    5.89 +             & is_subspace H E
    5.90 +             & is_subspace F H
    5.91 +             & (graph F f <= graph H h)
    5.92 +             & (ALL x:H. h x <= p x))
    5.93 +   ==> (g: norm_prev_extensions E p F f) ";
    5.94 + by (unfold norm_prev_extensions_def) force;
    5.95 +
    5.96 +
    5.97 +end;
    5.98 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Fri Sep 10 17:28:51 1999 +0200
     6.3 @@ -0,0 +1,434 @@
     6.4 +
     6.5 +theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
     6.6 +
     6.7 +
     6.8 +theorems [elim!!] = psubsetI;
     6.9 +
    6.10 +
    6.11 +theorem hahnbanach: 
    6.12 +  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
    6.13 +      ALL x:F. f x <= p x |]
    6.14 +  ==> EX h. is_linearform E h
    6.15 +          & (ALL x:F. h x = f x)
    6.16 +          & (ALL x:E. h x <= p x)";
    6.17 +proof -;
    6.18 +  assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
    6.19 +    and "ALL x:F. f x <= p x";
    6.20 +  def M_def: M == "norm_prev_extensions E p F f";
    6.21 + 
    6.22 +  have aM: "graph F f : norm_prev_extensions E p F f";
    6.23 +  proof (rule norm_prev_extension_I2);
    6.24 +    show "is_subspace F F"; by (rule subspace_refl, rule subspace_vs);
    6.25 +  qed blast+;
    6.26 +
    6.27 +
    6.28 +  sect {* Part I a of the proof of the Hahn-Banach Theorem, 
    6.29 +     H. Heuser, Funktionalanalysis, p.231 *};
    6.30 +
    6.31 +
    6.32 +  have "!! (c:: 'a graph set). c : chain M ==> EX x. x:c ==> (Union c) : M";  
    6.33 +  proof -;
    6.34 +    fix c; assume "c:chain M"; assume "EX x. x:c";
    6.35 +    show "(Union c) : M"; 
    6.36 +
    6.37 +    proof (unfold M_def, rule norm_prev_extension_I);
    6.38 +      show "EX (H::'a set) h::'a => real. graph H h = Union c
    6.39 +              & is_linearform H h 
    6.40 +              & is_subspace H E 
    6.41 +              & is_subspace F H 
    6.42 +              & (graph F f <= graph H h)
    6.43 +              & (ALL x::'a:H. h x <= p x)" (is "EX (H::'a set) h::'a => real. ?Q H h");
    6.44 +      proof;
    6.45 +        let ?H = "domain (Union c)";
    6.46 +	show "EX h. ?Q ?H h";
    6.47 +	proof;
    6.48 +	  let ?h = "funct (Union c)";
    6.49 +	  show "?Q ?H ?h";
    6.50 +	  proof (intro conjI);
    6.51 + 	    show a: "graph ?H ?h = Union c"; 
    6.52 +            proof (rule graph_domain_funct);
    6.53 +              fix x y z; assume "EX x. x : c" "(x, y) : Union c" "(x, z) : Union c";
    6.54 +              show "z = y"; by (rule sup_uniq);
    6.55 +            qed;
    6.56 +            
    6.57 +	    show "is_linearform ?H ?h";
    6.58 +              by (asm_simp add: sup_lf a);       
    6.59 +
    6.60 +	    show "is_subspace ?H E";
    6.61 +              by (rule sup_subE, rule a) asm_simp+;
    6.62 +
    6.63 +	    show "is_subspace F ?H";
    6.64 +              by (rule sup_supF, rule a) asm_simp+;
    6.65 +
    6.66 +	    show "graph F f <= graph ?H ?h";       
    6.67 +               by (rule sup_ext, rule a) asm_simp+;
    6.68 +
    6.69 +	    show "ALL x::'a:?H. ?h x <= p x"; 
    6.70 +               by (rule sup_norm_prev, rule a) asm_simp+;
    6.71 +	  qed;
    6.72 +	qed;
    6.73 +      qed;
    6.74 +    qed;
    6.75 +  qed;
    6.76 +      
    6.77 +  
    6.78 +  with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
    6.79 +    by (asm_simp add: Zorn's_Lemma);
    6.80 +  thus ?thesis;
    6.81 +  proof;
    6.82 +    fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x";
    6.83 + 
    6.84 +    have ex_Hh: "EX H h. graph H h = g 
    6.85 +                         & is_linearform H h 
    6.86 +                         & is_subspace H E 
    6.87 +                         & is_subspace F H
    6.88 +                         & (graph F f <= graph H h)
    6.89 +                         & (ALL x:H. h x <= p x) "; 
    6.90 +      by (asm_simp add: norm_prev_extension_D);
    6.91 +    thus ?thesis;
    6.92 +    proof (elim exE conjE);
    6.93 +      fix H h; assume "graph H h = g" "is_linearform (H::'a set) h"
    6.94 +	"is_subspace H E" "is_subspace F H"
    6.95 +        "(graph F f <= graph H h)"; assume h_bound: "ALL x:H. h x <= p x";
    6.96 +      show ?thesis; 
    6.97 +      proof;
    6.98 +        have h: "is_vectorspace H"; by (rule subspace_vs);
    6.99 +        have f: "is_vectorspace F"; by (rule subspace_vs);
   6.100 +
   6.101 +
   6.102 +        sect {* Part I a of the proof of the Hahn-Banach Theorem,
   6.103 +            H. Heuser, Funktionalanalysis, p.230 *};
   6.104 +
   6.105 +	have eq: "H = E"; 
   6.106 +	proof (rule classical);
   6.107 +          assume "H ~= E";
   6.108 +          show ?thesis; 
   6.109 +          proof -;
   6.110 +            have "EX x:M. g <= x & g ~= x";
   6.111 +            proof -;
   6.112 +	      have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
   6.113 +	      proof-;
   6.114 +                from subspace_subset [of H E]; have "H <= E"; ..;
   6.115 +                hence "H < E"; ..;
   6.116 +                hence "EX x0:E. x0~:H"; by (rule set_less_imp_diff_not_empty);
   6.117 +                thus ?thesis;
   6.118 +                proof;
   6.119 +                  fix x0; assume "x0:E" "x0~:H";
   6.120 +                  have x0:  "x0 ~= <0>";
   6.121 +                  proof (rule classical);
   6.122 +                    presume "x0 = <0>";
   6.123 +                    have "x0 : H"; by (asm_simp add: zero_in_vs [OF h]);
   6.124 +                    thus "x0 ~= <0>"; by contradiction;
   6.125 +                  qed force;
   6.126 +
   6.127 +       		  def H0_def: H0 == "vectorspace_sum H (lin x0)";
   6.128 +                  have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M"; 
   6.129 +                  proof -;
   6.130 +                    from h; have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi) 
   6.131 +                                   & (ALL y:H. xi <= p (y [+] x0) - h y)"; 
   6.132 +                    proof (rule ex_xi);
   6.133 +                      fix u v; assume "u:H" "v:H"; 
   6.134 +                      show "- p (u [+] x0) - h u <= p (v [+] x0) - h v";
   6.135 +                      proof -;
   6.136 +                        show "!! a b c d::real. d - b <= c + a ==> - a - b <= c - d";
   6.137 +                        proof -; (* arith *)
   6.138 +			  fix a b c d; assume "d - b <= c + (a::real)";
   6.139 +                          have "- a - b = d - b + (- d - a)"; by asm_simp;
   6.140 +                          also; have "... <= c + a + (- d - a)";
   6.141 +                            by (rule real_add_le_mono1);
   6.142 +                          also; have "... = c - d"; by asm_simp;
   6.143 +                          finally; show "- a - b <= c - d"; .;
   6.144 +                        qed;
   6.145 +                        show "h v - h u <= p (v [+] x0) + p (u [+] x0)"; 
   6.146 +                        proof -;
   6.147 +                          from h; have "h v - h u = h (v [-] u)";
   6.148 +                            by  (rule linearform_diff_linear [RS sym]);
   6.149 +                          also; have "... <= p (v [-] u)";
   6.150 +			  proof -;  
   6.151 +			    from h; have "v [-] u : H"; by asm_simp; 
   6.152 +                            with h_bound; show ?thesis; ..;
   6.153 +			  qed;
   6.154 +                          also; have "v [-] u  = x0 [+] [-] x0 [+] v [+] [-] u"; 
   6.155 +                            by (asm_simp add: vs_add_minus_eq_diff);
   6.156 +                          also; have "... = v [+] x0 [+] [-] (u [+] x0)"; 
   6.157 +                            by asm_simp;
   6.158 +                          also; have "... = (v [+] x0) [-] (u [+] x0)";  
   6.159 +                            by (asm_simp only: vs_add_minus_eq_diff);
   6.160 +                          also; have "p ... <= p (v [+] x0) + p (u [+] x0)"; 
   6.161 +                            by (rule quasinorm_diff_triangle_ineq) asm_simp+;
   6.162 +                          finally; show ?thesis; .;
   6.163 +                        qed;
   6.164 +                      qed;
   6.165 +                    qed;
   6.166 +                    
   6.167 +                    thus ?thesis;
   6.168 +                    proof (elim exE, intro exI conjI);
   6.169 +                      fix xi; assume a: "(ALL y:H. - p (y [+] x0) - h y <= xi) &
   6.170 +                                         (ALL y:H. xi <= p (y [+] x0) - h y)";
   6.171 +                      def h0_def: h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
   6.172 +                                            in (h y) + a * xi";
   6.173 +
   6.174 +	              have "graph H h <= graph H0 h0"; 
   6.175 +                      proof% (rule graph_lemma5);
   6.176 +                        fix t; assume "t:H"; 
   6.177 +                        show "h t = h0 t";
   6.178 +                        proof -;
   6.179 +                          have "(@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
   6.180 +                            by (rule lemma1, rule x0); 
   6.181 +                          thus ?thesis; by (asm_simp add: Let_def);
   6.182 +                        qed;
   6.183 +                      next;
   6.184 +                        show "H <= H0";
   6.185 +		        proof (rule subspace_subset);
   6.186 +			  show "is_subspace H H0";
   6.187 +			  proof (unfold H0_def, rule subspace_vs_sum1);
   6.188 +			    show "is_vectorspace H"; ..;
   6.189 +			    show "is_vectorspace (lin x0)"; ..;
   6.190 +			  qed;
   6.191 +			qed;
   6.192 +		      qed;
   6.193 +                      thus "g <= graph H0 h0"; by asm_simp;
   6.194 +
   6.195 +                      have "graph H h ~= graph H0 h0";
   6.196 +                      proof;
   6.197 +                        assume "graph H h = graph H0 h0";
   6.198 +                        have x1: "(x0, h0 x0) : graph H0 h0";
   6.199 +                        proof (rule graph_I);
   6.200 +                          show "x0:H0";
   6.201 +                          proof (unfold H0_def, rule vs_sum_I);
   6.202 +                            from h; show "<0> : H"; by (rule zero_in_vs);
   6.203 +                            show "x0 : lin x0"; by (rule x_lin_x);
   6.204 +                            show "x0 = <0> [+] x0"; by (rule vs_add_zero_left [RS sym]);
   6.205 +                          qed;
   6.206 +                        qed;
   6.207 +                        have "(x0, h0 x0) ~: graph H h";
   6.208 +                        proof;
   6.209 +                          assume "(x0, h0 x0) : graph H h";
   6.210 +                          have "x0:H"; by (rule graphD1);
   6.211 +                          thus "False"; by contradiction;
   6.212 +                        qed;
   6.213 +                        hence "(x0, h0 x0) ~: graph H0 h0"; by asm_simp;
   6.214 +                        with x1; show "False"; by contradiction;
   6.215 +                      qed;
   6.216 +                      thus "g ~= graph H0 h0"; by asm_simp;
   6.217 +
   6.218 +                      have "graph H0 h0 : norm_prev_extensions E p F f";
   6.219 +                      proof (rule norm_prev_extension_I2);
   6.220 +
   6.221 +                        show "is_linearform H0 h0";
   6.222 +                          by (rule h0_lf, rule x0) asm_simp+;
   6.223 +
   6.224 +                        show "is_subspace H0 E";
   6.225 +                        proof -;
   6.226 +                        have "is_subspace (vectorspace_sum H (lin x0)) E";
   6.227 +			  by (rule vs_sum_subspace, rule lin_subspace);
   6.228 +                          thus ?thesis; by asm_simp;
   6.229 +                        qed;
   6.230 +
   6.231 +                        show f_h0: "is_subspace F H0";
   6.232 +                        proof (rule subspace_trans [of F H H0]);
   6.233 +                          from h lin_vs; have "is_subspace H (vectorspace_sum H (lin x0))";
   6.234 +                            by (rule subspace_vs_sum1);
   6.235 +                          thus "is_subspace H H0"; by asm_simp;
   6.236 +                        qed;
   6.237 +
   6.238 +                        show "graph F f <= graph H0 h0";
   6.239 +                        proof(rule graph_lemma5);
   6.240 +                          fix x; assume "x:F";
   6.241 +                          show "f x = h0 x";
   6.242 +                          proof -;
   6.243 +                            have "x:H"; 
   6.244 +                            proof (rule subsetD);
   6.245 +                              show "F <= H"; by (rule subspace_subset);
   6.246 +                            qed;
   6.247 +                            have eq: "(@ (y, a). x = y [+] a [*] x0 & y : H) = (x, 0r)";
   6.248 +                              by (rule lemma1, rule x0) asm_simp+;
   6.249 + 
   6.250 +                            have "h0 x = (let (y,a) = @ (y,a). x = y [+] a [*] x0 & y : H
   6.251 +                                          in h y + a * xi)"; 
   6.252 +                              by asm_simp;
   6.253 +                            also; from eq; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
   6.254 +                              by simp;
   6.255 +                            also; have " ... = h x + 0r * xi";
   6.256 +                              by (asm_simp add: Let_def);
   6.257 +                            also; have "... = h x"; by asm_simp;
   6.258 +                            also; have "... = f x"; by (rule graph_lemma3 [RS sym, of F f H h]);
   6.259 +                            finally; show ?thesis; by (rule sym);
   6.260 +                          qed;
   6.261 +                        next;
   6.262 +                          from f_h0; show "F <= H0"; by (rule subspace_subset);
   6.263 +                        qed;
   6.264 +
   6.265 +                        show "ALL x:H0. h0 x <= p x";
   6.266 +                          by (rule h0_norm_prev, rule x0) (assumption | asm_simp)+;
   6.267 +                      qed;
   6.268 +                      thus "graph H0 h0 : M"; by asm_simp;
   6.269 +                    qed;
   6.270 +                  qed;
   6.271 +                  thus ?thesis; ..;
   6.272 +                qed;
   6.273 +              qed;
   6.274 +
   6.275 +              thus ?thesis;
   6.276 +                by (elim exE conjE, intro bexI conjI);
   6.277 +            qed;
   6.278 +            hence "~ (ALL x:M. g <= x --> g = x)"; by force;
   6.279 +            thus ?thesis; by contradiction;
   6.280 +          qed;
   6.281 +	qed; 
   6.282 +
   6.283 +        show "is_linearform E h & (ALL x:F. h x = f x) & (ALL x:E. h x <= p x)";
   6.284 +        proof (intro conjI); 
   6.285 +          from eq; show "is_linearform E h"; by asm_simp;
   6.286 +          show "ALL x:F. h x = f x"; by (intro ballI, rule graph_lemma3 [RS sym]); 
   6.287 +          from eq; show "ALL x:E. h x <= p x"; by force;
   6.288 +        qed;
   6.289 +      qed;  
   6.290 +    qed; 
   6.291 +  qed;
   6.292 +qed;
   6.293 +
   6.294 +
   6.295 +theorem rabs_hahnbanach:
   6.296 +  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
   6.297 +     ALL x:F. rabs (f x) <= p x |]
   6.298 + ==> EX g. is_linearform E g
   6.299 +         & (ALL x:F. g x = f x)
   6.300 +         & (ALL x:E. rabs (g x) <= p x)";
   6.301 +proof -; 
   6.302 +
   6.303 + sect {* Part I (for real linear spaces) of the proof of the Hahn-banach Theorem,
   6.304 +   H. Heuser, Funktionalanalysis, p.229 *};
   6.305 +
   6.306 +  assume e: "is_vectorspace E"; 
   6.307 +  assume "is_subspace F E" "is_quasinorm E p" "is_linearform F f" "ALL x:F. rabs (f x) <= p x";
   6.308 +  have "ALL x:F. f x <= p x";
   6.309 +    by (asm_simp only: rabs_ineq);
   6.310 +  hence  "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)";
   6.311 +    by (asm_simp only: hahnbanach);
   6.312 +  thus ?thesis;
   6.313 +  proof (elim exE conjE);
   6.314 +    fix g; assume "is_linearform E g" "ALL x:F. g x = f x" "ALL x:E. g x <= p x";
   6.315 +    show ?thesis;
   6.316 +    proof (intro exI conjI)+;
   6.317 +      from e; show "ALL x:E. rabs (g x) <= p x";
   6.318 +        by (asm_simp add: rabs_ineq [OF subspace_refl]);
   6.319 +    qed;
   6.320 +  qed;
   6.321 +qed;
   6.322 +
   6.323 +
   6.324 +theorem norm_hahnbanach:
   6.325 +  "[| is_normed_vectorspace E norm; is_subspace F E; is_linearform F f;
   6.326 +      is_continous F norm f |] 
   6.327 +  ==> EX g. is_linearform E g
   6.328 +         & is_continous E norm g 
   6.329 +         & (ALL x:F. g x = f x) 
   6.330 +         & function_norm E norm g = function_norm F norm f"
   6.331 +  (concl is "EX g::'a=>real. ?P g");
   6.332 +
   6.333 +proof -;
   6.334 +sect {* Proof of the Hahn-Banach Theorem for normed spaces,
   6.335 +   H. Heuser, Funktionalanalysis, p.232 *};
   6.336 +
   6.337 +  assume a: "is_normed_vectorspace E norm";
   6.338 +  assume b: "is_subspace F E" "is_linearform F f";
   6.339 +  assume c: "is_continous F norm f";
   6.340 +  hence e: "is_vectorspace E"; by (asm_simp add: normed_vs_vs);
   6.341 +  from _ e;
   6.342 +  have f: "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
   6.343 +  def p_def: p == "%x::'a. (function_norm F norm f) * norm x";
   6.344 +  
   6.345 +  let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. rabs (g x) <= p x)";
   6.346 +
   6.347 +  have q: "is_quasinorm E p";
   6.348 +  proof;
   6.349 +    fix x y a; assume "x:E" "y:E";
   6.350 +
   6.351 +    show "0r <= p x";
   6.352 +    proof (unfold p_def, rule real_le_mult_order);
   6.353 +      from c f; show "0r <= function_norm F norm f";
   6.354 +        by (rule fnorm_ge_zero);
   6.355 +      from a; show "0r <= norm x"; by (rule normed_vs_norm_ge_zero); 
   6.356 +    qed;
   6.357 +
   6.358 +    show "p (a [*] x) = (rabs a) * (p x)";
   6.359 +    proof -; 
   6.360 +      have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by asm_simp;
   6.361 +      also; from a; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
   6.362 +      also; have "(function_norm F norm f) * ... = rabs a * ((function_norm F norm f) * norm x)";
   6.363 +        by (asm_simp only: real_mult_left_commute);
   6.364 +      also; have "... = (rabs a) * (p x)"; by asm_simp;
   6.365 +      finally; show ?thesis; .;
   6.366 +    qed;
   6.367 +
   6.368 +    show "p (x [+] y) <= p x + p y";
   6.369 +    proof -;
   6.370 +      have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by asm_simp;
   6.371 +      also; have "... <=  (function_norm F norm f) * (norm x + norm y)";
   6.372 +      proof (rule real_mult_le_le_mono1);
   6.373 +        from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
   6.374 +        show "norm (x [+] y) <= norm x + norm y"; by (rule normed_vs_norm_triangle_ineq);
   6.375 +      qed;
   6.376 +      also; have "... = (function_norm F norm f) * (norm x) + (function_norm F norm f) * (norm y)";
   6.377 +        by (asm_simp only: real_add_mult_distrib2);
   6.378 +      finally; show ?thesis; by asm_simp;
   6.379 +    qed;
   6.380 +  qed;
   6.381 + 
   6.382 +  have "ALL x:F. rabs (f x) <= p x";
   6.383 +  proof;
   6.384 +    fix x; assume "x:F";
   6.385 +    from f; show "rabs (f x) <= p x"; by (asm_simp add: norm_fx_le_norm_f_norm_x);
   6.386 +  qed;
   6.387 +
   6.388 +  with e b q; have "EX g. ?P' g";
   6.389 +    by (asm_simp add: rabs_hahnbanach);
   6.390 +
   6.391 +  thus "?thesis";
   6.392 +  proof (elim exE conjE, intro exI conjI);
   6.393 +    fix g;
   6.394 +    assume "is_linearform E g" and a: "ALL x:F. g x = f x" and "ALL x:E. rabs (g x) <= p x";
   6.395 +    show ce: "is_continous E norm g";
   6.396 +    proof (rule lipschitz_continous_I);
   6.397 +      fix x; assume "x:E";
   6.398 +      show "rabs (g x) <= function_norm F norm f * norm x";
   6.399 +        by (rule bspec [of _ _ x], asm_simp);
   6.400 +    qed;
   6.401 +    show "function_norm E norm g = function_norm F norm f";
   6.402 +    proof (rule order_antisym);
   6.403 +      from _ ce; show "function_norm E norm g <= function_norm F norm f";
   6.404 +      proof (rule fnorm_le_ub);
   6.405 +        show "ALL x:E. rabs (g x) <=  function_norm F norm f * norm x";
   6.406 +        proof;
   6.407 +          fix x; assume "x:E"; 
   6.408 +          show "rabs (g x) <= function_norm F norm f * norm x";
   6.409 +            by (rule bspec [of _ _ x], asm_simp);
   6.410 +        qed;
   6.411 +        from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
   6.412 +      qed;
   6.413 +      show "function_norm F norm f <= function_norm E norm g"; 
   6.414 +      proof (rule fnorm_le_ub);
   6.415 +        show "ALL x:F. rabs (f x) <=  function_norm E norm g * norm x";
   6.416 +        proof;
   6.417 +          fix x; assume "x:F"; 
   6.418 +          from a; have "f x = g x"; by (rule bspec [of _ _ x, RS sym]);
   6.419 +          hence "rabs (f x) = rabs (g x)"; by simp;
   6.420 +          also; from _ _ ce; have "... <= function_norm E norm g * norm x"; 
   6.421 +          proof (rule norm_fx_le_norm_f_norm_x);
   6.422 +            show "x:E";
   6.423 +            proof (rule subsetD); 
   6.424 +              show "F<=E"; by (rule subspace_subset);
   6.425 +            qed;
   6.426 +          qed;
   6.427 +          finally; show "rabs (f x) <= function_norm E norm g * norm x"; .;
   6.428 +        qed;
   6.429 +        from _ e; show "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
   6.430 +        from ce; show "0r <= function_norm E norm g"; by (rule fnorm_ge_zero);
   6.431 +      qed;
   6.432 +    qed;
   6.433 +  qed;
   6.434 +qed;
   6.435 +
   6.436 +
   6.437 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy	Fri Sep 10 17:28:51 1999 +0200
     7.3 @@ -0,0 +1,358 @@
     7.4 +
     7.5 +theory HahnBanach_h0_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
     7.6 +
     7.7 +
     7.8 +theorems [intro!!] = zero_in_vs isLub_isUb;
     7.9 +
    7.10 +lemma ex_xi: "[| is_vectorspace F;  (!! u v. [| u:F; v:F |] ==> a u <= b v )|]
    7.11 +       ==> EX xi::real. (ALL y:F. (a::'a => real) y <= xi) & (ALL y:F. xi <= b y)"; 
    7.12 +proof -;
    7.13 +  assume "is_vectorspace F";
    7.14 +  assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
    7.15 +  have "EX t. isLub UNIV {s::real . EX u:F. s = a u} t";  
    7.16 +  proof (rule reals_complete);
    7.17 +    have "a <0> : {s. EX u:F. s = a u}"; by force;
    7.18 +    thus "EX X. X : {s. EX u:F. s = a u}"; ..;
    7.19 +
    7.20 +    show "EX Y. isUb UNIV {s. EX u:F. s = a u} Y"; 
    7.21 +    proof; 
    7.22 +      show "isUb UNIV {s. EX u:F. s = a u} (b <0>)";
    7.23 +      proof (intro isUbI setleI ballI, fast);
    7.24 +        fix y; assume "y : {s. EX u:F. s = a u}"; 
    7.25 +        show "y <= b <0>"; 
    7.26 +        proof -;
    7.27 +          have "EX u:F. y = a u"; by fast;
    7.28 +          thus ?thesis;
    7.29 +          proof;
    7.30 +            fix u; assume "u:F"; 
    7.31 +            assume "y = a u";
    7.32 +            also; have "a u <= b <0>"; 
    7.33 +            proof (rule r);
    7.34 +              show "<0> : F"; ..;
    7.35 +            qed;
    7.36 +            finally; show ?thesis;.;
    7.37 +          qed;
    7.38 +        qed;
    7.39 +      qed;
    7.40 +    qed;
    7.41 +  qed;
    7.42 +  thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)"; 
    7.43 +  proof (elim exE);
    7.44 +    fix t; assume "isLub UNIV {s::real . EX u:F. s = a u} t"; 
    7.45 +    show ?thesis;
    7.46 +    proof (intro exI conjI ballI); 
    7.47 +      fix y; assume "y:F";
    7.48 +      show "a y <= t";    
    7.49 +      proof (rule isUbD);  
    7.50 +        show"isUb UNIV {s. EX u:F. s = a u} t"; ..;
    7.51 +      qed fast;
    7.52 +    next;
    7.53 +      fix y; assume "y:F";
    7.54 +      show "t <= b y";  
    7.55 +      proof (intro isLub_le_isUb isUbI setleI);
    7.56 +        show "ALL ya : {s. EX u:F. s = a u}. ya <= b y"; 
    7.57 +        proof (intro ballI); 
    7.58 +          fix au; 
    7.59 +          assume "au : {s. EX u:F. s = a u} ";
    7.60 +          show "au <= b y";
    7.61 +          proof -; 
    7.62 +            have "EX u:F. au = a u"; by fast;
    7.63 +            thus "au <= b y";
    7.64 +            proof;
    7.65 +              fix u; assume "u:F";
    7.66 +              assume "au = a u";  
    7.67 +              also; have "... <= b y"; by (rule r);
    7.68 +              finally; show ?thesis; .;
    7.69 +            qed;
    7.70 +          qed;
    7.71 +        qed;
    7.72 +        show "b y : UNIV"; by fast;
    7.73 +      qed; 
    7.74 +    qed;
    7.75 +  qed;
    7.76 +qed;
    7.77 +
    7.78 +
    7.79 +theorems [dest!!] = vs_sumD linD;
    7.80 +
    7.81 +lemma h0_lf: 
    7.82 +  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
    7.83 +      H0 = vectorspace_sum H (lin x0); is_subspace H E; is_linearform H h; x0 ~: H; 
    7.84 +      x0 : E; x0 ~= <0>; is_vectorspace E |]
    7.85 +    ==> is_linearform H0 h0";
    7.86 +proof -;
    7.87 +  assume h0_def:  "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi)"
    7.88 +    and H0_def: "H0 = vectorspace_sum H (lin x0)"
    7.89 +    and [simp]: "is_subspace H E" "is_linearform H h" "x0 ~: H" "x0 ~= <0>"
    7.90 +    and [simp]: "x0 : E" "is_vectorspace E";
    7.91 +
    7.92 +  have h0: "is_vectorspace H0"; 
    7.93 +  proof (asm_simp, rule vs_sum_vs);
    7.94 +    show "is_subspace (lin x0) E"; by (rule lin_subspace); 
    7.95 +  qed simp+; 
    7.96 +
    7.97 +  show ?thesis;
    7.98 +  proof;
    7.99 +    fix x1 x2; assume "x1 : H0" "x2 : H0"; 
   7.100 +    have x1x2: "x1 [+] x2 : H0"; 
   7.101 +      by (rule vs_add_closed, rule h0);
   7.102 +  
   7.103 +    have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0  & y1 : H)"; 
   7.104 +      by (asm_simp add: vectorspace_sum_def lin_def) blast;
   7.105 +    have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)"; 
   7.106 +      by (asm_simp add: vectorspace_sum_def lin_def) blast;
   7.107 +    from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0  & y : H)";    
   7.108 +      by (asm_simp add: vectorspace_sum_def lin_def) force;
   7.109 +    from ex_x1 ex_x2 ex_x1x2;
   7.110 +    show "h0 (x1 [+] x2) = h0 x1 + h0 x2";
   7.111 +    proof (elim exE conjE);
   7.112 +      fix y1 y2 y a1 a2 a;
   7.113 +      assume "x1 = y1 [+] a1 [*] x0"        "y1 : H"
   7.114 +             "x2 = y2 [+] a2 [*] x0"        "y2 : H" 
   7.115 +             "x1 [+] x2 = y  [+] a  [*] x0" "y  : H"; 
   7.116 +
   7.117 +      have ya: "y1 [+] y2 = y & a1 + a2 = a"; 
   7.118 +      proof (rule lemma4); 
   7.119 +        show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0"; 
   7.120 +        proof -;
   7.121 +          have "y [+] a [*] x0 = x1 [+] x2"; by asm_simp; 
   7.122 +          also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by asm_simp; 
   7.123 +          also; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
   7.124 +            by asm_simp_tac;
   7.125 +         also; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0"; 
   7.126 +            by (asm_simp add: vs_add_mult_distrib2[of E]);
   7.127 +          finally; show ?thesis; by (rule sym);
   7.128 +        qed;
   7.129 +        show "y1 [+] y2 : H"; by (rule subspace_add_closed);
   7.130 +      qed;
   7.131 +      have y: "y1 [+] y2 = y"; by (rule conjunct1 [OF ya]);
   7.132 +      have a: "a1 + a2 = a";  by (rule conjunct2 [OF ya]);
   7.133 +
   7.134 +      have "h0 (x1 [+] x2) = h y + a * xi";
   7.135 +	by (rule lemma3);
   7.136 +      also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (asm_simp add: y a);
   7.137 +      also; have  "... = h y1 + h y2 + a1 * xi + a2 * xi"; 
   7.138 +	by (asm_simp add: linearform_add_linear [of H] real_add_mult_distrib);
   7.139 +      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by asm_simp;
   7.140 +      also; have "... = h0 x1 + h0 x2"; 
   7.141 +      proof -; 
   7.142 +        have x1: "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
   7.143 +        have x2: "h0 x2 = h y2 + a2 * xi"; by (rule lemma3);
   7.144 +        from x1 x2; show ?thesis; by asm_simp;
   7.145 +      qed;
   7.146 +      finally; show ?thesis; .;
   7.147 +    qed;
   7.148 + 
   7.149 +  next;  
   7.150 +    fix c x1; assume  "x1 : H0";
   7.151 +    
   7.152 +    have ax1: "c [*] x1 : H0";
   7.153 +      by (rule vs_mult_closed, rule h0);
   7.154 +    have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
   7.155 +      by (asm_simp add: vectorspace_sum_def lin_def, fast);
   7.156 +    have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)"; 
   7.157 +      by (asm_simp add: vectorspace_sum_def lin_def, fast);
   7.158 +    note ex_ax1 = ex_x [of "c [*] x1", OF ax1];
   7.159 +    from ex_x1 ex_ax1; show "h0 (c [*] x1) = c * (h0 x1)";  
   7.160 +    proof (elim exE conjE);
   7.161 +      fix y1 y a1 a; 
   7.162 +      assume "x1 = y1 [+] a1 [*] x0"       "y1 : H"
   7.163 +	     "c [*] x1 = y  [+] a  [*] x0" "y  : H"; 
   7.164 +
   7.165 +      have ya: "c [*] y1 = y & c * a1 = a"; 
   7.166 +      proof (rule lemma4); 
   7.167 +	show "c [*] y1 [+] (c * a1) [*] x0 = y [+] a [*] x0"; 
   7.168 +	proof -; 
   7.169 +          have "y [+] a [*] x0 = c [*] x1"; by asm_simp;
   7.170 +          also; have "... = c [*] (y1 [+] a1 [*] x0)"; by asm_simp;
   7.171 +          also; have "... = c [*] y1 [+] c [*] (a1 [*] x0)"; 
   7.172 +            by (asm_simp_tac add: vs_add_mult_distrib1);
   7.173 +          also; have "... = c [*] y1 [+] (c * a1) [*] x0";
   7.174 +            by (asm_simp_tac);
   7.175 +          finally; show ?thesis; by (rule sym);
   7.176 +        qed;
   7.177 +        show "c [*] y1: H"; by (rule subspace_mult_closed);
   7.178 +      qed;
   7.179 +      have y: "c [*] y1 = y"; by (rule conjunct1 [OF ya]);
   7.180 +      have a: "c * a1 = a"; by (rule conjunct2 [OF ya]);
   7.181 +      
   7.182 +      have "h0 (c [*] x1) = h y + a * xi"; 
   7.183 +	by (rule lemma3);
   7.184 +      also; have "... = h (c [*] y1) + (c * a1) * xi";
   7.185 +        by (asm_simp add: y a);
   7.186 +      also; have  "... = c * h y1 + c * a1 * xi"; 
   7.187 +	by (asm_simp add: linearform_mult_linear [of H] real_add_mult_distrib);
   7.188 +      also; have "... = c * (h y1 + a1 * xi)"; 
   7.189 +	by (asm_simp add: real_add_mult_distrib2 real_mult_assoc);
   7.190 +      also; have "... = c * (h0 x1)"; 
   7.191 +      proof -; 
   7.192 +        have "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
   7.193 +        thus ?thesis; by asm_simp;
   7.194 +      qed;
   7.195 +      finally; show ?thesis; .;
   7.196 +    qed;
   7.197 +  qed;
   7.198 +qed;
   7.199 +
   7.200 +
   7.201 +lemma h0_norm_prev:
   7.202 +    "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
   7.203 +      H0 = vectorspace_sum H (lin x0); x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
   7.204 +      is_subspace H E; is_quasinorm E p; is_linearform H h; ALL y:H. h y <= p y;
   7.205 +      (ALL y:H. - p (y [+] x0) - h y <= xi) & (ALL y:H. xi <= p (y [+] x0) - h y)|]
   7.206 +   ==> ALL x:H0. h0 x <= p x"; 
   7.207 +proof; 
   7.208 +  assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi)"
   7.209 +         "H0 = vectorspace_sum H (lin x0)" "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
   7.210 +         "is_subspace H E" "is_quasinorm E p" "is_linearform H h" and a: " ALL y:H. h y <= p y";
   7.211 +  presume a1: "(ALL y:H. - p (y [+] x0) - h y <= xi)";
   7.212 +  presume a2: "(ALL y:H. xi <= p (y [+] x0) - h y)";
   7.213 +  fix x; assume "x : H0"; 
   7.214 +  show "h0 x <= p x"; 
   7.215 +  proof -; 
   7.216 +    have ex_x: "!! x. x : H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
   7.217 +      by (asm_simp add: vectorspace_sum_def lin_def, fast);
   7.218 +    have "? y a. (x = y [+] a [*] x0 & y : H)";
   7.219 +      by (rule ex_x);
   7.220 +    thus ?thesis;
   7.221 +    proof (elim exE conjE);
   7.222 +      fix y a; assume "x = y [+] a [*] x0" "y : H";
   7.223 +      show ?thesis;
   7.224 +      proof -;
   7.225 +        have "h0 x = h y + a * xi";
   7.226 +          by (rule lemma3);
   7.227 +        also; have "... <= p (y [+] a [*] x0)";
   7.228 +        proof (rule real_linear [of a "0r", elimify], elim disjE); (* case distinction *)
   7.229 +          assume lz: "a < 0r"; 
   7.230 +          hence nz: "a ~= 0r"; by force;
   7.231 +          show ?thesis;
   7.232 +          proof -;
   7.233 +            from a1; have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
   7.234 +            proof (rule bspec); 
   7.235 +              show "(rinv a) [*] y : H"; by (rule subspace_mult_closed);
   7.236 +            qed;
   7.237 +            with lz; have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
   7.238 +              by (rule real_mult_less_le_anti);
   7.239 +            also; have "... = - a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   7.240 +              by (rule real_mult_diff_distrib);
   7.241 +            also; have "... = (rabs a) * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   7.242 +            proof -; 
   7.243 +              from lz; have "rabs a = - a";
   7.244 +                by (rule rabs_minus_eqI2); 
   7.245 +              thus ?thesis; by simp;
   7.246 +            qed;
   7.247 +            also; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   7.248 +              by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
   7.249 +            also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
   7.250 +            proof simp;
   7.251 +              have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
   7.252 +                by (rule vs_add_mult_distrib1) asm_simp+;
   7.253 +              also; have "... = (a * rinv a) [*] y [+] a [*] x0";
   7.254 +                by asm_simp;
   7.255 +              finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
   7.256 +              thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
   7.257 +                by simp;
   7.258 +            qed;
   7.259 +            also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))"; 
   7.260 +              by asm_simp;
   7.261 +            also; from nz; have "... = p (y [+] a [*] x0) - (h y)"; 
   7.262 +            proof asm_simp;
   7.263 +              have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))"; 
   7.264 +                by (asm_simp_tac add: linearform_mult_linear [RS sym]); 
   7.265 +              also; have "... = h y"; 
   7.266 +              proof -;
   7.267 +                from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
   7.268 +                thus ?thesis; by simp;
   7.269 +              qed;
   7.270 +              finally; have "a * (h (rinv a [*] y)) = h y"; .;
   7.271 +              thus "- (a * (h (rinv a [*] y))) = - (h y)"; by simp;
   7.272 +            qed;
   7.273 +            finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
   7.274 +            hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
   7.275 +              by (rule real_add_left_cancel_le [RS iffD2]); (* arith *)
   7.276 +            thus ?thesis; 
   7.277 +              by force;
   7.278 +          qed;
   7.279 +
   7.280 +        next;
   7.281 +          assume "a = 0r"; show ?thesis; 
   7.282 +          proof -;
   7.283 +            have "h y + a * xi = h y"; by asm_simp;
   7.284 +            also; from a; have "... <= p y"; ..; 
   7.285 +            also; have "... = p (y [+] a [*] x0)";
   7.286 +            proof -; 
   7.287 +              have "y = y [+] <0>"; by asm_simp;
   7.288 +              also; have "... = y [+] a [*] x0"; 
   7.289 +              proof -; 
   7.290 +                have "<0> = 0r [*] x0";
   7.291 +                  by asm_simp;
   7.292 +                also; have "... = a [*] x0"; by asm_simp;
   7.293 +                finally; have "<0> = a [*] x0";.;
   7.294 +                thus ?thesis; by simp;
   7.295 +              qed; 
   7.296 +              finally; have "y = y [+] a [*] x0"; by simp;
   7.297 +              thus ?thesis; by simp;
   7.298 +            qed;
   7.299 +            finally; show ?thesis; .;
   7.300 +          qed;
   7.301 +
   7.302 +        next; 
   7.303 +          assume gz: "0r < a"; hence nz: "a ~= 0r"; by force;
   7.304 +          show ?thesis;
   7.305 +          proof -;
   7.306 +            from a2; have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
   7.307 +            proof (rule bspec);
   7.308 +              show "rinv a [*] y : H"; by (rule subspace_mult_closed);
   7.309 +            qed;
   7.310 +            with gz; have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
   7.311 +              by (rule real_mult_less_le_mono);
   7.312 +            also; have "... = a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   7.313 +              by (rule real_mult_diff_distrib2); 
   7.314 +            also; have "... = (rabs a) * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   7.315 +            proof -; 
   7.316 +              from gz; have "rabs a = a";
   7.317 +                by (rule rabs_eqI2); 
   7.318 +              thus ?thesis; by simp;
   7.319 +            qed;
   7.320 +            also; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   7.321 +              by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
   7.322 +            also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))"; 
   7.323 +            proof simp;
   7.324 +              have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
   7.325 +                by (rule vs_add_mult_distrib1) asm_simp+;
   7.326 +              also; have "... = (a * rinv a) [*] y [+] a [*] x0";
   7.327 +                by asm_simp;
   7.328 +              finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
   7.329 +              thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
   7.330 +                by simp;
   7.331 +            qed;
   7.332 +            also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))"; 
   7.333 +              by asm_simp;
   7.334 +            also; from nz; have "... = p (y [+] a [*] x0) - (h y)"; 
   7.335 +            proof asm_simp;
   7.336 +              have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))"; 
   7.337 +                by (rule linearform_mult_linear [RS sym]) asm_simp+;
   7.338 +              also; have "... = h y"; 
   7.339 +              proof -;
   7.340 +                from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
   7.341 +                thus ?thesis; by simp;
   7.342 +              qed;
   7.343 +              finally; have "a * (h (rinv a [*] y)) = h y"; .;
   7.344 +              thus "- (a * (h (rinv a [*] y))) = - (h y)"; by simp;
   7.345 +            qed;
   7.346 +            finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
   7.347 +            hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
   7.348 +              by (rule real_add_left_cancel_le [RS iffD2]); (* arith *)
   7.349 +            thus ?thesis; 
   7.350 +              by force;
   7.351 +          qed;
   7.352 +        qed;
   7.353 +        also; have "... = p x"; by asm_simp;
   7.354 +        finally; show ?thesis; .;
   7.355 +      qed; 
   7.356 +    qed;
   7.357 +  qed; 
   7.358 +qed blast+;
   7.359 +
   7.360 +
   7.361 +end;
   7.362 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Fri Sep 10 17:28:51 1999 +0200
     8.3 @@ -0,0 +1,474 @@
     8.4 +
     8.5 +theory HahnBanach_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
     8.6 +
     8.7 +
     8.8 +theorems [dest!!] = subsetD;
     8.9 +theorems [intro!!] = subspace_subset; 
    8.10 +
    8.11 +lemma rabs_ineq: "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] \
    8.12 + \ ==>  (ALL x:H. rabs (h x) <= p x)  = ( ALL x:H. h x <= p x)" (concl is "?L = ?R");
    8.13 +proof -;
    8.14 +  assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" "is_linearform H h";
    8.15 +  have H: "is_vectorspace H"; by (rule subspace_vs);
    8.16 +  show ?thesis;
    8.17 +  proof; 
    8.18 +    assume l: ?L;
    8.19 +    then; show ?R;
    8.20 +    proof (intro ballI); 
    8.21 +      fix x; assume "x:H";
    8.22 +      have "h x <= rabs (h x)"; by (rule rabs_ge_self);
    8.23 +      also; have "rabs (h x) <= p x"; by fast;
    8.24 +      finally; show "h x <= p x"; .;
    8.25 +    qed;
    8.26 +  next;
    8.27 +    assume r: ?R;
    8.28 +    then; show ?L;
    8.29 +    proof (intro ballI);
    8.30 +      fix x; assume "x:H";
    8.31 +      have lem: "!! r x. [| - r <= x; x <= r |] ==> rabs x <= r";
    8.32 +        by (rule conjI [RS rabs_interval_iff_1 [RS iffD2]]); (* arith *)
    8.33 +      show "rabs (h x) <= p x"; 
    8.34 +      proof (rule lem);  
    8.35 +	show "- p x <= h x"; 
    8.36 +	proof (rule minus_le);
    8.37 +	  from H; have "- h x = h ([-] x)"; by (rule linearform_neg_linear [RS sym]);
    8.38 +	  also; from r; have "... <= p ([-] x)"; 
    8.39 +	  proof -; 
    8.40 +	    from H; have "[-] x : H"; by asm_simp;
    8.41 +            with r; show ?thesis; ..;
    8.42 +          qed;
    8.43 +	  also; have "... = p x"; 
    8.44 +          proof (rule quasinorm_minus);
    8.45 +            show "x:E";
    8.46 +            proof (rule subsetD);
    8.47 +              show "H <= E"; ..; 
    8.48 +            qed;
    8.49 +          qed;
    8.50 +	  finally; show "- h x <= p x"; .; 
    8.51 +	qed;
    8.52 +	from r; show "h x <= p x"; ..; 
    8.53 +      qed;
    8.54 +    qed;
    8.55 +  qed;
    8.56 +qed;  
    8.57 +
    8.58 +
    8.59 +lemma  some_H'h't:
    8.60 +  "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H|]
    8.61 +   ==> EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c & t:graph H' h' &
    8.62 +                       is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
    8.63 +                       (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
    8.64 +proof -;
    8.65 +  assume "M = norm_prev_extensions E p F f" and cM: "c: chain M" 
    8.66 +     and "graph H h = Union c" "x:H"; 
    8.67 +
    8.68 +  let ?P = "%H h. is_linearform H h 
    8.69 +                    & is_subspace H E 
    8.70 +                    & is_subspace F H
    8.71 +                    & (graph F f <= graph H h)
    8.72 +                    & (ALL x:H. h x <= p x)";
    8.73 +
    8.74 +  have "EX t : (graph H h). t = (x, h x)"; 
    8.75 +    by (rule graph_lemma1);
    8.76 +  thus ?thesis;
    8.77 +  proof (elim bexE); 
    8.78 +    fix t; assume "t : (graph H h)" and "t = (x, h x)";
    8.79 +    have ex1: "EX g:c. t:g";
    8.80 +      by (asm_simp only: Union_iff);
    8.81 +    thus ?thesis;
    8.82 +    proof (elim bexE);
    8.83 +      fix g; assume "g:c" "t:g";
    8.84 +      have gM: "g:M"; 
    8.85 +      proof -;
    8.86 +        from cM; have "c <= M"; by (rule chainD2);
    8.87 +        thus ?thesis; ..;
    8.88 +      qed;
    8.89 +      have "EX H' h'. graph H' h' = g & ?P H' h'"; 
    8.90 +      proof (rule norm_prev_extension_D);
    8.91 +        from gM; show "g: norm_prev_extensions E p F f"; by asm_simp;
    8.92 +      qed;
    8.93 +      thus ?thesis; by (elim exE conjE, intro exI conjI) (asm_simp+);
    8.94 +    qed;
    8.95 +  qed;
    8.96 +qed;
    8.97 +      
    8.98 +
    8.99 +lemma some_H'h': "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H|] 
   8.100 + ==> EX H' h'. x:H' & (graph H' h' <= graph H h) & 
   8.101 +               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.102 +               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   8.103 +proof -;
   8.104 +  assume "M = norm_prev_extensions E p F f" "c: chain M" "graph H h = Union c" "x:H"; 
   8.105 +
   8.106 +  have "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c & t:graph H' h'
   8.107 +                  & is_linearform H' h' & is_subspace H' E & is_subspace F H'
   8.108 +                  & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
   8.109 +    by (rule some_H'h't);
   8.110 + 
   8.111 +  thus ?thesis; 
   8.112 +  proof (elim exE conjE, intro exI conjI);
   8.113 +    fix H' h' t; 
   8.114 +    assume "t : graph H h" "t = (x, h x)" "graph H' h' : c" "t : graph H' h'" 
   8.115 +           "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
   8.116 +           "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
   8.117 +    show x: "x:H'"; by (asm_simp, rule graphD1);
   8.118 +    show "graph H' h' <= graph H h";
   8.119 +      by (asm_simp only: chain_ball_Union_upper);
   8.120 +  qed;
   8.121 +qed;
   8.122 +
   8.123 +
   8.124 +lemma some_H'h'2: 
   8.125 +  "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H; y:H|] 
   8.126 +  ==> EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h)
   8.127 +                & is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.128 +                (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   8.129 +proof -;
   8.130 +  assume "M = norm_prev_extensions E p F f" "c: chain M" "graph H h = Union c";
   8.131 + 
   8.132 +  let ?P = "%H h. is_linearform H h 
   8.133 +                    & is_subspace H E 
   8.134 +                    & is_subspace F H
   8.135 +                    & (graph F f <= graph H h)
   8.136 +                    & (ALL x:H. h x <= p x)";
   8.137 +  assume "x:H";
   8.138 +  have e1: "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c & t:graph H' h' &
   8.139 +                        ?P H' h'";
   8.140 +    by (rule some_H'h't); 
   8.141 +  assume "y:H";
   8.142 +  have e2: "EX H' h' t. t : (graph H h) & t = (y, h y) & (graph H' h'):c & t:graph H' h' & 
   8.143 +                        ?P H' h'";
   8.144 +    by (rule some_H'h't); 
   8.145 +
   8.146 +  from e1 e2; show ?thesis; 
   8.147 +  proof (elim exE conjE);
   8.148 +    fix H' h' t' H'' h'' t''; 
   8.149 +    assume "t' : graph H h" "t'' : graph H h" 
   8.150 +      "t' = (y, h y)" "t'' = (x, h x)"
   8.151 +      "graph H' h' : c" "graph H'' h'' : c"
   8.152 +      "t' : graph H' h'" "t'' : graph H'' h''" 
   8.153 +      "is_linearform H' h'" "is_linearform H'' h''"
   8.154 +      "is_subspace H' E" "is_subspace H'' E"
   8.155 +      "is_subspace F H'" "is_subspace F H''"
   8.156 +      "graph F f <= graph H' h'" "graph F f <= graph H'' h''"
   8.157 +      "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x";
   8.158 +
   8.159 +    have "(graph H'' h'') <= (graph H' h') | (graph H' h') <= (graph H'' h'')";
   8.160 +      by (rule chainD);
   8.161 +    thus "?thesis";
   8.162 +    proof; 
   8.163 +      assume "(graph H'' h'') <= (graph H' h')";
   8.164 +      show ?thesis;
   8.165 +      proof (intro exI conjI);
   8.166 +	have xh: "(x, h x): graph H' h'"; by (fast);
   8.167 +	thus x: "x:H'"; by (rule graphD1);
   8.168 +	show y: "y:H'"; by (asm_simp, rule graphD1);
   8.169 +	show "(graph H' h') <= (graph H h)";
   8.170 +	  by (asm_simp only: chain_ball_Union_upper);
   8.171 +      qed;
   8.172 +    next;
   8.173 +      assume "(graph H' h') <= (graph H'' h'')";
   8.174 +      show ?thesis;
   8.175 +      proof (intro exI conjI);
   8.176 +	show x: "x:H''"; by (asm_simp, rule graphD1);
   8.177 +	have yh: "(y, h y): graph H'' h''"; by (fast);
   8.178 +        thus y: "y:H''"; by (rule graphD1);
   8.179 +        show "(graph H'' h'') <= (graph H h)";
   8.180 +          by (asm_simp only: chain_ball_Union_upper);
   8.181 +      qed;
   8.182 +    qed;
   8.183 +  qed;
   8.184 +qed;
   8.185 +
   8.186 +
   8.187 +
   8.188 +lemma sup_uniq: "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
   8.189 +       ALL x:F. f x <= p x; M == norm_prev_extensions E p F f; c : chain M;
   8.190 +       EX x. x : c; (x, y) : Union c; (x, z) : Union c |]
   8.191 +     ==> z = y";
   8.192 +proof -;
   8.193 +  assume "M == norm_prev_extensions E p F f" "c : chain M" "(x, y) : Union c" " (x, z) : Union c";
   8.194 +  have "EX H h. (x, y) : graph H h & (x, z) : graph H h"; 
   8.195 +  proof (elim UnionE chainD2 [elimify]); 
   8.196 +    fix G1 G2; assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
   8.197 +    have "G1 : M"; by (rule subsetD);
   8.198 +    hence e1: "EX H1 h1. graph H1 h1 = G1";  
   8.199 +      by (force dest: norm_prev_extension_D);
   8.200 +    have "G2 : M"; by (rule subsetD);
   8.201 +    hence e2: "EX H2 h2. graph H2 h2 = G2";  
   8.202 +      by (force dest: norm_prev_extension_D);
   8.203 +    from e1 e2; show ?thesis; 
   8.204 +    proof (elim exE);
   8.205 +      fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
   8.206 +      have "G1 <= G2 | G2 <= G1"; by (rule chainD);
   8.207 +      thus ?thesis;
   8.208 +      proof;
   8.209 +        assume "G1 <= G2";
   8.210 +        thus ?thesis;
   8.211 +        proof (intro exI conjI);
   8.212 +          show "(x, y) : graph H2 h2"; by force;
   8.213 +          show "(x, z) : graph H2 h2"; by asm_simp;
   8.214 +        qed;
   8.215 +      next;
   8.216 +        assume "G2 <= G1";
   8.217 +        thus ?thesis;
   8.218 +        proof (intro exI conjI);
   8.219 +          show "(x, y) : graph H1 h1"; by asm_simp;
   8.220 +          show "(x, z) : graph H1 h1"; by force; 
   8.221 +        qed;
   8.222 +      qed;
   8.223 +    qed;
   8.224 +  qed;
   8.225 +  thus ?thesis; 
   8.226 +  proof (elim exE conjE);
   8.227 +    fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h";
   8.228 +    have "y = h x"; by (rule graph_lemma2);
   8.229 +    also; have "h x = z"; by (rule graph_lemma2 [RS sym]);
   8.230 +    finally; show "z = y"; by (rule sym);
   8.231 +  qed;
   8.232 +qed;
   8.233 +
   8.234 +
   8.235 +lemma sup_lf: "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c|] 
   8.236 +   ==> is_linearform H h";
   8.237 +proof -; 
   8.238 +  assume "M = norm_prev_extensions E p F f" "c: chain M" "graph H h = Union c";
   8.239 + 
   8.240 +  let ?P = "%H h. is_linearform H h 
   8.241 +                    & is_subspace H E 
   8.242 +                    & is_subspace F H
   8.243 +                    & (graph F f <= graph H h)
   8.244 +                    & (ALL x:H. h x <= p x)";
   8.245 +
   8.246 +  show "is_linearform H h";
   8.247 +  proof;
   8.248 +    fix x y; assume "x : H" "y : H"; 
   8.249 +    show "h (x [+] y) = h x + h y"; 
   8.250 +    proof -;
   8.251 +      have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) &
   8.252 +                    is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.253 +                    (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
   8.254 +        by (rule some_H'h'2);
   8.255 +      thus ?thesis; 
   8.256 +      proof (elim exE conjE);
   8.257 +        fix H' h'; assume "x:H'" "y:H'" 
   8.258 +          and b: "graph H' h' <= graph H h" 
   8.259 +          and "is_linearform H' h'" "is_subspace H' E";
   8.260 +        have h'x: "h' x = h x"; by (rule graph_lemma3); 
   8.261 +        have h'y: "h' y = h y"; by (rule graph_lemma3);
   8.262 +        have h'xy: "h' (x [+] y) = h' x + h' y"; by (rule linearform_add_linear);
   8.263 +        have "h' (x [+] y) = h (x [+] y)";  
   8.264 +        proof -;
   8.265 +          have "x [+] y : H'";
   8.266 +            by (rule subspace_add_closed);
   8.267 +          with b; show ?thesis; by (rule graph_lemma3);
   8.268 +        qed;
   8.269 +        with h'x h'y h'xy; show ?thesis;
   8.270 +          by asm_simp; 
   8.271 +      qed;
   8.272 +    qed;
   8.273 +
   8.274 +  next;  
   8.275 +    fix a x; assume  "x : H";
   8.276 +    show "h (a [*] x) = a * (h x)"; 
   8.277 +    proof -;
   8.278 +      have "EX H' h'. x:H' & (graph H' h' <= graph H h) &
   8.279 +                      is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.280 +                      (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
   8.281 +	by (rule some_H'h');
   8.282 +      thus ?thesis; 
   8.283 +      proof (elim exE conjE);
   8.284 +	fix H' h';
   8.285 +	assume b: "graph H' h' <= graph H h";
   8.286 +	assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
   8.287 +	have h'x: "h' x = h x"; by (rule graph_lemma3);
   8.288 +	have h'ax: "h' (a [*] x) = a * h' x"; by (rule linearform_mult_linear);
   8.289 +	have "h' (a [*] x) = h (a [*] x)";
   8.290 +	proof -;
   8.291 +	  have "a [*] x : H'";
   8.292 +	    by (rule subspace_mult_closed);
   8.293 +	  with b; show ?thesis; by (rule graph_lemma3);
   8.294 +	qed;
   8.295 +	with h'x h'ax; show ?thesis;
   8.296 +	  by asm_simp;
   8.297 +      qed;
   8.298 +    qed;
   8.299 +  qed;
   8.300 +qed;
   8.301 +
   8.302 +
   8.303 +lemma sup_ext: "[| M = norm_prev_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c|] 
   8.304 +   ==> graph F f <= graph H h";
   8.305 +proof -;
   8.306 +  assume "M = norm_prev_extensions E p F f" "c: chain M"  "graph H h = Union c"
   8.307 +    and  e: "EX x. x:c";
   8.308 + 
   8.309 +  show ?thesis; 
   8.310 +  proof (elim exE);
   8.311 +    fix x; assume "x:c"; 
   8.312 +    show ?thesis;    
   8.313 +    proof -;
   8.314 +      have "x:norm_prev_extensions E p F f"; 
   8.315 +      proof (rule subsetD);
   8.316 +	show "c <= norm_prev_extensions E p F f"; by (asm_simp add: chainD2);
   8.317 +      qed;
   8.318 + 
   8.319 +      hence "(EX G g. graph G g = x
   8.320 +                    & is_linearform G g 
   8.321 +                    & is_subspace G E
   8.322 +                    & is_subspace F G
   8.323 +                    & (graph F f <= graph G g) 
   8.324 +                    & (ALL x:G. g x <= p x))";
   8.325 +	by (asm_simp add: norm_prev_extension_D);
   8.326 +
   8.327 +      thus ?thesis; 
   8.328 +      proof (elim exE conjE); 
   8.329 +	fix G g; assume "graph G g = x" "graph F f <= graph G g";
   8.330 +	show ?thesis; 
   8.331 +        proof -; 
   8.332 +          have "graph F f <= graph G g"; by assumption;
   8.333 +          also; have "graph G g <= graph H h"; by (asm_simp, fast);
   8.334 +          finally; show ?thesis; .;
   8.335 +        qed;
   8.336 +      qed;
   8.337 +    qed;
   8.338 +  qed;
   8.339 +qed;
   8.340 +
   8.341 +
   8.342 +lemma sup_supF: "[| M = norm_prev_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c;
   8.343 +                    is_subspace F E |] ==> is_subspace F H";
   8.344 +proof -; 
   8.345 +  assume "M = norm_prev_extensions E p F f" "c: chain M" "EX x. x:c" "graph H h = Union c"
   8.346 +    "is_subspace F E";
   8.347 +
   8.348 +  show ?thesis; 
   8.349 +  proof (rule subspace_I);
   8.350 +    show "<0> : F"; by (rule zero_in_subspace); 
   8.351 +    show "F <= H"; 
   8.352 +    proof (rule graph_lemma4);
   8.353 +      show "graph F f <= graph H h";
   8.354 +        by (rule sup_ext);
   8.355 +    qed;
   8.356 +    show "ALL x:F. ALL y:F. x [+] y : F"; 
   8.357 +    proof (intro ballI); 
   8.358 +      fix x y; assume "x:F" "y:F";
   8.359 +      show "x [+] y : F"; by asm_simp;
   8.360 +    qed;
   8.361 +    show "ALL x:F. ALL a. a [*] x : F";
   8.362 +    proof (intro ballI allI);
   8.363 +      fix x a; assume "x:F";
   8.364 +      show "a [*] x : F"; by asm_simp;
   8.365 +    qed;
   8.366 +  qed;
   8.367 +qed;
   8.368 +
   8.369 +
   8.370 +lemma sup_subE: "[| M = norm_prev_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c;
   8.371 +                    is_subspace F E|] ==> is_subspace H E";
   8.372 +proof -; 
   8.373 +  assume "M = norm_prev_extensions E p F f" "c: chain M" "EX x. x:c" "graph H h = Union c"
   8.374 +    "is_subspace F E";
   8.375 +
   8.376 +  show ?thesis; 
   8.377 +  proof (rule subspace_I);
   8.378 +
   8.379 +    show "<0> : H"; 
   8.380 +    proof (rule subsetD [of F H]);
   8.381 +      have "is_subspace F H"; by (rule sup_supF);
   8.382 +      thus "F <= H"; by (rule subspace_subset);
   8.383 +      show  "<0> :F"; by (rule zero_in_subspace); 
   8.384 +    qed;
   8.385 +
   8.386 +    show "H <= E"; 
   8.387 +    proof;
   8.388 +      fix x; assume "x:H";
   8.389 +      show "x:E";
   8.390 +      proof -;
   8.391 +	have "EX H' h'. x:H' & (graph H' h' <= graph H h) & 
   8.392 +               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.393 +               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   8.394 +	  by (rule some_H'h');
   8.395 +	thus ?thesis;
   8.396 +	proof (elim exE conjE);
   8.397 +	  fix H' h'; assume "x:H'" "is_subspace H' E";
   8.398 +	  show "x:E"; 
   8.399 +	  proof (rule subsetD);
   8.400 +	    show "H' <= E";
   8.401 +	      by (rule subspace_subset);    
   8.402 +	  qed;
   8.403 +	qed;
   8.404 +      qed;
   8.405 +    qed;
   8.406 +
   8.407 +    show "ALL x:H. ALL y:H. x [+] y : H"; 
   8.408 +    proof (intro ballI); 
   8.409 +      fix x y; assume "x:H" "y:H";
   8.410 +      show "x [+] y : H";   
   8.411 +      proof -;
   8.412 + 	have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) & 
   8.413 +               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.414 +               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   8.415 +	  by (rule some_H'h'2); 
   8.416 +	thus ?thesis;
   8.417 +	proof (elim exE conjE); 
   8.418 +	  fix H' h'; assume "x:H'" "y:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   8.419 +	  have "H' <= H"; by (rule graph_lemma4);
   8.420 +	  thus ?thesis;
   8.421 +	  proof (rule subsetD);
   8.422 +	    show "x [+] y : H'"; by (rule subspace_add_closed);
   8.423 +	  qed;
   8.424 +	qed;
   8.425 +      qed;
   8.426 +    qed;      
   8.427 +
   8.428 +    show "ALL x:H. ALL a. a [*] x : H"; 
   8.429 +    proof (intro ballI allI); 
   8.430 +      fix x and a::real; assume "x:H";
   8.431 +      show "a [*] x : H"; 
   8.432 +      proof -;
   8.433 +	have "EX H' h'. x:H' & (graph H' h' <= graph H h) & 
   8.434 +               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.435 +               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   8.436 +	  by (rule some_H'h'); 
   8.437 +	thus ?thesis;
   8.438 +	proof (elim exE conjE);
   8.439 +	  fix H' h'; assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   8.440 +  	  have "H' <= H"; by (rule graph_lemma4);
   8.441 +	  thus ?thesis;
   8.442 +	  proof (rule subsetD);
   8.443 +	    show "a [*] x : H'"; by (rule subspace_mult_closed);
   8.444 +	  qed;
   8.445 +	qed;
   8.446 +      qed;
   8.447 +    qed;
   8.448 +  qed;
   8.449 +qed;
   8.450 +
   8.451 +
   8.452 +lemma sup_norm_prev: "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c|] 
   8.453 +   ==> ALL x::'a:H. h x <= p x";
   8.454 +proof;
   8.455 +  assume "M = norm_prev_extensions E p F f" "c: chain M" "graph H h = Union c";
   8.456 +  fix x; assume "x:H";
   8.457 +  show "h x <= p x"; 
   8.458 +  proof -; 
   8.459 +    have "EX H' h'. x:H' & (graph H' h' <= graph H h) & 
   8.460 +               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   8.461 +               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   8.462 +      by (rule some_H'h');
   8.463 +    thus ?thesis; 
   8.464 +    proof (elim exE conjE);
   8.465 +      fix H' h'; assume "x: H'" "graph H' h' <= graph H h" and a: "ALL x: H'. h' x <= p x" ;
   8.466 +      have "h x = h' x"; 
   8.467 +      proof(rule sym); 
   8.468 +        show "h' x = h x"; by (rule graph_lemma3);
   8.469 +      qed;
   8.470 +      also; from a; have "... <= p x "; ..;
   8.471 +      finally; show ?thesis; .;  
   8.472 +    qed;
   8.473 +  qed;
   8.474 +qed;
   8.475 +
   8.476 +
   8.477 +end;
   8.478 \ No newline at end of file
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Real/HahnBanach/LinearSpace.thy	Fri Sep 10 17:28:51 1999 +0200
     9.3 @@ -0,0 +1,485 @@
     9.4 +
     9.5 +theory LinearSpace = Main + RealAbs + Bounds + Aux:;
     9.6 +
     9.7 +
     9.8 +section {* vector spaces *};
     9.9 +
    9.10 +consts
    9.11 +  sum	:: "['a, 'a] => 'a"                      (infixl "[+]" 65)  
    9.12 +  prod  :: "[real, 'a] => 'a"                    (infixr "[*]" 70) 
    9.13 +  zero   :: "'a"                                 ("<0>");
    9.14 +
    9.15 +constdefs
    9.16 +  negate :: "'a => 'a"                           ("[-] _" [100] 100)
    9.17 +  "[-] x == (- 1r) [*] x"
    9.18 +  diff :: "'a => 'a => 'a"                       (infixl "[-]" 68)
    9.19 +  "x [-] y == x [+] [-] y";
    9.20 +
    9.21 +constdefs
    9.22 +  is_vectorspace :: "'a set => bool"
    9.23 +  "is_vectorspace V == <0>:V &
    9.24 +   (ALL x:V. ALL y:V. ALL z:V. ALL a b. x [+] y: V 
    9.25 +                          & a [*] x: V                        
    9.26 +                          & x [+] y [+] z = x [+] (y [+] z)  
    9.27 +                          & x [+] y = y [+] x             
    9.28 +                          & x [-] x = <0>         
    9.29 +                          & <0> [+] x = x 
    9.30 +                          & a [*] (x [+] y) = a [*] x [+] a [*] y
    9.31 +                          & (a + b) [*] x = a [*] x [+] b [*] x
    9.32 +                          & (a * b) [*] x = a [*] b [*] x     
    9.33 +                          & 1r [*] x = x)";
    9.34 +
    9.35 +
    9.36 +subsection {* neg, diff *};
    9.37 +
    9.38 +lemma vs_mult_minus_1: "(- 1r) [*] x = [-] x";
    9.39 +  by (simp add: negate_def);
    9.40 +
    9.41 +lemma vs_add_mult_minus_1_eq_diff: "x [+] (- 1r) [*] y = x [-] y";
    9.42 +  by (simp add: diff_def negate_def);
    9.43 +
    9.44 +lemma vs_add_minus_eq_diff: "x [+] [-] y = x [-] y";
    9.45 +  by (simp add: diff_def);
    9.46 +
    9.47 +lemma vs_I:
    9.48 +  "[| <0>:V; \
    9.49 +  \      ALL x: V. ALL a::real. a [*] x: V; \     
    9.50 +  \      ALL x: V. ALL y: V. x [+] y = y [+] x; \
    9.51 +  \      ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z =  x [+] (y [+] z); \
    9.52 +  \      ALL x: V. ALL y: V. x [+] y: V; \
    9.53 +  \      ALL x: V.  x [-] x = <0>; \
    9.54 +  \      ALL x: V.  <0> [+] x = x; \
    9.55 +  \      ALL x: V. ALL y: V. ALL a::real. a [*] (x [+] y) = a [*] x [+] a [*] y; \
    9.56 +  \      ALL x: V. ALL a::real. ALL b::real. (a + b) [*] x = a [*] x [+] b [*] x; \
    9.57 +  \      ALL x: V. ALL a::real. ALL b::real. (a * b) [*] x = a [*] b [*] x; \
    9.58 +  \      ALL x: V. 1r [*] x = x |] ==> is_vectorspace V";
    9.59 +  by (unfold is_vectorspace_def) auto;
    9.60 +
    9.61 +lemma zero_in_vs [simp, dest]: "is_vectorspace V ==> <0>:V";
    9.62 +  by (unfold is_vectorspace_def) asm_simp;
    9.63 +
    9.64 +lemma vs_not_empty: "is_vectorspace V ==> (V ~= {})"; 
    9.65 +  by (unfold is_vectorspace_def) fast;
    9.66 + 
    9.67 +lemma vs_add_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V"; 
    9.68 +  by (unfold is_vectorspace_def) asm_simp;
    9.69 +
    9.70 +lemma vs_mult_closed [simp]: "[| is_vectorspace V; x: V |] ==> a [*] x: V"; 
    9.71 +  by (unfold is_vectorspace_def) asm_simp;
    9.72 +
    9.73 +lemma vs_diff_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
    9.74 +  by (unfold diff_def negate_def) asm_simp;
    9.75 +
    9.76 +lemma vs_neg_closed  [simp]: "[| is_vectorspace V; x: V |] ==>  [-] x: V";
    9.77 +  by (unfold negate_def) asm_simp;
    9.78 +
    9.79 +lemma vs_add_assoc [simp]:  
    9.80 +  "[| is_vectorspace V; x: V; y: V; z: V|] ==> x [+] y [+] z =  x [+] (y [+] z)";
    9.81 +  by (unfold is_vectorspace_def) fast;
    9.82 +
    9.83 +lemma vs_add_commute [simp]: "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
    9.84 +  by (unfold is_vectorspace_def) asm_simp;
    9.85 +
    9.86 +lemma vs_add_left_commute [simp]:
    9.87 +  "[| is_vectorspace V; x:V; y:V; z:V |] ==> x [+] (y [+] z) = y [+] (x [+] z)";
    9.88 +proof -;
    9.89 +  assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
    9.90 +  have "x [+] (y [+] z) = (x [+] y) [+] z";
    9.91 +    by (asm_simp only: vs_add_assoc);
    9.92 +  also; have "... = (y [+] x) [+] z";
    9.93 +    by (asm_simp only: vs_add_commute);
    9.94 +  also; have "... = y [+] (x [+] z)";
    9.95 +    by (asm_simp only: vs_add_assoc);
    9.96 +  finally; show ?thesis; .;
    9.97 +qed;
    9.98 +
    9.99 +
   9.100 +theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
   9.101 +
   9.102 +lemma vs_diff_self [simp]: "[| is_vectorspace V; x:V |] ==>  x [-] x = <0>"; 
   9.103 +  by (unfold is_vectorspace_def) asm_simp;
   9.104 +
   9.105 +lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==>  <0> [+] x = x";
   9.106 +  by (unfold is_vectorspace_def) asm_simp;
   9.107 +
   9.108 +lemma vs_add_zero_right [simp]: "[| is_vectorspace V; x:V |] ==>  x [+] <0> = x";
   9.109 +proof -;
   9.110 +  assume vs: "is_vectorspace V" "x:V";
   9.111 +  have "x [+] <0> = <0> [+] x";
   9.112 +    by asm_simp;
   9.113 +  also; have "... = x";
   9.114 +    by asm_simp;
   9.115 +  finally; show ?thesis; .;
   9.116 +qed;
   9.117 +
   9.118 +lemma vs_add_mult_distrib1: 
   9.119 +  "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
   9.120 +  by (unfold is_vectorspace_def) asm_simp;
   9.121 +
   9.122 +lemma vs_add_mult_distrib2: 
   9.123 +  "[| is_vectorspace V; x:V |] ==>  (a + b) [*] x = a [*] x [+] b [*] x"; 
   9.124 +  by (unfold is_vectorspace_def) asm_simp;
   9.125 +
   9.126 +lemma vs_mult_assoc: "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";   
   9.127 +  by (unfold is_vectorspace_def) asm_simp;
   9.128 +
   9.129 +lemma vs_mult_assoc2 [simp]: "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
   9.130 +  by (asm_simp only: vs_mult_assoc);
   9.131 +
   9.132 +lemma vs_mult_1 [simp]: "[| is_vectorspace V; x:V |] ==> 1r [*] x = x"; 
   9.133 +  by (unfold is_vectorspace_def) asm_simp;
   9.134 +
   9.135 +lemma vs_diff_mult_distrib1: 
   9.136 +  "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
   9.137 +  by (asm_simp add: diff_def negate_def vs_add_mult_distrib1);
   9.138 +
   9.139 +lemma vs_minus_eq: "[| is_vectorspace V; x:V |] ==> - b [*] x = [-] (b [*] x)";
   9.140 +  by (asm_simp add: negate_def);
   9.141 +
   9.142 +lemma vs_diff_mult_distrib2: 
   9.143 +  "[| is_vectorspace V; x:V |] ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
   9.144 +proof -;
   9.145 +  assume "is_vectorspace V" "x:V";
   9.146 +  have " (a - b) [*] x = (a + - b ) [*] x"; by (unfold real_diff_def, simp);
   9.147 +  also; have "... = a [*] x [+] (- b) [*] x"; by (rule vs_add_mult_distrib2);
   9.148 +  also; have "... = a [*] x [+] [-] (b [*] x)"; by (asm_simp add: vs_minus_eq);
   9.149 +  also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp);
   9.150 +  finally; show ?thesis; .;
   9.151 +qed;
   9.152 +
   9.153 +lemma vs_mult_zero_left [simp]: "[| is_vectorspace V; x: V|] ==> 0r [*] x = <0>";
   9.154 +proof -;
   9.155 +  assume vs: "is_vectorspace V" "x:V";
   9.156 +  have  "0r [*] x = (1r - 1r) [*] x";
   9.157 +    by (asm_simp only: real_diff_self);
   9.158 +  also; have "... = (1r + - 1r) [*] x";
   9.159 +    by simp;
   9.160 +  also; have "... =  1r [*] x [+] (- 1r) [*] x";
   9.161 +    by (rule vs_add_mult_distrib2);
   9.162 +  also; have "... = x [+] (- 1r) [*] x";
   9.163 +    by asm_simp;
   9.164 +  also; have "... = x [-] x";
   9.165 +    by (rule vs_add_mult_minus_1_eq_diff);
   9.166 +  also; have "... = <0>";
   9.167 +    by asm_simp;
   9.168 +  finally; show ?thesis; .;
   9.169 +qed;
   9.170 +
   9.171 +lemma vs_mult_zero_right [simp]: "[| is_vectorspace (V:: 'a set) |] ==> a [*] <0> = (<0>::'a)";
   9.172 +proof -;
   9.173 +  assume vs: "is_vectorspace V";
   9.174 +  have "a [*] <0> = a [*] (<0> [-] (<0>::'a))";
   9.175 +    by (asm_simp);
   9.176 +  also; from zero_in_vs [of V]; have "... =  a [*] <0> [-] a [*] <0>";
   9.177 +    by (asm_simp only: vs_diff_mult_distrib1);
   9.178 +  also; have "... = <0>";
   9.179 +    by asm_simp;
   9.180 +  finally; show ?thesis; .;
   9.181 +qed;
   9.182 +
   9.183 +lemma vs_minus_mult_cancel [simp]:  "[| is_vectorspace V; x:V |] ==>  (- a) [*] [-] x = a [*] x";
   9.184 +  by (unfold negate_def) asm_simp;
   9.185 +
   9.186 +lemma vs_add_minus_left_eq_diff: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] y = y [-] x";
   9.187 +proof -; 
   9.188 +  assume vs: "is_vectorspace V";
   9.189 +  assume x: "x:V"; hence nx: "[-] x:V"; by asm_simp;
   9.190 +  assume y: "y:V";
   9.191 +  have "[-] x [+] y = y [+] [-] x";
   9.192 +    by (asm_simp add: vs_add_commute [RS sym, of V "[-] x"]);
   9.193 +  also; have "... = y [-] x";
   9.194 +    by (simp only: vs_add_minus_eq_diff);
   9.195 +  finally; show ?thesis; .;
   9.196 +qed;
   9.197 +
   9.198 +lemma vs_add_minus [simp]: "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>";
   9.199 +  by (asm_simp add: vs_add_minus_eq_diff); 
   9.200 +
   9.201 +lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+]  x = <0>";
   9.202 +  by (asm_simp add: vs_add_minus_eq_diff); 
   9.203 +
   9.204 +lemma vs_minus_minus [simp]: "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
   9.205 +  by (unfold negate_def) asm_simp;
   9.206 +
   9.207 +lemma vs_minus_zero [simp]: "[| is_vectorspace (V::'a set)|] ==>  [-] (<0>::'a) = <0>"; 
   9.208 +  by (unfold negate_def) asm_simp;
   9.209 +
   9.210 +lemma vs_minus_zero_iff [simp]:
   9.211 +  "[| is_vectorspace V; x:V|] ==>  ([-] x = <0>) = (x = <0>)" (concl is "?L = ?R");
   9.212 +proof -;
   9.213 +  assume vs: "is_vectorspace V" "x:V";
   9.214 +  show "?L = ?R";
   9.215 +  proof;
   9.216 +    assume l: ?L;
   9.217 +    have "x = [-] [-] x";
   9.218 +      by (rule vs_minus_minus [RS sym]);
   9.219 +    also; have "... = [-] <0>";
   9.220 +      by (rule l [RS arg_cong] );
   9.221 +    also; have "... = <0>";
   9.222 +      by (rule vs_minus_zero);
   9.223 +    finally; show ?R; .;
   9.224 +  next;
   9.225 +    assume ?R;
   9.226 +    with vs; show ?L;
   9.227 +    by simp;
   9.228 +  qed;
   9.229 +qed;
   9.230 +
   9.231 +lemma vs_add_minus_cancel [simp]:  "[| is_vectorspace V; x:V; y:V|] ==>  x [+] ([-] x [+] y) = y"; 
   9.232 +  by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
   9.233 +
   9.234 +lemma vs_minus_add_cancel [simp]: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] (x [+] y) = y"; 
   9.235 +  by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
   9.236 +
   9.237 +lemma vs_minus_add_distrib [simp]:  
   9.238 +  "[| is_vectorspace V; x:V; y:V|] ==>  [-] (x [+] y) = [-] x [+] [-] y";
   9.239 +  by (unfold negate_def, asm_simp add: vs_add_mult_distrib1);
   9.240 +
   9.241 +lemma vs_diff_zero [simp]: "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
   9.242 +  by (unfold diff_def) asm_simp;  
   9.243 +
   9.244 +lemma vs_diff_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
   9.245 +  by (unfold diff_def) asm_simp;
   9.246 +
   9.247 +lemma vs_add_left_cancel:
   9.248 +  "[|is_vectorspace V; x:V; y:V; z:V|] ==> (x [+] y = x [+] z) = (y = z)"  
   9.249 +  (concl is "?L = ?R");
   9.250 +proof;
   9.251 +  assume vs: "is_vectorspace V" and x: "x:V" and y: "y:V" and z: "z:V";
   9.252 +  assume l: ?L; 
   9.253 +  have "y = <0> [+] y";
   9.254 +    by asm_simp;
   9.255 +  also; have "... = [-] x [+] x [+] y";
   9.256 +    by asm_simp;
   9.257 +  also; from vs vs_neg_closed x y ; have "... = [-] x [+] (x [+] y)";
   9.258 +    by (rule vs_add_assoc);
   9.259 +  also; have "...  = [-] x [+] (x [+] z)"; 
   9.260 +    by (asm_simp only: l);
   9.261 +  also; from vs vs_neg_closed x z; have "... = [-] x [+] x [+] z";
   9.262 +    by (rule vs_add_assoc [RS sym]);
   9.263 +  also; have "... = z";
   9.264 +    by asm_simp;
   9.265 +  finally; show ?R;.;
   9.266 +next;    
   9.267 +  assume ?R;
   9.268 +  show ?L;
   9.269 +    by force;
   9.270 +qed;
   9.271 +
   9.272 +lemma vs_add_right_cancel: 
   9.273 +  "[| is_vectorspace V; x:V; y:V; z:V |] ==>  (y [+] x = z [+] x) = (y = z)";  
   9.274 +  by (asm_simp only: vs_add_commute vs_add_left_cancel);
   9.275 +
   9.276 +lemma vs_add_assoc_cong [tag FIXME simp]: "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] \
   9.277 +\   ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)"; 
   9.278 +  by (asm_simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
   9.279 +
   9.280 +lemma vs_mult_left_commute: 
   9.281 +  "[| is_vectorspace V; x:V; y:V; z:V |] ==>  x [*] y [*] z = y [*] x [*] z";  
   9.282 +  by (asm_simp add: real_mult_commute);
   9.283 +
   9.284 +lemma vs_mult_left_cancel: 
   9.285 +  "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>  (a [*] x = a [*] y) = (x = y)"
   9.286 +  (concl is "?L = ?R");
   9.287 +proof;
   9.288 +  assume vs: "is_vectorspace V";
   9.289 +  assume x: "x:V";
   9.290 +  assume y: "y:V";
   9.291 +  assume a: "a ~= 0r";
   9.292 +  assume l: ?L;
   9.293 +  have "x = 1r [*] x";
   9.294 +    by (asm_simp);
   9.295 +  also; have "... = (rinv a * a) [*] x";
   9.296 +    by (asm_simp);
   9.297 +  also; have "... = rinv a [*] (a [*] x)";
   9.298 +    by (asm_simp only: vs_mult_assoc);
   9.299 +  also; have "... = rinv a [*] (a [*] y)";
   9.300 +    by (asm_simp only: l);
   9.301 +  also; have "... = y";
   9.302 +    by (asm_simp);
   9.303 +  finally; show ?R;.;
   9.304 +next;
   9.305 +  assume ?R;
   9.306 +  show ?L;
   9.307 +    by (asm_simp);
   9.308 +qed;
   9.309 +
   9.310 +lemma vs_eq_diff_eq: 
   9.311 +  "[| is_vectorspace V; x:V; y:V; z:V |] ==>  (x = z [-] y) = (x [+] y = z)"
   9.312 +   (concl is "?L = ?R" );  
   9.313 +proof -;
   9.314 +  assume vs: "is_vectorspace V";
   9.315 +  assume x: "x:V";
   9.316 +  assume y: "y:V"; hence n: "[-] y:V"; by asm_simp;
   9.317 +  assume z: "z:V";
   9.318 +  show "?L = ?R";   
   9.319 +  proof;
   9.320 +    assume l: ?L;
   9.321 +    have "x [+] y = z [-] y [+] y";
   9.322 +      by (asm_simp add: l);
   9.323 +    also; have "... = z [+] [-] y [+] y";        
   9.324 +      by (asm_simp only: vs_add_minus_eq_diff);
   9.325 +    also; from vs z n y; have "... = z [+] ([-] y [+] y)";
   9.326 +      by (asm_simp only: vs_add_assoc);
   9.327 +    also; have "... = z [+] <0>";
   9.328 +      by (asm_simp only: vs_add_minus_left);
   9.329 +    also; have "... = z";
   9.330 +      by (asm_simp only: vs_add_zero_right);
   9.331 +    finally; show ?R;.;
   9.332 +  next;
   9.333 +    assume r: ?R;
   9.334 +    have "z [-] y = (x [+] y) [-] y";
   9.335 +      by (asm_simp only: r);
   9.336 +    also; have "... = x [+] y [+] [-] y";
   9.337 +      by (asm_simp only: vs_add_minus_eq_diff);
   9.338 +   also; from vs x y n; have "... = x [+] (y [+] [-] y)";
   9.339 +      by (rule vs_add_assoc); 
   9.340 +    also; have "... = x";     
   9.341 +      by (asm_simp);
   9.342 +    finally; show ?L; by (rule sym);
   9.343 +  qed;
   9.344 +qed;
   9.345 +
   9.346 +lemma vs_add_minus_eq_minus: "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x"; 
   9.347 +proof -;
   9.348 +  assume vs: "is_vectorspace V";
   9.349 +  assume x: "x:V"; hence n: "[-] x : V"; by (asm_simp);
   9.350 +  assume y: "y:V";
   9.351 +  assume xy: "<0> = x [+] y";
   9.352 +  from vs n; have "[-] x = [-] x [+] <0>";
   9.353 +    by asm_simp;
   9.354 +  also; have "... = [-] x [+] (x [+] y)"; 
   9.355 +    by (asm_simp);
   9.356 +  also; from vs n x y; have "... = [-] x [+] x [+] y";
   9.357 +    by (rule vs_add_assoc [RS sym]);
   9.358 +  also; from vs x y; have "... = (x [+] [-] x) [+] y";
   9.359 +    by (simp);
   9.360 +  also; from vs y; have "... = y";
   9.361 +    by (asm_simp);
   9.362 +  finally; show ?thesis;
   9.363 +    by (rule sym);
   9.364 +qed;  
   9.365 +
   9.366 +lemma vs_add_minus_eq: "[| is_vectorspace V; x:V; y:V; x [-] y = <0> |] ==> x = y"; 
   9.367 +proof -;
   9.368 +  assume "is_vectorspace V" "x:V" "y:V" "x [-] y = <0>";
   9.369 +  have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
   9.370 +  also; have "... = <0>"; .;
   9.371 +  finally; have e: "<0> = x [+] [-] y"; by (rule sym);
   9.372 +  have "x = [-] [-] x"; by asm_simp;
   9.373 +  also; from _ _ _ e; have "[-] x = [-] y"; 
   9.374 +    by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) asm_simp+;
   9.375 +  also; have "[-] ... = y"; by asm_simp; 
   9.376 +  finally; show "x = y"; .;
   9.377 +qed;
   9.378 +
   9.379 +lemma vs_add_diff_swap:
   9.380 +  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] ==> a [-] c = d [-] b";
   9.381 +proof -; 
   9.382 +  assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" and eq: "a [+] b = c [+] d";
   9.383 +  have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (asm_simp add: vs_add_left_cancel);
   9.384 +  also; have "... = d"; by (rule vs_minus_add_cancel);
   9.385 +  finally; have eq: "[-] c [+] (a [+] b) = d"; .;
   9.386 +  from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b"; 
   9.387 +    by (simp add: vs_add_ac diff_def);
   9.388 +  also; from eq; have "...  = d [+] [-] b"; by (asm_simp add: vs_add_right_cancel);
   9.389 +  also; have "... = d [-] b"; by (simp add : diff_def);
   9.390 +  finally; show "a [-] c = d [-] b"; .;
   9.391 +qed;
   9.392 +
   9.393 +
   9.394 +lemma vs_mult_zero_uniq :
   9.395 +  "[| is_vectorspace V; x:V; a [*] x = <0>; x ~= <0> |] ==> a = 0r";
   9.396 +proof (rule classical);
   9.397 +  assume "is_vectorspace V" "x:V" "a [*] x = <0>" "x ~= <0>";
   9.398 +  assume "a ~= 0r";
   9.399 +  have "x = (rinv a * a) [*] x"; by asm_simp;
   9.400 +  also; have "... = (rinv a) [*] (a [*] x)"; by (rule vs_mult_assoc);
   9.401 +  also; have "... = (rinv a) [*] <0>"; by asm_simp;
   9.402 +  also; have "... = <0>"; by asm_simp;
   9.403 +  finally; have "x = <0>"; .;
   9.404 +  thus "a = 0r"; by contradiction; 
   9.405 +qed;
   9.406 +
   9.407 +lemma vs_add_cancel_21: 
   9.408 +  "[| is_vectorspace V; x:V; y:V; z:V; u:V|] ==> (x [+] (y [+] z) = y [+] u) = ((x [+] z) = u)"
   9.409 +  (concl is "?L = ?R" ); 
   9.410 +proof -; 
   9.411 +  assume vs: "is_vectorspace V";
   9.412 +  assume x: "x:V";
   9.413 +  assume y: "y:V"; hence n: "[-] y:V"; by (asm_simp);
   9.414 +  assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
   9.415 +  assume u: "u:V";
   9.416 +  show "?L = ?R";
   9.417 +  proof;
   9.418 +    assume l: ?L;
   9.419 +    from vs u; have "u = <0> [+] u";
   9.420 +      by asm_simp;
   9.421 +    also; from vs y vs_neg_closed u; have "... = [-] y [+] y [+] u";
   9.422 +      by asm_simp;
   9.423 +    also; from vs n y u; have "... = [-] y [+] (y [+] u)";
   9.424 +      by (asm_simp only: vs_add_assoc);
   9.425 +    also; have "... = [-] y [+] (x [+] (y [+] z))";
   9.426 +      by (asm_simp only: l);
   9.427 +    also; have "... = [-] y [+] (y [+] (x [+] z))";
   9.428 +      by (asm_simp only: vs_add_left_commute);
   9.429 +    also; from vs n y xz; have "... = [-] y [+] y [+] (x [+] z)";
   9.430 +      by (asm_simp only: vs_add_assoc);
   9.431 +    also; have "... = (x [+] z)";
   9.432 +      by (asm_simp);
   9.433 +    finally; show ?R; by (rule sym);
   9.434 +  next;
   9.435 +    assume r: ?R;
   9.436 +    have "x [+] (y [+] z) = y [+] (x [+] z)";
   9.437 +      by (asm_simp only: vs_add_left_commute [of V x y z]);
   9.438 +    also; have "... = y [+] u";
   9.439 +      by (asm_simp only: r);
   9.440 +    finally; show ?L; .;
   9.441 +  qed;
   9.442 +qed;
   9.443 +
   9.444 +lemma vs_add_cancel_end: 
   9.445 +  "[| is_vectorspace V;  x:V; y:V; z:V |] ==> (x [+] (y [+] z) = y) = (x = [-] z)"
   9.446 +  (concl is "?L = ?R" );
   9.447 +proof -;
   9.448 +  assume vs: "is_vectorspace V";
   9.449 +  assume x: "x:V";
   9.450 +  assume y: "y:V"; 
   9.451 +  assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
   9.452 +  hence nz: "[-] z: V"; by (asm_simp);
   9.453 +  show "?L = ?R";
   9.454 +  proof;
   9.455 +    assume l: ?L;
   9.456 +    have n: "<0>:V"; by (asm_simp);
   9.457 +    have "y [+] <0> = y";
   9.458 +      by (asm_simp only: vs_add_zero_right); 
   9.459 +    also; have "... =  x [+] (y [+] z)";
   9.460 +      by (asm_simp only: l); 
   9.461 +    also; have "... = y [+] (x [+] z)";
   9.462 +      by (asm_simp only: vs_add_left_commute); 
   9.463 +    finally; have "y [+] <0> = y [+] (x [+] z)"; .;
   9.464 +    with vs y n xz; have "<0> = x [+] z";
   9.465 +      by (rule vs_add_left_cancel [RS iffD1]); 
   9.466 +    with vs x z; have "z = [-] x";
   9.467 +      by (asm_simp only: vs_add_minus_eq_minus);
   9.468 +    then; show ?R; 
   9.469 +      by (asm_simp); 
   9.470 +  next;
   9.471 +    assume r: ?R;
   9.472 +    have "x [+] (y [+] z) = [-] z [+] (y [+] z)";
   9.473 +      by (asm_simp only: r); 
   9.474 +    also; from vs nz y z; have "... = y [+] ([-] z [+] z)";
   9.475 +       by (asm_simp only: vs_add_left_commute);
   9.476 +    also; have "... = y [+] <0>";
   9.477 +      by (asm_simp);
   9.478 +    also; have "... = y";
   9.479 +      by (asm_simp);
   9.480 +    finally; show ?L; .;
   9.481 +  qed;
   9.482 +qed;
   9.483 +
   9.484 +lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
   9.485 +  by (asm_simp); 
   9.486 +
   9.487 +
   9.488 +end;
   9.489 \ No newline at end of file
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Fri Sep 10 17:28:51 1999 +0200
    10.3 @@ -0,0 +1,53 @@
    10.4 +
    10.5 +theory Linearform = LinearSpace:;
    10.6 +
    10.7 +section {* linearforms *};
    10.8 +
    10.9 +constdefs
   10.10 +  is_linearform :: "['a set, 'a => real] => bool" 
   10.11 +  "is_linearform V f == 
   10.12 +      (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) &
   10.13 +      (ALL x: V. ALL a. f (a [*] x) = a * (f x))"; 
   10.14 +
   10.15 +lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
   10.16 +    !! x c. x : V ==> f (c [*] x) = c * f x |]
   10.17 + ==> is_linearform V f";
   10.18 + by (unfold is_linearform_def, force);
   10.19 +
   10.20 +lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
   10.21 + by (unfold is_linearform_def, auto);
   10.22 +
   10.23 +lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
   10.24 + by (unfold is_linearform_def, auto);
   10.25 +
   10.26 +lemma linearform_neg_linear:
   10.27 +  "[|  is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
   10.28 +proof -; 
   10.29 +  assume "is_linearform V f" "is_vectorspace V" "x:V"; 
   10.30 +  have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1);
   10.31 +  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
   10.32 +  also; have "... = - (f x)"; by asm_simp;
   10.33 +  finally; show ?thesis; .;
   10.34 +qed;
   10.35 +
   10.36 +lemma linearform_diff_linear: 
   10.37 +  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";  
   10.38 +proof -;
   10.39 +  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
   10.40 +  have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
   10.41 +  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+);
   10.42 +  also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
   10.43 +  finally; show "f (x [-] y) = f x - f y"; by asm_simp;
   10.44 +qed;
   10.45 +
   10.46 +lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
   10.47 +proof -; 
   10.48 +  assume "is_vectorspace V" "is_linearform V f";
   10.49 +  have "f <0> = f (<0> [-] <0>)"; by asm_simp;
   10.50 +  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+;
   10.51 +  also; have "... = 0r"; by simp;
   10.52 +  finally; show "f <0> = 0r"; .;
   10.53 +qed; 
   10.54 +
   10.55 +end;
   10.56 +
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Sep 10 17:28:51 1999 +0200
    11.3 @@ -0,0 +1,142 @@
    11.4 +
    11.5 +theory NormedSpace =  Subspace:;
    11.6 +
    11.7 +
    11.8 +section {* normed vector spaces *};
    11.9 +
   11.10 +subsection {* quasinorm *};
   11.11 +
   11.12 +constdefs
   11.13 +  is_quasinorm :: "['a set,  'a => real] => bool"
   11.14 +  "is_quasinorm V norm == ALL x: V. ALL y:V. ALL a. 
   11.15 +        0r <= norm x 
   11.16 +      & norm (a [*] x) = (rabs a) * (norm x)
   11.17 +      & norm (x [+] y) <= norm x + norm y";
   11.18 +
   11.19 +lemma is_quasinormI[intro]: 
   11.20 +  "[| !! x y a. [| x:V; y:V|] ==>  0r <= norm x;
   11.21 +      !! x a. x:V ==> norm (a [*] x) = (rabs a) * (norm x);
   11.22 +      !! x y. [|x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y |] 
   11.23 +    ==> is_quasinorm V norm";
   11.24 +  by (unfold is_quasinorm_def, force);
   11.25 +
   11.26 +lemma quasinorm_ge_zero:
   11.27 +  "[|is_quasinorm V norm; x:V |] ==> 0r <= norm x";
   11.28 +  by (unfold is_quasinorm_def, force);
   11.29 +
   11.30 +lemma quasinorm_mult_distrib: 
   11.31 +  "[|is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
   11.32 +  by (unfold is_quasinorm_def, force);
   11.33 +
   11.34 +lemma quasinorm_triangle_ineq: 
   11.35 +  "[|is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
   11.36 +  by (unfold is_quasinorm_def, force);
   11.37 +
   11.38 +lemma quasinorm_diff_triangle_ineq: 
   11.39 +  "[|is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
   11.40 +proof -;
   11.41 +  assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
   11.42 +  have "norm (x [-] y) = norm (x [+] - 1r [*] y)";  by (simp add: diff_def negate_def);
   11.43 +  also; have "... <= norm x + norm  (- 1r [*] y)"; by (rule quasinorm_triangle_ineq, asm_simp+);
   11.44 +  also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; by (rule quasinorm_mult_distrib);
   11.45 +  also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   11.46 +  finally; show "norm (x [-] y) <= norm x + norm y"; by simp;
   11.47 +qed;
   11.48 +
   11.49 +lemma quasinorm_minus: 
   11.50 +  "[|is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
   11.51 +proof -;
   11.52 +  assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
   11.53 +  have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force;
   11.54 +  also; have "... = rabs (-1r) * norm x"; by (rule quasinorm_mult_distrib);
   11.55 +  also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   11.56 +  finally; show "norm ([-] x) = norm x"; by simp;
   11.57 +qed;
   11.58 +
   11.59 +
   11.60 +subsection {* norm *};
   11.61 +
   11.62 +constdefs
   11.63 +  is_norm :: "['a set, 'a => real] => bool"
   11.64 +  "is_norm V norm == ALL x: V.  is_quasinorm V norm 
   11.65 +      & (norm x = 0r) = (x = <0>)";
   11.66 +
   11.67 +lemma is_norm_I: "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
   11.68 +  by (unfold is_norm_def, force);
   11.69 +
   11.70 +lemma norm_is_quasinorm: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
   11.71 +  by (unfold is_norm_def, force);
   11.72 +
   11.73 +lemma norm_zero_iff: "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
   11.74 +  by (unfold is_norm_def, force);
   11.75 +
   11.76 +lemma norm_ge_zero:
   11.77 +  "[|is_norm V norm; x:V |] ==> 0r <= norm x";
   11.78 +  by (unfold is_norm_def, unfold is_quasinorm_def, force);
   11.79 +
   11.80 +
   11.81 +subsection {* normed vector space *};
   11.82 +
   11.83 +constdefs
   11.84 +  is_normed_vectorspace :: "['a set, 'a => real] => bool"
   11.85 +  "is_normed_vectorspace V norm ==
   11.86 +      is_vectorspace V &
   11.87 +      is_norm V norm";
   11.88 +
   11.89 +lemma normed_vsI: "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
   11.90 +  by (unfold is_normed_vectorspace_def, intro conjI);
   11.91 +
   11.92 +lemma normed_vs_vs: "is_normed_vectorspace V norm ==> is_vectorspace V";
   11.93 +  by (unfold is_normed_vectorspace_def, force);
   11.94 +
   11.95 +lemma normed_vs_norm: "is_normed_vectorspace V norm ==> is_norm V norm";
   11.96 +  by (unfold is_normed_vectorspace_def, force);
   11.97 +
   11.98 +lemma normed_vs_norm_ge_zero: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
   11.99 +  by (unfold is_normed_vectorspace_def, elim conjE, rule norm_ge_zero);
  11.100 +
  11.101 +lemma normed_vs_norm_gt_zero: 
  11.102 +  "[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
  11.103 +proof (unfold is_normed_vectorspace_def, elim conjE);
  11.104 +  assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
  11.105 +  have "0r <= norm x"; by (rule norm_ge_zero);
  11.106 +  also; have "0r ~= norm x";
  11.107 +  proof; 
  11.108 +    presume "norm x = 0r";
  11.109 +    have "x = <0>"; by (asm_simp add: norm_zero_iff);
  11.110 +    thus "False"; by contradiction;
  11.111 +  qed (rule sym);
  11.112 +  finally; show "0r < norm x"; .;
  11.113 +qed;
  11.114 +
  11.115 +lemma normed_vs_norm_mult_distrib: 
  11.116 +  "[| is_normed_vectorspace V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
  11.117 +  by (unfold is_normed_vectorspace_def, elim conjE, 
  11.118 +      rule quasinorm_mult_distrib, rule norm_is_quasinorm);
  11.119 +
  11.120 +lemma normed_vs_norm_triangle_ineq: 
  11.121 +  "[| is_normed_vectorspace V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
  11.122 +  by (unfold is_normed_vectorspace_def, elim conjE, 
  11.123 +      rule quasinorm_triangle_ineq, rule norm_is_quasinorm);
  11.124 +
  11.125 +lemma subspace_normed_vs: 
  11.126 +  "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm";
  11.127 +proof (rule normed_vsI);
  11.128 +  assume "is_subspace F E" "is_vectorspace E" "is_normed_vectorspace E norm";
  11.129 +  show "is_vectorspace F"; by (rule subspace_vs);
  11.130 +  show "is_norm F norm"; 
  11.131 +  proof (intro is_norm_I ballI conjI);
  11.132 +    show "is_quasinorm F norm"; 
  11.133 +    proof (rule is_quasinormI, rule normed_vs_norm_ge_zero [of E norm], 
  11.134 +       rule normed_vs_norm_mult_distrib [of E norm], rule normed_vs_norm_triangle_ineq);
  11.135 +    qed ( rule subsetD [OF subspace_subset], assumption+)+; 
  11.136 +
  11.137 +    fix x; assume "x : F";
  11.138 +    have n: "is_norm E norm"; by (unfold is_normed_vectorspace_def, asm_simp);
  11.139 +    have "x:E"; by (rule subsetD [OF subspace_subset]);
  11.140 +    from n this; show "(norm x = 0r) = (x = <0>)"; by (rule norm_zero_iff);
  11.141 +  qed;
  11.142 +qed;
  11.143 +
  11.144 +end;
  11.145 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Real/HahnBanach/ROOT.ML	Fri Sep 10 17:28:51 1999 +0200
    12.3 @@ -0,0 +1,8 @@
    12.4 +(*  Title:      HOL/Real/HahnBanach/ROOT.ML
    12.5 +    ID:         $Id$
    12.6 +    Author:     Gertrud Bauer, TU Munich
    12.7 +
    12.8 +The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
    12.9 +*)
   12.10 +
   12.11 +time_use_thy "HahnBanach";
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Sep 10 17:28:51 1999 +0200
    13.3 @@ -0,0 +1,319 @@
    13.4 +
    13.5 +theory Subspace = LinearSpace:;
    13.6 +
    13.7 +
    13.8 +section {* subspaces *};
    13.9 +
   13.10 +constdefs
   13.11 +  is_subspace ::  "['a set, 'a set] => bool"
   13.12 +  "is_subspace U V ==  <0>:U  & U <= V 
   13.13 +     &  (ALL x:U. ALL y:U. ALL a. x [+] y : U                          
   13.14 +                       & a [*] x : U)";                            
   13.15 +
   13.16 +lemma subspace_I: 
   13.17 +  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
   13.18 +  \ ==> is_subspace U V";
   13.19 +  by (unfold is_subspace_def) blast;
   13.20 +
   13.21 +lemma "is_subspace U V ==> U ~= {}";
   13.22 +  by (unfold is_subspace_def) force;
   13.23 +
   13.24 +lemma zero_in_subspace: "is_subspace U V ==> <0>:U";
   13.25 +  by (unfold is_subspace_def) force;
   13.26 +
   13.27 +lemma subspace_subset: "is_subspace U V ==> U <= V";
   13.28 +  by (unfold is_subspace_def) fast;
   13.29 +
   13.30 +lemma subspace_subset2 [simp]: "[| is_subspace U V; x:U |]==> x:V";
   13.31 +  by (unfold is_subspace_def) fast;
   13.32 +
   13.33 +lemma subspace_add_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
   13.34 +  by (unfold is_subspace_def) asm_simp;
   13.35 +
   13.36 +lemma subspace_mult_closed [simp]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
   13.37 +  by (unfold is_subspace_def) asm_simp;
   13.38 +
   13.39 +lemma subspace_diff_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
   13.40 +  by (unfold diff_def negate_def) asm_simp;
   13.41 +
   13.42 +lemma subspace_neg_closed [simp]: "[| is_subspace U V; x: U |] ==> [-] x: U";
   13.43 + by (unfold negate_def) asm_simp;
   13.44 +
   13.45 +theorem subspace_vs [intro!!]:
   13.46 +  "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
   13.47 +proof -;
   13.48 +  presume "U <= V";
   13.49 +  assume "is_vectorspace V";
   13.50 +  assume "is_subspace U V";
   13.51 +  show ?thesis;
   13.52 +  proof (rule vs_I);
   13.53 +    show "<0>:U"; by (rule zero_in_subspace);
   13.54 +    show "ALL x:U. ALL a. a [*] x : U"; by asm_simp;
   13.55 +    show "ALL x:U. ALL y:U. x [+] y : U"; by asm_simp;
   13.56 +  qed (asm_simp add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
   13.57 +next;
   13.58 +  assume "is_subspace U V";
   13.59 +  show "U <= V"; by (rule subspace_subset);
   13.60 +qed;
   13.61 +
   13.62 +lemma subspace_refl: "is_vectorspace V ==> is_subspace V V";
   13.63 +proof (unfold is_subspace_def, intro conjI); 
   13.64 +  assume "is_vectorspace V";
   13.65 +  show "<0> : V"; by (rule zero_in_vs [of V], assumption);
   13.66 +  show "V <= V"; by (simp);
   13.67 +  show "ALL x::'a:V. ALL y::'a:V. ALL a::real. x [+] y : V & a [*] x : V"; by (asm_simp);
   13.68 +qed;
   13.69 +
   13.70 +lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
   13.71 +proof (rule subspace_I); 
   13.72 +  assume "is_subspace U V" "is_subspace V W";
   13.73 +  show "<0> : U"; by (rule zero_in_subspace);;
   13.74 +  from subspace_subset [of U] subspace_subset [of V]; show uw: "U <= W"; by force;
   13.75 +  show "ALL x:U. ALL y:U. x [+] y : U"; 
   13.76 +  proof (intro ballI);
   13.77 +    fix x y; assume "x:U" "y:U";
   13.78 +    show "x [+] y : U"; by (rule subspace_add_closed);
   13.79 +  qed;
   13.80 +  show "ALL x:U. ALL a. a [*] x : U";
   13.81 +  proof (intro ballI allI);
   13.82 +    fix x a; assume "x:U";
   13.83 +    show "a [*] x : U"; by (rule subspace_mult_closed);
   13.84 +  qed;
   13.85 +qed;
   13.86 +
   13.87 +
   13.88 +section {* linear closure *};
   13.89 +
   13.90 +constdefs
   13.91 +  lin :: "'a => 'a set"
   13.92 +  "lin x == {y. ? a. y = a [*] x}";
   13.93 +
   13.94 +lemma linD: "x : lin v = (? a::real. x = a [*] v)";
   13.95 +  by (unfold lin_def) fast;
   13.96 +
   13.97 +lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
   13.98 +proof (unfold lin_def, intro CollectI exI);
   13.99 +  assume "is_vectorspace V" "x:V";
  13.100 +  show "x = 1r [*] x"; by (asm_simp);
  13.101 +qed;
  13.102 +
  13.103 +lemma lin_subspace: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
  13.104 +proof (rule subspace_I);
  13.105 +  assume "is_vectorspace V" "x:V";
  13.106 +  show "<0> : lin x"; 
  13.107 +  proof (unfold lin_def, intro CollectI exI);
  13.108 +    show "<0> = 0r [*] x"; by asm_simp;
  13.109 +  qed;
  13.110 +  show "lin x <= V";
  13.111 +  proof (unfold lin_def, intro subsetI, elim CollectD [elimify] exE); 
  13.112 +    fix xa a; assume "xa = a [*] x"; show "xa:V"; by asm_simp;
  13.113 +  qed;
  13.114 +  show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; 
  13.115 +  proof (intro ballI);
  13.116 +    fix x1 x2; assume "x1 : lin x" "x2 : lin x"; show "x1 [+] x2 : lin x";
  13.117 +    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
  13.118 +      fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
  13.119 +      show "x1 [+] x2 = (a1 + a2) [*] x"; by (asm_simp add: vs_add_mult_distrib2);
  13.120 +    qed;
  13.121 +  qed;
  13.122 +  show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
  13.123 +  proof (intro ballI allI);
  13.124 +    fix x1 a; assume "x1 : lin x"; show "a [*] x1 : lin x";
  13.125 +    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
  13.126 +      fix a1; assume "x1 = a1 [*] x";
  13.127 +      show "a [*] x1 = (a * a1) [*] x"; by asm_simp;
  13.128 +    qed;
  13.129 +  qed; 
  13.130 +qed;
  13.131 +
  13.132 +
  13.133 +lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
  13.134 +proof (rule subspace_vs);
  13.135 +  assume "is_vectorspace V" "x:V";
  13.136 +  show "is_subspace (lin x) V"; by (rule lin_subspace);
  13.137 +qed;
  13.138 +
  13.139 +section {* sum of two vectorspaces *};
  13.140 +
  13.141 +constdefs 
  13.142 +  vectorspace_sum :: "['a set, 'a set] => 'a set"
  13.143 +  "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
  13.144 +
  13.145 +lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
  13.146 +  by (unfold vectorspace_sum_def) fast;
  13.147 +
  13.148 +lemma vs_sum_I: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
  13.149 +  by (unfold vectorspace_sum_def, intro CollectI bexI); 
  13.150 +
  13.151 +lemma subspace_vs_sum1 [intro!!]: 
  13.152 +  "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
  13.153 +proof (rule subspace_I);
  13.154 +  assume "is_vectorspace U" "is_vectorspace V";
  13.155 +  show "<0> : U"; by (rule zero_in_vs);
  13.156 +  show "U <= vectorspace_sum U V";
  13.157 +  proof (intro subsetI vs_sum_I);
  13.158 +  fix x; assume "x:U";
  13.159 +    show "x = x [+] <0>"; by asm_simp;
  13.160 +    show "<0> : V"; by asm_simp;
  13.161 +  qed;
  13.162 +  show "ALL x:U. ALL y:U. x [+] y : U"; 
  13.163 +  proof (intro ballI);
  13.164 +    fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by asm_simp;
  13.165 +  qed;
  13.166 +  show "ALL x:U. ALL a. a [*] x : U"; 
  13.167 +  proof (intro ballI allI);
  13.168 +    fix x a; assume "x:U"; show "a [*] x : U"; by asm_simp;
  13.169 +  qed;
  13.170 +qed;
  13.171 +
  13.172 +lemma vs_sum_subspace: 
  13.173 +  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_subspace (vectorspace_sum U V) E";
  13.174 +proof (rule subspace_I);
  13.175 +  assume u: "is_subspace U E" and v: "is_subspace V E" and e: "is_vectorspace E";
  13.176 +
  13.177 +  show "<0> : vectorspace_sum U V";
  13.178 +  by (intro vs_sum_I, rule vs_add_zero_left [RS sym], 
  13.179 +      rule zero_in_subspace, rule zero_in_subspace, rule zero_in_vs); 
  13.180 +
  13.181 +  show "vectorspace_sum U V <= E";
  13.182 +  proof (intro subsetI, elim vs_sumD [RS iffD1, elimify] bexE);
  13.183 +    fix x u v; assume "u : U" "v : V" "x = u [+] v";
  13.184 +    show "x:E"; by (asm_simp);
  13.185 +  qed;
  13.186 +  
  13.187 +  show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
  13.188 +  proof (intro ballI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
  13.189 +    fix x y ux vx uy vy; assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
  13.190 +    show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by asm_simp;
  13.191 +  qed asm_simp+;
  13.192 +
  13.193 +  show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
  13.194 +  proof (intro ballI allI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
  13.195 +    fix a x u v; assume "u : U" "v : V" "x = u [+] v";
  13.196 +    show "a [*] x = (a [*] u) [+] (a [*] v)"; by (asm_simp add: vs_add_mult_distrib1 [OF e]);
  13.197 +  qed asm_simp+;
  13.198 +qed;
  13.199 +
  13.200 +lemma vs_sum_vs: 
  13.201 +  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_vectorspace (vectorspace_sum U V)";
  13.202 +  by (rule subspace_vs [OF vs_sum_subspace]);
  13.203 +
  13.204 +
  13.205 +section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
  13.206 +
  13.207 +
  13.208 +lemma lemma4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
  13.209 +  x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
  13.210 +  ==> y1 = y2 & a1 = a2";
  13.211 +proof;
  13.212 +  assume "is_vectorspace E" "is_subspace H E"
  13.213 +         "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
  13.214 +         "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
  13.215 +  have h: "is_vectorspace H"; by (rule subspace_vs);
  13.216 +  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0"; 
  13.217 +    by (rule vs_add_diff_swap) asm_simp+;
  13.218 +  also; have "... = (a2 - a1) [*] x0";
  13.219 +    by (rule vs_diff_mult_distrib2 [RS sym]);
  13.220 +  finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
  13.221 +
  13.222 +  have y: "y1 [-] y2 : H"; by asm_simp;
  13.223 +  have x: "(a2 - a1) [*] x0 : lin x0"; by (asm_simp add: lin_def) force; 
  13.224 +  from y; have y': "y1 [-] y2 : lin x0"; by (simp only: eq x);
  13.225 +  from x; have x': "(a2 - a1) [*] x0 : H"; by (simp only: eq [RS sym] y);
  13.226 +
  13.227 +  have int: "H Int (lin x0) = {<0>}"; 
  13.228 +  proof;
  13.229 +    show "H Int lin x0 <= {<0>}"; 
  13.230 +    proof (intro subsetI, unfold lin_def, elim IntE CollectD[elimify] exE,
  13.231 +      rule singleton_iff[RS iffD2]);
  13.232 +      fix x a; assume "x : H" and ax0: "x = a [*] x0";
  13.233 +      show "x = <0>";
  13.234 +      proof (rule case [of "a=0r"]);
  13.235 +        assume "a = 0r"; show ?thesis; by asm_simp;
  13.236 +      next;
  13.237 +        assume "a ~= 0r"; 
  13.238 +        have "(rinv a) [*] a [*] x0 : H"; 
  13.239 +          by (rule vs_mult_closed [OF h]) asm_simp;
  13.240 +        also; have "(rinv a) [*] a [*] x0 = x0"; by asm_simp;
  13.241 +        finally; have "x0 : H"; .;
  13.242 +        thus ?thesis; by contradiction;
  13.243 +      qed;
  13.244 +    qed;
  13.245 +    show "{<0>} <= H Int lin x0"; 
  13.246 +    proof (intro subsetI, elim singletonD[elimify], intro IntI, asm_simp+);
  13.247 +      show "<0> : H"; by (rule zero_in_vs [OF h]);
  13.248 +      show "<0> : lin x0"; by (rule zero_in_vs [OF lin_vs]);
  13.249 +    qed;
  13.250 +  qed;
  13.251 +
  13.252 +  from h; show "y1 = y2";
  13.253 +  proof (rule vs_add_minus_eq);
  13.254 +    show "y1 [-] y2 = <0>";
  13.255 +      by (rule Int_singeltonD [OF int y y']); 
  13.256 +  qed;
  13.257 + 
  13.258 +  show "a1 = a2";
  13.259 +  proof (rule real_add_minus_eq [RS sym]);
  13.260 +    show "a2 - a1 = 0r";
  13.261 +    proof (rule vs_mult_zero_uniq);
  13.262 +      show "(a2 - a1) [*] x0 = <0>";  by (rule Int_singeltonD [OF int x' x]);
  13.263 +    qed;
  13.264 +  qed;
  13.265 +qed;
  13.266 +
  13.267 + 
  13.268 +lemma lemma1: 
  13.269 +  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] 
  13.270 +  ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
  13.271 +proof (rule, unfold split_paired_all);
  13.272 +  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
  13.273 +  have h: "is_vectorspace H"; by (rule subspace_vs);
  13.274 +  fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
  13.275 +  have "y = t & a = 0r"; 
  13.276 +    by (rule lemma4) (assumption+, asm_simp); 
  13.277 +  thus "(y, a) = (t, 0r)"; by asm_simp;
  13.278 +qed asm_simp+;
  13.279 +
  13.280 +
  13.281 +lemma lemma3: "!! x0 h xi x y a H. [| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
  13.282 +                            in (h y) + a * xi);
  13.283 +                  x = y [+] a [*] x0; 
  13.284 +                  is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
  13.285 +  ==> h0 x = h y + a * xi";
  13.286 +proof -;  
  13.287 +  fix x0 h xi x y a H;
  13.288 +  assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
  13.289 +                            in (h y) + a * xi)";
  13.290 +  assume "x = y [+] a [*] x0";
  13.291 +  assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
  13.292 +
  13.293 +  have "x : vectorspace_sum H (lin x0)"; 
  13.294 +    by (asm_simp add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
  13.295 +  have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
  13.296 +  proof;
  13.297 +    show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
  13.298 +      by (asm_simp, rule exI, force);
  13.299 +  next;
  13.300 +    fix xa ya;
  13.301 +    assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
  13.302 +           "(%(y,a). x = y [+] a [*] x0 & y : H) ya";
  13.303 +    show "xa = ya"; ;
  13.304 +    proof -;
  13.305 +      show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
  13.306 +        by(rule Pair_fst_snd_eq [RS iffD2]);
  13.307 +      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by force;
  13.308 +      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by force;
  13.309 +      from x y; show "fst xa = fst ya & snd xa = snd ya"; 
  13.310 +        by (elim conjE) (rule lemma4, asm_simp+);
  13.311 +    qed;
  13.312 +  qed;
  13.313 +  hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
  13.314 +    by (rule select1_equality, force);
  13.315 +  thus "h0 x = h y + a * xi"; 
  13.316 +    by (asm_simp add: Let_def);
  13.317 +qed;  
  13.318 +
  13.319 +
  13.320 +end;
  13.321 +
  13.322 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy	Fri Sep 10 17:28:51 1999 +0200
    14.3 @@ -0,0 +1,33 @@
    14.4 +
    14.5 +theory Zorn_Lemma = Zorn:;
    14.6 +
    14.7 +
    14.8 +lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==>
    14.9 + EX y: S. ALL z: S. y <= z --> y = z";
   14.10 +proof (rule Zorn_Lemma2);
   14.11 +  assume aS: "a:S";
   14.12 +  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
   14.13 +  show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
   14.14 +  proof;
   14.15 +    fix c; assume "c:chain S"; 
   14.16 +    have s: "EX x. x:c ==> Union c : S";
   14.17 +      by (rule r);
   14.18 +    show "EX y:S. ALL z:c. z <= y";
   14.19 +    proof (rule case [of "c={}"]);
   14.20 +      assume "c={}"; 
   14.21 +      show ?thesis; by fast;
   14.22 +    next;
   14.23 +      assume "c~={}";
   14.24 +      show ?thesis; 
   14.25 +      proof;
   14.26 +        have "EX x. x:c"; by fast;
   14.27 +        thus "Union c : S"; by (rule s);
   14.28 +        show "ALL z:c. z <= Union c"; by fast;
   14.29 +      qed;
   14.30 +    qed;
   14.31 +  qed;
   14.32 +qed;
   14.33 +
   14.34 +
   14.35 +
   14.36 +end;