src/HOL/Real/HahnBanach/Subspace.thy
changeset 9408 d3d56e1d2ec1
parent 9374 153853af318b
child 9623 3ade112482af
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 23 11:59:21 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 23 12:01:05 2000 +0200
     1.3 @@ -28,25 +28,25 @@
     1.4    assume "0 \<in> U" thus "U \<noteq> {}" by fast
     1.5  qed (simp+)
     1.6  
     1.7 -lemma subspace_not_empty [intro??]: "is_subspace U V ==> U \<noteq> {}"
     1.8 +lemma subspace_not_empty [intro?]: "is_subspace U V ==> U \<noteq> {}"
     1.9    by (unfold is_subspace_def) simp 
    1.10  
    1.11 -lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"
    1.12 +lemma subspace_subset [intro?]: "is_subspace U V ==> U <= V"
    1.13    by (unfold is_subspace_def) simp
    1.14  
    1.15 -lemma subspace_subsetD [simp, intro??]: 
    1.16 +lemma subspace_subsetD [simp, intro?]: 
    1.17    "[| is_subspace U V; x \<in> U |] ==> x \<in> V"
    1.18    by (unfold is_subspace_def) force
    1.19  
    1.20 -lemma subspace_add_closed [simp, intro??]: 
    1.21 +lemma subspace_add_closed [simp, intro?]: 
    1.22    "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U"
    1.23    by (unfold is_subspace_def) simp
    1.24  
    1.25 -lemma subspace_mult_closed [simp, intro??]: 
    1.26 +lemma subspace_mult_closed [simp, intro?]: 
    1.27    "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U"
    1.28    by (unfold is_subspace_def) simp
    1.29  
    1.30 -lemma subspace_diff_closed [simp, intro??]: 
    1.31 +lemma subspace_diff_closed [simp, intro?]: 
    1.32    "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |] 
    1.33    ==> x - y \<in> U"
    1.34    by (simp! add: diff_eq1 negate_eq1)
    1.35 @@ -55,7 +55,7 @@
    1.36  zero element in every subspace follows from the non-emptiness 
    1.37  of the carrier set and by vector space laws.*}
    1.38  
    1.39 -lemma zero_in_subspace [intro??]:
    1.40 +lemma zero_in_subspace [intro?]:
    1.41    "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U"
    1.42  proof - 
    1.43    assume "is_subspace U V" and v: "is_vectorspace V"
    1.44 @@ -71,14 +71,14 @@
    1.45    qed
    1.46  qed
    1.47  
    1.48 -lemma subspace_neg_closed [simp, intro??]: 
    1.49 +lemma subspace_neg_closed [simp, intro?]: 
    1.50    "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U"
    1.51    by (simp add: negate_eq1)
    1.52  
    1.53  text_raw {* \medskip *}
    1.54  text {* Further derived laws: every subspace is a vector space. *}
    1.55  
    1.56 -lemma subspace_vs [intro??]:
    1.57 +lemma subspace_vs [intro?]:
    1.58    "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"
    1.59  proof -
    1.60    assume "is_subspace U V" "is_vectorspace V"
    1.61 @@ -144,7 +144,7 @@
    1.62  lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
    1.63    by (unfold lin_def) fast
    1.64  
    1.65 -lemma linI [intro??]: "a \<cdot> x0 \<in> lin x0"
    1.66 +lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0"
    1.67    by (unfold lin_def) fast
    1.68  
    1.69  text {* Every vector is contained in its linear closure. *}
    1.70 @@ -157,7 +157,7 @@
    1.71  
    1.72  text {* Any linear closure is a subspace. *}
    1.73  
    1.74 -lemma lin_subspace [intro??]: 
    1.75 +lemma lin_subspace [intro?]: 
    1.76    "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V"
    1.77  proof
    1.78    assume "is_vectorspace V" "x \<in> V"
    1.79 @@ -198,7 +198,7 @@
    1.80  
    1.81  text {* Any linear closure is a vector space. *}
    1.82  
    1.83 -lemma lin_vs [intro??]: 
    1.84 +lemma lin_vs [intro?]: 
    1.85    "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)"
    1.86  proof (rule subspace_vs)
    1.87    assume "is_vectorspace V" "x \<in> V"
    1.88 @@ -229,13 +229,13 @@
    1.89  
    1.90  lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
    1.91  
    1.92 -lemma vs_sumI [intro??]: 
    1.93 +lemma vs_sumI [intro?]: 
    1.94    "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
    1.95    by (unfold vs_sum_def) fast
    1.96  
    1.97  text{* $U$ is a subspace of $U + V$. *}
    1.98  
    1.99 -lemma subspace_vs_sum1 [intro??]: 
   1.100 +lemma subspace_vs_sum1 [intro?]: 
   1.101    "[| is_vectorspace U; is_vectorspace V |]
   1.102    ==> is_subspace U (U + V)"
   1.103  proof 
   1.104 @@ -259,7 +259,7 @@
   1.105  
   1.106  text{* The sum of two subspaces is again a subspace.*}
   1.107  
   1.108 -lemma vs_sum_subspace [intro??]: 
   1.109 +lemma vs_sum_subspace [intro?]: 
   1.110    "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   1.111    ==> is_subspace (U + V) E"
   1.112  proof 
   1.113 @@ -303,7 +303,7 @@
   1.114  
   1.115  text{* The sum of two subspaces is a vectorspace. *}
   1.116  
   1.117 -lemma vs_sum_vs [intro??]: 
   1.118 +lemma vs_sum_vs [intro?]: 
   1.119    "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   1.120    ==> is_vectorspace (U + V)"
   1.121  proof (rule subspace_vs)