src/HOL/Real/HahnBanach/Linearform.thy
changeset 10687 c186279eecea
parent 9408 d3d56e1d2ec1
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Sat Dec 16 21:41:14 2000 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Sat Dec 16 21:41:51 2000 +0100
     1.3 @@ -7,63 +7,65 @@
     1.4  
     1.5  theory Linearform = VectorSpace:
     1.6  
     1.7 -text{* A \emph{linear form} is a function on a vector
     1.8 -space into the reals that is additive and multiplicative. *}
     1.9 +text {*
    1.10 +  A \emph{linear form} is a function on a vector space into the reals
    1.11 +  that is additive and multiplicative.
    1.12 +*}
    1.13  
    1.14  constdefs
    1.15 -  is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool" 
    1.16 -  "is_linearform V f == 
    1.17 +  is_linearform :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
    1.18 +  "is_linearform V f \<equiv>
    1.19        (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
    1.20 -      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))" 
    1.21 +      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"
    1.22  
    1.23 -lemma is_linearformI [intro]: 
    1.24 -  "[| !! x y. [| x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y;
    1.25 -    !! x c. x \<in> V ==> f (c \<cdot> x) = c * f x |]
    1.26 - ==> is_linearform V f"
    1.27 - by (unfold is_linearform_def) force
    1.28 +lemma is_linearformI [intro]:
    1.29 +  "(\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y) \<Longrightarrow>
    1.30 +    (\<And>x c. x \<in> V \<Longrightarrow> f (c \<cdot> x) = c * f x)
    1.31 + \<Longrightarrow> is_linearform V f"
    1.32 + by (unfold is_linearform_def) blast
    1.33  
    1.34 -lemma linearform_add [intro?]: 
    1.35 -  "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
    1.36 -  by (unfold is_linearform_def) fast
    1.37 +lemma linearform_add [intro?]:
    1.38 +  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
    1.39 +  by (unfold is_linearform_def) blast
    1.40  
    1.41 -lemma linearform_mult [intro?]: 
    1.42 -  "[| is_linearform V f; x \<in> V |] ==>  f (a \<cdot> x) = a * (f x)" 
    1.43 -  by (unfold is_linearform_def) fast
    1.44 +lemma linearform_mult [intro?]:
    1.45 +  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow>  f (a \<cdot> x) = a * (f x)"
    1.46 +  by (unfold is_linearform_def) blast
    1.47  
    1.48  lemma linearform_neg [intro?]:
    1.49 -  "[|  is_vectorspace V; is_linearform V f; x \<in> V|] 
    1.50 -  ==> f (- x) = - f x"
    1.51 -proof - 
    1.52 -  assume "is_linearform V f" "is_vectorspace V" "x \<in> V"
    1.53 +  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V
    1.54 +  \<Longrightarrow> f (- x) = - f x"
    1.55 +proof -
    1.56 +  assume "is_linearform V f"  "is_vectorspace V"  "x \<in> V"
    1.57    have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
    1.58    also have "... = (- #1) * (f x)" by (rule linearform_mult)
    1.59    also have "... = - (f x)" by (simp!)
    1.60    finally show ?thesis .
    1.61  qed
    1.62  
    1.63 -lemma linearform_diff [intro?]: 
    1.64 -  "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] 
    1.65 -  ==> f (x - y) = f x - f y"  
    1.66 +lemma linearform_diff [intro?]:
    1.67 +  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
    1.68 +  \<Longrightarrow> f (x - y) = f x - f y"
    1.69  proof -
    1.70 -  assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V"
    1.71 +  assume "is_vectorspace V"  "is_linearform V f"  "x \<in> V"  "y \<in> V"
    1.72    have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
    1.73 -  also have "... = f x + f (- y)" 
    1.74 +  also have "... = f x + f (- y)"
    1.75      by (rule linearform_add) (simp!)+
    1.76    also have "f (- y) = - f y" by (rule linearform_neg)
    1.77    finally show "f (x - y) = f x - f y" by (simp!)
    1.78  qed
    1.79  
    1.80 -text{* Every linear form yields $0$ for the $\zero$ vector.*}
    1.81 +text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
    1.82  
    1.83 -lemma linearform_zero [intro?, simp]: 
    1.84 -  "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
    1.85 -proof - 
    1.86 -  assume "is_vectorspace V" "is_linearform V f"
    1.87 +lemma linearform_zero [intro?, simp]:
    1.88 +  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = #0"
    1.89 +proof -
    1.90 +  assume "is_vectorspace V"  "is_linearform V f"
    1.91    have "f 0 = f (0 - 0)" by (simp!)
    1.92 -  also have "... = f 0 - f 0" 
    1.93 +  also have "... = f 0 - f 0"
    1.94      by (rule linearform_diff) (simp!)+
    1.95    also have "... = #0" by simp
    1.96    finally show "f 0 = #0" .
    1.97 -qed 
    1.98 +qed
    1.99  
   1.100 -end
   1.101 \ No newline at end of file
   1.102 +end