renamed 'RS' to 'THEN';
authorwenzelm
Thu Aug 17 10:35:49 2000 +0200 (2000-08-17)
changeset 96233ade112482af
parent 9622 d9aa8ca06bc2
child 9624 de254f375477
renamed 'RS' to 'THEN';
'symmetric' attribute;
src/HOL/Real/HahnBanach/FunctionOrder.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Aug 17 10:34:52 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Aug 17 10:35:49 2000 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4    show "\<exists>y. (a, y) \<in> g" ..
     1.5    assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
     1.6    show "b = (SOME y. (a, y) \<in> g)"
     1.7 -  proof (rule select_equality [RS sym])
     1.8 +  proof (rule select_equality [symmetric])
     1.9      fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
    1.10    qed
    1.11  qed
     2.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 17 10:34:52 2000 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 17 10:35:49 2000 +0200
     2.3 @@ -271,7 +271,7 @@
     2.4                    by (simp add: Let_def)
     2.5                  also have 
     2.6                    "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
     2.7 -                  by (rule decomp_H'_H [RS sym]) (simp! add: x')+
     2.8 +                  by (rule decomp_H'_H [symmetric]) (simp! add: x')+
     2.9                  also have 
    2.10                    "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
    2.11                      in h y + a * xi) = h' x" by (simp!)
    2.12 @@ -328,7 +328,7 @@
    2.13  proof -
    2.14  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
    2.15  "is_linearform F f"  "\<forall>x \<in> F. |f x| <= p x"
    2.16 -have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
    2.17 +have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [THEN iffD1])
    2.18  hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
    2.19            \<and> (\<forall>x \<in> E. g x <= p x)"
    2.20  by (simp! only: HahnBanach)
     3.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 17 10:34:52 2000 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 17 10:35:49 2000 +0200
     3.3 @@ -185,9 +185,9 @@
     3.4        also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
     3.5          by simp;
     3.6        also; have "h y1 + a1 * xi = h' x1";
     3.7 -        by (rule h'_definite [RS sym]);
     3.8 +        by (rule h'_definite [symmetric]);
     3.9        also; have "h y2 + a2 * xi = h' x2"; 
    3.10 -        by (rule h'_definite [RS sym]);
    3.11 +        by (rule h'_definite [symmetric]);
    3.12        finally; show ?thesis; .;
    3.13      qed;
    3.14   
    3.15 @@ -229,7 +229,7 @@
    3.16        also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
    3.17  	by (simp add: real_add_mult_distrib2 real_mult_assoc);
    3.18        also; have "h y1 + a1 * xi = h' x1"; 
    3.19 -        by (rule h'_definite [RS sym]);
    3.20 +        by (rule h'_definite [symmetric]);
    3.21        finally; show ?thesis; .;
    3.22      qed;
    3.23    qed;
    3.24 @@ -300,7 +300,7 @@
    3.25        also; from nz vs y; have "... = p (y + a \<cdot> x0)";
    3.26          by (simp add: vs_add_mult_distrib1);
    3.27        also; from nz vs y; have "a * (h (rinv a \<cdot> y)) =  h y";
    3.28 -        by (simp add: linearform_mult [RS sym]);
    3.29 +        by (simp add: linearform_mult [symmetric]);
    3.30        finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
    3.31  
    3.32        hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y";
    3.33 @@ -329,7 +329,7 @@
    3.34        also; from nz vs y; have "... = p (y + a \<cdot> x0)";
    3.35          by (simp add: vs_add_mult_distrib1);
    3.36        also; from nz vs y; have "a * h (rinv a \<cdot> y) = h y";
    3.37 -        by (simp add: linearform_mult [RS sym]); 
    3.38 +        by (simp add: linearform_mult [symmetric]); 
    3.39        finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
    3.40   
    3.41        hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)";
     4.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 17 10:34:52 2000 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 17 10:35:49 2000 +0200
     4.3 @@ -333,7 +333,7 @@
     4.4        also assume "graph G g = x"
     4.5        also have "... \<in> c" .
     4.6        hence "x \<subseteq> \<Union>c" by fast
     4.7 -      also have [RS sym]: "graph H h = \<Union>c" .
     4.8 +      also have [symmetric]: "graph H h = \<Union>c" .
     4.9        finally show ?thesis .
    4.10      qed
    4.11    qed
    4.12 @@ -476,7 +476,7 @@
    4.13      fix H' h' 
    4.14      assume "x \<in> H'" "graph H' h' \<subseteq> graph H h" 
    4.15        and a: "\<forall>x \<in> H'. h' x <= p x"
    4.16 -    have [RS sym]: "h' x = h x" ..
    4.17 +    have [symmetric]: "h' x = h x" ..
    4.18      also from a have "h' x <= p x " ..
    4.19      finally show ?thesis .  
    4.20    qed
    4.21 @@ -522,7 +522,7 @@
    4.22        show "- p x <= h x"
    4.23        proof (rule real_minus_le)
    4.24  	from h have "- h x = h (- x)"
    4.25 -          by (rule linearform_neg [RS sym])
    4.26 +          by (rule linearform_neg [symmetric])
    4.27  	also from r have "... <= p (- x)" by (simp!)
    4.28  	also have "... = p x" 
    4.29          proof (rule seminorm_minus)
     5.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 17 10:34:52 2000 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 17 10:35:49 2000 +0200
     5.3 @@ -227,7 +227,7 @@
     5.4    "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
     5.5      by (unfold vs_sum_def) fast
     5.6  
     5.7 -lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
     5.8 +lemmas vs_sumE = vs_sumD [THEN iffD1, elimify, standard]
     5.9  
    5.10  lemma vs_sumI [intro?]: 
    5.11    "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
    5.12 @@ -343,7 +343,7 @@
    5.13    qed
    5.14  
    5.15    show "v1 = v2"
    5.16 -  proof (rule vs_add_minus_eq [RS sym])
    5.17 +  proof (rule vs_add_minus_eq [symmetric])
    5.18      show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
    5.19      show "v1 \<in> E" ..
    5.20      show "v2 \<in> E" ..
    5.21 @@ -372,7 +372,7 @@
    5.22      show "H \<inter> (lin x') = {0}" 
    5.23      proof
    5.24        show "H \<inter> lin x' <= {0}" 
    5.25 -      proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2])
    5.26 +      proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2])
    5.27          fix x assume "x \<in> H" "x \<in> lin x'" 
    5.28          thus "x = 0"
    5.29          proof (unfold lin_def, elim CollectE exE conjE)
    5.30 @@ -406,7 +406,7 @@
    5.31    from c show "y1 = y2" by simp
    5.32    
    5.33    show  "a1 = a2" 
    5.34 -  proof (rule vs_mult_right_cancel [RS iffD1])
    5.35 +  proof (rule vs_mult_right_cancel [THEN iffD1])
    5.36      from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
    5.37    qed
    5.38  qed
     6.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Aug 17 10:34:52 2000 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Aug 17 10:35:49 2000 +0200
     6.3 @@ -292,11 +292,11 @@
     6.4  
     6.5  lemma vs_add_minus_cancel [simp]:  
     6.6    "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y" 
     6.7 -  by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
     6.8 +  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 
     6.9  
    6.10  lemma vs_minus_add_cancel [simp]: 
    6.11    "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y" 
    6.12 -  by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
    6.13 +  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 
    6.14  
    6.15  lemma vs_minus_add_distrib [simp]:  
    6.16    "[| is_vectorspace V; x \<in> V; y \<in> V |] 
    6.17 @@ -323,7 +323,7 @@
    6.18      by (simp! only: vs_add_assoc vs_neg_closed)
    6.19    also assume "x + y = x + z"
    6.20    also have "- x + (x + z) = - x + x + z" 
    6.21 -    by (simp! only: vs_add_assoc [RS sym] vs_neg_closed)
    6.22 +    by (simp! only: vs_add_assoc [symmetric] vs_neg_closed)
    6.23    also have "... = z" by (simp!)
    6.24    finally show ?R .
    6.25  qed force
    6.26 @@ -336,7 +336,7 @@
    6.27  lemma vs_add_assoc_cong: 
    6.28    "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |] 
    6.29    ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
    6.30 -  by (simp only: vs_add_assoc [RS sym]) 
    6.31 +  by (simp only: vs_add_assoc [symmetric]) 
    6.32  
    6.33  lemma vs_mult_left_commute: 
    6.34    "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
    6.35 @@ -504,7 +504,7 @@
    6.36    proof
    6.37      assume l: ?L
    6.38      have "x + z = 0" 
    6.39 -    proof (rule vs_add_left_cancel [RS iffD1])
    6.40 +    proof (rule vs_add_left_cancel [THEN iffD1])
    6.41        have "y + (x + z) = x + (y + z)" by (simp!)
    6.42        also note l
    6.43        also have "y = y + 0" by (simp!)