src/HOL/Real/HahnBanach/Linearform.thy

--- a/src/HOL/Real/HahnBanach/Linearform.thy	Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Tue Sep 21 17:31:20 1999 +0200
@@ -1,3 +1,7 @@
+(*  Title:      HOL/Real/HahnBanach/Linearform.thy
+    ID:         $Id$
+    Author:     Gertrud Bauer, TU Munich
+*)
 
 theory Linearform = LinearSpace:;
 
@@ -12,39 +16,41 @@
 lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
     !! x c. x : V ==> f (c [*] x) = c * f x |]
  ==> is_linearform V f";
- by (unfold is_linearform_def, force);
+ by (unfold is_linearform_def) force;
 
-lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
- by (unfold is_linearform_def, auto);
+lemma linearform_add_linear [intro!!]: 
+  "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
+  by (unfold is_linearform_def) auto;
 
-lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
- by (unfold is_linearform_def, auto);
+lemma linearform_mult_linear [intro!!]: 
+  "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
+  by (unfold is_linearform_def) auto;
 
-lemma linearform_neg_linear:
+lemma linearform_neg_linear [intro!!]:
   "[|  is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
 proof -; 
   assume "is_linearform V f" "is_vectorspace V" "x:V"; 
-  have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1);
+  have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);
   also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
-  also; have "... = - (f x)"; by asm_simp;
+  also; have "... = - (f x)"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
-lemma linearform_diff_linear: 
+lemma linearform_diff_linear [intro!!]: 
   "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";  
 proof -;
   assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
   have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
-  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+);
+  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;
   also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
-  finally; show "f (x [-] y) = f x - f y"; by asm_simp;
+  finally; show "f (x [-] y) = f x - f y"; by (simp!);
 qed;
 
-lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
+lemma linearform_zero [intro!!]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
 proof -; 
   assume "is_vectorspace V" "is_linearform V f";
-  have "f <0> = f (<0> [-] <0>)"; by asm_simp;
-  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+;
+  have "f <0> = f (<0> [-] <0>)"; by (simp!);
+  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;
   also; have "... = 0r"; by simp;
   finally; show "f <0> = 0r"; .;
 qed;