src/HOL/Real/HahnBanach/FunctionNorm.thy
 changeset 7566 c5a3f980a7af parent 7535 599d3414b51d child 7567 62384a807775
```     1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 17:30:55 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 17:31:20 1999 +0200
1.3 @@ -1,15 +1,17 @@
1.4 +(*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Gertrud Bauer, TU Munich
1.7 +*)
1.8
1.9  theory FunctionNorm = NormedSpace + FunctionOrder:;
1.10
1.11
1.12 -theorems [elim!!] = bspec;
1.13 -
1.14  constdefs
1.15    is_continous :: "['a set, 'a => real, 'a => real] => bool"
1.16    "is_continous V norm f == (is_linearform V f
1.17                             & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
1.18
1.19 -lemma lipschitz_continous_I:
1.20 +lemma lipschitz_continousI [intro]:
1.21    "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |]
1.22    ==> is_continous V norm f";
1.23  proof (unfold is_continous_def, intro exI conjI ballI);
1.24 @@ -17,10 +19,11 @@
1.25    fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
1.26  qed;
1.27
1.28 -lemma continous_linearform: "is_continous V norm f ==> is_linearform V f";
1.29 +lemma continous_linearform [intro!!]: "is_continous V norm f ==> is_linearform V f";
1.30    by (unfold is_continous_def) force;
1.31
1.32 -lemma continous_bounded: "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
1.33 +lemma continous_bounded [intro!!]:
1.34 +  "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
1.35    by (unfold is_continous_def) force;
1.36
1.37  constdefs
1.38 @@ -40,13 +43,7 @@
1.39  lemma B_not_empty: "0r : B V norm f";
1.40    by (unfold B_def, force);
1.41
1.42 -lemma le_max1: "x <= max x (y::'a::linorder)";
1.43 -  by (simp add: le_max_iff_disj[of x x y]);
1.44 -
1.45 -lemma le_max2: "y <= max x (y::'a::linorder)";
1.46 -  by (simp add: le_max_iff_disj[of y x y]);
1.47 -
1.48 -lemma ex_fnorm:
1.49 +lemma ex_fnorm [intro!!]:
1.50    "[| is_normed_vectorspace V norm; is_continous V norm f|]
1.51       ==> is_function_norm V norm f (function_norm V norm f)";
1.52  proof (unfold function_norm_def is_function_norm_def is_continous_def Sup_def, elim conjE,
1.53 @@ -67,56 +64,70 @@
1.54
1.55        show "EX Y. isUb UNIV (B V norm f) Y";
1.56        proof (intro exI isUbI setleI ballI, unfold B_def,
1.57 -	elim CollectD [elimify] disjE bexE conjE);
1.58 +	elim CollectE disjE bexE conjE);
1.59  	fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)";
1.60          from a; have le: "rabs (f x) <= c * norm x"; ..;
1.61          have "y = rabs (f x) * rinv (norm x)";.;
1.62          also; from _  le; have "... <= c * norm x * rinv (norm x)";
1.63          proof (rule real_mult_le_le_mono2);
1.64            show "0r <= rinv (norm x)";
1.65 -            by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero);
1.66 +          proof (rule less_imp_le);
1.67 +            show "0r < rinv (norm x)";
1.68 +            proof (rule real_rinv_gt_zero);
1.69 +              show "0r < norm x"; ..;
1.70 +            qed;
1.71 +          qed;
1.72 +     (*** or:  by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
1.73          qed;
1.74          also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
1.75          also; have "(norm x * rinv (norm x)) = 1r";
1.76          proof (rule real_mult_inv_right);
1.77            show "norm x ~= 0r";
1.78 -            by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero);
1.79 +          proof (rule not_sym);
1.80 +            show "0r ~= norm x";
1.81 +            proof (rule lt_imp_not_eq);
1.82 +              show "0r < norm x"; ..;
1.83 +            qed;
1.84 +          qed;
1.85 +     (*** or:  by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero); ***)
1.86          qed;
1.87 -        also; have "c * ... = c"; by asm_simp;
1.88 -        also; have "... <= b"; by (asm_simp add: le_max1);
1.89 +        also; have "c * ... = c"; by (simp!);
1.90 +        also; have "... <= b"; by (simp! add: le_max1);
1.91  	finally; show "y <= b"; .;
1.92        next;
1.93 -	fix y; assume "y = 0r"; show "y <= b"; by (asm_simp add: le_max2);
1.94 +	fix y; assume "y = 0r"; show "y <= b"; by (simp! add: le_max2);
1.95        qed simp;
1.96      qed;
1.97    qed;
1.98  qed;
1.99
1.100 -lemma fnorm_ge_zero: "[| is_continous V norm f; is_normed_vectorspace V norm|]
1.101 +lemma fnorm_ge_zero [intro!!]: "[| is_continous V norm f; is_normed_vectorspace V norm|]
1.102     ==> 0r <= function_norm V norm f";
1.103  proof -;
1.104    assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
1.105 -  have "is_function_norm V norm f (function_norm V norm f)"; by (rule ex_fnorm);
1.106 +  have "is_function_norm V norm f (function_norm V norm f)"; ..;
1.107    hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)";
1.109    show ?thesis;
1.110    proof (unfold function_norm_def, rule sup_ub1);
1.111      show "ALL x:(B V norm f). 0r <= x";
1.112 -    proof (intro ballI, unfold B_def, elim CollectD [elimify] bexE conjE disjE);
1.113 -      fix x r; assume "is_normed_vectorspace V norm" "x : V" "x ~= <0>"
1.114 +    proof (intro ballI, unfold B_def, elim CollectE bexE conjE disjE);
1.115 +      fix x r; assume "x : V" "x ~= <0>"
1.116          "r = rabs (f x) * rinv (norm x)";
1.117        show  "0r <= r";
1.118 -      proof (asm_simp, rule real_le_mult_order);
1.119 -        show "0r <= rabs (f x)"; by (asm_simp only: rabs_ge_zero);
1.120 +      proof (simp!, rule real_le_mult_order);
1.121 +        show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
1.122          show "0r <= rinv (norm x)";
1.123          proof (rule less_imp_le);
1.124            show "0r < rinv (norm x)";
1.125 -            by (rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero [of V norm]);
1.126 +          proof (rule real_rinv_gt_zero);
1.127 +            show "0r < norm x"; ..;
1.128 +          qed;
1.129          qed;
1.130        qed;
1.131 -    qed asm_simp;
1.132 +    qed (simp!);
1.133      from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
1.134 -      by (asm_simp add: is_function_norm_def function_norm_def);
1.135 +      by (simp! add: is_function_norm_def function_norm_def);
1.136      show "0r : B V norm f"; by (rule B_not_empty);
1.137    qed;
1.138  qed;
1.139 @@ -127,27 +138,31 @@
1.140      ==> rabs (f x) <= (function_norm V norm f) * norm x";
1.141  proof -;
1.142    assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
1.143 -  have v: "is_vectorspace V"; by (rule normed_vs_vs);
1.144 +  have v: "is_vectorspace V"; ..;
1.145    assume "x:V";
1.146    show "?thesis";
1.147    proof (rule case [of "x = <0>"]);
1.148      assume "x ~= <0>";
1.149      show "?thesis";
1.150      proof -;
1.151 -      have n: "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
1.152 +      have n: "0r <= norm x"; ..;
1.153        have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f";
1.154          proof (unfold function_norm_def, rule sup_ub);
1.155            from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
1.156 -             by (asm_simp add: is_function_norm_def function_norm_def);
1.157 +             by (simp! add: is_function_norm_def function_norm_def);
1.158            show "rabs (f x) * rinv (norm x) : B V norm f";
1.159              by (unfold B_def, intro CollectI disjI2 bexI [of _ x] conjI, simp);
1.160          qed;
1.161 -      have "rabs (f x) = rabs (f x) * 1r"; by asm_simp;
1.162 +      have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
1.163        also; have "1r = rinv (norm x) * norm x";
1.164 -        by (rule real_mult_inv_left [RS sym], rule lt_imp_not_eq[RS not_sym],
1.165 -              rule normed_vs_norm_gt_zero[of V norm]);
1.166 +      proof (rule real_mult_inv_left [RS sym]);
1.167 +        show "norm x ~= 0r";
1.168 +        proof (rule lt_imp_not_eq[RS not_sym]);
1.169 +          show "0r < norm x"; ..;
1.170 +        qed;
1.171 +      qed;
1.172        also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x";
1.173 -        by (asm_simp add: real_mult_assoc [of "rabs (f x)"]);
1.174 +        by (simp! add: real_mult_assoc [of "rabs (f x)"]);
1.175        also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x";
1.176          by (rule real_mult_le_le_mono2 [OF n le]);
1.177        finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
1.178 @@ -156,13 +171,13 @@
1.179      assume "x = <0>";
1.180      then; show "?thesis";
1.181      proof -;
1.182 -      have "rabs (f x) = rabs (f <0>)"; by asm_simp;
1.183 -      also; have "f <0> = 0r"; by (rule linearform_zero [OF v continous_linearform]);
1.184 +      have "rabs (f x) = rabs (f <0>)"; by (simp!);
1.185 +      also; from v continous_linearform; have "f <0> = 0r"; ..;
1.186        also; note rabs_zero;
1.187        also; have" 0r <= function_norm V norm f * norm x";
1.188        proof (rule real_le_mult_order);
1.189 -        show "0r <= function_norm V norm f"; by (rule fnorm_ge_zero);
1.190 -        show "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
1.191 +        show "0r <= function_norm V norm f"; ..;
1.192 +        show "0r <= norm x"; ..;
1.193        qed;
1.194        finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
1.195      qed;
1.196 @@ -184,21 +199,24 @@
1.197    show "Sup UNIV (B V norm f) <= c";
1.198    proof (rule ub_ge_sup);
1.199      from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
1.200 -      by (asm_simp add: is_function_norm_def function_norm_def);
1.201 +      by (simp! add: is_function_norm_def function_norm_def);
1.202      show "isUb UNIV (B V norm f) c";
1.203      proof (intro isUbI setleI ballI);
1.204        fix y; assume "y: B V norm f";
1.205 -      show le: "y <= c";
1.206 -      proof (unfold B_def, elim CollectD [elimify] disjE bexE);
1.207 +      thus le: "y <= c";
1.208 +      proof (-, unfold B_def, elim CollectE disjE bexE);
1.209  	fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
1.210  	assume x: "x : V";
1.211 -	have lt: "0r < norm x";
1.212 -	  by (asm_simp add: normed_vs_norm_gt_zero);
1.213 -	hence "0r ~= norm x"; by (asm_simp add: order_less_imp_not_eq);
1.214 -	hence neq: "norm x ~= 0r"; by (rule not_sym);
1.215 -
1.216 +        have lt: "0r < norm x";  by (simp! add: normed_vs_norm_gt_zero);
1.217 +
1.218 +        have neq: "norm x ~= 0r";
1.219 +        proof (rule not_sym);
1.220 +          from lt; show "0r ~= norm x";
1.221 +          by (simp! add: order_less_imp_not_eq);
1.222 +        qed;
1.223 +
1.224  	from lt; have "0r < rinv (norm x)";
1.225 -	  by (asm_simp add: real_rinv_gt_zero);
1.226 +	  by (simp! add: real_rinv_gt_zero);
1.227  	then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le);
1.228
1.229  	from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
1.230 @@ -211,7 +229,7 @@
1.231  	finally; show ?thesis; .;
1.232        next;
1.233          assume "y = 0r";
1.234 -        show "y <= c"; by force;
1.235 +        show "y <= c"; by (force!);
1.236        qed;
1.237      qed force;
1.238    qed;
```