real literals using binary arithmetic
authorpaulson
Thu Aug 19 18:36:41 1999 +0200 (1999-08-19)
changeset 7292dff3470c5c62
parent 7291 8aa66ddc0bea
child 7293 959e060f4a2f
real literals using binary arithmetic
src/HOL/Real/Hyperreal/HyperDef.thy
src/HOL/Real/PNat.ML
src/HOL/Real/RComplete.thy
src/HOL/Real/ROOT.ML
src/HOL/Real/Real.ML
src/HOL/Real/RealBin.ML
src/HOL/Real/RealBin.thy
src/HOL/Real/RealDef.ML
src/HOL/Real/RealInt.ML
src/HOL/Real/RealInt.thy
src/HOL/Real/RealPow.ML
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.thy	Thu Aug 19 17:06:05 1999 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.thy	Thu Aug 19 18:36:41 1999 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4      Description : Construction of hyperreals using ultrafilters
     1.5  *) 
     1.6  
     1.7 -HyperDef = Filter + Real +
     1.8 +HyperDef = Filter + RealBin +
     1.9  
    1.10  consts 
    1.11   
     2.1 --- a/src/HOL/Real/PNat.ML	Thu Aug 19 17:06:05 1999 +0200
     2.2 +++ b/src/HOL/Real/PNat.ML	Thu Aug 19 18:36:41 1999 +0200
     2.3 @@ -708,3 +708,9 @@
     2.4  qed "pnat_of_nat_less_iff";
     2.5  Addsimps [pnat_of_nat_less_iff RS sym];
     2.6  
     2.7 +goalw PNat.thy [pnat_mult_def,pnat_of_nat_def] 
     2.8 +      "pnat_of_nat n1 * pnat_of_nat n2 = \
     2.9 +\      pnat_of_nat (n1 * n2 + n1 + n2)";
    2.10 +by (auto_tac (claset(),simpset() addsimps [mult_Rep_pnat_mult,
    2.11 +    pnat_add_def,Abs_pnat_inverse,gt_0_mem_pnat]));
    2.12 +qed "pnat_of_nat_mult";
     3.1 --- a/src/HOL/Real/RComplete.thy	Thu Aug 19 17:06:05 1999 +0200
     3.2 +++ b/src/HOL/Real/RComplete.thy	Thu Aug 19 18:36:41 1999 +0200
     3.3 @@ -6,5 +6,5 @@
     3.4                    reals and reals 
     3.5  *) 
     3.6  
     3.7 -RComplete = Lubs + Real
     3.8 +RComplete = Lubs + RealBin
     3.9  
     4.1 --- a/src/HOL/Real/ROOT.ML	Thu Aug 19 17:06:05 1999 +0200
     4.2 +++ b/src/HOL/Real/ROOT.ML	Thu Aug 19 18:36:41 1999 +0200
     4.3 @@ -11,7 +11,6 @@
     4.4  set proof_timing;
     4.5  time_use_thy "RealDef";
     4.6  use          "simproc.ML";
     4.7 -time_use_thy "RealAbs";
     4.8  time_use_thy "RComplete";
     4.9  time_use_thy "Hyperreal/Filter";
    4.10  time_use_thy "Hyperreal/HyperDef";
     5.1 --- a/src/HOL/Real/Real.ML	Thu Aug 19 17:06:05 1999 +0200
     5.2 +++ b/src/HOL/Real/Real.ML	Thu Aug 19 18:36:41 1999 +0200
     5.3 @@ -280,7 +280,7 @@
     5.4  qed "real_of_posnat_two";
     5.5  
     5.6  Goalw [real_of_posnat_def]
     5.7 -          "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
     5.8 +    "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
     5.9  by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym,
    5.10      real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym,
    5.11      prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
    5.12 @@ -292,13 +292,9 @@
    5.13  by (full_simp_tac (simpset() addsimps [real_of_posnat_two,real_add_assoc]) 1);
    5.14  qed "real_of_posnat_add_one";
    5.15  
    5.16 -Goal "Suc n = n + 1";
    5.17 -by Auto_tac;
    5.18 -qed "lemmaS";
    5.19 -
    5.20  Goal "real_of_posnat (Suc n) = real_of_posnat n + 1r";
    5.21 -by (stac lemmaS 1);
    5.22 -by (rtac real_of_posnat_add_one 1);
    5.23 +by (stac (real_of_posnat_add_one RS sym) 1);
    5.24 +by (Simp_tac 1);
    5.25  qed "real_of_posnat_Suc";
    5.26  
    5.27  Goal "inj(real_of_posnat)";
    5.28 @@ -369,7 +365,7 @@
    5.29  qed "real_of_posnat_rinv_gt_zero";
    5.30  Addsimps [real_of_posnat_rinv_gt_zero];
    5.31  
    5.32 -Goal "x+x=x*(1r+1r)";
    5.33 +Goal "x+x = x*(1r+1r)";
    5.34  by (simp_tac (simpset() addsimps 
    5.35                [real_add_mult_distrib2]) 1);
    5.36  qed "real_add_self";
    5.37 @@ -452,8 +448,7 @@
    5.38  by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
    5.39  qed "real_mult_le_le_mono1";
    5.40  
    5.41 -Goal "[| 0r < r1; r1 <r2; 0r < x; x < y|] \
    5.42 -\                  ==> r1 * x < r2 * y";
    5.43 +Goal "[| 0r < r1; r1 <r2; 0r < x; x < y|] ==> r1 * x < r2 * y";
    5.44  by (dres_inst_tac [("x","x")] real_mult_less_mono2 1);
    5.45  by (dres_inst_tac [("R1.0","0r")] real_less_trans 2);
    5.46  by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
    5.47 @@ -461,22 +456,19 @@
    5.48  by (blast_tac (claset() addIs [real_less_trans]) 1);
    5.49  qed "real_mult_less_mono";
    5.50  
    5.51 -Goal "[| 0r < r1; r1 <r2; 0r < y|] \
    5.52 -\                           ==> 0r < r2 * y";
    5.53 +Goal "[| 0r < r1; r1 <r2; 0r < y|] ==> 0r < r2 * y";
    5.54  by (dres_inst_tac [("R1.0","0r")] real_less_trans 1);
    5.55  by (assume_tac 1);
    5.56  by (blast_tac (claset() addIs [real_mult_order]) 1);
    5.57  qed "real_mult_order_trans";
    5.58  
    5.59 -Goal "[| 0r < r1; r1 <r2; 0r <= x; x < y|] \
    5.60 -\                  ==> r1 * x < r2 * y";
    5.61 +Goal "[| 0r < r1; r1 <r2; 0r <= x; x < y|] ==> r1 * x < r2 * y";
    5.62  by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
    5.63  	               addIs [real_mult_less_mono,real_mult_order_trans],
    5.64                simpset()));
    5.65  qed "real_mult_less_mono3";
    5.66  
    5.67 -Goal "[| 0r <= r1; r1 <r2; 0r <= x; x < y|] \
    5.68 -\                  ==> r1 * x < r2 * y";
    5.69 +Goal "[| 0r <= r1; r1 <r2; 0r <= x; x < y|] ==> r1 * x < r2 * y";
    5.70  by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
    5.71  	               addIs [real_mult_less_mono,real_mult_order_trans,
    5.72  			      real_mult_order],
    5.73 @@ -486,8 +478,7 @@
    5.74  by (blast_tac (claset() addIs [real_mult_order]) 1);
    5.75  qed "real_mult_less_mono4";
    5.76  
    5.77 -Goal "[| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \
    5.78 -\                  ==> r1 * x <= r2 * y";
    5.79 +Goal "[| 0r < r1; r1 <= r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
    5.80  by (rtac real_less_or_eq_imp_le 1);
    5.81  by (REPEAT(dtac real_le_imp_less_or_eq 1));
    5.82  by (auto_tac (claset() addIs [real_mult_less_mono,
    5.83 @@ -495,8 +486,7 @@
    5.84  	      simpset()));
    5.85  qed "real_mult_le_mono";
    5.86  
    5.87 -Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] \
    5.88 -\                  ==> r1 * x <= r2 * y";
    5.89 +Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
    5.90  by (rtac real_less_or_eq_imp_le 1);
    5.91  by (REPEAT(dtac real_le_imp_less_or_eq 1));
    5.92  by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order_trans,
    5.93 @@ -504,16 +494,14 @@
    5.94  	      simpset()));
    5.95  qed "real_mult_le_mono2";
    5.96  
    5.97 -Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \
    5.98 -\                  ==> r1 * x <= r2 * y";
    5.99 +Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
   5.100  by (dtac real_le_imp_less_or_eq 1);
   5.101  by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
   5.102  by (dtac real_le_trans 1 THEN assume_tac 1);
   5.103  by (auto_tac (claset() addIs [real_less_le_mult_order], simpset()));
   5.104  qed "real_mult_le_mono3";
   5.105  
   5.106 -Goal "[| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \
   5.107 -\                  ==> r1 * x <= r2 * y";
   5.108 +Goal "[| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
   5.109  by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1);
   5.110  by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1],
   5.111  	      simpset()));
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Real/RealBin.ML	Thu Aug 19 18:36:41 1999 +0200
     6.3 @@ -0,0 +1,153 @@
     6.4 +(*  Title:      HOL/RealBin.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1999  University of Cambridge
     6.8 +
     6.9 +Binary arithmetic for the reals (integer literals only)
    6.10 +*)
    6.11 +
    6.12 +(** real_of_int (coercion from int to real) **)
    6.13 +
    6.14 +Goal "real_of_int (number_of w) = number_of w";
    6.15 +by (simp_tac (simpset() addsimps [real_number_of_def]) 1);
    6.16 +qed "real_number_of";
    6.17 +Addsimps [real_number_of];
    6.18 +
    6.19 +Goalw [real_number_of_def] "0r = #0";
    6.20 +by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1);
    6.21 +qed "zero_eq_numeral_0";
    6.22 +
    6.23 +Goalw [real_number_of_def] "1r = #1";
    6.24 +by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1);
    6.25 +qed "one_eq_numeral_1";
    6.26 +
    6.27 +(** Addition **)
    6.28 +
    6.29 +Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')";
    6.30 +by (simp_tac
    6.31 +    (simpset_of Int.thy addsimps [real_number_of_def, 
    6.32 +				  real_of_int_add, number_of_add]) 1);
    6.33 +qed "add_real_number_of";
    6.34 +
    6.35 +Addsimps [add_real_number_of];
    6.36 +
    6.37 +
    6.38 +(** Subtraction **)
    6.39 +
    6.40 +Goalw [real_number_of_def] "- (number_of w :: real) = number_of (bin_minus w)";
    6.41 +by (simp_tac
    6.42 +    (simpset_of Int.thy addsimps [number_of_minus, real_of_int_minus]) 1);
    6.43 +qed "minus_real_number_of";
    6.44 +
    6.45 +Goalw [real_number_of_def]
    6.46 +   "(number_of v :: real) - number_of w = number_of (bin_add v (bin_minus w))";
    6.47 +by (simp_tac
    6.48 +    (simpset_of Int.thy addsimps [diff_number_of_eq, real_of_int_diff]) 1);
    6.49 +qed "diff_real_number_of";
    6.50 +
    6.51 +Addsimps [minus_real_number_of, diff_real_number_of];
    6.52 +
    6.53 +
    6.54 +(** Multiplication **)
    6.55 +
    6.56 +Goal "(number_of v :: real) * number_of v' = number_of (bin_mult v v')";
    6.57 +by (simp_tac
    6.58 +    (simpset_of Int.thy addsimps [real_number_of_def, 
    6.59 +				  real_of_int_mult, number_of_mult]) 1);
    6.60 +qed "mult_real_number_of";
    6.61 +
    6.62 +Addsimps [mult_real_number_of];
    6.63 +
    6.64 +
    6.65 +(*** Comparisons ***)
    6.66 +
    6.67 +(** Equals (=) **)
    6.68 +
    6.69 +Goal "((number_of v :: real) = number_of v') = \
    6.70 +\     iszero (number_of (bin_add v (bin_minus v')))";
    6.71 +by (simp_tac
    6.72 +    (simpset_of Int.thy addsimps [real_number_of_def, 
    6.73 +				  real_of_int_eq_iff, eq_number_of_eq]) 1);
    6.74 +qed "eq_real_number_of";
    6.75 +
    6.76 +Addsimps [eq_real_number_of];
    6.77 +
    6.78 +(** Less-than (<) **)
    6.79 +
    6.80 +(*"neg" is used in rewrite rules for binary comparisons*)
    6.81 +Goal "((number_of v :: real) < number_of v') = \
    6.82 +\     neg (number_of (bin_add v (bin_minus v')))";
    6.83 +by (simp_tac
    6.84 +    (simpset_of Int.thy addsimps [real_number_of_def, real_of_int_less_iff, 
    6.85 +				  less_number_of_eq_neg]) 1);
    6.86 +qed "less_real_number_of";
    6.87 +
    6.88 +Addsimps [less_real_number_of];
    6.89 +
    6.90 +
    6.91 +(** Less-than-or-equals (<=) **)
    6.92 +
    6.93 +Goal "(number_of x <= (number_of y::real)) = \
    6.94 +\     (~ number_of y < (number_of x::real))";
    6.95 +by (rtac (linorder_not_less RS sym) 1);
    6.96 +qed "le_real_number_of_eq_not_less"; 
    6.97 +
    6.98 +Addsimps [le_real_number_of_eq_not_less];
    6.99 +
   6.100 +
   6.101 +(** rabs (absolute value) **)
   6.102 +
   6.103 +Goalw [rabs_def]
   6.104 +     "rabs (number_of v :: real) = \
   6.105 +\       (if neg (number_of v) then number_of (bin_minus v) \
   6.106 +\        else number_of v)";
   6.107 +by (simp_tac
   6.108 +    (simpset_of Int.thy addsimps
   6.109 +      bin_arith_simps@
   6.110 +      [minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less,
   6.111 +       less_real_number_of, real_of_int_le_iff]) 1);
   6.112 +qed "rabs_nat_number_of";
   6.113 +
   6.114 +Addsimps [rabs_nat_number_of];
   6.115 +
   6.116 +
   6.117 +(*** New versions of existing theorems involving 0r, 1r ***)
   6.118 +
   6.119 +Goal "- #1 = (#-1::real)";
   6.120 +by (Simp_tac 1);
   6.121 +qed "minus_numeral_one";
   6.122 +
   6.123 +
   6.124 +(*Maps 0r to #0 and 1r to #1 and -1r to #-1*)
   6.125 +val real_numeral_ss = 
   6.126 +    HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
   6.127 +		     minus_numeral_one];
   6.128 +
   6.129 +fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
   6.130 +
   6.131 +
   6.132 +fun inst x t = read_instantiate_sg (sign_of RealBin.thy) [(x,t)];
   6.133 +
   6.134 +
   6.135 +(*Now insert some identities previously stated for 0r and 1r*)
   6.136 +
   6.137 +(** RealDef & Real **)
   6.138 +
   6.139 +Addsimps (map (rename_numerals thy) 
   6.140 +	  [real_minus_zero, real_minus_zero_iff,
   6.141 +	   real_add_zero_left, real_add_zero_right, 
   6.142 +	   real_diff_0, real_diff_0_right,
   6.143 +	   real_mult_0_right, real_mult_0, real_mult_1_right, real_mult_1,
   6.144 +	   real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
   6.145 +	   real_minus_zero_less_iff]);
   6.146 +
   6.147 +(** RealPow **)
   6.148 +
   6.149 +Addsimps (map (rename_numerals thy) 
   6.150 +	  [realpow_zero, realpow_two_le, realpow_zero_le,
   6.151 +	   realpow_eq_one, rabs_minus_realpow_one, rabs_realpow_minus_one,
   6.152 +	   realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);
   6.153 +
   6.154 +(*Perhaps add some theorems that aren't in the default simpset, as
   6.155 +  done in Integ/NatBin.ML*)
   6.156 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Real/RealBin.thy	Thu Aug 19 18:36:41 1999 +0200
     7.3 @@ -0,0 +1,21 @@
     7.4 +(*  Title:      HOL/RealBin.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   1999  University of Cambridge
     7.8 +
     7.9 +Binary arithmetic for the reals
    7.10 +
    7.11 +This case is reduced to that for the integers
    7.12 +*)
    7.13 +
    7.14 +RealBin = RealInt + Bin + RealPow +
    7.15 +
    7.16 +instance
    7.17 +  real :: number 
    7.18 +
    7.19 +defs
    7.20 +  real_number_of_def
    7.21 +    "number_of v == real_of_int (number_of v)"
    7.22 +     (*::bin=>real               ::bin=>int*)
    7.23 +
    7.24 +end
     8.1 --- a/src/HOL/Real/RealDef.ML	Thu Aug 19 17:06:05 1999 +0200
     8.2 +++ b/src/HOL/Real/RealDef.ML	Thu Aug 19 18:36:41 1999 +0200
     8.3 @@ -748,8 +748,8 @@
     8.4  
     8.5  Goalw [real_zero_def] "- real_of_preal m < 0r";
     8.6  by (auto_tac (claset(),
     8.7 -    simpset() addsimps [real_of_preal_def,
     8.8 -    real_less_def,real_minus]));
     8.9 +	      simpset() addsimps [real_of_preal_def,
    8.10 +				  real_less_def,real_minus]));
    8.11  by (REPEAT(rtac exI 1));
    8.12  by (EVERY[rtac conjI 1, rtac conjI 2]);
    8.13  by (REPEAT(Blast_tac 2));
    8.14 @@ -776,7 +776,7 @@
    8.15  Goal "~ real_of_preal m < 0r";
    8.16  by (cut_facts_tac [real_of_preal_zero_less] 1);
    8.17  by (blast_tac (claset() addDs [real_less_trans] 
    8.18 -               addEs [real_less_irrefl]) 1);
    8.19 +                        addEs [real_less_irrefl]) 1);
    8.20  qed "real_of_preal_not_less_zero";
    8.21  
    8.22  Goal "0r < - (- real_of_preal m)";
    8.23 @@ -789,7 +789,7 @@
    8.24        "0r < real_of_preal m + real_of_preal m1";
    8.25  by (auto_tac (claset(),
    8.26  	      simpset() addsimps [real_of_preal_def,
    8.27 -              real_less_def,real_add]));
    8.28 +				  real_less_def,real_add]));
    8.29  by (REPEAT(rtac exI 1));
    8.30  by (EVERY[rtac conjI 1, rtac conjI 2]);
    8.31  by (REPEAT(Blast_tac 2));
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Real/RealInt.ML	Thu Aug 19 18:36:41 1999 +0200
     9.3 @@ -0,0 +1,145 @@
     9.4 +(*  Title:       RealInt.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:      Jacques D. Fleuriot
     9.7 +    Copyright:   1999 University of Edinburgh
     9.8 +    Description: Embedding the integers in the reals
     9.9 +*)
    9.10 +
    9.11 +
    9.12 +Goalw [congruent_def]
    9.13 +  "congruent intrel (%p. split (%i j. realrel ^^ \
    9.14 +\  {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
    9.15 +\    preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)";
    9.16 +by (auto_tac (claset(),simpset() addsimps [pnat_of_nat_add,
    9.17 +    prat_of_pnat_add RS sym,preal_of_prat_add RS sym]));
    9.18 +qed "real_of_int_congruent";
    9.19 +
    9.20 +val real_of_int_ize = RSLIST [equiv_intrel, real_of_int_congruent];
    9.21 +
    9.22 +Goalw [real_of_int_def]
    9.23 +   "real_of_int (Abs_Integ (intrel ^^ {(i, j)})) = \
    9.24 +\     Abs_real(realrel ^^ \
    9.25 +\       {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
    9.26 +\         preal_of_prat (prat_of_pnat (pnat_of_nat j)))})";
    9.27 +by (res_inst_tac [("f","Abs_real")] arg_cong 1);
    9.28 +by (simp_tac (simpset() addsimps 
    9.29 +   [realrel_in_real RS Abs_real_inverse,
    9.30 +    real_of_int_ize UN_equiv_class]) 1);
    9.31 +qed "real_of_int";
    9.32 +
    9.33 +Goal "inj(real_of_int)";
    9.34 +by (rtac injI 1);
    9.35 +by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
    9.36 +by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
    9.37 +by (auto_tac (claset() addSDs [inj_preal_of_prat RS injD,
    9.38 +    inj_prat_of_pnat RS injD,inj_pnat_of_nat RS injD],
    9.39 +    simpset() addsimps [real_of_int,preal_of_prat_add RS sym,
    9.40 +     prat_of_pnat_add RS sym,pnat_of_nat_add]));
    9.41 +qed "inj_real_of_int";
    9.42 +
    9.43 +Goalw [int_def,real_zero_def] "real_of_int (int 0) = 0r";
    9.44 +by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
    9.45 +qed "real_of_int_zero";
    9.46 +
    9.47 +Goalw [int_def,real_one_def] "real_of_int (int 1) = 1r";
    9.48 +by (auto_tac (claset(),
    9.49 +	      simpset() addsimps [real_of_int,
    9.50 +				  preal_of_prat_add RS sym,pnat_two_eq,
    9.51 +			       prat_of_pnat_add RS sym,pnat_one_iff RS sym]));
    9.52 +qed "real_of_int_one";
    9.53 +
    9.54 +Goal "real_of_int x + real_of_int y = real_of_int (x + y)";
    9.55 +by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
    9.56 +by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
    9.57 +by (auto_tac (claset(),simpset() addsimps [real_of_int,
    9.58 +    preal_of_prat_add RS sym,prat_of_pnat_add RS sym,
    9.59 +    zadd,real_add,pnat_of_nat_add] @ pnat_add_ac));
    9.60 +qed "real_of_int_add";
    9.61 +
    9.62 +Goal "-real_of_int x = real_of_int (-x)";
    9.63 +by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
    9.64 +by (auto_tac (claset(),simpset() addsimps [real_of_int,
    9.65 +    real_minus,zminus]));
    9.66 +qed "real_of_int_minus";
    9.67 +
    9.68 +Goalw [zdiff_def,real_diff_def]
    9.69 +  "real_of_int x - real_of_int y = real_of_int (x - y)";
    9.70 +by (simp_tac (simpset() addsimps [real_of_int_add,
    9.71 +    real_of_int_minus]) 1);
    9.72 +qed "real_of_int_diff";
    9.73 +
    9.74 +Goal "real_of_int x * real_of_int y = real_of_int (x * y)";
    9.75 +by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
    9.76 +by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
    9.77 +by (auto_tac (claset(),simpset() addsimps [real_of_int,
    9.78 +    real_mult,zmult,preal_of_prat_mult RS sym,pnat_of_nat_mult,
    9.79 +    prat_of_pnat_mult RS sym,preal_of_prat_add RS sym,
    9.80 +    prat_of_pnat_add RS sym,pnat_of_nat_add] @ mult_ac @add_ac 
    9.81 +    @ pnat_add_ac));
    9.82 +qed "real_of_int_mult";
    9.83 +
    9.84 +Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r";
    9.85 +by (simp_tac (simpset() addsimps [real_of_int_one RS sym,
    9.86 +				  real_of_int_add,zadd_int]) 1);
    9.87 +qed "real_of_int_Suc";
    9.88 +
    9.89 +(* relating two of the embeddings *)
    9.90 +Goal "real_of_int (int n) = real_of_nat n";
    9.91 +by (induct_tac "n" 1);
    9.92 +by (auto_tac (claset(),simpset() addsimps [real_of_int_zero,
    9.93 +    real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc]));
    9.94 +qed "real_of_int_real_of_nat";
    9.95 +
    9.96 +Goal "~neg z ==> real_of_nat (nat z) = real_of_int z";
    9.97 +by (asm_simp_tac (simpset() addsimps [not_neg_nat,
    9.98 +    real_of_int_real_of_nat RS sym]) 1);
    9.99 +qed "real_of_nat_real_of_int";
   9.100 +
   9.101 +(* put with other properties of real_of_nat? *)
   9.102 +Goal "neg z ==> real_of_nat (nat z) = 0r";
   9.103 +by (asm_simp_tac (simpset() addsimps [neg_nat,
   9.104 +    real_of_nat_zero]) 1);
   9.105 +qed "real_of_nat_neg_int";
   9.106 +Addsimps [real_of_nat_neg_int];
   9.107 +
   9.108 +Goal "(real_of_int x = 0r) = (x = int 0)";
   9.109 +by (auto_tac (claset() addIs [inj_real_of_int RS injD],
   9.110 +    simpset() addsimps [real_of_int_zero]));
   9.111 +qed "real_of_int_zero_cancel";
   9.112 +Addsimps [real_of_int_zero_cancel];
   9.113 +
   9.114 +Goal "real_of_int x < real_of_int y ==> x < y";
   9.115 +by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
   9.116 +by (auto_tac (claset(),
   9.117 +	      simpset() addsimps [zle_iff_zadd, real_of_int_add RS sym,
   9.118 +				  real_of_int_real_of_nat,
   9.119 +				  real_of_nat_zero RS sym]));
   9.120 +qed "real_of_int_less_cancel";
   9.121 +
   9.122 +Goal "x < y ==> (real_of_int x < real_of_int y)";
   9.123 +by (auto_tac (claset(),
   9.124 +	      simpset() addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym,
   9.125 +				  real_of_int_real_of_nat,
   9.126 +				  real_of_nat_Suc]));
   9.127 +by (simp_tac (simpset() addsimps [real_of_nat_one RS
   9.128 +    sym,real_of_nat_zero RS sym,real_of_nat_add]) 1); 
   9.129 +qed "real_of_int_less_mono";
   9.130 +
   9.131 +Goal "(real_of_int x < real_of_int y) = (x < y)";
   9.132 +by (auto_tac (claset() addIs [real_of_int_less_cancel,
   9.133 +			      real_of_int_less_mono],
   9.134 +	      simpset()));
   9.135 +qed "real_of_int_less_iff";
   9.136 +Addsimps [real_of_int_less_iff];
   9.137 +
   9.138 +Goal "(real_of_int x <= real_of_int y) = (x <= y)";
   9.139 +by (auto_tac (claset(),
   9.140 +	      simpset() addsimps [real_le_def, zle_def]));
   9.141 +qed "real_of_int_le_iff";
   9.142 +Addsimps [real_of_int_le_iff];
   9.143 +
   9.144 +Goal "(real_of_int x = real_of_int y) = (x = y)";
   9.145 +by (auto_tac (claset() addSIs [order_antisym],
   9.146 +	      simpset() addsimps [real_of_int_le_iff RS iffD1]));
   9.147 +qed "real_of_int_eq_iff";
   9.148 +Addsimps [real_of_int_eq_iff];
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Real/RealInt.thy	Thu Aug 19 18:36:41 1999 +0200
    10.3 @@ -0,0 +1,17 @@
    10.4 +(*  Title:       RealInt.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:      Jacques D. Fleuriot
    10.7 +    Copyright:   1999 University of Edinburgh
    10.8 +    Description: Embedding the integers in the reals
    10.9 +*)
   10.10 +
   10.11 +RealInt = Real + Int + 
   10.12 +
   10.13 +constdefs 
   10.14 +   real_of_int :: int => real
   10.15 +   "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ^^ 
   10.16 +                     {(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
   10.17 +                       preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
   10.18 +
   10.19 +
   10.20 +end
    11.1 --- a/src/HOL/Real/RealPow.ML	Thu Aug 19 17:06:05 1999 +0200
    11.2 +++ b/src/HOL/Real/RealPow.ML	Thu Aug 19 18:36:41 1999 +0200
    11.3 @@ -17,7 +17,7 @@
    11.4      simpset() addsimps [real_zero_not_eq_one RS not_sym]));
    11.5  qed_spec_mp "realpow_not_zero";
    11.6  
    11.7 -Goal "!!r. r ^ n = 0r ==> r = 0r";
    11.8 +Goal "r ^ n = 0r ==> r = 0r";
    11.9  by (blast_tac (claset() addIs [ccontr] 
   11.10      addDs [realpow_not_zero]) 1);
   11.11  qed "realpow_zero_zero";
   11.12 @@ -128,7 +128,7 @@
   11.13  qed "realpow_two_rabs";
   11.14  Addsimps [realpow_two_rabs];
   11.15  
   11.16 -Goal "!!r. 1r < r ==> 1r < r ^ 2";
   11.17 +Goal "1r < r ==> 1r < r ^ 2";
   11.18  by (auto_tac (claset(),simpset() addsimps [realpow_two]));
   11.19  by (cut_facts_tac [real_zero_less_one] 1);
   11.20  by (forw_inst_tac [("R1.0","0r")] real_less_trans 1);
   11.21 @@ -137,7 +137,7 @@
   11.22  by (auto_tac (claset() addIs [real_less_trans],simpset()));
   11.23  qed "realpow_two_gt_one";
   11.24  
   11.25 -Goal "!!r. 1r <= r ==> 1r <= r ^ 2";
   11.26 +Goal "1r <= r ==> 1r <= r ^ 2";
   11.27  by (etac (real_le_imp_less_or_eq RS disjE) 1);
   11.28  by (etac (realpow_two_gt_one RS real_less_imp_le) 1);
   11.29  by (asm_simp_tac (simpset()) 1);
   11.30 @@ -154,7 +154,7 @@
   11.31      simpset() addsimps [real_zero_less_one]));
   11.32  qed_spec_mp "realpow_ge_one";
   11.33  
   11.34 -Goal "!!r. 1r < r ==> 1r < r ^ (Suc n)";
   11.35 +Goal "1r < r ==> 1r < r ^ (Suc n)";
   11.36  by (forw_inst_tac [("n","n")] realpow_ge_one 1);
   11.37  by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
   11.38  by (dtac sym 2);
   11.39 @@ -164,13 +164,13 @@
   11.40       simpset()));
   11.41  qed "realpow_Suc_gt_one";
   11.42  
   11.43 -Goal "!!r. 1r <= r ==> 1r <= r ^ n";
   11.44 +Goal "1r <= r ==> 1r <= r ^ n";
   11.45  by (dtac real_le_imp_less_or_eq 1); 
   11.46  by (auto_tac (claset() addDs [realpow_ge_one],
   11.47      simpset()));
   11.48  qed "realpow_ge_one2";
   11.49  
   11.50 -Goal "!!r. 0r < r ==> 0r < r ^ Suc n";
   11.51 +Goal "0r < r ==> 0r < r ^ Suc n";
   11.52  by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
   11.53  by (forw_inst_tac [("n1","n")]
   11.54      ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
   11.55 @@ -178,7 +178,7 @@
   11.56       addIs [real_mult_order],simpset()));
   11.57  qed "realpow_Suc_gt_zero";
   11.58  
   11.59 -Goal "!!r. 0r <= r ==> 0r <= r ^ Suc n";
   11.60 +Goal "0r <= r ==> 0r <= r ^ Suc n";
   11.61  by (etac (real_le_imp_less_or_eq RS disjE) 1);
   11.62  by (etac (realpow_ge_zero) 1);
   11.63  by (asm_simp_tac (simpset()) 1);
   11.64 @@ -194,12 +194,11 @@
   11.65  
   11.66  Goal "real_of_nat n < (1r + 1r) ^ n";
   11.67  by (induct_tac "n" 1);
   11.68 -by (rtac (lemmaS RS ssubst) 2);
   11.69 -by (rtac (real_of_nat_add RS subst) 2);
   11.70 -by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero,
   11.71 -    real_zero_less_one,real_add_mult_distrib,real_of_nat_one]));
   11.72 -by (blast_tac (claset() addSIs [real_add_less_le_mono,
   11.73 -    two_realpow_ge_one]) 1);
   11.74 +by (auto_tac (claset(),
   11.75 +	      simpset() addsimps [real_of_nat_Suc, real_of_nat_zero,
   11.76 +				  real_zero_less_one,real_add_mult_distrib,
   11.77 +				  real_of_nat_one]));
   11.78 +by (blast_tac (claset() addSIs [real_add_less_le_mono, two_realpow_ge_one]) 1);
   11.79  qed "two_realpow_gt";
   11.80  Addsimps [two_realpow_gt,two_realpow_ge_one];
   11.81  
   11.82 @@ -249,7 +248,7 @@
   11.83      realpow_Suc_less]) 1);
   11.84  qed_spec_mp "realpow_Suc_le2";
   11.85  
   11.86 -Goal "!!r. [| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n";
   11.87 +Goal "[| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n";
   11.88  by (etac (real_le_imp_less_or_eq RS disjE) 1);
   11.89  by (rtac realpow_Suc_le2 1);
   11.90  by (Auto_tac);
   11.91 @@ -266,20 +265,19 @@
   11.92      [less_Suc_eq]));
   11.93  qed_spec_mp "realpow_less_le";
   11.94  
   11.95 -Goal "!!r. [| 0r <= r; r < 1r; n <= N |] \
   11.96 -\          ==> r ^ N <= r ^ n";
   11.97 +Goal "[| 0r <= r; r < 1r; n <= N |] ==> r ^ N <= r ^ n";
   11.98  by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
   11.99  by (auto_tac (claset() addIs [realpow_less_le],
  11.100      simpset()));
  11.101  qed "realpow_le_le";
  11.102  
  11.103 -Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n <= r";
  11.104 +Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n <= r";
  11.105  by (dres_inst_tac [("n","1"),("N","Suc n")] 
  11.106      (real_less_imp_le RS realpow_le_le) 1);
  11.107  by (Auto_tac);
  11.108  qed "realpow_Suc_le_self";
  11.109  
  11.110 -Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n < 1r";
  11.111 +Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n < 1r";
  11.112  by (blast_tac (claset() addIs [realpow_Suc_le_self,
  11.113                 real_le_less_trans]) 1);
  11.114  qed "realpow_Suc_less_one";
  11.115 @@ -327,35 +325,35 @@
  11.116      simpset() addsimps [less_Suc_eq]));
  11.117  qed_spec_mp "realpow_gt_ge2";
  11.118  
  11.119 -Goal "!!r. [| 1r < r; n <= N |] ==> r ^ n <= r ^ N";
  11.120 +Goal "[| 1r < r; n <= N |] ==> r ^ n <= r ^ N";
  11.121  by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  11.122  by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
  11.123  qed "realpow_ge_ge";
  11.124  
  11.125 -Goal "!!r. [| 1r <= r; n <= N |] ==> r ^ n <= r ^ N";
  11.126 +Goal "[| 1r <= r; n <= N |] ==> r ^ n <= r ^ N";
  11.127  by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  11.128  by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
  11.129  qed "realpow_ge_ge2";
  11.130  
  11.131 -Goal "!!r. 1r < r ==> r <= r ^ Suc n";
  11.132 +Goal "1r < r ==> r <= r ^ Suc n";
  11.133  by (dres_inst_tac [("n","1"),("N","Suc n")] 
  11.134      realpow_ge_ge 1);
  11.135  by (Auto_tac);
  11.136  qed_spec_mp "realpow_Suc_ge_self";
  11.137  
  11.138 -Goal "!!r. 1r <= r ==> r <= r ^ Suc n";
  11.139 +Goal "1r <= r ==> r <= r ^ Suc n";
  11.140  by (dres_inst_tac [("n","1"),("N","Suc n")] 
  11.141      realpow_ge_ge2 1);
  11.142  by (Auto_tac);
  11.143  qed_spec_mp "realpow_Suc_ge_self2";
  11.144  
  11.145 -Goal "!!r. [| 1r < r; 0 < n |] ==> r <= r ^ n";
  11.146 +Goal "[| 1r < r; 0 < n |] ==> r <= r ^ n";
  11.147  by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
  11.148  by (auto_tac (claset() addSIs 
  11.149      [realpow_Suc_ge_self],simpset()));
  11.150  qed "realpow_ge_self";
  11.151  
  11.152 -Goal "!!r. [| 1r <= r; 0 < n |] ==> r <= r ^ n";
  11.153 +Goal "[| 1r <= r; 0 < n |] ==> r <= r ^ n";
  11.154  by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
  11.155  by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
  11.156  qed "realpow_ge_self2";
  11.157 @@ -367,7 +365,7 @@
  11.158  qed_spec_mp "realpow_minus_mult";
  11.159  Addsimps [realpow_minus_mult];
  11.160  
  11.161 -Goal "!!r. r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
  11.162 +Goal "r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
  11.163  by (asm_simp_tac (simpset() addsimps [realpow_two,
  11.164                    real_mult_assoc RS sym]) 1);
  11.165  qed "realpow_two_mult_rinv";