accomodate refined facts handling;
authorwenzelm
Tue Sep 21 17:31:20 1999 +0200 (1999-09-21)
changeset 7566c5a3f980a7af
parent 7565 bfa85f429629
child 7567 62384a807775
accomodate refined facts handling;
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/Subspace.thy
src/HOL/Real/HahnBanach/Zorn_Lemma.thy
     1.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 21 17:30:55 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 21 17:31:20 1999 +0200
     1.3 @@ -1,16 +1,31 @@
     1.4 +(*  Title:      HOL/Real/HahnBanach/Aux.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gertrud Bauer, TU Munich
     1.7 +*)
     1.8  
     1.9 -theory Aux = Main + Real:;
    1.10 +theory Aux = Real:;
    1.11  
    1.12 +theorems case = case_split_thm;  (* FIXME tmp *);
    1.13 +
    1.14 +lemmas CollectE = CollectD [elimify];
    1.15  
    1.16  theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y";	    (*  <=  ~=  < *)
    1.17 -  by (asm_simp add: order_less_le);
    1.18 +  by (simp! add: order_less_le);
    1.19 +
    1.20 +lemma le_max1: "x <= max x (y::'a::linorder)";
    1.21 +  by (simp add: le_max_iff_disj[of x x y]);
    1.22 +
    1.23 +lemma le_max2: "y <= max x (y::'a::linorder)"; 
    1.24 +  by (simp add: le_max_iff_disj[of y x y]);
    1.25  
    1.26  lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; 
    1.27    by (rule order_less_le[RS iffD1, RS conjunct2]);
    1.28  
    1.29 -lemma Int_singeltonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
    1.30 +lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
    1.31    by (fast elim: equalityE);
    1.32  
    1.33 +lemmas singletonE = singletonD[elimify];
    1.34 +
    1.35  lemma real_add_minus_eq: "x - y = 0r ==> x = y";
    1.36  proof -;
    1.37    assume "x - y = 0r";
    1.38 @@ -18,7 +33,7 @@
    1.39    also; have "... = 0r"; .;
    1.40    finally; have "x + - y = 0r"; .;
    1.41    hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
    1.42 -  also; have "... = y"; by asm_simp;
    1.43 +  also; have "... = y"; by (simp!);
    1.44    finally; show "x = y"; .;
    1.45  qed;
    1.46  
    1.47 @@ -29,8 +44,8 @@
    1.48      show "-1r < 0r";
    1.49        by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
    1.50    qed;
    1.51 -  also; have "... = 1r"; by asm_simp; 
    1.52 -  finally; show ?thesis; by asm_simp;
    1.53 +  also; have "... = 1r"; by (simp!); 
    1.54 +  finally; show ?thesis; by (simp!);
    1.55  qed;
    1.56  
    1.57  axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
    1.58 @@ -39,21 +54,21 @@
    1.59  
    1.60  axioms real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
    1.61  
    1.62 -axioms real_mult_diff_distrib: "a * (- x - y) = - a * x - a * y";
    1.63 +axioms real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y";
    1.64  
    1.65 -axioms real_mult_diff_distrib2: "a * (x - y) = a * x - a * y";
    1.66 +axioms real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
    1.67  
    1.68  lemma less_imp_le: "(x::real) < y ==> x <= y";
    1.69 -  by (asm_simp only: real_less_imp_le);
    1.70 +  by (simp! only: real_less_imp_le);
    1.71  
    1.72  lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
    1.73  proof -;
    1.74    assume "x <= (r::'a::order)";
    1.75    assume "x ~= r";
    1.76    then; have "x < r | x = r";
    1.77 -    by (asm_simp add: order_le_less);
    1.78 +    by (simp! add: order_le_less);
    1.79    then; show ?thesis;
    1.80 -    by asm_simp;
    1.81 +    by (simp!);
    1.82  qed;
    1.83  
    1.84  lemma minus_le: "- (x::real) <= y ==> - y <= x";
    1.85 @@ -65,11 +80,11 @@
    1.86       assume "- x < y"; show ?thesis; 
    1.87       proof -; 
    1.88         have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]); 
    1.89 -       hence "- y < x"; by asm_simp;
    1.90 +       hence "- y < x"; by (simp!);
    1.91         thus ?thesis; by (rule real_less_imp_le);
    1.92      qed;
    1.93    next; 
    1.94 -     assume "- x = y"; show ?thesis; by force;
    1.95 +     assume "- x = y"; show ?thesis; by (force!);
    1.96    qed;
    1.97  qed;
    1.98  
    1.99 @@ -82,14 +97,14 @@
   1.100      show "- r <= x & x <= r";
   1.101      proof;
   1.102        have "- x <= rabs x"; by (rule rabs_ge_minus_self);
   1.103 -      hence "- x <= r"; by asm_simp;
   1.104 -      thus "- r <= x"; by (asm_simp add : minus_le [of "x" "r"]);
   1.105 +      hence "- x <= r"; by (simp!);
   1.106 +      thus "- r <= x"; by (simp! add : minus_le [of "x" "r"]);
   1.107        have "x <= rabs x"; by (rule rabs_ge_self); 
   1.108 -      thus "x <= r"; by asm_simp; 
   1.109 +      thus "x <= r"; by (simp!); 
   1.110      qed;
   1.111    next; 
   1.112      assume "- r <= x & x <= r";
   1.113 -    show "rabs x <= r";  by fast;  
   1.114 +    show "rabs x <= r"; by (fast!);
   1.115    qed;
   1.116  next;   
   1.117    assume "rabs x ~= r";
   1.118 @@ -113,10 +128,10 @@
   1.119        show ?thesis; 
   1.120        proof (rule rabs_disj [RS disjE, of x]);
   1.121          assume  "rabs x = x";
   1.122 -        show ?thesis; by asm_simp; 
   1.123 +        show ?thesis; by (simp!); 
   1.124        next; 
   1.125          assume "rabs x = - x";
   1.126 -        from minus_le [of r x]; show ?thesis; by asm_simp;
   1.127 +        from minus_le [of r x]; show ?thesis; by (simp!);
   1.128        qed;
   1.129      qed;
   1.130    qed;
     2.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Tue Sep 21 17:30:55 1999 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Tue Sep 21 17:31:20 1999 +0200
     2.3 @@ -1,3 +1,7 @@
     2.4 +(*  Title:      HOL/Real/HahnBanach/Bounds.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Gertrud Bauer, TU Munich
     2.7 +*)
     2.8  
     2.9  theory Bounds = Main + Real:;
    2.10  
    2.11 @@ -60,8 +64,6 @@
    2.12    is_Sup :: "('a::order) set => 'a set => 'a => bool"
    2.13    "is_Sup A B x == isLub A B x"
    2.14     
    2.15 -  (* was:  x:A & is_Least (UpperBounds A B) x" *)
    2.16 -
    2.17    Sup :: "('a::order) set => 'a set => 'a"
    2.18    "Sup A B == Eps (is_Sup A B)"
    2.19  
    2.20 @@ -84,9 +86,6 @@
    2.21    "INF x. P" == "INF x:UNIV. P";
    2.22  
    2.23  
    2.24 -lemma [intro]: "[| x:A; !!y. y:B ==> y <= x |] ==> x: UpperBounds A B";
    2.25 -  by (unfold UpperBounds_def is_UpperBound_def) force;
    2.26 -
    2.27  lemma ub_ge_sup: "isUb A B y ==> is_Sup A B s ==> s <= y";
    2.28    by (unfold is_Sup_def, rule isLub_le_isUb);
    2.29  
     3.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 17:30:55 1999 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 21 17:31:20 1999 +0200
     3.3 @@ -1,15 +1,17 @@
     3.4 +(*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Gertrud Bauer, TU Munich
     3.7 +*)
     3.8  
     3.9  theory FunctionNorm = NormedSpace + FunctionOrder:;
    3.10  
    3.11  
    3.12 -theorems [elim!!] = bspec;
    3.13 -
    3.14  constdefs
    3.15    is_continous :: "['a set, 'a => real, 'a => real] => bool" 
    3.16    "is_continous V norm f == (is_linearform V f
    3.17                             & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
    3.18  
    3.19 -lemma lipschitz_continous_I: 
    3.20 +lemma lipschitz_continousI [intro]: 
    3.21    "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] 
    3.22    ==> is_continous V norm f";
    3.23  proof (unfold is_continous_def, intro exI conjI ballI);
    3.24 @@ -17,10 +19,11 @@
    3.25    fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
    3.26  qed;
    3.27    
    3.28 -lemma continous_linearform: "is_continous V norm f ==> is_linearform V f";
    3.29 +lemma continous_linearform [intro!!]: "is_continous V norm f ==> is_linearform V f";
    3.30    by (unfold is_continous_def) force;
    3.31  
    3.32 -lemma continous_bounded: "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
    3.33 +lemma continous_bounded [intro!!]:
    3.34 +  "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
    3.35    by (unfold is_continous_def) force;
    3.36  
    3.37  constdefs
    3.38 @@ -40,13 +43,7 @@
    3.39  lemma B_not_empty: "0r : B V norm f";
    3.40    by (unfold B_def, force);
    3.41  
    3.42 -lemma le_max1: "x <= max x (y::'a::linorder)";
    3.43 -  by (simp add: le_max_iff_disj[of x x y]);
    3.44 -
    3.45 -lemma le_max2: "y <= max x (y::'a::linorder)"; 
    3.46 -  by (simp add: le_max_iff_disj[of y x y]);
    3.47 -
    3.48 -lemma ex_fnorm: 
    3.49 +lemma ex_fnorm [intro!!]: 
    3.50    "[| is_normed_vectorspace V norm; is_continous V norm f|]
    3.51       ==> is_function_norm V norm f (function_norm V norm f)"; 
    3.52  proof (unfold function_norm_def is_function_norm_def is_continous_def Sup_def, elim conjE, 
    3.53 @@ -67,56 +64,70 @@
    3.54  
    3.55        show "EX Y. isUb UNIV (B V norm f) Y";
    3.56        proof (intro exI isUbI setleI ballI, unfold B_def, 
    3.57 -	elim CollectD [elimify] disjE bexE conjE);
    3.58 +	elim CollectE disjE bexE conjE);
    3.59  	fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)";
    3.60          from a; have le: "rabs (f x) <= c * norm x"; ..;
    3.61          have "y = rabs (f x) * rinv (norm x)";.;
    3.62          also; from _  le; have "... <= c * norm x * rinv (norm x)";
    3.63          proof (rule real_mult_le_le_mono2);
    3.64            show "0r <= rinv (norm x)";
    3.65 -            by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero);
    3.66 +          proof (rule less_imp_le);
    3.67 +            show "0r < rinv (norm x)";
    3.68 +            proof (rule real_rinv_gt_zero);
    3.69 +              show "0r < norm x"; ..;
    3.70 +            qed;
    3.71 +          qed;
    3.72 +     (*** or:  by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
    3.73          qed;
    3.74          also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
    3.75          also; have "(norm x * rinv (norm x)) = 1r"; 
    3.76          proof (rule real_mult_inv_right);
    3.77            show "norm x ~= 0r"; 
    3.78 -            by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero);
    3.79 +          proof (rule not_sym);
    3.80 +            show "0r ~= norm x"; 
    3.81 +            proof (rule lt_imp_not_eq);
    3.82 +              show "0r < norm x"; ..;
    3.83 +            qed;
    3.84 +          qed;
    3.85 +     (*** or:  by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero); ***)
    3.86          qed;
    3.87 -        also; have "c * ... = c"; by asm_simp;
    3.88 -        also; have "... <= b"; by (asm_simp add: le_max1);
    3.89 +        also; have "c * ... = c"; by (simp!);
    3.90 +        also; have "... <= b"; by (simp! add: le_max1);
    3.91  	finally; show "y <= b"; .;
    3.92        next; 
    3.93 -	fix y; assume "y = 0r"; show "y <= b"; by (asm_simp add: le_max2);
    3.94 +	fix y; assume "y = 0r"; show "y <= b"; by (simp! add: le_max2);
    3.95        qed simp;
    3.96      qed;
    3.97    qed;
    3.98  qed;
    3.99  
   3.100 -lemma fnorm_ge_zero: "[| is_continous V norm f; is_normed_vectorspace V norm|]
   3.101 +lemma fnorm_ge_zero [intro!!]: "[| is_continous V norm f; is_normed_vectorspace V norm|]
   3.102     ==> 0r <= function_norm V norm f";
   3.103  proof -;
   3.104    assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
   3.105 -  have "is_function_norm V norm f (function_norm V norm f)"; by (rule ex_fnorm);
   3.106 +  have "is_function_norm V norm f (function_norm V norm f)"; ..;
   3.107    hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)"; 
   3.108      by (simp add: is_function_norm_def);
   3.109    show ?thesis; 
   3.110    proof (unfold function_norm_def, rule sup_ub1);
   3.111      show "ALL x:(B V norm f). 0r <= x"; 
   3.112 -    proof (intro ballI, unfold B_def, elim CollectD [elimify] bexE conjE disjE);
   3.113 -      fix x r; assume "is_normed_vectorspace V norm" "x : V" "x ~= <0>" 
   3.114 +    proof (intro ballI, unfold B_def, elim CollectE bexE conjE disjE);
   3.115 +      fix x r; assume "x : V" "x ~= <0>" 
   3.116          "r = rabs (f x) * rinv (norm x)"; 
   3.117        show  "0r <= r";
   3.118 -      proof (asm_simp, rule real_le_mult_order);
   3.119 -        show "0r <= rabs (f x)"; by (asm_simp only: rabs_ge_zero);
   3.120 +      proof (simp!, rule real_le_mult_order);
   3.121 +        show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
   3.122          show "0r <= rinv (norm x)";
   3.123          proof (rule less_imp_le);
   3.124            show "0r < rinv (norm x)"; 
   3.125 -            by (rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero [of V norm]);
   3.126 +          proof (rule real_rinv_gt_zero);
   3.127 +            show "0r < norm x"; ..;
   3.128 +          qed;
   3.129          qed;
   3.130        qed;
   3.131 -    qed asm_simp;
   3.132 +    qed (simp!);
   3.133      from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
   3.134 -      by (asm_simp add: is_function_norm_def function_norm_def); 
   3.135 +      by (simp! add: is_function_norm_def function_norm_def); 
   3.136      show "0r : B V norm f"; by (rule B_not_empty);
   3.137    qed;
   3.138  qed;
   3.139 @@ -127,27 +138,31 @@
   3.140      ==> rabs (f x) <= (function_norm V norm f) * norm x"; 
   3.141  proof -; 
   3.142    assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
   3.143 -  have v: "is_vectorspace V"; by (rule normed_vs_vs);
   3.144 +  have v: "is_vectorspace V"; ..;
   3.145    assume "x:V";
   3.146    show "?thesis";
   3.147    proof (rule case [of "x = <0>"]);
   3.148      assume "x ~= <0>";
   3.149      show "?thesis";
   3.150      proof -;
   3.151 -      have n: "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
   3.152 +      have n: "0r <= norm x"; ..;
   3.153        have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f"; 
   3.154          proof (unfold function_norm_def, rule sup_ub);
   3.155            from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
   3.156 -             by (asm_simp add: is_function_norm_def function_norm_def); 
   3.157 +             by (simp! add: is_function_norm_def function_norm_def); 
   3.158            show "rabs (f x) * rinv (norm x) : B V norm f"; 
   3.159              by (unfold B_def, intro CollectI disjI2 bexI [of _ x] conjI, simp);
   3.160          qed;
   3.161 -      have "rabs (f x) = rabs (f x) * 1r"; by asm_simp;
   3.162 +      have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
   3.163        also; have "1r = rinv (norm x) * norm x"; 
   3.164 -        by (rule real_mult_inv_left [RS sym], rule lt_imp_not_eq[RS not_sym], 
   3.165 -              rule normed_vs_norm_gt_zero[of V norm]);
   3.166 +      proof (rule real_mult_inv_left [RS sym]);
   3.167 +        show "norm x ~= 0r";
   3.168 +        proof (rule lt_imp_not_eq[RS not_sym]);
   3.169 +          show "0r < norm x"; ..;
   3.170 +        qed;
   3.171 +      qed;
   3.172        also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x"; 
   3.173 -        by (asm_simp add: real_mult_assoc [of "rabs (f x)"]);
   3.174 +        by (simp! add: real_mult_assoc [of "rabs (f x)"]);
   3.175        also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x"; 
   3.176          by (rule real_mult_le_le_mono2 [OF n le]);
   3.177        finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
   3.178 @@ -156,13 +171,13 @@
   3.179      assume "x = <0>";
   3.180      then; show "?thesis";
   3.181      proof -;
   3.182 -      have "rabs (f x) = rabs (f <0>)"; by asm_simp;
   3.183 -      also; have "f <0> = 0r"; by (rule linearform_zero [OF v continous_linearform]); 
   3.184 +      have "rabs (f x) = rabs (f <0>)"; by (simp!);
   3.185 +      also; from v continous_linearform; have "f <0> = 0r"; ..;
   3.186        also; note rabs_zero;
   3.187        also; have" 0r <= function_norm V norm f * norm x";
   3.188        proof (rule real_le_mult_order);
   3.189 -        show "0r <= function_norm V norm f"; by (rule fnorm_ge_zero);
   3.190 -        show "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
   3.191 +        show "0r <= function_norm V norm f"; ..;
   3.192 +        show "0r <= norm x"; ..;
   3.193        qed;
   3.194        finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
   3.195      qed;
   3.196 @@ -184,21 +199,24 @@
   3.197    show "Sup UNIV (B V norm f) <= c"; 
   3.198    proof (rule ub_ge_sup);
   3.199      from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
   3.200 -      by (asm_simp add: is_function_norm_def function_norm_def); 
   3.201 +      by (simp! add: is_function_norm_def function_norm_def); 
   3.202      show "isUb UNIV (B V norm f) c";  
   3.203      proof (intro isUbI setleI ballI);
   3.204        fix y; assume "y: B V norm f";
   3.205 -      show le: "y <= c";
   3.206 -      proof (unfold B_def, elim CollectD [elimify] disjE bexE);
   3.207 +      thus le: "y <= c";
   3.208 +      proof (-, unfold B_def, elim CollectE disjE bexE);
   3.209  	fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
   3.210  	assume x: "x : V";
   3.211 -	have lt: "0r < norm x";
   3.212 -	  by (asm_simp add: normed_vs_norm_gt_zero);
   3.213 -	hence "0r ~= norm x"; by (asm_simp add: order_less_imp_not_eq);
   3.214 -	hence neq: "norm x ~= 0r"; by (rule not_sym);
   3.215 -
   3.216 +        have lt: "0r < norm x";  by (simp! add: normed_vs_norm_gt_zero);
   3.217 +          
   3.218 +        have neq: "norm x ~= 0r"; 
   3.219 +        proof (rule not_sym);
   3.220 +          from lt; show "0r ~= norm x";
   3.221 +          by (simp! add: order_less_imp_not_eq);
   3.222 +        qed;
   3.223 +            
   3.224  	from lt; have "0r < rinv (norm x)";
   3.225 -	  by (asm_simp add: real_rinv_gt_zero);
   3.226 +	  by (simp! add: real_rinv_gt_zero);
   3.227  	then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le);
   3.228  
   3.229  	from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
   3.230 @@ -211,7 +229,7 @@
   3.231  	finally; show ?thesis; .;
   3.232        next;
   3.233          assume "y = 0r";
   3.234 -        show "y <= c"; by force;
   3.235 +        show "y <= c"; by (force!);
   3.236        qed;
   3.237      qed force;
   3.238    qed;
     4.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Sep 21 17:30:55 1999 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Sep 21 17:31:20 1999 +0200
     4.3 @@ -1,3 +1,7 @@
     4.4 +(*  Title:      HOL/Real/HahnBanach/FunctionOrder.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Gertrud Bauer, TU Munich
     4.7 +*)
     4.8  
     4.9  theory FunctionOrder = Subspace + Linearform:;
    4.10  
    4.11 @@ -18,14 +22,30 @@
    4.12    funct :: "'a graph => ('a => real)"
    4.13    "funct g == %x. (@ y. (x, y):g)";
    4.14  
    4.15 -lemma graph_I: "x:F ==> (x, f x) : graph F f";
    4.16 +lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
    4.17    by (unfold graph_def, intro CollectI exI) force;
    4.18  
    4.19 -lemma graphD1: "(x, y): graph F f ==> x:F";
    4.20 -  by (unfold graph_def, elim CollectD [elimify] exE) force;
    4.21 +lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)";
    4.22 +  by (unfold graph_def, force);
    4.23 +
    4.24 +lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F";
    4.25 +  by (unfold graph_def, elim CollectE exE) force;
    4.26 +
    4.27 +lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
    4.28 +  by (unfold graph_def, elim CollectE exE) force; 
    4.29  
    4.30 -lemma graph_domain_funct: "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
    4.31 -proof ( unfold domain_def, unfold funct_def, unfold graph_def, auto);
    4.32 +lemma graph_extD1 [intro!!]: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
    4.33 +  by (unfold graph_def, force);
    4.34 +
    4.35 +lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'";
    4.36 +  by (unfold graph_def, force);
    4.37 +
    4.38 +lemma graph_extI: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
    4.39 +  by (unfold graph_def, force);
    4.40 +
    4.41 +lemma graph_domain_funct: 
    4.42 +  "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
    4.43 +proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
    4.44    fix a b; assume "(a, b) : g";
    4.45    show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
    4.46    show "EX y. (a, y) : g"; ..;
    4.47 @@ -36,22 +56,6 @@
    4.48    qed;
    4.49  qed;
    4.50  
    4.51 -lemma graph_lemma1: "x:F ==> EX t: (graph F f). t = (x, f x)";
    4.52 -  by (unfold graph_def, force);
    4.53 -
    4.54 -lemma graph_lemma2: "(x, y): graph H h ==> y = h x";
    4.55 -  by (unfold graph_def, elim CollectD [elimify] exE) force; 
    4.56 -
    4.57 -lemma graph_lemma3: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
    4.58 -  by (unfold graph_def, force);
    4.59 -
    4.60 -lemma graph_lemma4: "[| graph H h <= graph H' h' |] ==> H <= H'";
    4.61 -  by (unfold graph_def, force);
    4.62 -
    4.63 -lemma graph_lemma5: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
    4.64 -  by (unfold graph_def, force);
    4.65 -
    4.66 -
    4.67  constdefs
    4.68    norm_prev_extensions :: 
    4.69     "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
    4.70 @@ -71,7 +75,7 @@
    4.71                                                & (ALL x:H. h x <= p x))";
    4.72   by (unfold norm_prev_extensions_def) force;
    4.73  
    4.74 -lemma norm_prev_extension_I2 [intro]:  
    4.75 +lemma norm_prev_extensionI2 [intro]:  
    4.76     "[| is_linearform H h;    
    4.77         is_subspace H E;
    4.78         is_subspace F H;
    4.79 @@ -80,7 +84,7 @@
    4.80     ==> (graph H h : norm_prev_extensions E p F f)";
    4.81   by (unfold norm_prev_extensions_def) force;
    4.82  
    4.83 -lemma norm_prev_extension_I [intro]:  
    4.84 +lemma norm_prev_extensionI [intro]:  
    4.85     "(EX H h. graph H h = g 
    4.86               & is_linearform H h    
    4.87               & is_subspace H E
     5.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Sep 21 17:30:55 1999 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Sep 21 17:31:20 1999 +0200
     5.3 @@ -1,10 +1,13 @@
     5.4 +(*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Gertrud Bauer, TU Munich
     5.7 +*)
     5.8  
     5.9  theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
    5.10  
    5.11  
    5.12  theorems [elim!!] = psubsetI;
    5.13  
    5.14 -
    5.15  theorem hahnbanach: 
    5.16    "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
    5.17        ALL x:F. f x <= p x |]
    5.18 @@ -14,12 +17,15 @@
    5.19  proof -;
    5.20    assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
    5.21      and "ALL x:F. f x <= p x";
    5.22 -  def M_def: M == "norm_prev_extensions E p F f";
    5.23 +  def M == "norm_prev_extensions E p F f";
    5.24   
    5.25    have aM: "graph F f : norm_prev_extensions E p F f";
    5.26 -  proof (rule norm_prev_extension_I2);
    5.27 -    show "is_subspace F F"; by (rule subspace_refl, rule subspace_vs);
    5.28 -  qed blast+;
    5.29 +  proof (rule norm_prev_extensionI2);
    5.30 +    show "is_subspace F F"; 
    5.31 +    proof;
    5.32 +      show "is_vectorspace F"; ..;
    5.33 +    qed;
    5.34 +  qed (blast!)+;
    5.35  
    5.36  
    5.37    sect {* Part I a of the proof of the Hahn-Banach Theorem, 
    5.38 @@ -31,7 +37,7 @@
    5.39      fix c; assume "c:chain M"; assume "EX x. x:c";
    5.40      show "(Union c) : M"; 
    5.41  
    5.42 -    proof (unfold M_def, rule norm_prev_extension_I);
    5.43 +    proof (unfold M_def, rule norm_prev_extensionI);
    5.44        show "EX (H::'a set) h::'a => real. graph H h = Union c
    5.45                & is_linearform H h 
    5.46                & is_subspace H E 
    5.47 @@ -47,24 +53,24 @@
    5.48  	  proof (intro conjI);
    5.49   	    show a: "graph ?H ?h = Union c"; 
    5.50              proof (rule graph_domain_funct);
    5.51 -              fix x y z; assume "EX x. x : c" "(x, y) : Union c" "(x, z) : Union c";
    5.52 +              fix x y z; assume "(x, y) : Union c" "(x, z) : Union c";
    5.53                show "z = y"; by (rule sup_uniq);
    5.54              qed;
    5.55              
    5.56  	    show "is_linearform ?H ?h";
    5.57 -              by (asm_simp add: sup_lf a);       
    5.58 +              by (simp! add: sup_lf a);       
    5.59  
    5.60  	    show "is_subspace ?H E";
    5.61 -              by (rule sup_subE, rule a) asm_simp+;
    5.62 +              by (rule sup_subE, rule a) (simp!)+;
    5.63  
    5.64  	    show "is_subspace F ?H";
    5.65 -              by (rule sup_supF, rule a) asm_simp+;
    5.66 +              by (rule sup_supF, rule a) (simp!)+;
    5.67  
    5.68  	    show "graph F f <= graph ?H ?h";       
    5.69 -               by (rule sup_ext, rule a) asm_simp+;
    5.70 +               by (rule sup_ext, rule a) (simp!)+;
    5.71  
    5.72  	    show "ALL x::'a:?H. ?h x <= p x"; 
    5.73 -               by (rule sup_norm_prev, rule a) asm_simp+;
    5.74 +               by (rule sup_norm_prev, rule a) (simp!)+;
    5.75  	  qed;
    5.76  	qed;
    5.77        qed;
    5.78 @@ -73,7 +79,7 @@
    5.79        
    5.80    
    5.81    with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
    5.82 -    by (asm_simp add: Zorn's_Lemma);
    5.83 +    by (simp! add: Zorn's_Lemma);
    5.84    thus ?thesis;
    5.85    proof;
    5.86      fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x";
    5.87 @@ -84,7 +90,7 @@
    5.88                           & is_subspace F H
    5.89                           & (graph F f <= graph H h)
    5.90                           & (ALL x:H. h x <= p x) "; 
    5.91 -      by (asm_simp add: norm_prev_extension_D);
    5.92 +      by (simp! add: norm_prev_extension_D);
    5.93      thus ?thesis;
    5.94      proof (elim exE conjE);
    5.95        fix H h; assume "graph H h = g" "is_linearform (H::'a set) h"
    5.96 @@ -92,8 +98,8 @@
    5.97          "(graph F f <= graph H h)"; assume h_bound: "ALL x:H. h x <= p x";
    5.98        show ?thesis; 
    5.99        proof;
   5.100 -        have h: "is_vectorspace H"; by (rule subspace_vs);
   5.101 -        have f: "is_vectorspace F"; by (rule subspace_vs);
   5.102 +        have h: "is_vectorspace H"; ..;
   5.103 +        have f: "is_vectorspace F"; ..;
   5.104  
   5.105  
   5.106          sect {* Part I a of the proof of the Hahn-Banach Theorem,
   5.107 @@ -108,7 +114,7 @@
   5.108              proof -;
   5.109  	      have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
   5.110  	      proof-;
   5.111 -                from subspace_subset [of H E]; have "H <= E"; ..;
   5.112 +                have "H <= E"; ..;
   5.113                  hence "H < E"; ..;
   5.114                  hence "EX x0:E. x0~:H"; by (rule set_less_imp_diff_not_empty);
   5.115                  thus ?thesis;
   5.116 @@ -117,11 +123,12 @@
   5.117                    have x0:  "x0 ~= <0>";
   5.118                    proof (rule classical);
   5.119                      presume "x0 = <0>";
   5.120 -                    have "x0 : H"; by (asm_simp add: zero_in_vs [OF h]);
   5.121 -                    thus "x0 ~= <0>"; by contradiction;
   5.122 +                    also; have "<0> : H"; ..;
   5.123 +                    finally; have "x0 : H"; .;
   5.124 +                    thus ?thesis; by contradiction;
   5.125                    qed force;
   5.126  
   5.127 -       		  def H0_def: H0 == "vectorspace_sum H (lin x0)";
   5.128 +       		  def H0 == "vectorspace_sum H (lin x0)";
   5.129                    have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M"; 
   5.130                    proof -;
   5.131                      from h; have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi) 
   5.132 @@ -133,10 +140,10 @@
   5.133                          show "!! a b c d::real. d - b <= c + a ==> - a - b <= c - d";
   5.134                          proof -; (* arith *)
   5.135  			  fix a b c d; assume "d - b <= c + (a::real)";
   5.136 -                          have "- a - b = d - b + (- d - a)"; by asm_simp;
   5.137 +                          have "- a - b = d - b + (- d - a)"; by (simp!);
   5.138                            also; have "... <= c + a + (- d - a)";
   5.139                              by (rule real_add_le_mono1);
   5.140 -                          also; have "... = c - d"; by asm_simp;
   5.141 +                          also; have "... = c - d"; by (simp!);
   5.142                            finally; show "- a - b <= c - d"; .;
   5.143                          qed;
   5.144                          show "h v - h u <= p (v [+] x0) + p (u [+] x0)"; 
   5.145 @@ -145,17 +152,17 @@
   5.146                              by  (rule linearform_diff_linear [RS sym]);
   5.147                            also; have "... <= p (v [-] u)";
   5.148  			  proof -;  
   5.149 -			    from h; have "v [-] u : H"; by asm_simp; 
   5.150 +			    from h; have "v [-] u : H"; by (simp!); 
   5.151                              with h_bound; show ?thesis; ..;
   5.152  			  qed;
   5.153                            also; have "v [-] u  = x0 [+] [-] x0 [+] v [+] [-] u"; 
   5.154 -                            by (asm_simp add: vs_add_minus_eq_diff);
   5.155 +                            by (simp! add: vs_add_minus_eq_diff);
   5.156                            also; have "... = v [+] x0 [+] [-] (u [+] x0)"; 
   5.157 -                            by asm_simp;
   5.158 +                            by (simp!);
   5.159                            also; have "... = (v [+] x0) [-] (u [+] x0)";  
   5.160 -                            by (asm_simp only: vs_add_minus_eq_diff);
   5.161 +                            by (simp! only: vs_add_minus_eq_diff);
   5.162                            also; have "p ... <= p (v [+] x0) + p (u [+] x0)"; 
   5.163 -                            by (rule quasinorm_diff_triangle_ineq) asm_simp+;
   5.164 +                            by (rule quasinorm_diff_triangle_ineq) (simp!)+;
   5.165                            finally; show ?thesis; .;
   5.166                          qed;
   5.167                        qed;
   5.168 @@ -165,17 +172,17 @@
   5.169                      proof (elim exE, intro exI conjI);
   5.170                        fix xi; assume a: "(ALL y:H. - p (y [+] x0) - h y <= xi) &
   5.171                                           (ALL y:H. xi <= p (y [+] x0) - h y)";
   5.172 -                      def h0_def: h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
   5.173 +                      def h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
   5.174                                              in (h y) + a * xi";
   5.175  
   5.176  	              have "graph H h <= graph H0 h0"; 
   5.177 -                      proof% (rule graph_lemma5);
   5.178 +                      proof (rule graph_extI);
   5.179                          fix t; assume "t:H"; 
   5.180                          show "h t = h0 t";
   5.181                          proof -;
   5.182                            have "(@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
   5.183 -                            by (rule lemma1, rule x0); 
   5.184 -                          thus ?thesis; by (asm_simp add: Let_def);
   5.185 +                            by (rule decomp1, rule x0); 
   5.186 +                          thus ?thesis; by (simp! add: Let_def);
   5.187                          qed;
   5.188                        next;
   5.189                          show "H <= H0";
   5.190 @@ -187,82 +194,85 @@
   5.191  			  qed;
   5.192  			qed;
   5.193  		      qed;
   5.194 -                      thus "g <= graph H0 h0"; by asm_simp;
   5.195 +                      thus "g <= graph H0 h0"; by (simp!);
   5.196  
   5.197                        have "graph H h ~= graph H0 h0";
   5.198                        proof;
   5.199                          assume "graph H h = graph H0 h0";
   5.200                          have x1: "(x0, h0 x0) : graph H0 h0";
   5.201 -                        proof (rule graph_I);
   5.202 +                        proof (rule graphI);
   5.203                            show "x0:H0";
   5.204 -                          proof (unfold H0_def, rule vs_sum_I);
   5.205 -                            from h; show "<0> : H"; by (rule zero_in_vs);
   5.206 +                          proof (unfold H0_def, rule vs_sumI);
   5.207 +                            from h; show "<0> : H"; ..;
   5.208                              show "x0 : lin x0"; by (rule x_lin_x);
   5.209 -                            show "x0 = <0> [+] x0"; by (rule vs_add_zero_left [RS sym]);
   5.210 +                            show "x0 = <0> [+] x0"; by (simp!);
   5.211                            qed;
   5.212                          qed;
   5.213                          have "(x0, h0 x0) ~: graph H h";
   5.214                          proof;
   5.215                            assume "(x0, h0 x0) : graph H h";
   5.216 -                          have "x0:H"; by (rule graphD1);
   5.217 +                          have "x0:H"; ..;
   5.218                            thus "False"; by contradiction;
   5.219                          qed;
   5.220 -                        hence "(x0, h0 x0) ~: graph H0 h0"; by asm_simp;
   5.221 +                        hence "(x0, h0 x0) ~: graph H0 h0"; by (simp!);
   5.222                          with x1; show "False"; by contradiction;
   5.223                        qed;
   5.224 -                      thus "g ~= graph H0 h0"; by asm_simp;
   5.225 +                      thus "g ~= graph H0 h0"; by (simp!);
   5.226  
   5.227                        have "graph H0 h0 : norm_prev_extensions E p F f";
   5.228 -                      proof (rule norm_prev_extension_I2);
   5.229 +                      proof (rule norm_prev_extensionI2);
   5.230  
   5.231                          show "is_linearform H0 h0";
   5.232 -                          by (rule h0_lf, rule x0) asm_simp+;
   5.233 +                          by (rule h0_lf, rule x0) (simp!)+;
   5.234  
   5.235                          show "is_subspace H0 E";
   5.236                          proof -;
   5.237 -                        have "is_subspace (vectorspace_sum H (lin x0)) E";
   5.238 +                        have "is_subspace (vectorspace_sum H (lin x0)) E"; 
   5.239  			  by (rule vs_sum_subspace, rule lin_subspace);
   5.240 -                          thus ?thesis; by asm_simp;
   5.241 +                          thus ?thesis; by (simp!);
   5.242                          qed;
   5.243  
   5.244                          show f_h0: "is_subspace F H0";
   5.245                          proof (rule subspace_trans [of F H H0]);
   5.246                            from h lin_vs; have "is_subspace H (vectorspace_sum H (lin x0))";
   5.247                              by (rule subspace_vs_sum1);
   5.248 -                          thus "is_subspace H H0"; by asm_simp;
   5.249 +                          thus "is_subspace H H0"; by (simp!);
   5.250                          qed;
   5.251  
   5.252                          show "graph F f <= graph H0 h0";
   5.253 -                        proof(rule graph_lemma5);
   5.254 +                        proof(rule graph_extI);
   5.255                            fix x; assume "x:F";
   5.256                            show "f x = h0 x";
   5.257                            proof -;
   5.258                              have "x:H"; 
   5.259                              proof (rule subsetD);
   5.260 -                              show "F <= H"; by (rule subspace_subset);
   5.261 +                              show "F <= H"; ..;
   5.262                              qed;
   5.263                              have eq: "(@ (y, a). x = y [+] a [*] x0 & y : H) = (x, 0r)";
   5.264 -                              by (rule lemma1, rule x0) asm_simp+;
   5.265 +                              by (rule decomp1, rule x0) (simp!)+;
   5.266   
   5.267                              have "h0 x = (let (y,a) = @ (y,a). x = y [+] a [*] x0 & y : H
   5.268                                            in h y + a * xi)"; 
   5.269 -                              by asm_simp;
   5.270 +                              by (simp!);
   5.271                              also; from eq; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
   5.272                                by simp;
   5.273                              also; have " ... = h x + 0r * xi";
   5.274 -                              by (asm_simp add: Let_def);
   5.275 -                            also; have "... = h x"; by asm_simp;
   5.276 -                            also; have "... = f x"; by (rule graph_lemma3 [RS sym, of F f H h]);
   5.277 +                              by (simp! add: Let_def);
   5.278 +                            also; have "... = h x"; by (simp!);
   5.279 +                            also; have "... = f x"; 
   5.280 +                            proof (rule sym);
   5.281 +                              show "f x = h x"; ..;
   5.282 +                            qed;
   5.283                              finally; show ?thesis; by (rule sym);
   5.284                            qed;
   5.285                          next;
   5.286 -                          from f_h0; show "F <= H0"; by (rule subspace_subset);
   5.287 +                          from f_h0; show "F <= H0"; ..;
   5.288                          qed;
   5.289  
   5.290                          show "ALL x:H0. h0 x <= p x";
   5.291 -                          by (rule h0_norm_prev, rule x0) (assumption | asm_simp)+;
   5.292 +                          by (rule h0_norm_prev, rule x0) (assumption | (simp!))+;
   5.293                        qed;
   5.294 -                      thus "graph H0 h0 : M"; by asm_simp;
   5.295 +                      thus "graph H0 h0 : M"; by (simp!);
   5.296                      qed;
   5.297                    qed;
   5.298                    thus ?thesis; ..;
   5.299 @@ -279,9 +289,12 @@
   5.300  
   5.301          show "is_linearform E h & (ALL x:F. h x = f x) & (ALL x:E. h x <= p x)";
   5.302          proof (intro conjI); 
   5.303 -          from eq; show "is_linearform E h"; by asm_simp;
   5.304 -          show "ALL x:F. h x = f x"; by (intro ballI, rule graph_lemma3 [RS sym]); 
   5.305 -          from eq; show "ALL x:E. h x <= p x"; by force;
   5.306 +          from eq; show "is_linearform E h"; by (simp!);
   5.307 +          show "ALL x:F. h x = f x"; 
   5.308 +          proof (intro ballI, rule sym);
   5.309 +            fix x; assume "x:F"; show "f x = h x "; ..;
   5.310 +          qed;
   5.311 +          from eq; show "ALL x:E. h x <= p x"; by (force!);
   5.312          qed;
   5.313        qed;  
   5.314      qed; 
   5.315 @@ -302,17 +315,16 @@
   5.316  
   5.317    assume e: "is_vectorspace E"; 
   5.318    assume "is_subspace F E" "is_quasinorm E p" "is_linearform F f" "ALL x:F. rabs (f x) <= p x";
   5.319 -  have "ALL x:F. f x <= p x";
   5.320 -    by (asm_simp only: rabs_ineq);
   5.321 +  have "ALL x:F. f x <= p x"; by (rule rabs_ineq [RS iffD1]);
   5.322    hence  "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)";
   5.323 -    by (asm_simp only: hahnbanach);
   5.324 +    by (simp! only: hahnbanach);
   5.325    thus ?thesis;
   5.326    proof (elim exE conjE);
   5.327      fix g; assume "is_linearform E g" "ALL x:F. g x = f x" "ALL x:E. g x <= p x";
   5.328      show ?thesis;
   5.329      proof (intro exI conjI)+;
   5.330 -      from e; show "ALL x:E. rabs (g x) <= p x";
   5.331 -        by (asm_simp add: rabs_ineq [OF subspace_refl]);
   5.332 +      from e; show "ALL x:E. rabs (g x) <= p x"; 
   5.333 +        by (simp! add: rabs_ineq [OF subspace_refl]);
   5.334      qed;
   5.335    qed;
   5.336  qed;
   5.337 @@ -334,10 +346,10 @@
   5.338    assume a: "is_normed_vectorspace E norm";
   5.339    assume b: "is_subspace F E" "is_linearform F f";
   5.340    assume c: "is_continous F norm f";
   5.341 -  hence e: "is_vectorspace E"; by (asm_simp add: normed_vs_vs);
   5.342 +  have e: "is_vectorspace E"; ..;
   5.343    from _ e;
   5.344 -  have f: "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
   5.345 -  def p_def: p == "%x::'a. (function_norm F norm f) * norm x";
   5.346 +  have f: "is_normed_vectorspace F norm"; ..;
   5.347 +  def p == "%x::'a. (function_norm F norm f) * norm x";
   5.348    
   5.349    let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. rabs (g x) <= p x)";
   5.350  
   5.351 @@ -347,53 +359,52 @@
   5.352  
   5.353      show "0r <= p x";
   5.354      proof (unfold p_def, rule real_le_mult_order);
   5.355 -      from c f; show "0r <= function_norm F norm f";
   5.356 -        by (rule fnorm_ge_zero);
   5.357 -      from a; show "0r <= norm x"; by (rule normed_vs_norm_ge_zero); 
   5.358 +      from _ f; show "0r <= function_norm F norm f"; ..;
   5.359 +      show "0r <= norm x"; ..;
   5.360      qed;
   5.361  
   5.362      show "p (a [*] x) = (rabs a) * (p x)";
   5.363      proof -; 
   5.364 -      have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by asm_simp;
   5.365 -      also; from a; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
   5.366 +      have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by (simp!);
   5.367 +      also; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
   5.368        also; have "(function_norm F norm f) * ... = rabs a * ((function_norm F norm f) * norm x)";
   5.369 -        by (asm_simp only: real_mult_left_commute);
   5.370 -      also; have "... = (rabs a) * (p x)"; by asm_simp;
   5.371 +        by (simp! only: real_mult_left_commute);
   5.372 +      also; have "... = (rabs a) * (p x)"; by (simp!);
   5.373        finally; show ?thesis; .;
   5.374      qed;
   5.375  
   5.376      show "p (x [+] y) <= p x + p y";
   5.377      proof -;
   5.378 -      have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by asm_simp;
   5.379 +      have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by (simp!);
   5.380        also; have "... <=  (function_norm F norm f) * (norm x + norm y)";
   5.381        proof (rule real_mult_le_le_mono1);
   5.382 -        from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
   5.383 -        show "norm (x [+] y) <= norm x + norm y"; by (rule normed_vs_norm_triangle_ineq);
   5.384 +        from _ f; show "0r <= function_norm F norm f"; ..;
   5.385 +        show "norm (x [+] y) <= norm x + norm y"; ..;
   5.386        qed;
   5.387        also; have "... = (function_norm F norm f) * (norm x) + (function_norm F norm f) * (norm y)";
   5.388 -        by (asm_simp only: real_add_mult_distrib2);
   5.389 -      finally; show ?thesis; by asm_simp;
   5.390 +        by (simp! only: real_add_mult_distrib2);
   5.391 +      finally; show ?thesis; by (simp!);
   5.392      qed;
   5.393    qed;
   5.394   
   5.395    have "ALL x:F. rabs (f x) <= p x";
   5.396    proof;
   5.397      fix x; assume "x:F";
   5.398 -    from f; show "rabs (f x) <= p x"; by (asm_simp add: norm_fx_le_norm_f_norm_x);
   5.399 +     from f; show "rabs (f x) <= p x"; by (simp! add: norm_fx_le_norm_f_norm_x);
   5.400    qed;
   5.401  
   5.402    with e b q; have "EX g. ?P' g";
   5.403 -    by (asm_simp add: rabs_hahnbanach);
   5.404 +    by (simp! add: rabs_hahnbanach);
   5.405  
   5.406    thus "?thesis";
   5.407    proof (elim exE conjE, intro exI conjI);
   5.408      fix g;
   5.409      assume "is_linearform E g" and a: "ALL x:F. g x = f x" and "ALL x:E. rabs (g x) <= p x";
   5.410      show ce: "is_continous E norm g";
   5.411 -    proof (rule lipschitz_continous_I);
   5.412 +    proof (rule lipschitz_continousI);
   5.413        fix x; assume "x:E";
   5.414        show "rabs (g x) <= function_norm F norm f * norm x";
   5.415 -        by (rule bspec [of _ _ x], asm_simp);
   5.416 +        by (rule bspec [of _ _ x], (simp!));
   5.417      qed;
   5.418      show "function_norm E norm g = function_norm F norm f";
   5.419      proof (rule order_antisym);
   5.420 @@ -403,28 +414,28 @@
   5.421          proof;
   5.422            fix x; assume "x:E"; 
   5.423            show "rabs (g x) <= function_norm F norm f * norm x";
   5.424 -            by (rule bspec [of _ _ x], asm_simp);
   5.425 +            by (rule bspec [of _ _ x], (simp!));
   5.426          qed;
   5.427 -        from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
   5.428 +        from c f; show "0r <= function_norm F norm f"; ..;
   5.429        qed;
   5.430        show "function_norm F norm f <= function_norm E norm g"; 
   5.431        proof (rule fnorm_le_ub);
   5.432          show "ALL x:F. rabs (f x) <=  function_norm E norm g * norm x";
   5.433          proof;
   5.434 -          fix x; assume "x:F"; 
   5.435 -          from a; have "f x = g x"; by (rule bspec [of _ _ x, RS sym]);
   5.436 +          fix x; assume "x : F"; 
   5.437 +          from a; have "g x = f x"; ..;
   5.438            hence "rabs (f x) = rabs (g x)"; by simp;
   5.439            also; from _ _ ce; have "... <= function_norm E norm g * norm x"; 
   5.440            proof (rule norm_fx_le_norm_f_norm_x);
   5.441 -            show "x:E";
   5.442 +            show "x : E";
   5.443              proof (rule subsetD); 
   5.444 -              show "F<=E"; by (rule subspace_subset);
   5.445 +              show "F <= E"; ..;
   5.446              qed;
   5.447            qed;
   5.448            finally; show "rabs (f x) <= function_norm E norm g * norm x"; .;
   5.449          qed;
   5.450 -        from _ e; show "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
   5.451 -        from ce; show "0r <= function_norm E norm g"; by (rule fnorm_ge_zero);
   5.452 +        from _ e; show "is_normed_vectorspace F norm"; ..;
   5.453 +        from ce; show "0r <= function_norm E norm g"; ..;
   5.454        qed;
   5.455      qed;
   5.456    qed;
   5.457 @@ -432,3 +443,4 @@
   5.458  
   5.459  
   5.460  end;
   5.461 +
     6.1 --- a/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy	Tue Sep 21 17:30:55 1999 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy	Tue Sep 21 17:31:20 1999 +0200
     6.3 @@ -1,8 +1,12 @@
     6.4 +(*  Title:      HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Gertrud Bauer, TU Munich
     6.7 +*)
     6.8  
     6.9 -theory HahnBanach_h0_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
    6.10 +theory HahnBanach_h0_lemmas = FunctionNorm:;
    6.11  
    6.12  
    6.13 -theorems [intro!!] = zero_in_vs isLub_isUb;
    6.14 +theorems [intro!!] = isLub_isUb;
    6.15  
    6.16  lemma ex_xi: "[| is_vectorspace F;  (!! u v. [| u:F; v:F |] ==> a u <= b v )|]
    6.17         ==> EX xi::real. (ALL y:F. (a::'a => real) y <= xi) & (ALL y:F. xi <= b y)"; 
    6.18 @@ -11,7 +15,7 @@
    6.19    assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
    6.20    have "EX t. isLub UNIV {s::real . EX u:F. s = a u} t";  
    6.21    proof (rule reals_complete);
    6.22 -    have "a <0> : {s. EX u:F. s = a u}"; by force;
    6.23 +    have "a <0> : {s. EX u:F. s = a u}"; by (force!);
    6.24      thus "EX X. X : {s. EX u:F. s = a u}"; ..;
    6.25  
    6.26      show "EX Y. isUb UNIV {s. EX u:F. s = a u} Y"; 
    6.27 @@ -21,7 +25,7 @@
    6.28          fix y; assume "y : {s. EX u:F. s = a u}"; 
    6.29          show "y <= b <0>"; 
    6.30          proof -;
    6.31 -          have "EX u:F. y = a u"; by fast;
    6.32 +          have "EX u:F. y = a u"; by (fast!);
    6.33            thus ?thesis;
    6.34            proof;
    6.35              fix u; assume "u:F"; 
    6.36 @@ -45,7 +49,7 @@
    6.37        show "a y <= t";    
    6.38        proof (rule isUbD);  
    6.39          show"isUb UNIV {s. EX u:F. s = a u} t"; ..;
    6.40 -      qed fast;
    6.41 +      qed (fast!);
    6.42      next;
    6.43        fix y; assume "y:F";
    6.44        show "t <= b y";  
    6.45 @@ -56,7 +60,7 @@
    6.46            assume "au : {s. EX u:F. s = a u} ";
    6.47            show "au <= b y";
    6.48            proof -; 
    6.49 -            have "EX u:F. au = a u"; by fast;
    6.50 +            have "EX u:F. au = a u"; by (fast!);
    6.51              thus "au <= b y";
    6.52              proof;
    6.53                fix u; assume "u:F";
    6.54 @@ -73,8 +77,6 @@
    6.55  qed;
    6.56  
    6.57  
    6.58 -theorems [dest!!] = vs_sumD linD;
    6.59 -
    6.60  lemma h0_lf: 
    6.61    "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
    6.62        H0 = vectorspace_sum H (lin x0); is_subspace H E; is_linearform H h; x0 ~: H; 
    6.63 @@ -87,7 +89,7 @@
    6.64      and [simp]: "x0 : E" "is_vectorspace E";
    6.65  
    6.66    have h0: "is_vectorspace H0"; 
    6.67 -  proof (asm_simp, rule vs_sum_vs);
    6.68 +  proof ((simp!), rule vs_sum_vs);
    6.69      show "is_subspace (lin x0) E"; by (rule lin_subspace); 
    6.70    qed simp+; 
    6.71  
    6.72 @@ -98,11 +100,11 @@
    6.73        by (rule vs_add_closed, rule h0);
    6.74    
    6.75      have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0  & y1 : H)"; 
    6.76 -      by (asm_simp add: vectorspace_sum_def lin_def) blast;
    6.77 +      by (simp! add: vectorspace_sum_def lin_def) blast;
    6.78      have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)"; 
    6.79 -      by (asm_simp add: vectorspace_sum_def lin_def) blast;
    6.80 +      by (simp! add: vectorspace_sum_def lin_def) blast;
    6.81      from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0  & y : H)";    
    6.82 -      by (asm_simp add: vectorspace_sum_def lin_def) force;
    6.83 +      by (simp! add: vectorspace_sum_def lin_def) force;
    6.84      from ex_x1 ex_x2 ex_x1x2;
    6.85      show "h0 (x1 [+] x2) = h0 x1 + h0 x2";
    6.86      proof (elim exE conjE);
    6.87 @@ -112,33 +114,33 @@
    6.88               "x1 [+] x2 = y  [+] a  [*] x0" "y  : H"; 
    6.89  
    6.90        have ya: "y1 [+] y2 = y & a1 + a2 = a"; 
    6.91 -      proof (rule lemma4); 
    6.92 +      proof (rule decomp4); 
    6.93          show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0"; 
    6.94          proof -;
    6.95 -          have "y [+] a [*] x0 = x1 [+] x2"; by asm_simp; 
    6.96 -          also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by asm_simp; 
    6.97 -          also; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
    6.98 -            by asm_simp_tac;
    6.99 +          have "y [+] a [*] x0 = x1 [+] x2"; by (simp!); 
   6.100 +          also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by (simp!); 
   6.101 +          also; from prems; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
   6.102 +	    by asm_simp_tac;   (* FIXME !?? *)
   6.103           also; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0"; 
   6.104 -            by (asm_simp add: vs_add_mult_distrib2[of E]);
   6.105 +            by (simp! add: vs_add_mult_distrib2[of E]);
   6.106            finally; show ?thesis; by (rule sym);
   6.107          qed;
   6.108 -        show "y1 [+] y2 : H"; by (rule subspace_add_closed);
   6.109 +        show "y1 [+] y2 : H"; ..;
   6.110        qed;
   6.111        have y: "y1 [+] y2 = y"; by (rule conjunct1 [OF ya]);
   6.112        have a: "a1 + a2 = a";  by (rule conjunct2 [OF ya]);
   6.113  
   6.114        have "h0 (x1 [+] x2) = h y + a * xi";
   6.115 -	by (rule lemma3);
   6.116 -      also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (asm_simp add: y a);
   6.117 +	by (rule decomp3);
   6.118 +      also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (simp! add: y a);
   6.119        also; have  "... = h y1 + h y2 + a1 * xi + a2 * xi"; 
   6.120 -	by (asm_simp add: linearform_add_linear [of H] real_add_mult_distrib);
   6.121 -      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by asm_simp;
   6.122 +	by (simp! add: linearform_add_linear [of H] real_add_mult_distrib);
   6.123 +      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by (simp!);
   6.124        also; have "... = h0 x1 + h0 x2"; 
   6.125        proof -; 
   6.126 -        have x1: "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
   6.127 -        have x2: "h0 x2 = h y2 + a2 * xi"; by (rule lemma3);
   6.128 -        from x1 x2; show ?thesis; by asm_simp;
   6.129 +        have x1: "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
   6.130 +        have x2: "h0 x2 = h y2 + a2 * xi"; by (rule decomp3);
   6.131 +        from x1 x2; show ?thesis; by (simp!);
   6.132        qed;
   6.133        finally; show ?thesis; .;
   6.134      qed;
   6.135 @@ -149,9 +151,9 @@
   6.136      have ax1: "c [*] x1 : H0";
   6.137        by (rule vs_mult_closed, rule h0);
   6.138      have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
   6.139 -      by (asm_simp add: vectorspace_sum_def lin_def, fast);
   6.140 +      by (simp! add: vectorspace_sum_def lin_def, fast);
   6.141      have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)"; 
   6.142 -      by (asm_simp add: vectorspace_sum_def lin_def, fast);
   6.143 +      by (simp! add: vectorspace_sum_def lin_def, fast);
   6.144      note ex_ax1 = ex_x [of "c [*] x1", OF ax1];
   6.145      from ex_x1 ex_ax1; show "h0 (c [*] x1) = c * (h0 x1)";  
   6.146      proof (elim exE conjE);
   6.147 @@ -160,34 +162,34 @@
   6.148  	     "c [*] x1 = y  [+] a  [*] x0" "y  : H"; 
   6.149  
   6.150        have ya: "c [*] y1 = y & c * a1 = a"; 
   6.151 -      proof (rule lemma4); 
   6.152 +      proof (rule decomp4); 
   6.153  	show "c [*] y1 [+] (c * a1) [*] x0 = y [+] a [*] x0"; 
   6.154  	proof -; 
   6.155 -          have "y [+] a [*] x0 = c [*] x1"; by asm_simp;
   6.156 -          also; have "... = c [*] (y1 [+] a1 [*] x0)"; by asm_simp;
   6.157 -          also; have "... = c [*] y1 [+] c [*] (a1 [*] x0)"; 
   6.158 -            by (asm_simp_tac add: vs_add_mult_distrib1);
   6.159 -          also; have "... = c [*] y1 [+] (c * a1) [*] x0";
   6.160 -            by (asm_simp_tac);
   6.161 +          have "y [+] a [*] x0 = c [*] x1"; by (simp!);
   6.162 +          also; have "... = c [*] (y1 [+] a1 [*] x0)"; by (simp!);
   6.163 +          also; from prems; have "... = c [*] y1 [+] c [*] (a1 [*] x0)"; 
   6.164 +            by (asm_simp_tac add: vs_add_mult_distrib1);  (* FIXME *)
   6.165 +          also; from prems; have "... = c [*] y1 [+] (c * a1) [*] x0";
   6.166 +            by asm_simp_tac;
   6.167            finally; show ?thesis; by (rule sym);
   6.168          qed;
   6.169 -        show "c [*] y1: H"; by (rule subspace_mult_closed);
   6.170 +        show "c [*] y1: H"; ..;
   6.171        qed;
   6.172        have y: "c [*] y1 = y"; by (rule conjunct1 [OF ya]);
   6.173        have a: "c * a1 = a"; by (rule conjunct2 [OF ya]);
   6.174        
   6.175        have "h0 (c [*] x1) = h y + a * xi"; 
   6.176 -	by (rule lemma3);
   6.177 +	by (rule decomp3);
   6.178        also; have "... = h (c [*] y1) + (c * a1) * xi";
   6.179 -        by (asm_simp add: y a);
   6.180 +        by (simp! add: y a);
   6.181        also; have  "... = c * h y1 + c * a1 * xi"; 
   6.182 -	by (asm_simp add: linearform_mult_linear [of H] real_add_mult_distrib);
   6.183 +	by (simp! add: linearform_mult_linear [of H] real_add_mult_distrib);
   6.184        also; have "... = c * (h y1 + a1 * xi)"; 
   6.185 -	by (asm_simp add: real_add_mult_distrib2 real_mult_assoc);
   6.186 +	by (simp! add: real_add_mult_distrib2 real_mult_assoc);
   6.187        also; have "... = c * (h0 x1)"; 
   6.188        proof -; 
   6.189 -        have "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
   6.190 -        thus ?thesis; by asm_simp;
   6.191 +        have "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
   6.192 +        thus ?thesis; by (simp!);
   6.193        qed;
   6.194        finally; show ?thesis; .;
   6.195      qed;
   6.196 @@ -211,7 +213,7 @@
   6.197    show "h0 x <= p x"; 
   6.198    proof -; 
   6.199      have ex_x: "!! x. x : H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
   6.200 -      by (asm_simp add: vectorspace_sum_def lin_def, fast);
   6.201 +      by (simp! add: vectorspace_sum_def lin_def, fast);
   6.202      have "? y a. (x = y [+] a [*] x0 & y : H)";
   6.203        by (rule ex_x);
   6.204      thus ?thesis;
   6.205 @@ -220,16 +222,16 @@
   6.206        show ?thesis;
   6.207        proof -;
   6.208          have "h0 x = h y + a * xi";
   6.209 -          by (rule lemma3);
   6.210 +          by (rule decomp3);
   6.211          also; have "... <= p (y [+] a [*] x0)";
   6.212 -        proof (rule real_linear [of a "0r", elimify], elim disjE); (* case distinction *)
   6.213 +        proof (rule real_linear [of a "0r", elimify], elim disjE); (*** case distinction ***)
   6.214            assume lz: "a < 0r"; 
   6.215            hence nz: "a ~= 0r"; by force;
   6.216            show ?thesis;
   6.217            proof -;
   6.218              from a1; have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
   6.219              proof (rule bspec); 
   6.220 -              show "(rinv a) [*] y : H"; by (rule subspace_mult_closed);
   6.221 +              show "(rinv a) [*] y : H"; ..;
   6.222              qed;
   6.223              with lz; have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
   6.224                by (rule real_mult_less_le_anti);
   6.225 @@ -241,52 +243,46 @@
   6.226                  by (rule rabs_minus_eqI2); 
   6.227                thus ?thesis; by simp;
   6.228              qed;
   6.229 -            also; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   6.230 -              by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
   6.231 +            also; from prems; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   6.232 +              by (simp!, asm_simp_tac add: quasinorm_mult_distrib);
   6.233              also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
   6.234              proof simp;
   6.235                have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
   6.236 -                by (rule vs_add_mult_distrib1) asm_simp+;
   6.237 +                by (rule vs_add_mult_distrib1) (simp!)+;
   6.238                also; have "... = (a * rinv a) [*] y [+] a [*] x0";
   6.239 -                by asm_simp;
   6.240 +                by (simp!);
   6.241                finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
   6.242                thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
   6.243                  by simp;
   6.244              qed;
   6.245              also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))"; 
   6.246 -              by asm_simp;
   6.247 -            also; from nz; have "... = p (y [+] a [*] x0) - (h y)"; 
   6.248 -            proof asm_simp;
   6.249 -              have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))"; 
   6.250 +              by (simp!);
   6.251 +            also; have "a * (h (rinv a [*] y)) = h y";
   6.252 +	    proof -;
   6.253 +              from prems; have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))"; 
   6.254                  by (asm_simp_tac add: linearform_mult_linear [RS sym]); 
   6.255 -              also; have "... = h y"; 
   6.256 -              proof -;
   6.257 -                from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
   6.258 -                thus ?thesis; by simp;
   6.259 -              qed;
   6.260 -              finally; have "a * (h (rinv a [*] y)) = h y"; .;
   6.261 -              thus "- (a * (h (rinv a [*] y))) = - (h y)"; by simp;
   6.262 +	      also; from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
   6.263 +              finally; show ?thesis; .;
   6.264              qed;
   6.265 -            finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
   6.266 +            finally; have "a * xi <= p (y [+] a [*] x0) - ..."; .;
   6.267              hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
   6.268                by (rule real_add_left_cancel_le [RS iffD2]); (* arith *)
   6.269              thus ?thesis; 
   6.270                by force;
   6.271 -          qed;
   6.272 -
   6.273 +	  qed;
   6.274          next;
   6.275            assume "a = 0r"; show ?thesis; 
   6.276            proof -;
   6.277 -            have "h y + a * xi = h y"; by asm_simp;
   6.278 +            have "h y + a * xi = h y"; by (simp!);
   6.279              also; from a; have "... <= p y"; ..; 
   6.280              also; have "... = p (y [+] a [*] x0)";
   6.281              proof -; 
   6.282 -              have "y = y [+] <0>"; by asm_simp;
   6.283 +              have "y = y [+] <0>"; by (simp!);
   6.284                also; have "... = y [+] a [*] x0"; 
   6.285                proof -; 
   6.286                  have "<0> = 0r [*] x0";
   6.287 -                  by asm_simp;
   6.288 -                also; have "... = a [*] x0"; by asm_simp;
   6.289 +                  by (simp!);
   6.290 +                also; have "... = a [*] x0"; by (simp!);
   6.291                  finally; have "<0> = a [*] x0";.;
   6.292                  thus ?thesis; by simp;
   6.293                qed; 
   6.294 @@ -302,7 +298,7 @@
   6.295            proof -;
   6.296              from a2; have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
   6.297              proof (rule bspec);
   6.298 -              show "rinv a [*] y : H"; by (rule subspace_mult_closed);
   6.299 +              show "rinv a [*] y : H"; ..;
   6.300              qed;
   6.301              with gz; have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
   6.302                by (rule real_mult_less_le_mono);
   6.303 @@ -314,27 +310,27 @@
   6.304                  by (rule rabs_eqI2); 
   6.305                thus ?thesis; by simp;
   6.306              qed;
   6.307 -            also; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   6.308 -              by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
   6.309 +            also; from prems; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
   6.310 +              by (simp, asm_simp_tac add: quasinorm_mult_distrib);
   6.311              also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))"; 
   6.312              proof simp;
   6.313                have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
   6.314 -                by (rule vs_add_mult_distrib1) asm_simp+;
   6.315 +                by (rule vs_add_mult_distrib1) (simp!)+;
   6.316                also; have "... = (a * rinv a) [*] y [+] a [*] x0";
   6.317 -                by asm_simp;
   6.318 +                by (simp!);
   6.319                finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
   6.320                thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
   6.321                  by simp;
   6.322              qed;
   6.323              also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))"; 
   6.324 -              by asm_simp;
   6.325 +              by (simp!);
   6.326              also; from nz; have "... = p (y [+] a [*] x0) - (h y)"; 
   6.327 -            proof asm_simp;
   6.328 +            proof (simp!);
   6.329                have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))"; 
   6.330 -                by (rule linearform_mult_linear [RS sym]) asm_simp+;
   6.331 +                by (rule linearform_mult_linear [RS sym]) (simp!)+;
   6.332                also; have "... = h y"; 
   6.333                proof -;
   6.334 -                from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
   6.335 +                from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
   6.336                  thus ?thesis; by simp;
   6.337                qed;
   6.338                finally; have "a * (h (rinv a [*] y)) = h y"; .;
   6.339 @@ -347,7 +343,7 @@
   6.340                by force;
   6.341            qed;
   6.342          qed;
   6.343 -        also; have "... = p x"; by asm_simp;
   6.344 +        also; have "... = p x"; by (simp!);
   6.345          finally; show ?thesis; .;
   6.346        qed; 
   6.347      qed;
     7.1 --- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Tue Sep 21 17:30:55 1999 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Tue Sep 21 17:31:20 1999 +0200
     7.3 @@ -1,9 +1,10 @@
     7.4 -
     7.5 -theory HahnBanach_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
     7.6 +(*  Title:      HOL/Real/HahnBanach/HahnBanach_lemmas.thy
     7.7 +    ID:         $Id$
     7.8 +    Author:     Gertrud Bauer, TU Munich
     7.9 +*)
    7.10  
    7.11 +theory HahnBanach_lemmas = FunctionNorm + Zorn_Lemma:;
    7.12  
    7.13 -theorems [dest!!] = subsetD;
    7.14 -theorems [intro!!] = subspace_subset; 
    7.15  
    7.16  lemma rabs_ineq: "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] \
    7.17   \ ==>  (ALL x:H. rabs (h x) <= p x)  = ( ALL x:H. h x <= p x)" (concl is "?L = ?R");
    7.18 @@ -17,7 +18,7 @@
    7.19      proof (intro ballI); 
    7.20        fix x; assume "x:H";
    7.21        have "h x <= rabs (h x)"; by (rule rabs_ge_self);
    7.22 -      also; have "rabs (h x) <= p x"; by fast;
    7.23 +      also; have "rabs (h x) <= p x"; by (fast!);
    7.24        finally; show "h x <= p x"; .;
    7.25      qed;
    7.26    next;
    7.27 @@ -34,15 +35,12 @@
    7.28  	  from H; have "- h x = h ([-] x)"; by (rule linearform_neg_linear [RS sym]);
    7.29  	  also; from r; have "... <= p ([-] x)"; 
    7.30  	  proof -; 
    7.31 -	    from H; have "[-] x : H"; by asm_simp;
    7.32 +	    from H; have "[-] x : H"; by (simp!);
    7.33              with r; show ?thesis; ..;
    7.34            qed;
    7.35  	  also; have "... = p x"; 
    7.36            proof (rule quasinorm_minus);
    7.37 -            show "x:E";
    7.38 -            proof (rule subsetD);
    7.39 -              show "H <= E"; ..; 
    7.40 -            qed;
    7.41 +            show "x:E"; ..;
    7.42            qed;
    7.43  	  finally; show "- h x <= p x"; .; 
    7.44  	qed;
    7.45 @@ -69,12 +67,12 @@
    7.46                      & (ALL x:H. h x <= p x)";
    7.47  
    7.48    have "EX t : (graph H h). t = (x, h x)"; 
    7.49 -    by (rule graph_lemma1);
    7.50 +    by (rule graphI2);
    7.51    thus ?thesis;
    7.52    proof (elim bexE); 
    7.53      fix t; assume "t : (graph H h)" and "t = (x, h x)";
    7.54      have ex1: "EX g:c. t:g";
    7.55 -      by (asm_simp only: Union_iff);
    7.56 +      by (simp! only: Union_iff);
    7.57      thus ?thesis;
    7.58      proof (elim bexE);
    7.59        fix g; assume "g:c" "t:g";
    7.60 @@ -85,9 +83,9 @@
    7.61        qed;
    7.62        have "EX H' h'. graph H' h' = g & ?P H' h'"; 
    7.63        proof (rule norm_prev_extension_D);
    7.64 -        from gM; show "g: norm_prev_extensions E p F f"; by asm_simp;
    7.65 +        from gM; show "g: norm_prev_extensions E p F f"; by (simp!);
    7.66        qed;
    7.67 -      thus ?thesis; by (elim exE conjE, intro exI conjI) (asm_simp+);
    7.68 +      thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+;
    7.69      qed;
    7.70    qed;
    7.71  qed;
    7.72 @@ -111,12 +109,13 @@
    7.73      assume "t : graph H h" "t = (x, h x)" "graph H' h' : c" "t : graph H' h'" 
    7.74             "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
    7.75             "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
    7.76 -    show x: "x:H'"; by (asm_simp, rule graphD1);
    7.77 +    show x: "x:H'"; by (simp!, rule graphD1);
    7.78      show "graph H' h' <= graph H h";
    7.79 -      by (asm_simp only: chain_ball_Union_upper);
    7.80 +      by (simp! only: chain_ball_Union_upper);
    7.81    qed;
    7.82  qed;
    7.83  
    7.84 +theorems [trans] = subsetD [COMP swap_prems_rl];
    7.85  
    7.86  lemma some_H'h'2: 
    7.87    "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H; y:H|] 
    7.88 @@ -159,28 +158,33 @@
    7.89      proof; 
    7.90        assume "(graph H'' h'') <= (graph H' h')";
    7.91        show ?thesis;
    7.92 -      proof (intro exI conjI);
    7.93 -	have xh: "(x, h x): graph H' h'"; by (fast);
    7.94 +      proof (intro exI conjI); note [trans] = subsetD;
    7.95 +        have "(x, h x) : graph H'' h''"; by (simp!);
    7.96 +	also; have "... <= graph H' h'"; by (simp!); 
    7.97 +        finally; have xh: "(x, h x): graph H' h'"; .;
    7.98  	thus x: "x:H'"; by (rule graphD1);
    7.99 -	show y: "y:H'"; by (asm_simp, rule graphD1);
   7.100 +	show y: "y:H'"; by (simp!, rule graphD1);
   7.101  	show "(graph H' h') <= (graph H h)";
   7.102 -	  by (asm_simp only: chain_ball_Union_upper);
   7.103 +	  by (simp! only: chain_ball_Union_upper);
   7.104        qed;
   7.105      next;
   7.106        assume "(graph H' h') <= (graph H'' h'')";
   7.107        show ?thesis;
   7.108        proof (intro exI conjI);
   7.109 -	show x: "x:H''"; by (asm_simp, rule graphD1);
   7.110 -	have yh: "(y, h y): graph H'' h''"; by (fast);
   7.111 +	show x: "x:H''"; by (simp!, rule graphD1);
   7.112 +        have "(y, h y) : graph H' h'"; by (simp!);
   7.113 +        also; have "... <= graph H'' h''"; by (simp!);
   7.114 +	finally; have yh: "(y, h y): graph H'' h''"; .;
   7.115          thus y: "y:H''"; by (rule graphD1);
   7.116          show "(graph H'' h'') <= (graph H h)";
   7.117 -          by (asm_simp only: chain_ball_Union_upper);
   7.118 +          by (simp! only: chain_ball_Union_upper);
   7.119        qed;
   7.120      qed;
   7.121    qed;
   7.122  qed;
   7.123  
   7.124 -
   7.125 +lemmas chainE2 = chainD2 [elimify];
   7.126 +lemmas [intro!!] = subsetD chainD; 
   7.127  
   7.128  lemma sup_uniq: "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
   7.129         ALL x:F. f x <= p x; M == norm_prev_extensions E p F f; c : chain M;
   7.130 @@ -188,33 +192,33 @@
   7.131       ==> z = y";
   7.132  proof -;
   7.133    assume "M == norm_prev_extensions E p F f" "c : chain M" "(x, y) : Union c" " (x, z) : Union c";
   7.134 -  have "EX H h. (x, y) : graph H h & (x, z) : graph H h"; 
   7.135 -  proof (elim UnionE chainD2 [elimify]); 
   7.136 +  hence "EX H h. (x, y) : graph H h & (x, z) : graph H h"; 
   7.137 +  proof (elim UnionE chainE2); 
   7.138      fix G1 G2; assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
   7.139 -    have "G1 : M"; by (rule subsetD);
   7.140 +    have "G1 : M"; ..;
   7.141      hence e1: "EX H1 h1. graph H1 h1 = G1";  
   7.142 -      by (force dest: norm_prev_extension_D);
   7.143 -    have "G2 : M"; by (rule subsetD);
   7.144 +      by (force! dest: norm_prev_extension_D);
   7.145 +    have "G2 : M"; ..;
   7.146      hence e2: "EX H2 h2. graph H2 h2 = G2";  
   7.147 -      by (force dest: norm_prev_extension_D);
   7.148 +      by (force! dest: norm_prev_extension_D);
   7.149      from e1 e2; show ?thesis; 
   7.150      proof (elim exE);
   7.151        fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
   7.152 -      have "G1 <= G2 | G2 <= G1"; by (rule chainD);
   7.153 +      have "G1 <= G2 | G2 <= G1"; ..;
   7.154        thus ?thesis;
   7.155        proof;
   7.156          assume "G1 <= G2";
   7.157          thus ?thesis;
   7.158          proof (intro exI conjI);
   7.159 -          show "(x, y) : graph H2 h2"; by force;
   7.160 -          show "(x, z) : graph H2 h2"; by asm_simp;
   7.161 +          show "(x, y) : graph H2 h2"; by (force!);
   7.162 +          show "(x, z) : graph H2 h2"; by (simp!);
   7.163          qed;
   7.164        next;
   7.165          assume "G2 <= G1";
   7.166          thus ?thesis;
   7.167          proof (intro exI conjI);
   7.168 -          show "(x, y) : graph H1 h1"; by asm_simp;
   7.169 -          show "(x, z) : graph H1 h1"; by force; 
   7.170 +          show "(x, y) : graph H1 h1"; by (simp!);
   7.171 +          show "(x, z) : graph H1 h1"; by (force!);
   7.172          qed;
   7.173        qed;
   7.174      qed;
   7.175 @@ -222,8 +226,8 @@
   7.176    thus ?thesis; 
   7.177    proof (elim exE conjE);
   7.178      fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h";
   7.179 -    have "y = h x"; by (rule graph_lemma2);
   7.180 -    also; have "h x = z"; by (rule graph_lemma2 [RS sym]);
   7.181 +    have "y = h x"; ..;
   7.182 +    also; have "... = z"; by (rule sym, rule);
   7.183      finally; show "z = y"; by (rule sym);
   7.184    qed;
   7.185  qed;
   7.186 @@ -254,17 +258,16 @@
   7.187          fix H' h'; assume "x:H'" "y:H'" 
   7.188            and b: "graph H' h' <= graph H h" 
   7.189            and "is_linearform H' h'" "is_subspace H' E";
   7.190 -        have h'x: "h' x = h x"; by (rule graph_lemma3); 
   7.191 -        have h'y: "h' y = h y"; by (rule graph_lemma3);
   7.192 +        have h'x: "h' x = h x"; ..;
   7.193 +        have h'y: "h' y = h y"; ..;
   7.194          have h'xy: "h' (x [+] y) = h' x + h' y"; by (rule linearform_add_linear);
   7.195          have "h' (x [+] y) = h (x [+] y)";  
   7.196          proof -;
   7.197 -          have "x [+] y : H'";
   7.198 -            by (rule subspace_add_closed);
   7.199 -          with b; show ?thesis; by (rule graph_lemma3);
   7.200 +          have "x [+] y : H'"; ..;
   7.201 +          with b; show ?thesis; ..;
   7.202          qed;
   7.203          with h'x h'y h'xy; show ?thesis;
   7.204 -          by asm_simp; 
   7.205 +          by (simp!); 
   7.206        qed;
   7.207      qed;
   7.208  
   7.209 @@ -281,16 +284,15 @@
   7.210  	fix H' h';
   7.211  	assume b: "graph H' h' <= graph H h";
   7.212  	assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
   7.213 -	have h'x: "h' x = h x"; by (rule graph_lemma3);
   7.214 +	have h'x: "h' x = h x"; ..;
   7.215  	have h'ax: "h' (a [*] x) = a * h' x"; by (rule linearform_mult_linear);
   7.216  	have "h' (a [*] x) = h (a [*] x)";
   7.217  	proof -;
   7.218 -	  have "a [*] x : H'";
   7.219 -	    by (rule subspace_mult_closed);
   7.220 -	  with b; show ?thesis; by (rule graph_lemma3);
   7.221 +	  have "a [*] x : H'"; ..;
   7.222 +	  with b; show ?thesis; ..;
   7.223  	qed;
   7.224  	with h'x h'ax; show ?thesis;
   7.225 -	  by asm_simp;
   7.226 +	  by (simp!);
   7.227        qed;
   7.228      qed;
   7.229    qed;
   7.230 @@ -303,14 +305,14 @@
   7.231    assume "M = norm_prev_extensions E p F f" "c: chain M"  "graph H h = Union c"
   7.232      and  e: "EX x. x:c";
   7.233   
   7.234 -  show ?thesis; 
   7.235 +  thus ?thesis; 
   7.236    proof (elim exE);
   7.237      fix x; assume "x:c"; 
   7.238      show ?thesis;    
   7.239      proof -;
   7.240        have "x:norm_prev_extensions E p F f"; 
   7.241        proof (rule subsetD);
   7.242 -	show "c <= norm_prev_extensions E p F f"; by (asm_simp add: chainD2);
   7.243 +	show "c <= norm_prev_extensions E p F f"; by (simp! add: chainD2);
   7.244        qed;
   7.245   
   7.246        hence "(EX G g. graph G g = x
   7.247 @@ -319,15 +321,15 @@
   7.248                      & is_subspace F G
   7.249                      & (graph F f <= graph G g) 
   7.250                      & (ALL x:G. g x <= p x))";
   7.251 -	by (asm_simp add: norm_prev_extension_D);
   7.252 +	by (simp! add: norm_prev_extension_D);
   7.253  
   7.254        thus ?thesis; 
   7.255        proof (elim exE conjE); 
   7.256  	fix G g; assume "graph G g = x" "graph F f <= graph G g";
   7.257  	show ?thesis; 
   7.258          proof -; 
   7.259 -          have "graph F f <= graph G g"; by assumption;
   7.260 -          also; have "graph G g <= graph H h"; by (asm_simp, fast);
   7.261 +          have "graph F f <= graph G g"; .;
   7.262 +          also; have "graph G g <= graph H h"; by ((simp!), fast);
   7.263            finally; show ?thesis; .;
   7.264          qed;
   7.265        qed;
   7.266 @@ -343,22 +345,22 @@
   7.267      "is_subspace F E";
   7.268  
   7.269    show ?thesis; 
   7.270 -  proof (rule subspace_I);
   7.271 -    show "<0> : F"; by (rule zero_in_subspace); 
   7.272 +  proof (rule subspaceI);
   7.273 +    show "<0> : F"; ..;
   7.274      show "F <= H"; 
   7.275 -    proof (rule graph_lemma4);
   7.276 +    proof (rule graph_extD2);
   7.277        show "graph F f <= graph H h";
   7.278          by (rule sup_ext);
   7.279      qed;
   7.280      show "ALL x:F. ALL y:F. x [+] y : F"; 
   7.281      proof (intro ballI); 
   7.282        fix x y; assume "x:F" "y:F";
   7.283 -      show "x [+] y : F"; by asm_simp;
   7.284 +      show "x [+] y : F"; by (simp!);
   7.285      qed;
   7.286      show "ALL x:F. ALL a. a [*] x : F";
   7.287      proof (intro ballI allI);
   7.288        fix x a; assume "x:F";
   7.289 -      show "a [*] x : F"; by asm_simp;
   7.290 +      show "a [*] x : F"; by (simp!);
   7.291      qed;
   7.292    qed;
   7.293  qed;
   7.294 @@ -371,13 +373,13 @@
   7.295      "is_subspace F E";
   7.296  
   7.297    show ?thesis; 
   7.298 -  proof (rule subspace_I);
   7.299 +  proof;
   7.300  
   7.301      show "<0> : H"; 
   7.302      proof (rule subsetD [of F H]);
   7.303        have "is_subspace F H"; by (rule sup_supF);
   7.304 -      thus "F <= H"; by (rule subspace_subset);
   7.305 -      show  "<0> :F"; by (rule zero_in_subspace); 
   7.306 +      thus "F <= H"; ..;
   7.307 +      show  "<0> : F"; ..;
   7.308      qed;
   7.309  
   7.310      show "H <= E"; 
   7.311 @@ -394,8 +396,7 @@
   7.312  	  fix H' h'; assume "x:H'" "is_subspace H' E";
   7.313  	  show "x:E"; 
   7.314  	  proof (rule subsetD);
   7.315 -	    show "H' <= E";
   7.316 -	      by (rule subspace_subset);    
   7.317 +	    show "H' <= E"; ..;
   7.318  	  qed;
   7.319  	qed;
   7.320        qed;
   7.321 @@ -413,10 +414,10 @@
   7.322  	thus ?thesis;
   7.323  	proof (elim exE conjE); 
   7.324  	  fix H' h'; assume "x:H'" "y:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   7.325 -	  have "H' <= H"; by (rule graph_lemma4);
   7.326 +	  have "H' <= H"; ..;
   7.327  	  thus ?thesis;
   7.328  	  proof (rule subsetD);
   7.329 -	    show "x [+] y : H'"; by (rule subspace_add_closed);
   7.330 +	    show "x [+] y : H'"; ..; 
   7.331  	  qed;
   7.332  	qed;
   7.333        qed;
   7.334 @@ -434,10 +435,10 @@
   7.335  	thus ?thesis;
   7.336  	proof (elim exE conjE);
   7.337  	  fix H' h'; assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   7.338 -  	  have "H' <= H"; by (rule graph_lemma4);
   7.339 +  	  have "H' <= H"; ..;
   7.340  	  thus ?thesis;
   7.341  	  proof (rule subsetD);
   7.342 -	    show "a [*] x : H'"; by (rule subspace_mult_closed);
   7.343 +	    show "a [*] x : H'"; ..;
   7.344  	  qed;
   7.345  	qed;
   7.346        qed;
   7.347 @@ -461,8 +462,8 @@
   7.348      proof (elim exE conjE);
   7.349        fix H' h'; assume "x: H'" "graph H' h' <= graph H h" and a: "ALL x: H'. h' x <= p x" ;
   7.350        have "h x = h' x"; 
   7.351 -      proof(rule sym); 
   7.352 -        show "h' x = h x"; by (rule graph_lemma3);
   7.353 +      proof (rule sym); 
   7.354 +        show "h' x = h x"; ..;
   7.355        qed;
   7.356        also; from a; have "... <= p x "; ..;
   7.357        finally; show ?thesis; .;  
   7.358 @@ -471,4 +472,4 @@
   7.359  qed;
   7.360  
   7.361  
   7.362 -end;
   7.363 \ No newline at end of file
   7.364 +end;
     8.1 --- a/src/HOL/Real/HahnBanach/LinearSpace.thy	Tue Sep 21 17:30:55 1999 +0200
     8.2 +++ b/src/HOL/Real/HahnBanach/LinearSpace.thy	Tue Sep 21 17:31:20 1999 +0200
     8.3 @@ -1,5 +1,9 @@
     8.4 +(*  Title:      HOL/Real/HahnBanach/LinearSpace.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Gertrud Bauer, TU Munich
     8.7 +*)
     8.8  
     8.9 -theory LinearSpace = Main + RealAbs + Bounds + Aux:;
    8.10 +theory LinearSpace = Bounds + Aux:;
    8.11  
    8.12  
    8.13  section {* vector spaces *};
    8.14 @@ -7,7 +11,7 @@
    8.15  consts
    8.16    sum	:: "['a, 'a] => 'a"                      (infixl "[+]" 65)  
    8.17    prod  :: "[real, 'a] => 'a"                    (infixr "[*]" 70) 
    8.18 -  zero   :: "'a"                                 ("<0>");
    8.19 +  zero  :: 'a                                    ("<0>");
    8.20  
    8.21  constdefs
    8.22    negate :: "'a => 'a"                           ("[-] _" [100] 100)
    8.23 @@ -41,7 +45,7 @@
    8.24  lemma vs_add_minus_eq_diff: "x [+] [-] y = x [-] y";
    8.25    by (simp add: diff_def);
    8.26  
    8.27 -lemma vs_I:
    8.28 +lemma vsI [intro]:
    8.29    "[| <0>:V; \
    8.30    \      ALL x: V. ALL a::real. a [*] x: V; \     
    8.31    \      ALL x: V. ALL y: V. x [+] y = y [+] x; \
    8.32 @@ -53,43 +57,49 @@
    8.33    \      ALL x: V. ALL a::real. ALL b::real. (a + b) [*] x = a [*] x [+] b [*] x; \
    8.34    \      ALL x: V. ALL a::real. ALL b::real. (a * b) [*] x = a [*] b [*] x; \
    8.35    \      ALL x: V. 1r [*] x = x |] ==> is_vectorspace V";
    8.36 -  by (unfold is_vectorspace_def) auto;
    8.37 +proof (unfold is_vectorspace_def, intro conjI ballI allI);
    8.38 +  fix x y z; assume "x:V" "y:V" "z:V"; 
    8.39 +  assume "ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z =  x [+] (y [+] z)";
    8.40 +  thus "x [+] y [+] z =  x [+] (y [+] z)"; by (elim bspec[elimify]);
    8.41 +qed force+;
    8.42  
    8.43 -lemma zero_in_vs [simp, dest]: "is_vectorspace V ==> <0>:V";
    8.44 -  by (unfold is_vectorspace_def) asm_simp;
    8.45 +  
    8.46  
    8.47 -lemma vs_not_empty: "is_vectorspace V ==> (V ~= {})"; 
    8.48 +lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
    8.49 +  by (unfold is_vectorspace_def) (simp!);
    8.50 +
    8.51 +lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})"; 
    8.52    by (unfold is_vectorspace_def) fast;
    8.53   
    8.54 -lemma vs_add_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V"; 
    8.55 -  by (unfold is_vectorspace_def) asm_simp;
    8.56 +lemma vs_add_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V"; 
    8.57 +  by (unfold is_vectorspace_def) (simp!);
    8.58  
    8.59 -lemma vs_mult_closed [simp]: "[| is_vectorspace V; x: V |] ==> a [*] x: V"; 
    8.60 -  by (unfold is_vectorspace_def) asm_simp;
    8.61 +lemma vs_mult_closed [simp, intro!!]: "[| is_vectorspace V; x: V |] ==> a [*] x: V"; 
    8.62 +  by (unfold is_vectorspace_def) (simp!);
    8.63  
    8.64 -lemma vs_diff_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
    8.65 -  by (unfold diff_def negate_def) asm_simp;
    8.66 +lemma vs_diff_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
    8.67 +  by (unfold diff_def negate_def) (simp!);
    8.68  
    8.69 -lemma vs_neg_closed  [simp]: "[| is_vectorspace V; x: V |] ==>  [-] x: V";
    8.70 -  by (unfold negate_def) asm_simp;
    8.71 +lemma vs_neg_closed  [simp, intro!!]: "[| is_vectorspace V; x: V |] ==>  [-] x: V";
    8.72 +  by (unfold negate_def) (simp!);
    8.73  
    8.74  lemma vs_add_assoc [simp]:  
    8.75    "[| is_vectorspace V; x: V; y: V; z: V|] ==> x [+] y [+] z =  x [+] (y [+] z)";
    8.76    by (unfold is_vectorspace_def) fast;
    8.77  
    8.78  lemma vs_add_commute [simp]: "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
    8.79 -  by (unfold is_vectorspace_def) asm_simp;
    8.80 +  by (unfold is_vectorspace_def) (simp!);
    8.81  
    8.82  lemma vs_add_left_commute [simp]:
    8.83    "[| is_vectorspace V; x:V; y:V; z:V |] ==> x [+] (y [+] z) = y [+] (x [+] z)";
    8.84  proof -;
    8.85    assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
    8.86    have "x [+] (y [+] z) = (x [+] y) [+] z";
    8.87 -    by (asm_simp only: vs_add_assoc);
    8.88 +    by (simp! only: vs_add_assoc);
    8.89    also; have "... = (y [+] x) [+] z";
    8.90 -    by (asm_simp only: vs_add_commute);
    8.91 +    by (simp! only: vs_add_commute);
    8.92    also; have "... = y [+] (x [+] z)";
    8.93 -    by (asm_simp only: vs_add_assoc);
    8.94 +    by (simp! only: vs_add_assoc);
    8.95    finally; show ?thesis; .;
    8.96  qed;
    8.97  
    8.98 @@ -97,44 +107,44 @@
    8.99  theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
   8.100  
   8.101  lemma vs_diff_self [simp]: "[| is_vectorspace V; x:V |] ==>  x [-] x = <0>"; 
   8.102 -  by (unfold is_vectorspace_def) asm_simp;
   8.103 +  by (unfold is_vectorspace_def) (simp!);
   8.104  
   8.105  lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==>  <0> [+] x = x";
   8.106 -  by (unfold is_vectorspace_def) asm_simp;
   8.107 +  by (unfold is_vectorspace_def) (simp!);
   8.108  
   8.109  lemma vs_add_zero_right [simp]: "[| is_vectorspace V; x:V |] ==>  x [+] <0> = x";
   8.110  proof -;
   8.111    assume vs: "is_vectorspace V" "x:V";
   8.112    have "x [+] <0> = <0> [+] x";
   8.113 -    by asm_simp;
   8.114 +    by (simp!);
   8.115    also; have "... = x";
   8.116 -    by asm_simp;
   8.117 +    by (simp!);
   8.118    finally; show ?thesis; .;
   8.119  qed;
   8.120  
   8.121  lemma vs_add_mult_distrib1: 
   8.122    "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
   8.123 -  by (unfold is_vectorspace_def) asm_simp;
   8.124 +  by (unfold is_vectorspace_def) (simp!);
   8.125  
   8.126  lemma vs_add_mult_distrib2: 
   8.127    "[| is_vectorspace V; x:V |] ==>  (a + b) [*] x = a [*] x [+] b [*] x"; 
   8.128 -  by (unfold is_vectorspace_def) asm_simp;
   8.129 +  by (unfold is_vectorspace_def) (simp!);
   8.130  
   8.131  lemma vs_mult_assoc: "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";   
   8.132 -  by (unfold is_vectorspace_def) asm_simp;
   8.133 +  by (unfold is_vectorspace_def) (simp!);
   8.134  
   8.135  lemma vs_mult_assoc2 [simp]: "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
   8.136 -  by (asm_simp only: vs_mult_assoc);
   8.137 +  by (simp! only: vs_mult_assoc);
   8.138  
   8.139  lemma vs_mult_1 [simp]: "[| is_vectorspace V; x:V |] ==> 1r [*] x = x"; 
   8.140 -  by (unfold is_vectorspace_def) asm_simp;
   8.141 +  by (unfold is_vectorspace_def) (simp!);
   8.142  
   8.143  lemma vs_diff_mult_distrib1: 
   8.144    "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
   8.145 -  by (asm_simp add: diff_def negate_def vs_add_mult_distrib1);
   8.146 +  by (simp! add: diff_def negate_def vs_add_mult_distrib1);
   8.147  
   8.148  lemma vs_minus_eq: "[| is_vectorspace V; x:V |] ==> - b [*] x = [-] (b [*] x)";
   8.149 -  by (asm_simp add: negate_def);
   8.150 +  by (simp! add: negate_def);
   8.151  
   8.152  lemma vs_diff_mult_distrib2: 
   8.153    "[| is_vectorspace V; x:V |] ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
   8.154 @@ -142,7 +152,7 @@
   8.155    assume "is_vectorspace V" "x:V";
   8.156    have " (a - b) [*] x = (a + - b ) [*] x"; by (unfold real_diff_def, simp);
   8.157    also; have "... = a [*] x [+] (- b) [*] x"; by (rule vs_add_mult_distrib2);
   8.158 -  also; have "... = a [*] x [+] [-] (b [*] x)"; by (asm_simp add: vs_minus_eq);
   8.159 +  also; have "... = a [*] x [+] [-] (b [*] x)"; by (simp! add: vs_minus_eq);
   8.160    also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp);
   8.161    finally; show ?thesis; .;
   8.162  qed;
   8.163 @@ -151,17 +161,17 @@
   8.164  proof -;
   8.165    assume vs: "is_vectorspace V" "x:V";
   8.166    have  "0r [*] x = (1r - 1r) [*] x";
   8.167 -    by (asm_simp only: real_diff_self);
   8.168 +    by (simp! only: real_diff_self);
   8.169    also; have "... = (1r + - 1r) [*] x";
   8.170      by simp;
   8.171    also; have "... =  1r [*] x [+] (- 1r) [*] x";
   8.172      by (rule vs_add_mult_distrib2);
   8.173    also; have "... = x [+] (- 1r) [*] x";
   8.174 -    by asm_simp;
   8.175 +    by (simp!);
   8.176    also; have "... = x [-] x";
   8.177      by (rule vs_add_mult_minus_1_eq_diff);
   8.178    also; have "... = <0>";
   8.179 -    by asm_simp;
   8.180 +    by (simp!);
   8.181    finally; show ?thesis; .;
   8.182  qed;
   8.183  
   8.184 @@ -169,40 +179,40 @@
   8.185  proof -;
   8.186    assume vs: "is_vectorspace V";
   8.187    have "a [*] <0> = a [*] (<0> [-] (<0>::'a))";
   8.188 -    by (asm_simp);
   8.189 +    by (simp!);
   8.190    also; from zero_in_vs [of V]; have "... =  a [*] <0> [-] a [*] <0>";
   8.191 -    by (asm_simp only: vs_diff_mult_distrib1);
   8.192 +    by (simp! only: vs_diff_mult_distrib1);
   8.193    also; have "... = <0>";
   8.194 -    by asm_simp;
   8.195 +    by (simp!);
   8.196    finally; show ?thesis; .;
   8.197  qed;
   8.198  
   8.199  lemma vs_minus_mult_cancel [simp]:  "[| is_vectorspace V; x:V |] ==>  (- a) [*] [-] x = a [*] x";
   8.200 -  by (unfold negate_def) asm_simp;
   8.201 +  by (unfold negate_def) (simp!);
   8.202  
   8.203  lemma vs_add_minus_left_eq_diff: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] y = y [-] x";
   8.204  proof -; 
   8.205    assume vs: "is_vectorspace V";
   8.206 -  assume x: "x:V"; hence nx: "[-] x:V"; by asm_simp;
   8.207 +  assume x: "x:V"; hence nx: "[-] x:V"; by (simp!);
   8.208    assume y: "y:V";
   8.209    have "[-] x [+] y = y [+] [-] x";
   8.210 -    by (asm_simp add: vs_add_commute [RS sym, of V "[-] x"]);
   8.211 +    by (simp! add: vs_add_commute [RS sym, of V "[-] x"]);
   8.212    also; have "... = y [-] x";
   8.213      by (simp only: vs_add_minus_eq_diff);
   8.214    finally; show ?thesis; .;
   8.215  qed;
   8.216  
   8.217  lemma vs_add_minus [simp]: "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>";
   8.218 -  by (asm_simp add: vs_add_minus_eq_diff); 
   8.219 +  by (simp! add: vs_add_minus_eq_diff); 
   8.220  
   8.221  lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+]  x = <0>";
   8.222 -  by (asm_simp add: vs_add_minus_eq_diff); 
   8.223 +  by (simp! add: vs_add_minus_eq_diff); 
   8.224  
   8.225  lemma vs_minus_minus [simp]: "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
   8.226 -  by (unfold negate_def) asm_simp;
   8.227 +  by (unfold negate_def) (simp!);
   8.228  
   8.229  lemma vs_minus_zero [simp]: "[| is_vectorspace (V::'a set)|] ==>  [-] (<0>::'a) = <0>"; 
   8.230 -  by (unfold negate_def) asm_simp;
   8.231 +  by (unfold negate_def) (simp!);
   8.232  
   8.233  lemma vs_minus_zero_iff [simp]:
   8.234    "[| is_vectorspace V; x:V|] ==>  ([-] x = <0>) = (x = <0>)" (concl is "?L = ?R");
   8.235 @@ -226,20 +236,20 @@
   8.236  qed;
   8.237  
   8.238  lemma vs_add_minus_cancel [simp]:  "[| is_vectorspace V; x:V; y:V|] ==>  x [+] ([-] x [+] y) = y"; 
   8.239 -  by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
   8.240 +  by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute); 
   8.241  
   8.242  lemma vs_minus_add_cancel [simp]: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] (x [+] y) = y"; 
   8.243 -  by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
   8.244 +  by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute); 
   8.245  
   8.246  lemma vs_minus_add_distrib [simp]:  
   8.247    "[| is_vectorspace V; x:V; y:V|] ==>  [-] (x [+] y) = [-] x [+] [-] y";
   8.248 -  by (unfold negate_def, asm_simp add: vs_add_mult_distrib1);
   8.249 +  by (unfold negate_def, simp! add: vs_add_mult_distrib1);
   8.250  
   8.251  lemma vs_diff_zero [simp]: "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
   8.252 -  by (unfold diff_def) asm_simp;  
   8.253 +  by (unfold diff_def) (simp!);  
   8.254  
   8.255  lemma vs_diff_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
   8.256 -  by (unfold diff_def) asm_simp;
   8.257 +  by (unfold diff_def) (simp!);
   8.258  
   8.259  lemma vs_add_left_cancel:
   8.260    "[|is_vectorspace V; x:V; y:V; z:V|] ==> (x [+] y = x [+] z) = (y = z)"  
   8.261 @@ -248,35 +258,34 @@
   8.262    assume vs: "is_vectorspace V" and x: "x:V" and y: "y:V" and z: "z:V";
   8.263    assume l: ?L; 
   8.264    have "y = <0> [+] y";
   8.265 -    by asm_simp;
   8.266 +    by (simp!);
   8.267    also; have "... = [-] x [+] x [+] y";
   8.268 -    by asm_simp;
   8.269 +    by (simp!);
   8.270    also; from vs vs_neg_closed x y ; have "... = [-] x [+] (x [+] y)";
   8.271      by (rule vs_add_assoc);
   8.272    also; have "...  = [-] x [+] (x [+] z)"; 
   8.273 -    by (asm_simp only: l);
   8.274 +    by (simp! only: l);
   8.275    also; from vs vs_neg_closed x z; have "... = [-] x [+] x [+] z";
   8.276      by (rule vs_add_assoc [RS sym]);
   8.277    also; have "... = z";
   8.278 -    by asm_simp;
   8.279 +    by (simp!);
   8.280    finally; show ?R;.;
   8.281  next;    
   8.282    assume ?R;
   8.283 -  show ?L;
   8.284 -    by force;
   8.285 +  thus ?L; by force;
   8.286  qed;
   8.287  
   8.288  lemma vs_add_right_cancel: 
   8.289    "[| is_vectorspace V; x:V; y:V; z:V |] ==>  (y [+] x = z [+] x) = (y = z)";  
   8.290 -  by (asm_simp only: vs_add_commute vs_add_left_cancel);
   8.291 +  by (simp! only: vs_add_commute vs_add_left_cancel);
   8.292  
   8.293  lemma vs_add_assoc_cong [tag FIXME simp]: "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] \
   8.294  \   ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)"; 
   8.295 -  by (asm_simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
   8.296 +  by (simp! del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
   8.297  
   8.298  lemma vs_mult_left_commute: 
   8.299    "[| is_vectorspace V; x:V; y:V; z:V |] ==>  x [*] y [*] z = y [*] x [*] z";  
   8.300 -  by (asm_simp add: real_mult_commute);
   8.301 +  by (simp! add: real_mult_commute);
   8.302  
   8.303  lemma vs_mult_left_cancel: 
   8.304    "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>  (a [*] x = a [*] y) = (x = y)"
   8.305 @@ -288,20 +297,20 @@
   8.306    assume a: "a ~= 0r";
   8.307    assume l: ?L;
   8.308    have "x = 1r [*] x";
   8.309 -    by (asm_simp);
   8.310 +    by (simp!);
   8.311    also; have "... = (rinv a * a) [*] x";
   8.312 -    by (asm_simp);
   8.313 +    by (simp!);
   8.314    also; have "... = rinv a [*] (a [*] x)";
   8.315 -    by (asm_simp only: vs_mult_assoc);
   8.316 +    by (simp! only: vs_mult_assoc);
   8.317    also; have "... = rinv a [*] (a [*] y)";
   8.318 -    by (asm_simp only: l);
   8.319 +    by (simp! only: l);
   8.320    also; have "... = y";
   8.321 -    by (asm_simp);
   8.322 +    by (simp!);
   8.323    finally; show ?R;.;
   8.324  next;
   8.325    assume ?R;
   8.326    show ?L;
   8.327 -    by (asm_simp);
   8.328 +    by (simp!);
   8.329  qed;
   8.330  
   8.331  lemma vs_eq_diff_eq: 
   8.332 @@ -310,32 +319,32 @@
   8.333  proof -;
   8.334    assume vs: "is_vectorspace V";
   8.335    assume x: "x:V";
   8.336 -  assume y: "y:V"; hence n: "[-] y:V"; by asm_simp;
   8.337 +  assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
   8.338    assume z: "z:V";
   8.339    show "?L = ?R";   
   8.340    proof;
   8.341      assume l: ?L;
   8.342      have "x [+] y = z [-] y [+] y";
   8.343 -      by (asm_simp add: l);
   8.344 +      by (simp! add: l);
   8.345      also; have "... = z [+] [-] y [+] y";        
   8.346 -      by (asm_simp only: vs_add_minus_eq_diff);
   8.347 +      by (simp! only: vs_add_minus_eq_diff);
   8.348      also; from vs z n y; have "... = z [+] ([-] y [+] y)";
   8.349 -      by (asm_simp only: vs_add_assoc);
   8.350 +      by (simp! only: vs_add_assoc);
   8.351      also; have "... = z [+] <0>";
   8.352 -      by (asm_simp only: vs_add_minus_left);
   8.353 +      by (simp! only: vs_add_minus_left);
   8.354      also; have "... = z";
   8.355 -      by (asm_simp only: vs_add_zero_right);
   8.356 +      by (simp! only: vs_add_zero_right);
   8.357      finally; show ?R;.;
   8.358    next;
   8.359      assume r: ?R;
   8.360      have "z [-] y = (x [+] y) [-] y";
   8.361 -      by (asm_simp only: r);
   8.362 +      by (simp! only: r);
   8.363      also; have "... = x [+] y [+] [-] y";
   8.364 -      by (asm_simp only: vs_add_minus_eq_diff);
   8.365 +      by (simp! only: vs_add_minus_eq_diff);
   8.366     also; from vs x y n; have "... = x [+] (y [+] [-] y)";
   8.367        by (rule vs_add_assoc); 
   8.368      also; have "... = x";     
   8.369 -      by (asm_simp);
   8.370 +      by (simp!);
   8.371      finally; show ?L; by (rule sym);
   8.372    qed;
   8.373  qed;
   8.374 @@ -343,19 +352,19 @@
   8.375  lemma vs_add_minus_eq_minus: "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x"; 
   8.376  proof -;
   8.377    assume vs: "is_vectorspace V";
   8.378 -  assume x: "x:V"; hence n: "[-] x : V"; by (asm_simp);
   8.379 +  assume x: "x:V"; hence n: "[-] x : V"; by (simp!);
   8.380    assume y: "y:V";
   8.381    assume xy: "<0> = x [+] y";
   8.382    from vs n; have "[-] x = [-] x [+] <0>";
   8.383 -    by asm_simp;
   8.384 +    by (simp!);
   8.385    also; have "... = [-] x [+] (x [+] y)"; 
   8.386 -    by (asm_simp);
   8.387 +    by (simp!);
   8.388    also; from vs n x y; have "... = [-] x [+] x [+] y";
   8.389      by (rule vs_add_assoc [RS sym]);
   8.390    also; from vs x y; have "... = (x [+] [-] x) [+] y";
   8.391 -    by (simp);
   8.392 +    by simp;
   8.393    also; from vs y; have "... = y";
   8.394 -    by (asm_simp);
   8.395 +    by (simp!);
   8.396    finally; show ?thesis;
   8.397      by (rule sym);
   8.398  qed;  
   8.399 @@ -366,10 +375,10 @@
   8.400    have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
   8.401    also; have "... = <0>"; .;
   8.402    finally; have e: "<0> = x [+] [-] y"; by (rule sym);
   8.403 -  have "x = [-] [-] x"; by asm_simp;
   8.404 +  have "x = [-] [-] x"; by (simp!);
   8.405    also; from _ _ _ e; have "[-] x = [-] y"; 
   8.406 -    by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) asm_simp+;
   8.407 -  also; have "[-] ... = y"; by asm_simp; 
   8.408 +    by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) (simp!)+;
   8.409 +  also; have "[-] ... = y"; by (simp!); 
   8.410    finally; show "x = y"; .;
   8.411  qed;
   8.412  
   8.413 @@ -377,12 +386,12 @@
   8.414    "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] ==> a [-] c = d [-] b";
   8.415  proof -; 
   8.416    assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" and eq: "a [+] b = c [+] d";
   8.417 -  have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (asm_simp add: vs_add_left_cancel);
   8.418 +  have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (simp! add: vs_add_left_cancel);
   8.419    also; have "... = d"; by (rule vs_minus_add_cancel);
   8.420    finally; have eq: "[-] c [+] (a [+] b) = d"; .;
   8.421    from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b"; 
   8.422      by (simp add: vs_add_ac diff_def);
   8.423 -  also; from eq; have "...  = d [+] [-] b"; by (asm_simp add: vs_add_right_cancel);
   8.424 +  also; from eq; have "...  = d [+] [-] b"; by (simp! add: vs_add_right_cancel);
   8.425    also; have "... = d [-] b"; by (simp add : diff_def);
   8.426    finally; show "a [-] c = d [-] b"; .;
   8.427  qed;
   8.428 @@ -393,10 +402,10 @@
   8.429  proof (rule classical);
   8.430    assume "is_vectorspace V" "x:V" "a [*] x = <0>" "x ~= <0>";
   8.431    assume "a ~= 0r";
   8.432 -  have "x = (rinv a * a) [*] x"; by asm_simp;
   8.433 +  have "x = (rinv a * a) [*] x"; by (simp!);
   8.434    also; have "... = (rinv a) [*] (a [*] x)"; by (rule vs_mult_assoc);
   8.435 -  also; have "... = (rinv a) [*] <0>"; by asm_simp;
   8.436 -  also; have "... = <0>"; by asm_simp;
   8.437 +  also; have "... = (rinv a) [*] <0>"; by (simp!);
   8.438 +  also; have "... = <0>"; by (simp!);
   8.439    finally; have "x = <0>"; .;
   8.440    thus "a = 0r"; by contradiction; 
   8.441  qed;
   8.442 @@ -407,33 +416,33 @@
   8.443  proof -; 
   8.444    assume vs: "is_vectorspace V";
   8.445    assume x: "x:V";
   8.446 -  assume y: "y:V"; hence n: "[-] y:V"; by (asm_simp);
   8.447 -  assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
   8.448 +  assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
   8.449 +  assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
   8.450    assume u: "u:V";
   8.451    show "?L = ?R";
   8.452    proof;
   8.453      assume l: ?L;
   8.454      from vs u; have "u = <0> [+] u";
   8.455 -      by asm_simp;
   8.456 +      by (simp!);
   8.457      also; from vs y vs_neg_closed u; have "... = [-] y [+] y [+] u";
   8.458 -      by asm_simp;
   8.459 +      by (simp!);
   8.460      also; from vs n y u; have "... = [-] y [+] (y [+] u)";
   8.461 -      by (asm_simp only: vs_add_assoc);
   8.462 +      by (simp! only: vs_add_assoc);
   8.463      also; have "... = [-] y [+] (x [+] (y [+] z))";
   8.464 -      by (asm_simp only: l);
   8.465 +      by (simp! only: l);
   8.466      also; have "... = [-] y [+] (y [+] (x [+] z))";
   8.467 -      by (asm_simp only: vs_add_left_commute);
   8.468 +      by (simp! only: vs_add_left_commute);
   8.469      also; from vs n y xz; have "... = [-] y [+] y [+] (x [+] z)";
   8.470 -      by (asm_simp only: vs_add_assoc);
   8.471 +      by (simp! only: vs_add_assoc);
   8.472      also; have "... = (x [+] z)";
   8.473 -      by (asm_simp);
   8.474 +      by (simp!);
   8.475      finally; show ?R; by (rule sym);
   8.476    next;
   8.477      assume r: ?R;
   8.478      have "x [+] (y [+] z) = y [+] (x [+] z)";
   8.479 -      by (asm_simp only: vs_add_left_commute [of V x y z]);
   8.480 +      by (simp! only: vs_add_left_commute [of V x y z]);
   8.481      also; have "... = y [+] u";
   8.482 -      by (asm_simp only: r);
   8.483 +      by (simp! only: r);
   8.484      finally; show ?L; .;
   8.485    qed;
   8.486  qed;
   8.487 @@ -445,41 +454,41 @@
   8.488    assume vs: "is_vectorspace V";
   8.489    assume x: "x:V";
   8.490    assume y: "y:V"; 
   8.491 -  assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
   8.492 -  hence nz: "[-] z: V"; by (asm_simp);
   8.493 +  assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
   8.494 +  hence nz: "[-] z: V"; by (simp!);
   8.495    show "?L = ?R";
   8.496    proof;
   8.497      assume l: ?L;
   8.498 -    have n: "<0>:V"; by (asm_simp);
   8.499 +    have n: "<0>:V"; by (simp!);
   8.500      have "y [+] <0> = y";
   8.501 -      by (asm_simp only: vs_add_zero_right); 
   8.502 +      by (simp! only: vs_add_zero_right); 
   8.503      also; have "... =  x [+] (y [+] z)";
   8.504 -      by (asm_simp only: l); 
   8.505 +      by (simp! only: l); 
   8.506      also; have "... = y [+] (x [+] z)";
   8.507 -      by (asm_simp only: vs_add_left_commute); 
   8.508 +      by (simp! only: vs_add_left_commute); 
   8.509      finally; have "y [+] <0> = y [+] (x [+] z)"; .;
   8.510      with vs y n xz; have "<0> = x [+] z";
   8.511        by (rule vs_add_left_cancel [RS iffD1]); 
   8.512      with vs x z; have "z = [-] x";
   8.513 -      by (asm_simp only: vs_add_minus_eq_minus);
   8.514 +      by (simp! only: vs_add_minus_eq_minus);
   8.515      then; show ?R; 
   8.516 -      by (asm_simp); 
   8.517 +      by (simp!); 
   8.518    next;
   8.519      assume r: ?R;
   8.520      have "x [+] (y [+] z) = [-] z [+] (y [+] z)";
   8.521 -      by (asm_simp only: r); 
   8.522 +      by (simp! only: r); 
   8.523      also; from vs nz y z; have "... = y [+] ([-] z [+] z)";
   8.524 -       by (asm_simp only: vs_add_left_commute);
   8.525 +       by (simp! only: vs_add_left_commute);
   8.526      also; have "... = y [+] <0>";
   8.527 -      by (asm_simp);
   8.528 +      by (simp!);
   8.529      also; have "... = y";
   8.530 -      by (asm_simp);
   8.531 +      by (simp!);
   8.532      finally; show ?L; .;
   8.533    qed;
   8.534  qed;
   8.535  
   8.536  lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
   8.537 -  by (asm_simp); 
   8.538 +  by (simp!); 
   8.539  
   8.540  
   8.541  end;
   8.542 \ No newline at end of file
     9.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Tue Sep 21 17:30:55 1999 +0200
     9.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Tue Sep 21 17:31:20 1999 +0200
     9.3 @@ -1,3 +1,7 @@
     9.4 +(*  Title:      HOL/Real/HahnBanach/Linearform.thy
     9.5 +    ID:         $Id$
     9.6 +    Author:     Gertrud Bauer, TU Munich
     9.7 +*)
     9.8  
     9.9  theory Linearform = LinearSpace:;
    9.10  
    9.11 @@ -12,39 +16,41 @@
    9.12  lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
    9.13      !! x c. x : V ==> f (c [*] x) = c * f x |]
    9.14   ==> is_linearform V f";
    9.15 - by (unfold is_linearform_def, force);
    9.16 + by (unfold is_linearform_def) force;
    9.17  
    9.18 -lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
    9.19 - by (unfold is_linearform_def, auto);
    9.20 +lemma linearform_add_linear [intro!!]: 
    9.21 +  "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
    9.22 +  by (unfold is_linearform_def) auto;
    9.23  
    9.24 -lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
    9.25 - by (unfold is_linearform_def, auto);
    9.26 +lemma linearform_mult_linear [intro!!]: 
    9.27 +  "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
    9.28 +  by (unfold is_linearform_def) auto;
    9.29  
    9.30 -lemma linearform_neg_linear:
    9.31 +lemma linearform_neg_linear [intro!!]:
    9.32    "[|  is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
    9.33  proof -; 
    9.34    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
    9.35 -  have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1);
    9.36 +  have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);
    9.37    also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
    9.38 -  also; have "... = - (f x)"; by asm_simp;
    9.39 +  also; have "... = - (f x)"; by (simp!);
    9.40    finally; show ?thesis; .;
    9.41  qed;
    9.42  
    9.43 -lemma linearform_diff_linear: 
    9.44 +lemma linearform_diff_linear [intro!!]: 
    9.45    "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";  
    9.46  proof -;
    9.47    assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
    9.48    have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
    9.49 -  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+);
    9.50 +  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;
    9.51    also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
    9.52 -  finally; show "f (x [-] y) = f x - f y"; by asm_simp;
    9.53 +  finally; show "f (x [-] y) = f x - f y"; by (simp!);
    9.54  qed;
    9.55  
    9.56 -lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    9.57 +lemma linearform_zero [intro!!]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    9.58  proof -; 
    9.59    assume "is_vectorspace V" "is_linearform V f";
    9.60 -  have "f <0> = f (<0> [-] <0>)"; by asm_simp;
    9.61 -  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+;
    9.62 +  have "f <0> = f (<0> [-] <0>)"; by (simp!);
    9.63 +  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;
    9.64    also; have "... = 0r"; by simp;
    9.65    finally; show "f <0> = 0r"; .;
    9.66  qed; 
    10.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Sep 21 17:30:55 1999 +0200
    10.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Sep 21 17:31:20 1999 +0200
    10.3 @@ -1,3 +1,7 @@
    10.4 +(*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Gertrud Bauer, TU Munich
    10.7 +*)
    10.8  
    10.9  theory NormedSpace =  Subspace:;
   10.10  
   10.11 @@ -20,31 +24,31 @@
   10.12      ==> is_quasinorm V norm";
   10.13    by (unfold is_quasinorm_def, force);
   10.14  
   10.15 -lemma quasinorm_ge_zero:
   10.16 -  "[|is_quasinorm V norm; x:V |] ==> 0r <= norm x";
   10.17 +lemma quasinorm_ge_zero [intro!!]:
   10.18 +  "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x";
   10.19    by (unfold is_quasinorm_def, force);
   10.20  
   10.21  lemma quasinorm_mult_distrib: 
   10.22 -  "[|is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
   10.23 +  "[| is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
   10.24    by (unfold is_quasinorm_def, force);
   10.25  
   10.26  lemma quasinorm_triangle_ineq: 
   10.27 -  "[|is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
   10.28 +  "[| is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
   10.29    by (unfold is_quasinorm_def, force);
   10.30  
   10.31  lemma quasinorm_diff_triangle_ineq: 
   10.32 -  "[|is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
   10.33 +  "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
   10.34  proof -;
   10.35    assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
   10.36    have "norm (x [-] y) = norm (x [+] - 1r [*] y)";  by (simp add: diff_def negate_def);
   10.37 -  also; have "... <= norm x + norm  (- 1r [*] y)"; by (rule quasinorm_triangle_ineq, asm_simp+);
   10.38 +  also; have "... <= norm x + norm  (- 1r [*] y)"; by (simp! add: quasinorm_triangle_ineq);
   10.39    also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; by (rule quasinorm_mult_distrib);
   10.40    also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   10.41    finally; show "norm (x [-] y) <= norm x + norm y"; by simp;
   10.42  qed;
   10.43  
   10.44  lemma quasinorm_minus: 
   10.45 -  "[|is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
   10.46 +  "[| is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
   10.47  proof -;
   10.48    assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
   10.49    have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force;
   10.50 @@ -61,18 +65,19 @@
   10.51    "is_norm V norm == ALL x: V.  is_quasinorm V norm 
   10.52        & (norm x = 0r) = (x = <0>)";
   10.53  
   10.54 -lemma is_norm_I: "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
   10.55 +lemma is_normI [intro]: 
   10.56 +  "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
   10.57    by (unfold is_norm_def, force);
   10.58  
   10.59 -lemma norm_is_quasinorm: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
   10.60 +lemma norm_is_quasinorm [intro!!]: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
   10.61    by (unfold is_norm_def, force);
   10.62  
   10.63  lemma norm_zero_iff: "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
   10.64    by (unfold is_norm_def, force);
   10.65  
   10.66 -lemma norm_ge_zero:
   10.67 +lemma norm_ge_zero [intro!!]:
   10.68    "[|is_norm V norm; x:V |] ==> 0r <= norm x";
   10.69 -  by (unfold is_norm_def, unfold is_quasinorm_def, force);
   10.70 +  by (unfold is_norm_def is_quasinorm_def, force);
   10.71  
   10.72  
   10.73  subsection {* normed vector space *};
   10.74 @@ -83,60 +88,65 @@
   10.75        is_vectorspace V &
   10.76        is_norm V norm";
   10.77  
   10.78 -lemma normed_vsI: "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
   10.79 -  by (unfold is_normed_vectorspace_def, intro conjI);
   10.80 +lemma normed_vsI [intro]: 
   10.81 +  "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
   10.82 +  by (unfold is_normed_vectorspace_def) blast; 
   10.83  
   10.84 -lemma normed_vs_vs: "is_normed_vectorspace V norm ==> is_vectorspace V";
   10.85 -  by (unfold is_normed_vectorspace_def, force);
   10.86 +lemma normed_vs_vs [intro!!]: "is_normed_vectorspace V norm ==> is_vectorspace V";
   10.87 +  by (unfold is_normed_vectorspace_def) force;
   10.88  
   10.89 -lemma normed_vs_norm: "is_normed_vectorspace V norm ==> is_norm V norm";
   10.90 -  by (unfold is_normed_vectorspace_def, force);
   10.91 +lemma normed_vs_norm [intro!!]: "is_normed_vectorspace V norm ==> is_norm V norm";
   10.92 +  by (unfold is_normed_vectorspace_def, elim conjE);
   10.93  
   10.94 -lemma normed_vs_norm_ge_zero: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
   10.95 -  by (unfold is_normed_vectorspace_def, elim conjE, rule norm_ge_zero);
   10.96 +lemma normed_vs_norm_ge_zero [intro!!]: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
   10.97 +  by (unfold is_normed_vectorspace_def, rule, elim conjE);
   10.98  
   10.99 -lemma normed_vs_norm_gt_zero: 
  10.100 +lemma normed_vs_norm_gt_zero [intro!!]: 
  10.101    "[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
  10.102  proof (unfold is_normed_vectorspace_def, elim conjE);
  10.103    assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
  10.104 -  have "0r <= norm x"; by (rule norm_ge_zero);
  10.105 +  have "0r <= norm x"; ..;
  10.106    also; have "0r ~= norm x";
  10.107 -  proof; 
  10.108 +  proof;
  10.109      presume "norm x = 0r";
  10.110 -    have "x = <0>"; by (asm_simp add: norm_zero_iff);
  10.111 +    also; have "?this = (x = <0>)"; by (rule norm_zero_iff);
  10.112 +    finally; have "x = <0>"; .;
  10.113      thus "False"; by contradiction;
  10.114    qed (rule sym);
  10.115    finally; show "0r < norm x"; .;
  10.116  qed;
  10.117  
  10.118 -lemma normed_vs_norm_mult_distrib: 
  10.119 +lemma normed_vs_norm_mult_distrib [intro!!]: 
  10.120    "[| is_normed_vectorspace V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
  10.121 -  by (unfold is_normed_vectorspace_def, elim conjE, 
  10.122 -      rule quasinorm_mult_distrib, rule norm_is_quasinorm);
  10.123 +  by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, rule normed_vs_norm);
  10.124  
  10.125 -lemma normed_vs_norm_triangle_ineq: 
  10.126 +lemma normed_vs_norm_triangle_ineq [intro!!]: 
  10.127    "[| is_normed_vectorspace V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
  10.128 -  by (unfold is_normed_vectorspace_def, elim conjE, 
  10.129 -      rule quasinorm_triangle_ineq, rule norm_is_quasinorm);
  10.130 +  by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, rule normed_vs_norm);
  10.131  
  10.132 -lemma subspace_normed_vs: 
  10.133 -  "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm";
  10.134 +lemma subspace_normed_vs [intro!!]: 
  10.135 +  "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] 
  10.136 +   ==> is_normed_vectorspace F norm";
  10.137  proof (rule normed_vsI);
  10.138    assume "is_subspace F E" "is_vectorspace E" "is_normed_vectorspace E norm";
  10.139 -  show "is_vectorspace F"; by (rule subspace_vs);
  10.140 +  show "is_vectorspace F"; ..;
  10.141    show "is_norm F norm"; 
  10.142 -  proof (intro is_norm_I ballI conjI);
  10.143 +  proof (intro is_normI ballI conjI);
  10.144      show "is_quasinorm F norm"; 
  10.145 -    proof (rule is_quasinormI, rule normed_vs_norm_ge_zero [of E norm], 
  10.146 -       rule normed_vs_norm_mult_distrib [of E norm], rule normed_vs_norm_triangle_ineq);
  10.147 -    qed ( rule subsetD [OF subspace_subset], assumption+)+; 
  10.148 +    proof;
  10.149 +      fix x y a; presume "x : E";
  10.150 +      show "0r <= norm x"; ..;
  10.151 +      show "norm (a [*] x) = rabs a * norm x"; ..;
  10.152 +      presume "y : E";
  10.153 +      show "norm (x [+] y) <= norm x + norm y"; ..;
  10.154 +    qed (simp!)+;
  10.155  
  10.156      fix x; assume "x : F";
  10.157 -    have n: "is_norm E norm"; by (unfold is_normed_vectorspace_def, asm_simp);
  10.158 -    have "x:E"; by (rule subsetD [OF subspace_subset]);
  10.159 -    from n this; show "(norm x = 0r) = (x = <0>)"; by (rule norm_zero_iff);
  10.160 +    show "(norm x = 0r) = (x = <0>)"; 
  10.161 +    proof (rule norm_zero_iff);
  10.162 +      show "is_norm E norm"; ..;
  10.163 +    qed (simp!);
  10.164    qed;
  10.165  qed;
  10.166  
  10.167  end;
  10.168 -
    11.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 17:30:55 1999 +0200
    11.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 17:31:20 1999 +0200
    11.3 @@ -1,3 +1,7 @@
    11.4 +(*  Title:      HOL/Real/HahnBanach/Subspace.thy
    11.5 +    ID:         $Id$
    11.6 +    Author:     Gertrud Bauer, TU Munich
    11.7 +*)
    11.8  
    11.9  theory Subspace = LinearSpace:;
   11.10  
   11.11 @@ -10,74 +14,75 @@
   11.12       &  (ALL x:U. ALL y:U. ALL a. x [+] y : U                          
   11.13                         & a [*] x : U)";                            
   11.14  
   11.15 -lemma subspace_I: 
   11.16 +lemma subspaceI [intro]: 
   11.17    "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
   11.18    \ ==> is_subspace U V";
   11.19 -  by (unfold is_subspace_def) blast;
   11.20 +  by (unfold is_subspace_def) (simp!);
   11.21  
   11.22  lemma "is_subspace U V ==> U ~= {}";
   11.23    by (unfold is_subspace_def) force;
   11.24  
   11.25 -lemma zero_in_subspace: "is_subspace U V ==> <0>:U";
   11.26 +lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
   11.27 +  by (unfold is_subspace_def) (simp!);;
   11.28 +
   11.29 +lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
   11.30 +  by (unfold is_subspace_def) (simp!);
   11.31 +
   11.32 +lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
   11.33    by (unfold is_subspace_def) force;
   11.34  
   11.35 -lemma subspace_subset: "is_subspace U V ==> U <= V";
   11.36 -  by (unfold is_subspace_def) fast;
   11.37 +lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
   11.38 +  by (unfold is_subspace_def) (simp!);
   11.39  
   11.40 -lemma subspace_subset2 [simp]: "[| is_subspace U V; x:U |]==> x:V";
   11.41 -  by (unfold is_subspace_def) fast;
   11.42 -
   11.43 -lemma subspace_add_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
   11.44 -  by (unfold is_subspace_def) asm_simp;
   11.45 +lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
   11.46 +  by (unfold is_subspace_def) (simp!);
   11.47  
   11.48 -lemma subspace_mult_closed [simp]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
   11.49 -  by (unfold is_subspace_def) asm_simp;
   11.50 +lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
   11.51 +  by (unfold diff_def negate_def) (simp!);
   11.52  
   11.53 -lemma subspace_diff_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
   11.54 -  by (unfold diff_def negate_def) asm_simp;
   11.55 +lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
   11.56 + by (unfold negate_def) (simp!);
   11.57  
   11.58 -lemma subspace_neg_closed [simp]: "[| is_subspace U V; x: U |] ==> [-] x: U";
   11.59 - by (unfold negate_def) asm_simp;
   11.60  
   11.61  theorem subspace_vs [intro!!]:
   11.62    "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
   11.63  proof -;
   11.64 -  presume "U <= V";
   11.65 +  assume "is_subspace U V";
   11.66    assume "is_vectorspace V";
   11.67    assume "is_subspace U V";
   11.68    show ?thesis;
   11.69 -  proof (rule vs_I);
   11.70 -    show "<0>:U"; by (rule zero_in_subspace);
   11.71 -    show "ALL x:U. ALL a. a [*] x : U"; by asm_simp;
   11.72 -    show "ALL x:U. ALL y:U. x [+] y : U"; by asm_simp;
   11.73 -  qed (asm_simp add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
   11.74 -next;
   11.75 -  assume "is_subspace U V";
   11.76 -  show "U <= V"; by (rule subspace_subset);
   11.77 +  proof; 
   11.78 +    show "<0>:U"; ..;
   11.79 +    show "ALL x:U. ALL a. a [*] x : U"; by (simp!);
   11.80 +    show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!);
   11.81 +  qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
   11.82  qed;
   11.83  
   11.84 -lemma subspace_refl: "is_vectorspace V ==> is_subspace V V";
   11.85 -proof (unfold is_subspace_def, intro conjI); 
   11.86 +lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
   11.87 +proof; 
   11.88    assume "is_vectorspace V";
   11.89 -  show "<0> : V"; by (rule zero_in_vs [of V], assumption);
   11.90 -  show "V <= V"; by (simp);
   11.91 -  show "ALL x::'a:V. ALL y::'a:V. ALL a::real. x [+] y : V & a [*] x : V"; by (asm_simp);
   11.92 +  show "<0> : V"; ..;
   11.93 +  show "V <= V"; ..;
   11.94 +  show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!);
   11.95 +  show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
   11.96  qed;
   11.97  
   11.98  lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
   11.99 -proof (rule subspace_I); 
  11.100 +proof; 
  11.101    assume "is_subspace U V" "is_subspace V W";
  11.102 -  show "<0> : U"; by (rule zero_in_subspace);;
  11.103 -  from subspace_subset [of U] subspace_subset [of V]; show uw: "U <= W"; by force;
  11.104 +  show "<0> : U"; ..;
  11.105 +  have "U <= V"; ..;
  11.106 +  also; have "V <= W"; ..;
  11.107 +  finally; show "U <= W"; .;
  11.108    show "ALL x:U. ALL y:U. x [+] y : U"; 
  11.109    proof (intro ballI);
  11.110      fix x y; assume "x:U" "y:U";
  11.111 -    show "x [+] y : U"; by (rule subspace_add_closed);
  11.112 +    show "x [+] y : U"; by (simp!);
  11.113    qed;
  11.114    show "ALL x:U. ALL a. a [*] x : U";
  11.115    proof (intro ballI allI);
  11.116      fix x a; assume "x:U";
  11.117 -    show "a [*] x : U"; by (rule subspace_mult_closed);
  11.118 +    show "a [*] x : U"; by (simp!);
  11.119    qed;
  11.120  qed;
  11.121  
  11.122 @@ -89,39 +94,45 @@
  11.123    "lin x == {y. ? a. y = a [*] x}";
  11.124  
  11.125  lemma linD: "x : lin v = (? a::real. x = a [*] v)";
  11.126 -  by (unfold lin_def) fast;
  11.127 +  by (unfold lin_def) force;
  11.128  
  11.129  lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
  11.130  proof (unfold lin_def, intro CollectI exI);
  11.131    assume "is_vectorspace V" "x:V";
  11.132 -  show "x = 1r [*] x"; by (asm_simp);
  11.133 +  show "x = 1r [*] x"; by (simp!);
  11.134  qed;
  11.135  
  11.136 -lemma lin_subspace: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
  11.137 -proof (rule subspace_I);
  11.138 +lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
  11.139 +proof;
  11.140    assume "is_vectorspace V" "x:V";
  11.141    show "<0> : lin x"; 
  11.142    proof (unfold lin_def, intro CollectI exI);
  11.143 -    show "<0> = 0r [*] x"; by asm_simp;
  11.144 +    show "<0> = 0r [*] x"; by (simp!);
  11.145    qed;
  11.146 +
  11.147    show "lin x <= V";
  11.148 -  proof (unfold lin_def, intro subsetI, elim CollectD [elimify] exE); 
  11.149 -    fix xa a; assume "xa = a [*] x"; show "xa:V"; by asm_simp;
  11.150 +  proof (unfold lin_def, intro subsetI, elim CollectE exE); 
  11.151 +    fix xa a; assume "xa = a [*] x"; 
  11.152 +    show "xa:V"; by (simp!);
  11.153    qed;
  11.154 +
  11.155    show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; 
  11.156    proof (intro ballI);
  11.157 -    fix x1 x2; assume "x1 : lin x" "x2 : lin x"; show "x1 [+] x2 : lin x";
  11.158 -    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
  11.159 +    fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
  11.160 +    thus "x1 [+] x2 : lin x";
  11.161 +    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);   (* FIXME !? *)
  11.162        fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
  11.163 -      show "x1 [+] x2 = (a1 + a2) [*] x"; by (asm_simp add: vs_add_mult_distrib2);
  11.164 +      show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
  11.165      qed;
  11.166    qed;
  11.167 +
  11.168    show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
  11.169    proof (intro ballI allI);
  11.170 -    fix x1 a; assume "x1 : lin x"; show "a [*] x1 : lin x";
  11.171 -    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
  11.172 +    fix x1 a; assume "x1 : lin x"; 
  11.173 +    thus "a [*] x1 : lin x";
  11.174 +    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);
  11.175        fix a1; assume "x1 = a1 [*] x";
  11.176 -      show "a [*] x1 = (a * a1) [*] x"; by asm_simp;
  11.177 +      show "a [*] x1 = (a * a1) [*] x"; by (simp!);
  11.178      qed;
  11.179    qed; 
  11.180  qed;
  11.181 @@ -130,7 +141,7 @@
  11.182  lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
  11.183  proof (rule subspace_vs);
  11.184    assume "is_vectorspace V" "x:V";
  11.185 -  show "is_subspace (lin x) V"; by (rule lin_subspace);
  11.186 +  show "is_subspace (lin x) V"; ..;
  11.187  qed;
  11.188  
  11.189  section {* sum of two vectorspaces *};
  11.190 @@ -140,159 +151,181 @@
  11.191    "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
  11.192  
  11.193  lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
  11.194 -  by (unfold vectorspace_sum_def) fast;
  11.195 +  by (unfold vectorspace_sum_def) (simp!);
  11.196  
  11.197 -lemma vs_sum_I: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
  11.198 +lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
  11.199 +
  11.200 +lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
  11.201    by (unfold vectorspace_sum_def, intro CollectI bexI); 
  11.202  
  11.203  lemma subspace_vs_sum1 [intro!!]: 
  11.204    "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
  11.205 -proof (rule subspace_I);
  11.206 +proof; 
  11.207    assume "is_vectorspace U" "is_vectorspace V";
  11.208 -  show "<0> : U"; by (rule zero_in_vs);
  11.209 +  show "<0> : U"; ..;
  11.210    show "U <= vectorspace_sum U V";
  11.211 -  proof (intro subsetI vs_sum_I);
  11.212 +  proof (intro subsetI vs_sumI);
  11.213    fix x; assume "x:U";
  11.214 -    show "x = x [+] <0>"; by asm_simp;
  11.215 -    show "<0> : V"; by asm_simp;
  11.216 +    show "x = x [+] <0>"; by (simp!);
  11.217 +    show "<0> : V"; by (simp!);
  11.218    qed;
  11.219    show "ALL x:U. ALL y:U. x [+] y : U"; 
  11.220    proof (intro ballI);
  11.221 -    fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by asm_simp;
  11.222 +    fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!);
  11.223    qed;
  11.224    show "ALL x:U. ALL a. a [*] x : U"; 
  11.225    proof (intro ballI allI);
  11.226 -    fix x a; assume "x:U"; show "a [*] x : U"; by asm_simp;
  11.227 +    fix x a; assume "x:U"; show "a [*] x : U"; by (simp!);
  11.228    qed;
  11.229  qed;
  11.230  
  11.231 -lemma vs_sum_subspace: 
  11.232 -  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_subspace (vectorspace_sum U V) E";
  11.233 -proof (rule subspace_I);
  11.234 -  assume u: "is_subspace U E" and v: "is_subspace V E" and e: "is_vectorspace E";
  11.235 +lemma vs_sum_subspace [intro!!]: 
  11.236 +  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
  11.237 +  ==> is_subspace (vectorspace_sum U V) E";
  11.238 +proof; 
  11.239 +  assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
  11.240  
  11.241    show "<0> : vectorspace_sum U V";
  11.242 -  by (intro vs_sum_I, rule vs_add_zero_left [RS sym], 
  11.243 -      rule zero_in_subspace, rule zero_in_subspace, rule zero_in_vs); 
  11.244 -
  11.245 +  proof (intro vs_sumI);
  11.246 +    show "<0> : U"; ..;
  11.247 +    show "<0> : V"; ..;
  11.248 +    show "(<0>::'a) = <0> [+] <0>"; 
  11.249 +      by (simp!);
  11.250 +  qed;
  11.251 +  
  11.252    show "vectorspace_sum U V <= E";
  11.253 -  proof (intro subsetI, elim vs_sumD [RS iffD1, elimify] bexE);
  11.254 +  proof (intro subsetI, elim vs_sumE bexE);
  11.255      fix x u v; assume "u : U" "v : V" "x = u [+] v";
  11.256 -    show "x:E"; by (asm_simp);
  11.257 +    show "x:E"; by (simp!);
  11.258    qed;
  11.259    
  11.260    show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
  11.261 -  proof (intro ballI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
  11.262 -    fix x y ux vx uy vy; assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
  11.263 -    show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by asm_simp;
  11.264 -  qed asm_simp+;
  11.265 +  proof (intro ballI);
  11.266 +    fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
  11.267 +    thus "x [+] y : vectorspace_sum U V";
  11.268 +    proof (elim vs_sumE bexE, intro vs_sumI);
  11.269 +      fix ux vx uy vy; 
  11.270 +      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
  11.271 +      show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
  11.272 +    qed (simp!)+;
  11.273 +  qed;
  11.274  
  11.275    show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
  11.276 -  proof (intro ballI allI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
  11.277 -    fix a x u v; assume "u : U" "v : V" "x = u [+] v";
  11.278 -    show "a [*] x = (a [*] u) [+] (a [*] v)"; by (asm_simp add: vs_add_mult_distrib1 [OF e]);
  11.279 -  qed asm_simp+;
  11.280 +  proof (intro ballI allI);
  11.281 +    fix x a; assume "x:vectorspace_sum U V";
  11.282 +    thus "a [*] x : vectorspace_sum U V";
  11.283 +    proof (elim vs_sumE bexE, intro vs_sumI);
  11.284 +      fix a x u v; assume "u : U" "v : V" "x = u [+] v";
  11.285 +      show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1);
  11.286 +    qed (simp!)+;
  11.287 +  qed;
  11.288  qed;
  11.289  
  11.290 -lemma vs_sum_vs: 
  11.291 -  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_vectorspace (vectorspace_sum U V)";
  11.292 -  by (rule subspace_vs [OF vs_sum_subspace]);
  11.293 +lemma vs_sum_vs [intro!!]: 
  11.294 +  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
  11.295 +  ==> is_vectorspace (vectorspace_sum U V)";
  11.296 +proof (rule subspace_vs);
  11.297 +  assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
  11.298 +  show "is_subspace (vectorspace_sum U V) E"; ..;
  11.299 +qed;
  11.300  
  11.301  
  11.302  section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
  11.303  
  11.304 -
  11.305 -lemma lemma4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
  11.306 +lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
  11.307    x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
  11.308    ==> y1 = y2 & a1 = a2";
  11.309  proof;
  11.310    assume "is_vectorspace E" "is_subspace H E"
  11.311           "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
  11.312           "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
  11.313 -  have h: "is_vectorspace H"; by (rule subspace_vs);
  11.314 -  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0"; 
  11.315 -    by (rule vs_add_diff_swap) asm_simp+;
  11.316 +  have h: "is_vectorspace H"; ..;
  11.317 +  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
  11.318 +    by (simp! add: vs_add_diff_swap);
  11.319    also; have "... = (a2 - a1) [*] x0";
  11.320      by (rule vs_diff_mult_distrib2 [RS sym]);
  11.321    finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
  11.322  
  11.323 -  have y: "y1 [-] y2 : H"; by asm_simp;
  11.324 -  have x: "(a2 - a1) [*] x0 : lin x0"; by (asm_simp add: lin_def) force; 
  11.325 -  from y; have y': "y1 [-] y2 : lin x0"; by (simp only: eq x);
  11.326 -  from x; have x': "(a2 - a1) [*] x0 : H"; by (simp only: eq [RS sym] y);
  11.327 +  have y: "y1 [-] y2 : H"; by (simp!);
  11.328 +  have x: "(a2 - a1) [*] x0 : lin x0"; by (simp! add: lin_def) force; 
  11.329 +  from eq y x; have y': "y1 [-] y2 : lin x0"; by simp;
  11.330 +  from eq y x; have x': "(a2 - a1) [*] x0 : H"; by simp;
  11.331  
  11.332    have int: "H Int (lin x0) = {<0>}"; 
  11.333    proof;
  11.334      show "H Int lin x0 <= {<0>}"; 
  11.335 -    proof (intro subsetI, unfold lin_def, elim IntE CollectD[elimify] exE,
  11.336 -      rule singleton_iff[RS iffD2]);
  11.337 -      fix x a; assume "x : H" and ax0: "x = a [*] x0";
  11.338 -      show "x = <0>";
  11.339 -      proof (rule case [of "a=0r"]);
  11.340 -        assume "a = 0r"; show ?thesis; by asm_simp;
  11.341 -      next;
  11.342 -        assume "a ~= 0r"; 
  11.343 -        have "(rinv a) [*] a [*] x0 : H"; 
  11.344 -          by (rule vs_mult_closed [OF h]) asm_simp;
  11.345 -        also; have "(rinv a) [*] a [*] x0 = x0"; by asm_simp;
  11.346 -        finally; have "x0 : H"; .;
  11.347 -        thus ?thesis; by contradiction;
  11.348 -      qed;
  11.349 +    proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
  11.350 +      fix x; assume "x:H" "x:lin x0"; 
  11.351 +      thus "x = <0>";
  11.352 +      proof (-, unfold lin_def, elim CollectE exE);
  11.353 +        fix a; assume "x = a [*] x0";
  11.354 +        show ?thesis;
  11.355 +        proof (rule case [of "a = 0r"]);
  11.356 +          assume "a = 0r"; show ?thesis; by (simp!);
  11.357 +        next;
  11.358 +          assume "a ~= 0r"; 
  11.359 +          have "(rinv a) [*] a [*] x0 : H"; 
  11.360 +            by (rule vs_mult_closed [OF h]) (simp!);
  11.361 +          also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
  11.362 +          finally; have "x0 : H"; .;
  11.363 +          thus ?thesis; by contradiction;
  11.364 +        qed;
  11.365 +     qed;
  11.366      qed;
  11.367 -    show "{<0>} <= H Int lin x0"; 
  11.368 -    proof (intro subsetI, elim singletonD[elimify], intro IntI, asm_simp+);
  11.369 -      show "<0> : H"; by (rule zero_in_vs [OF h]);
  11.370 -      show "<0> : lin x0"; by (rule zero_in_vs [OF lin_vs]);
  11.371 +    show "{<0>} <= H Int lin x0";
  11.372 +    proof (intro subsetI, elim singletonE, intro IntI, simp+);
  11.373 +      show "<0> : H"; ..;
  11.374 +      from lin_vs; show "<0> : lin x0"; ..;
  11.375      qed;
  11.376    qed;
  11.377  
  11.378    from h; show "y1 = y2";
  11.379    proof (rule vs_add_minus_eq);
  11.380 -    show "y1 [-] y2 = <0>";
  11.381 -      by (rule Int_singeltonD [OF int y y']); 
  11.382 +    show "y1 [-] y2 = <0>"; 
  11.383 +      by (rule Int_singletonD [OF int y y']); 
  11.384    qed;
  11.385   
  11.386    show "a1 = a2";
  11.387    proof (rule real_add_minus_eq [RS sym]);
  11.388      show "a2 - a1 = 0r";
  11.389      proof (rule vs_mult_zero_uniq);
  11.390 -      show "(a2 - a1) [*] x0 = <0>";  by (rule Int_singeltonD [OF int x' x]);
  11.391 +      show "(a2 - a1) [*] x0 = <0>";  by (rule Int_singletonD [OF int x' x]);
  11.392      qed;
  11.393    qed;
  11.394  qed;
  11.395  
  11.396   
  11.397 -lemma lemma1: 
  11.398 +lemma decomp1: 
  11.399    "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] 
  11.400    ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
  11.401  proof (rule, unfold split_paired_all);
  11.402    assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
  11.403 -  have h: "is_vectorspace H"; by (rule subspace_vs);
  11.404 +  have h: "is_vectorspace H"; ..;
  11.405    fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
  11.406    have "y = t & a = 0r"; 
  11.407 -    by (rule lemma4) (assumption+, asm_simp); 
  11.408 -  thus "(y, a) = (t, 0r)"; by asm_simp;
  11.409 -qed asm_simp+;
  11.410 +    by (rule decomp4) (assumption+, (simp!)); 
  11.411 +  thus "(y, a) = (t, 0r)"; by (simp!);
  11.412 +qed (simp!)+;
  11.413  
  11.414  
  11.415 -lemma lemma3: "!! x0 h xi x y a H. [| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
  11.416 -                            in (h y) + a * xi);
  11.417 -                  x = y [+] a [*] x0; 
  11.418 -                  is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
  11.419 +lemma decomp3:
  11.420 +  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
  11.421 +                in (h y) + a * xi);
  11.422 +      x = y [+] a [*] x0; 
  11.423 +      is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
  11.424    ==> h0 x = h y + a * xi";
  11.425  proof -;  
  11.426 -  fix x0 h xi x y a H;
  11.427    assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
  11.428 -                            in (h y) + a * xi)";
  11.429 +                    in (h y) + a * xi)";
  11.430    assume "x = y [+] a [*] x0";
  11.431    assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
  11.432  
  11.433    have "x : vectorspace_sum H (lin x0)"; 
  11.434 -    by (asm_simp add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
  11.435 +    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
  11.436    have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
  11.437    proof;
  11.438 -    show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
  11.439 -      by (asm_simp, rule exI, force);
  11.440 +    show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
  11.441 +      by (force!);
  11.442    next;
  11.443      fix xa ya;
  11.444      assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
  11.445 @@ -300,18 +333,18 @@
  11.446      show "xa = ya"; ;
  11.447      proof -;
  11.448        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
  11.449 -        by(rule Pair_fst_snd_eq [RS iffD2]);
  11.450 -      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by force;
  11.451 -      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by force;
  11.452 +        by (rule Pair_fst_snd_eq [RS iffD2]);
  11.453 +      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!);
  11.454 +      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!);
  11.455        from x y; show "fst xa = fst ya & snd xa = snd ya"; 
  11.456 -        by (elim conjE) (rule lemma4, asm_simp+);
  11.457 +        by (elim conjE) (rule decomp4, (simp!)+);
  11.458      qed;
  11.459    qed;
  11.460    hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
  11.461 -    by (rule select1_equality, force);
  11.462 +    by (rule select1_equality) (force!);
  11.463    thus "h0 x = h y + a * xi"; 
  11.464 -    by (asm_simp add: Let_def);
  11.465 -qed;  
  11.466 +    by (simp! add: Let_def);
  11.467 +qed;
  11.468  
  11.469  
  11.470  end;
    12.1 --- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy	Tue Sep 21 17:30:55 1999 +0200
    12.2 +++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy	Tue Sep 21 17:31:20 1999 +0200
    12.3 @@ -1,5 +1,9 @@
    12.4 +(*  Title:      HOL/Real/HahnBanach/Zorn_Lemma.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Gertrud Bauer, TU Munich
    12.7 +*)
    12.8  
    12.9 -theory Zorn_Lemma = Zorn:;
   12.10 +theory Zorn_Lemma = Aux + Zorn:;
   12.11  
   12.12  
   12.13  lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==>
   12.14 @@ -15,12 +19,12 @@
   12.15      show "EX y:S. ALL z:c. z <= y";
   12.16      proof (rule case [of "c={}"]);
   12.17        assume "c={}"; 
   12.18 -      show ?thesis; by fast;
   12.19 +      show ?thesis; by (fast!);
   12.20      next;
   12.21        assume "c~={}";
   12.22        show ?thesis; 
   12.23        proof;
   12.24 -        have "EX x. x:c"; by fast;
   12.25 +        have "EX x. x:c"; by (fast!);
   12.26          thus "Union c : S"; by (rule s);
   12.27          show "ALL z:c. z <= Union c"; by fast;
   12.28        qed;