heavily revised by Jacques: coercions have alphabetic names;
authorpaulson
Fri Jul 23 17:29:12 1999 +0200 (1999-07-23)
changeset 707760b098bb8b8a
parent 7076 a30e024791c6
child 7078 4e64b2bd10ce
heavily revised by Jacques: coercions have alphabetic names;
exponentiation is available, etc.
src/HOL/Real/PNat.ML
src/HOL/Real/PNat.thy
src/HOL/Real/PRat.ML
src/HOL/Real/PRat.thy
src/HOL/Real/PReal.ML
src/HOL/Real/PReal.thy
src/HOL/Real/RComplete.ML
src/HOL/Real/Real.ML
src/HOL/Real/Real.thy
src/HOL/Real/RealAbs.ML
src/HOL/Real/RealDef.ML
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.ML
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/PNat.ML	Fri Jul 23 17:28:18 1999 +0200
     1.2 +++ b/src/HOL/Real/PNat.ML	Fri Jul 23 17:29:12 1999 +0200
     1.3 @@ -662,22 +662,23 @@
     1.4  (** embedding of naturals in positive naturals **)
     1.5  
     1.6  (* pnat_one_eq! *)
     1.7 -Goalw [pnat_nat_def,pnat_one_def]"1p = *#0";
     1.8 +Goalw [pnat_of_nat_def,pnat_one_def]"1p = pnat_of_nat 0";
     1.9  by (Full_simp_tac 1);
    1.10  qed "pnat_one_iff";
    1.11  
    1.12 -Goalw [pnat_nat_def,pnat_one_def,pnat_add_def] "1p + 1p = *#1";
    1.13 +Goalw [pnat_of_nat_def,pnat_one_def,
    1.14 +       pnat_add_def] "1p + 1p = pnat_of_nat 1";
    1.15  by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
    1.16  by (auto_tac (claset() addIs [(gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst)],
    1.17      simpset()));
    1.18  qed "pnat_two_eq";
    1.19  
    1.20 -Goal "inj(pnat_nat)";
    1.21 +Goal "inj(pnat_of_nat)";
    1.22  by (rtac injI 1);
    1.23 -by (rewtac pnat_nat_def);
    1.24 +by (rewtac pnat_of_nat_def);
    1.25  by (dtac (inj_on_Abs_pnat RS inj_onD) 1);
    1.26  by (auto_tac (claset() addSIs [gt_0_mem_pnat],simpset()));
    1.27 -qed "inj_pnat_nat";
    1.28 +qed "inj_pnat_of_nat";
    1.29  
    1.30  Goal "0 < n + 1";
    1.31  by Auto_tac;
    1.32 @@ -688,8 +689,9 @@
    1.33  qed "nat_add_one_less1";
    1.34  
    1.35  (* this worked with one call to auto_tac before! *)
    1.36 -Goalw [pnat_add_def,pnat_nat_def,pnat_one_def] 
    1.37 -          "*#n1 + *#n2 = *#(n1 + n2) + 1p";
    1.38 +Goalw [pnat_add_def,pnat_of_nat_def,pnat_one_def] 
    1.39 +      "pnat_of_nat n1 + pnat_of_nat n2 = \
    1.40 +\      pnat_of_nat (n1 + n2) + 1p";
    1.41  by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
    1.42  by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 1);
    1.43  by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 2);
    1.44 @@ -698,12 +700,12 @@
    1.45  by (auto_tac (claset(),
    1.46  	      simpset() addsimps [sum_Rep_pnat_sum,
    1.47  				  nat_add_one_less,nat_add_one_less1]));
    1.48 -qed "pnat_nat_add";
    1.49 +qed "pnat_of_nat_add";
    1.50  
    1.51 -Goalw [pnat_nat_def,pnat_less_def] "(n < m) = (*#n < *#m)";
    1.52 +Goalw [pnat_of_nat_def,pnat_less_def] 
    1.53 +       "(n < m) = (pnat_of_nat n < pnat_of_nat m)";
    1.54  by (auto_tac (claset(),simpset() 
    1.55      addsimps [Abs_pnat_inverse,Collect_pnat_gt_0]));
    1.56 -qed "pnat_nat_less_iff";
    1.57 +qed "pnat_of_nat_less_iff";
    1.58 +Addsimps [pnat_of_nat_less_iff RS sym];
    1.59  
    1.60 -Addsimps [pnat_nat_less_iff RS sym];
    1.61 -
     2.1 --- a/src/HOL/Real/PNat.thy	Fri Jul 23 17:28:18 1999 +0200
     2.2 +++ b/src/HOL/Real/PNat.thy	Fri Jul 23 17:29:12 1999 +0200
     2.3 @@ -7,10 +7,6 @@
     2.4  
     2.5  PNat = Arith +
     2.6  
     2.7 -(** type pnat **)
     2.8 -
     2.9 -(* type definition *)
    2.10 -
    2.11  typedef
    2.12    pnat = "lfp(%X. {1} Un (Suc``X))"   (lfp_def)
    2.13  
    2.14 @@ -24,14 +20,15 @@
    2.15  
    2.16  constdefs
    2.17    
    2.18 -  pnat_nat  :: nat => pnat                  ("*# _" [80] 80) 
    2.19 -  "*# n     == Abs_pnat(n + 1)"
    2.20 +  pnat_of_nat  :: nat => pnat           
    2.21 +  "pnat_of_nat n     == Abs_pnat(n + 1)"
    2.22   
    2.23  defs
    2.24  
    2.25 -  pnat_one_def      "1p == Abs_pnat(1)"
    2.26 -  pnat_Suc_def      "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
    2.27 -
    2.28 +  pnat_one_def      
    2.29 +       "1p == Abs_pnat(1)"
    2.30 +  pnat_Suc_def      
    2.31 +       "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
    2.32  
    2.33    pnat_add_def
    2.34         "x + y == Abs_pnat(Rep_pnat(x) +  Rep_pnat(y))"
    2.35 @@ -39,10 +36,10 @@
    2.36    pnat_mult_def
    2.37         "x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))"
    2.38  
    2.39 - pnat_less_def
    2.40 +  pnat_less_def
    2.41         "x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)"
    2.42  
    2.43 - pnat_le_def
    2.44 +  pnat_le_def
    2.45         "x <= (y::pnat) ==  ~(y < x)"
    2.46  
    2.47  end
     3.1 --- a/src/HOL/Real/PRat.ML	Fri Jul 23 17:28:18 1999 +0200
     3.2 +++ b/src/HOL/Real/PRat.ML	Fri Jul 23 17:29:12 1999 +0200
     3.3 @@ -86,10 +86,10 @@
     3.4  by (rtac Rep_prat_inverse 1);
     3.5  qed "inj_Rep_prat";
     3.6  
     3.7 -(** prat_pnat: the injection from pnat to prat **)
     3.8 -Goal "inj(prat_pnat)";
     3.9 +(** prat_of_pnat: the injection from pnat to prat **)
    3.10 +Goal "inj(prat_of_pnat)";
    3.11  by (rtac injI 1);
    3.12 -by (rewtac prat_pnat_def);
    3.13 +by (rewtac prat_of_pnat_def);
    3.14  by (dtac (inj_on_Abs_prat RS inj_onD) 1);
    3.15  by (REPEAT (rtac ratrel_in_prat 1));
    3.16  by (dtac eq_equiv_class 1);
    3.17 @@ -97,9 +97,8 @@
    3.18  by (Fast_tac 1);
    3.19  by Safe_tac;
    3.20  by (Asm_full_simp_tac 1);
    3.21 -qed "inj_prat_pnat";
    3.22 +qed "inj_prat_of_pnat";
    3.23  
    3.24 -(* lcp's original eq_Abs_Integ *)
    3.25  val [prem] = goal thy
    3.26      "(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P";
    3.27  by (res_inst_tac [("x1","z")] 
    3.28 @@ -139,7 +138,8 @@
    3.29  by (asm_full_simp_tac (simpset() addsimps [qinv_qinv]) 1);
    3.30  qed "inj_qinv";
    3.31  
    3.32 -Goalw [prat_pnat_def] "qinv($# (Abs_pnat 1)) = $#(Abs_pnat 1)";
    3.33 +Goalw [prat_of_pnat_def] 
    3.34 +      "qinv(prat_of_pnat  (Abs_pnat 1)) = prat_of_pnat (Abs_pnat 1)";
    3.35  by (simp_tac (simpset() addsimps [qinv]) 1);
    3.36  qed "qinv_1";
    3.37  
    3.38 @@ -244,49 +244,57 @@
    3.39  qed "prat_mult_left_commute";
    3.40  
    3.41  (*Positive Rational multiplication is an AC operator*)
    3.42 -val prat_mult_ac = [prat_mult_assoc,prat_mult_commute,prat_mult_left_commute];
    3.43 +val prat_mult_ac = [prat_mult_assoc,
    3.44 +                    prat_mult_commute,prat_mult_left_commute];
    3.45  
    3.46 -Goalw [prat_pnat_def] "($#Abs_pnat 1) * z = z";
    3.47 +Goalw [prat_of_pnat_def] 
    3.48 +      "(prat_of_pnat (Abs_pnat 1)) * z = z";
    3.49  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
    3.50 -by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
    3.51 +by (asm_full_simp_tac (simpset() addsimps 
    3.52 +   [prat_mult] @ pnat_mult_ac) 1);
    3.53  qed "prat_mult_1";
    3.54  
    3.55 -Goalw [prat_pnat_def] "z * ($#Abs_pnat 1) = z";
    3.56 +Goalw [prat_of_pnat_def] 
    3.57 +      "z * (prat_of_pnat (Abs_pnat 1)) = z";
    3.58  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
    3.59 -by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
    3.60 +by (asm_full_simp_tac (simpset() addsimps 
    3.61 +    [prat_mult] @ pnat_mult_ac) 1);
    3.62  qed "prat_mult_1_right";
    3.63  
    3.64 -Goalw [prat_pnat_def] 
    3.65 -            "$#((z1::pnat) + z2) = $#z1 + $#z2";
    3.66 +Goalw [prat_of_pnat_def] 
    3.67 +      "prat_of_pnat ((z1::pnat) + z2) = \
    3.68 +\      prat_of_pnat z1 + prat_of_pnat z2";
    3.69  by (asm_simp_tac (simpset() addsimps [prat_add,
    3.70         pnat_add_mult_distrib,pnat_mult_1]) 1);
    3.71 -qed "prat_pnat_add";
    3.72 +qed "prat_of_pnat_add";
    3.73  
    3.74 -Goalw [prat_pnat_def] 
    3.75 -            "$#((z1::pnat) * z2) = $#z1 * $#z2";
    3.76 +Goalw [prat_of_pnat_def] 
    3.77 +      "prat_of_pnat ((z1::pnat) * z2) = \
    3.78 +\      prat_of_pnat z1 * prat_of_pnat z2";
    3.79  by (asm_simp_tac (simpset() addsimps [prat_mult,
    3.80                                pnat_mult_1]) 1);
    3.81 -qed "prat_pnat_mult";
    3.82 +qed "prat_of_pnat_mult";
    3.83  
    3.84  (*** prat_mult and qinv ***)
    3.85  
    3.86 -Goalw [prat_def,prat_pnat_def] "qinv (q) * q = $# (Abs_pnat 1)";
    3.87 +Goalw [prat_def,prat_of_pnat_def] 
    3.88 +      "qinv (q) * q = prat_of_pnat (Abs_pnat 1)";
    3.89  by (res_inst_tac [("z","q")] eq_Abs_prat 1);
    3.90  by (asm_full_simp_tac (simpset() addsimps [qinv,
    3.91          prat_mult,pnat_mult_1,pnat_mult_1_left,
    3.92                          pnat_mult_commute]) 1);
    3.93  qed "prat_mult_qinv";
    3.94  
    3.95 -Goal "q * qinv (q) = $# (Abs_pnat 1)";
    3.96 +Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1)";
    3.97  by (rtac (prat_mult_commute RS subst) 1);
    3.98  by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
    3.99  qed "prat_mult_qinv_right";
   3.100  
   3.101 -Goal "? y. (x::prat) * y = $# Abs_pnat 1";
   3.102 +Goal "? y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
   3.103  by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
   3.104  qed "prat_qinv_ex";
   3.105  
   3.106 -Goal "?! y. (x::prat) * y = $# Abs_pnat 1";
   3.107 +Goal "?! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
   3.108  by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
   3.109  by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
   3.110  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
   3.111 @@ -294,7 +302,7 @@
   3.112      prat_mult_1,prat_mult_1_right]) 1);
   3.113  qed "prat_qinv_ex1";
   3.114  
   3.115 -Goal "?! y. y * (x::prat) = $# Abs_pnat 1";
   3.116 +Goal "?! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
   3.117  by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
   3.118  by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
   3.119  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
   3.120 @@ -302,7 +310,7 @@
   3.121      prat_mult_1,prat_mult_1_right]) 1);
   3.122  qed "prat_qinv_left_ex1";
   3.123  
   3.124 -Goal "x * y = $# Abs_pnat 1 ==> x = qinv y";
   3.125 +Goal "x * y = prat_of_pnat (Abs_pnat 1) ==> x = qinv y";
   3.126  by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
   3.127  by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
   3.128  by (Blast_tac 1);
   3.129 @@ -526,8 +534,9 @@
   3.130  by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"),
   3.131     ("q2.0","qinv (q2)")] prat_mult_left_less2_mono1 1);
   3.132  by Auto_tac;
   3.133 -by (dres_inst_tac [("q2.0","$#Abs_pnat 1")] prat_less_trans 1);
   3.134 -by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   3.135 +by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1)")] prat_less_trans 1);
   3.136 +by (auto_tac (claset(),simpset() addsimps 
   3.137 +    [prat_less_not_refl]));
   3.138  qed "lemma2_qinv_prat_less";
   3.139  
   3.140  Goal 
   3.141 @@ -538,25 +547,31 @@
   3.142                   lemma2_qinv_prat_less],simpset()));
   3.143  qed "qinv_prat_less";
   3.144  
   3.145 -Goal "!!(q1::prat). q1 < $#Abs_pnat 1 ==> $#Abs_pnat 1 < qinv(q1)";
   3.146 +Goal "!!(q1::prat). q1 < prat_of_pnat (Abs_pnat 1) \
   3.147 +\     ==> prat_of_pnat (Abs_pnat 1) < qinv(q1)";
   3.148  by (dtac qinv_prat_less 1);
   3.149  by (full_simp_tac (simpset() addsimps [qinv_1]) 1);
   3.150  qed "prat_qinv_gt_1";
   3.151  
   3.152 -Goalw [pnat_one_def] "!!(q1::prat). q1 < $#1p ==> $#1p < qinv(q1)";
   3.153 +Goalw [pnat_one_def] 
   3.154 +     "!!(q1::prat). q1 < prat_of_pnat 1p \
   3.155 +\     ==> prat_of_pnat 1p < qinv(q1)";
   3.156  by (etac prat_qinv_gt_1 1);
   3.157  qed "prat_qinv_is_gt_1";
   3.158  
   3.159 -Goalw [prat_less_def] "$#Abs_pnat 1 < $#Abs_pnat 1 + $#Abs_pnat 1";
   3.160 +Goalw [prat_less_def] 
   3.161 +      "prat_of_pnat (Abs_pnat 1) < prat_of_pnat (Abs_pnat 1) \
   3.162 +\                   + prat_of_pnat (Abs_pnat 1)";
   3.163  by (Fast_tac 1); 
   3.164  qed "prat_less_1_2";
   3.165  
   3.166 -Goal "qinv($#Abs_pnat 1 + $#Abs_pnat 1) < $#Abs_pnat 1";
   3.167 +Goal "qinv(prat_of_pnat (Abs_pnat 1) + \
   3.168 +\     prat_of_pnat (Abs_pnat 1)) < prat_of_pnat (Abs_pnat 1)";
   3.169  by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1);
   3.170  by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1);
   3.171  qed "prat_less_qinv_2_1";
   3.172  
   3.173 -Goal "!!(x::prat). x < y ==> x*qinv(y) < $#Abs_pnat 1";
   3.174 +Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1)";
   3.175  by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1);
   3.176  by (Asm_full_simp_tac 1);
   3.177  qed "prat_mult_qinv_less_1";
   3.178 @@ -578,7 +593,7 @@
   3.179  by (simp_tac (simpset() addsimps [prat_self_less_add_right]) 1);
   3.180  qed "prat_self_less_add_left";
   3.181  
   3.182 -Goalw [prat_less_def] "$#1p < y ==> (x::prat) < x * y";
   3.183 +Goalw [prat_less_def] "prat_of_pnat 1p < y ==> (x::prat) < x * y";
   3.184  by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
   3.185      prat_add_mult_distrib2]));
   3.186  qed "prat_self_less_mult_right";
   3.187 @@ -720,7 +735,8 @@
   3.188  qed "prat_add_left_less_cancel";
   3.189  
   3.190  (*** lemmas required for lemma_gleason9_34 in PReal : w*y > y/z ***)
   3.191 -Goalw [prat_pnat_def] "Abs_prat(ratrel^^{(x,y)}) = $#x*qinv($#y)";
   3.192 +Goalw [prat_of_pnat_def] 
   3.193 +      "Abs_prat(ratrel^^{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
   3.194  by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left,
   3.195      pnat_mult_1]));
   3.196  qed "Abs_prat_mult_qinv";
   3.197 @@ -730,28 +746,29 @@
   3.198  by (rtac prat_mult_left_le2_mono1 1);
   3.199  by (rtac qinv_prat_le 1);
   3.200  by (pnat_ind_tac "y" 1);
   3.201 -by (dres_inst_tac [("x","$#Abs_pnat 1")] prat_add_le2_mono1 2);
   3.202 +by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] prat_add_le2_mono1 2);
   3.203  by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2);
   3.204  by (auto_tac (claset() addIs [prat_le_trans],
   3.205      simpset() addsimps [prat_le_refl,
   3.206 -    pSuc_is_plus_one,pnat_one_def,prat_pnat_add]));
   3.207 +    pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
   3.208  qed "lemma_Abs_prat_le1";
   3.209  
   3.210  Goal "Abs_prat(ratrel^^{(x,Abs_pnat 1)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
   3.211  by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
   3.212  by (rtac prat_mult_le2_mono1 1);
   3.213  by (pnat_ind_tac "y" 1);
   3.214 -by (dres_inst_tac [("x","$#x")] prat_add_le2_mono1 2);
   3.215 -by (cut_inst_tac [("z","$#x")] (prat_self_less_add_self 
   3.216 +by (dres_inst_tac [("x","prat_of_pnat x")] prat_add_le2_mono1 2);
   3.217 +by (cut_inst_tac [("z","prat_of_pnat x")] (prat_self_less_add_self 
   3.218      RS prat_less_imp_le) 2);
   3.219  by (auto_tac (claset() addIs [prat_le_trans],
   3.220      simpset() addsimps [prat_le_refl,
   3.221      pSuc_is_plus_one,pnat_one_def,prat_add_mult_distrib2,
   3.222 -    prat_pnat_add,prat_pnat_mult]));
   3.223 +    prat_of_pnat_add,prat_of_pnat_mult]));
   3.224  qed "lemma_Abs_prat_le2";
   3.225  
   3.226  Goal "Abs_prat(ratrel^^{(x,z)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
   3.227 -by (fast_tac (claset() addIs [prat_le_trans,lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
   3.228 +by (fast_tac (claset() addIs [prat_le_trans,
   3.229 +    lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
   3.230  qed "lemma_Abs_prat_le3";
   3.231  
   3.232  Goal "Abs_prat(ratrel^^{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel^^{(w,x)}) = \
   3.233 @@ -766,61 +783,62 @@
   3.234      [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
   3.235  qed "pre_lemma_gleason9_34b";
   3.236  
   3.237 -Goal "($#n < $#m) = (n < m)";
   3.238 +Goal "(prat_of_pnat n < prat_of_pnat m) = (n < m)";
   3.239  by (auto_tac (claset(),simpset() addsimps [prat_less_def,
   3.240 -    pnat_less_iff,prat_pnat_add]));
   3.241 +    pnat_less_iff,prat_of_pnat_add]));
   3.242  by (res_inst_tac [("z","T")] eq_Abs_prat 1);
   3.243  by (auto_tac (claset() addDs [pnat_eq_lessI],
   3.244      simpset() addsimps [prat_add,pnat_mult_1,
   3.245 -    pnat_mult_1_left,prat_pnat_def,pnat_less_iff RS sym]));
   3.246 -qed "prat_pnat_less_iff";
   3.247 +    pnat_mult_1_left,prat_of_pnat_def,pnat_less_iff RS sym]));
   3.248 +qed "prat_of_pnat_less_iff";
   3.249  
   3.250 -Addsimps [prat_pnat_less_iff];
   3.251 +Addsimps [prat_of_pnat_less_iff];
   3.252  
   3.253 -(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)
   3.254 +(*------------------------------------------------------------------*)
   3.255  
   3.256  (*** prove witness that will be required to prove non-emptiness ***)
   3.257 -(*** of preal type as defined using Dedekind Sections in PReal ***)
   3.258 +(*** of preal type as defined using Dedekind Sections in PReal  ***)
   3.259  (*** Show that exists positive real `one' ***)
   3.260  
   3.261 -Goal "? q. q: {x::prat. x < $#Abs_pnat 1}";
   3.262 +Goal "? q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
   3.263  by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
   3.264  qed "lemma_prat_less_1_memEx";
   3.265  
   3.266 -Goal "{x::prat. x < $#Abs_pnat 1} ~= {}";
   3.267 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {}";
   3.268  by (rtac notI 1);
   3.269  by (cut_facts_tac [lemma_prat_less_1_memEx] 1);
   3.270  by (Asm_full_simp_tac 1);
   3.271  qed "lemma_prat_less_1_set_non_empty";
   3.272  
   3.273 -Goalw [psubset_def] "{} < {x::prat. x < $#Abs_pnat 1}";
   3.274 +Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
   3.275  by (asm_full_simp_tac (simpset() addsimps 
   3.276           [lemma_prat_less_1_set_non_empty RS not_sym]) 1);
   3.277  qed "empty_set_psubset_lemma_prat_less_1_set";
   3.278  
   3.279 -(*** exists rational not in set --- $#Abs_pnat 1 itself ***)
   3.280 -Goal "? q. q ~: {x::prat. x < $#Abs_pnat 1}";
   3.281 -by (res_inst_tac [("x","$#Abs_pnat 1")] exI 1);
   3.282 +(*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
   3.283 +Goal "? q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
   3.284 +by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
   3.285  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   3.286  qed "lemma_prat_less_1_not_memEx";
   3.287  
   3.288 -Goal "{x::prat. x < $#Abs_pnat 1} ~= {q::prat. True}";
   3.289 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {q::prat. True}";
   3.290  by (rtac notI 1);
   3.291  by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
   3.292  by (Asm_full_simp_tac 1);
   3.293  qed "lemma_prat_less_1_set_not_rat_set";
   3.294  
   3.295  Goalw [psubset_def,subset_def] 
   3.296 -      "{x::prat. x < $#Abs_pnat 1} < {q::prat. True}";
   3.297 +      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < {q::prat. True}";
   3.298  by (asm_full_simp_tac (simpset() addsimps 
   3.299        [lemma_prat_less_1_set_not_rat_set,
   3.300         lemma_prat_less_1_not_memEx]) 1);
   3.301  qed "lemma_prat_less_1_set_psubset_rat_set";
   3.302  
   3.303  (*** prove non_emptiness of type ***)
   3.304 -Goal "{x::prat. x < $#Abs_pnat 1} : {A. {} < A & A < {q::prat. True} & \
   3.305 -\                                        (!y: A. ((!z. z < y --> z: A) & \
   3.306 -\                                        (? u: A. y < u)))}";
   3.307 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
   3.308 +\               A < {q::prat. True} & \
   3.309 +\               (!y: A. ((!z. z < y --> z: A) & \
   3.310 +\               (? u: A. y < u)))}";
   3.311  by (auto_tac (claset() addDs [prat_less_trans],
   3.312      simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set,
   3.313                         lemma_prat_less_1_set_psubset_rat_set]));
     4.1 --- a/src/HOL/Real/PRat.thy	Fri Jul 23 17:28:18 1999 +0200
     4.2 +++ b/src/HOL/Real/PRat.thy	Fri Jul 23 17:29:12 1999 +0200
     4.3 @@ -18,11 +18,11 @@
     4.4  
     4.5  constdefs
     4.6  
     4.7 -  prat_pnat :: pnat => prat              ("$#_" [80] 80)
     4.8 -  "$# m     == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
     4.9 +  prat_of_pnat :: pnat => prat           
    4.10 +  "prat_of_pnat m     == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
    4.11  
    4.12    qinv      :: prat => prat
    4.13 -  "qinv(Q)  == Abs_prat(UN p:Rep_prat(Q). split (%x y. ratrel^^{(y,x)}) p)" 
    4.14 +  "qinv(Q)  == Abs_prat(UN (x,y):Rep_prat(Q). ratrel^^{(y,x)})" 
    4.15  
    4.16  defs
    4.17  
     5.1 --- a/src/HOL/Real/PReal.ML	Fri Jul 23 17:28:18 1999 +0200
     5.2 +++ b/src/HOL/Real/PReal.ML	Fri Jul 23 17:29:12 1999 +0200
     5.3 @@ -31,7 +31,7 @@
     5.4  
     5.5  Addsimps [empty_not_mem_preal];
     5.6  
     5.7 -Goalw [preal_def] "{x::prat. x < $#Abs_pnat 1} : preal";
     5.8 +Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : preal";
     5.9  by (rtac preal_1 1);
    5.10  qed "one_set_mem_preal";
    5.11  
    5.12 @@ -114,7 +114,7 @@
    5.13  by (blast_tac (claset() addIs [set_ext] addEs [swap]) 1);
    5.14  qed "not_mem_Rep_preal_Ex";
    5.15  
    5.16 -(** prat_pnat: the injection from prat to preal **)
    5.17 +(** preal_of_prat: the injection from prat to preal **)
    5.18  (** A few lemmas **)
    5.19  Goal "{} < {xa::prat. xa < y}";
    5.20  by (cut_facts_tac [qless_Ex] 1);
    5.21 @@ -145,14 +145,14 @@
    5.22  by (auto_tac (claset() addDs [prat_less_not_sym],simpset()));
    5.23  qed "lemma_prat_set_eq";
    5.24  
    5.25 -Goal "inj(preal_prat)";
    5.26 +Goal "inj(preal_of_prat)";
    5.27  by (rtac injI 1);
    5.28 -by (rewtac preal_prat_def);
    5.29 +by (rewtac preal_of_prat_def);
    5.30  by (dtac (inj_on_Abs_preal RS inj_onD) 1);
    5.31  by (rtac lemma_prat_less_set_mem_preal 1);
    5.32  by (rtac lemma_prat_less_set_mem_preal 1);
    5.33  by (etac lemma_prat_set_eq 1);
    5.34 -qed "inj_preal_prat";
    5.35 +qed "inj_preal_of_prat";
    5.36  
    5.37        (*** theorems for ordering ***)
    5.38  (* prove introduction and elimination rules for preal_less *)
    5.39 @@ -249,9 +249,9 @@
    5.40  \         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
    5.41  by Auto_tac;
    5.42  by (forward_tac [prat_mult_qinv_less_1] 1);
    5.43 -by (forw_inst_tac [("x","x"),("q2.0","$#Abs_pnat 1")] 
    5.44 +by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
    5.45      prat_mult_less2_mono1 1);
    5.46 -by (forw_inst_tac [("x","ya"),("q2.0","$#Abs_pnat 1")] 
    5.47 +by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
    5.48      prat_mult_less2_mono1 1);
    5.49  by (Asm_full_simp_tac 1);
    5.50  by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
    5.51 @@ -385,7 +385,8 @@
    5.52  
    5.53  (* Positive Real 1 is the multiplicative identity element *) 
    5.54  (* long *)
    5.55 -Goalw [preal_prat_def,preal_mult_def] "(@#($#Abs_pnat 1)) * z = z";
    5.56 +Goalw [preal_of_prat_def,preal_mult_def] 
    5.57 +      "(preal_of_prat (prat_of_pnat (Abs_pnat 1))) * z = z";
    5.58  by (rtac (Rep_preal_inverse RS subst) 1);
    5.59  by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
    5.60  by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
    5.61 @@ -401,7 +402,7 @@
    5.62  by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
    5.63  qed "preal_mult_1";
    5.64  
    5.65 -Goal "z * (@#($#Abs_pnat 1)) = z";
    5.66 +Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1))) = z";
    5.67  by (rtac (preal_mult_commute RS subst) 1);
    5.68  by (rtac preal_mult_1 1);
    5.69  qed "preal_mult_1_right";
    5.70 @@ -585,9 +586,10 @@
    5.71  qed "preal_mem_inv_set";
    5.72  
    5.73  (*more lemmas for inverse *)
    5.74 -Goal "x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
    5.75 +Goal "x: Rep_preal(pinv(A)*A) ==> \
    5.76 +\     x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
    5.77  by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
    5.78 -              simpset() addsimps [pinv_def,preal_prat_def] ));
    5.79 +              simpset() addsimps [pinv_def,preal_of_prat_def] ));
    5.80  by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
    5.81  by (auto_tac (claset() addSDs [not_in_preal_ub],simpset()));
    5.82  by (dtac prat_mult_less_mono 1 THEN Blast_tac 1);
    5.83 @@ -596,11 +598,12 @@
    5.84  
    5.85  (*** Gleason's Lemma 9-3.4 p 122 ***)
    5.86  Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
    5.87 -\            ? xb : Rep_preal(A). xb + ($#p)*x : Rep_preal(A)";
    5.88 +\            ? xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
    5.89  by (cut_facts_tac [mem_Rep_preal_Ex] 1);
    5.90  by (res_inst_tac [("n","p")] pnat_induct 1);
    5.91  by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
    5.92 -    pSuc_is_plus_one,prat_add_mult_distrib,prat_pnat_add,prat_add_assoc RS sym]));
    5.93 +    pSuc_is_plus_one,prat_add_mult_distrib,
    5.94 +   prat_of_pnat_add,prat_add_assoc RS sym]));
    5.95  qed "lemma1_gleason9_34";
    5.96  
    5.97  Goal "Abs_prat (ratrel ^^ {(y, z)}) < xb + \
    5.98 @@ -622,9 +625,9 @@
    5.99  by (etac bexE 1);
   5.100  by (cut_inst_tac [("x","y"),("y","xb"),("w","xaa"),
   5.101      ("z","ya"),("xb","xba")] lemma1b_gleason9_34 1);
   5.102 -by (dres_inst_tac [("x","xba + $#(y * xb) * x")]  bspec 1);
   5.103 +by (dres_inst_tac [("x","xba + prat_of_pnat (y * xb) * x")]  bspec 1);
   5.104  by (auto_tac (claset() addIs [prat_less_asym],
   5.105 -    simpset() addsimps [prat_pnat_def]));
   5.106 +    simpset() addsimps [prat_of_pnat_def]));
   5.107  qed "lemma_gleason9_34a";
   5.108  
   5.109  Goal "? r: Rep_preal(R). r + x ~: Rep_preal(R)";
   5.110 @@ -648,7 +651,7 @@
   5.111  (******)
   5.112  
   5.113  (*** FIXME: long! ***)
   5.114 -Goal "$#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.115 +Goal "prat_of_pnat 1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.116  by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
   5.117  by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
   5.118  by (Fast_tac 1);
   5.119 @@ -671,15 +674,17 @@
   5.120  by Auto_tac;
   5.121  qed "lemma_gleason9_36";
   5.122  
   5.123 -Goal "$#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.124 +Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
   5.125 +\     ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.126  by (rtac lemma_gleason9_36 1);
   5.127  by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
   5.128  qed "lemma_gleason9_36a";
   5.129  
   5.130  (*** Part 2 of existence of inverse ***)
   5.131 -Goal "x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
   5.132 +Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1))) \
   5.133 +\     ==> x: Rep_preal(pinv(A)*A)";
   5.134  by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
   5.135 -              simpset() addsimps [pinv_def,preal_prat_def] ));
   5.136 +              simpset() addsimps [pinv_def,preal_of_prat_def] ));
   5.137  by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
   5.138  by (dtac prat_qinv_gt_1 1);
   5.139  by (dres_inst_tac [("A","A")] lemma_gleason9_36a 1);
   5.140 @@ -696,13 +701,13 @@
   5.141      prat_mult_left_commute]));
   5.142  qed "preal_mem_mult_invI";
   5.143  
   5.144 -Goal "pinv(A)*A = (@#($#Abs_pnat 1))";
   5.145 +Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
   5.146  by (rtac (inj_Rep_preal RS injD) 1);
   5.147  by (rtac set_ext 1);
   5.148  by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
   5.149  qed "preal_mult_inv";
   5.150  
   5.151 -Goal "A*pinv(A) = (@#($#Abs_pnat 1))";
   5.152 +Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
   5.153  by (rtac (preal_mult_commute RS subst) 1);
   5.154  by (rtac preal_mult_inv 1);
   5.155  qed "preal_mult_inv_right";
   5.156 @@ -1240,8 +1245,9 @@
   5.157  by (etac lemma_preal_rat_less 1);
   5.158  qed "lemma_preal_rat_less2";
   5.159  
   5.160 -Goalw [preal_prat_def,preal_add_def] 
   5.161 -            "@#((z1::prat) + z2) = @#z1 + @#z2";
   5.162 +Goalw [preal_of_prat_def,preal_add_def] 
   5.163 +      "preal_of_prat ((z1::prat) + z2) = \
   5.164 +\      preal_of_prat z1 + preal_of_prat z2";
   5.165  by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   5.166  by (auto_tac (claset() addIs [prat_add_less_mono] addSIs [set_ext],simpset() addsimps 
   5.167      [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
   5.168 @@ -1251,7 +1257,7 @@
   5.169  by (etac lemma_preal_rat_less2 1);
   5.170  by (asm_full_simp_tac (simpset() addsimps [prat_add_mult_distrib RS sym,
   5.171       prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
   5.172 -qed "preal_prat_add";
   5.173 +qed "preal_of_prat_add";
   5.174  
   5.175  Goal "x < xa ==> x*z1*qinv(xa) < z1";
   5.176  by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
   5.177 @@ -1265,8 +1271,9 @@
   5.178  by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
   5.179  qed "lemma_preal_rat_less4";
   5.180  
   5.181 -Goalw [preal_prat_def,preal_mult_def] 
   5.182 -            "@#((z1::prat) * z2) = @#z1 * @#z2";
   5.183 +Goalw [preal_of_prat_def,preal_mult_def] 
   5.184 +      "preal_of_prat ((z1::prat) * z2) = \
   5.185 +\      preal_of_prat z1 * preal_of_prat z2";
   5.186  by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   5.187  by (auto_tac (claset() addIs [prat_mult_less_mono] addSIs [set_ext],simpset() addsimps 
   5.188      [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
   5.189 @@ -1280,15 +1287,15 @@
   5.190      addsimps [qinv_mult_eq RS sym] @ prat_mult_ac) 1);
   5.191  by (asm_full_simp_tac (simpset() 
   5.192      addsimps [prat_mult_assoc RS sym]) 1);
   5.193 -qed "preal_prat_mult";
   5.194 +qed "preal_of_prat_mult";
   5.195  
   5.196 -Goalw [preal_prat_def,preal_less_def] 
   5.197 -      "(@#p < @#q) = (p < q)";
   5.198 +Goalw [preal_of_prat_def,preal_less_def] 
   5.199 +      "(preal_of_prat p < preal_of_prat q) = (p < q)";
   5.200  by (auto_tac (claset() addSDs [lemma_prat_set_eq] addEs [prat_less_trans],
   5.201      simpset() addsimps [lemma_prat_less_set_mem_preal,
   5.202      psubset_def,prat_less_not_refl]));
   5.203  by (res_inst_tac [("q1.0","p"),("q2.0","q")] prat_linear_less2 1);
   5.204  by (auto_tac (claset() addIs [prat_less_irrefl],simpset()));
   5.205 -qed "preal_prat_less_iff";
   5.206 +qed "preal_of_prat_less_iff";
   5.207  
   5.208 -Addsimps [preal_prat_less_iff];
   5.209 +Addsimps [preal_of_prat_less_iff];
     6.1 --- a/src/HOL/Real/PReal.thy	Fri Jul 23 17:28:18 1999 +0200
     6.2 +++ b/src/HOL/Real/PReal.thy	Fri Jul 23 17:29:12 1999 +0200
     6.3 @@ -15,8 +15,8 @@
     6.4     preal :: {ord, plus, times}
     6.5  
     6.6  constdefs
     6.7 -  preal_prat :: prat => preal              ("@#_" [80] 80)
     6.8 -   "@# q     == Abs_preal({x::prat. x < q})"
     6.9 +  preal_of_prat :: prat => preal             
    6.10 +   "preal_of_prat q     == Abs_preal({x::prat. x < q})"
    6.11  
    6.12    pinv       :: preal => preal
    6.13    "pinv(R)   == Abs_preal({w. ? y. w < y & qinv y ~: Rep_preal(R)})" 
     7.1 --- a/src/HOL/Real/RComplete.ML	Fri Jul 23 17:28:18 1999 +0200
     7.2 +++ b/src/HOL/Real/RComplete.ML	Fri Jul 23 17:29:12 1999 +0200
     7.3 @@ -10,6 +10,75 @@
     7.4  
     7.5  claset_ref() := claset() delWrapper "bspec";
     7.6  
     7.7 +(*---------------------------------------------------------
     7.8 +       Completeness of reals: use supremum property of 
     7.9 +       preal and theorems about real_preal. Theorems 
    7.10 +       previously in Real.ML. 
    7.11 + ---------------------------------------------------------*)
    7.12 + (*a few lemmas*)
    7.13 +Goal "! x:P. 0r < x ==> \ 
    7.14 +\       ((? x:P. y < x) = (? X. real_of_preal X : P & \
    7.15 +\                          y < real_of_preal X))";
    7.16 +by (blast_tac (claset() addSDs [bspec,
    7.17 +    real_gt_zero_preal_Ex RS iffD1]) 1);
    7.18 +qed "real_sup_lemma1";
    7.19 +
    7.20 +Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
    7.21 +\         ==> (? X. X: {w. real_of_preal w : P}) & \
    7.22 +\             (? Y. !X: {w. real_of_preal w : P}. X < Y)";
    7.23 +by (rtac conjI 1);
    7.24 +by (blast_tac (claset() addDs [bspec,
    7.25 +    real_gt_zero_preal_Ex RS iffD1]) 1);
    7.26 +by Auto_tac;
    7.27 +by (dtac bspec 1 THEN assume_tac 1);
    7.28 +by (forward_tac [bspec] 1  THEN assume_tac 1);
    7.29 +by (dtac real_less_trans 1 THEN assume_tac 1);
    7.30 +by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1);
    7.31 +by (res_inst_tac [("x","ya")] exI 1);
    7.32 +by Auto_tac;
    7.33 +by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1);
    7.34 +by (etac real_of_preal_lessD 1);
    7.35 +qed "real_sup_lemma2";
    7.36 +
    7.37 +(*-------------------------------------------------------------
    7.38 +            Completeness of Positive Reals
    7.39 + -------------------------------------------------------------*)
    7.40 +
    7.41 +(* Supremum property for the set of positive reals *)
    7.42 +(* FIXME: long proof - can be improved - need only have 
    7.43 +   one case split *) (* will do for now *)
    7.44 +Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
    7.45 +\         ==> (? S. !y. (? x: P. y < x) = (y < S))";
    7.46 +by (res_inst_tac 
    7.47 +   [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
    7.48 +by Auto_tac;
    7.49 +by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
    7.50 +by (case_tac "0r < ya" 1);
    7.51 +by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
    7.52 +by (dtac real_less_all_real2 2);
    7.53 +by Auto_tac;
    7.54 +by (rtac (preal_complete RS spec RS iffD1) 1);
    7.55 +by Auto_tac;
    7.56 +by (forward_tac [real_gt_preal_preal_Ex] 1);
    7.57 +by Auto_tac;
    7.58 +(* second part *)
    7.59 +by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
    7.60 +by (case_tac "0r < ya" 1);
    7.61 +by (auto_tac (claset() addSDs [real_less_all_real2,
    7.62 +        real_gt_zero_preal_Ex RS iffD1],simpset()));
    7.63 +by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac);
    7.64 +by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
    7.65 +by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
    7.66 +by (Blast_tac 3);
    7.67 +by (Blast_tac 1);
    7.68 +by (Blast_tac 1);
    7.69 +by (Blast_tac 1);
    7.70 +qed "posreal_complete";
    7.71 +
    7.72 +(*--------------------------------------------------------
    7.73 +   Completeness properties using isUb, isLub etc.
    7.74 + -------------------------------------------------------*)
    7.75 +
    7.76  Goal "!!(x::real). [| isLub R S x; isLub R S y |] ==> x = y";
    7.77  by (forward_tac [isLub_isUb] 1);
    7.78  by (forw_inst_tac [("x","y")] isLub_isUb 1);
    7.79 @@ -30,26 +99,26 @@
    7.80  \                 EX x. x: S; \
    7.81  \                 EX u. isUb (UNIV::real set) S u \
    7.82  \              |] ==> EX t. isLub (UNIV::real set) S t";
    7.83 -by (res_inst_tac [("x","%#psup({w. %#w : S})")] exI 1);
    7.84 +by (res_inst_tac [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1);
    7.85  by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def]));
    7.86  by (auto_tac (claset() addSIs [setleI,setgeI] 
    7.87  	               addSDs [real_gt_zero_preal_Ex RS iffD1],simpset()));
    7.88  by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
    7.89  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
    7.90 -by (auto_tac (claset(), simpset() addsimps [real_preal_le_iff]));
    7.91 +by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
    7.92  by (rtac preal_psup_leI2a 1);
    7.93 -by (forw_inst_tac [("y","%#ya")] setleD 1 THEN assume_tac 1);
    7.94 +by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1);
    7.95  by (forward_tac  [real_ge_preal_preal_Ex] 1);
    7.96  by (Step_tac 1);
    7.97  by (res_inst_tac [("x","y")] exI 1);
    7.98 -by (blast_tac (claset() addSDs [setleD] addIs [real_preal_le_iff RS iffD1]) 1);
    7.99 +by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1);
   7.100  by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
   7.101  by (forward_tac [isUbD2] 1);
   7.102  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
   7.103  by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
   7.104 -	      simpset() addsimps [real_preal_le_iff]));
   7.105 +	      simpset() addsimps [real_of_preal_le_iff]));
   7.106  by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] 
   7.107 -	                addIs [real_preal_le_iff RS iffD1]) 1);
   7.108 +	                addIs [real_of_preal_le_iff RS iffD1]) 1);
   7.109  qed "posreals_complete";
   7.110  
   7.111  
   7.112 @@ -142,24 +211,26 @@
   7.113  qed "reals_complete";
   7.114  
   7.115  (*----------------------------------------------------------------
   7.116 -        Related property: Archimedean property of reals
   7.117 +        Related: Archimedean property of reals
   7.118   ----------------------------------------------------------------*)
   7.119  
   7.120 -Goal "0r < x ==> EX n. rinv(%%#n) < x";
   7.121 -by (stac real_nat_rinv_Ex_iff 1);
   7.122 +Goal "0r < x ==> EX n. rinv(real_of_posnat n) < x";
   7.123 +by (stac real_of_posnat_rinv_Ex_iff 1);
   7.124  by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
   7.125  by (fold_tac [real_le_def]);
   7.126 -by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} 1r" 1);
   7.127 -by (subgoal_tac "EX X. X : {z. EX n. z = x*%%#n}" 1);
   7.128 +by (subgoal_tac "isUb (UNIV::real set) \
   7.129 +\   {z. EX n. z = x*(real_of_posnat n)} 1r" 1);
   7.130 +by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1);
   7.131  by (dtac reals_complete 1);
   7.132  by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
   7.133 -by (subgoal_tac "ALL m. x*(%%#Suc m) <= t" 1);
   7.134 +by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1);
   7.135  by (asm_full_simp_tac (simpset() addsimps 
   7.136 -   [real_nat_Suc,real_add_mult_distrib2]) 1);
   7.137 +   [real_of_posnat_Suc,real_add_mult_distrib2]) 1);
   7.138  by (blast_tac (claset() addIs [isLubD2]) 2);
   7.139  by (asm_full_simp_tac
   7.140      (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
   7.141 -by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + -x)" 1);
   7.142 +by (subgoal_tac "isUb (UNIV::real set) \
   7.143 +\   {z. EX n. z = x*(real_of_posnat n)} (t + -x)" 1);
   7.144  by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
   7.145  by (dres_inst_tac [("y","t+-x")] isLub_le_isUb 1);
   7.146  by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
   7.147 @@ -168,20 +239,20 @@
   7.148  	      simpset() addsimps [real_less_not_refl,real_add_assoc RS sym]));
   7.149  qed "reals_Archimedean";
   7.150  
   7.151 -Goal "EX n. (x::real) < %%#n";
   7.152 +Goal "EX n. (x::real) < real_of_posnat n";
   7.153  by (res_inst_tac [("R1.0","x"),("R2.0","0r")] real_linear_less2 1);
   7.154  by (res_inst_tac [("x","0")] exI 1);
   7.155  by (res_inst_tac [("x","0")] exI 2);
   7.156  by (auto_tac (claset() addEs [real_less_trans],
   7.157 -	      simpset() addsimps [real_nat_one,real_zero_less_one]));
   7.158 +	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
   7.159  by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1);
   7.160  by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
   7.161  by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1);
   7.162  by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
   7.163  by (dres_inst_tac [("n1","n"),("y","1r")] 
   7.164 -     (real_nat_less_zero RS real_mult_less_mono2)  1);
   7.165 +     (real_of_posnat_less_zero RS real_mult_less_mono2)  1);
   7.166  by (auto_tac (claset(),
   7.167 -	      simpset() addsimps [real_nat_less_zero,
   7.168 +	      simpset() addsimps [real_of_posnat_less_zero,
   7.169  				  real_not_refl2 RS not_sym,
   7.170  				  real_mult_assoc RS sym]));
   7.171  qed "reals_Archimedean2";
     8.1 --- a/src/HOL/Real/Real.ML	Fri Jul 23 17:28:18 1999 +0200
     8.2 +++ b/src/HOL/Real/Real.ML	Fri Jul 23 17:29:12 1999 +0200
     8.3 @@ -1,38 +1,34 @@
     8.4 -(*  Title:      HOL/Real/Real.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1998  University of Cambridge
     8.8 -
     8.9 -Type "real" is a linear order
    8.10 +(*  Title:       HOL/Real/Real.ML
    8.11 +    Author:      Lawrence C. Paulson
    8.12 +                 Jacques D. Fleuriot
    8.13 +    Copyright:   1998  University of Cambridge
    8.14 +    Description: Type "real" is a linear order
    8.15  *)
    8.16  
    8.17 -
    8.18 -
    8.19 -(** lemma **)
    8.20 -Goal "(0r < x) = (? y. x = %#y)";
    8.21 -by (auto_tac (claset(),simpset() addsimps [real_preal_zero_less]));
    8.22 -by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
    8.23 +Goal "(0r < x) = (? y. x = real_of_preal y)";
    8.24 +by (auto_tac (claset(),simpset() addsimps [real_of_preal_zero_less]));
    8.25 +by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
    8.26  by (blast_tac (claset() addSEs [real_less_irrefl,
    8.27 -     real_preal_not_minus_gt_zero RS notE]) 1);
    8.28 +     real_of_preal_not_minus_gt_zero RS notE]) 1);
    8.29  qed "real_gt_zero_preal_Ex";
    8.30  
    8.31 -Goal "%#z < x ==> ? y. x = %#y";
    8.32 -by (blast_tac (claset() addSDs [real_preal_zero_less RS real_less_trans]
    8.33 +Goal "real_of_preal z < x ==> ? y. x = real_of_preal y";
    8.34 +by (blast_tac (claset() addSDs [real_of_preal_zero_less RS real_less_trans]
    8.35                 addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
    8.36  qed "real_gt_preal_preal_Ex";
    8.37  
    8.38 -Goal "%#z <= x ==> ? y. x = %#y";
    8.39 +Goal "real_of_preal z <= x ==> ? y. x = real_of_preal y";
    8.40  by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
    8.41                real_gt_preal_preal_Ex]) 1);
    8.42  qed "real_ge_preal_preal_Ex";
    8.43  
    8.44 -Goal "y <= 0r ==> !x. y < %#x";
    8.45 +Goal "y <= 0r ==> !x. y < real_of_preal x";
    8.46  by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
    8.47 -              addIs [real_preal_zero_less RSN(2,real_less_trans)],
    8.48 -              simpset() addsimps [real_preal_zero_less]));
    8.49 +              addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
    8.50 +              simpset() addsimps [real_of_preal_zero_less]));
    8.51  qed "real_less_all_preal";
    8.52  
    8.53 -Goal "~ 0r < y ==> !x. y < %#x";
    8.54 +Goal "~ 0r < y ==> !x. y < real_of_preal x";
    8.55  by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
    8.56  qed "real_less_all_real2";
    8.57  
    8.58 @@ -66,7 +62,7 @@
    8.59  by (blast_tac (claset() addIs [real_less_trans]) 2);
    8.60  by (auto_tac (claset(),
    8.61  	      simpset() addsimps 
    8.62 -	      [real_gt_zero_preal_Ex,real_preal_minus_less_self]));
    8.63 +	      [real_gt_zero_preal_Ex,real_of_preal_minus_less_self]));
    8.64  qed "real_gt_zero_iff";
    8.65  
    8.66  Goal "(x < 0r) = (x < -x)";
    8.67 @@ -83,17 +79,17 @@
    8.68  by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym]));
    8.69  qed "real_le_zero_iff";
    8.70  
    8.71 -Goal "(%#m1 <= %#m2) = (m1 <= m2)";
    8.72 +Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)";
    8.73  by (auto_tac (claset() addSIs [preal_leI],
    8.74      simpset() addsimps [real_less_le_iff RS sym]));
    8.75  by (dtac preal_le_less_trans 1 THEN assume_tac 1);
    8.76  by (etac preal_less_irrefl 1);
    8.77 -qed "real_preal_le_iff";
    8.78 +qed "real_of_preal_le_iff";
    8.79  
    8.80  Goal "!!(x::real). [| 0r < x; 0r < y |] ==> 0r < x * y";
    8.81  by (auto_tac (claset(),simpset() addsimps [real_gt_zero_preal_Ex]));  
    8.82  by (res_inst_tac [("x","y*ya")] exI 1);
    8.83 -by (full_simp_tac (simpset() addsimps [real_preal_mult]) 1);
    8.84 +by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1);
    8.85  qed "real_mult_order";
    8.86  
    8.87  Goal "!!(x::real). [| x < 0r; y < 0r |] ==> 0r < x * y";
    8.88 @@ -108,6 +104,12 @@
    8.89  	      simpset()));
    8.90  qed "real_le_mult_order";
    8.91  
    8.92 +Goal "!!(x::real). [| 0r < x; 0r <= y |] ==> 0r <= x * y";
    8.93 +by (dtac real_le_imp_less_or_eq 1);
    8.94 +by (auto_tac (claset() addIs [real_mult_order,
    8.95 +    real_less_imp_le],simpset()));
    8.96 +qed "real_less_le_mult_order";
    8.97 +
    8.98  Goal "!!(x::real). [| x <= 0r; y <= 0r |] ==> 0r <= x * y";
    8.99  by (rtac real_less_or_eq_imp_le 1);
   8.100  by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
   8.101 @@ -135,67 +137,9 @@
   8.102  
   8.103  Goalw [real_one_def] "0r < 1r";
   8.104  by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2],
   8.105 -    simpset() addsimps [real_preal_def]));
   8.106 +    simpset() addsimps [real_of_preal_def]));
   8.107  qed "real_zero_less_one";
   8.108  
   8.109 -(*** Completeness of reals ***)
   8.110 -(** use supremum property of preal and theorems about real_preal **)
   8.111 -              (*** a few lemmas ***)
   8.112 -Goal "! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
   8.113 -by (blast_tac (claset() addSDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
   8.114 -qed "real_sup_lemma1";
   8.115 -
   8.116 -Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
   8.117 -\         ==> (? X. X: {w. %#w : P}) & (? Y. !X: {w. %#w : P}. X < Y)";
   8.118 -by (rtac conjI 1);
   8.119 -by (blast_tac (claset() addDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
   8.120 -by Auto_tac;
   8.121 -by (dtac bspec 1 THEN assume_tac 1);
   8.122 -by (forward_tac [bspec] 1  THEN assume_tac 1);
   8.123 -by (dtac real_less_trans 1 THEN assume_tac 1);
   8.124 -by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1);
   8.125 -by (res_inst_tac [("x","ya")] exI 1);
   8.126 -by Auto_tac;
   8.127 -by (dres_inst_tac [("x","%#X")] bspec 1 THEN assume_tac 1);
   8.128 -by (etac real_preal_lessD 1);
   8.129 -qed "real_sup_lemma2";
   8.130 -
   8.131 -(*-------------------------------------------------------------
   8.132 -            Completeness of Positive Reals
   8.133 - -------------------------------------------------------------*)
   8.134 -
   8.135 -(* Supremum property for the set of positive reals *)
   8.136 -(* FIXME: long proof - can be improved - need only have one case split *)
   8.137 -(* will do for now *)
   8.138 -Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
   8.139 -\         ==> (? S. !y. (? x: P. y < x) = (y < S))";
   8.140 -by (res_inst_tac [("x","%#psup({w. %#w : P})")] exI 1);
   8.141 -by Auto_tac;
   8.142 -by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
   8.143 -by (case_tac "0r < ya" 1);
   8.144 -by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
   8.145 -by (dtac real_less_all_real2 2);
   8.146 -by Auto_tac;
   8.147 -by (rtac (preal_complete RS spec RS iffD1) 1);
   8.148 -by Auto_tac;
   8.149 -by (forward_tac [real_gt_preal_preal_Ex] 1);
   8.150 -by Auto_tac;
   8.151 -(* second part *)
   8.152 -by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
   8.153 -by (case_tac "0r < ya" 1);
   8.154 -by (auto_tac (claset() addSDs [real_less_all_real2,
   8.155 -        real_gt_zero_preal_Ex RS iffD1],simpset()));
   8.156 -by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac);
   8.157 -by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
   8.158 -by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
   8.159 -by (Blast_tac 3);
   8.160 -by (Blast_tac 1);
   8.161 -by (Blast_tac 1);
   8.162 -by (Blast_tac 1);
   8.163 -qed "posreal_complete";
   8.164 -
   8.165 -
   8.166 -
   8.167  (*** Monotonicity results ***)
   8.168  
   8.169  Goal "(v+z < w+z) = (v < (w::real))";
   8.170 @@ -227,8 +171,12 @@
   8.171  Goal "!!z z'::real. [| w'<w; z'<=z |] ==> w' + z' < w + z";
   8.172  by (etac (real_add_less_mono1 RS real_less_le_trans) 1);
   8.173  by (Simp_tac 1);
   8.174 -qed "real_add_less_mono";
   8.175 +qed "real_add_less_le_mono";
   8.176  
   8.177 +Goal "!!z z'::real. [| w'<=w; z'<z |] ==> w' + z' < w + z";
   8.178 +by (etac (real_add_le_mono1 RS real_le_less_trans) 1);
   8.179 +by (Simp_tac 1);
   8.180 +qed "real_add_le_less_mono";
   8.181  
   8.182  Goal "!!(A::real). A < B ==> C + A < C + B";
   8.183  by (Simp_tac 1);
   8.184 @@ -242,6 +190,14 @@
   8.185  by (Full_simp_tac 1);
   8.186  qed "real_less_add_left_cancel";
   8.187  
   8.188 +Goal "!!(A::real). A + C <= B + C ==> A <= B";
   8.189 +by (Full_simp_tac 1);
   8.190 +qed "real_le_add_right_cancel";
   8.191 +
   8.192 +Goal "!!(A::real). C + A <= C + B ==> A <= B";
   8.193 +by (Full_simp_tac 1);
   8.194 +qed "real_le_add_left_cancel";
   8.195 +
   8.196  Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
   8.197  by (etac real_less_trans 1);
   8.198  by (dtac real_add_less_mono2 1);
   8.199 @@ -277,80 +233,116 @@
   8.200  	  simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
   8.201  qed "real_less_Ex";
   8.202  
   8.203 +Goal "!!(u::real). 0r < r ==>  u + -r < u";
   8.204 +by (res_inst_tac [("C","r")] real_less_add_right_cancel 1);
   8.205 +by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
   8.206 +qed "real_add_minus_positive_less_self";
   8.207 +
   8.208 +Goal "((r::real) <= s) = (-s <= -r)";
   8.209 +by (Step_tac 1);
   8.210 +by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1);
   8.211 +by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2);
   8.212 +by (Auto_tac);
   8.213 +by (dres_inst_tac [("z","-r")] real_add_le_mono1 1);
   8.214 +by (dres_inst_tac [("z","s")] real_add_le_mono1 2);
   8.215 +by (auto_tac (claset(),simpset() addsimps [real_add_assoc]));
   8.216 +qed "real_le_minus_iff";
   8.217 +Addsimps [real_le_minus_iff RS sym];
   8.218 +          
   8.219 +Goal "0r <= 1r";
   8.220 +by (rtac (real_zero_less_one RS real_less_imp_le) 1);
   8.221 +qed "real_zero_le_one";
   8.222 +Addsimps [real_zero_le_one];
   8.223 +
   8.224 +Goal "0r <= x*x";
   8.225 +by (res_inst_tac [("R2.0","0r"),("R1.0","x")] real_linear_less2 1);
   8.226 +by (auto_tac (claset() addIs [real_mult_order,
   8.227 +    real_mult_less_zero1,real_less_imp_le],
   8.228 +    simpset()));
   8.229 +qed "real_le_square";
   8.230 +Addsimps [real_le_square];
   8.231 +
   8.232  (*---------------------------------------------------------------------------------
   8.233               An embedding of the naturals in the reals
   8.234   ---------------------------------------------------------------------------------*)
   8.235  
   8.236 -Goalw [real_nat_def] "%%#0 = 1r";
   8.237 -by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_preal_def]) 1);
   8.238 +Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r";
   8.239 +by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def]) 1);
   8.240  by (fold_tac [real_one_def]);
   8.241  by (rtac refl 1);
   8.242 -qed "real_nat_one";
   8.243 +qed "real_of_posnat_one";
   8.244  
   8.245 -Goalw [real_nat_def] "%%#1 = 1r + 1r";
   8.246 -by (full_simp_tac (simpset() addsimps [real_preal_def,real_one_def,
   8.247 -    pnat_two_eq,real_add,prat_pnat_add RS sym,preal_prat_add RS sym
   8.248 +Goalw [real_of_posnat_def] "real_of_posnat 1 = 1r + 1r";
   8.249 +by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
   8.250 +    pnat_two_eq,real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym
   8.251      ] @ pnat_add_ac) 1);
   8.252 -qed "real_nat_two";
   8.253 +qed "real_of_posnat_two";
   8.254  
   8.255 -Goalw [real_nat_def]
   8.256 -          "%%#n1 + %%#n2 = %%#(n1 + n2) + 1r";
   8.257 -by (full_simp_tac (simpset() addsimps [real_nat_one RS sym,
   8.258 -    real_nat_def,real_preal_add RS sym,preal_prat_add RS sym,
   8.259 -    prat_pnat_add RS sym,pnat_nat_add]) 1);
   8.260 -qed "real_nat_add";
   8.261 +Goalw [real_of_posnat_def]
   8.262 +          "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
   8.263 +by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym,
   8.264 +    real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym,
   8.265 +    prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
   8.266 +qed "real_of_posnat_add";
   8.267  
   8.268 -Goal "%%#(n + 1) = %%#n + 1r";
   8.269 +Goal "real_of_posnat (n + 1) = real_of_posnat n + 1r";
   8.270  by (res_inst_tac [("x1","1r")] (real_add_right_cancel RS iffD1) 1);
   8.271 -by (rtac (real_nat_add RS subst) 1);
   8.272 -by (full_simp_tac (simpset() addsimps [real_nat_two,real_add_assoc]) 1);
   8.273 -qed "real_nat_add_one";
   8.274 +by (rtac (real_of_posnat_add RS subst) 1);
   8.275 +by (full_simp_tac (simpset() addsimps [real_of_posnat_two,real_add_assoc]) 1);
   8.276 +qed "real_of_posnat_add_one";
   8.277  
   8.278  Goal "Suc n = n + 1";
   8.279  by Auto_tac;
   8.280 -qed "lemma";
   8.281 +qed "lemmaS";
   8.282  
   8.283 -Goal "%%#Suc n = %%#n + 1r";
   8.284 -by (stac lemma 1);
   8.285 -by (rtac real_nat_add_one 1);
   8.286 -qed "real_nat_Suc";
   8.287 +Goal "real_of_posnat (Suc n) = real_of_posnat n + 1r";
   8.288 +by (stac lemmaS 1);
   8.289 +by (rtac real_of_posnat_add_one 1);
   8.290 +qed "real_of_posnat_Suc";
   8.291  
   8.292 -Goal "inj(real_nat)";
   8.293 +Goal "inj(real_of_posnat)";
   8.294  by (rtac injI 1);
   8.295 -by (rewtac real_nat_def);
   8.296 -by (dtac (inj_real_preal RS injD) 1);
   8.297 -by (dtac (inj_preal_prat RS injD) 1);
   8.298 -by (dtac (inj_prat_pnat RS injD) 1);
   8.299 -by (etac (inj_pnat_nat RS injD) 1);
   8.300 -qed "inj_real_nat";
   8.301 +by (rewtac real_of_posnat_def);
   8.302 +by (dtac (inj_real_of_preal RS injD) 1);
   8.303 +by (dtac (inj_preal_of_prat RS injD) 1);
   8.304 +by (dtac (inj_prat_of_pnat RS injD) 1);
   8.305 +by (etac (inj_pnat_of_nat RS injD) 1);
   8.306 +qed "inj_real_of_posnat";
   8.307  
   8.308 -Goalw [real_nat_def] "0r < %%#n";
   8.309 +Goalw [real_of_posnat_def] "0r < real_of_posnat n";
   8.310  by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
   8.311  by (Blast_tac 1);
   8.312 -qed "real_nat_less_zero";
   8.313 +qed "real_of_posnat_less_zero";
   8.314  
   8.315 -Goal "1r <= %%#n";
   8.316 -by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
   8.317 +Goal "real_of_posnat n ~= 0r";
   8.318 +by (rtac (real_of_posnat_less_zero RS real_not_refl2 RS not_sym) 1);
   8.319 +qed "real_of_posnat_not_eq_zero";
   8.320 +Addsimps[real_of_posnat_not_eq_zero];
   8.321 +
   8.322 +Goal "1r <= real_of_posnat n";
   8.323 +by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1);
   8.324  by (induct_tac "n" 1);
   8.325  by (auto_tac (claset(),
   8.326 -	      simpset () addsimps [real_nat_Suc,real_nat_one,
   8.327 -				   real_nat_less_zero, real_less_imp_le]));
   8.328 -qed "real_nat_less_one";
   8.329 -
   8.330 -Goal "rinv(%%#n) ~= 0r";
   8.331 -by (rtac ((real_nat_less_zero RS 
   8.332 -    real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
   8.333 -qed "real_nat_rinv_not_zero";
   8.334 +	      simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
   8.335 +				   real_of_posnat_less_zero, real_less_imp_le]));
   8.336 +qed "real_of_posnat_less_one";
   8.337 +Addsimps [real_of_posnat_less_one];
   8.338  
   8.339 -Goal "rinv(%%#x) = rinv(%%#y) ==> x = y";
   8.340 -by (rtac (inj_real_nat RS injD) 1);
   8.341 +Goal "rinv(real_of_posnat n) ~= 0r";
   8.342 +by (rtac ((real_of_posnat_less_zero RS 
   8.343 +    real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
   8.344 +qed "real_of_posnat_rinv_not_zero";
   8.345 +Addsimps [real_of_posnat_rinv_not_zero];
   8.346 +
   8.347 +Goal "rinv(real_of_posnat x) = rinv(real_of_posnat y) ==> x = y";
   8.348 +by (rtac (inj_real_of_posnat RS injD) 1);
   8.349  by (res_inst_tac [("n2","x")] 
   8.350 -    (real_nat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1);
   8.351 -by (full_simp_tac (simpset() addsimps [(real_nat_less_zero RS 
   8.352 +    (real_of_posnat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1);
   8.353 +by (full_simp_tac (simpset() addsimps [(real_of_posnat_less_zero RS 
   8.354      real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1);
   8.355 -by (asm_full_simp_tac (simpset() addsimps [(real_nat_less_zero RS 
   8.356 +by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_less_zero RS 
   8.357      real_not_refl2 RS not_sym)]) 1);
   8.358 -qed "real_nat_rinv_inj";
   8.359 +qed "real_of_posnat_rinv_inj";
   8.360  
   8.361  Goal "0r < x ==> 0r < rinv x";
   8.362  by (EVERY1[rtac ccontr, dtac real_leI]);
   8.363 @@ -372,8 +364,14 @@
   8.364      simpset()));
   8.365  qed "real_rinv_less_zero";
   8.366  
   8.367 +Goal "0r < rinv(real_of_posnat n)";
   8.368 +by (rtac (real_of_posnat_less_zero RS real_rinv_gt_zero) 1);
   8.369 +qed "real_of_posnat_rinv_gt_zero";
   8.370 +Addsimps [real_of_posnat_rinv_gt_zero];
   8.371 +
   8.372  Goal "x+x=x*(1r+1r)";
   8.373 -by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
   8.374 +by (simp_tac (simpset() addsimps 
   8.375 +              [real_add_mult_distrib2]) 1);
   8.376  qed "real_add_self";
   8.377  
   8.378  Goal "x < x + 1r";
   8.379 @@ -454,6 +452,90 @@
   8.380  by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
   8.381  qed "real_mult_le_le_mono1";
   8.382  
   8.383 +Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r < x; x < y|] \
   8.384 +\                  ==> r1 * x < r2 * y";
   8.385 +by (dres_inst_tac [("x","x")] real_mult_less_mono2 1);
   8.386 +by (dres_inst_tac [("R1.0","0r")] real_less_trans 2);
   8.387 +by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
   8.388 +by (Auto_tac);
   8.389 +by (blast_tac (claset() addIs [real_less_trans]) 1);
   8.390 +qed "real_mult_less_mono";
   8.391 +
   8.392 +Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r < y|] \
   8.393 +\                           ==> 0r < r2 * y";
   8.394 +by (dres_inst_tac [("R1.0","0r")] real_less_trans 1);
   8.395 +by (assume_tac 1);
   8.396 +by (blast_tac (claset() addIs [real_mult_order]) 1);
   8.397 +qed "real_mult_order_trans";
   8.398 +
   8.399 +Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r <= x; x < y|] \
   8.400 +\                  ==> r1 * x < r2 * y";
   8.401 +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs
   8.402 +              [real_mult_less_mono,real_mult_order_trans],
   8.403 +              simpset()));
   8.404 +qed "real_mult_less_mono3";
   8.405 +
   8.406 +Goal "!!(x::real). [| 0r <= r1; r1 <r2; 0r <= x; x < y|] \
   8.407 +\                  ==> r1 * x < r2 * y";
   8.408 +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs
   8.409 +              [real_mult_less_mono,real_mult_order_trans,
   8.410 +               real_mult_order],simpset()));
   8.411 +by (dres_inst_tac [("R2.0","x")] real_less_trans 1);
   8.412 +by (assume_tac 1);
   8.413 +by (blast_tac (claset() addIs [real_mult_order]) 1);
   8.414 +qed "real_mult_less_mono4";
   8.415 +
   8.416 +Goal "!!(x::real). [| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \
   8.417 +\                  ==> r1 * x <= r2 * y";
   8.418 +by (rtac real_less_or_eq_imp_le 1);
   8.419 +by (REPEAT(dtac real_le_imp_less_or_eq 1));
   8.420 +by (auto_tac (claset() addIs [real_mult_less_mono,
   8.421 +    real_mult_order_trans,real_mult_order],simpset()));
   8.422 +qed "real_mult_le_mono";
   8.423 +
   8.424 +Goal "!!(x::real). [| 0r < r1; r1 < r2; 0r <= x; x <= y |] \
   8.425 +\                  ==> r1 * x <= r2 * y";
   8.426 +by (rtac real_less_or_eq_imp_le 1);
   8.427 +by (REPEAT(dtac real_le_imp_less_or_eq 1));
   8.428 +by (auto_tac (claset() addIs [real_mult_less_mono,
   8.429 +    real_mult_order_trans,real_mult_order],simpset()));
   8.430 +qed "real_mult_le_mono2";
   8.431 +
   8.432 +Goal "!!(x::real). [| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \
   8.433 +\                  ==> r1 * x <= r2 * y";
   8.434 +by (dtac real_le_imp_less_or_eq 1);
   8.435 +by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
   8.436 +by (dtac real_le_trans 1 THEN assume_tac 1);
   8.437 +by (auto_tac (claset() addIs [real_less_le_mult_order],simpset()));
   8.438 +qed "real_mult_le_mono3";
   8.439 +
   8.440 +Goal "!!(x::real). [| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \
   8.441 +\                  ==> r1 * x <= r2 * y";
   8.442 +by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1);
   8.443 +by (auto_tac (claset() addIs [real_mult_le_mono3,
   8.444 +    real_mult_le_le_mono1],simpset()));
   8.445 +qed "real_mult_le_mono4";
   8.446 +
   8.447 +Goal "!!x. 1r <= x ==> 0r < x";
   8.448 +by (rtac ccontr 1 THEN dtac real_leI 1);
   8.449 +by (dtac real_le_trans 1 THEN assume_tac 1);
   8.450 +by (auto_tac (claset() addDs [real_zero_less_one 
   8.451 +    RSN (2,real_le_less_trans)],simpset() addsimps 
   8.452 +    [real_less_not_refl]));
   8.453 +qed "real_gt_zero";
   8.454 +
   8.455 +Goal "!!r. [| 1r < r; 1r <= x |]  ==> x <= r * x";
   8.456 +by (dtac (real_gt_zero RS real_less_imp_le) 1);
   8.457 +by (auto_tac (claset() addSDs [real_mult_le_less_mono1],
   8.458 +    simpset()));
   8.459 +qed "real_mult_self_le";
   8.460 +
   8.461 +Goal "!!r. [| 1r <= r; 1r <= x |]  ==> x <= r * x";
   8.462 +by (dtac real_le_imp_less_or_eq 1);
   8.463 +by (auto_tac (claset() addIs [real_mult_self_le],
   8.464 +    simpset() addsimps [real_le_refl]));
   8.465 +qed "real_mult_self_le2";
   8.466 +
   8.467  Goal "!!(x::real). x < y ==> x < (x + y)*rinv(1r + 1r)";
   8.468  by (dres_inst_tac [("C","x")] real_add_less_mono2 1);
   8.469  by (dtac (real_add_self RS subst) 1);
   8.470 @@ -471,57 +553,276 @@
   8.471  qed "real_gt_half_sum";
   8.472  
   8.473  Goal "!!(x::real). x < y ==> EX r. x < r & r < y";
   8.474 -by (blast_tac (claset() addSIs [real_less_half_sum,real_gt_half_sum]) 1);
   8.475 +by (blast_tac (claset() addSIs [real_less_half_sum,
   8.476 +    real_gt_half_sum]) 1);
   8.477  qed "real_dense";
   8.478  
   8.479 -Goal "(EX n. rinv(%%#n) < r) = (EX n. 1r < r * %%#n)";
   8.480 +Goal "(EX n. rinv(real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
   8.481  by (Step_tac 1);
   8.482 -by (dres_inst_tac [("n1","n")] (real_nat_less_zero 
   8.483 +by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero 
   8.484                         RS real_mult_less_mono1) 1);
   8.485 -by (dres_inst_tac [("n2","n")] (real_nat_less_zero RS 
   8.486 +by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS 
   8.487          real_rinv_gt_zero RS real_mult_less_mono1) 2);
   8.488  by (auto_tac (claset(),
   8.489 -	      simpset() addsimps [(real_nat_less_zero RS 
   8.490 +	      simpset() addsimps [(real_of_posnat_less_zero RS 
   8.491      real_not_refl2 RS not_sym),real_mult_assoc]));
   8.492 -qed "real_nat_rinv_Ex_iff";
   8.493 +qed "real_of_posnat_rinv_Ex_iff";
   8.494 +
   8.495 +Goal "(rinv(real_of_posnat n) < r) = (1r < r * real_of_posnat n)";
   8.496 +by (Step_tac 1);
   8.497 +by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero 
   8.498 +                       RS real_mult_less_mono1) 1);
   8.499 +by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS 
   8.500 +        real_rinv_gt_zero RS real_mult_less_mono1) 2);
   8.501 +by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]));
   8.502 +qed "real_of_posnat_rinv_iff";
   8.503  
   8.504 -Goalw [real_nat_def] "(%%#n < %%#m) = (n < m)";
   8.505 +Goal "(rinv(real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)";
   8.506 +by (Step_tac 1);
   8.507 +by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS 
   8.508 +    real_less_imp_le RS real_mult_le_le_mono1) 1);
   8.509 +by (dres_inst_tac [("n3","n")] (real_of_posnat_less_zero RS 
   8.510 +        real_rinv_gt_zero RS real_less_imp_le RS 
   8.511 +        real_mult_le_le_mono1) 2);
   8.512 +by (auto_tac (claset(),simpset() addsimps real_mult_ac));
   8.513 +qed "real_of_posnat_rinv_le_iff";
   8.514 +
   8.515 +Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)";
   8.516  by Auto_tac;
   8.517 -qed "real_nat_less_iff";
   8.518 +qed "real_of_posnat_less_iff";
   8.519  
   8.520 -Addsimps [real_nat_less_iff];
   8.521 +Addsimps [real_of_posnat_less_iff];
   8.522  
   8.523 -Goal "0r < u  ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
   8.524 +Goal "0r < u  ==> (u < rinv (real_of_posnat n)) = (real_of_posnat n < rinv(u))";
   8.525  by (Step_tac 1);
   8.526 -by (res_inst_tac [("n2","n")] (real_nat_less_zero RS 
   8.527 +by (res_inst_tac [("n2","n")] (real_of_posnat_less_zero RS 
   8.528      real_rinv_gt_zero RS real_mult_less_cancel1) 1);
   8.529  by (res_inst_tac [("x1","u")] ( real_rinv_gt_zero
   8.530     RS real_mult_less_cancel1) 2);
   8.531  by (auto_tac (claset(),
   8.532 -	      simpset() addsimps [real_nat_less_zero, 
   8.533 +	      simpset() addsimps [real_of_posnat_less_zero, 
   8.534      real_not_refl2 RS not_sym]));
   8.535  by (res_inst_tac [("z","u")] real_mult_less_cancel2 1);
   8.536 -by (res_inst_tac [("n1","n")] (real_nat_less_zero RS 
   8.537 +by (res_inst_tac [("n1","n")] (real_of_posnat_less_zero RS 
   8.538      real_mult_less_cancel2) 3);
   8.539  by (auto_tac (claset(),
   8.540 -	      simpset() addsimps [real_nat_less_zero, 
   8.541 +	      simpset() addsimps [real_of_posnat_less_zero, 
   8.542      real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
   8.543 -qed "real_nat_less_rinv_iff";
   8.544 +qed "real_of_posnat_less_rinv_iff";
   8.545  
   8.546 -Goal "0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
   8.547 +Goal "0r < u ==> (u = rinv(real_of_posnat n)) = (real_of_posnat n = rinv u)";
   8.548  by (auto_tac (claset(),
   8.549  	      simpset() addsimps [real_rinv_rinv,
   8.550 -    real_nat_less_zero,real_not_refl2 RS not_sym]));
   8.551 -qed "real_nat_rinv_eq_iff";
   8.552 +    real_of_posnat_less_zero,real_not_refl2 RS not_sym]));
   8.553 +qed "real_of_posnat_rinv_eq_iff";
   8.554 +
   8.555 +Goal "!!x. [| 0r < r; r < x |] ==> rinv x < rinv r";
   8.556 +by (forward_tac [real_less_trans] 1 THEN assume_tac 1);
   8.557 +by (forward_tac [real_rinv_gt_zero] 1);
   8.558 +by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1);
   8.559 +by (forw_inst_tac [("x","r"),("z","rinv r")] real_mult_less_mono1 1);
   8.560 +by (assume_tac 1);
   8.561 +by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS 
   8.562 +         not_sym RS real_mult_inv_right]) 1);
   8.563 +by (forward_tac [real_rinv_gt_zero] 1);
   8.564 +by (forw_inst_tac [("x","1r"),("z","rinv x")] real_mult_less_mono2 1);
   8.565 +by (assume_tac 1);
   8.566 +by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS 
   8.567 +         not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
   8.568 +qed "real_rinv_less_swap";
   8.569 +
   8.570 +Goal "!!x. [| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)";
   8.571 +by (auto_tac (claset() addIs [real_rinv_less_swap],simpset()));
   8.572 +by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
   8.573 +by (etac (real_not_refl2 RS not_sym) 1);
   8.574 +by (res_inst_tac [("t","x")] (real_rinv_rinv RS subst) 1);
   8.575 +by (etac (real_not_refl2 RS not_sym) 1);
   8.576 +by (auto_tac (claset() addIs [real_rinv_less_swap],
   8.577 +    simpset() addsimps [real_rinv_gt_zero]));
   8.578 +qed "real_rinv_less_iff";
   8.579 +
   8.580 +Goal "r < r + rinv(real_of_posnat n)";
   8.581 +by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
   8.582 +by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   8.583 +qed "real_add_rinv_real_of_posnat_less";
   8.584 +Addsimps [real_add_rinv_real_of_posnat_less];
   8.585 +
   8.586 +Goal "r <= r + rinv(real_of_posnat n)";
   8.587 +by (rtac real_less_imp_le 1);
   8.588 +by (Simp_tac 1);
   8.589 +qed "real_add_rinv_real_of_posnat_le";
   8.590 +Addsimps [real_add_rinv_real_of_posnat_le];
   8.591 +
   8.592 +Goal "r + -rinv(real_of_posnat n) < r";
   8.593 +by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
   8.594 +by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
   8.595 +    real_minus_zero_less_iff2]) 1);
   8.596 +qed "real_add_minus_rinv_real_of_posnat_less";
   8.597 +Addsimps [real_add_minus_rinv_real_of_posnat_less];
   8.598 +
   8.599 +Goal "r + -rinv(real_of_posnat n) <= r";
   8.600 +by (rtac real_less_imp_le 1);
   8.601 +by (Simp_tac 1);
   8.602 +qed "real_add_minus_rinv_real_of_posnat_le";
   8.603 +Addsimps [real_add_minus_rinv_real_of_posnat_le];
   8.604 +
   8.605 +Goal "!!r. 0r < r ==> r*(1r + -rinv(real_of_posnat n)) < r";
   8.606 +by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
   8.607 +by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
   8.608 +by (auto_tac (claset() addIs [real_mult_order],simpset() 
   8.609 +    addsimps [real_add_assoc RS sym,real_minus_mult_eq2 RS sym,
   8.610 +    real_minus_zero_less_iff2]));
   8.611 +qed "real_mult_less_self";
   8.612 +
   8.613 +Goal "0r <= 1r + -rinv(real_of_posnat n)";
   8.614 +by (res_inst_tac [("C","rinv(real_of_posnat n)")] real_le_add_right_cancel 1);
   8.615 +by (simp_tac (simpset() addsimps [real_add_assoc,
   8.616 +    real_of_posnat_rinv_le_iff]) 1);
   8.617 +qed "real_add_one_minus_rinv_ge_zero";
   8.618 +
   8.619 +Goal "!!r. 0r < r ==> 0r <= r*(1r + -rinv(real_of_posnat n))";
   8.620 +by (dtac (real_add_one_minus_rinv_ge_zero RS 
   8.621 +          real_mult_le_less_mono1) 1);
   8.622 +by (Auto_tac);
   8.623 +qed "real_mult_add_one_minus_ge_zero";
   8.624 +
   8.625 +Goal "!!x. x*y = 0r ==> x = 0r | y = 0r";
   8.626 +by (auto_tac (claset() addIs [ccontr] addDs 
   8.627 +    [real_mult_not_zero],simpset()));
   8.628 +qed "real_mult_zero_disj";
   8.629 + 
   8.630 +Goal "x + x*y = x*(1r + y)";
   8.631 +by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
   8.632 +qed "real_add_mult_distrib_one";
   8.633 +
   8.634 +Goal "!!x. [| x ~= 1r; y * x = y |] ==> y = 0r";
   8.635 +by (dtac (sym RS (real_eq_minus_iff RS iffD1)) 1);
   8.636 +by (dtac sym 1);
   8.637 +by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2,
   8.638 +    real_add_mult_distrib_one]) 1);
   8.639 +by (dtac real_mult_zero_disj 1);
   8.640 +by (auto_tac (claset(),simpset() 
   8.641 +   addsimps [real_eq_minus_iff2 RS sym]));
   8.642 +qed "real_mult_eq_self_zero";
   8.643 +Addsimps [real_mult_eq_self_zero];
   8.644 +
   8.645 +Goal "!!x. [| x ~= 1r; y = y * x |] ==> y = 0r";
   8.646 +by (dtac sym 1);
   8.647 +by (Asm_full_simp_tac 1);
   8.648 +qed "real_mult_eq_self_zero2";
   8.649 +Addsimps [real_mult_eq_self_zero2];
   8.650  
   8.651 -(*
   8.652 -(*------------------------------------------------------------------
   8.653 -     lemmas about upper bounds and least upper bound
   8.654 - ------------------------------------------------------------------*)
   8.655 -Goalw [real_ub_def] "[| real_ub u S; x : S |] ==> x <= u";
   8.656 -by Auto_tac;
   8.657 -qed "real_ubD";
   8.658 +Goal "!!x. [| 0r <= x*y; 0r < x |] ==> 0r <= y";
   8.659 +by (forward_tac [real_rinv_gt_zero] 1);
   8.660 +by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1);
   8.661 +by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
   8.662 +by (auto_tac (claset(),simpset() addsimps 
   8.663 +    [real_mult_assoc RS sym]));
   8.664 +qed "real_mult_ge_zero_cancel";
   8.665 +
   8.666 +Goal "!!x. [|x ~= 0r; y ~= 0r |] ==> \
   8.667 +\          rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
   8.668 +by (asm_full_simp_tac (simpset() addsimps 
   8.669 +    [real_rinv_distrib,real_add_mult_distrib,
   8.670 +     real_mult_assoc RS sym]) 1);
   8.671 +by (rtac (real_mult_assoc RS ssubst) 1);
   8.672 +by (rtac (real_mult_left_commute RS subst) 1);
   8.673 +by (asm_full_simp_tac (simpset() addsimps 
   8.674 +    [real_add_commute]) 1);
   8.675 +qed "real_rinv_add";
   8.676 +
   8.677 +(*---------------------------------------------------------------------------------
   8.678 +     Another embedding of the naturals in the reals (see real_of_posnat)
   8.679 + ---------------------------------------------------------------------------------*)
   8.680 +Goalw [real_of_nat_def] "real_of_nat 0 = 0r";
   8.681 +by (full_simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
   8.682 +qed "real_of_nat_zero";
   8.683 +
   8.684 +Goalw [real_of_nat_def] "real_of_nat 1 = 1r";
   8.685 +by (full_simp_tac (simpset() addsimps [real_of_posnat_two,
   8.686 +    real_add_assoc]) 1);
   8.687 +qed "real_of_nat_one";
   8.688 +
   8.689 +Goalw [real_of_nat_def]
   8.690 +          "real_of_nat n1 + real_of_nat n2 = real_of_nat (n1 + n2)";
   8.691 +by (simp_tac (simpset() addsimps 
   8.692 +    [real_of_posnat_add,real_add_assoc RS sym]) 1);
   8.693 +qed "real_of_nat_add";
   8.694 +
   8.695 +Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r";
   8.696 +by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
   8.697 +qed "real_of_nat_Suc";
   8.698 +    
   8.699 +Goalw [real_of_nat_def] "(n < m) = (real_of_nat n < real_of_nat m)";
   8.700 +by (Auto_tac);
   8.701 +qed "real_of_nat_less_iff";
   8.702 +
   8.703 +Addsimps [real_of_nat_less_iff RS sym];
   8.704 +
   8.705 +Goal "inj real_of_nat";
   8.706 +by (rtac injI 1);
   8.707 +by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD],
   8.708 +    simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
   8.709 +qed "inj_real_of_nat";
   8.710  
   8.711 -*)
   8.712 +Goalw [real_of_nat_def] "0r <= real_of_nat n";
   8.713 +by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1);
   8.714 +by (asm_full_simp_tac (simpset() addsimps 
   8.715 +        [real_add_assoc]) 1);
   8.716 +qed "real_of_nat_ge_zero";
   8.717 +Addsimps [real_of_nat_ge_zero];
   8.718 +
   8.719 +Goal "real_of_nat n1 * real_of_nat n2 = real_of_nat (n1 * n2)";
   8.720 +by (induct_tac "n1" 1);
   8.721 +by (dtac sym 2);
   8.722 +by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero,
   8.723 +    real_of_nat_add RS sym,real_of_nat_Suc,real_add_mult_distrib,
   8.724 +    real_add_commute]));
   8.725 +qed "real_of_nat_mult";
   8.726 +
   8.727 +Goal "(real_of_nat n = real_of_nat m) = (n = m)";
   8.728 +by (auto_tac (claset() addDs [inj_real_of_nat RS injD],
   8.729 +              simpset()));
   8.730 +qed "real_of_nat_eq_cancel";
   8.731 +
   8.732 +(*------- lemmas -------*)
   8.733 +goal NatDef.thy "!!m. [| m < Suc n; n <= m |] ==> m = n";
   8.734 +by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
   8.735 +    simpset() addsimps [less_Suc_eq]));
   8.736 +qed "lemma_nat_not_dense";
   8.737 +
   8.738 +goal NatDef.thy "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
   8.739 +by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
   8.740 +    simpset() addsimps [le_Suc_eq]));
   8.741 +qed "lemma_nat_not_dense2";
   8.742 +
   8.743 +goal NatDef.thy "!!m. m < Suc n ==> ~ Suc n <= m";
   8.744 +by (blast_tac (claset() addDs 
   8.745 +     [less_le_trans] addIs [less_asym]) 1);
   8.746 +qed "lemma_not_leI";
   8.747 +
   8.748 +goalw NatDef.thy [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
   8.749 +by (Auto_tac);
   8.750 +qed "lemma_not_leI2";
   8.751 +
   8.752 +(*------- lemmas -------*)
   8.753 +val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
   8.754 +by (rtac (prem RS rev_mp) 1);
   8.755 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   8.756 +by (ALLGOALS Asm_simp_tac);
   8.757 +qed "Suc_diff_n";
   8.758 +
   8.759 +(* Goalw  [real_of_nat_def] 
   8.760 +   "real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";*)
   8.761 +
   8.762 +Goal "n2 < n1 --> real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";
   8.763 +by (induct_tac "n1" 1);
   8.764 +by (Step_tac 1 THEN dtac leI 1 THEN dtac sym 2);
   8.765 +by (dtac lemma_nat_not_dense 1);
   8.766 +by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
   8.767 +              real_of_nat_zero] @ real_add_ac));
   8.768 +by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
   8.769 +             real_of_nat_add,Suc_diff_n]) 1);
   8.770 +qed "real_of_nat_minus";
   8.771  
   8.772  
     9.1 --- a/src/HOL/Real/Real.thy	Fri Jul 23 17:28:18 1999 +0200
     9.2 +++ b/src/HOL/Real/Real.thy	Fri Jul 23 17:29:12 1999 +0200
     9.3 @@ -1,9 +1,8 @@
     9.4 -(*  Title:      Real/Real.thy
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1998  University of Cambridge
     9.8 -
     9.9 -Type "real" is a linear order
    9.10 +(*  Title:       Real/Real.thy
    9.11 +    Author:      Lawrence C. Paulson
    9.12 +                 Jacques D. Fleuriot
    9.13 +    Copyright:   1998  University of Cambridge
    9.14 +    Description: Type "real" is a linear order
    9.15  *)
    9.16  
    9.17  Real = RealDef +
    10.1 --- a/src/HOL/Real/RealAbs.ML	Fri Jul 23 17:28:18 1999 +0200
    10.2 +++ b/src/HOL/Real/RealAbs.ML	Fri Jul 23 17:29:12 1999 +0200
    10.3 @@ -122,6 +122,12 @@
    10.4     simpset() addsimps [real_ge_zero_iff]));
    10.5  qed "rabs_minus_cancel";
    10.6  
    10.7 +Goal "rabs(x + -y) = rabs (y + -x)";
    10.8 +by (rtac (rabs_minus_cancel RS subst) 1);
    10.9 +by (simp_tac (simpset() addsimps 
   10.10 +    [real_add_commute]) 1);
   10.11 +qed "rabs_minus_add_cancel";
   10.12 +
   10.13  Goal "rabs(x + -y) <= rabs x + rabs y";
   10.14  by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1);
   10.15  by (rtac rabs_triangle_ineq 1);
   10.16 @@ -134,6 +140,13 @@
   10.17  by (rtac rabs_triangle_ineq 1);
   10.18  qed "rabs_sum_triangle_ineq";
   10.19  
   10.20 +Goal "rabs(x) <= rabs(x + -y) + rabs(y)";
   10.21 +by (res_inst_tac [("j","rabs(x + -y + y)")] real_le_trans 1);
   10.22 +by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
   10.23 +by (simp_tac (simpset() addsimps [real_add_assoc RS sym,
   10.24 +              rabs_triangle_ineq]) 1);
   10.25 +qed "rabs_triangle_ineq_minus_cancel";
   10.26 +
   10.27  Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s";
   10.28  by (rtac real_le_less_trans 1);
   10.29  by (rtac rabs_triangle_ineq 1);
   10.30 @@ -235,3 +248,67 @@
   10.31  by (assume_tac 3 THEN Auto_tac);
   10.32  qed "rabs_interval_iff";
   10.33  
   10.34 +Goal "(rabs x < r) = (-x < r & x < r)";
   10.35 +by (auto_tac (claset(),simpset() addsimps [rabs_interval_iff]));
   10.36 +by (dtac (real_less_swap_iff RS iffD1) 1);
   10.37 +by (dtac (real_less_swap_iff RS iffD1) 2);
   10.38 +by (Auto_tac);
   10.39 +qed "rabs_interval_iff2";
   10.40 +
   10.41 +Goal "!!x. rabs x <= r ==> -r<=x & x<=r";
   10.42 +by (dtac real_le_imp_less_or_eq 1);
   10.43 +by (auto_tac (claset() addSDs [real_less_imp_le],
   10.44 +    simpset() addsimps [rabs_interval_iff,rabs_ge_self]));
   10.45 +by (auto_tac (claset(),simpset() addsimps [real_le_def]));
   10.46 +by (dtac (real_less_swap_iff RS iffD1) 1);
   10.47 +by (auto_tac (claset() addSDs [rabs_ge_minus_self 
   10.48 +    RS real_le_less_trans],simpset() addsimps [real_less_not_refl]));
   10.49 +qed "rabs_leD";
   10.50 +
   10.51 +Goal "!!x. [| -r<x; x<=r |] ==> rabs x <= r";
   10.52 +by (dtac real_le_imp_less_or_eq 1);
   10.53 +by (Step_tac 1);
   10.54 +by (blast_tac (claset() addIs 
   10.55 +    [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
   10.56 +by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps 
   10.57 +    [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl]));
   10.58 +qed "rabs_leI1";
   10.59 +
   10.60 +Goal "!!x. [| -r<=x; x<=r |] ==> rabs x <= r";
   10.61 +by (REPEAT(dtac real_le_imp_less_or_eq 1));
   10.62 +by (Step_tac 1);
   10.63 +by (blast_tac (claset() addIs 
   10.64 +    [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
   10.65 +by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps 
   10.66 +    [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl,
   10.67 +    rabs_minus_cancel]));
   10.68 +by (cut_inst_tac [("x","r")] rabs_disj 1);
   10.69 +by (rotate_tac 1 1);
   10.70 +by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
   10.71 +qed "rabs_leI";
   10.72 +
   10.73 +Goal "(rabs x <= r) = (-r<=x & x<=r)";
   10.74 +by (blast_tac (claset() addSIs [rabs_leD,rabs_leI]) 1);
   10.75 +qed "rabs_le_interval_iff";
   10.76 +
   10.77 +Goal 
   10.78 +     "(rabs (x + -y) < r) = (y + -r < x & x < y + r)";
   10.79 +by (auto_tac (claset(),simpset() addsimps 
   10.80 +     [rabs_interval_iff]));
   10.81 +by (ALLGOALS(dtac real_less_sum_gt_zero));
   10.82 +by (ALLGOALS(dtac real_less_sum_gt_zero));
   10.83 +by (ALLGOALS(rtac real_sum_gt_zero_less));
   10.84 +by (auto_tac (claset(),simpset() addsimps 
   10.85 +    [real_minus_add_distrib] addsimps real_add_ac));
   10.86 +qed "rabs_add_minus_interval_iff";
   10.87 +
   10.88 +Goal "!!k. 0r < k ==> 0r < k + rabs(x)";
   10.89 +by (res_inst_tac [("t","0r")] (real_add_zero_right RS subst) 1);
   10.90 +by (etac (rabs_ge_zero RSN (2,real_add_less_le_mono)) 1);
   10.91 +qed "rabs_add_pos_gt_zero";
   10.92 +
   10.93 +Goal "0r < 1r + rabs(x)";
   10.94 +by (rtac (real_zero_less_one RS rabs_add_pos_gt_zero) 1);
   10.95 +qed "rabs_add_one_gt_zero";
   10.96 +Addsimps [rabs_add_one_gt_zero];
   10.97 +
    11.1 --- a/src/HOL/Real/RealDef.ML	Fri Jul 23 17:28:18 1999 +0200
    11.2 +++ b/src/HOL/Real/RealDef.ML	Fri Jul 23 17:29:12 1999 +0200
    11.3 @@ -80,10 +80,10 @@
    11.4  by (rtac Rep_real_inverse 1);
    11.5  qed "inj_Rep_real";
    11.6  
    11.7 -(** real_preal: the injection from preal to real **)
    11.8 -Goal "inj(real_preal)";
    11.9 +(** real_of_preal: the injection from preal to real **)
   11.10 +Goal "inj(real_of_preal)";
   11.11  by (rtac injI 1);
   11.12 -by (rewtac real_preal_def);
   11.13 +by (rewtac real_of_preal_def);
   11.14  by (dtac (inj_on_Abs_real RS inj_onD) 1);
   11.15  by (REPEAT (rtac realrel_in_real 1));
   11.16  by (dtac eq_equiv_class 1);
   11.17 @@ -91,7 +91,7 @@
   11.18  by (Blast_tac 1);
   11.19  by Safe_tac;
   11.20  by (Asm_full_simp_tac 1);
   11.21 -qed "inj_real_preal";
   11.22 +qed "inj_real_of_preal";
   11.23  
   11.24  val [prem] = goal thy
   11.25      "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
   11.26 @@ -195,7 +195,7 @@
   11.27  (* real addition is an AC operator *)
   11.28  val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute];
   11.29  
   11.30 -Goalw [real_preal_def,real_zero_def] "0r + z = z";
   11.31 +Goalw [real_of_preal_def,real_zero_def] "0r + z = z";
   11.32  by (res_inst_tac [("z","z")] eq_Abs_real 1);
   11.33  by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
   11.34  qed "real_add_zero_left";
   11.35 @@ -253,6 +253,12 @@
   11.36  by (Blast_tac 1);
   11.37  qed "real_add_minus_eq_minus";
   11.38  
   11.39 +Goal "? (y::real). x = -y";
   11.40 +by (cut_inst_tac [("x","x")] real_minus_ex 1);
   11.41 +by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
   11.42 +by (Fast_tac 1);
   11.43 +qed "real_as_add_inverse_ex";
   11.44 +
   11.45  Goal "-(x + y) = -x + -(y::real)";
   11.46  by (res_inst_tac [("z","x")] eq_Abs_real 1);
   11.47  by (res_inst_tac [("z","y")] eq_Abs_real 1);
   11.48 @@ -271,6 +277,20 @@
   11.49  by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
   11.50  qed "real_add_right_cancel";
   11.51  
   11.52 +Goal "((x::real) = y) = (0r = x + - y)";
   11.53 +by (Step_tac 1);
   11.54 +by (res_inst_tac [("x1","-y")] 
   11.55 +      (real_add_right_cancel RS iffD1) 2);
   11.56 +by (Auto_tac);
   11.57 +qed "real_eq_minus_iff"; 
   11.58 +
   11.59 +Goal "((x::real) = y) = (x + - y = 0r)";
   11.60 +by (Step_tac 1);
   11.61 +by (res_inst_tac [("x1","-y")] 
   11.62 +      (real_add_right_cancel RS iffD1) 2);
   11.63 +by (Auto_tac);
   11.64 +qed "real_eq_minus_iff2"; 
   11.65 +
   11.66  Goal "0r - x = -x";
   11.67  by (simp_tac (simpset() addsimps [real_diff_def]) 1);
   11.68  qed "real_diff_0";
   11.69 @@ -458,8 +478,12 @@
   11.70  by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
   11.71  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   11.72             simpset() addsimps [real_zero_iff RS sym]));
   11.73 -by (res_inst_tac [("x","Abs_real (realrel ^^ {(@#$#1p,pinv(D)+@#$#1p)})")] exI 1);
   11.74 -by (res_inst_tac [("x","Abs_real (realrel ^^ {(pinv(D)+@#$#1p,@#$#1p)})")] exI 2);
   11.75 +by (res_inst_tac [("x","Abs_real (realrel ^^ \
   11.76 +\   {(preal_of_prat(prat_of_pnat 1p),pinv(D)+\
   11.77 +\    preal_of_prat(prat_of_pnat 1p))})")] exI 1);
   11.78 +by (res_inst_tac [("x","Abs_real (realrel ^^ \
   11.79 +\   {(pinv(D)+preal_of_prat(prat_of_pnat 1p),\
   11.80 +\    preal_of_prat(prat_of_pnat 1p))})")] exI 2);
   11.81  by (auto_tac (claset(),
   11.82  	      simpset() addsimps [real_mult,
   11.83      pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2,
   11.84 @@ -496,6 +520,14 @@
   11.85  by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   11.86  qed "real_mult_right_cancel";
   11.87  
   11.88 +Goal "!!a. c*a ~= c*b ==> a ~= b";
   11.89 +by (Auto_tac);
   11.90 +qed "real_mult_left_cancel_ccontr";
   11.91 +
   11.92 +Goal "!!a. a*c ~= b*c ==> a ~= b";
   11.93 +by (Auto_tac);
   11.94 +qed "real_mult_right_cancel_ccontr";
   11.95 +
   11.96  Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
   11.97  by (forward_tac [real_mult_inv_left_ex] 1);
   11.98  by (etac exE 1);
   11.99 @@ -507,6 +539,14 @@
  11.100  
  11.101  Addsimps [real_mult_inv_left,real_mult_inv_right];
  11.102  
  11.103 +Goal "!!x. [| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
  11.104 +by (Step_tac 1);
  11.105 +by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1);
  11.106 +by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
  11.107 +qed "real_mult_not_zero";
  11.108 +
  11.109 +bind_thm ("real_mult_not_zeroE",real_mult_not_zero RS notE);
  11.110 +
  11.111  Goal "x ~= 0r ==> rinv(rinv x) = x";
  11.112  by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
  11.113  by (etac rinv_not_zero 1);
  11.114 @@ -522,16 +562,30 @@
  11.115  	      simpset() addsimps 
  11.116      [real_zero_not_eq_one RS not_sym]));
  11.117  qed "real_rinv_1";
  11.118 +Addsimps [real_rinv_1];
  11.119  
  11.120  Goal "x ~= 0r ==> rinv(-x) = -rinv(x)";
  11.121  by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
  11.122  by Auto_tac;
  11.123  qed "real_minus_rinv";
  11.124  
  11.125 -      (*** theorems for ordering ***)
  11.126 +Goal "!!x y. [| x ~= 0r; y ~= 0r |] \
  11.127 +\                     ==> rinv(x*y) = rinv(x)*rinv(y)";
  11.128 +by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
  11.129 +by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
  11.130 +by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
  11.131 +by (res_inst_tac [("c1","y")] (real_mult_left_cancel RS iffD1) 1);
  11.132 +by (auto_tac (claset(),simpset() addsimps [real_mult_left_commute]));
  11.133 +by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
  11.134 +qed "real_rinv_distrib";
  11.135 +
  11.136 +(*---------------------------------------------------------
  11.137 +     Theorems for ordering
  11.138 + --------------------------------------------------------*)
  11.139  (* prove introduction and elimination rules for real_less *)
  11.140  
  11.141 -(* real_less is a strong order i.e nonreflexive and transitive *)
  11.142 +(* real_less is a strong order i.e. nonreflexive and transitive *)
  11.143 +
  11.144  (*** lemmas ***)
  11.145  Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y";
  11.146  by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1);
  11.147 @@ -599,195 +653,209 @@
  11.148  (****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
  11.149      (****** Map and more real_less ******)
  11.150  (*** mapping from preal into real ***)
  11.151 -Goalw [real_preal_def] 
  11.152 -            "%#((z1::preal) + z2) = %#z1 + %#z2";
  11.153 +Goalw [real_of_preal_def] 
  11.154 +     "real_of_preal ((z1::preal) + z2) = \
  11.155 +\     real_of_preal z1 + real_of_preal z2";
  11.156  by (asm_simp_tac (simpset() addsimps [real_add,
  11.157         preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1);
  11.158 -qed "real_preal_add";
  11.159 +qed "real_of_preal_add";
  11.160  
  11.161 -Goalw [real_preal_def] 
  11.162 -            "%#((z1::preal) * z2) = %#z1* %#z2";
  11.163 +Goalw [real_of_preal_def] 
  11.164 +     "real_of_preal ((z1::preal) * z2) = \
  11.165 +\     real_of_preal z1* real_of_preal z2";
  11.166  by (full_simp_tac (simpset() addsimps [real_mult,
  11.167          preal_add_mult_distrib2,preal_mult_1,
  11.168          preal_mult_1_right,pnat_one_def] 
  11.169          @ preal_add_ac @ preal_mult_ac) 1);
  11.170 -qed "real_preal_mult";
  11.171 +qed "real_of_preal_mult";
  11.172  
  11.173 -Goalw [real_preal_def]
  11.174 -      "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m";
  11.175 +Goalw [real_of_preal_def]
  11.176 +      "!!(x::preal). y < x ==> \
  11.177 +\      ? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m";
  11.178  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  11.179      simpset() addsimps preal_add_ac));
  11.180 -qed "real_preal_ExI";
  11.181 +qed "real_of_preal_ExI";
  11.182  
  11.183 -Goalw [real_preal_def]
  11.184 -      "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#m ==> y < x";
  11.185 +Goalw [real_of_preal_def]
  11.186 +      "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = \
  11.187 +\                    real_of_preal m ==> y < x";
  11.188  by (auto_tac (claset(),
  11.189  	      simpset() addsimps 
  11.190      [preal_add_commute,preal_add_assoc]));
  11.191  by (asm_full_simp_tac (simpset() addsimps 
  11.192      [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
  11.193 -qed "real_preal_ExD";
  11.194 +qed "real_of_preal_ExD";
  11.195  
  11.196 -Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)";
  11.197 -by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1);
  11.198 -qed "real_preal_iff";
  11.199 +Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)";
  11.200 +by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
  11.201 +qed "real_of_preal_iff";
  11.202  
  11.203  (*** Gleason prop 9-4.4 p 127 ***)
  11.204 -Goalw [real_preal_def,real_zero_def] 
  11.205 -      "? m. (x::real) = %#m | x = 0r | x = -(%#m)";
  11.206 +Goalw [real_of_preal_def,real_zero_def] 
  11.207 +      "? m. (x::real) = real_of_preal m | x = 0r | x = -(real_of_preal m)";
  11.208  by (res_inst_tac [("z","x")] eq_Abs_real 1);
  11.209  by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
  11.210  by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
  11.211  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  11.212      simpset() addsimps [preal_add_assoc RS sym]));
  11.213  by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
  11.214 -qed "real_preal_trichotomy";
  11.215 +qed "real_of_preal_trichotomy";
  11.216  
  11.217 -Goal "!!P. [| !!m. x = %#m ==> P; \
  11.218 +Goal "!!P. [| !!m. x = real_of_preal m ==> P; \
  11.219  \             x = 0r ==> P; \
  11.220 -\             !!m. x = -(%#m) ==> P |] ==> P";
  11.221 -by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
  11.222 +\             !!m. x = -(real_of_preal m) ==> P |] ==> P";
  11.223 +by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
  11.224  by Auto_tac;
  11.225 -qed "real_preal_trichotomyE";
  11.226 +qed "real_of_preal_trichotomyE";
  11.227  
  11.228 -Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
  11.229 +Goalw [real_of_preal_def] 
  11.230 +      "real_of_preal m1 < real_of_preal m2 ==> m1 < m2";
  11.231  by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
  11.232  by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
  11.233  by (auto_tac (claset(),simpset() addsimps preal_add_ac));
  11.234 -qed "real_preal_lessD";
  11.235 +qed "real_of_preal_lessD";
  11.236  
  11.237 -Goal "m1 < m2 ==> %#m1 < %#m2";
  11.238 +Goal "m1 < m2 ==> real_of_preal m1 < real_of_preal m2";
  11.239  by (dtac preal_less_add_left_Ex 1);
  11.240  by (auto_tac (claset(),
  11.241 -	      simpset() addsimps [real_preal_add,
  11.242 -    real_preal_def,real_less_def]));
  11.243 +	      simpset() addsimps [real_of_preal_add,
  11.244 +    real_of_preal_def,real_less_def]));
  11.245  by (REPEAT(rtac exI 1));
  11.246  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.247  by (REPEAT(Blast_tac 2));
  11.248  by (simp_tac (simpset() addsimps [preal_self_less_add_left] 
  11.249      delsimps [preal_add_less_iff2]) 1);
  11.250 -qed "real_preal_lessI";
  11.251 +qed "real_of_preal_lessI";
  11.252  
  11.253 -Goal "(%#m1 < %#m2) = (m1 < m2)";
  11.254 -by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1);
  11.255 -qed "real_preal_less_iff1";
  11.256 +Goal "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)";
  11.257 +by (blast_tac (claset() addIs [real_of_preal_lessI,real_of_preal_lessD]) 1);
  11.258 +qed "real_of_preal_less_iff1";
  11.259  
  11.260 -Addsimps [real_preal_less_iff1];
  11.261 +Addsimps [real_of_preal_less_iff1];
  11.262  
  11.263 -Goal "- %#m < %#m";
  11.264 +Goal "- real_of_preal m < real_of_preal m";
  11.265  by (auto_tac (claset(),
  11.266  	      simpset() addsimps 
  11.267 -    [real_preal_def,real_less_def,real_minus]));
  11.268 +    [real_of_preal_def,real_less_def,real_minus]));
  11.269  by (REPEAT(rtac exI 1));
  11.270  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.271  by (REPEAT(Blast_tac 2));
  11.272  by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
  11.273  by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
  11.274      preal_add_assoc RS sym]) 1);
  11.275 -qed "real_preal_minus_less_self";
  11.276 +qed "real_of_preal_minus_less_self";
  11.277  
  11.278 -Goalw [real_zero_def] "- %#m < 0r";
  11.279 +Goalw [real_zero_def] "- real_of_preal m < 0r";
  11.280  by (auto_tac (claset(),
  11.281 -	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
  11.282 +    simpset() addsimps [real_of_preal_def,
  11.283 +    real_less_def,real_minus]));
  11.284  by (REPEAT(rtac exI 1));
  11.285  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.286  by (REPEAT(Blast_tac 2));
  11.287  by (full_simp_tac (simpset() addsimps 
  11.288    [preal_self_less_add_right] @ preal_add_ac) 1);
  11.289 -qed "real_preal_minus_less_zero";
  11.290 +qed "real_of_preal_minus_less_zero";
  11.291  
  11.292 -Goal "~ 0r < - %#m";
  11.293 -by (cut_facts_tac [real_preal_minus_less_zero] 1);
  11.294 +Goal "~ 0r < - real_of_preal m";
  11.295 +by (cut_facts_tac [real_of_preal_minus_less_zero] 1);
  11.296  by (fast_tac (claset() addDs [real_less_trans] 
  11.297                          addEs [real_less_irrefl]) 1);
  11.298 -qed "real_preal_not_minus_gt_zero";
  11.299 +qed "real_of_preal_not_minus_gt_zero";
  11.300  
  11.301 -Goalw [real_zero_def] "0r < %#m";
  11.302 -by (auto_tac (claset(),
  11.303 -	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
  11.304 +Goalw [real_zero_def] "0r < real_of_preal m";
  11.305 +by (auto_tac (claset(),simpset() addsimps 
  11.306 +   [real_of_preal_def,real_less_def,real_minus]));
  11.307  by (REPEAT(rtac exI 1));
  11.308  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.309  by (REPEAT(Blast_tac 2));
  11.310  by (full_simp_tac (simpset() addsimps 
  11.311  		   [preal_self_less_add_right] @ preal_add_ac) 1);
  11.312 -qed "real_preal_zero_less";
  11.313 +qed "real_of_preal_zero_less";
  11.314  
  11.315 -Goal "~ %#m < 0r";
  11.316 -by (cut_facts_tac [real_preal_zero_less] 1);
  11.317 +Goal "~ real_of_preal m < 0r";
  11.318 +by (cut_facts_tac [real_of_preal_zero_less] 1);
  11.319  by (blast_tac (claset() addDs [real_less_trans] 
  11.320                 addEs [real_less_irrefl]) 1);
  11.321 -qed "real_preal_not_less_zero";
  11.322 +qed "real_of_preal_not_less_zero";
  11.323  
  11.324 -Goal "0r < - - %#m";
  11.325 +Goal "0r < - - real_of_preal m";
  11.326  by (simp_tac (simpset() addsimps 
  11.327 -    [real_preal_zero_less]) 1);
  11.328 +    [real_of_preal_zero_less]) 1);
  11.329  qed "real_minus_minus_zero_less";
  11.330  
  11.331  (* another lemma *)
  11.332 -Goalw [real_zero_def] "0r < %#m + %#m1";
  11.333 +Goalw [real_zero_def]
  11.334 +      "0r < real_of_preal m + real_of_preal m1";
  11.335  by (auto_tac (claset(),
  11.336 -	      simpset() addsimps [real_preal_def,real_less_def,real_add]));
  11.337 +	      simpset() addsimps [real_of_preal_def,
  11.338 +              real_less_def,real_add]));
  11.339  by (REPEAT(rtac exI 1));
  11.340  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.341  by (REPEAT(Blast_tac 2));
  11.342  by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
  11.343  by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
  11.344      preal_add_assoc RS sym]) 1);
  11.345 -qed "real_preal_sum_zero_less";
  11.346 +qed "real_of_preal_sum_zero_less";
  11.347  
  11.348 -Goal "- %#m < %#m1";
  11.349 +Goal "- real_of_preal m < real_of_preal m1";
  11.350  by (auto_tac (claset(),
  11.351 -	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
  11.352 +	      simpset() addsimps [real_of_preal_def,
  11.353 +              real_less_def,real_minus]));
  11.354  by (REPEAT(rtac exI 1));
  11.355  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.356  by (REPEAT(Blast_tac 2));
  11.357  by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
  11.358  by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
  11.359      preal_add_assoc RS sym]) 1);
  11.360 -qed "real_preal_minus_less_all";
  11.361 +qed "real_of_preal_minus_less_all";
  11.362  
  11.363 -Goal "~ %#m < - %#m1";
  11.364 -by (cut_facts_tac [real_preal_minus_less_all] 1);
  11.365 +Goal "~ real_of_preal m < - real_of_preal m1";
  11.366 +by (cut_facts_tac [real_of_preal_minus_less_all] 1);
  11.367  by (blast_tac (claset() addDs [real_less_trans] 
  11.368                 addEs [real_less_irrefl]) 1);
  11.369 -qed "real_preal_not_minus_gt_all";
  11.370 +qed "real_of_preal_not_minus_gt_all";
  11.371  
  11.372 -Goal "- %#m1 < - %#m2 ==> %#m2 < %#m1";
  11.373 +Goal "- real_of_preal m1 < - real_of_preal m2 \
  11.374 +\     ==> real_of_preal m2 < real_of_preal m1";
  11.375  by (auto_tac (claset(),
  11.376 -	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
  11.377 +	      simpset() addsimps [real_of_preal_def,
  11.378 +              real_less_def,real_minus]));
  11.379  by (REPEAT(rtac exI 1));
  11.380  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.381  by (REPEAT(Blast_tac 2));
  11.382  by (auto_tac (claset(),simpset() addsimps preal_add_ac));
  11.383  by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
  11.384  by (auto_tac (claset(),simpset() addsimps preal_add_ac));
  11.385 -qed "real_preal_minus_less_rev1";
  11.386 +qed "real_of_preal_minus_less_rev1";
  11.387  
  11.388 -Goal "%#m1 < %#m2 ==> - %#m2 < - %#m1";
  11.389 +Goal "real_of_preal m1 < real_of_preal m2 \
  11.390 +\     ==> - real_of_preal m2 < - real_of_preal m1";
  11.391  by (auto_tac (claset(),
  11.392 -	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
  11.393 +	      simpset() addsimps [real_of_preal_def,
  11.394 +              real_less_def,real_minus]));
  11.395  by (REPEAT(rtac exI 1));
  11.396  by (EVERY[rtac conjI 1, rtac conjI 2]);
  11.397  by (REPEAT(Blast_tac 2));
  11.398  by (auto_tac (claset(),simpset() addsimps preal_add_ac));
  11.399  by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
  11.400  by (auto_tac (claset(),simpset() addsimps preal_add_ac));
  11.401 -qed "real_preal_minus_less_rev2";
  11.402 +qed "real_of_preal_minus_less_rev2";
  11.403  
  11.404 -Goal "(- %#m1 < - %#m2) = (%#m2 < %#m1)";
  11.405 -by (blast_tac (claset() addSIs [real_preal_minus_less_rev1,
  11.406 -               real_preal_minus_less_rev2]) 1);
  11.407 -qed "real_preal_minus_less_rev_iff";
  11.408 +Goal "(- real_of_preal m1 < - real_of_preal m2) = \
  11.409 +\     (real_of_preal m2 < real_of_preal m1)";
  11.410 +by (blast_tac (claset() addSIs [real_of_preal_minus_less_rev1,
  11.411 +               real_of_preal_minus_less_rev2]) 1);
  11.412 +qed "real_of_preal_minus_less_rev_iff";
  11.413  
  11.414 -Addsimps [real_preal_minus_less_rev_iff];
  11.415 +Addsimps [real_of_preal_minus_less_rev_iff];
  11.416  
  11.417  (*** linearity ***)
  11.418  Goal "(R1::real) < R2 | R1 = R2 | R2 < R1";
  11.419 -by (res_inst_tac [("x","R1")]  real_preal_trichotomyE 1);
  11.420 -by (ALLGOALS(res_inst_tac [("x","R2")]  real_preal_trichotomyE));
  11.421 +by (res_inst_tac [("x","R1")]  real_of_preal_trichotomyE 1);
  11.422 +by (ALLGOALS(res_inst_tac [("x","R2")]  real_of_preal_trichotomyE));
  11.423  by (auto_tac (claset() addSDs [preal_le_anti_sym],
  11.424 -              simpset() addsimps [preal_less_le_iff,real_preal_minus_less_zero,
  11.425 -               real_preal_zero_less,real_preal_minus_less_all]));
  11.426 +              simpset() addsimps [preal_less_le_iff,real_of_preal_minus_less_zero,
  11.427 +               real_of_preal_zero_less,real_of_preal_minus_less_all]));
  11.428  qed "real_linear";
  11.429  
  11.430  Goal "!!w::real. (w ~= z) = (w<z | z<w)";
  11.431 @@ -883,46 +951,42 @@
  11.432  by (blast_tac (claset() addSEs [real_less_asym]) 1);
  11.433  qed "real_less_le";
  11.434  
  11.435 -
  11.436  Goal "(0r < -R) = (R < 0r)";
  11.437 -by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
  11.438 +by (res_inst_tac [("x","R")]  real_of_preal_trichotomyE 1);
  11.439  by (auto_tac (claset(),
  11.440 -	      simpset() addsimps [real_preal_not_minus_gt_zero,
  11.441 -                        real_preal_not_less_zero,real_preal_zero_less,
  11.442 -                        real_preal_minus_less_zero]));
  11.443 +	      simpset() addsimps [real_of_preal_not_minus_gt_zero,
  11.444 +                        real_of_preal_not_less_zero,real_of_preal_zero_less,
  11.445 +                        real_of_preal_minus_less_zero]));
  11.446  qed "real_minus_zero_less_iff";
  11.447  
  11.448  Addsimps [real_minus_zero_less_iff];
  11.449  
  11.450  Goal "(-R < 0r) = (0r < R)";
  11.451 -by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
  11.452 +by (res_inst_tac [("x","R")]  real_of_preal_trichotomyE 1);
  11.453  by (auto_tac (claset(),
  11.454 -	      simpset() addsimps [real_preal_not_minus_gt_zero,
  11.455 -                        real_preal_not_less_zero,real_preal_zero_less,
  11.456 -                        real_preal_minus_less_zero]));
  11.457 +	      simpset() addsimps [real_of_preal_not_minus_gt_zero,
  11.458 +                        real_of_preal_not_less_zero,real_of_preal_zero_less,
  11.459 +                        real_of_preal_minus_less_zero]));
  11.460  qed "real_minus_zero_less_iff2";
  11.461  
  11.462 -
  11.463  (*Alternative definition for real_less*)
  11.464  Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S";
  11.465 -by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
  11.466 -by (ALLGOALS(res_inst_tac [("x","S")]  real_preal_trichotomyE));
  11.467 +by (res_inst_tac [("x","R")]  real_of_preal_trichotomyE 1);
  11.468 +by (ALLGOALS(res_inst_tac [("x","S")]  real_of_preal_trichotomyE));
  11.469  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  11.470 -	      simpset() addsimps [real_preal_not_minus_gt_all,
  11.471 -				  real_preal_add, real_preal_not_less_zero,
  11.472 +	      simpset() addsimps [real_of_preal_not_minus_gt_all,
  11.473 +				  real_of_preal_add, real_of_preal_not_less_zero,
  11.474  				  real_less_not_refl,
  11.475 -				  real_preal_not_minus_gt_zero]));
  11.476 -by (res_inst_tac [("x","%#D")] exI 1);
  11.477 -by (res_inst_tac [("x","%#m+%#ma")] exI 2);
  11.478 -by (res_inst_tac [("x","%#m")] exI 3);
  11.479 -by (res_inst_tac [("x","%#D")] exI 4);
  11.480 +				  real_of_preal_not_minus_gt_zero]));
  11.481 +by (res_inst_tac [("x","real_of_preal D")] exI 1);
  11.482 +by (res_inst_tac [("x","real_of_preal m+real_of_preal ma")] exI 2);
  11.483 +by (res_inst_tac [("x","real_of_preal m")] exI 3);
  11.484 +by (res_inst_tac [("x","real_of_preal D")] exI 4);
  11.485  by (auto_tac (claset(),
  11.486 -	      simpset() addsimps [real_preal_zero_less,
  11.487 -				  real_preal_sum_zero_less,real_add_assoc]));
  11.488 +	      simpset() addsimps [real_of_preal_zero_less,
  11.489 +				  real_of_preal_sum_zero_less,real_add_assoc]));
  11.490  qed "real_less_add_positive_left_Ex";
  11.491  
  11.492 -
  11.493 -
  11.494  (** change naff name(s)! **)
  11.495  Goal "(W < S) ==> (0r < S + -W)";
  11.496  by (dtac real_less_add_positive_left_Ex 1);
    12.1 --- a/src/HOL/Real/RealDef.thy	Fri Jul 23 17:28:18 1999 +0200
    12.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jul 23 17:29:12 1999 +0200
    12.3 @@ -23,24 +23,33 @@
    12.4  
    12.5  defs
    12.6  
    12.7 -  real_zero_def  "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})"
    12.8 -  real_one_def   "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})"
    12.9 +  real_zero_def  
   12.10 +     "0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
   12.11 +                                preal_of_prat(prat_of_pnat 1p))})"
   12.12 +  real_one_def   
   12.13 +     "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
   12.14 +            preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
   12.15  
   12.16    real_minus_def
   12.17 -    "- R ==  Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)"
   12.18 +    "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
   12.19  
   12.20    real_diff_def "x - y == x + -(y::real)"
   12.21  
   12.22  constdefs
   12.23  
   12.24 -  real_preal :: preal => real              ("%#_" [100] 100)
   12.25 -  "%# m     == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})"
   12.26 +  real_of_preal :: preal => real            
   12.27 +  "real_of_preal m     ==
   12.28 +           Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p),
   12.29 +                               preal_of_prat(prat_of_pnat 1p))})"
   12.30  
   12.31    rinv       :: real => real
   12.32    "rinv(R)   == (@S. R ~= 0r & S*R = 1r)"
   12.33  
   12.34 -  real_nat :: nat => real                  ("%%# _" [100] 100) 
   12.35 -  "%%# n      == %#(@#($#(*# n)))"
   12.36 +  real_of_posnat :: nat => real             
   12.37 +  "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
   12.38 +
   12.39 +  real_of_nat :: nat => real          
   12.40 +  "real_of_nat n    == real_of_posnat n + -1r"
   12.41  
   12.42  defs
   12.43  
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Real/RealPow.ML	Fri Jul 23 17:29:12 1999 +0200
    13.3 @@ -0,0 +1,374 @@
    13.4 +(*  Title       : RealPow.ML
    13.5 +    Author      : Jacques D. Fleuriot  
    13.6 +    Copyright   : 1998  University of Cambridge
    13.7 +    Description : Natural Powers of reals theory
    13.8 +
    13.9 +*)
   13.10 +
   13.11 +Goal "0r ^ (Suc n) = 0r";
   13.12 +by (Auto_tac);
   13.13 +qed "realpow_zero";
   13.14 +Addsimps [realpow_zero];
   13.15 +
   13.16 +Goal "r ~= 0r --> r ^ n ~= 0r";
   13.17 +by (induct_tac "n" 1);
   13.18 +by (auto_tac (claset() addIs [real_mult_not_zeroE],
   13.19 +    simpset() addsimps [real_zero_not_eq_one RS not_sym]));
   13.20 +qed_spec_mp "realpow_not_zero";
   13.21 +
   13.22 +Goal "!!r. r ^ n = 0r ==> r = 0r";
   13.23 +by (blast_tac (claset() addIs [ccontr] 
   13.24 +    addDs [realpow_not_zero]) 1);
   13.25 +qed "realpow_zero_zero";
   13.26 +
   13.27 +Goal "r ~= 0r --> rinv(r ^ n) = (rinv r) ^ n";
   13.28 +by (induct_tac "n" 1);
   13.29 +by (Auto_tac);
   13.30 +by (forw_inst_tac [("n","n")] realpow_not_zero 1);
   13.31 +by (auto_tac (claset() addDs [real_rinv_distrib],
   13.32 +    simpset()));
   13.33 +qed_spec_mp "realpow_rinv";
   13.34 +
   13.35 +Goal "rabs r ^ n = rabs (r ^ n)";
   13.36 +by (induct_tac "n" 1);
   13.37 +by (auto_tac (claset(),simpset() addsimps 
   13.38 +    [rabs_mult,rabs_one]));
   13.39 +qed "realpow_rabs";
   13.40 +
   13.41 +Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
   13.42 +by (induct_tac "n" 1);
   13.43 +by (auto_tac (claset(),simpset() addsimps real_mult_ac));
   13.44 +qed "realpow_add";
   13.45 +
   13.46 +Goal "(r::real) ^ 1 = r";
   13.47 +by (Simp_tac 1);
   13.48 +qed "realpow_one";
   13.49 +Addsimps [realpow_one];
   13.50 +
   13.51 +Goal "(r::real) ^ 2 = r * r";
   13.52 +by (Simp_tac 1);
   13.53 +qed "realpow_two";
   13.54 +
   13.55 +Goal "0r < r --> 0r <= r ^ n";
   13.56 +by (induct_tac "n" 1);
   13.57 +by (auto_tac (claset() addDs [real_less_imp_le] 
   13.58 +    addIs [real_le_mult_order],simpset()));
   13.59 +qed_spec_mp "realpow_ge_zero";
   13.60 +
   13.61 +Goal "0r < r --> 0r < r ^ n";
   13.62 +by (induct_tac "n" 1);
   13.63 +by (auto_tac (claset() addIs [real_mult_order],
   13.64 +    simpset() addsimps [real_zero_less_one]));
   13.65 +qed_spec_mp "realpow_gt_zero";
   13.66 +
   13.67 +Goal "0r <= r --> 0r <= r ^ n";
   13.68 +by (induct_tac "n" 1);
   13.69 +by (auto_tac (claset() addIs [real_le_mult_order],
   13.70 +              simpset()));
   13.71 +qed_spec_mp "realpow_ge_zero2";
   13.72 +
   13.73 +Goal "0r < x & x <= y --> x ^ n <= y ^ n";
   13.74 +by (induct_tac "n" 1);
   13.75 +by (auto_tac (claset() addSIs [real_mult_le_mono],
   13.76 +    simpset()));
   13.77 +by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
   13.78 +qed_spec_mp "realpow_le";
   13.79 +
   13.80 +Goal "0r <= x & x <= y --> x ^ n <= y ^ n";
   13.81 +by (induct_tac "n" 1);
   13.82 +by (auto_tac (claset() addSIs [real_mult_le_mono4],
   13.83 +    simpset()));
   13.84 +by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
   13.85 +qed_spec_mp "realpow_le2";
   13.86 +
   13.87 +Goal "0r < x & x < y & 0 < n --> x ^ n < y ^ n";
   13.88 +by (induct_tac "n" 1);
   13.89 +by (auto_tac (claset() addIs [real_mult_less_mono,
   13.90 +    gr0I] addDs [realpow_gt_zero],simpset()));
   13.91 +qed_spec_mp "realpow_less";
   13.92 +
   13.93 +Goal  "1r ^ n = 1r";
   13.94 +by (induct_tac "n" 1);
   13.95 +by (Auto_tac);
   13.96 +qed "realpow_eq_one";
   13.97 +Addsimps [realpow_eq_one];
   13.98 +
   13.99 +Goal "rabs(-(1r ^ n)) = 1r";
  13.100 +by (simp_tac (simpset() addsimps 
  13.101 +    [rabs_minus_cancel,rabs_one]) 1);
  13.102 +qed "rabs_minus_realpow_one";
  13.103 +Addsimps [rabs_minus_realpow_one];
  13.104 +
  13.105 +Goal "rabs((-1r) ^ n) = 1r";
  13.106 +by (induct_tac "n" 1);
  13.107 +by (auto_tac (claset(),simpset() addsimps [rabs_mult,
  13.108 +         rabs_minus_cancel,rabs_one]));
  13.109 +qed "rabs_realpow_minus_one";
  13.110 +Addsimps [rabs_realpow_minus_one];
  13.111 +
  13.112 +Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
  13.113 +by (induct_tac "n" 1);
  13.114 +by (auto_tac (claset(),simpset() addsimps real_mult_ac));
  13.115 +qed "realpow_mult";
  13.116 +
  13.117 +Goal "0r <= r ^ 2";
  13.118 +by (simp_tac (simpset() addsimps [realpow_two]) 1);
  13.119 +qed "realpow_two_le";
  13.120 +Addsimps [realpow_two_le];
  13.121 +
  13.122 +Goal "rabs(x ^ 2) = x ^ 2";
  13.123 +by (simp_tac (simpset() addsimps [rabs_eqI1]) 1);
  13.124 +qed "rabs_realpow_two";
  13.125 +Addsimps [rabs_realpow_two];
  13.126 +
  13.127 +Goal "rabs(x) ^ 2 = x ^ 2";
  13.128 +by (simp_tac (simpset() addsimps 
  13.129 +    [realpow_rabs,rabs_eqI1] delsimps [realpow_Suc]) 1);
  13.130 +qed "realpow_two_rabs";
  13.131 +Addsimps [realpow_two_rabs];
  13.132 +
  13.133 +Goal "!!r. 1r < r ==> 1r < r ^ 2";
  13.134 +by (auto_tac (claset(),simpset() addsimps [realpow_two]));
  13.135 +by (cut_facts_tac [real_zero_less_one] 1);
  13.136 +by (forw_inst_tac [("R1.0","0r")] real_less_trans 1);
  13.137 +by (assume_tac 1);
  13.138 +by (dres_inst_tac [("z","r"),("x","1r")] real_mult_less_mono1 1);
  13.139 +by (auto_tac (claset() addIs [real_less_trans],simpset()));
  13.140 +qed "realpow_two_gt_one";
  13.141 +
  13.142 +Goal "!!r. 1r <= r ==> 1r <= r ^ 2";
  13.143 +by (etac (real_le_imp_less_or_eq RS disjE) 1);
  13.144 +by (etac (realpow_two_gt_one RS real_less_imp_le) 1);
  13.145 +by (asm_simp_tac (simpset()) 1);
  13.146 +qed "realpow_two_ge_one";
  13.147 +
  13.148 +(* more general result *)
  13.149 +Goal "1r < r --> 1r <= r ^ n";
  13.150 +by (induct_tac "n" 1);
  13.151 +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
  13.152 +    simpset()));
  13.153 +by (dtac (real_zero_less_one RS real_mult_less_mono) 1);
  13.154 +by (dtac sym 4);
  13.155 +by (auto_tac (claset() addSIs [real_less_imp_le],
  13.156 +    simpset() addsimps [real_zero_less_one]));
  13.157 +qed_spec_mp "realpow_ge_one";
  13.158 +
  13.159 +Goal "!!r. 1r < r ==> 1r < r ^ (Suc n)";
  13.160 +by (forw_inst_tac [("n","n")] realpow_ge_one 1);
  13.161 +by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
  13.162 +by (dtac sym 2);
  13.163 +by (forward_tac [real_zero_less_one RS real_less_trans] 1);
  13.164 +by (dres_inst_tac [("y","r ^ n")] real_mult_less_mono2 1);
  13.165 +by (auto_tac (claset() addDs [real_less_trans],
  13.166 +     simpset()));
  13.167 +qed "realpow_Suc_gt_one";
  13.168 +
  13.169 +Goal "!!r. 1r <= r ==> 1r <= r ^ n";
  13.170 +by (dtac real_le_imp_less_or_eq 1); 
  13.171 +by (auto_tac (claset() addDs [realpow_ge_one],
  13.172 +    simpset()));
  13.173 +qed "realpow_ge_one2";
  13.174 +
  13.175 +Goal "!!r. 0r < r ==> 0r < r ^ Suc n";
  13.176 +by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
  13.177 +by (forw_inst_tac [("n1","n")]
  13.178 +    ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
  13.179 +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
  13.180 +     addIs [real_mult_order],simpset()));
  13.181 +qed "realpow_Suc_gt_zero";
  13.182 +
  13.183 +Goal "!!r. 0r <= r ==> 0r <= r ^ Suc n";
  13.184 +by (etac (real_le_imp_less_or_eq RS disjE) 1);
  13.185 +by (etac (realpow_ge_zero) 1);
  13.186 +by (asm_simp_tac (simpset()) 1);
  13.187 +qed "realpow_Suc_ge_zero";
  13.188 +
  13.189 +Goal "1r <= (1r +1r) ^ n";
  13.190 +by (res_inst_tac [("j","1r ^ n")] real_le_trans 1);
  13.191 +by (rtac realpow_le 2);
  13.192 +by (auto_tac (claset() addIs [real_less_imp_le],
  13.193 +    simpset() addsimps [real_zero_less_one,
  13.194 +    real_one_less_two]));
  13.195 +qed "two_realpow_ge_one";
  13.196 +
  13.197 +Goal "real_of_nat n < (1r + 1r) ^ n";
  13.198 +by (induct_tac "n" 1);
  13.199 +by (rtac (lemmaS RS ssubst) 2);
  13.200 +by (rtac (real_of_nat_add RS subst) 2);
  13.201 +by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero,
  13.202 +    real_zero_less_one,real_add_mult_distrib,real_of_nat_one]));
  13.203 +by (blast_tac (claset() addSIs [real_add_less_le_mono,
  13.204 +    two_realpow_ge_one]) 1);
  13.205 +qed "two_realpow_gt";
  13.206 +Addsimps [two_realpow_gt,two_realpow_ge_one];
  13.207 +
  13.208 +Goal "(-1r) ^ (2*n) = 1r";
  13.209 +by (induct_tac "n" 1);
  13.210 +by (Auto_tac);
  13.211 +qed "realpow_minus_one";
  13.212 +Addsimps [realpow_minus_one];
  13.213 +
  13.214 +Goal "(-1r) ^ (n + n) = 1r";
  13.215 +by (induct_tac "n" 1);
  13.216 +by (Auto_tac);
  13.217 +qed "realpow_minus_one2";
  13.218 +Addsimps [realpow_minus_one2];
  13.219 +
  13.220 +Goal "(-1r) ^ Suc (n + n) = -1r";
  13.221 +by (induct_tac "n" 1);
  13.222 +by (Auto_tac);
  13.223 +qed "realpow_minus_one_odd";
  13.224 +Addsimps [realpow_minus_one_odd];
  13.225 +
  13.226 +Goal "(-1r) ^ Suc (Suc (n + n)) = 1r";
  13.227 +by (induct_tac "n" 1);
  13.228 +by (Auto_tac);
  13.229 +qed "realpow_minus_one_even";
  13.230 +Addsimps [realpow_minus_one_even];
  13.231 +
  13.232 +Goal "0r < r & r < 1r --> r ^ Suc n < r ^ n";
  13.233 +by (induct_tac "n" 1);
  13.234 +by (Auto_tac);
  13.235 +qed_spec_mp "realpow_Suc_less";
  13.236 +
  13.237 +Goal "0r <= r & r < 1r --> r ^ Suc n <= r ^ n";
  13.238 +by (induct_tac "n" 1);
  13.239 +by (auto_tac (claset() addIs [real_less_imp_le] addSDs
  13.240 +     [real_le_imp_less_or_eq],simpset()));
  13.241 +qed_spec_mp "realpow_Suc_le";
  13.242 +
  13.243 +Goal "0r <= 0r ^ n";
  13.244 +by (exhaust_tac "n" 1);
  13.245 +by (Auto_tac);
  13.246 +qed "realpow_zero_le";
  13.247 +Addsimps [realpow_zero_le];
  13.248 +
  13.249 +Goal "0r < r & r < 1r --> r ^ Suc n <= r ^ n";
  13.250 +by (blast_tac (claset() addSIs [real_less_imp_le,
  13.251 +    realpow_Suc_less]) 1);
  13.252 +qed_spec_mp "realpow_Suc_le2";
  13.253 +
  13.254 +Goal "!!r. [| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n";
  13.255 +by (etac (real_le_imp_less_or_eq RS disjE) 1);
  13.256 +by (rtac realpow_Suc_le2 1);
  13.257 +by (Auto_tac);
  13.258 +qed "realpow_Suc_le3";
  13.259 +
  13.260 +Goal "0r <= r & r < 1r & n < N --> r ^ N <= r ^ n";
  13.261 +by (induct_tac "N" 1);
  13.262 +by (Auto_tac);
  13.263 +by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
  13.264 +by (ALLGOALS(dtac real_mult_le_mono3));
  13.265 +by (REPEAT(assume_tac 1));
  13.266 +by (REPEAT(assume_tac 3));
  13.267 +by (auto_tac (claset(),simpset() addsimps 
  13.268 +    [less_Suc_eq]));
  13.269 +qed_spec_mp "realpow_less_le";
  13.270 +
  13.271 +Goal "!!r. [| 0r <= r; r < 1r; n <= N |] \
  13.272 +\          ==> r ^ N <= r ^ n";
  13.273 +by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  13.274 +by (auto_tac (claset() addIs [realpow_less_le],
  13.275 +    simpset()));
  13.276 +qed "realpow_le_le";
  13.277 +
  13.278 +Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n <= r";
  13.279 +by (dres_inst_tac [("n","1"),("N","Suc n")] 
  13.280 +    (real_less_imp_le RS realpow_le_le) 1);
  13.281 +by (Auto_tac);
  13.282 +qed "realpow_Suc_le_self";
  13.283 +
  13.284 +Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n < 1r";
  13.285 +by (blast_tac (claset() addIs [realpow_Suc_le_self,
  13.286 +               real_le_less_trans]) 1);
  13.287 +qed "realpow_Suc_less_one";
  13.288 +
  13.289 +Goal "1r <= r --> r ^ n <= r ^ Suc n";
  13.290 +by (induct_tac "n" 1);
  13.291 +by (auto_tac (claset() addSIs [real_mult_le_le_mono1],simpset()));
  13.292 +by (rtac ccontr 1 THEN dtac not_real_leE 1);
  13.293 +by (dtac real_le_less_trans 1 THEN assume_tac 1);
  13.294 +by (etac (real_zero_less_one RS real_less_asym) 1);
  13.295 +qed_spec_mp "realpow_le_Suc";
  13.296 +
  13.297 +Goal "1r < r --> r ^ n < r ^ Suc n";
  13.298 +by (induct_tac "n" 1);
  13.299 +by (auto_tac (claset() addSIs [real_mult_less_mono2],simpset()));
  13.300 +by (rtac ccontr 1 THEN dtac real_leI 1);
  13.301 +by (dtac real_less_le_trans 1 THEN assume_tac 1);
  13.302 +by (etac (real_zero_less_one RS real_less_asym) 1);
  13.303 +qed_spec_mp "realpow_less_Suc";
  13.304 +
  13.305 +Goal "1r < r --> r ^ n <= r ^ Suc n";
  13.306 +by (blast_tac (claset() addSIs [real_less_imp_le,
  13.307 +    realpow_less_Suc]) 1);
  13.308 +qed_spec_mp "realpow_le_Suc2";
  13.309 +
  13.310 +Goal "1r < r & n < N --> r ^ n <= r ^ N";
  13.311 +by (induct_tac "N" 1);
  13.312 +by (Auto_tac);
  13.313 +by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
  13.314 +by (ALLGOALS(dtac real_mult_self_le));
  13.315 +by (assume_tac 1);
  13.316 +by (assume_tac 2);
  13.317 +by (auto_tac (claset() addIs [real_le_trans],
  13.318 +    simpset() addsimps [less_Suc_eq]));
  13.319 +qed_spec_mp "realpow_gt_ge";
  13.320 +
  13.321 +Goal "1r <= r & n < N --> r ^ n <= r ^ N";
  13.322 +by (induct_tac "N" 1);
  13.323 +by (Auto_tac);
  13.324 +by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
  13.325 +by (ALLGOALS(dtac real_mult_self_le2));
  13.326 +by (assume_tac 1);
  13.327 +by (assume_tac 2);
  13.328 +by (auto_tac (claset() addIs [real_le_trans],
  13.329 +    simpset() addsimps [less_Suc_eq]));
  13.330 +qed_spec_mp "realpow_gt_ge2";
  13.331 +
  13.332 +Goal "!!r. [| 1r < r; n <= N |] ==> r ^ n <= r ^ N";
  13.333 +by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  13.334 +by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
  13.335 +qed "realpow_ge_ge";
  13.336 +
  13.337 +Goal "!!r. [| 1r <= r; n <= N |] ==> r ^ n <= r ^ N";
  13.338 +by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
  13.339 +by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
  13.340 +qed "realpow_ge_ge2";
  13.341 +
  13.342 +Goal "!!r. 1r < r ==> r <= r ^ Suc n";
  13.343 +by (dres_inst_tac [("n","1"),("N","Suc n")] 
  13.344 +    realpow_ge_ge 1);
  13.345 +by (Auto_tac);
  13.346 +qed_spec_mp "realpow_Suc_ge_self";
  13.347 +
  13.348 +Goal "!!r. 1r <= r ==> r <= r ^ Suc n";
  13.349 +by (dres_inst_tac [("n","1"),("N","Suc n")] 
  13.350 +    realpow_ge_ge2 1);
  13.351 +by (Auto_tac);
  13.352 +qed_spec_mp "realpow_Suc_ge_self2";
  13.353 +
  13.354 +Goal "!!r. [| 1r < r; 0 < n |] ==> r <= r ^ n";
  13.355 +by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
  13.356 +by (auto_tac (claset() addSIs 
  13.357 +    [realpow_Suc_ge_self],simpset()));
  13.358 +qed "realpow_ge_self";
  13.359 +
  13.360 +Goal "!!r. [| 1r <= r; 0 < n |] ==> r <= r ^ n";
  13.361 +by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
  13.362 +by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
  13.363 +qed "realpow_ge_self2";
  13.364 +
  13.365 +Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n";
  13.366 +by (induct_tac "n" 1);
  13.367 +by (auto_tac (claset(),simpset() 
  13.368 +    addsimps [real_mult_commute]));
  13.369 +qed_spec_mp "realpow_minus_mult";
  13.370 +Addsimps [realpow_minus_mult];
  13.371 +
  13.372 +Goal "!!r. r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
  13.373 +by (asm_simp_tac (simpset() addsimps [realpow_two,
  13.374 +                  real_mult_assoc RS sym]) 1);
  13.375 +qed "realpow_two_mult_rinv";
  13.376 +Addsimps [realpow_two_mult_rinv];
  13.377 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Real/RealPow.thy	Fri Jul 23 17:29:12 1999 +0200
    14.3 @@ -0,0 +1,16 @@
    14.4 +(*  Title       : RealPow.thy
    14.5 +    Author      : Jacques D. Fleuriot  
    14.6 +    Copyright   : 1998  University of Cambridge
    14.7 +    Description : Natural powers theory
    14.8 +
    14.9 +*)
   14.10 +
   14.11 +RealPow = WF_Rel + RealAbs + 
   14.12 +
   14.13 +instance real :: {power}
   14.14 +
   14.15 +primrec
   14.16 +     realpow_0   "r ^ 0       = 1r"
   14.17 +     realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
   14.18 +
   14.19 +end