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.108      by (simp add: is_function_norm_def);
   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;