src/HOL/Real/HahnBanach/NormedSpace.thy
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7808 fd019ac3485f
     1.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Sep 21 17:30:55 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Sep 21 17:31:20 1999 +0200
     1.3 @@ -1,3 +1,7 @@
     1.4 +(*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gertrud Bauer, TU Munich
     1.7 +*)
     1.8  
     1.9  theory NormedSpace =  Subspace:;
    1.10  
    1.11 @@ -20,31 +24,31 @@
    1.12      ==> is_quasinorm V norm";
    1.13    by (unfold is_quasinorm_def, force);
    1.14  
    1.15 -lemma quasinorm_ge_zero:
    1.16 -  "[|is_quasinorm V norm; x:V |] ==> 0r <= norm x";
    1.17 +lemma quasinorm_ge_zero [intro!!]:
    1.18 +  "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x";
    1.19    by (unfold is_quasinorm_def, force);
    1.20  
    1.21  lemma quasinorm_mult_distrib: 
    1.22 -  "[|is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
    1.23 +  "[| is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
    1.24    by (unfold is_quasinorm_def, force);
    1.25  
    1.26  lemma quasinorm_triangle_ineq: 
    1.27 -  "[|is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
    1.28 +  "[| is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
    1.29    by (unfold is_quasinorm_def, force);
    1.30  
    1.31  lemma quasinorm_diff_triangle_ineq: 
    1.32 -  "[|is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
    1.33 +  "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
    1.34  proof -;
    1.35    assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
    1.36    have "norm (x [-] y) = norm (x [+] - 1r [*] y)";  by (simp add: diff_def negate_def);
    1.37 -  also; have "... <= norm x + norm  (- 1r [*] y)"; by (rule quasinorm_triangle_ineq, asm_simp+);
    1.38 +  also; have "... <= norm x + norm  (- 1r [*] y)"; by (simp! add: quasinorm_triangle_ineq);
    1.39    also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; by (rule quasinorm_mult_distrib);
    1.40    also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
    1.41    finally; show "norm (x [-] y) <= norm x + norm y"; by simp;
    1.42  qed;
    1.43  
    1.44  lemma quasinorm_minus: 
    1.45 -  "[|is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
    1.46 +  "[| is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
    1.47  proof -;
    1.48    assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
    1.49    have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force;
    1.50 @@ -61,18 +65,19 @@
    1.51    "is_norm V norm == ALL x: V.  is_quasinorm V norm 
    1.52        & (norm x = 0r) = (x = <0>)";
    1.53  
    1.54 -lemma is_norm_I: "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
    1.55 +lemma is_normI [intro]: 
    1.56 +  "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
    1.57    by (unfold is_norm_def, force);
    1.58  
    1.59 -lemma norm_is_quasinorm: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
    1.60 +lemma norm_is_quasinorm [intro!!]: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
    1.61    by (unfold is_norm_def, force);
    1.62  
    1.63  lemma norm_zero_iff: "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
    1.64    by (unfold is_norm_def, force);
    1.65  
    1.66 -lemma norm_ge_zero:
    1.67 +lemma norm_ge_zero [intro!!]:
    1.68    "[|is_norm V norm; x:V |] ==> 0r <= norm x";
    1.69 -  by (unfold is_norm_def, unfold is_quasinorm_def, force);
    1.70 +  by (unfold is_norm_def is_quasinorm_def, force);
    1.71  
    1.72  
    1.73  subsection {* normed vector space *};
    1.74 @@ -83,60 +88,65 @@
    1.75        is_vectorspace V &
    1.76        is_norm V norm";
    1.77  
    1.78 -lemma normed_vsI: "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
    1.79 -  by (unfold is_normed_vectorspace_def, intro conjI);
    1.80 +lemma normed_vsI [intro]: 
    1.81 +  "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
    1.82 +  by (unfold is_normed_vectorspace_def) blast; 
    1.83  
    1.84 -lemma normed_vs_vs: "is_normed_vectorspace V norm ==> is_vectorspace V";
    1.85 -  by (unfold is_normed_vectorspace_def, force);
    1.86 +lemma normed_vs_vs [intro!!]: "is_normed_vectorspace V norm ==> is_vectorspace V";
    1.87 +  by (unfold is_normed_vectorspace_def) force;
    1.88  
    1.89 -lemma normed_vs_norm: "is_normed_vectorspace V norm ==> is_norm V norm";
    1.90 -  by (unfold is_normed_vectorspace_def, force);
    1.91 +lemma normed_vs_norm [intro!!]: "is_normed_vectorspace V norm ==> is_norm V norm";
    1.92 +  by (unfold is_normed_vectorspace_def, elim conjE);
    1.93  
    1.94 -lemma normed_vs_norm_ge_zero: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
    1.95 -  by (unfold is_normed_vectorspace_def, elim conjE, rule norm_ge_zero);
    1.96 +lemma normed_vs_norm_ge_zero [intro!!]: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
    1.97 +  by (unfold is_normed_vectorspace_def, rule, elim conjE);
    1.98  
    1.99 -lemma normed_vs_norm_gt_zero: 
   1.100 +lemma normed_vs_norm_gt_zero [intro!!]: 
   1.101    "[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
   1.102  proof (unfold is_normed_vectorspace_def, elim conjE);
   1.103    assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
   1.104 -  have "0r <= norm x"; by (rule norm_ge_zero);
   1.105 +  have "0r <= norm x"; ..;
   1.106    also; have "0r ~= norm x";
   1.107 -  proof; 
   1.108 +  proof;
   1.109      presume "norm x = 0r";
   1.110 -    have "x = <0>"; by (asm_simp add: norm_zero_iff);
   1.111 +    also; have "?this = (x = <0>)"; by (rule norm_zero_iff);
   1.112 +    finally; have "x = <0>"; .;
   1.113      thus "False"; by contradiction;
   1.114    qed (rule sym);
   1.115    finally; show "0r < norm x"; .;
   1.116  qed;
   1.117  
   1.118 -lemma normed_vs_norm_mult_distrib: 
   1.119 +lemma normed_vs_norm_mult_distrib [intro!!]: 
   1.120    "[| is_normed_vectorspace V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
   1.121 -  by (unfold is_normed_vectorspace_def, elim conjE, 
   1.122 -      rule quasinorm_mult_distrib, rule norm_is_quasinorm);
   1.123 +  by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, rule normed_vs_norm);
   1.124  
   1.125 -lemma normed_vs_norm_triangle_ineq: 
   1.126 +lemma normed_vs_norm_triangle_ineq [intro!!]: 
   1.127    "[| is_normed_vectorspace V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
   1.128 -  by (unfold is_normed_vectorspace_def, elim conjE, 
   1.129 -      rule quasinorm_triangle_ineq, rule norm_is_quasinorm);
   1.130 +  by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, rule normed_vs_norm);
   1.131  
   1.132 -lemma subspace_normed_vs: 
   1.133 -  "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm";
   1.134 +lemma subspace_normed_vs [intro!!]: 
   1.135 +  "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] 
   1.136 +   ==> is_normed_vectorspace F norm";
   1.137  proof (rule normed_vsI);
   1.138    assume "is_subspace F E" "is_vectorspace E" "is_normed_vectorspace E norm";
   1.139 -  show "is_vectorspace F"; by (rule subspace_vs);
   1.140 +  show "is_vectorspace F"; ..;
   1.141    show "is_norm F norm"; 
   1.142 -  proof (intro is_norm_I ballI conjI);
   1.143 +  proof (intro is_normI ballI conjI);
   1.144      show "is_quasinorm F norm"; 
   1.145 -    proof (rule is_quasinormI, rule normed_vs_norm_ge_zero [of E norm], 
   1.146 -       rule normed_vs_norm_mult_distrib [of E norm], rule normed_vs_norm_triangle_ineq);
   1.147 -    qed ( rule subsetD [OF subspace_subset], assumption+)+; 
   1.148 +    proof;
   1.149 +      fix x y a; presume "x : E";
   1.150 +      show "0r <= norm x"; ..;
   1.151 +      show "norm (a [*] x) = rabs a * norm x"; ..;
   1.152 +      presume "y : E";
   1.153 +      show "norm (x [+] y) <= norm x + norm y"; ..;
   1.154 +    qed (simp!)+;
   1.155  
   1.156      fix x; assume "x : F";
   1.157 -    have n: "is_norm E norm"; by (unfold is_normed_vectorspace_def, asm_simp);
   1.158 -    have "x:E"; by (rule subsetD [OF subspace_subset]);
   1.159 -    from n this; show "(norm x = 0r) = (x = <0>)"; by (rule norm_zero_iff);
   1.160 +    show "(norm x = 0r) = (x = <0>)"; 
   1.161 +    proof (rule norm_zero_iff);
   1.162 +      show "is_norm E norm"; ..;
   1.163 +    qed (simp!);
   1.164    qed;
   1.165  qed;
   1.166  
   1.167  end;
   1.168 -