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.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 -
```