src/HOL/Real/HahnBanach/Subspace.thy
changeset 8203 2fcc6017cb72
parent 8169 77b3bc101de5
child 8280 259073d16f84
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Feb 07 15:28:43 2000 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Feb 07 18:38:51 2000 +0100
     1.3 @@ -28,25 +28,25 @@
     1.4    assume "<0> : U"; thus "U ~= {}"; by fast;
     1.5  qed (simp+);
     1.6  
     1.7 -lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
     1.8 +lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}";
     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:U |] ==> x: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:U; y:U |] ==> x + y : 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:U |] ==> a <*> x : 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:U; y:U |] 
    1.33    ==> x - y : 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> : 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:U |] ==> - x : 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 : lin v = (EX a::real. x = a <*> v)";
    1.63    by (unfold lin_def) fast;
    1.64  
    1.65 -lemma linI [intro!!]: "a <*> x0 : lin x0";
    1.66 +lemma linI [intro??]: "a <*> x0 : 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:V |] ==> is_subspace (lin x) V";
    1.77  proof;
    1.78    assume "is_vectorspace V" "x: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:V |] ==> is_vectorspace (lin x)";
    1.86  proof (rule subspace_vs);
    1.87    assume "is_vectorspace V" "x: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:U; y:V; t= x + y |] ==> t : 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);