Updated files to remove 0r and 1r from theorems in descendant theories
authorfleuriot
Thu Jun 01 11:22:27 2000 +0200 (2000-06-01)
changeset 90139dd0274f76af
parent 9012 d1bd2144ab5d
child 9014 4382883421ec
Updated files to remove 0r and 1r from theorems in descendant theories
of RealBin. Some new theorems added.
src/HOL/Real/HahnBanach/Aux.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/HyperDef.thy
src/HOL/Real/RComplete.ML
src/HOL/Real/ROOT.ML
src/HOL/Real/RealAbs.ML
src/HOL/Real/RealAbs.thy
src/HOL/Real/RealBin.ML
src/HOL/Real/RealOrd.ML
src/HOL/Real/RealOrd.thy
src/HOL/Real/RealPow.ML
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Wed May 31 18:06:02 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Thu Jun 01 11:22:27 2000 +0200
     1.3 @@ -53,58 +53,83 @@
     1.4  text_raw {* \medskip *};
     1.5  text{* Some lemmas for the reals. *};
     1.6  
     1.7 -lemma real_add_minus_eq: "x - y = 0r ==> x = y";
     1.8 -proof -;
     1.9 -  assume "x - y = 0r";
    1.10 -  have "x + - y = 0r"; by (simp!);
    1.11 -  hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
    1.12 -  also; have "... = y"; by simp;
    1.13 -  finally; show "?thesis"; .;
    1.14 -qed;
    1.15 +lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y";
    1.16 +  by simp;
    1.17 +
    1.18 +lemma abs_minus_one: "abs (- (#1::real)) = #1"; 
    1.19 +  by simp;
    1.20 +
    1.21  
    1.22 -lemma abs_minus_one: "abs (- 1r) = 1r"; 
    1.23 -proof -; 
    1.24 -  have "-1r < 0r"; 
    1.25 -    by (rule real_minus_zero_less_iff[RS iffD1], simp, 
    1.26 -        rule real_zero_less_one);
    1.27 -  hence "abs (- 1r) = - (- 1r)"; 
    1.28 -    by (rule abs_minus_eqI2);
    1.29 -  also; have "... = 1r"; by simp; 
    1.30 -  finally; show ?thesis; .;
    1.31 +lemma real_mult_le_le_mono1a: 
    1.32 +  "[| (#0::real) <= z; x <= y |] ==> z * x  <= z * y";
    1.33 +proof -;
    1.34 +  assume "(#0::real) <= z" "x <= y";
    1.35 +  hence "x < y | x = y"; by (force simp add: order_le_less);
    1.36 +  thus ?thesis;
    1.37 +  proof (elim disjE); 
    1.38 +   assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono2) simp;
    1.39 +  next; 
    1.40 +   assume "x = y"; thus ?thesis;; by simp;
    1.41 +  qed;
    1.42  qed;
    1.43  
    1.44  lemma real_mult_le_le_mono2: 
    1.45 -  "[| 0r <= z; x <= y |] ==> x * z <= y * z";
    1.46 +  "[| (#0::real) <= z; x <= y |] ==> x * z <= y * z";
    1.47  proof -;
    1.48 -  assume "0r <= z" "x <= y";
    1.49 +  assume "(#0::real) <= z" "x <= y";
    1.50    hence "x < y | x = y"; by (force simp add: order_le_less);
    1.51    thus ?thesis;
    1.52    proof (elim disjE); 
    1.53 -    assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1);
    1.54 +   assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1) simp;
    1.55    next; 
    1.56 -    assume "x = y"; thus ?thesis;; by simp;
    1.57 +   assume "x = y"; thus ?thesis;; by simp;
    1.58    qed;
    1.59  qed;
    1.60  
    1.61  lemma real_mult_less_le_anti: 
    1.62 -  "[| z < 0r; x <= y |] ==> z * y <= z * x";
    1.63 +  "[| z < (#0::real); x <= y |] ==> z * y <= z * x";
    1.64  proof -;
    1.65 -  assume "z < 0r" "x <= y";
    1.66 -  hence "0r < - z"; by simp;
    1.67 -  hence "0r <= - z"; by (rule real_less_imp_le);
    1.68 -  hence "(- z) * x <= (- z) * y"; 
    1.69 -    by (rule real_mult_le_le_mono1);
    1.70 -  hence  "- (z * x) <= - (z * y)"; 
    1.71 -    by (simp only: real_minus_mult_eq1);
    1.72 +  assume "z < (#0::real)" "x <= y";
    1.73 +  hence "(#0::real) < - z"; by simp;
    1.74 +  hence "(#0::real) <= - z"; by (rule real_less_imp_le);
    1.75 +  hence "x * (- z) <= y * (- z)"; 
    1.76 +    by (rule real_mult_le_le_mono2);
    1.77 +  hence  "- (x * z) <= - (y * z)"; 
    1.78 +    by (simp only: real_minus_mult_eq2);
    1.79 +  thus ?thesis; by (simp only: real_mult_commute);
    1.80 +qed;
    1.81 +
    1.82 +lemma real_mult_less_le_mono: 
    1.83 +  "[| (#0::real) < z; x <= y |] ==> z * x <= z * y";
    1.84 +proof -; 
    1.85 +  assume "(#0::real) < z" "x <= y";
    1.86 +  have "(#0::real) <= z"; by (rule real_less_imp_le);
    1.87 +  hence "x * z <= y * z"; 
    1.88 +    by (rule real_mult_le_le_mono2);
    1.89 +  thus ?thesis; by (simp only: real_mult_commute);
    1.90 +qed;
    1.91 +
    1.92 +lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x";
    1.93 +proof -; 
    1.94 +  assume "#0 < x";
    1.95 +  have "0r < x"; by simp;
    1.96 +  hence "0r < rinv x"; by (rule real_rinv_gt_zero);
    1.97    thus ?thesis; by simp;
    1.98  qed;
    1.99  
   1.100 -lemma real_mult_less_le_mono: 
   1.101 -  "[| 0r < z; x <= y |] ==> z * x <= z * y";
   1.102 -proof -; 
   1.103 -  assume "0r < z" "x <= y";
   1.104 -  have "0r <= z"; by (rule real_less_imp_le);
   1.105 -  thus ?thesis; by (rule real_mult_le_le_mono1); 
   1.106 +lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1";
   1.107 +   by simp;
   1.108 +
   1.109 +lemma real_mult_inv_left1: "x ~= #0 ==> rinv(x)*x = #1";
   1.110 +   by simp;
   1.111 +
   1.112 +lemma real_le_mult_order1a: 
   1.113 +      "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y";
   1.114 +proof -;
   1.115 +  assume "#0 <= x" "#0 <= y";
   1.116 +    have "[|0r <= x; 0r <= y|] ==> 0r <= x * y";  
   1.117 +      by (rule real_le_mult_order);
   1.118 +    thus ?thesis; by (simp!);
   1.119  qed;
   1.120  
   1.121  lemma real_mult_diff_distrib: 
     2.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Wed May 31 18:06:02 2000 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Jun 01 11:22:27 2000 +0200
     2.3 @@ -66,7 +66,7 @@
     2.4  constdefs
     2.5    B :: "[ 'a set, 'a => real, 'a => real ] => real set"
     2.6    "B V norm f == 
     2.7 -  {0r} \Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";
     2.8 +  {(#0::real)} \Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";
     2.9  
    2.10  text{* $n$ is the function norm of $f$, iff 
    2.11  $n$ is the supremum of $B$. 
    2.12 @@ -84,7 +84,7 @@
    2.13    function_norm :: " ['a set, 'a => real, 'a => real] => real"
    2.14    "function_norm V norm f == Sup UNIV (B V norm f)";
    2.15  
    2.16 -lemma B_not_empty: "0r : B V norm f";
    2.17 +lemma B_not_empty: "(#0::real) : B V norm f";
    2.18    by (unfold B_def, force);
    2.19  
    2.20  text {* The following lemma states that every continuous linear form
    2.21 @@ -110,7 +110,7 @@
    2.22  
    2.23      show "EX X. X : B V norm f"; 
    2.24      proof (intro exI);
    2.25 -      show "0r : (B V norm f)"; by (unfold B_def, force);
    2.26 +      show "(#0::real) : (B V norm f)"; by (unfold B_def, force);
    2.27      qed;
    2.28  
    2.29      txt {* Then we have to show that $B$ is bounded: *};
    2.30 @@ -121,7 +121,7 @@
    2.31        txt {* We know that $f$ is bounded by some value $c$. *};  
    2.32    
    2.33        fix c; assume a: "ALL x:V. abs (f x) <= c * norm x";
    2.34 -      def b == "max c 0r";
    2.35 +      def b == "max c (#0::real)";
    2.36  
    2.37        show "?thesis";
    2.38        proof (intro exI isUbI setleI ballI, unfold B_def, 
    2.39 @@ -132,7 +132,7 @@
    2.40          Due to the definition of $B$ there are two cases for
    2.41          $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *};
    2.42  
    2.43 -	fix y; assume "y = 0r";
    2.44 +	fix y; assume "y = (#0::real)";
    2.45          show "y <= b"; by (simp! add: le_max2);
    2.46  
    2.47          txt{* The second case is 
    2.48 @@ -143,22 +143,22 @@
    2.49  	fix x y;
    2.50          assume "x:V" "x ~= 00"; (***
    2.51  
    2.52 -         have ge: "0r <= rinv (norm x)";
    2.53 +         have ge: "(#0::real) <= rinv (norm x)";
    2.54            by (rule real_less_imp_le, rule real_rinv_gt_zero, 
    2.55                  rule normed_vs_norm_gt_zero); (***
    2.56            proof (rule real_less_imp_le);
    2.57 -            show "0r < rinv (norm x)";
    2.58 +            show "(#0::real) < rinv (norm x)";
    2.59              proof (rule real_rinv_gt_zero);
    2.60 -              show "0r < norm x"; ..;
    2.61 +              show "(#0::real) < norm x"; ..;
    2.62              qed;
    2.63            qed; ***)
    2.64 -        have nz: "norm x ~= 0r"; 
    2.65 +        have nz: "norm x ~= (#0::real)"; 
    2.66            by (rule not_sym, rule lt_imp_not_eq, 
    2.67                rule normed_vs_norm_gt_zero); (***
    2.68            proof (rule not_sym);
    2.69 -            show "0r ~= norm x"; 
    2.70 +            show "(#0::real) ~= norm x"; 
    2.71              proof (rule lt_imp_not_eq);
    2.72 -              show "0r < norm x"; ..;
    2.73 +              show "(#0::real) < norm x"; ..;
    2.74              qed;
    2.75            qed; ***)***)
    2.76  
    2.77 @@ -168,16 +168,16 @@
    2.78          assume "y = abs (f x) * rinv (norm x)";
    2.79          also; have "... <= c * norm x * rinv (norm x)";
    2.80          proof (rule real_mult_le_le_mono2);
    2.81 -          show "0r <= rinv (norm x)";
    2.82 -            by (rule real_less_imp_le, rule real_rinv_gt_zero, 
    2.83 +          show "(#0::real) <= rinv (norm x)";
    2.84 +            by (rule real_less_imp_le, rule real_rinv_gt_zero1, 
    2.85                  rule normed_vs_norm_gt_zero);
    2.86            from a; show "abs (f x) <= c * norm x"; ..;
    2.87          qed;
    2.88          also; have "... = c * (norm x * rinv (norm x))"; 
    2.89            by (rule real_mult_assoc);
    2.90 -        also; have "(norm x * rinv (norm x)) = 1r"; 
    2.91 -        proof (rule real_mult_inv_right);
    2.92 -          show nz: "norm x ~= 0r"; 
    2.93 +        also; have "(norm x * rinv (norm x)) = (#1::real)"; 
    2.94 +        proof (rule real_mult_inv_right1);
    2.95 +          show nz: "norm x ~= (#0::real)"; 
    2.96              by (rule not_sym, rule lt_imp_not_eq, 
    2.97                rule normed_vs_norm_gt_zero);
    2.98          qed;
    2.99 @@ -192,7 +192,7 @@
   2.100  
   2.101  lemma fnorm_ge_zero [intro??]: 
   2.102    "[| is_continuous V norm f; is_normed_vectorspace V norm|]
   2.103 -   ==> 0r <= function_norm V norm f";
   2.104 +   ==> (#0::real) <= function_norm V norm f";
   2.105  proof -;
   2.106    assume c: "is_continuous V norm f" 
   2.107       and n: "is_normed_vectorspace V norm";
   2.108 @@ -203,24 +203,24 @@
   2.109  
   2.110    show ?thesis; 
   2.111    proof (unfold function_norm_def, rule sup_ub1);
   2.112 -    show "ALL x:(B V norm f). 0r <= x"; 
   2.113 +    show "ALL x:(B V norm f). (#0::real) <= x"; 
   2.114      proof (intro ballI, unfold B_def,
   2.115             elim UnE singletonE CollectE exE conjE); 
   2.116        fix x r;
   2.117        assume "x : V" "x ~= 00" 
   2.118          and r: "r = abs (f x) * rinv (norm x)";
   2.119  
   2.120 -      have ge: "0r <= abs (f x)"; by (simp! only: abs_ge_zero);
   2.121 -      have "0r <= rinv (norm x)"; 
   2.122 -        by (rule real_less_imp_le, rule real_rinv_gt_zero, rule);(***
   2.123 +      have ge: "(#0::real) <= abs (f x)"; by (simp! only: abs_ge_zero);
   2.124 +      have "(#0::real) <= rinv (norm x)"; 
   2.125 +        by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule);(***
   2.126          proof (rule real_less_imp_le);
   2.127 -          show "0r < rinv (norm x)"; 
   2.128 +          show "(#0::real) < rinv (norm x)"; 
   2.129            proof (rule real_rinv_gt_zero);
   2.130 -            show "0r < norm x"; ..;
   2.131 +            show "(#0::real) < norm x"; ..;
   2.132            qed;
   2.133          qed; ***)
   2.134 -      with ge; show "0r <= r";
   2.135 -       by (simp only: r, rule real_le_mult_order);
   2.136 +      with ge; show "(#0::real) <= r";
   2.137 +       by (simp only: r, rule real_le_mult_order1a);
   2.138      qed (simp!);
   2.139  
   2.140      txt {* Since $f$ is continuous the function norm exists: *};
   2.141 @@ -231,7 +231,7 @@
   2.142  
   2.143      txt {* $B$ is non-empty by construction: *};
   2.144  
   2.145 -    show "0r : B V norm f"; by (rule B_not_empty);
   2.146 +    show "(#0::real) : B V norm f"; by (rule B_not_empty);
   2.147    qed;
   2.148  qed;
   2.149    
   2.150 @@ -261,22 +261,22 @@
   2.151  
   2.152      assume "x = 00";
   2.153      have "abs (f x) = abs (f 00)"; by (simp!);
   2.154 -    also; from v continuous_linearform; have "f 00 = 0r"; ..;
   2.155 +    also; from v continuous_linearform; have "f 00 = (#0::real)"; ..;
   2.156      also; note abs_zero;
   2.157 -    also; have "0r <= function_norm V norm f * norm x";
   2.158 -    proof (rule real_le_mult_order);
   2.159 -      show "0r <= function_norm V norm f"; ..;
   2.160 -      show "0r <= norm x"; ..;
   2.161 +    also; have "(#0::real) <= function_norm V norm f * norm x";
   2.162 +    proof (rule real_le_mult_order1a);
   2.163 +      show "(#0::real) <= function_norm V norm f"; ..;
   2.164 +      show "(#0::real) <= norm x"; ..;
   2.165      qed;
   2.166      finally; 
   2.167      show "abs (f x) <= function_norm V norm f * norm x"; .;
   2.168  
   2.169    next;
   2.170      assume "x ~= 00";
   2.171 -    have n: "0r <= norm x"; ..;
   2.172 -    have nz: "norm x ~= 0r";
   2.173 +    have n: "(#0::real) <= norm x"; ..;
   2.174 +    have nz: "norm x ~= (#0::real)";
   2.175      proof (rule lt_imp_not_eq [RS not_sym]);
   2.176 -      show "0r < norm x"; ..;
   2.177 +      show "(#0::real) < norm x"; ..;
   2.178      qed;
   2.179  
   2.180      txt {* For the case $x\neq \zero$ we derive the following
   2.181 @@ -294,9 +294,9 @@
   2.182  
   2.183      txt {* The thesis now follows by a short calculation: *};
   2.184  
   2.185 -    have "abs (f x) = abs (f x) * 1r"; by (simp!);
   2.186 -    also; from nz; have "1r = rinv (norm x) * norm x"; 
   2.187 -      by (rule real_mult_inv_left [RS sym]);
   2.188 +    have "abs (f x) = abs (f x) * (#1::real)"; by (simp!);
   2.189 +    also; from nz; have "(#1::real) = rinv (norm x) * norm x"; 
   2.190 +      by (rule real_mult_inv_left1 [RS sym]);
   2.191      also; 
   2.192      have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x";
   2.193        by (simp! add: real_mult_assoc [of "abs (f x)"]);
   2.194 @@ -316,13 +316,13 @@
   2.195  
   2.196  lemma fnorm_le_ub: 
   2.197    "[| is_normed_vectorspace V norm; is_continuous V norm f;
   2.198 -     ALL x:V. abs (f x) <= c * norm x; 0r <= c |]
   2.199 +     ALL x:V. abs (f x) <= c * norm x; (#0::real) <= c |]
   2.200    ==> function_norm V norm f <= c";
   2.201  proof (unfold function_norm_def);
   2.202    assume "is_normed_vectorspace V norm"; 
   2.203    assume c: "is_continuous V norm f";
   2.204    assume fb: "ALL x:V. abs (f x) <= c * norm x"
   2.205 -         and "0r <= c";
   2.206 +         and "(#0::real) <= c";
   2.207  
   2.208    txt {* Suppose the inequation holds for some $c\geq 0$.
   2.209    If $c$ is an upper bound of $B$, then $c$ is greater 
   2.210 @@ -347,7 +347,7 @@
   2.211  
   2.212         txt {* The first case for $y\in B$ is $y=0$. *};
   2.213  
   2.214 -        assume "y = 0r";
   2.215 +        assume "y = (#0::real)";
   2.216          show "y <= c"; by (force!);
   2.217  
   2.218          txt{* The second case is 
   2.219 @@ -358,18 +358,18 @@
   2.220  	fix x; 
   2.221          assume "x : V" "x ~= 00"; 
   2.222  
   2.223 -        have lz: "0r < norm x"; 
   2.224 +        have lz: "(#0::real) < norm x"; 
   2.225            by (simp! add: normed_vs_norm_gt_zero);
   2.226            
   2.227 -        have nz: "norm x ~= 0r"; 
   2.228 +        have nz: "norm x ~= (#0::real)"; 
   2.229          proof (rule not_sym);
   2.230 -          from lz; show "0r ~= norm x";
   2.231 +          from lz; show "(#0::real) ~= norm x";
   2.232              by (simp! add: order_less_imp_not_eq);
   2.233          qed;
   2.234              
   2.235 -	from lz; have "0r < rinv (norm x)";
   2.236 -	  by (simp! add: real_rinv_gt_zero);
   2.237 -	hence rinv_gez: "0r <= rinv (norm x)";
   2.238 +	from lz; have "(#0::real) < rinv (norm x)";
   2.239 +	  by (simp! add: real_rinv_gt_zero1);
   2.240 +	hence rinv_gez: "(#0::real) <= rinv (norm x)";
   2.241            by (rule real_less_imp_le);
   2.242  
   2.243  	assume "y = abs (f x) * rinv (norm x)"; 
     3.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed May 31 18:06:02 2000 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jun 01 11:22:27 2000 +0200
     3.3 @@ -206,7 +206,7 @@
     3.4                    proof (rule graph_extI);
     3.5  		    fix t; assume "t:H"; 
     3.6  		    have "(SOME (y, a). t = y + a (*) x0 & y : H)
     3.7 -                         = (t,0r)";
     3.8 +                         = (t,#0)";
     3.9  		      by (rule decomp_H0_H [OF _ _ _ _ _ x0]);
    3.10  		    thus "h t = h0 t"; by (simp! add: Let_def);
    3.11  		  next;
    3.12 @@ -261,11 +261,11 @@
    3.13  		  proof (rule graph_extI);
    3.14  		    fix x; assume "x:F";
    3.15  		    have "f x = h x"; ..;
    3.16 -		    also; have " ... = h x + 0r * xi"; by simp;
    3.17 -		    also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
    3.18 +		    also; have " ... = h x + #0 * xi"; by simp;
    3.19 +		    also; have "... = (let (y,a) = (x, #0) in h y + a * xi)";
    3.20  		      by (simp add: Let_def);
    3.21  		    also; have 
    3.22 -		      "(x, 0r) = (SOME (y, a). x = y + a (*) x0 & y : H)";
    3.23 +		      "(x, #0) = (SOME (y, a). x = y + a (*) x0 & y : H)";
    3.24  		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+;
    3.25  		    also; have 
    3.26  		      "(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H)
    3.27 @@ -480,7 +480,7 @@
    3.28        have  "graph H h <= graph H0 h0"; 
    3.29        proof (rule graph_extI);
    3.30          fix t; assume "t:H"; 
    3.31 -        have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,0r)";
    3.32 +        have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,#0)";
    3.33            by (rule decomp_H0_H, rule x0); 
    3.34          thus "h t = h0 t"; by (simp! add: Let_def);
    3.35        next;
    3.36 @@ -541,11 +541,11 @@
    3.37          proof (rule graph_extI);
    3.38            fix x; assume "x:F";
    3.39            have "f x = h x"; ..;
    3.40 -          also; have " ... = h x + 0r * xi"; by simp;
    3.41 -          also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
    3.42 +          also; have " ... = h x + #0 * xi"; by simp;
    3.43 +          also; have "... = (let (y,a) = (x, #0) in h y + a * xi)";
    3.44              by (simp add: Let_def);
    3.45            also; have 
    3.46 -            "(x, 0r) = (SOME (y, a). x = y + a ( * ) x0 & y : H)";
    3.47 +            "(x, #0) = (SOME (y, a). x = y + a ( * ) x0 & y : H)";
    3.48              by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
    3.49            also; have 
    3.50              "(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H)
    3.51 @@ -664,10 +664,10 @@
    3.52  
    3.53      txt{* $p$ is positive definite: *};
    3.54  
    3.55 -    show "0r <= p x";
    3.56 -    proof (unfold p_def, rule real_le_mult_order);
    3.57 -      from _ f_norm; show "0r <= function_norm F norm f"; ..;
    3.58 -      show "0r <= norm x"; ..;
    3.59 +    show "#0 <= p x";
    3.60 +    proof (unfold p_def, rule real_le_mult_order1a);
    3.61 +      from _ f_norm; show "#0 <= function_norm F norm f"; ..;
    3.62 +      show "#0 <= norm x"; ..;
    3.63      qed;
    3.64  
    3.65      txt{* $p$ is absolutely homogenous: *};
    3.66 @@ -693,8 +693,8 @@
    3.67          by (simp!);
    3.68        also; 
    3.69        have "... <= function_norm F norm f * (norm x + norm y)";
    3.70 -      proof (rule real_mult_le_le_mono1);
    3.71 -        from _ f_norm; show "0r <= function_norm F norm f"; ..;
    3.72 +      proof (rule real_mult_le_le_mono1a);
    3.73 +        from _ f_norm; show "#0 <= function_norm F norm f"; ..;
    3.74          show "norm (x + y) <= norm x + norm y"; ..;
    3.75        qed;
    3.76        also; have "... = function_norm F norm f * norm x 
    3.77 @@ -774,7 +774,7 @@
    3.78  
    3.79          with _ g_cont; show "?L <= ?R";
    3.80          proof (rule fnorm_le_ub);
    3.81 -          from f_cont f_norm; show "0r <= function_norm F norm f"; ..;
    3.82 +          from f_cont f_norm; show "#0 <= function_norm F norm f"; ..;
    3.83          qed;
    3.84  
    3.85          txt{* The other direction is achieved by a similar 
    3.86 @@ -794,7 +794,7 @@
    3.87          qed; 
    3.88          thus "?R <= ?L"; 
    3.89          proof (rule fnorm_le_ub [OF f_norm f_cont]);
    3.90 -          from g_cont; show "0r <= function_norm E norm g"; ..;
    3.91 +          from g_cont; show "#0 <= function_norm E norm g"; ..;
    3.92          qed;
    3.93        qed;
    3.94      qed;
     4.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Wed May 31 18:06:02 2000 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Jun 01 11:22:27 2000 +0200
     4.3 @@ -275,14 +275,14 @@
     4.4      also; have "... <= p (y + a (*) x0)";
     4.5      proof (rule linorder_linear_split); 
     4.6  
     4.7 -      assume z: "a = 0r"; 
     4.8 +      assume z: "a = (#0::real)"; 
     4.9        with vs y a; show ?thesis; by simp;
    4.10  
    4.11      txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ 
    4.12      taken as $y/a$: *};
    4.13  
    4.14      next;
    4.15 -      assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
    4.16 +      assume lz: "a < #0"; hence nz: "a ~= #0"; by simp;
    4.17        from a1; 
    4.18        have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
    4.19          by (rule bspec) (simp!);
    4.20 @@ -312,7 +312,7 @@
    4.21        taken as $y/a$: *};
    4.22  
    4.23      next; 
    4.24 -      assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
    4.25 +      assume gz: "#0 < a"; hence nz: "a ~= #0"; by simp;
    4.26        from a2;
    4.27        have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
    4.28          by (rule bspec) (simp!);
     5.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Wed May 31 18:06:02 2000 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Jun 01 11:22:27 2000 +0200
     5.3 @@ -35,8 +35,8 @@
     5.4    ==> f (- x) = - f x";
     5.5  proof -; 
     5.6    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
     5.7 -  have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
     5.8 -  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
     5.9 +  have "f (- x) = f ((- (#1::real)) (*) x)"; by (simp! add: negate_eq1);
    5.10 +  also; have "... = (- #1) * (f x)"; by (rule linearform_mult);
    5.11    also; have "... = - (f x)"; by (simp!);
    5.12    finally; show ?thesis; .;
    5.13  qed;
    5.14 @@ -56,14 +56,14 @@
    5.15  text{* Every linear form yields $0$ for the $\zero$ vector.*};
    5.16  
    5.17  lemma linearform_zero [intro??, simp]: 
    5.18 -  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r"; 
    5.19 +  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = (#0::real)"; 
    5.20  proof -; 
    5.21    assume "is_vectorspace V" "is_linearform V f";
    5.22    have "f 00 = f (00 - 00)"; by (simp!);
    5.23    also; have "... = f 00 - f 00"; 
    5.24      by (rule linearform_diff) (simp!)+;
    5.25 -  also; have "... = 0r"; by simp;
    5.26 -  finally; show "f 00 = 0r"; .;
    5.27 +  also; have "... = (#0::real)"; by simp;
    5.28 +  finally; show "f 00 = (#0::real)"; .;
    5.29  qed; 
    5.30  
    5.31  end;
    5.32 \ No newline at end of file
     6.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Wed May 31 18:06:02 2000 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Jun 01 11:22:27 2000 +0200
     6.3 @@ -18,19 +18,19 @@
     6.4  constdefs
     6.5    is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
     6.6    "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
     6.7 -        0r <= norm x 
     6.8 +        (#0::real) <= norm x 
     6.9        & norm (a (*) x) = (abs a) * (norm x)
    6.10        & norm (x + y) <= norm x + norm y";
    6.11  
    6.12  lemma is_seminormI [intro]: 
    6.13 -  "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
    6.14 +  "[| !! x y a. [| x:V; y:V|] ==> (#0::real) <= norm x;
    6.15    !! x a. x:V ==> norm (a (*) x) = (abs a) * (norm x);
    6.16    !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
    6.17    ==> is_seminorm V norm";
    6.18    by (unfold is_seminorm_def, force);
    6.19  
    6.20  lemma seminorm_ge_zero [intro??]:
    6.21 -  "[| is_seminorm V norm; x:V |] ==> 0r <= norm x";
    6.22 +  "[| is_seminorm V norm; x:V |] ==> (#0::real) <= norm x";
    6.23    by (unfold is_seminorm_def, force);
    6.24  
    6.25  lemma seminorm_abs_homogenous: 
    6.26 @@ -48,13 +48,13 @@
    6.27    ==> norm (x - y) <= norm x + norm y";
    6.28  proof -;
    6.29    assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
    6.30 -  have "norm (x - y) = norm (x + - 1r (*) y)";  
    6.31 -    by (simp! add: diff_eq2 negate_eq2);
    6.32 -  also; have "... <= norm x + norm  (- 1r (*) y)"; 
    6.33 +  have "norm (x - y) = norm (x + - (#1::real) (*) y)";  
    6.34 +    by (simp! add: diff_eq2 negate_eq2a);
    6.35 +  also; have "... <= norm x + norm  (- (#1::real) (*) y)"; 
    6.36      by (simp! add: seminorm_subadditive);
    6.37 -  also; have "norm (- 1r (*) y) = abs (- 1r) * norm y"; 
    6.38 +  also; have "norm (- (#1::real) (*) y) = abs (- (#1::real)) * norm y"; 
    6.39      by (rule seminorm_abs_homogenous);
    6.40 -  also; have "abs (- 1r) = 1r"; by (rule abs_minus_one);
    6.41 +  also; have "abs (- (#1::real)) = (#1::real)"; by (rule abs_minus_one);
    6.42    finally; show "norm (x - y) <= norm x + norm y"; by simp;
    6.43  qed;
    6.44  
    6.45 @@ -63,10 +63,10 @@
    6.46    ==> norm (- x) = norm x";
    6.47  proof -;
    6.48    assume "is_seminorm V norm" "x:V" "is_vectorspace V";
    6.49 -  have "norm (- x) = norm (- 1r (*) x)"; by (simp! only: negate_eq1);
    6.50 -  also; have "... = abs (- 1r) * norm x"; 
    6.51 +  have "norm (- x) = norm (- (#1::real) (*) x)"; by (simp! only: negate_eq1);
    6.52 +  also; have "... = abs (- (#1::real)) * norm x"; 
    6.53      by (rule seminorm_abs_homogenous);
    6.54 -  also; have "abs (- 1r) = 1r"; by (rule abs_minus_one);
    6.55 +  also; have "abs (- (#1::real)) = (#1::real)"; by (rule abs_minus_one);
    6.56    finally; show "norm (- x) = norm x"; by simp;
    6.57  qed;
    6.58  
    6.59 @@ -79,10 +79,10 @@
    6.60  constdefs
    6.61    is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
    6.62    "is_norm V norm == ALL x: V.  is_seminorm V norm 
    6.63 -      & (norm x = 0r) = (x = 00)";
    6.64 +      & (norm x = (#0::real)) = (x = 00)";
    6.65  
    6.66  lemma is_normI [intro]: 
    6.67 -  "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (x = 00) 
    6.68 +  "ALL x: V.  is_seminorm V norm  & (norm x = (#0::real)) = (x = 00) 
    6.69    ==> is_norm V norm"; by (simp only: is_norm_def);
    6.70  
    6.71  lemma norm_is_seminorm [intro??]: 
    6.72 @@ -90,11 +90,11 @@
    6.73    by (unfold is_norm_def, force);
    6.74  
    6.75  lemma norm_zero_iff: 
    6.76 -  "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = 00)";
    6.77 +  "[| is_norm V norm; x:V |] ==> (norm x = (#0::real)) = (x = 00)";
    6.78    by (unfold is_norm_def, force);
    6.79  
    6.80  lemma norm_ge_zero [intro??]:
    6.81 -  "[|is_norm V norm; x:V |] ==> 0r <= norm x";
    6.82 +  "[|is_norm V norm; x:V |] ==> (#0::real) <= norm x";
    6.83    by (unfold is_norm_def is_seminorm_def, force);
    6.84  
    6.85  
    6.86 @@ -124,22 +124,22 @@
    6.87    by (unfold is_normed_vectorspace_def, elim conjE);
    6.88  
    6.89  lemma normed_vs_norm_ge_zero [intro??]: 
    6.90 -  "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
    6.91 +  "[| is_normed_vectorspace V norm; x:V |] ==> (#0::real) <= norm x";
    6.92    by (unfold is_normed_vectorspace_def, rule, elim conjE);
    6.93  
    6.94  lemma normed_vs_norm_gt_zero [intro??]: 
    6.95 -  "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> 0r < norm x";
    6.96 +  "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> (#0::real) < norm x";
    6.97  proof (unfold is_normed_vectorspace_def, elim conjE);
    6.98    assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm";
    6.99 -  have "0r <= norm x"; ..;
   6.100 -  also; have "0r ~= norm x";
   6.101 +  have "(#0::real) <= norm x"; ..;
   6.102 +  also; have "(#0::real) ~= norm x";
   6.103    proof;
   6.104 -    presume "norm x = 0r";
   6.105 +    presume "norm x = (#0::real)";
   6.106      also; have "?this = (x = 00)"; by (rule norm_zero_iff);
   6.107      finally; have "x = 00"; .;
   6.108      thus "False"; by contradiction;
   6.109    qed (rule sym);
   6.110 -  finally; show "0r < norm x"; .;
   6.111 +  finally; show "(#0::real) < norm x"; .;
   6.112  qed;
   6.113  
   6.114  lemma normed_vs_norm_abs_homogenous [intro??]: 
   6.115 @@ -169,14 +169,14 @@
   6.116      show "is_seminorm F norm"; 
   6.117      proof;
   6.118        fix x y a; presume "x : E";
   6.119 -      show "0r <= norm x"; ..;
   6.120 +      show "(#0::real) <= norm x"; ..;
   6.121        show "norm (a (*) x) = abs a * norm x"; ..;
   6.122        presume "y : E";
   6.123        show "norm (x + y) <= norm x + norm y"; ..;
   6.124      qed (simp!)+;
   6.125  
   6.126      fix x; assume "x : F";
   6.127 -    show "(norm x = 0r) = (x = 00)"; 
   6.128 +    show "(norm x = (#0::real)) = (x = 00)"; 
   6.129      proof (rule norm_zero_iff);
   6.130        show "is_norm E norm"; ..;
   6.131      qed (simp!);
     7.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed May 31 18:06:02 2000 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Jun 01 11:22:27 2000 +0200
     7.3 @@ -87,7 +87,7 @@
     7.4      show "00 : U"; ..;
     7.5      show "ALL x:U. ALL a. a (*) x : U"; by (simp!);
     7.6      show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
     7.7 -    show "ALL x:U. - x = -1r (*) x"; by (simp! add: negate_eq1);
     7.8 +    show "ALL x:U. - x = -#1 (*) x"; by (simp! add: negate_eq1);
     7.9      show "ALL x:U. ALL y:U. x - y =  x + - y"; 
    7.10        by (simp! add: diff_eq1);
    7.11    qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
    7.12 @@ -152,7 +152,7 @@
    7.13  lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
    7.14  proof (unfold lin_def, intro CollectI exI conjI);
    7.15    assume "is_vectorspace V" "x:V";
    7.16 -  show "x = 1r (*) x"; by (simp!);
    7.17 +  show "x = #1 (*) x"; by (simp!);
    7.18  qed simp;
    7.19  
    7.20  text {* Any linear closure is a subspace. *};
    7.21 @@ -163,7 +163,7 @@
    7.22    assume "is_vectorspace V" "x:V";
    7.23    show "00 : lin x"; 
    7.24    proof (unfold lin_def, intro CollectI exI conjI);
    7.25 -    show "00 = 0r (*) x"; by (simp!);
    7.26 +    show "00 = (#0::real) (*) x"; by (simp!);
    7.27    qed simp;
    7.28  
    7.29    show "lin x <= V";
    7.30 @@ -379,9 +379,9 @@
    7.31            fix a; assume "x = a (*) x0";
    7.32            show ?thesis;
    7.33            proof cases;
    7.34 -            assume "a = 0r"; show ?thesis; by (simp!);
    7.35 +            assume "a = (#0::real)"; show ?thesis; by (simp!);
    7.36            next;
    7.37 -            assume "a ~= 0r"; 
    7.38 +            assume "a ~= (#0::real)"; 
    7.39              from h; have "rinv a (*) a (*) x0 : H"; 
    7.40                by (rule subspace_mult_closed) (simp!);
    7.41              also; have "rinv a (*) a (*) x0 = x0"; by (simp!);
    7.42 @@ -419,15 +419,15 @@
    7.43  lemma decomp_H0_H: 
    7.44    "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
    7.45    x0 ~= 00 |] 
    7.46 -  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, 0r)";
    7.47 +  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))";
    7.48  proof (rule, unfold split_paired_all);
    7.49    assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
    7.50      "x0 ~= 00";
    7.51    have h: "is_vectorspace H"; ..;
    7.52    fix y a; presume t1: "t = y + a (*) x0" and "y:H";
    7.53 -  have "y = t & a = 0r"; 
    7.54 +  have "y = t & a = (#0::real)"; 
    7.55      by (rule decomp_H0) (assumption | (simp!))+;
    7.56 -  thus "(y, a) = (t, 0r)"; by (simp!);
    7.57 +  thus "(y, a) = (t, (#0::real))"; by (simp!);
    7.58  qed (simp!)+;
    7.59  
    7.60  text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
     8.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed May 31 18:06:02 2000 +0200
     8.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Jun 01 11:22:27 2000 +0200
     8.3 @@ -29,7 +29,7 @@
     8.4  (***
     8.5  constdefs 
     8.6    negate :: "'a => 'a"                           ("- _" [100] 100)
     8.7 -  "- x == (- 1r) ( * ) x"
     8.8 +  "- x == (- (#1::real)) ( * ) x"
     8.9    diff :: "'a => 'a => 'a"                       (infixl "-" 68)
    8.10    "x - y == x + - y";
    8.11  ***)
    8.12 @@ -59,8 +59,8 @@
    8.13        & a (*) (x + y) = a (*) x + a (*) y       
    8.14        & (a + b) (*) x = a (*) x + b (*) x         
    8.15        & (a * b) (*) x = a (*) b (*) x               
    8.16 -      & 1r (*) x = x
    8.17 -      & - x = (- 1r) (*) x
    8.18 +      & (#1::real) (*) x = x
    8.19 +      & - x = (- (#1::real)) (*) x
    8.20        & x - y = x + - y)";                             
    8.21  
    8.22  text_raw {* \medskip *};
    8.23 @@ -77,8 +77,8 @@
    8.24    ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
    8.25    ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
    8.26    ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x; 
    8.27 -  ALL x:V. 1r (*) x = x; 
    8.28 -  ALL x:V. - x = (- 1r) (*) x; 
    8.29 +  ALL x:V. (#1::real) (*) x = x; 
    8.30 +  ALL x:V. - x = (- (#1::real)) (*) x; 
    8.31    ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
    8.32  proof (unfold is_vectorspace_def, intro conjI ballI allI);
    8.33    fix x y z; 
    8.34 @@ -91,7 +91,7 @@
    8.35  text {* The corresponding destruction rules are: *};
    8.36  
    8.37  lemma negate_eq1: 
    8.38 -  "[| is_vectorspace V; x:V |] ==> - x = (- 1r) (*) x";
    8.39 +  "[| is_vectorspace V; x:V |] ==> - x = (- (#1::real)) (*) x";
    8.40    by (unfold is_vectorspace_def) simp;
    8.41  
    8.42  lemma diff_eq1: 
    8.43 @@ -99,7 +99,11 @@
    8.44    by (unfold is_vectorspace_def) simp; 
    8.45  
    8.46  lemma negate_eq2: 
    8.47 -  "[| is_vectorspace V; x:V |] ==> (- 1r) (*) x = - x";
    8.48 +  "[| is_vectorspace V; x:V |] ==> (- (#1::real)) (*) x = - x";
    8.49 +  by (unfold is_vectorspace_def) simp;
    8.50 +
    8.51 +lemma negate_eq2a: 
    8.52 +  "[| is_vectorspace V; x:V |] ==> ((#-1::real)) (*) x = - x";
    8.53    by (unfold is_vectorspace_def) simp;
    8.54  
    8.55  lemma diff_eq2: 
    8.56 @@ -201,7 +205,7 @@
    8.57    by (simp only: vs_mult_assoc);
    8.58  
    8.59  lemma vs_mult_1 [simp]: 
    8.60 -  "[| is_vectorspace V; x:V |] ==> 1r (*) x = x"; 
    8.61 +  "[| is_vectorspace V; x:V |] ==> (#1::real) (*) x = x"; 
    8.62    by (unfold is_vectorspace_def) simp;
    8.63  
    8.64  lemma vs_diff_mult_distrib1: 
    8.65 @@ -230,15 +234,15 @@
    8.66  text{* Further derived laws: *};
    8.67  
    8.68  lemma vs_mult_zero_left [simp]: 
    8.69 -  "[| is_vectorspace V; x:V |] ==> 0r (*) x = 00";
    8.70 +  "[| is_vectorspace V; x:V |] ==> (#0::real) (*) x = 00";
    8.71  proof -;
    8.72    assume "is_vectorspace V" "x:V";
    8.73 -  have  "0r (*) x = (1r - 1r) (*) x"; by (simp only: real_diff_self);
    8.74 -  also; have "... = (1r + - 1r) (*) x"; by simp;
    8.75 -  also; have "... =  1r (*) x + (- 1r) (*) x"; 
    8.76 +  have  "(#0::real) (*) x = ((#1::real) - (#1::real)) (*) x"; by simp;
    8.77 +  also; have "... = ((#1::real) + - (#1::real)) (*) x"; by simp;
    8.78 +  also; have "... =  (#1::real) (*) x + (- (#1::real)) (*) x"; 
    8.79      by (rule vs_add_mult_distrib2);
    8.80 -  also; have "... = x + (- 1r) (*) x"; by (simp!);
    8.81 -  also; have "... = x + - x"; by (simp! add: negate_eq2);;
    8.82 +  also; have "... = x + (- (#1::real)) (*) x"; by (simp!);
    8.83 +  also; have "... = x + - x"; by (simp! add: negate_eq2a);;
    8.84    also; have "... = x - x"; by (simp! add: diff_eq2);
    8.85    also; have "... = 00"; by (simp!);
    8.86    finally; show ?thesis; .;
    8.87 @@ -354,25 +358,25 @@
    8.88    by (simp add: real_mult_commute);
    8.89  
    8.90  lemma vs_mult_zero_uniq :
    8.91 -  "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = 0r";
    8.92 +  "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = (#0::real)";
    8.93  proof (rule classical);
    8.94    assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00";
    8.95 -  assume "a ~= 0r";
    8.96 +  assume "a ~= (#0::real)";
    8.97    have "x = (rinv a * a) (*) x"; by (simp!);
    8.98    also; have "... = rinv a (*) (a (*) x)"; by (rule vs_mult_assoc);
    8.99    also; have "... = rinv a (*) 00"; by (simp!);
   8.100    also; have "... = 00"; by (simp!);
   8.101    finally; have "x = 00"; .;
   8.102 -  thus "a = 0r"; by contradiction; 
   8.103 +  thus "a = (#0::real)"; by contradiction; 
   8.104  qed;
   8.105  
   8.106  lemma vs_mult_left_cancel: 
   8.107 -  "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> 
   8.108 +  "[| is_vectorspace V; x:V; y:V; a ~= (#0::real) |] ==> 
   8.109    (a (*) x = a (*) y) = (x = y)"
   8.110    (concl is "?L = ?R");
   8.111  proof;
   8.112 -  assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
   8.113 -  have "x = 1r (*) x"; by (simp!);
   8.114 +  assume "is_vectorspace V" "x:V" "y:V" "a ~= (#0::real)";
   8.115 +  have "x = (#1::real) (*) x"; by (simp!);
   8.116    also; have "... = (rinv a * a) (*) x"; by (simp!);
   8.117    also; have "... = rinv a (*) (a (*) x)"; 
   8.118      by (simp! only: vs_mult_assoc);
   8.119 @@ -390,7 +394,7 @@
   8.120      by (simp! add: vs_diff_mult_distrib2);
   8.121    also; assume ?L; hence "a (*) x - b (*) x = 00"; by (simp!);
   8.122    finally; have "(a - b) (*) x = 00"; .; 
   8.123 -  hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
   8.124 +  hence "a - b = (#0::real)"; by (simp! add: vs_mult_zero_uniq);
   8.125    thus "a = b"; by (rule real_add_minus_eq);
   8.126  qed simp; (*** 
   8.127  
   8.128 @@ -404,7 +408,7 @@
   8.129    assume l: ?L; 
   8.130    show "a = b"; 
   8.131    proof (rule real_add_minus_eq);
   8.132 -    show "a - b = 0r"; 
   8.133 +    show "a - b = (#0::real)"; 
   8.134      proof (rule vs_mult_zero_uniq);
   8.135        have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
   8.136          by (simp! add: vs_diff_mult_distrib2);
     9.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed May 31 18:06:02 2000 +0200
     9.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Jun 01 11:22:27 2000 +0200
     9.3 @@ -327,7 +327,7 @@
     9.4  (**** hrinv: multiplicative inverse on hypreal ****)
     9.5  
     9.6  Goalw [congruent_def]
     9.7 -  "congruent hyprel (%X. hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})";
     9.8 +  "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else rinv(X n)})";
     9.9  by (Auto_tac THEN Ultra_tac 1);
    9.10  qed "hypreal_hrinv_congruent";
    9.11  
    9.12 @@ -336,7 +336,7 @@
    9.13  
    9.14  Goalw [hrinv_def]
    9.15        "hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
    9.16 -\      Abs_hypreal(hyprel ^^ {%n. if X n = 0r then 0r else rinv(X n)})";
    9.17 +\      Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else rinv(X n)})";
    9.18  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    9.19  by (simp_tac (simpset() addsimps 
    9.20     [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
    9.21 @@ -347,7 +347,8 @@
    9.22  by (rotate_tac 1 1);
    9.23  by (asm_full_simp_tac (simpset() addsimps 
    9.24      [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
    9.25 -by (ultra_tac (claset() addDs [rinv_not_zero,real_rinv_rinv],simpset()) 1);
    9.26 +by (ultra_tac (claset() addDs (map (full_rename_numerals thy)
    9.27 +    [rinv_not_zero,real_rinv_rinv]),simpset()) 1);
    9.28  qed "hypreal_hrinv_hrinv";
    9.29  
    9.30  Addsimps [hypreal_hrinv_hrinv];
    9.31 @@ -718,7 +719,7 @@
    9.32      hypreal_mult] setloop (split_tac [expand_if])) 1);
    9.33  by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
    9.34  by (ultra_tac (claset() addIs [ccontr] addDs 
    9.35 -    [rinv_not_zero],simpset()) 1);
    9.36 +    [full_rename_numerals thy rinv_not_zero],simpset()) 1);
    9.37  qed "hrinv_not_zero";
    9.38  
    9.39  Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
    9.40 @@ -861,15 +862,16 @@
    9.41  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    9.42  by (auto_tac (claset() addSIs [exI],simpset() addsimps
    9.43      [hypreal_less_def,hypreal_mult]));
    9.44 -by (ultra_tac (claset() addIs [real_mult_order],simpset()) 1);
    9.45 +by (ultra_tac (claset() addIs [rename_numerals thy 
    9.46 +    real_mult_order],simpset()) 1);
    9.47  qed "hypreal_mult_order";
    9.48  
    9.49  (*---------------------------------------------------------------------------------
    9.50                           Trichotomy of the hyperreals
    9.51    --------------------------------------------------------------------------------*)
    9.52  
    9.53 -Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. 0r}";
    9.54 -by (res_inst_tac [("x","%n. 0r")] exI 1);
    9.55 +Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. #0}";
    9.56 +by (res_inst_tac [("x","%n. #0")] exI 1);
    9.57  by (Step_tac 1);
    9.58  by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
    9.59  qed "lemma_hyprel_0r_mem";
    9.60 @@ -1153,8 +1155,8 @@
    9.61  qed "hypreal_mult_less_zero";
    9.62  
    9.63  Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
    9.64 -by (res_inst_tac [("x","%n. 0r")] exI 1);
    9.65 -by (res_inst_tac [("x","%n. 1r")] exI 1);
    9.66 +by (res_inst_tac [("x","%n. #0")] exI 1);
    9.67 +by (res_inst_tac [("x","%n. #1")] exI 1);
    9.68  by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
    9.69      FreeUltrafilterNat_Nat_set]));
    9.70  qed "hypreal_zero_less_one";
    9.71 @@ -1326,25 +1328,25 @@
    9.72      simpset()));
    9.73  qed "hypreal_hrinv_less_zero";
    9.74  
    9.75 -Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  1r = 1hr";
    9.76 +Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  #1 = 1hr";
    9.77  by (Step_tac 1);
    9.78  qed "hypreal_of_real_one";
    9.79  
    9.80 -Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  0r = 0hr";
    9.81 +Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  #0 = 0hr";
    9.82  by (Step_tac 1);
    9.83  qed "hypreal_of_real_zero";
    9.84  
    9.85 -Goal "(hypreal_of_real  r = 0hr) = (r = 0r)";
    9.86 +Goal "(hypreal_of_real  r = 0hr) = (r = #0)";
    9.87  by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
    9.88      simpset() addsimps [hypreal_of_real_def,
    9.89      hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
    9.90  qed "hypreal_of_real_zero_iff";
    9.91  
    9.92 -Goal "(hypreal_of_real  r ~= 0hr) = (r ~= 0r)";
    9.93 +Goal "(hypreal_of_real  r ~= 0hr) = (r ~= #0)";
    9.94  by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
    9.95  qed "hypreal_of_real_not_zero_iff";
    9.96  
    9.97 -Goal "r ~= 0r ==> hrinv (hypreal_of_real r) = \
    9.98 +Goal "r ~= #0 ==> hrinv (hypreal_of_real r) = \
    9.99  \          hypreal_of_real (rinv r)";
   9.100  by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
   9.101  by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
   9.102 @@ -1665,6 +1667,7 @@
   9.103  qed "hypreal_three_squares_add_zero_iff";
   9.104  Addsimps [hypreal_three_squares_add_zero_iff];
   9.105  
   9.106 +Addsimps [rename_numerals thy real_le_square];
   9.107  Goal "(x::hypreal)*x <= x*x + y*y";
   9.108  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   9.109  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   9.110 @@ -1679,7 +1682,7 @@
   9.111  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   9.112  by (auto_tac (claset(),simpset() addsimps 
   9.113      [hypreal_mult,hypreal_add,hypreal_le,
   9.114 -    real_le_add_order]));
   9.115 +    rename_numerals thy real_le_add_order]));
   9.116  qed "hypreal_self_le_add_pos2";
   9.117  Addsimps [hypreal_self_le_add_pos2];
   9.118  
   9.119 @@ -1690,13 +1693,15 @@
   9.120  by (full_simp_tac (simpset() addsimps 
   9.121      [pnat_one_iff RS sym,real_of_preal_def]) 1);
   9.122  by (fold_tac [real_one_def]);
   9.123 -by (rtac hypreal_of_real_one 1);
   9.124 +by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
   9.125  qed "hypreal_of_posnat_one";
   9.126  
   9.127  Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
   9.128 -by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
   9.129 -    hypreal_one_def,hypreal_add,hypreal_of_real_def,pnat_two_eq,
   9.130 -    real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ pnat_add_ac) 1);
   9.131 +by (full_simp_tac (simpset() addsimps [real_of_preal_def,
   9.132 +    rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
   9.133 +     hypreal_add,hypreal_of_real_def,pnat_two_eq,hypreal_one_def,
   9.134 +    real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ 
   9.135 +    pnat_add_ac) 1);
   9.136  qed "hypreal_of_posnat_two";
   9.137  
   9.138  Goalw [hypreal_of_posnat_def]
   9.139 @@ -1788,9 +1793,10 @@
   9.140  
   9.141  Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
   9.142  by (auto_tac (claset(),simpset() addsimps 
   9.143 -    [real_of_posnat_rinv_not_zero]));
   9.144 +    [rename_numerals thy real_of_posnat_rinv_not_zero]));
   9.145  qed "hypreal_epsilon_not_zero";
   9.146  
   9.147 +Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];
   9.148  Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
   9.149  by (Simp_tac 1);
   9.150  qed "hypreal_omega_not_zero";
    10.1 --- a/src/HOL/Real/Hyperreal/HyperDef.thy	Wed May 31 18:06:02 2000 +0200
    10.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.thy	Thu Jun 01 11:22:27 2000 +0200
    10.3 @@ -5,7 +5,7 @@
    10.4      Description : Construction of hyperreals using ultrafilters
    10.5  *) 
    10.6  
    10.7 -HyperDef = Filter + RealBin +
    10.8 +HyperDef = Filter + Real +
    10.9  
   10.10  consts 
   10.11   
   10.12 @@ -37,8 +37,8 @@
   10.13  
   10.14  defs
   10.15  
   10.16 -  hypreal_zero_def     "0hr == Abs_hypreal(hyprel^^{%n::nat. 0r})"
   10.17 -  hypreal_one_def      "1hr == Abs_hypreal(hyprel^^{%n::nat. 1r})"
   10.18 +  hypreal_zero_def     "0hr == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
   10.19 +  hypreal_one_def      "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})"
   10.20  
   10.21    (* an infinite number = [<1,2,3,...>] *)
   10.22    omega_def   "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
   10.23 @@ -54,19 +54,19 @@
   10.24  
   10.25  constdefs
   10.26  
   10.27 -  hypreal_of_real  :: real => hypreal                 ("&# _" [80] 80)
   10.28 +  hypreal_of_real  :: real => hypreal                 
   10.29    "hypreal_of_real r         == Abs_hypreal(hyprel^^{%n::nat. r})"
   10.30    
   10.31    hrinv       :: hypreal => hypreal
   10.32    "hrinv(P)   == Abs_hypreal(UN X: Rep_hypreal(P). 
   10.33 -                    hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})"
   10.34 +                    hyprel^^{%n. if X n = #0 then #0 else rinv(X n)})"
   10.35  
   10.36    (* n::nat --> (n+1)::hypreal *)
   10.37 -  hypreal_of_posnat :: nat => hypreal                ("&&# _" [80] 80)
   10.38 +  hypreal_of_posnat :: nat => hypreal                
   10.39    "hypreal_of_posnat n  == (hypreal_of_real(real_of_preal
   10.40                              (preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
   10.41  
   10.42 -  hypreal_of_nat :: nat => hypreal                   ("&&## _" [80] 80)
   10.43 +  hypreal_of_nat :: nat => hypreal                   
   10.44    "hypreal_of_nat n      == hypreal_of_posnat n + -1hr"
   10.45  
   10.46  defs 
    11.1 --- a/src/HOL/Real/RComplete.ML	Wed May 31 18:06:02 2000 +0200
    11.2 +++ b/src/HOL/Real/RComplete.ML	Thu Jun 01 11:22:27 2000 +0200
    11.3 @@ -14,23 +14,25 @@
    11.4         previously in Real.ML. 
    11.5   ---------------------------------------------------------*)
    11.6   (*a few lemmas*)
    11.7 -Goal "! x:P. 0r < x ==> \ 
    11.8 +Goal "! x:P. #0 < x ==> \ 
    11.9  \       ((? x:P. y < x) = (? X. real_of_preal X : P & \
   11.10  \                          y < real_of_preal X))";
   11.11 -by (blast_tac (claset() addSDs [bspec,
   11.12 +by (blast_tac (claset() addSDs [bspec,rename_numerals thy
   11.13  				real_gt_zero_preal_Ex RS iffD1]) 1);
   11.14  qed "real_sup_lemma1";
   11.15  
   11.16 -Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
   11.17 +Goal "[| ! x:P. #0 < x; ? x. x: P; ? y. !x: P. x < y |] \
   11.18  \         ==> (? X. X: {w. real_of_preal w : P}) & \
   11.19  \             (? Y. !X: {w. real_of_preal w : P}. X < Y)";
   11.20  by (rtac conjI 1);
   11.21 -by (blast_tac (claset() addDs [bspec, real_gt_zero_preal_Ex RS iffD1]) 1);
   11.22 +by (blast_tac (claset() addDs [bspec, rename_numerals thy 
   11.23 +    real_gt_zero_preal_Ex RS iffD1]) 1);
   11.24  by Auto_tac;
   11.25  by (dtac bspec 1 THEN assume_tac 1);
   11.26  by (ftac bspec 1  THEN assume_tac 1);
   11.27  by (dtac real_less_trans 1 THEN assume_tac 1);
   11.28 -by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1);
   11.29 +by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1
   11.30 +    THEN etac exE 1);    
   11.31  by (res_inst_tac [("x","ya")] exI 1);
   11.32  by Auto_tac;
   11.33  by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1);
   11.34 @@ -41,18 +43,21 @@
   11.35              Completeness of Positive Reals
   11.36   -------------------------------------------------------------*)
   11.37  
   11.38 -(* Supremum property for the set of positive reals *)
   11.39 -(* FIXME: long proof - can be improved - need only have 
   11.40 -   one case split *) (* will do for now *)
   11.41 -Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
   11.42 +(**
   11.43 + Supremum property for the set of positive reals
   11.44 + FIXME: long proof - should be improved - need 
   11.45 + only have one case split 
   11.46 +**)
   11.47 +
   11.48 +Goal "[| ! x:P. (#0::real) < x; ? x. x: P; ? y. !x: P. x < y |] \
   11.49  \         ==> (? S. !y. (? x: P. y < x) = (y < S))";
   11.50  by (res_inst_tac 
   11.51     [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
   11.52  by Auto_tac;
   11.53  by (ftac real_sup_lemma2 1 THEN Auto_tac);
   11.54 -by (case_tac "0r < ya" 1);
   11.55 -by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
   11.56 -by (dtac real_less_all_real2 2);
   11.57 +by (case_tac "#0 < ya" 1);
   11.58 +by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
   11.59 +by (dtac (full_rename_numerals thy real_less_all_real2) 2);
   11.60  by Auto_tac;
   11.61  by (rtac (preal_complete RS spec RS iffD1) 1);
   11.62  by Auto_tac;
   11.63 @@ -60,16 +65,15 @@
   11.64  by Auto_tac;
   11.65  (* second part *)
   11.66  by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
   11.67 -by (case_tac "0r < ya" 1);
   11.68 -by (auto_tac (claset() addSDs [real_less_all_real2,
   11.69 -			       real_gt_zero_preal_Ex RS iffD1],simpset()));
   11.70 +by (case_tac "#0 < ya" 1);
   11.71 +by (auto_tac (claset() addSDs (map (full_rename_numerals 
   11.72 +    thy) [real_less_all_real2,real_gt_zero_preal_Ex RS iffD1]),
   11.73 +    simpset()));
   11.74  by (ftac real_sup_lemma2 2 THEN Auto_tac);
   11.75  by (ftac real_sup_lemma2 1 THEN Auto_tac);
   11.76  by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
   11.77  by (Blast_tac 3);
   11.78 -by (Blast_tac 1);
   11.79 -by (Blast_tac 1);
   11.80 -by (Blast_tac 1);
   11.81 +by (ALLGOALS(Blast_tac));
   11.82  qed "posreal_complete";
   11.83  
   11.84  (*--------------------------------------------------------
   11.85 @@ -91,17 +95,19 @@
   11.86             Completeness theorem for the positive reals(again)
   11.87   ----------------------------------------------------------------*)
   11.88  
   11.89 -Goal "[| ALL x: S. 0r < x; \
   11.90 +Goal "[| ALL x: S. #0 < x; \
   11.91  \        EX x. x: S; \
   11.92  \        EX u. isUb (UNIV::real set) S u \
   11.93  \     |] ==> EX t. isLub (UNIV::real set) S t";
   11.94 -by (res_inst_tac [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1);
   11.95 -by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def]));
   11.96 +by (res_inst_tac 
   11.97 +    [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1);
   11.98 +by (auto_tac (claset(), simpset() addsimps 
   11.99 +    [isLub_def,leastP_def,isUb_def]));
  11.100  by (auto_tac (claset() addSIs [setleI,setgeI] 
  11.101 -	               addSDs [real_gt_zero_preal_Ex RS iffD1],
  11.102 -	      simpset()));
  11.103 +     addSDs [(rename_numerals thy real_gt_zero_preal_Ex)
  11.104 +     RS iffD1],simpset()));
  11.105  by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
  11.106 -by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
  11.107 +by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
  11.108  by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
  11.109  by (rtac preal_psup_leI2a 1);
  11.110  by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1);
  11.111 @@ -111,7 +117,7 @@
  11.112  by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1);
  11.113  by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
  11.114  by (ftac isUbD2 1);
  11.115 -by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
  11.116 +by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
  11.117  by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
  11.118  	      simpset() addsimps [real_of_preal_le_iff]));
  11.119  by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] 
  11.120 @@ -122,63 +128,49 @@
  11.121  (*-------------------------------
  11.122      Lemmas
  11.123   -------------------------------*)
  11.124 -Goal "! y : {z. ? x: P. z = x + (-xa) + 1r} Int {x. 0r < x}. 0r < y";
  11.125 +Goal "! y : {z. ? x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y";
  11.126  by Auto_tac;
  11.127  qed "real_sup_lemma3";
  11.128   
  11.129  Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))";
  11.130 -by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
  11.131 -	                         real_add_ac) 1);
  11.132 +by (Auto_tac);
  11.133  qed "lemma_le_swap2";
  11.134  
  11.135 -Goal "[| 0r < x + (-X) + 1r; x < xa |] ==> 0r < xa + (-X) + 1r";
  11.136 -by (dtac real_add_less_mono 1);
  11.137 -by (assume_tac 1);
  11.138 -by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1);
  11.139 -by (asm_full_simp_tac
  11.140 -    (simpset() addsimps [real_add_zero_right, real_add_assoc RS sym,
  11.141 -			 real_add_minus_left,real_add_zero_left]) 1);
  11.142 +Goal "[| #0 < (x::real) + (-X) + #1; x < xa |] ==> #0 < xa + (-X) + #1";
  11.143 +by (Auto_tac);
  11.144  qed "lemma_real_complete1";
  11.145  
  11.146 -Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa + (-X) + 1r <= S";
  11.147 -by (dtac real_less_imp_le 1);
  11.148 -by (dtac real_add_le_mono 1);
  11.149 -by (assume_tac 1);
  11.150 -by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
  11.151 +Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa + (-X) + #1 <= S";
  11.152 +by (Auto_tac);
  11.153  qed "lemma_real_complete2";
  11.154  
  11.155 -Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa <= S + X + (-1r)"; (**)
  11.156 -by (rtac (lemma_le_swap2 RS iffD2) 1);
  11.157 -by (etac lemma_real_complete2 1);
  11.158 -by (assume_tac 1);
  11.159 +Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa <= S + X + (-#1)"; (**)
  11.160 +by (Auto_tac);
  11.161  qed "lemma_real_complete2a";
  11.162  
  11.163 -Goal "[| x + (-X) + 1r <= S; xa <= x |] ==> xa <= S + X + (-1r)";
  11.164 -by (rotate_tac 1 1);
  11.165 -by (etac (real_le_imp_less_or_eq RS disjE) 1);
  11.166 -by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
  11.167 -by (blast_tac (claset() addIs [(lemma_le_swap2 RS iffD2)]) 1);
  11.168 +Goal "[| (x::real) + (-X) + #1 <= S; xa <= x |] ==> xa <= S + X + (-#1)";
  11.169 +by (Auto_tac);
  11.170  qed "lemma_real_complete2b";
  11.171  
  11.172 -(*------------------------------------
  11.173 +(*----------------------------------------------------------
  11.174        reals Completeness (again!)
  11.175 - ------------------------------------*)
  11.176 + ----------------------------------------------------------*)
  11.177  Goal "[| EX X. X: S;  EX Y. isUb (UNIV::real set) S Y |]  \
  11.178  \     ==> EX t. isLub (UNIV :: real set) S t";
  11.179  by (Step_tac 1);
  11.180 -by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + 1r} \
  11.181 -\                Int {x. 0r < x}" 1);
  11.182 -by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + 1r} \
  11.183 -\                Int {x. 0r < x})  (Y + (-X) + 1r)" 1); 
  11.184 +by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + #1} \
  11.185 +\                Int {x. #0 < x}" 1);
  11.186 +by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + #1} \
  11.187 +\                Int {x. #0 < x})  (Y + (-X) + #1)" 1); 
  11.188  by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
  11.189  by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, 
  11.190  	   Step_tac]);
  11.191 -by (res_inst_tac [("x","t + X + (-1r)")] exI 1);
  11.192 +by (res_inst_tac [("x","t + X + (-#1)")] exI 1);
  11.193  by (rtac isLubI2 1);
  11.194  by (rtac setgeI 2 THEN Step_tac 2);
  11.195 -by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + 1r} \
  11.196 -\                Int {x. 0r < x})  (y + (-X) + 1r)" 2); 
  11.197 -by (dres_inst_tac [("y","(y + (- X) + 1r)")] isLub_le_isUb 2 
  11.198 +by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + #1} \
  11.199 +\                Int {x. #0 < x})  (y + (-X) + #1)" 2); 
  11.200 +by (dres_inst_tac [("y","(y + (- X) + #1)")] isLub_le_isUb 2 
  11.201        THEN assume_tac 2);
  11.202  by (full_simp_tac
  11.203      (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
  11.204 @@ -202,21 +194,19 @@
  11.205                          addIs [real_add_le_mono1]) 1);
  11.206  by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
  11.207                          addIs [real_add_le_mono1]) 1);
  11.208 -by (auto_tac (claset(),
  11.209 -	      simpset() addsimps [real_add_assoc RS sym,
  11.210 -				  real_zero_less_one]));
  11.211 +by (Auto_tac);
  11.212  qed "reals_complete";
  11.213  
  11.214  (*----------------------------------------------------------------
  11.215          Related: Archimedean property of reals
  11.216   ----------------------------------------------------------------*)
  11.217  
  11.218 -Goal "0r < x ==> EX n. rinv(real_of_posnat n) < x";
  11.219 +Goal "#0 < x ==> EX n. rinv(real_of_posnat n) < x";
  11.220  by (stac real_of_posnat_rinv_Ex_iff 1);
  11.221  by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
  11.222  by (fold_tac [real_le_def]);
  11.223  by (subgoal_tac "isUb (UNIV::real set) \
  11.224 -\   {z. EX n. z = x*(real_of_posnat n)} 1r" 1);
  11.225 +\   {z. EX n. z = x*(real_of_posnat n)} #1" 1);
  11.226  by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1);
  11.227  by (dtac reals_complete 1);
  11.228  by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
  11.229 @@ -237,19 +227,22 @@
  11.230  qed "reals_Archimedean";
  11.231  
  11.232  Goal "EX n. (x::real) < real_of_posnat n";
  11.233 -by (res_inst_tac [("R1.0","x"),("R2.0","0r")] real_linear_less2 1);
  11.234 +by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1);
  11.235  by (res_inst_tac [("x","0")] exI 1);
  11.236  by (res_inst_tac [("x","0")] exI 2);
  11.237  by (auto_tac (claset() addEs [real_less_trans],
  11.238  	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
  11.239 -by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1);
  11.240 +by (forward_tac [((full_rename_numerals thy real_rinv_gt_zero)
  11.241 +     RS reals_Archimedean)] 1);
  11.242  by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
  11.243 -by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1);
  11.244 +by (forw_inst_tac [("y","rinv x")] 
  11.245 +    (full_rename_numerals thy real_mult_less_mono1) 1);
  11.246  by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
  11.247 -by (dres_inst_tac [("n1","n"),("y","1r")] 
  11.248 +by (dres_inst_tac [("n1","n"),("y","#1")] 
  11.249       (real_of_posnat_less_zero RS real_mult_less_mono2)  1);
  11.250  by (auto_tac (claset(),
  11.251 -	      simpset() addsimps [real_of_posnat_less_zero,
  11.252 +	      simpset() addsimps [rename_numerals thy 
  11.253 +                                  real_of_posnat_less_zero,
  11.254  				  real_not_refl2 RS not_sym,
  11.255  				  real_mult_assoc RS sym]));
  11.256  qed "reals_Archimedean2";
    12.1 --- a/src/HOL/Real/ROOT.ML	Wed May 31 18:06:02 2000 +0200
    12.2 +++ b/src/HOL/Real/ROOT.ML	Thu Jun 01 11:22:27 2000 +0200
    12.3 @@ -12,7 +12,3 @@
    12.4  use          "simproc.ML";
    12.5  time_use_thy "Real";
    12.6  time_use_thy "Hyperreal/HyperDef";
    12.7 -
    12.8 -(*FIXME: move to RealBin and eliminate all references to 0r, 1r in 
    12.9 -  descendant theories*)
   12.10 -Addsimps [zero_eq_numeral_0, one_eq_numeral_1];
    13.1 --- a/src/HOL/Real/RealAbs.ML	Wed May 31 18:06:02 2000 +0200
    13.2 +++ b/src/HOL/Real/RealAbs.ML	Thu Jun 01 11:22:27 2000 +0200
    13.3 @@ -5,53 +5,76 @@
    13.4      Description : Absolute value function for the reals
    13.5  *) 
    13.6  
    13.7 +
    13.8 +(** abs (absolute value) **)
    13.9 +
   13.10 +Goalw [abs_real_def]
   13.11 +     "abs (number_of v :: real) = \
   13.12 +\       (if neg (number_of v) then number_of (bin_minus v) \
   13.13 +\        else number_of v)";
   13.14 +by (simp_tac
   13.15 +    (simpset_of Int.thy addsimps
   13.16 +      bin_arith_simps@
   13.17 +      [minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less,
   13.18 +       less_real_number_of, real_of_int_le_iff]) 1);
   13.19 +qed "abs_nat_number_of";
   13.20 +
   13.21 +Addsimps [abs_nat_number_of];
   13.22 +
   13.23 +Goalw [abs_real_def]
   13.24 +  "P(abs (x::real)) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))";
   13.25 +by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
   13.26 +qed "abs_split";
   13.27 +
   13.28 +arith_tac_split_thms := !arith_tac_split_thms @ [abs_split];
   13.29 +
   13.30  (*----------------------------------------------------------------------------
   13.31         Properties of the absolute value function over the reals
   13.32         (adapted version of previously proved theorems about abs)
   13.33   ----------------------------------------------------------------------------*)
   13.34 -Goalw [abs_real_def] "abs r = (if 0r<=r then r else -r)";
   13.35 +
   13.36 +Goalw [abs_real_def] "abs (r::real) = (if #0<=r then r else -r)";
   13.37  by Auto_tac;
   13.38  qed "abs_iff";
   13.39  
   13.40 -Goalw [abs_real_def] "abs 0r = 0r";
   13.41 -by (rtac (real_le_refl RS if_P) 1);
   13.42 +Goalw [abs_real_def] "abs #0 = (#0::real)";
   13.43 +by Auto_tac;
   13.44  qed "abs_zero";
   13.45 -
   13.46  Addsimps [abs_zero];
   13.47  
   13.48 -Goalw [abs_real_def] "abs 0r = -0r";
   13.49 +Goalw [abs_real_def] "abs (#0::real) = -#0";
   13.50  by (Simp_tac 1);
   13.51  qed "abs_minus_zero";
   13.52  
   13.53 -Goalw [abs_real_def] "0r<=x ==> abs x = x";
   13.54 +Goalw [abs_real_def] "(#0::real)<=x ==> abs x = x";
   13.55  by (Asm_simp_tac 1);
   13.56  qed "abs_eqI1";
   13.57  
   13.58 -Goalw [abs_real_def] "0r<x ==> abs x = x";
   13.59 +Goalw [abs_real_def] "(#0::real)<x ==> abs x = x";
   13.60  by (Asm_simp_tac 1);
   13.61  qed "abs_eqI2";
   13.62  
   13.63 -Goalw [abs_real_def,real_le_def] "x<0r ==> abs x = -x";
   13.64 +Goalw [abs_real_def,real_le_def] "x<(#0::real) ==> abs x = -x";
   13.65  by (Asm_simp_tac 1);
   13.66  qed "abs_minus_eqI2";
   13.67  
   13.68 -Goalw [abs_real_def] "x<=0r ==> abs x = -x";
   13.69 -by (asm_full_simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   13.70 +Goalw [abs_real_def] "x<=(#0::real) ==> abs x = -x";
   13.71 +by (Asm_simp_tac 1);
   13.72  qed "abs_minus_eqI1";
   13.73  
   13.74 -Goalw [abs_real_def] "0r<= abs x";
   13.75 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   13.76 +Goalw [abs_real_def] "(#0::real)<= abs x";
   13.77 +by (Simp_tac 1);
   13.78  qed "abs_ge_zero";
   13.79  
   13.80  Goalw [abs_real_def] "abs(abs x)=abs (x::real)";
   13.81 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   13.82 +by (Simp_tac 1);
   13.83  qed "abs_idempotent";
   13.84  
   13.85 -Goalw [abs_real_def] "(x=0r) = (abs x = 0r)";
   13.86 +Goalw [abs_real_def] "(x=(#0::real)) = (abs x = #0)";
   13.87  by (Full_simp_tac 1);
   13.88  qed "abs_zero_iff";
   13.89  
   13.90 -Goal  "(x ~= 0r) = (abs x ~= 0r)";
   13.91 +Goal  "(x ~= (#0::real)) = (abs x ~= #0)";
   13.92  by (full_simp_tac (simpset() addsimps [abs_zero_iff RS sym]) 1);
   13.93  qed "abs_not_zero_iff";
   13.94  
   13.95 @@ -68,32 +91,32 @@
   13.96  by (auto_tac (claset(),
   13.97  	      simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute,
   13.98  				  real_minus_mult_eq2]));
   13.99 -by (blast_tac (claset() addDs [real_le_mult_order]) 1);
  13.100 +by (blast_tac (claset() addDs [full_rename_numerals thy real_le_mult_order]) 1);
  13.101  by (auto_tac (claset() addSDs [not_real_leE], simpset()));
  13.102 -by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]);
  13.103 -by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]);
  13.104 -by (dtac real_mult_less_zero1 5 THEN assume_tac 5);
  13.105 +by (EVERY1[dtac (full_rename_numerals thy real_mult_le_zero), 
  13.106 +    assume_tac, dtac real_le_anti_sym]);
  13.107 +by (EVERY[dtac (full_rename_numerals thy real_mult_le_zero) 3,
  13.108 +     assume_tac 3, dtac real_le_anti_sym 3]);
  13.109 +by (dtac (full_rename_numerals thy real_mult_less_zero1) 5 THEN assume_tac 5);
  13.110  by (auto_tac (claset() addDs [real_less_asym,sym],
  13.111  	      simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
  13.112  qed "abs_mult";
  13.113  
  13.114 -Goalw [abs_real_def] "x~= 0r ==> abs(rinv(x)) = rinv(abs(x))";
  13.115 -by (auto_tac (claset(), simpset() addsimps [real_minus_rinv]));
  13.116 -by (ALLGOALS(dtac not_real_leE));
  13.117 -by (etac real_less_asym 1);
  13.118 -by (blast_tac (claset() addDs [real_le_imp_less_or_eq, real_rinv_gt_zero]) 1);
  13.119 -by (dtac (rinv_not_zero RS not_sym) 1);
  13.120 -by (rtac (real_rinv_less_zero RSN (2,real_less_asym)) 1);
  13.121 -by (assume_tac 2);
  13.122 -by (blast_tac (claset() addSDs [real_le_imp_less_or_eq]) 1);
  13.123 +Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))";
  13.124 +by (auto_tac (claset(), simpset() addsimps [real_le_less] @ 
  13.125 +    (map (full_rename_numerals thy) [real_minus_rinv,
  13.126 +    real_rinv_gt_zero])));
  13.127 +by (etac (full_rename_numerals thy (real_rinv_less_zero 
  13.128 +    RSN (2,real_less_asym))) 1);
  13.129 +by (arith_tac 1);
  13.130  qed "abs_rinv";
  13.131  
  13.132 -Goal "y ~= 0r ==> abs(x*rinv(y)) = abs(x)*rinv(abs(y))";
  13.133 +Goal "y ~= #0 ==> abs(x*rinv(y)) = abs(x)*rinv(abs(y))";
  13.134  by (asm_simp_tac (simpset() addsimps [abs_mult, abs_rinv]) 1);
  13.135  qed "abs_mult_rinv";
  13.136  
  13.137  Goalw [abs_real_def] "abs(x+y) <= abs x + abs (y::real)";
  13.138 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
  13.139 +by (Simp_tac 1);
  13.140  qed "abs_triangle_ineq";
  13.141  
  13.142  (*Unused, but perhaps interesting as an example*)
  13.143 @@ -102,52 +125,49 @@
  13.144  qed "abs_triangle_ineq_four";
  13.145  
  13.146  Goalw [abs_real_def] "abs(-x)=abs(x::real)";
  13.147 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
  13.148 +by (Simp_tac 1);
  13.149  qed "abs_minus_cancel";
  13.150  
  13.151  Goalw [abs_real_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
  13.152 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
  13.153 +by (Simp_tac 1);
  13.154  qed "abs_minus_add_cancel";
  13.155  
  13.156  Goalw [abs_real_def] "abs(x + (-y)) <= abs x + abs (y::real)";
  13.157 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
  13.158 +by (Simp_tac 1);
  13.159  qed "abs_triangle_minus_ineq";
  13.160  
  13.161  Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)";
  13.162 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
  13.163 +by (Simp_tac 1);
  13.164  qed_spec_mp "abs_add_less";
  13.165  
  13.166  Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)";
  13.167 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
  13.168 +by (Simp_tac 1);
  13.169  qed "abs_add_minus_less";
  13.170  
  13.171  (* lemmas manipulating terms *)
  13.172 -Goal "(0r*x<r)=(0r<r)";
  13.173 +Goal "((#0::real)*x<r)=(#0<r)";
  13.174  by (Simp_tac 1);
  13.175  qed "real_mult_0_less";
  13.176  
  13.177 -Goal "[| 0r<y; x<r; y*r<t*s |] ==> y*x<t*s";
  13.178 -by (blast_tac (claset() addSIs [real_mult_less_mono2]
  13.179 -	                addIs  [real_less_trans]) 1);
  13.180 +Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s";
  13.181 +by (blast_tac (claset() addSIs [full_rename_numerals thy 
  13.182 +    real_mult_less_mono2] addIs  [real_less_trans]) 1);
  13.183  qed "real_mult_less_trans";
  13.184  
  13.185 -Goal "[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s";
  13.186 +Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s";
  13.187  by (dtac real_le_imp_less_or_eq 1);
  13.188  by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
  13.189  			    real_mult_less_trans]) 1);
  13.190  qed "real_mult_le_less_trans";
  13.191  
  13.192 -(* proofs lifted from previous older version
  13.193 -   FIXME: use a stronger version of real_mult_less_mono *)
  13.194  Goal "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::real)";
  13.195  by (simp_tac (simpset() addsimps [abs_mult]) 1);
  13.196  by (rtac real_mult_le_less_trans 1);
  13.197  by (rtac abs_ge_zero 1);
  13.198  by (assume_tac 1);
  13.199 -by (blast_tac (HOL_cs addIs [abs_ge_zero, real_mult_less_mono1, 
  13.200 -			     real_le_less_trans]) 1);
  13.201 -by (blast_tac (HOL_cs addIs [abs_ge_zero, real_mult_order, 
  13.202 -			     real_le_less_trans]) 1);
  13.203 +by (rtac (full_rename_numerals thy real_mult_order) 2);
  13.204 +by (auto_tac (claset() addSIs [real_mult_less_mono1,
  13.205 +    abs_ge_zero] addIs [real_le_less_trans],simpset()));
  13.206  qed "abs_mult_less";
  13.207  
  13.208  Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)";
  13.209 @@ -155,52 +175,112 @@
  13.210                simpset() addsimps [abs_mult RS sym]));
  13.211  qed "abs_mult_less2";
  13.212  
  13.213 -Goal "1r < abs x ==> abs y <= abs(x*y)";
  13.214 +Goal "(#1::real) < abs x ==> abs y <= abs(x*y)";
  13.215  by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1);
  13.216  by (EVERY1[etac disjE,rtac real_less_imp_le]);
  13.217 -by (dres_inst_tac [("W","1r")]  real_less_sum_gt_zero 1);
  13.218 -by (forw_inst_tac [("y","abs x + (-1r)")] real_mult_order 1);
  13.219 -by (assume_tac 1);
  13.220 -by (rtac real_sum_gt_zero_less 1);
  13.221 -by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
  13.222 -					   real_mult_commute, abs_mult]) 1);
  13.223 -by (dtac sym 1);
  13.224 -by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1);
  13.225 +by (dres_inst_tac [("W","#1")]  real_less_sum_gt_zero 1);
  13.226 +by (forw_inst_tac [("y","abs x + (-#1)")] (full_rename_numerals thy
  13.227 +    real_mult_order) 1);
  13.228 +by (rtac real_sum_gt_zero_less 2);
  13.229 +by (asm_full_simp_tac (simpset() 
  13.230 +    addsimps [real_add_mult_distrib2,
  13.231 +    real_mult_commute, abs_mult]) 2);
  13.232 +by (dtac sym 2);
  13.233 +by (auto_tac (claset(),simpset() addsimps [abs_mult]));
  13.234  qed "abs_mult_le";
  13.235  
  13.236 -Goal "[| 1r < abs x; r < abs y|] ==> r < abs(x*y)";
  13.237 +Goal "[| (#1::real) < abs x; r < abs y|] ==> r < abs(x*y)";
  13.238  by (blast_tac (HOL_cs addIs [abs_mult_le, real_less_le_trans]) 1);
  13.239  qed "abs_mult_gt";
  13.240  
  13.241 -Goal "abs(x)<r ==> 0r<r";
  13.242 +Goal "abs(x)<r ==> (#0::real)<r";
  13.243  by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1);
  13.244  qed "abs_less_gt_zero";
  13.245  
  13.246 -Goalw [abs_real_def] "abs 1r = 1r";
  13.247 -by (simp_tac (simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]) 1);
  13.248 +Goalw [abs_real_def] "abs #1 = (#1::real)";
  13.249 +by (Simp_tac 1);
  13.250  qed "abs_one";
  13.251  
  13.252 +Goalw [abs_real_def] "abs (-#1) = (#1::real)";
  13.253 +by (Simp_tac 1);
  13.254 +qed "abs_minus_one";
  13.255 +Addsimps [abs_minus_one];
  13.256 +
  13.257  Goalw [abs_real_def] "abs x =x | abs x = -(x::real)";
  13.258 -by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
  13.259 +by Auto_tac;
  13.260  qed "abs_disj";
  13.261  
  13.262  Goalw [abs_real_def] "(abs x < r) = (-r<x & x<(r::real))";
  13.263 -by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
  13.264 +by Auto_tac;
  13.265  qed "abs_interval_iff";
  13.266  
  13.267  Goalw [abs_real_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
  13.268 -by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
  13.269 +by Auto_tac;
  13.270  qed "abs_le_interval_iff";
  13.271  
  13.272  Goalw [abs_real_def] "(abs (x + (-y)) < r) = (y + (-r) < x & x < y + (r::real))";
  13.273 -by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
  13.274 +by Auto_tac;
  13.275  qed "abs_add_minus_interval_iff";
  13.276  
  13.277 -Goalw [abs_real_def] "0r < k ==> 0r < k + abs(x)";
  13.278 -by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
  13.279 +Goalw [abs_real_def] "(#0::real) < k ==> #0 < k + abs(x)";
  13.280 +by Auto_tac;
  13.281  qed "abs_add_pos_gt_zero";
  13.282  
  13.283 -Goalw [abs_real_def] "0r < 1r + abs(x)";
  13.284 -by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]));
  13.285 +Goalw [abs_real_def] "(#0::real) < #1 + abs(x)";
  13.286 +by Auto_tac;
  13.287  qed "abs_add_one_gt_zero";
  13.288  Addsimps [abs_add_one_gt_zero];
  13.289 +
  13.290 +(* 05/2000 *)
  13.291 +Goalw [abs_real_def] "~ abs x < (#0::real)";
  13.292 +by Auto_tac;
  13.293 +qed "abs_not_less_zero";
  13.294 +Addsimps [abs_not_less_zero];
  13.295 +
  13.296 +Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)";
  13.297 +by (auto_tac (claset() addIs [abs_triangle_ineq RS real_le_less_trans], 
  13.298 +    simpset()));
  13.299 +qed "abs_circle";
  13.300 +
  13.301 +Goalw [abs_real_def] "(abs x <= (#0::real)) = (x = #0)";
  13.302 +by Auto_tac;
  13.303 +qed "abs_le_zero_iff";
  13.304 +Addsimps [abs_le_zero_iff];
  13.305 +
  13.306 +Goal "abs (real_of_nat x) = real_of_nat x";
  13.307 +by (auto_tac (claset() addIs [abs_eqI1],simpset()
  13.308 +    addsimps [rename_numerals thy real_of_nat_ge_zero]));
  13.309 +qed "abs_real_of_nat_cancel";
  13.310 +Addsimps [abs_real_of_nat_cancel];
  13.311 +
  13.312 +Goal "~ abs(x) + (#1::real) < x";
  13.313 +by (rtac real_leD 1);
  13.314 +by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans],simpset()));
  13.315 +qed "abs_add_one_not_less_self";
  13.316 +Addsimps [abs_add_one_not_less_self];
  13.317 +
  13.318 +(* used in vector theory *)
  13.319 +Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)";
  13.320 +by (auto_tac (claset() addSIs [(abs_triangle_ineq 
  13.321 +    RS real_le_trans),real_add_left_le_mono1],
  13.322 +    simpset() addsimps [real_add_assoc]));
  13.323 +qed "abs_triangle_ineq_three";
  13.324 +
  13.325 +Goalw [abs_real_def] "abs(x - y) < y ==> (#0::real) < y";
  13.326 +by (case_tac "#0 <= x - y" 1);
  13.327 +by (Auto_tac);
  13.328 +qed "abs_diff_less_imp_gt_zero";
  13.329 +
  13.330 +Goalw [abs_real_def] "abs(x - y) < x ==> (#0::real) < x";
  13.331 +by (case_tac "#0 <= x - y" 1);
  13.332 +by (Auto_tac);
  13.333 +qed "abs_diff_less_imp_gt_zero2";
  13.334 +
  13.335 +Goal "abs(x - y) < y ==> (#0::real) < x";
  13.336 +by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
  13.337 +qed "abs_diff_less_imp_gt_zero3";
  13.338 +
  13.339 +Goal "abs(x - y) < -y ==> x < (#0::real)";
  13.340 +by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
  13.341 +qed "abs_diff_less_imp_gt_zero4";
  13.342 +
    14.1 --- a/src/HOL/Real/RealAbs.thy	Wed May 31 18:06:02 2000 +0200
    14.2 +++ b/src/HOL/Real/RealAbs.thy	Thu Jun 01 11:22:27 2000 +0200
    14.3 @@ -7,4 +7,8 @@
    14.4  
    14.5  RealAbs = RealBin +
    14.6  
    14.7 +
    14.8 +defs
    14.9 +  abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
   14.10 +
   14.11  end
    15.1 --- a/src/HOL/Real/RealBin.ML	Wed May 31 18:06:02 2000 +0200
    15.2 +++ b/src/HOL/Real/RealBin.ML	Thu Jun 01 11:22:27 2000 +0200
    15.3 @@ -109,23 +109,6 @@
    15.4  
    15.5  Addsimps [le_real_number_of_eq_not_less];
    15.6  
    15.7 -
    15.8 -(** abs (absolute value) **)
    15.9 -
   15.10 -Goalw [abs_real_def]
   15.11 -     "abs (number_of v :: real) = \
   15.12 -\       (if neg (number_of v) then number_of (bin_minus v) \
   15.13 -\        else number_of v)";
   15.14 -by (simp_tac
   15.15 -    (simpset_of Int.thy addsimps
   15.16 -      bin_arith_simps@
   15.17 -      [minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less,
   15.18 -       less_real_number_of, real_of_int_le_iff]) 1);
   15.19 -qed "abs_nat_number_of";
   15.20 -
   15.21 -Addsimps [abs_nat_number_of];
   15.22 -
   15.23 -
   15.24  (*** New versions of existing theorems involving 0r, 1r ***)
   15.25  
   15.26  Goal "- #1 = (#-1::real)";
   15.27 @@ -209,11 +192,12 @@
   15.28  in
   15.29  Addsimprocs [fast_real_arith_simproc]
   15.30  end;
   15.31 + 
   15.32  
   15.33 -Goalw [abs_real_def]
   15.34 -  "P(abs (x::real)) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))";
   15.35 -by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
   15.36 -qed "abs_split";
   15.37 +Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
   15.38  
   15.39 -arith_tac_split_thms := !arith_tac_split_thms @ [abs_split];
   15.40 +(* added by jdf *)
   15.41 +fun full_rename_numerals thy th = 
   15.42 +    asm_full_simplify real_numeral_ss (change_theory thy th);
   15.43  
   15.44 +
    16.1 --- a/src/HOL/Real/RealOrd.ML	Wed May 31 18:06:02 2000 +0200
    16.2 +++ b/src/HOL/Real/RealOrd.ML	Thu Jun 01 11:22:27 2000 +0200
    16.3 @@ -1,7 +1,6 @@
    16.4  (*  Title:       HOL/Real/Real.ML
    16.5      ID:          $Id$
    16.6 -    Author:      Lawrence C. Paulson
    16.7 -                 Jacques D. Fleuriot
    16.8 +    Author:      Jacques D. Fleuriot and Lawrence C. Paulson
    16.9      Copyright:   1998  University of Cambridge
   16.10      Description: Type "real" is a linear order
   16.11  *)
   16.12 @@ -434,6 +433,26 @@
   16.13  
   16.14  Addsimps [real_mult_less_iff1,real_mult_less_iff2];
   16.15  
   16.16 +(* 05/00 *)
   16.17 +Goalw [real_le_def] "[| 0r<z; x*z<=y*z |] ==> x<=y";
   16.18 +by (Auto_tac);
   16.19 +qed "real_mult_le_cancel1";
   16.20 +
   16.21 +Goalw [real_le_def] "!!(x::real). [| 0r<z; z*x<=z*y |] ==> x<=y";
   16.22 +by (Auto_tac);
   16.23 +qed "real_mult_le_cancel2";
   16.24 +
   16.25 +Goalw [real_le_def] "0r < z ==> (x*z <= y*z) = (x <= y)";
   16.26 +by (Auto_tac);
   16.27 +qed "real_mult_le_cancel_iff1";
   16.28 +
   16.29 +Goalw [real_le_def] "0r < z ==> (z*x <= z*y) = (x <= y)";
   16.30 +by (Auto_tac);
   16.31 +qed "real_mult_le_cancel_iff2";
   16.32 +
   16.33 +Addsimps [real_mult_le_cancel_iff1,real_mult_le_cancel_iff2];
   16.34 +
   16.35 +
   16.36  Goal "[| 0r<=z; x<y |] ==> x*z<=y*z";
   16.37  by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
   16.38  by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
   16.39 @@ -720,6 +739,34 @@
   16.40  by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   16.41  qed "real_rinv_add";
   16.42  
   16.43 +(* 05/00 *)
   16.44 +Goal "(0r <= -R) = (R <= 0r)";
   16.45 +by (auto_tac (claset() addDs [sym],
   16.46 +    simpset() addsimps [real_le_less]));
   16.47 +qed "real_minus_zero_le_iff";
   16.48 +
   16.49 +Goal "(-R <= 0r) = (0r <= R)";
   16.50 +by (auto_tac (claset(),simpset() addsimps 
   16.51 +    [real_minus_zero_less_iff2,real_le_less]));
   16.52 +qed "real_minus_zero_le_iff2";
   16.53 +
   16.54 +Goal "-(x*x) <= 0r";
   16.55 +by (simp_tac (simpset() addsimps [real_minus_zero_le_iff2]) 1);
   16.56 +qed "real_minus_squre_le_zero";
   16.57 +Addsimps [real_minus_squre_le_zero];
   16.58 +
   16.59 +Goal "x * x + y * y = 0r ==> x = 0r";
   16.60 +by (dtac real_add_minus_eq_minus 1);
   16.61 +by (cut_inst_tac [("x","x")] real_le_square 1);
   16.62 +by (Auto_tac THEN dtac real_le_anti_sym 1);
   16.63 +by (auto_tac (claset() addDs [real_mult_zero_disj],simpset()));
   16.64 +qed "real_sum_squares_cancel";
   16.65 +
   16.66 +Goal "x * x + y * y = 0r ==> y = 0r";
   16.67 +by (res_inst_tac [("y","x")] real_sum_squares_cancel 1);
   16.68 +by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   16.69 +qed "real_sum_squares_cancel2";
   16.70 +
   16.71  (*----------------------------------------------------------------------------
   16.72       Another embedding of the naturals in the reals (see real_of_posnat)
   16.73   ----------------------------------------------------------------------------*)
   16.74 @@ -780,3 +827,27 @@
   16.75  	      simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc, 
   16.76  				  real_of_nat_zero] @ real_add_ac));
   16.77  qed_spec_mp "real_of_nat_minus";
   16.78 +
   16.79 +(* 05/00 *)
   16.80 +Goal "n2 < n1 ==> real_of_nat (n1 - n2) = \
   16.81 +\     real_of_nat n1 + -real_of_nat n2";
   16.82 +by (auto_tac (claset() addIs [real_of_nat_minus],simpset()));
   16.83 +qed "real_of_nat_minus2";
   16.84 +
   16.85 +Goalw [real_diff_def] "n2 < n1 ==> real_of_nat (n1 - n2) = \
   16.86 +\     real_of_nat n1 - real_of_nat n2";
   16.87 +by (etac real_of_nat_minus2 1);
   16.88 +qed "real_of_nat_diff";
   16.89 +
   16.90 +Goalw [real_diff_def] "n2 <= n1 ==> real_of_nat (n1 - n2) = \
   16.91 +\     real_of_nat n1 - real_of_nat n2";
   16.92 +by (etac real_of_nat_minus 1);
   16.93 +qed "real_of_nat_diff2";
   16.94 +
   16.95 +Goal "(real_of_nat n ~= 0r) = (n ~= 0)";
   16.96 +by (auto_tac (claset() addIs [inj_real_of_nat RS injD],
   16.97 +    simpset() addsimps [real_of_nat_zero RS sym] 
   16.98 +    delsimps [neq0_conv]));
   16.99 +qed "real_of_nat_not_zero_iff";
  16.100 +Addsimps [real_of_nat_not_zero_iff];
  16.101 +
    17.1 --- a/src/HOL/Real/RealOrd.thy	Wed May 31 18:06:02 2000 +0200
    17.2 +++ b/src/HOL/Real/RealOrd.thy	Thu Jun 01 11:22:27 2000 +0200
    17.3 @@ -1,7 +1,6 @@
    17.4 -(*  Title:	Real/RealOrd.thy
    17.5 -    ID: 	$Id$
    17.6 -    Author:     Lawrence C. Paulson
    17.7 -                Jacques D. Fleuriot
    17.8 +(*  Title:	 Real/RealOrd.thy
    17.9 +    ID: 	 $Id$
   17.10 +    Author:      Jacques D. Fleuriot and Lawrence C. Paulson
   17.11      Copyright:   1998  University of Cambridge
   17.12      Description: Type "real" is a linear order
   17.13  *)
   17.14 @@ -11,7 +10,4 @@
   17.15  instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
   17.16  instance real :: linorder (real_le_linear)
   17.17  
   17.18 -defs
   17.19 -  abs_real_def "abs r == (if 0r <= r then r else -r)"
   17.20 -
   17.21  end
    18.1 --- a/src/HOL/Real/RealPow.ML	Wed May 31 18:06:02 2000 +0200
    18.2 +++ b/src/HOL/Real/RealPow.ML	Thu Jun 01 11:22:27 2000 +0200
    18.3 @@ -3,31 +3,30 @@
    18.4      Author      : Jacques D. Fleuriot  
    18.5      Copyright   : 1998  University of Cambridge
    18.6      Description : Natural Powers of reals theory
    18.7 -
    18.8  *)
    18.9  
   18.10 -Goal "0r ^ (Suc n) = 0r";
   18.11 +Goal "(#0::real) ^ (Suc n) = #0";
   18.12  by (Auto_tac);
   18.13  qed "realpow_zero";
   18.14  Addsimps [realpow_zero];
   18.15  
   18.16 -Goal "r ~= 0r --> r ^ n ~= 0r";
   18.17 +Goal "r ~= (#0::real) --> r ^ n ~= #0";
   18.18  by (induct_tac "n" 1);
   18.19  by (auto_tac (claset() addIs [real_mult_not_zeroE],
   18.20      simpset() addsimps [real_zero_not_eq_one RS not_sym]));
   18.21  qed_spec_mp "realpow_not_zero";
   18.22  
   18.23 -Goal "r ^ n = 0r ==> r = 0r";
   18.24 -by (blast_tac (claset() addIs [ccontr] 
   18.25 -    addDs [realpow_not_zero]) 1);
   18.26 +Goal "r ^ n = (#0::real) ==> r = #0";
   18.27 +by (rtac ccontr 1);
   18.28 +by (auto_tac (claset() addDs [realpow_not_zero],simpset()));
   18.29  qed "realpow_zero_zero";
   18.30  
   18.31 -Goal "r ~= 0r --> rinv(r ^ n) = (rinv r) ^ n";
   18.32 +Goal "r ~= #0 --> rinv(r ^ n) = (rinv r) ^ n";
   18.33  by (induct_tac "n" 1);
   18.34  by (Auto_tac);
   18.35  by (forw_inst_tac [("n","n")] realpow_not_zero 1);
   18.36 -by (auto_tac (claset() addDs [real_rinv_distrib],
   18.37 -    simpset()));
   18.38 +by (auto_tac (claset() addDs [full_rename_numerals 
   18.39 +    thy real_rinv_distrib],simpset()));
   18.40  qed_spec_mp "realpow_rinv";
   18.41  
   18.42  Goal "abs (r::real) ^ n = abs (r ^ n)";
   18.43 @@ -50,63 +49,58 @@
   18.44  by (Simp_tac 1);
   18.45  qed "realpow_two";
   18.46  
   18.47 -Goal "0r < r --> 0r <= r ^ n";
   18.48 +Goal "(#0::real) < r --> #0 <= r ^ n";
   18.49  by (induct_tac "n" 1);
   18.50  by (auto_tac (claset() addDs [real_less_imp_le] 
   18.51 -    addIs [real_le_mult_order],simpset()));
   18.52 +    addIs [rename_numerals thy real_le_mult_order],simpset()));
   18.53  qed_spec_mp "realpow_ge_zero";
   18.54  
   18.55 -Goal "0r < r --> 0r < r ^ n";
   18.56 +Goal "(#0::real) < r --> #0 < r ^ n";
   18.57  by (induct_tac "n" 1);
   18.58 -by (auto_tac (claset() addIs [real_mult_order],
   18.59 +by (auto_tac (claset() addIs [rename_numerals thy real_mult_order],
   18.60      simpset() addsimps [real_zero_less_one]));
   18.61  qed_spec_mp "realpow_gt_zero";
   18.62  
   18.63 -Goal "0r <= r --> 0r <= r ^ n";
   18.64 +Goal "(#0::real) <= r --> #0 <= r ^ n";
   18.65  by (induct_tac "n" 1);
   18.66 -by (auto_tac (claset() addIs [real_le_mult_order],
   18.67 +by (auto_tac (claset() addIs [rename_numerals thy real_le_mult_order],
   18.68                simpset()));
   18.69  qed_spec_mp "realpow_ge_zero2";
   18.70  
   18.71 -Goal "0r < x & x <= y --> x ^ n <= y ^ n";
   18.72 +Goal "(#0::real) < x & x <= y --> x ^ n <= y ^ n";
   18.73  by (induct_tac "n" 1);
   18.74  by (auto_tac (claset() addSIs [real_mult_le_mono],
   18.75      simpset()));
   18.76  by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
   18.77  qed_spec_mp "realpow_le";
   18.78  
   18.79 -Goal "0r <= x & x <= y --> x ^ n <= y ^ n";
   18.80 +Goal "(#0::real) <= x & x <= y --> x ^ n <= y ^ n";
   18.81  by (induct_tac "n" 1);
   18.82  by (auto_tac (claset() addSIs [real_mult_le_mono4],
   18.83      simpset()));
   18.84  by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
   18.85  qed_spec_mp "realpow_le2";
   18.86  
   18.87 -Goal "0r < x & x < y & 0 < n --> x ^ n < y ^ n";
   18.88 +Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n";
   18.89  by (induct_tac "n" 1);
   18.90 -by (auto_tac (claset() addIs [real_mult_less_mono,
   18.91 -    gr0I] addDs [realpow_gt_zero],simpset()));
   18.92 +by (auto_tac (claset() addIs [full_rename_numerals thy 
   18.93 +    real_mult_less_mono, gr0I] addDs [realpow_gt_zero],
   18.94 +    simpset()));
   18.95  qed_spec_mp "realpow_less";
   18.96  
   18.97 -Goal  "1r ^ n = 1r";
   18.98 +Goal  "#1 ^ n = (#1::real)";
   18.99  by (induct_tac "n" 1);
  18.100  by (Auto_tac);
  18.101  qed "realpow_eq_one";
  18.102  Addsimps [realpow_eq_one];
  18.103  
  18.104 -(** New versions using #0 and #1 instead of 0r and 1r
  18.105 -    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
  18.106 -
  18.107 -Addsimps (map (rename_numerals thy) [realpow_zero, realpow_eq_one]);
  18.108 -
  18.109 -
  18.110 -Goal "abs(-(1r ^ n)) = 1r";
  18.111 +Goal "abs(-(#1 ^ n)) = (#1::real)";
  18.112  by (simp_tac (simpset() addsimps 
  18.113      [abs_minus_cancel,abs_one]) 1);
  18.114  qed "abs_minus_realpow_one";
  18.115  Addsimps [abs_minus_realpow_one];
  18.116  
  18.117 -Goal "abs((-1r) ^ n) = 1r";
  18.118 +Goal "abs((-#1) ^ n) = (#1::real)";
  18.119  by (induct_tac "n" 1);
  18.120  by (auto_tac (claset(),simpset() addsimps [abs_mult,
  18.121           abs_minus_cancel,abs_one]));
  18.122 @@ -118,13 +112,15 @@
  18.123  by (auto_tac (claset(),simpset() addsimps real_mult_ac));
  18.124  qed "realpow_mult";
  18.125  
  18.126 -Goal "0r <= r ^ 2";
  18.127 -by (simp_tac (simpset() addsimps [realpow_two]) 1);
  18.128 +Goal "(#0::real) <= r ^ 2";
  18.129 +by (simp_tac (simpset() addsimps [rename_numerals 
  18.130 +    thy real_le_square]) 1);
  18.131  qed "realpow_two_le";
  18.132  Addsimps [realpow_two_le];
  18.133  
  18.134  Goal "abs((x::real) ^ 2) = x ^ 2";
  18.135 -by (simp_tac (simpset() addsimps [abs_eqI1]) 1);
  18.136 +by (simp_tac (simpset() addsimps [abs_eqI1,
  18.137 +    rename_numerals thy real_le_square]) 1);
  18.138  qed "abs_realpow_two";
  18.139  Addsimps [abs_realpow_two];
  18.140  
  18.141 @@ -134,222 +130,221 @@
  18.142  qed "realpow_two_abs";
  18.143  Addsimps [realpow_two_abs];
  18.144  
  18.145 -Goal "1r < r ==> 1r < r ^ 2";
  18.146 -by (auto_tac (claset(),simpset() addsimps [realpow_two]));
  18.147 -by (cut_facts_tac [real_zero_less_one] 1);
  18.148 -by (forw_inst_tac [("R1.0","0r")] real_less_trans 1);
  18.149 +Goal "(#1::real) < r ==> #1 < r ^ 2";
  18.150 +by Auto_tac;
  18.151 +by (cut_facts_tac [rename_numerals thy real_zero_less_one] 1);
  18.152 +by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
  18.153  by (assume_tac 1);
  18.154 -by (dres_inst_tac [("z","r"),("x","1r")] real_mult_less_mono1 1);
  18.155 +by (dres_inst_tac [("z","r"),("x","#1")] (full_rename_numerals thy 
  18.156 +    real_mult_less_mono1) 1);
  18.157  by (auto_tac (claset() addIs [real_less_trans],simpset()));
  18.158  qed "realpow_two_gt_one";
  18.159  
  18.160 -Goal "1r < r --> 1r <= r ^ n";
  18.161 +Goal "(#1::real) < r --> #1 <= r ^ n";
  18.162  by (induct_tac "n" 1);
  18.163  by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
  18.164  	      simpset()));
  18.165 -by (dtac (real_zero_less_one RS real_mult_less_mono) 1);
  18.166 +by (dtac (full_rename_numerals thy (real_zero_less_one
  18.167 +    RS real_mult_less_mono)) 1);
  18.168 +by (dtac sym 4);
  18.169  by (auto_tac (claset() addSIs [real_less_imp_le],
  18.170  	      simpset() addsimps [real_zero_less_one]));
  18.171  qed_spec_mp "realpow_ge_one";
  18.172  
  18.173 -Goal "1r < r ==> 1r < r ^ (Suc n)";
  18.174 +Goal "(#1::real) < r ==> #1 < r ^ (Suc n)";
  18.175  by (forw_inst_tac [("n","n")] realpow_ge_one 1);
  18.176  by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
  18.177  by (dtac sym 2);
  18.178 -by (forward_tac [real_zero_less_one RS real_less_trans] 1);
  18.179 -by (dres_inst_tac [("y","r ^ n")] real_mult_less_mono2 1);
  18.180 +by (forward_tac [full_rename_numerals thy 
  18.181 +    (real_zero_less_one RS real_less_trans)] 1);
  18.182 +by (dres_inst_tac [("y","r ^ n")] (full_rename_numerals thy 
  18.183 +    real_mult_less_mono2) 1);
  18.184 +by (assume_tac 1);
  18.185  by (auto_tac (claset() addDs [real_less_trans],
  18.186       simpset()));
  18.187  qed "realpow_Suc_gt_one";
  18.188  
  18.189 -Goal "1r <= r ==> 1r <= r ^ n";
  18.190 +Goal "(#1::real) <= r ==> #1 <= r ^ n";
  18.191  by (dtac real_le_imp_less_or_eq 1); 
  18.192  by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
  18.193  qed "realpow_ge_one2";
  18.194  
  18.195 -Goal "0r < r ==> 0r < r ^ Suc n";
  18.196 +Goal "(#0::real) < r ==> #0 < r ^ Suc n";
  18.197  by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
  18.198  by (forw_inst_tac [("n1","n")]
  18.199      ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
  18.200  by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
  18.201 -     addIs [real_mult_order],simpset()));
  18.202 +     addIs [rename_numerals thy real_mult_order],simpset()));
  18.203  qed "realpow_Suc_gt_zero";
  18.204  
  18.205 -Goal "0r <= r ==> 0r <= r ^ Suc n";
  18.206 +Goal "(#0::real) <= r ==> #0 <= r ^ Suc n";
  18.207  by (etac (real_le_imp_less_or_eq RS disjE) 1);
  18.208  by (etac (realpow_ge_zero) 1);
  18.209 +by (dtac sym 1);
  18.210  by (Asm_simp_tac 1);
  18.211  qed "realpow_Suc_ge_zero";
  18.212  
  18.213  Goal "(#1::real) <= #2 ^ n";
  18.214  by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
  18.215  by (rtac realpow_le 2);
  18.216 -by (auto_tac (claset() addIs [real_less_imp_le],
  18.217 -	      simpset() addsimps [zero_eq_numeral_0]));
  18.218 +by (auto_tac (claset() addIs [real_less_imp_le],simpset()));
  18.219  qed "two_realpow_ge_one";
  18.220  
  18.221  Goal "real_of_nat n < #2 ^ n";
  18.222  by (induct_tac "n" 1);
  18.223  by (auto_tac (claset(),
  18.224 -	      simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1,
  18.225 -				  real_mult_2,
  18.226 +	      simpset() addsimps [real_mult_2,
  18.227  				  real_of_nat_Suc, real_of_nat_zero,
  18.228  				  real_add_less_le_mono, two_realpow_ge_one]));
  18.229  qed "two_realpow_gt";
  18.230  Addsimps [two_realpow_gt,two_realpow_ge_one];
  18.231  
  18.232 -Goal "(-1r) ^ (2*n) = 1r";
  18.233 +Goal "(-#1) ^ (2*n) = (#1::real)";
  18.234  by (induct_tac "n" 1);
  18.235  by (Auto_tac);
  18.236  qed "realpow_minus_one";
  18.237  Addsimps [realpow_minus_one];
  18.238  
  18.239 -Goal "(-1r) ^ (n + n) = 1r";
  18.240 +Goal "(-#1) ^ (n + n) = (#1::real)";
  18.241  by (induct_tac "n" 1);
  18.242  by (Auto_tac);
  18.243  qed "realpow_minus_one2";
  18.244  Addsimps [realpow_minus_one2];
  18.245  
  18.246 -Goal "(-1r) ^ Suc (n + n) = -1r";
  18.247 +Goal "(-#1) ^ Suc (n + n) = -(#1::real)";
  18.248  by (induct_tac "n" 1);
  18.249  by (Auto_tac);
  18.250  qed "realpow_minus_one_odd";
  18.251  Addsimps [realpow_minus_one_odd];
  18.252  
  18.253 -Goal "(-1r) ^ Suc (Suc (n + n)) = 1r";
  18.254 +Goal "(-#1) ^ Suc (Suc (n + n)) = (#1::real)";
  18.255  by (induct_tac "n" 1);
  18.256  by (Auto_tac);
  18.257  qed "realpow_minus_one_even";
  18.258  Addsimps [realpow_minus_one_even];
  18.259  
  18.260 -Goal "0r < r & r < 1r --> r ^ Suc n < r ^ n";
  18.261 +Goal "(#0::real) < r & r < (#1::real) --> r ^ Suc n < r ^ n";
  18.262  by (induct_tac "n" 1);
  18.263  by (Auto_tac);
  18.264  qed_spec_mp "realpow_Suc_less";
  18.265  
  18.266 -Goal "0r <= r & r < 1r --> r ^ Suc n <= r ^ n";
  18.267 +Goal "#0 <= r & r < (#1::real) --> r ^ Suc n <= r ^ n";
  18.268  by (induct_tac "n" 1);
  18.269  by (auto_tac (claset() addIs [real_less_imp_le] addSDs
  18.270       [real_le_imp_less_or_eq],simpset()));
  18.271  qed_spec_mp "realpow_Suc_le";
  18.272  
  18.273 -Goal "0r <= 0r ^ n";
  18.274 +Goal "(#0::real) <= #0 ^ n";
  18.275  by (case_tac "n" 1);
  18.276  by (Auto_tac);
  18.277  qed "realpow_zero_le";
  18.278  Addsimps [realpow_zero_le];
  18.279  
  18.280 -Goal "0r < r & r < 1r --> r ^ Suc n <= r ^ n";
  18.281 +Goal "#0 < r & r < (#1::real) --> r ^ Suc n <= r ^ n";
  18.282  by (blast_tac (claset() addSIs [real_less_imp_le,
  18.283      realpow_Suc_less]) 1);
  18.284  qed_spec_mp "realpow_Suc_le2";
  18.285  
  18.286 -Goal "[| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n";
  18.287 +Goal "[| #0 <= r; r < (#1::real) |] ==> r ^ Suc n <= r ^ n";
  18.288  by (etac (real_le_imp_less_or_eq RS disjE) 1);
  18.289  by (rtac realpow_Suc_le2 1);
  18.290  by (Auto_tac);
  18.291  qed "realpow_Suc_le3";
  18.292  
  18.293 -Goal "0r <= r & r < 1r & n < N --> r ^ N <= r ^ n";
  18.294 +Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n";
  18.295  by (induct_tac "N" 1);
  18.296  by (Auto_tac);
  18.297  by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
  18.298 -by (ALLGOALS(dtac real_mult_le_mono3));
  18.299 +by (ALLGOALS(dtac (full_rename_numerals thy real_mult_le_mono3)));
  18.300  by (REPEAT(assume_tac 1));
  18.301  by (REPEAT(assume_tac 3));
  18.302  by (auto_tac (claset(),simpset() addsimps 
  18.303      [less_Suc_eq]));
  18.304  qed_spec_mp "realpow_less_le";
  18.305  
  18.306 -Goal "[| 0r <= r; r < 1r; n <= N |] ==> r ^ N <= r ^ n";
  18.307 +Goal "[| #0 <= r; r < (#1::real); n <= N |] ==> r ^ N <= r ^ n";
  18.308  by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  18.309  by (auto_tac (claset() addIs [realpow_less_le],
  18.310      simpset()));
  18.311  qed "realpow_le_le";
  18.312  
  18.313 -Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n <= r";
  18.314 +Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n <= r";
  18.315  by (dres_inst_tac [("n","1"),("N","Suc n")] 
  18.316      (real_less_imp_le RS realpow_le_le) 1);
  18.317  by (Auto_tac);
  18.318  qed "realpow_Suc_le_self";
  18.319  
  18.320 -Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n < 1r";
  18.321 +Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n < #1";
  18.322  by (blast_tac (claset() addIs [realpow_Suc_le_self,
  18.323                 real_le_less_trans]) 1);
  18.324  qed "realpow_Suc_less_one";
  18.325  
  18.326 -Goal "1r <= r --> r ^ n <= r ^ Suc n";
  18.327 +Goal "(#1::real) <= r --> r ^ n <= r ^ Suc n";
  18.328  by (induct_tac "n" 1);
  18.329 -by (auto_tac (claset() addSIs [real_mult_le_le_mono1],simpset()));
  18.330 -by (rtac ccontr 1 THEN dtac not_real_leE 1);
  18.331 -by (dtac real_le_less_trans 1 THEN assume_tac 1);
  18.332 -by (etac (real_zero_less_one RS real_less_asym) 1);
  18.333 +by Auto_tac;
  18.334  qed_spec_mp "realpow_le_Suc";
  18.335  
  18.336 -Goal "1r < r --> r ^ n < r ^ Suc n";
  18.337 +Goal "(#1::real) < r --> r ^ n < r ^ Suc n";
  18.338  by (induct_tac "n" 1);
  18.339 -by (auto_tac (claset() addSIs [real_mult_less_mono2],simpset()));
  18.340 -by (rtac ccontr 1 THEN dtac real_leI 1);
  18.341 -by (dtac real_less_le_trans 1 THEN assume_tac 1);
  18.342 -by (etac (real_zero_less_one RS real_less_asym) 1);
  18.343 +by Auto_tac;
  18.344  qed_spec_mp "realpow_less_Suc";
  18.345  
  18.346 -Goal "1r < r --> r ^ n <= r ^ Suc n";
  18.347 +Goal "(#1::real) < r --> r ^ n <= r ^ Suc n";
  18.348  by (blast_tac (claset() addSIs [real_less_imp_le,
  18.349      realpow_less_Suc]) 1);
  18.350  qed_spec_mp "realpow_le_Suc2";
  18.351  
  18.352 -Goal "1r < r & n < N --> r ^ n <= r ^ N";
  18.353 +Goal "(#1::real) < r & n < N --> r ^ n <= r ^ N";
  18.354  by (induct_tac "N" 1);
  18.355  by (Auto_tac);
  18.356  by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
  18.357 -by (ALLGOALS(dtac real_mult_self_le));
  18.358 +by (ALLGOALS(dtac (full_rename_numerals thy real_mult_self_le)));
  18.359  by (assume_tac 1);
  18.360  by (assume_tac 2);
  18.361  by (auto_tac (claset() addIs [real_le_trans],
  18.362      simpset() addsimps [less_Suc_eq]));
  18.363  qed_spec_mp "realpow_gt_ge";
  18.364  
  18.365 -Goal "1r <= r & n < N --> r ^ n <= r ^ N";
  18.366 +Goal "(#1::real) <= r & n < N --> r ^ n <= r ^ N";
  18.367  by (induct_tac "N" 1);
  18.368  by (Auto_tac);
  18.369  by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
  18.370 -by (ALLGOALS(dtac real_mult_self_le2));
  18.371 +by (ALLGOALS(dtac (full_rename_numerals thy real_mult_self_le2)));
  18.372  by (assume_tac 1);
  18.373  by (assume_tac 2);
  18.374  by (auto_tac (claset() addIs [real_le_trans],
  18.375      simpset() addsimps [less_Suc_eq]));
  18.376  qed_spec_mp "realpow_gt_ge2";
  18.377  
  18.378 -Goal "[| 1r < r; n <= N |] ==> r ^ n <= r ^ N";
  18.379 +Goal "[| (#1::real) < r; n <= N |] ==> r ^ n <= r ^ N";
  18.380  by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  18.381  by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
  18.382  qed "realpow_ge_ge";
  18.383  
  18.384 -Goal "[| 1r <= r; n <= N |] ==> r ^ n <= r ^ N";
  18.385 +Goal "[| (#1::real) <= r; n <= N |] ==> r ^ n <= r ^ N";
  18.386  by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  18.387  by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
  18.388  qed "realpow_ge_ge2";
  18.389  
  18.390 -Goal "1r < r ==> r <= r ^ Suc n";
  18.391 +Goal "(#1::real) < r ==> r <= r ^ Suc n";
  18.392  by (dres_inst_tac [("n","1"),("N","Suc n")] 
  18.393      realpow_ge_ge 1);
  18.394  by (Auto_tac);
  18.395  qed_spec_mp "realpow_Suc_ge_self";
  18.396  
  18.397 -Goal "1r <= r ==> r <= r ^ Suc n";
  18.398 +Goal "(#1::real) <= r ==> r <= r ^ Suc n";
  18.399  by (dres_inst_tac [("n","1"),("N","Suc n")] 
  18.400      realpow_ge_ge2 1);
  18.401  by (Auto_tac);
  18.402  qed_spec_mp "realpow_Suc_ge_self2";
  18.403  
  18.404 -Goal "[| 1r < r; 0 < n |] ==> r <= r ^ n";
  18.405 +Goal "[| (#1::real) < r; 0 < n |] ==> r <= r ^ n";
  18.406  by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
  18.407  by (auto_tac (claset() addSIs 
  18.408      [realpow_Suc_ge_self],simpset()));
  18.409  qed "realpow_ge_self";
  18.410  
  18.411 -Goal "[| 1r <= r; 0 < n |] ==> r <= r ^ n";
  18.412 +Goal "[| (#1::real) <= r; 0 < n |] ==> r <= r ^ n";
  18.413  by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
  18.414  by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
  18.415  qed "realpow_ge_self2";
  18.416 @@ -361,17 +356,107 @@
  18.417  qed_spec_mp "realpow_minus_mult";
  18.418  Addsimps [realpow_minus_mult];
  18.419  
  18.420 -Goal "r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
  18.421 +Goal "r ~= #0 ==> r * rinv(r) ^ 2 = rinv r";
  18.422  by (asm_simp_tac (simpset() addsimps [realpow_two,
  18.423                    real_mult_assoc RS sym]) 1);
  18.424  qed "realpow_two_mult_rinv";
  18.425  Addsimps [realpow_two_mult_rinv];
  18.426  
  18.427 +(* 05/00 *)
  18.428 +Goal "(-x) ^ 2 = (x::real) ^ 2";
  18.429 +by (Simp_tac 1);
  18.430 +qed "realpow_two_minus";
  18.431 +Addsimps [realpow_two_minus];
  18.432  
  18.433 -(** New versions using #0 and #1 instead of 0r and 1r
  18.434 -    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
  18.435 +Goal "(x::real) ^ 2 + - (y ^ 2) = (x + -y) * (x + y)";
  18.436 +by (simp_tac (simpset() addsimps [real_add_mult_distrib2,
  18.437 +    real_add_mult_distrib, real_minus_mult_eq2 RS sym] 
  18.438 +    @ real_mult_ac) 1);
  18.439 +qed "realpow_two_add_minus";
  18.440 +
  18.441 +goalw RealPow.thy [real_diff_def] 
  18.442 +      "(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
  18.443 +by (simp_tac (simpset() addsimps [realpow_two_add_minus]
  18.444 +               delsimps [realpow_Suc]) 1);
  18.445 +qed "realpow_two_diff";
  18.446 +
  18.447 +goalw RealPow.thy [real_diff_def] 
  18.448 +      "((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
  18.449 +by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
  18.450 +by (dtac (rename_numerals thy ((real_eq_minus_iff RS iffD1) 
  18.451 +    RS sym)) 1);
  18.452 +by (auto_tac (claset() addSDs [full_rename_numerals thy 
  18.453 +    real_mult_zero_disj] addDs [full_rename_numerals thy 
  18.454 +    real_add_minus_eq_minus], simpset() addsimps 
  18.455 +    [realpow_two_add_minus] delsimps [realpow_Suc]));
  18.456 +qed "realpow_two_disj";
  18.457 +
  18.458 +(* used in Transc *)
  18.459 +Goal  "!!x. [|x ~= #0; m <= n |] ==> \
  18.460 +\      x ^ (n - m) = x ^ n * rinv(x ^ m)";
  18.461 +by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
  18.462 +    less_iff_Suc_add,realpow_add,
  18.463 +    realpow_not_zero] @ real_mult_ac));
  18.464 +qed "realpow_diff";
  18.465 +
  18.466 +Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";
  18.467 +by (induct_tac "n" 1);
  18.468 +by (auto_tac (claset(),simpset() addsimps [real_of_nat_one,
  18.469 +    real_of_nat_mult]));
  18.470 +qed "realpow_real_of_nat";
  18.471  
  18.472 -Addsimps (map (rename_numerals thy) 
  18.473 -	  [realpow_two_le, realpow_zero_le,
  18.474 -	   abs_minus_realpow_one, abs_realpow_minus_one,
  18.475 -	   realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);
  18.476 +Goal "#0 < real_of_nat (2 ^ n)";
  18.477 +by (induct_tac "n" 1);
  18.478 +by (auto_tac (claset() addSIs [full_rename_numerals thy real_mult_order],
  18.479 +    simpset() addsimps [real_of_nat_mult RS sym,real_of_nat_one]));
  18.480 +by (simp_tac (simpset() addsimps [rename_numerals thy 
  18.481 +    (real_of_nat_zero RS sym)]) 1);
  18.482 +qed "realpow_real_of_nat_two_pos";
  18.483 +Addsimps [realpow_real_of_nat_two_pos];
  18.484 +
  18.485 +(* FIXME: annoyingly long proof! *)
  18.486 +Goal "(#0::real) <= x & #0 <= y &  x ^ Suc n <= y ^ Suc n --> x <= y";
  18.487 +by (induct_tac "n" 1);
  18.488 +by (Auto_tac);
  18.489 +by (dtac not_real_leE 1);
  18.490 +by (auto_tac (claset() addDs [real_less_asym],
  18.491 +    simpset() addsimps [real_le_less]));
  18.492 +by (forw_inst_tac [("r","y")] 
  18.493 +    (full_rename_numerals thy real_rinv_less_swap) 1);
  18.494 +by (rtac real_linear_less2 2);
  18.495 +by (rtac real_linear_less2 5);
  18.496 +by (dtac (full_rename_numerals thy 
  18.497 +    ((real_not_refl2 RS not_sym) RS real_mult_not_zero)) 9);
  18.498 +by (Auto_tac);
  18.499 +by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 1);
  18.500 +by (forward_tac [full_rename_numerals thy real_rinv_gt_zero] 1);
  18.501 +by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 3);
  18.502 +by (dtac (full_rename_numerals thy real_rinv_gt_zero) 3);
  18.503 +by (dtac (full_rename_numerals thy real_mult_less_zero) 3);
  18.504 +by (forw_inst_tac [("x","(y * y ^ n)"),("r1.0","y")] 
  18.505 +    (full_rename_numerals thy real_mult_less_mono) 2);
  18.506 +by (dres_inst_tac [("x","x * (x * x ^ n)"),("r1.0","rinv x")] 
  18.507 +    (full_rename_numerals thy real_mult_less_mono) 1);
  18.508 +by (Auto_tac);
  18.509 +by (auto_tac (claset() addIs (map (full_rename_numerals thy ) 
  18.510 +    [real_mult_order,realpow_gt_zero]),
  18.511 +    simpset() addsimps [real_mult_assoc 
  18.512 +    RS sym,real_not_refl2 RS not_sym]));
  18.513 +qed_spec_mp "realpow_increasing";
  18.514 +  
  18.515 +Goal "(#0::real) <= x & #0 <= y &  x ^ Suc n = y ^ Suc n --> x = y";
  18.516 +by (induct_tac "n" 1);
  18.517 +by (Auto_tac);
  18.518 +by (res_inst_tac [("R1.0","x"),("R2.0","y")] 
  18.519 +    real_linear_less2 1);
  18.520 +by (auto_tac (claset() addDs [real_less_asym],
  18.521 +    simpset() addsimps [real_le_less]));
  18.522 +by (dres_inst_tac [("n","Suc(Suc n)")]
  18.523 +    (conjI RSN(2,conjI RS realpow_less)) 1);
  18.524 +by (dres_inst_tac [("n","Suc(Suc n)"),("x","y")]
  18.525 +    (conjI RSN(2,conjI RS realpow_less)) 5);
  18.526 +by (EVERY[dtac sym 4, dtac not_sym 4, rtac sym 4]);
  18.527 +by (auto_tac (claset() addDs [real_not_refl2 RS not_sym,
  18.528 +     full_rename_numerals thy real_mult_not_zero] 
  18.529 +     addIs [ccontr],simpset()));
  18.530 +qed_spec_mp "realpow_Suc_cancel_eq";
    19.1 --- a/src/HOL/Real/RealPow.thy	Wed May 31 18:06:02 2000 +0200
    19.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jun 01 11:22:27 2000 +0200
    19.3 @@ -11,7 +11,7 @@
    19.4  instance real :: {power}
    19.5  
    19.6  primrec (realpow)
    19.7 -     realpow_0   "r ^ 0       = 1r"
    19.8 +     realpow_0   "r ^ 0       = #1"
    19.9       realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
   19.10  
   19.11  end