Revised version with Abelian group simprocs
authorpaulson
Thu Oct 01 18:18:01 1998 +0200 (1998-10-01)
changeset 5588a3ab526bb891
parent 5587 7fceb6eea475
child 5589 94c05305fb29
Revised version with Abelian group simprocs
src/HOL/Real/PNat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RComplete.ML
src/HOL/Real/ROOT.ML
src/HOL/Real/Real.ML
src/HOL/Real/Real.thy
src/HOL/Real/RealAbs.ML
src/HOL/Real/RealAbs.thy
src/HOL/Real/RealDef.ML
src/HOL/Real/RealDef.thy
src/HOL/Real/simproc.ML
     1.1 --- a/src/HOL/Real/PNat.ML	Tue Sep 29 18:13:05 1998 +0200
     1.2 +++ b/src/HOL/Real/PNat.ML	Thu Oct 01 18:18:01 1998 +0200
     1.3 @@ -518,7 +518,7 @@
     1.4  \     |] ==> f(i) <= (f(j)::pnat)";
     1.5  by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD],
     1.6               simpset() addsimps [pnat_le_iff_Rep_pnat_le,
     1.7 -                                     le_eq_less_or_eq]));
     1.8 +				 order_le_less]));
     1.9  qed "pnat_less_mono_imp_le_mono";
    1.10  
    1.11  Goal "!!i j k::pnat. i<=j ==> i + k <= j + k";
     2.1 --- a/src/HOL/Real/PReal.ML	Tue Sep 29 18:13:05 1998 +0200
     2.2 +++ b/src/HOL/Real/PReal.ML	Thu Oct 01 18:18:01 1998 +0200
     2.3 @@ -157,28 +157,6 @@
     2.4        (*** theorems for ordering ***)
     2.5  (* prove introduction and elimination rules for preal_less *)
     2.6  
     2.7 -Goalw [preal_less_def]
     2.8 -      "R1 < (R2::preal) = (Rep_preal(R1) < Rep_preal(R2))";
     2.9 -by (Fast_tac 1);
    2.10 -qed "preal_less_iff";
    2.11 -
    2.12 -Goalw [preal_less_def]
    2.13 -      "!! (R1::preal). R1 < R2 ==> (Rep_preal(R1) < Rep_preal(R2))";
    2.14 -by (Fast_tac  1);
    2.15 -qed "preal_lessI";
    2.16 -
    2.17 -Goalw [preal_less_def]
    2.18 -      "R1 < (R2::preal) --> (Rep_preal(R1) < Rep_preal(R2))";
    2.19 -by (Fast_tac  1);
    2.20 -qed "preal_lessE_lemma";
    2.21 -
    2.22 -Goal "!!P. [| R1 < (R2::preal); \
    2.23 -\             (Rep_preal(R1) < Rep_preal(R2)) ==> P |] \
    2.24 -\          ==> P";
    2.25 -by (dtac (preal_lessE_lemma RS mp) 1);
    2.26 -by Auto_tac;
    2.27 -qed "preal_lessE";
    2.28 -
    2.29  (* A positive fraction not in a positive real is an upper bound *)
    2.30  (* Gleason p. 122 - Remark (1)                                  *)
    2.31  
    2.32 @@ -806,10 +784,6 @@
    2.33  by Auto_tac;
    2.34  qed "preal_less_or_eq_imp_le";
    2.35  
    2.36 -Goal "(x <= (y::preal)) = (x < y | x=y)";
    2.37 -by (REPEAT(ares_tac [iffI, preal_less_or_eq_imp_le, preal_le_imp_less_or_eq] 1));
    2.38 -qed "preal_le_eq_less_or_eq";
    2.39 -
    2.40  Goalw [preal_le_def] "w <= (w::preal)";
    2.41  by (Simp_tac 1);
    2.42  qed "preal_le_refl";
    2.43 @@ -1037,13 +1011,6 @@
    2.44      simpset() addsimps [preal_add_commute]));
    2.45  qed "preal_add_le_mono1";
    2.46   
    2.47 -Goal "!!k l::preal. [|i<=j;  k<=l |] ==> i + k <= j + l";
    2.48 -by (etac (preal_add_le_mono1 RS preal_le_trans) 1);
    2.49 -by (simp_tac (simpset() addsimps [preal_add_commute]) 1);
    2.50 -(*j moves to the end because it is free while k, l are bound*)
    2.51 -by (etac preal_add_le_mono1 1);
    2.52 -qed "preal_add_le_mono";
    2.53 -
    2.54  Goal "!!(A::preal). A + C < B + C ==> A < B";
    2.55  by (cut_facts_tac [preal_linear] 1);
    2.56  by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
     3.1 --- a/src/HOL/Real/RComplete.ML	Tue Sep 29 18:13:05 1998 +0200
     3.2 +++ b/src/HOL/Real/RComplete.ML	Thu Oct 01 18:18:01 1998 +0200
     3.3 @@ -31,12 +31,12 @@
     3.4  \                 EX u. isUb (UNIV::real set) S u \
     3.5  \              |] ==> EX t. isLub (UNIV::real set) S t";
     3.6  by (res_inst_tac [("x","%#psup({w. %#w : S})")] exI 1);
     3.7 -by (auto_tac (claset(),simpset() addsimps [isLub_def,leastP_def,isUb_def]));
     3.8 +by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def]));
     3.9  by (auto_tac (claset() addSIs [setleI,setgeI] 
    3.10 -    addSDs [real_gt_zero_preal_Ex RS iffD1],simpset()));
    3.11 +	               addSDs [real_gt_zero_preal_Ex RS iffD1],simpset()));
    3.12  by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
    3.13  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
    3.14 -by (auto_tac (claset(),simpset() addsimps [real_preal_le_iff]));
    3.15 +by (auto_tac (claset(), simpset() addsimps [real_preal_le_iff]));
    3.16  by (rtac preal_psup_leI2a 1);
    3.17  by (forw_inst_tac [("y","%#ya")] setleD 1 THEN assume_tac 1);
    3.18  by (forward_tac  [real_ge_preal_preal_Ex] 1);
    3.19 @@ -46,73 +46,48 @@
    3.20  by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
    3.21  by (forward_tac [isUbD2] 1);
    3.22  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
    3.23 -by (auto_tac (claset() addSDs [isUbD,
    3.24 -    real_ge_preal_preal_Ex],simpset() addsimps [real_preal_le_iff]));
    3.25 -by (blast_tac (claset() addSDs [setleD] addSIs 
    3.26 -    [psup_le_ub1] addIs [real_preal_le_iff RS iffD1]) 1);
    3.27 +by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
    3.28 +	      simpset() addsimps [real_preal_le_iff]));
    3.29 +by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] 
    3.30 +	                addIs [real_preal_le_iff RS iffD1]) 1);
    3.31  qed "posreals_complete";
    3.32  
    3.33  
    3.34  (*-------------------------------
    3.35      Lemmas
    3.36   -------------------------------*)
    3.37 -Goal "! y : {z. ? x: P. z = x + %~xa + 1r} Int {x. 0r < x}. 0r < y";
    3.38 +Goal "! y : {z. ? x: P. z = x + -xa + 1r} Int {x. 0r < x}. 0r < y";
    3.39  by Auto_tac;
    3.40  qed "real_sup_lemma3";
    3.41   
    3.42 -(* lemmas re-arranging the terms *)
    3.43 -Goal "(S <= Y + %~X + Z) = (S + X + %~Z <= Y)";
    3.44 -by (Step_tac 1);
    3.45 -by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 1);
    3.46 -by (dres_inst_tac [("x","Z")] real_add_le_mono1 2);
    3.47 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    3.48 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    3.49 -by (dres_inst_tac [("x","X")] real_add_le_mono1 1);
    3.50 -by (dres_inst_tac [("x","%~X")] real_add_le_mono1 2);
    3.51 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    3.52 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    3.53 -by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
    3.54 -qed "lemma_le_swap";
    3.55 -
    3.56 -Goal "(xa <= S + X + %~Z) = (xa + %~X + Z <= S)";
    3.57 -by (Step_tac 1);
    3.58 -by (dres_inst_tac [("x","Z")] real_add_le_mono1 1);
    3.59 -by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 2);
    3.60 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    3.61 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    3.62 -by (dres_inst_tac [("x","%~X")] real_add_le_mono1 1);
    3.63 -by (dres_inst_tac [("x","X")] real_add_le_mono1 2);
    3.64 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    3.65 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    3.66 -by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
    3.67 +Goal "(xa <= S + X + -Z) = (xa + -X + Z <= (S::real))";
    3.68 +by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
    3.69 +	                         real_add_ac) 1);
    3.70  qed "lemma_le_swap2";
    3.71  
    3.72 -Goal "[| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
    3.73 +Goal "[| 0r < x + -X + 1r; x < xa |] ==> 0r < xa + -X + 1r";
    3.74  by (dtac real_add_less_mono 1);
    3.75  by (assume_tac 1);
    3.76 -by (dres_inst_tac [("C","%~x"),("A","0r + x")] real_add_less_mono2 1);
    3.77 +by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1);
    3.78  by (asm_full_simp_tac (simpset() addsimps [real_add_zero_right,
    3.79      real_add_assoc RS sym,real_add_minus_left,real_add_zero_left]) 1);
    3.80  by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
    3.81  qed "lemma_real_complete1";
    3.82  
    3.83 -Goal "!!x. [| x + %~X + 1r <= S; xa < x |] ==> xa + %~X + 1r <= S";
    3.84 +Goal "!!x. [| x + -X + 1r <= S; xa < x |] ==> xa + -X + 1r <= S";
    3.85  by (dtac real_less_imp_le 1);
    3.86  by (dtac real_add_le_mono 1);
    3.87  by (assume_tac 1);
    3.88  by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
    3.89 -by (dres_inst_tac [("x","%~x"),("q2.0","x + S")] real_add_left_le_mono1 1);
    3.90 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
    3.91 -        real_add_minus_left,real_add_zero_left]) 1);
    3.92  qed "lemma_real_complete2";
    3.93  
    3.94 -Goal "[| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
    3.95 +Goal "[| x + -X + 1r <= S; xa < x |] ==> xa <= S + X + -1r"; (**)
    3.96  by (rtac (lemma_le_swap2 RS iffD2) 1);
    3.97  by (etac lemma_real_complete2 1);
    3.98  by (assume_tac 1);
    3.99  qed "lemma_real_complete2a";
   3.100  
   3.101 -Goal "[| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
   3.102 +Goal "[| x + -X + 1r <= S; xa <= x |] ==> xa <= S + X + -1r";
   3.103  by (rotate_tac 1 1);
   3.104  by (etac (real_le_imp_less_or_eq RS disjE) 1);
   3.105  by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
   3.106 @@ -126,20 +101,22 @@
   3.107  \                             EX Y. isUb (UNIV::real set) S Y \
   3.108  \                          |] ==> EX t. isLub (UNIV :: real set) S t";
   3.109  by (Step_tac 1);
   3.110 -by (subgoal_tac "? u. u: {z. ? x: S. z = x + %~X + 1r} \
   3.111 +by (subgoal_tac "? u. u: {z. ? x: S. z = x + -X + 1r} \
   3.112  \                Int {x. 0r < x}" 1);
   3.113 -by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + %~X + 1r} \
   3.114 -\                Int {x. 0r < x})  (Y + %~X + 1r)" 1); 
   3.115 +by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + -X + 1r} \
   3.116 +\                Int {x. 0r < x})  (Y + -X + 1r)" 1); 
   3.117  by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
   3.118  by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, Step_tac]);
   3.119 -by (res_inst_tac [("x","t + X + %~1r")] exI 1);
   3.120 +by (res_inst_tac [("x","t + X + -1r")] exI 1);
   3.121  by (rtac isLubI2 1);
   3.122  by (rtac setgeI 2 THEN Step_tac 2);
   3.123 -by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + %~X + 1r} \
   3.124 -\                Int {x. 0r < x})  (y + %~X + 1r)" 2); 
   3.125 -by (dres_inst_tac [("y","(y + %~ X + 1r)")] isLub_le_isUb 2 
   3.126 +by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + -X + 1r} \
   3.127 +\                Int {x. 0r < x})  (y + -X + 1r)" 2); 
   3.128 +by (dres_inst_tac [("y","(y + - X + 1r)")] isLub_le_isUb 2 
   3.129        THEN assume_tac 2);
   3.130 -by (etac (lemma_le_swap RS subst) 2);
   3.131 +by (full_simp_tac
   3.132 +    (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
   3.133 +                        real_add_ac) 2);
   3.134  by (rtac (setleI RS isUbI) 1);
   3.135  by (Step_tac 1);
   3.136  by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1);
   3.137 @@ -154,27 +131,20 @@
   3.138  by (rtac lemma_real_complete2b 1);
   3.139  by (etac real_less_imp_le 2);
   3.140  by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1);
   3.141 -by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)]
   3.142 -    addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1);
   3.143 -by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)]
   3.144 -    addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1);
   3.145 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc RS sym,
   3.146 -     real_add_minus,real_add_zero_left,real_zero_less_one]));
   3.147 +by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   3.148 +by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
   3.149 +                        addIs [real_add_le_mono1]) 1);
   3.150 +by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
   3.151 +                        addIs [real_add_le_mono1]) 1);
   3.152 +by (auto_tac (claset(),
   3.153 +	      simpset() addsimps [real_add_assoc RS sym,
   3.154 +				  real_zero_less_one]));
   3.155  qed "reals_complete";
   3.156  
   3.157  (*----------------------------------------------------------------
   3.158          Related property: Archimedean property of reals
   3.159   ----------------------------------------------------------------*)
   3.160  
   3.161 -Goal "(ALL m. x*%%#m + x <= t) = (ALL m. x*%%#m <= t + %~x)";
   3.162 -by Auto_tac;
   3.163 -by (ALLGOALS(dres_inst_tac [("x","m")] spec));
   3.164 -by (dres_inst_tac [("x","%~x")] real_add_le_mono1 1);
   3.165 -by (dres_inst_tac [("x","x")] real_add_le_mono1 2);
   3.166 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
   3.167 -      real_add_minus,real_add_minus_left,real_add_zero_right]));
   3.168 -qed "lemma_arch";
   3.169 -
   3.170  Goal "0r < x ==> EX n. rinv(%%#n) < x";
   3.171  by (stac real_nat_rinv_Ex_iff 1);
   3.172  by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
   3.173 @@ -187,15 +157,15 @@
   3.174  by (asm_full_simp_tac (simpset() addsimps 
   3.175     [real_nat_Suc,real_add_mult_distrib2]) 1);
   3.176  by (blast_tac (claset() addIs [isLubD2]) 2);
   3.177 -by (asm_full_simp_tac (simpset() addsimps [lemma_arch]) 1);
   3.178 -by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + %~x)" 1);
   3.179 +by (asm_full_simp_tac
   3.180 +    (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
   3.181 +by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + -x)" 1);
   3.182  by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
   3.183 -by (dres_inst_tac [("y","t+%~x")] isLub_le_isUb 1);
   3.184 -by (dres_inst_tac [("x","%~t")] real_add_left_le_mono1 2);
   3.185 +by (dres_inst_tac [("y","t+-x")] isLub_le_isUb 1);
   3.186 +by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
   3.187  by (auto_tac (claset() addDs [real_le_less_trans,
   3.188 -    (real_minus_zero_less_iff2 RS iffD2)], simpset() 
   3.189 -    addsimps [real_less_not_refl,real_add_assoc RS sym,
   3.190 -    real_add_minus_left,real_add_zero_left]));
   3.191 +			      (real_minus_zero_less_iff2 RS iffD2)], 
   3.192 +	      simpset() addsimps [real_less_not_refl,real_add_assoc RS sym]));
   3.193  qed "reals_Archimedean";
   3.194  
   3.195  Goal "EX n. (x::real) < %%#n";
   3.196 @@ -203,15 +173,17 @@
   3.197  by (res_inst_tac [("x","0")] exI 1);
   3.198  by (res_inst_tac [("x","0")] exI 2);
   3.199  by (auto_tac (claset() addEs [real_less_trans],
   3.200 -    simpset() addsimps [real_nat_one,real_zero_less_one]));
   3.201 +	      simpset() addsimps [real_nat_one,real_zero_less_one]));
   3.202  by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1);
   3.203  by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
   3.204  by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1);
   3.205  by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
   3.206  by (dres_inst_tac [("n1","n"),("y","1r")] 
   3.207       (real_nat_less_zero RS real_mult_less_mono2)  1);
   3.208 -by (auto_tac (claset(),simpset() addsimps [real_nat_less_zero,
   3.209 -    real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
   3.210 +by (auto_tac (claset(),
   3.211 +	      simpset() addsimps [real_nat_less_zero,
   3.212 +				  real_not_refl2 RS not_sym,
   3.213 +				  real_mult_assoc RS sym]));
   3.214  qed "reals_Archimedean2";
   3.215  
   3.216  
     4.1 --- a/src/HOL/Real/ROOT.ML	Tue Sep 29 18:13:05 1998 +0200
     4.2 +++ b/src/HOL/Real/ROOT.ML	Thu Oct 01 18:18:01 1998 +0200
     4.3 @@ -11,5 +11,7 @@
     4.4  writeln"Root file for HOL/Real";
     4.5  
     4.6  set proof_timing;
     4.7 +time_use_thy "RealDef";
     4.8 +use          "simproc";
     4.9  time_use_thy "RealAbs";
    4.10  time_use_thy "RComplete";
     5.1 --- a/src/HOL/Real/Real.ML	Tue Sep 29 18:13:05 1998 +0200
     5.2 +++ b/src/HOL/Real/Real.ML	Thu Oct 01 18:18:01 1998 +0200
     5.3 @@ -1,872 +1,12 @@
     5.4 -(*  Title       : Real.ML
     5.5 -    Author      : Jacques D. Fleuriot
     5.6 -    Copyright   : 1998  University of Cambridge
     5.7 -    Description : The reals
     5.8 +(*  Title:      HOL/Real/Real.ML
     5.9 +    ID:         $Id$
    5.10 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    5.11 +    Copyright   1998  University of Cambridge
    5.12 +
    5.13 +Type "real" is a linear order
    5.14  *)
    5.15  
    5.16 -(*** Proving that realrel is an equivalence relation ***)
    5.17  
    5.18 -Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
    5.19 -\            ==> x1 + y3 = x3 + y1";        
    5.20 -by (res_inst_tac [("C","y2")] preal_add_right_cancel 1);
    5.21 -by (rotate_tac 1 1 THEN dtac sym 1);
    5.22 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
    5.23 -by (rtac (preal_add_left_commute RS subst) 1);
    5.24 -by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1);
    5.25 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
    5.26 -qed "preal_trans_lemma";
    5.27 -
    5.28 -(** Natural deduction for realrel **)
    5.29 -
    5.30 -Goalw [realrel_def]
    5.31 -    "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)";
    5.32 -by (Blast_tac 1);
    5.33 -qed "realrel_iff";
    5.34 -
    5.35 -Goalw [realrel_def]
    5.36 -    "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
    5.37 -by (Blast_tac  1);
    5.38 -qed "realrelI";
    5.39 -
    5.40 -Goalw [realrel_def]
    5.41 -  "p: realrel --> (EX x1 y1 x2 y2. \
    5.42 -\                  p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)";
    5.43 -by (Blast_tac 1);
    5.44 -qed "realrelE_lemma";
    5.45 -
    5.46 -val [major,minor] = goal thy
    5.47 -  "[| p: realrel;  \
    5.48 -\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1 \
    5.49 -\                    |] ==> Q |] ==> Q";
    5.50 -by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1);
    5.51 -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    5.52 -qed "realrelE";
    5.53 -
    5.54 -AddSIs [realrelI];
    5.55 -AddSEs [realrelE];
    5.56 -
    5.57 -Goal "(x,x): realrel";
    5.58 -by (stac surjective_pairing 1 THEN rtac (refl RS realrelI) 1);
    5.59 -qed "realrel_refl";
    5.60 -
    5.61 -Goalw [equiv_def, refl_def, sym_def, trans_def]
    5.62 -    "equiv {x::(preal*preal).True} realrel";
    5.63 -by (fast_tac (claset() addSIs [realrel_refl] 
    5.64 -                      addSEs [sym,preal_trans_lemma]) 1);
    5.65 -qed "equiv_realrel";
    5.66 -
    5.67 -val equiv_realrel_iff =
    5.68 -    [TrueI, TrueI] MRS 
    5.69 -    ([CollectI, CollectI] MRS 
    5.70 -    (equiv_realrel RS eq_equiv_class_iff));
    5.71 -
    5.72 -Goalw  [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
    5.73 -by (Blast_tac 1);
    5.74 -qed "realrel_in_real";
    5.75 -
    5.76 -Goal "inj_on Abs_real real";
    5.77 -by (rtac inj_on_inverseI 1);
    5.78 -by (etac Abs_real_inverse 1);
    5.79 -qed "inj_on_Abs_real";
    5.80 -
    5.81 -Addsimps [equiv_realrel_iff,inj_on_Abs_real RS inj_on_iff,
    5.82 -          realrel_iff, realrel_in_real, Abs_real_inverse];
    5.83 -
    5.84 -Addsimps [equiv_realrel RS eq_equiv_class_iff];
    5.85 -val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class);
    5.86 -
    5.87 -Goal "inj(Rep_real)";
    5.88 -by (rtac inj_inverseI 1);
    5.89 -by (rtac Rep_real_inverse 1);
    5.90 -qed "inj_Rep_real";
    5.91 -
    5.92 -(** real_preal: the injection from preal to real **)
    5.93 -Goal "inj(real_preal)";
    5.94 -by (rtac injI 1);
    5.95 -by (rewtac real_preal_def);
    5.96 -by (dtac (inj_on_Abs_real RS inj_onD) 1);
    5.97 -by (REPEAT (rtac realrel_in_real 1));
    5.98 -by (dtac eq_equiv_class 1);
    5.99 -by (rtac equiv_realrel 1);
   5.100 -by (Blast_tac 1);
   5.101 -by Safe_tac;
   5.102 -by (Asm_full_simp_tac 1);
   5.103 -qed "inj_real_preal";
   5.104 -
   5.105 -val [prem] = goal thy
   5.106 -    "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
   5.107 -by (res_inst_tac [("x1","z")] 
   5.108 -    (rewrite_rule [real_def] Rep_real RS quotientE) 1);
   5.109 -by (dres_inst_tac [("f","Abs_real")] arg_cong 1);
   5.110 -by (res_inst_tac [("p","x")] PairE 1);
   5.111 -by (rtac prem 1);
   5.112 -by (asm_full_simp_tac (simpset() addsimps [Rep_real_inverse]) 1);
   5.113 -qed "eq_Abs_real";
   5.114 -
   5.115 -(**** real_minus: additive inverse on real ****)
   5.116 -
   5.117 -Goalw [congruent_def]
   5.118 -  "congruent realrel (%p. split (%x y. realrel^^{(y,x)}) p)";
   5.119 -by Safe_tac;
   5.120 -by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   5.121 -qed "real_minus_congruent";
   5.122 -
   5.123 -(*Resolve th against the corresponding facts for real_minus*)
   5.124 -val real_minus_ize = RSLIST [equiv_realrel, real_minus_congruent];
   5.125 -
   5.126 -Goalw [real_minus_def]
   5.127 -      "%~ (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})";
   5.128 -by (res_inst_tac [("f","Abs_real")] arg_cong 1);
   5.129 -by (simp_tac (simpset() addsimps 
   5.130 -   [realrel_in_real RS Abs_real_inverse,real_minus_ize UN_equiv_class]) 1);
   5.131 -qed "real_minus";
   5.132 -
   5.133 -Goal "%~ (%~ z) = z";
   5.134 -by (res_inst_tac [("z","z")] eq_Abs_real 1);
   5.135 -by (asm_simp_tac (simpset() addsimps [real_minus]) 1);
   5.136 -qed "real_minus_minus";
   5.137 -
   5.138 -Addsimps [real_minus_minus];
   5.139 -
   5.140 -Goal "inj(real_minus)";
   5.141 -by (rtac injI 1);
   5.142 -by (dres_inst_tac [("f","real_minus")] arg_cong 1);
   5.143 -by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
   5.144 -qed "inj_real_minus";
   5.145 -
   5.146 -Goalw [real_zero_def] "%~0r = 0r";
   5.147 -by (simp_tac (simpset() addsimps [real_minus]) 1);
   5.148 -qed "real_minus_zero";
   5.149 -
   5.150 -Addsimps [real_minus_zero];
   5.151 -
   5.152 -Goal "(%~x = 0r) = (x = 0r)"; 
   5.153 -by (res_inst_tac [("z","x")] eq_Abs_real 1);
   5.154 -by (auto_tac (claset(),simpset() addsimps [real_zero_def,
   5.155 -    real_minus] @ preal_add_ac));
   5.156 -qed "real_minus_zero_iff";
   5.157 -
   5.158 -Addsimps [real_minus_zero_iff];
   5.159 -
   5.160 -Goal "(%~x ~= 0r) = (x ~= 0r)"; 
   5.161 -by Auto_tac;
   5.162 -qed "real_minus_not_zero_iff";
   5.163 -
   5.164 -(*** Congruence property for addition ***)
   5.165 -Goalw [congruent2_def]
   5.166 -    "congruent2 realrel (%p1 p2.                  \
   5.167 -\         split (%x1 y1. split (%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)";
   5.168 -by Safe_tac;
   5.169 -by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
   5.170 -by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
   5.171 -by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   5.172 -by (asm_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.173 -qed "real_add_congruent2";
   5.174 -
   5.175 -(*Resolve th against the corresponding facts for real_add*)
   5.176 -val real_add_ize = RSLIST [equiv_realrel, real_add_congruent2];
   5.177 -
   5.178 -Goalw [real_add_def]
   5.179 -  "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \
   5.180 -\  Abs_real(realrel^^{(x1+x2, y1+y2)})";
   5.181 -by (asm_simp_tac
   5.182 -    (simpset() addsimps [real_add_ize UN_equiv_class2]) 1);
   5.183 -qed "real_add";
   5.184 -
   5.185 -Goal "(z::real) + w = w + z";
   5.186 -by (res_inst_tac [("z","z")] eq_Abs_real 1);
   5.187 -by (res_inst_tac [("z","w")] eq_Abs_real 1);
   5.188 -by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
   5.189 -qed "real_add_commute";
   5.190 -
   5.191 -Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
   5.192 -by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   5.193 -by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   5.194 -by (res_inst_tac [("z","z3")] eq_Abs_real 1);
   5.195 -by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1);
   5.196 -qed "real_add_assoc";
   5.197 -
   5.198 -(*For AC rewriting*)
   5.199 -Goal "(x::real)+(y+z)=y+(x+z)";
   5.200 -by (rtac (real_add_commute RS trans) 1);
   5.201 -by (rtac (real_add_assoc RS trans) 1);
   5.202 -by (rtac (real_add_commute RS arg_cong) 1);
   5.203 -qed "real_add_left_commute";
   5.204 -
   5.205 -(* real addition is an AC operator *)
   5.206 -val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute];
   5.207 -
   5.208 -Goalw [real_preal_def,real_zero_def] "0r + z = z";
   5.209 -by (res_inst_tac [("z","z")] eq_Abs_real 1);
   5.210 -by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
   5.211 -qed "real_add_zero_left";
   5.212 -
   5.213 -Goal "z + 0r = z";
   5.214 -by (simp_tac (simpset() addsimps [real_add_zero_left,real_add_commute]) 1);
   5.215 -qed "real_add_zero_right";
   5.216 -
   5.217 -Goalw [real_zero_def] "z + %~z = 0r";
   5.218 -by (res_inst_tac [("z","z")] eq_Abs_real 1);
   5.219 -by (asm_full_simp_tac (simpset() addsimps [real_minus,
   5.220 -        real_add, preal_add_commute]) 1);
   5.221 -qed "real_add_minus";
   5.222 -
   5.223 -Goal "%~z + z = 0r";
   5.224 -by (simp_tac (simpset() addsimps 
   5.225 -    [real_add_commute,real_add_minus]) 1);
   5.226 -qed "real_add_minus_left";
   5.227 -
   5.228 -Goal "? y. (x::real) + y = 0r";
   5.229 -by (blast_tac (claset() addIs [real_add_minus]) 1);
   5.230 -qed "real_minus_ex";
   5.231 -
   5.232 -Goal "?! y. (x::real) + y = 0r";
   5.233 -by (auto_tac (claset() addIs [real_add_minus],simpset()));
   5.234 -by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   5.235 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   5.236 -by (asm_full_simp_tac (simpset() addsimps [real_add_commute,
   5.237 -    real_add_zero_right,real_add_zero_left]) 1);
   5.238 -qed "real_minus_ex1";
   5.239 -
   5.240 -Goal "?! y. y + (x::real) = 0r";
   5.241 -by (auto_tac (claset() addIs [real_add_minus_left],simpset()));
   5.242 -by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   5.243 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   5.244 -by (asm_full_simp_tac (simpset() addsimps [real_add_commute,
   5.245 -    real_add_zero_right,real_add_zero_left]) 1);
   5.246 -qed "real_minus_left_ex1";
   5.247 -
   5.248 -Goal "x + y = 0r ==> x = %~y";
   5.249 -by (cut_inst_tac [("z","y")] real_add_minus_left 1);
   5.250 -by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
   5.251 -by (Blast_tac 1);
   5.252 -qed "real_add_minus_eq_minus";
   5.253 -
   5.254 -Goal "? y. x = %~y";
   5.255 -by (cut_inst_tac [("x","x")] real_minus_ex 1);
   5.256 -by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
   5.257 -by (Blast_tac 1);
   5.258 -qed "real_as_add_inverse_ex";
   5.259 -
   5.260 -(* real_minus_add_distrib *)
   5.261 -Goal "%~(x + y) = %~x + %~y";
   5.262 -by (res_inst_tac [("z","x")] eq_Abs_real 1);
   5.263 -by (res_inst_tac [("z","y")] eq_Abs_real 1);
   5.264 -by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
   5.265 -qed "real_minus_add_eq";
   5.266 -
   5.267 -val real_minus_add_distrib = real_minus_add_eq;
   5.268 -
   5.269 -Goal "((x::real) + y = x + z) = (y = z)";
   5.270 -by (Step_tac 1);
   5.271 -by (dres_inst_tac [("f","%t.%~x + t")] arg_cong 1);
   5.272 -by (asm_full_simp_tac (simpset() addsimps [real_add_minus_left,
   5.273 -                 real_add_assoc RS sym,real_add_zero_left]) 1);
   5.274 -qed "real_add_left_cancel";
   5.275 -
   5.276 -Goal "(y + (x::real)= z + x) = (y = z)";
   5.277 -by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
   5.278 -qed "real_add_right_cancel";
   5.279 -
   5.280 -(*** Congruence property for multiplication ***)
   5.281 -Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \
   5.282 -\         x * x1 + y * y1 + (x * y2 + x2 * y) = \
   5.283 -\         x * x2 + y * y2 + (x * y1 + x1 * y)";
   5.284 -by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute,
   5.285 -    preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1);
   5.286 -by (rtac (preal_mult_commute RS subst) 1);
   5.287 -by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1);
   5.288 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc,
   5.289 -    preal_add_mult_distrib2 RS sym]) 1);
   5.290 -by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   5.291 -qed "real_mult_congruent2_lemma";
   5.292 -
   5.293 -Goal 
   5.294 -    "congruent2 realrel (%p1 p2.                  \
   5.295 -\         split (%x1 y1. split (%x2 y2. realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
   5.296 -by (rtac (equiv_realrel RS congruent2_commuteI) 1);
   5.297 -by Safe_tac;
   5.298 -by (rewtac split_def);
   5.299 -by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1);
   5.300 -by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
   5.301 -qed "real_mult_congruent2";
   5.302 -
   5.303 -(*Resolve th against the corresponding facts for real_mult*)
   5.304 -val real_mult_ize = RSLIST [equiv_realrel, real_mult_congruent2];
   5.305 -
   5.306 -Goalw [real_mult_def]
   5.307 -   "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) =   \
   5.308 -\   Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})";
   5.309 -by (simp_tac (simpset() addsimps [real_mult_ize UN_equiv_class2]) 1);
   5.310 -qed "real_mult";
   5.311 -
   5.312 -Goal "(z::real) * w = w * z";
   5.313 -by (res_inst_tac [("z","z")] eq_Abs_real 1);
   5.314 -by (res_inst_tac [("z","w")] eq_Abs_real 1);
   5.315 -by (asm_simp_tac
   5.316 -    (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
   5.317 -qed "real_mult_commute";
   5.318 -
   5.319 -Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
   5.320 -by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   5.321 -by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   5.322 -by (res_inst_tac [("z","z3")] eq_Abs_real 1);
   5.323 -by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @ 
   5.324 -                                     preal_add_ac @ preal_mult_ac) 1);
   5.325 -qed "real_mult_assoc";
   5.326 -
   5.327 -qed_goal "real_mult_left_commute" thy
   5.328 -    "(z1::real) * (z2 * z3) = z2 * (z1 * z3)"
   5.329 - (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1,
   5.330 -           rtac (real_mult_commute RS arg_cong) 1]);
   5.331 -
   5.332 -(* real multiplication is an AC operator *)
   5.333 -val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute];
   5.334 -
   5.335 -Goalw [real_one_def,pnat_one_def] "1r * z = z";
   5.336 -by (res_inst_tac [("z","z")] eq_Abs_real 1);
   5.337 -by (asm_full_simp_tac (simpset() addsimps [real_mult,
   5.338 -    preal_add_mult_distrib2,preal_mult_1_right] 
   5.339 -    @ preal_mult_ac @ preal_add_ac) 1);
   5.340 -qed "real_mult_1";
   5.341 -
   5.342 -Goal "z * 1r = z";
   5.343 -by (simp_tac (simpset() addsimps [real_mult_commute,
   5.344 -    real_mult_1]) 1);
   5.345 -qed "real_mult_1_right";
   5.346 -
   5.347 -Goalw [real_zero_def,pnat_one_def] "0r * z = 0r";
   5.348 -by (res_inst_tac [("z","z")] eq_Abs_real 1);
   5.349 -by (asm_full_simp_tac (simpset() addsimps [real_mult,
   5.350 -    preal_add_mult_distrib2,preal_mult_1_right] 
   5.351 -    @ preal_mult_ac @ preal_add_ac) 1);
   5.352 -qed "real_mult_0";
   5.353 -
   5.354 -Goal "z * 0r = 0r";
   5.355 -by (simp_tac (simpset() addsimps [real_mult_commute,
   5.356 -    real_mult_0]) 1);
   5.357 -qed "real_mult_0_right";
   5.358 -
   5.359 -Addsimps [real_mult_0_right,real_mult_0];
   5.360 -
   5.361 -Goal "%~(x * y) = %~x * y";
   5.362 -by (res_inst_tac [("z","x")] eq_Abs_real 1);
   5.363 -by (res_inst_tac [("z","y")] eq_Abs_real 1);
   5.364 -by (auto_tac (claset(),simpset() addsimps [real_minus,real_mult] 
   5.365 -    @ preal_mult_ac @ preal_add_ac));
   5.366 -qed "real_minus_mult_eq1";
   5.367 -
   5.368 -Goal "%~(x * y) = x * %~y";
   5.369 -by (res_inst_tac [("z","x")] eq_Abs_real 1);
   5.370 -by (res_inst_tac [("z","y")] eq_Abs_real 1);
   5.371 -by (auto_tac (claset(),simpset() addsimps [real_minus,real_mult] 
   5.372 -    @ preal_mult_ac @ preal_add_ac));
   5.373 -qed "real_minus_mult_eq2";
   5.374 -
   5.375 -Goal "%~x*%~y = x*y";
   5.376 -by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
   5.377 -    real_minus_mult_eq1 RS sym]) 1);
   5.378 -qed "real_minus_mult_cancel";
   5.379 -
   5.380 -Addsimps [real_minus_mult_cancel];
   5.381 -
   5.382 -Goal "%~x*y = x*%~y";
   5.383 -by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
   5.384 -    real_minus_mult_eq1 RS sym]) 1);
   5.385 -qed "real_minus_mult_commute";
   5.386 -
   5.387 -(*-----------------------------------------------------------------------------
   5.388 -
   5.389 - -----------------------------------------------------------------------------*)
   5.390 -
   5.391 -(** Lemmas **)
   5.392 -
   5.393 -qed_goal "real_add_assoc_cong" thy
   5.394 -    "!!z. (z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   5.395 - (fn _ => [(asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1)]);
   5.396 -
   5.397 -qed_goal "real_add_assoc_swap" thy "(z::real) + (v + w) = v + (z + w)"
   5.398 - (fn _ => [(REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1))]);
   5.399 -
   5.400 -Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)";
   5.401 -by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   5.402 -by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   5.403 -by (res_inst_tac [("z","w")] eq_Abs_real 1);
   5.404 -by (asm_simp_tac 
   5.405 -    (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @ 
   5.406 -                        preal_add_ac @ preal_mult_ac) 1);
   5.407 -qed "real_add_mult_distrib";
   5.408 -
   5.409 -val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute;
   5.410 -
   5.411 -Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)";
   5.412 -by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1);
   5.413 -qed "real_add_mult_distrib2";
   5.414 -
   5.415 -val real_mult_simps = [real_mult_1, real_mult_1_right];
   5.416 -Addsimps real_mult_simps;
   5.417 -
   5.418 -(*** one and zero are distinct ***)
   5.419 -Goalw [real_zero_def,real_one_def] "0r ~= 1r";
   5.420 -by (auto_tac (claset(),simpset() addsimps 
   5.421 -   [preal_self_less_add_left RS preal_not_refl2]));
   5.422 -qed "real_zero_not_eq_one";
   5.423 -
   5.424 -(*** existence of inverse ***)
   5.425 -(** lemma -- alternative definition for 0r **)
   5.426 -Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})";
   5.427 -by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   5.428 -qed "real_zero_iff";
   5.429 -
   5.430 -Goalw [real_zero_def,real_one_def] 
   5.431 -          "!!(x::real). x ~= 0r ==> ? y. x*y = 1r";
   5.432 -by (res_inst_tac [("z","x")] eq_Abs_real 1);
   5.433 -by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
   5.434 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   5.435 -           simpset() addsimps [real_zero_iff RS sym]));
   5.436 -by (res_inst_tac [("x","Abs_real (realrel ^^ {(@#$#1p,pinv(D)+@#$#1p)})")] exI 1);
   5.437 -by (res_inst_tac [("x","Abs_real (realrel ^^ {(pinv(D)+@#$#1p,@#$#1p)})")] exI 2);
   5.438 -by (auto_tac (claset(),simpset() addsimps [real_mult,
   5.439 -    pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2,
   5.440 -    preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right] 
   5.441 -    @ preal_add_ac @ preal_mult_ac));
   5.442 -qed "real_mult_inv_right_ex";
   5.443 -
   5.444 -Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r";
   5.445 -by (asm_simp_tac (simpset() addsimps [real_mult_commute,
   5.446 -    real_mult_inv_right_ex]) 1);
   5.447 -qed "real_mult_inv_left_ex";
   5.448 -
   5.449 -Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r";
   5.450 -by (forward_tac [real_mult_inv_left_ex] 1);
   5.451 -by (Step_tac 1);
   5.452 -by (rtac selectI2 1);
   5.453 -by Auto_tac;
   5.454 -qed "real_mult_inv_left";
   5.455 -
   5.456 -Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r";
   5.457 -by (auto_tac (claset() addIs [real_mult_commute RS subst],
   5.458 -              simpset() addsimps [real_mult_inv_left]));
   5.459 -qed "real_mult_inv_right";
   5.460 -
   5.461 -Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
   5.462 -by Auto_tac;
   5.463 -by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   5.464 -by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   5.465 -qed "real_mult_left_cancel";
   5.466 -    
   5.467 -Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
   5.468 -by (Step_tac 1);
   5.469 -by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   5.470 -by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   5.471 -qed "real_mult_right_cancel";
   5.472 -
   5.473 -Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
   5.474 -by (forward_tac [real_mult_inv_left_ex] 1);
   5.475 -by (etac exE 1);
   5.476 -by (rtac selectI2 1);
   5.477 -by (auto_tac (claset(),simpset() addsimps [real_mult_0,
   5.478 -    real_zero_not_eq_one]));
   5.479 -qed "rinv_not_zero";
   5.480 -
   5.481 -Addsimps [real_mult_inv_left,real_mult_inv_right];
   5.482 -
   5.483 -Goal "x ~= 0r ==> rinv(rinv x) = x";
   5.484 -by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
   5.485 -by (etac rinv_not_zero 1);
   5.486 -by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
   5.487 -qed "real_rinv_rinv";
   5.488 -
   5.489 -Goalw [rinv_def] "rinv(1r) = 1r";
   5.490 -by (cut_facts_tac [real_zero_not_eq_one RS 
   5.491 -       not_sym RS real_mult_inv_left_ex] 1);
   5.492 -by (etac exE 1);
   5.493 -by (rtac selectI2 1);
   5.494 -by (auto_tac (claset(),simpset() addsimps 
   5.495 -    [real_zero_not_eq_one RS not_sym]));
   5.496 -qed "real_rinv_1";
   5.497 -
   5.498 -Goal "x ~= 0r ==> rinv(%~x) = %~rinv(x)";
   5.499 -by (res_inst_tac [("c1","%~x")] (real_mult_right_cancel RS iffD1) 1);
   5.500 -by Auto_tac;
   5.501 -qed "real_minus_rinv";
   5.502 -
   5.503 -      (*** theorems for ordering ***)
   5.504 -(* prove introduction and elimination rules for real_less *)
   5.505 -
   5.506 -Goalw [real_less_def]
   5.507 - "P < (Q::real) = (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
   5.508 -\                                  (x1,y1::preal):Rep_real(P) & \
   5.509 -\                                  (x2,y2):Rep_real(Q))";
   5.510 -by (Blast_tac 1);
   5.511 -qed "real_less_iff";
   5.512 -
   5.513 -Goalw [real_less_def]
   5.514 - "[| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \
   5.515 -\         (x2,y2):Rep_real(Q) |] ==> P < (Q::real)";
   5.516 -by (Blast_tac 1);
   5.517 -qed "real_lessI";
   5.518 -
   5.519 -Goalw [real_less_def]
   5.520 - "!!P. [| R1 < (R2::real); \
   5.521 -\         !!x1 x2 y1 y2. x1 + y2 < x2 + y1 ==> P; \
   5.522 -\         !!x1 y1. (x1,y1::preal):Rep_real(R1) ==> P; \ 
   5.523 -\         !!x2 y2. (x2,y2::preal):Rep_real(R2) ==> P |] \
   5.524 -\     ==> P";
   5.525 -by Auto_tac;
   5.526 -qed "real_lessE";
   5.527 -
   5.528 -Goalw [real_less_def]
   5.529 - "R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
   5.530 -\                                  (x1,y1::preal):Rep_real(R1) & \
   5.531 -\                                  (x2,y2):Rep_real(R2))";
   5.532 -by (Blast_tac 1);
   5.533 -qed "real_lessD";
   5.534 -
   5.535 -(* real_less is a strong order i.e nonreflexive and transitive *)
   5.536 -(*** lemmas ***)
   5.537 -Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y";
   5.538 -by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   5.539 -qed "preal_lemma_eq_rev_sum";
   5.540 -
   5.541 -Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1";
   5.542 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.543 -qed "preal_add_left_commute_cancel";
   5.544 -
   5.545 -Goal 
   5.546 -     "!!(x::preal). [| x + y2a = x2a + y; \
   5.547 -\                      x + y2b = x2b + y |] \
   5.548 -\                   ==> x2a + y2b = x2b + y2a";
   5.549 -by (dtac preal_lemma_eq_rev_sum 1);
   5.550 -by (assume_tac 1);
   5.551 -by (thin_tac "x + y2b = x2b + y" 1);
   5.552 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.553 -by (dtac preal_add_left_commute_cancel 1);
   5.554 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.555 -qed "preal_lemma_for_not_refl";
   5.556 -
   5.557 -Goal "~ (R::real) < R";
   5.558 -by (res_inst_tac [("z","R")] eq_Abs_real 1);
   5.559 -by (auto_tac (claset(),simpset() addsimps [real_less_def]));
   5.560 -by (dtac preal_lemma_for_not_refl 1);
   5.561 -by (assume_tac 1 THEN rotate_tac 2 1);
   5.562 -by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
   5.563 -qed "real_less_not_refl";
   5.564 -
   5.565 -(*** y < y ==> P ***)
   5.566 -bind_thm("real_less_irrefl",real_less_not_refl RS notE);
   5.567 -
   5.568 -Goal "!!(x::real). x < y ==> x ~= y";
   5.569 -by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
   5.570 -qed "real_not_refl2";
   5.571 -
   5.572 -(* lemma re-arranging and eliminating terms *)
   5.573 -Goal "!! (a::preal). [| a + b = c + d; \
   5.574 -\            x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \
   5.575 -\         ==> x2b + y2e < x2e + y2b";
   5.576 -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.577 -by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1);
   5.578 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   5.579 -qed "preal_lemma_trans";
   5.580 -
   5.581 -(** heavy re-writing involved*)
   5.582 -Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   5.583 -by (res_inst_tac [("z","R1")] eq_Abs_real 1);
   5.584 -by (res_inst_tac [("z","R2")] eq_Abs_real 1);
   5.585 -by (res_inst_tac [("z","R3")] eq_Abs_real 1);
   5.586 -by (auto_tac (claset(),simpset() addsimps [real_less_def]));
   5.587 -by (REPEAT(rtac exI 1));
   5.588 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.589 -by (REPEAT(Blast_tac 2));
   5.590 -by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1);
   5.591 -by (blast_tac (claset() addDs [preal_add_less_mono] 
   5.592 -    addIs [preal_lemma_trans]) 1);
   5.593 -qed "real_less_trans";
   5.594 -
   5.595 -Goal "!! (R1::real). [| R1 < R2; R2 < R1 |] ==> P";
   5.596 -by (dtac real_less_trans 1 THEN assume_tac 1);
   5.597 -by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1);
   5.598 -qed "real_less_asym";
   5.599 -
   5.600 -(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
   5.601 -    (****** Map and more real_less ******)
   5.602 -(*** mapping from preal into real ***)
   5.603 -Goalw [real_preal_def] 
   5.604 -            "%#((z1::preal) + z2) = %#z1 + %#z2";
   5.605 -by (asm_simp_tac (simpset() addsimps [real_add,
   5.606 -       preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1);
   5.607 -qed "real_preal_add";
   5.608 -
   5.609 -Goalw [real_preal_def] 
   5.610 -            "%#((z1::preal) * z2) = %#z1* %#z2";
   5.611 -by (full_simp_tac (simpset() addsimps [real_mult,
   5.612 -        preal_add_mult_distrib2,preal_mult_1,
   5.613 -        preal_mult_1_right,pnat_one_def] 
   5.614 -        @ preal_add_ac @ preal_mult_ac) 1);
   5.615 -qed "real_preal_mult";
   5.616 -
   5.617 -Goalw [real_preal_def]
   5.618 -      "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m";
   5.619 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   5.620 -    simpset() addsimps preal_add_ac));
   5.621 -qed "real_preal_ExI";
   5.622 -
   5.623 -Goalw [real_preal_def]
   5.624 -      "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#m ==> y < x";
   5.625 -by (auto_tac (claset(),simpset() addsimps 
   5.626 -    [preal_add_commute,preal_add_assoc]));
   5.627 -by (asm_full_simp_tac (simpset() addsimps 
   5.628 -    [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
   5.629 -qed "real_preal_ExD";
   5.630 -
   5.631 -Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)";
   5.632 -by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1);
   5.633 -qed "real_preal_iff";
   5.634 -
   5.635 -(*** Gleason prop 9-4.4 p 127 ***)
   5.636 -Goalw [real_preal_def,real_zero_def] 
   5.637 -      "? m. (x::real) = %#m | x = 0r | x = %~(%#m)";
   5.638 -by (res_inst_tac [("z","x")] eq_Abs_real 1);
   5.639 -by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
   5.640 -by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
   5.641 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   5.642 -    simpset() addsimps [preal_add_assoc RS sym]));
   5.643 -by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   5.644 -qed "real_preal_trichotomy";
   5.645 -
   5.646 -Goal "!!P. [| !!m. x = %#m ==> P; \
   5.647 -\             x = 0r ==> P; \
   5.648 -\             !!m. x = %~(%#m) ==> P |] ==> P";
   5.649 -by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
   5.650 -by Auto_tac;
   5.651 -qed "real_preal_trichotomyE";
   5.652 -
   5.653 -Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
   5.654 -by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
   5.655 -by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
   5.656 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   5.657 -qed "real_preal_lessD";
   5.658 -
   5.659 -Goal "m1 < m2 ==> %#m1 < %#m2";
   5.660 -by (dtac preal_less_add_left_Ex 1);
   5.661 -by (auto_tac (claset(),simpset() addsimps [real_preal_add,
   5.662 -    real_preal_def,real_less_def]));
   5.663 -by (REPEAT(rtac exI 1));
   5.664 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.665 -by (REPEAT(Blast_tac 2));
   5.666 -by (simp_tac (simpset() addsimps [preal_self_less_add_left] 
   5.667 -    delsimps [preal_add_less_iff2]) 1);
   5.668 -qed "real_preal_lessI";
   5.669 -
   5.670 -Goal "(%#m1 < %#m2) = (m1 < m2)";
   5.671 -by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1);
   5.672 -qed "real_preal_less_iff1";
   5.673 -
   5.674 -Addsimps [real_preal_less_iff1];
   5.675 -
   5.676 -Goal "%~ %#m < %#m";
   5.677 -by (auto_tac (claset(),simpset() addsimps 
   5.678 -    [real_preal_def,real_less_def,real_minus]));
   5.679 -by (REPEAT(rtac exI 1));
   5.680 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.681 -by (REPEAT(Blast_tac 2));
   5.682 -by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.683 -by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   5.684 -    preal_add_assoc RS sym]) 1);
   5.685 -qed "real_preal_minus_less_self";
   5.686 -
   5.687 -Goalw [real_zero_def] "%~ %#m < 0r";
   5.688 -by (auto_tac (claset(),simpset() addsimps 
   5.689 -    [real_preal_def,real_less_def,real_minus]));
   5.690 -by (REPEAT(rtac exI 1));
   5.691 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.692 -by (REPEAT(Blast_tac 2));
   5.693 -by (full_simp_tac (simpset() addsimps 
   5.694 -  [preal_self_less_add_right] @ preal_add_ac) 1);
   5.695 -qed "real_preal_minus_less_zero";
   5.696 -
   5.697 -Goal "~ 0r < %~ %#m";
   5.698 -by (cut_facts_tac [real_preal_minus_less_zero] 1);
   5.699 -by (fast_tac (claset() addDs [real_less_trans] 
   5.700 -                        addEs [real_less_irrefl]) 1);
   5.701 -qed "real_preal_not_minus_gt_zero";
   5.702 -
   5.703 -Goalw [real_zero_def] " 0r < %#m";
   5.704 -by (auto_tac (claset(),simpset() addsimps 
   5.705 -    [real_preal_def,real_less_def,real_minus]));
   5.706 -by (REPEAT(rtac exI 1));
   5.707 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.708 -by (REPEAT(Blast_tac 2));
   5.709 -by (full_simp_tac (simpset() addsimps 
   5.710 -  [preal_self_less_add_right] @ preal_add_ac) 1);
   5.711 -qed "real_preal_zero_less";
   5.712 -
   5.713 -Goal "~ %#m < 0r";
   5.714 -by (cut_facts_tac [real_preal_zero_less] 1);
   5.715 -by (blast_tac (claset() addDs [real_less_trans] 
   5.716 -               addEs [real_less_irrefl]) 1);
   5.717 -qed "real_preal_not_less_zero";
   5.718 -
   5.719 -Goal "0r < %~ %~ %#m";
   5.720 -by (simp_tac (simpset() addsimps 
   5.721 -    [real_preal_zero_less]) 1);
   5.722 -qed "real_minus_minus_zero_less";
   5.723 -
   5.724 -(* another lemma *)
   5.725 -Goalw [real_zero_def] " 0r < %#m + %#m1";
   5.726 -by (auto_tac (claset(),simpset() addsimps 
   5.727 -    [real_preal_def,real_less_def,real_add]));
   5.728 -by (REPEAT(rtac exI 1));
   5.729 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.730 -by (REPEAT(Blast_tac 2));
   5.731 -by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.732 -by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   5.733 -    preal_add_assoc RS sym]) 1);
   5.734 -qed "real_preal_sum_zero_less";
   5.735 -
   5.736 -Goal "%~ %#m < %#m1";
   5.737 -by (auto_tac (claset(),simpset() addsimps 
   5.738 -    [real_preal_def,real_less_def,real_minus]));
   5.739 -by (REPEAT(rtac exI 1));
   5.740 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.741 -by (REPEAT(Blast_tac 2));
   5.742 -by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   5.743 -by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   5.744 -    preal_add_assoc RS sym]) 1);
   5.745 -qed "real_preal_minus_less_all";
   5.746 -
   5.747 -Goal "~ %#m < %~ %#m1";
   5.748 -by (cut_facts_tac [real_preal_minus_less_all] 1);
   5.749 -by (blast_tac (claset() addDs [real_less_trans] 
   5.750 -               addEs [real_less_irrefl]) 1);
   5.751 -qed "real_preal_not_minus_gt_all";
   5.752 -
   5.753 -Goal "%~ %#m1 < %~ %#m2 ==> %#m2 < %#m1";
   5.754 -by (auto_tac (claset(),simpset() addsimps 
   5.755 -    [real_preal_def,real_less_def,real_minus]));
   5.756 -by (REPEAT(rtac exI 1));
   5.757 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.758 -by (REPEAT(Blast_tac 2));
   5.759 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   5.760 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   5.761 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   5.762 -qed "real_preal_minus_less_rev1";
   5.763 -
   5.764 -Goal "%#m1 < %#m2 ==> %~ %#m2 < %~ %#m1";
   5.765 -by (auto_tac (claset(),simpset() addsimps 
   5.766 -    [real_preal_def,real_less_def,real_minus]));
   5.767 -by (REPEAT(rtac exI 1));
   5.768 -by (EVERY[rtac conjI 1, rtac conjI 2]);
   5.769 -by (REPEAT(Blast_tac 2));
   5.770 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   5.771 -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   5.772 -by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   5.773 -qed "real_preal_minus_less_rev2";
   5.774 -
   5.775 -Goal "(%~ %#m1 < %~ %#m2) = (%#m2 < %#m1)";
   5.776 -by (blast_tac (claset() addSIs [real_preal_minus_less_rev1,
   5.777 -               real_preal_minus_less_rev2]) 1);
   5.778 -qed "real_preal_minus_less_rev_iff";
   5.779 -
   5.780 -Addsimps [real_preal_minus_less_rev_iff];
   5.781 -
   5.782 -(*** linearity ***)
   5.783 -Goal "(R1::real) < R2 | R1 = R2 | R2 < R1";
   5.784 -by (res_inst_tac [("x","R1")]  real_preal_trichotomyE 1);
   5.785 -by (ALLGOALS(res_inst_tac [("x","R2")]  real_preal_trichotomyE));
   5.786 -by (auto_tac (claset() addSDs [preal_le_anti_sym],
   5.787 -              simpset() addsimps [preal_less_le_iff,real_preal_minus_less_zero,
   5.788 -               real_preal_zero_less,real_preal_minus_less_all]));
   5.789 -qed "real_linear";
   5.790 -
   5.791 -Goal "!!(R1::real). [| R1 < R2 ==> P;  R1 = R2 ==> P; \
   5.792 -\                      R2 < R1 ==> P |] ==> P";
   5.793 -by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1);
   5.794 -by Auto_tac;
   5.795 -qed "real_linear_less2";
   5.796 -
   5.797 -(*** Properties of <= ***)
   5.798 -
   5.799 -Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
   5.800 -by (assume_tac 1);
   5.801 -qed "real_leI";
   5.802 -
   5.803 -Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
   5.804 -by (assume_tac 1);
   5.805 -qed "real_leD";
   5.806 -
   5.807 -val real_leE = make_elim real_leD;
   5.808 -
   5.809 -Goal "(~(w < z)) = (z <= (w::real))";
   5.810 -by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);
   5.811 -qed "real_less_le_iff";
   5.812 -
   5.813 -Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
   5.814 -by (Blast_tac 1);
   5.815 -qed "not_real_leE";
   5.816 -
   5.817 -Goalw [real_le_def] "z < w ==> z <= (w::real)";
   5.818 -by (blast_tac (claset() addEs [real_less_asym]) 1);
   5.819 -qed "real_less_imp_le";
   5.820 -
   5.821 -Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
   5.822 -by (cut_facts_tac [real_linear] 1);
   5.823 -by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
   5.824 -qed "real_le_imp_less_or_eq";
   5.825 -
   5.826 -Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
   5.827 -by (cut_facts_tac [real_linear] 1);
   5.828 -by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
   5.829 -qed "real_less_or_eq_imp_le";
   5.830 -
   5.831 -Goal "(x <= (y::real)) = (x < y | x=y)";
   5.832 -by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1));
   5.833 -qed "real_le_eq_less_or_eq";
   5.834 -
   5.835 -Goal "w <= (w::real)";
   5.836 -by (simp_tac (simpset() addsimps [real_le_eq_less_or_eq]) 1);
   5.837 -qed "real_le_refl";
   5.838 -
   5.839 -val prems = goal Real.thy "!!i. [| i <= j; j < k |] ==> i < (k::real)";
   5.840 -by (dtac real_le_imp_less_or_eq 1);
   5.841 -by (blast_tac (claset() addIs [real_less_trans]) 1);
   5.842 -qed "real_le_less_trans";
   5.843 -
   5.844 -Goal "!! (i::real). [| i < j; j <= k |] ==> i < k";
   5.845 -by (dtac real_le_imp_less_or_eq 1);
   5.846 -by (blast_tac (claset() addIs [real_less_trans]) 1);
   5.847 -qed "real_less_le_trans";
   5.848 -
   5.849 -Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
   5.850 -by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
   5.851 -            rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]);
   5.852 -qed "real_le_trans";
   5.853 -
   5.854 -Goal "[| z <= w; w <= z |] ==> z = (w::real)";
   5.855 -by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
   5.856 -            fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
   5.857 -qed "real_le_anti_sym";
   5.858 -
   5.859 -Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
   5.860 -by (rtac not_real_leE 1);
   5.861 -by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
   5.862 -qed "not_less_not_eq_real_less";
   5.863 -
   5.864 -Goal "(0r < %~R) = (R < 0r)";
   5.865 -by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   5.866 -by (auto_tac (claset(),simpset() addsimps [real_preal_not_minus_gt_zero,
   5.867 -                        real_preal_not_less_zero,real_preal_zero_less,
   5.868 -                        real_preal_minus_less_zero]));
   5.869 -qed "real_minus_zero_less_iff";
   5.870 -
   5.871 -Addsimps [real_minus_zero_less_iff];
   5.872 -
   5.873 -Goal "(%~R < 0r) = (0r < R)";
   5.874 -by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   5.875 -by (auto_tac (claset(),simpset() addsimps [real_preal_not_minus_gt_zero,
   5.876 -                        real_preal_not_less_zero,real_preal_zero_less,
   5.877 -                        real_preal_minus_less_zero]));
   5.878 -qed "real_minus_zero_less_iff2";
   5.879  
   5.880  (** lemma **)
   5.881  Goal "(0r < x) = (? y. x = %#y)";
   5.882 @@ -896,78 +36,7 @@
   5.883  by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
   5.884  qed "real_less_all_real2";
   5.885  
   5.886 -(**** Derive alternative definition for real_less ****)
   5.887 -(** lemma **)
   5.888 -Goal "!!(R::real). ? A. S + A = R";
   5.889 -by (res_inst_tac [("x","%~S + R")] exI 1);
   5.890 -by (simp_tac (simpset() addsimps [real_add_minus,
   5.891 -    real_add_zero_right] @ real_add_ac) 1);
   5.892 -qed "real_lemma_add_left_ex";
   5.893 -
   5.894 -Goal "!!(R::real). R < S ==> ? T. R + T = S";
   5.895 -by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   5.896 -by (ALLGOALS(res_inst_tac [("x","S")]  real_preal_trichotomyE));
   5.897 -by (auto_tac (claset() addSDs [preal_le_anti_sym] addSDs [preal_less_add_left_Ex],
   5.898 -              simpset() addsimps [preal_less_le_iff,real_preal_add,real_minus_add_eq,
   5.899 -               real_preal_minus_less_zero,real_less_not_refl,real_minus_ex,real_add_assoc,
   5.900 -               real_preal_zero_less,real_preal_minus_less_all,real_add_minus_left,
   5.901 -               real_preal_not_less_zero,real_add_zero_left,real_lemma_add_left_ex]));
   5.902 -qed "real_less_add_left_Ex";
   5.903 -
   5.904 -Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S";
   5.905 -by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   5.906 -by (ALLGOALS(res_inst_tac [("x","S")]  real_preal_trichotomyE));
   5.907 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   5.908 -                         simpset() addsimps [real_preal_not_minus_gt_all,
   5.909 -            real_preal_add, real_preal_not_less_zero,real_less_not_refl,
   5.910 -    real_preal_not_minus_gt_zero,real_add_zero_left,real_minus_add_eq]));
   5.911 -by (res_inst_tac [("x","%#D")] exI 1);
   5.912 -by (res_inst_tac [("x","%#m+%#ma")] exI 2);
   5.913 -by (res_inst_tac [("x","%#m")] exI 3);
   5.914 -by (res_inst_tac [("x","%#D")] exI 4);
   5.915 -by (auto_tac (claset(),simpset() addsimps [real_preal_zero_less,
   5.916 -    real_preal_sum_zero_less,real_add_minus_left,real_add_assoc,
   5.917 -                          real_add_minus,real_add_zero_right]));
   5.918 -by (simp_tac (simpset() addsimps [real_add_assoc RS sym, 
   5.919 -            real_add_minus_left,real_add_zero_left]) 1);
   5.920 -qed "real_less_add_positive_left_Ex";
   5.921 -
   5.922 -(* lemmas *)
   5.923 -(** change naff name(s)! **)
   5.924 -Goal "(W < S) ==> (0r < S + %~W)";
   5.925 -by (dtac real_less_add_positive_left_Ex 1);
   5.926 -by (auto_tac (claset(),simpset() addsimps [real_add_minus,
   5.927 -    real_add_zero_right] @ real_add_ac));
   5.928 -qed "real_less_sum_gt_zero";
   5.929 -
   5.930 -Goal "!!S. T = S + W ==> S = T + %~W";
   5.931 -by (asm_simp_tac (simpset() addsimps [real_add_minus, real_add_zero_right] 
   5.932 -		                     @ real_add_ac) 1);
   5.933 -qed "real_lemma_change_eq_subj";
   5.934 -
   5.935 -(* FIXME: long! *)
   5.936 -Goal "(0r < S + %~W) ==> (W < S)";
   5.937 -by (rtac ccontr 1);
   5.938 -by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
   5.939 -by (auto_tac (claset(),
   5.940 -    simpset() addsimps [real_less_not_refl,real_add_minus]));
   5.941 -by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]);
   5.942 -by (asm_full_simp_tac (simpset() addsimps [real_add_zero_left]) 1);
   5.943 -by (dtac real_lemma_change_eq_subj 1);
   5.944 -by (auto_tac (claset(),simpset() addsimps [real_minus_minus]));
   5.945 -by (dtac real_less_sum_gt_zero 1);
   5.946 -by (asm_full_simp_tac (simpset() addsimps [real_minus_add_eq] @ real_add_ac) 1);
   5.947 -by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]);
   5.948 -by (auto_tac (claset() addEs [real_less_asym],
   5.949 -              simpset() addsimps [real_add_minus,real_add_zero_right]));
   5.950 -qed "real_sum_gt_zero_less";
   5.951 -
   5.952 -Goal "(0r < S + %~W) = (W < S)";
   5.953 -by (blast_tac (claset() addIs [real_less_sum_gt_zero,
   5.954 -    real_sum_gt_zero_less]) 1);
   5.955 -qed "real_less_sum_gt_0_iff";
   5.956 -
   5.957 -Goal "((x::real) < y) = (%~y < %~x)";
   5.958 +Goal "((x::real) < y) = (-y < -x)";
   5.959  by (rtac (real_less_sum_gt_0_iff RS subst) 1);
   5.960  by (res_inst_tac [("W1","x")] (real_less_sum_gt_0_iff RS subst) 1);
   5.961  by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   5.962 @@ -975,42 +44,42 @@
   5.963  
   5.964  Goal "[| R + L = S; 0r < L |] ==> R < S";
   5.965  by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
   5.966 -by (auto_tac (claset(),simpset() addsimps [
   5.967 -    real_add_minus,real_add_zero_right] @ real_add_ac));
   5.968 +by (auto_tac (claset(), simpset() addsimps real_add_ac));
   5.969  qed "real_lemma_add_positive_imp_less";
   5.970  
   5.971  Goal "!!(R::real). ? T. 0r < T & R + T = S ==> R < S";
   5.972  by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1);
   5.973  qed "real_ex_add_positive_left_less";
   5.974  
   5.975 -(*** alternative definition for real_less ***)
   5.976 -Goal "!!(R::real). (? T. 0r < T & R + T = S) = (R < S)";
   5.977 +(*Alternative definition for real_less.  NOT for rewriting*)
   5.978 +Goal "!!(R::real). (R < S) = (? T. 0r < T & R + T = S)";
   5.979  by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex,
   5.980 -    real_ex_add_positive_left_less]) 1);
   5.981 -qed "real_less_iffdef";
   5.982 +				real_ex_add_positive_left_less]) 1);
   5.983 +qed "real_less_iff_add";
   5.984  
   5.985 -Goal "(0r < x) = (%~x < x)";
   5.986 +Goal "(0r < x) = (-x < x)";
   5.987  by Safe_tac;
   5.988  by (rtac ccontr 2 THEN forward_tac 
   5.989      [real_leI RS real_le_imp_less_or_eq] 2);
   5.990  by (Step_tac 2);
   5.991  by (dtac (real_minus_zero_less_iff RS iffD2) 2);
   5.992  by (blast_tac (claset() addIs [real_less_trans]) 2);
   5.993 -by (auto_tac (claset(),simpset() addsimps 
   5.994 -    [real_gt_zero_preal_Ex,real_preal_minus_less_self]));
   5.995 +by (auto_tac (claset(),
   5.996 +	      simpset() addsimps 
   5.997 +	      [real_gt_zero_preal_Ex,real_preal_minus_less_self]));
   5.998  qed "real_gt_zero_iff";
   5.999  
  5.1000 -Goal "(x < 0r) = (x < %~x)";
  5.1001 +Goal "(x < 0r) = (x < -x)";
  5.1002  by (rtac (real_minus_zero_less_iff RS subst) 1);
  5.1003  by (stac real_gt_zero_iff 1);
  5.1004  by (Full_simp_tac 1);
  5.1005  qed "real_lt_zero_iff";
  5.1006  
  5.1007 -Goalw [real_le_def] "(0r <= x) = (%~x <= x)";
  5.1008 +Goalw [real_le_def] "(0r <= x) = (-x <= x)";
  5.1009  by (auto_tac (claset(),simpset() addsimps [real_lt_zero_iff RS sym]));
  5.1010  qed "real_ge_zero_iff";
  5.1011  
  5.1012 -Goalw [real_le_def] "(x <= 0r) = (x <= %~x)";
  5.1013 +Goalw [real_le_def] "(x <= 0r) = (x <= -x)";
  5.1014  by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym]));
  5.1015  qed "real_le_zero_iff";
  5.1016  
  5.1017 @@ -1035,8 +104,8 @@
  5.1018  
  5.1019  Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x * y";
  5.1020  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  5.1021 -by (auto_tac (claset() addIs [real_mult_order,
  5.1022 -    real_less_imp_le],simpset() addsimps [real_le_refl]));
  5.1023 +by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le],
  5.1024 +	      simpset()));
  5.1025  qed "real_le_mult_order";
  5.1026  
  5.1027  Goal "!!(x::real). [| x <= 0r; y <= 0r |] ==> 0r <= x * y";
  5.1028 @@ -1125,93 +194,89 @@
  5.1029  by (Blast_tac 1);
  5.1030  qed "posreal_complete";
  5.1031  
  5.1032 -(*------------------------------------------------------------------
  5.1033 +
  5.1034 +
  5.1035 +(*** Monotonicity results ***)
  5.1036 +
  5.1037 +Goal "(v+z < w+z) = (v < (w::real))";
  5.1038 +by (Simp_tac 1);
  5.1039 +qed "real_add_right_cancel_less";
  5.1040  
  5.1041 - ------------------------------------------------------------------*)
  5.1042 +Goal "(z+v < z+w) = (v < (w::real))";
  5.1043 +by (Simp_tac 1);
  5.1044 +qed "real_add_left_cancel_less";
  5.1045 +
  5.1046 +Addsimps [real_add_right_cancel_less, real_add_left_cancel_less];
  5.1047 +
  5.1048 +Goal "(v+z <= w+z) = (v <= (w::real))";
  5.1049 +by (Simp_tac 1);
  5.1050 +qed "real_add_right_cancel_le";
  5.1051  
  5.1052 -Goal "!!(A::real). A < B ==> A + C < B + C";
  5.1053 -by (dtac (real_less_iffdef RS iffD2) 1);
  5.1054 -by (rtac (real_less_iffdef RS iffD1) 1);
  5.1055 -by (REPEAT(Step_tac 1));
  5.1056 -by (full_simp_tac (simpset() addsimps real_add_ac) 1);
  5.1057 -qed "real_add_less_mono1";
  5.1058 +Goal "(z+v <= z+w) = (v <= (w::real))";
  5.1059 +by (Simp_tac 1);
  5.1060 +qed "real_add_left_cancel_le";
  5.1061 +
  5.1062 +Addsimps [real_add_right_cancel_le, real_add_left_cancel_le];
  5.1063 +
  5.1064 +(*"v<=w ==> v+z <= w+z"*)
  5.1065 +bind_thm ("real_add_less_mono1", real_add_right_cancel_less RS iffD2);
  5.1066 +
  5.1067 +(*"v<=w ==> v+z <= w+z"*)
  5.1068 +bind_thm ("real_add_le_mono1", real_add_right_cancel_le RS iffD2);
  5.1069 +
  5.1070 +Goal "!!z z'::real. [| w'<w; z'<=z |] ==> w' + z' < w + z";
  5.1071 +by (etac (real_add_less_mono1 RS real_less_le_trans) 1);
  5.1072 +by (Simp_tac 1);
  5.1073 +qed "real_add_less_mono";
  5.1074 +
  5.1075  
  5.1076  Goal "!!(A::real). A < B ==> C + A < C + B";
  5.1077 -by (auto_tac (claset() addIs [real_add_less_mono1],
  5.1078 -    simpset() addsimps [real_add_commute]));
  5.1079 +by (Simp_tac 1);
  5.1080  qed "real_add_less_mono2";
  5.1081  
  5.1082  Goal "!!(A::real). A + C < B + C ==> A < B";
  5.1083 -by (dres_inst_tac [("C","%~C")] real_add_less_mono1 1);
  5.1084 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc,
  5.1085 -    real_add_minus,real_add_zero_right]) 1);
  5.1086 +by (Full_simp_tac 1);
  5.1087  qed "real_less_add_right_cancel";
  5.1088  
  5.1089  Goal "!!(A::real). C + A < C + B ==> A < B";
  5.1090 -by (dres_inst_tac [("C","%~C")] real_add_less_mono2 1);
  5.1091 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
  5.1092 -    real_add_minus_left,real_add_zero_left]) 1);
  5.1093 +by (Full_simp_tac 1);
  5.1094  qed "real_less_add_left_cancel";
  5.1095  
  5.1096  Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
  5.1097 -by (REPEAT(dtac (real_gt_zero_preal_Ex RS iffD1) 1));
  5.1098 -by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
  5.1099 -by (Step_tac 1);
  5.1100 -by (res_inst_tac [("x","y + ya")] exI 1);
  5.1101 -by (full_simp_tac (simpset() addsimps [real_preal_add]) 1);
  5.1102 +be real_less_trans 1;
  5.1103 +bd real_add_less_mono2 1;
  5.1104 +by (Full_simp_tac 1);
  5.1105  qed "real_add_order";
  5.1106  
  5.1107  Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x + y";
  5.1108  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  5.1109 -by (auto_tac (claset() addIs [real_add_order,
  5.1110 -    real_less_imp_le],simpset() addsimps [real_add_zero_left,
  5.1111 -    real_add_zero_right,real_le_refl]));
  5.1112 +by (auto_tac (claset() addIs [real_add_order, real_less_imp_le],
  5.1113 +	      simpset()));
  5.1114  qed "real_le_add_order";
  5.1115  
  5.1116 -Goal 
  5.1117 -      "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
  5.1118 -by (dtac (real_less_iffdef RS iffD2) 1);
  5.1119 -by (dtac (real_less_iffdef RS iffD2) 1);
  5.1120 -by (rtac (real_less_iffdef RS iffD1) 1);
  5.1121 -by Auto_tac;
  5.1122 -by (res_inst_tac [("x","T + Ta")] exI 1);
  5.1123 -by (auto_tac (claset(),simpset() addsimps [real_add_order] @ real_add_ac));
  5.1124 +Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
  5.1125 +bd real_add_less_mono1 1;
  5.1126 +be real_less_trans 1;
  5.1127 +be real_add_less_mono2 1;
  5.1128  qed "real_add_less_mono";
  5.1129  
  5.1130 -Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x + y";
  5.1131 -by (REPEAT(dtac real_le_imp_less_or_eq 1));
  5.1132 -by (auto_tac (claset() addIs [real_add_order,
  5.1133 -    real_less_imp_le],simpset() addsimps [real_add_zero_left,
  5.1134 -    real_add_zero_right,real_le_refl]));
  5.1135 -qed "real_le_add_order";
  5.1136 -
  5.1137  Goal "!!(q1::real). q1 <= q2  ==> x + q1 <= x + q2";
  5.1138 -by (dtac real_le_imp_less_or_eq 1);
  5.1139 -by (Step_tac 1);
  5.1140 -by (auto_tac (claset() addSIs [real_le_refl,
  5.1141 -    real_less_imp_le,real_add_less_mono1],
  5.1142 -    simpset() addsimps [real_add_commute]));
  5.1143 +by (Simp_tac 1);
  5.1144  qed "real_add_left_le_mono1";
  5.1145  
  5.1146 -Goal "!!(q1::real). q1 <= q2  ==> q1 + x <= q2 + x";
  5.1147 -by (auto_tac (claset() addDs [real_add_left_le_mono1],
  5.1148 -    simpset() addsimps [real_add_commute]));
  5.1149 -qed "real_add_le_mono1";
  5.1150 -
  5.1151 -Goal "!!k l::real. [|i<=j;  k<=l |] ==> i + k <= j + l";
  5.1152 -by (etac (real_add_le_mono1 RS real_le_trans) 1);
  5.1153 -by (simp_tac (simpset() addsimps [real_add_commute]) 1);
  5.1154 -(*j moves to the end because it is free while k, l are bound*)
  5.1155 -by (etac real_add_le_mono1 1);
  5.1156 +Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::real)";
  5.1157 +bd real_add_le_mono1 1;
  5.1158 +be real_le_trans 1;
  5.1159 +by (Simp_tac 1);
  5.1160  qed "real_add_le_mono";
  5.1161  
  5.1162  Goal "EX (x::real). x < y";
  5.1163  by (rtac (real_add_zero_right RS subst) 1);
  5.1164 -by (res_inst_tac [("x","y + %~1r")] exI 1);
  5.1165 +by (res_inst_tac [("x","y + -1r")] exI 1);
  5.1166  by (auto_tac (claset() addSIs [real_add_less_mono2],
  5.1167 -    simpset() addsimps [real_minus_zero_less_iff2,
  5.1168 -    real_zero_less_one]));
  5.1169 +	  simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
  5.1170  qed "real_less_Ex";
  5.1171 +
  5.1172  (*---------------------------------------------------------------------------------
  5.1173               An embedding of the naturals in the reals
  5.1174   ---------------------------------------------------------------------------------*)
  5.1175 @@ -1267,13 +332,9 @@
  5.1176  Goal "1r <= %%#n";
  5.1177  by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
  5.1178  by (induct_tac "n" 1);
  5.1179 -by (auto_tac (claset(),simpset () 
  5.1180 -    addsimps [real_nat_Suc,real_le_refl,real_nat_one]));
  5.1181 -by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1);
  5.1182 -by (rtac real_add_le_mono 1);
  5.1183 -by (auto_tac (claset(),simpset () 
  5.1184 -    addsimps [real_le_refl,real_nat_less_zero,
  5.1185 -    real_less_imp_le,real_add_zero_left]));
  5.1186 +by (auto_tac (claset(),
  5.1187 +	      simpset () addsimps [real_nat_Suc,real_nat_one,
  5.1188 +				   real_nat_less_zero, real_less_imp_le]));
  5.1189  qed "real_nat_less_one";
  5.1190  
  5.1191  Goal "rinv(%%#n) ~= 0r";
  5.1192 @@ -1318,8 +379,7 @@
  5.1193  Goal "x < x + 1r";
  5.1194  by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
  5.1195  by (full_simp_tac (simpset() addsimps [real_zero_less_one,
  5.1196 -    real_add_assoc,real_add_minus,real_add_zero_right,
  5.1197 -    real_add_left_commute]) 1);
  5.1198 +				real_add_assoc, real_add_left_commute]) 1);
  5.1199  qed "real_self_less_add_one";
  5.1200  
  5.1201  Goal "1r < 1r + 1r";
  5.1202 @@ -1328,7 +388,7 @@
  5.1203  
  5.1204  Goal "0r < 1r + 1r";
  5.1205  by (rtac ([real_zero_less_one,
  5.1206 -          real_one_less_two] MRS real_less_trans) 1);
  5.1207 +	   real_one_less_two] MRS real_less_trans) 1);
  5.1208  qed "real_zero_less_two";
  5.1209  
  5.1210  Goal "1r + 1r ~= 0r";
  5.1211 @@ -1358,7 +418,8 @@
  5.1212  Goal "!!(x::real). [| 0r<z; x*z<y*z |] ==> x<y";
  5.1213  by (forw_inst_tac [("x","x*z")] (real_rinv_gt_zero 
  5.1214                         RS real_mult_less_mono1) 1);
  5.1215 -by (auto_tac (claset(),simpset() addsimps 
  5.1216 +by (auto_tac (claset(),
  5.1217 +	      simpset() addsimps 
  5.1218       [real_mult_assoc,real_not_refl2 RS not_sym]));
  5.1219  qed "real_mult_less_cancel1";
  5.1220  
  5.1221 @@ -1390,7 +451,7 @@
  5.1222  
  5.1223  Goal "!!x y (z::real). [| 0r<=z; x<=y |] ==> z*x<=z*y";
  5.1224  by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
  5.1225 -by (auto_tac (claset() addIs [real_mult_le_less_mono2,real_le_refl],simpset()));
  5.1226 +by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
  5.1227  qed "real_mult_le_le_mono1";
  5.1228  
  5.1229  Goal "!!(x::real). x < y ==> x < (x + y)*rinv(1r + 1r)";
  5.1230 @@ -1402,7 +463,7 @@
  5.1231  qed "real_less_half_sum";
  5.1232  
  5.1233  Goal "!!(x::real). x < y ==> (x + y)*rinv(1r + 1r) < y";
  5.1234 -by (dres_inst_tac [("C","y")] real_add_less_mono1 1);
  5.1235 +by (dtac real_add_less_mono1 1);
  5.1236  by (dtac (real_add_self RS subst) 1);
  5.1237  by (dtac (real_zero_less_two RS real_rinv_gt_zero RS 
  5.1238            real_mult_less_mono1) 1);
  5.1239 @@ -1419,7 +480,8 @@
  5.1240                         RS real_mult_less_mono1) 1);
  5.1241  by (dres_inst_tac [("n2","n")] (real_nat_less_zero RS 
  5.1242          real_rinv_gt_zero RS real_mult_less_mono1) 2);
  5.1243 -by (auto_tac (claset(),simpset() addsimps [(real_nat_less_zero RS 
  5.1244 +by (auto_tac (claset(),
  5.1245 +	      simpset() addsimps [(real_nat_less_zero RS 
  5.1246      real_not_refl2 RS not_sym),real_mult_assoc]));
  5.1247  qed "real_nat_rinv_Ex_iff";
  5.1248  
  5.1249 @@ -1435,17 +497,20 @@
  5.1250      real_rinv_gt_zero RS real_mult_less_cancel1) 1);
  5.1251  by (res_inst_tac [("x1","u")] ( real_rinv_gt_zero
  5.1252     RS real_mult_less_cancel1) 2);
  5.1253 -by (auto_tac (claset(),simpset() addsimps [real_nat_less_zero, 
  5.1254 +by (auto_tac (claset(),
  5.1255 +	      simpset() addsimps [real_nat_less_zero, 
  5.1256      real_not_refl2 RS not_sym]));
  5.1257  by (res_inst_tac [("z","u")] real_mult_less_cancel2 1);
  5.1258  by (res_inst_tac [("n1","n")] (real_nat_less_zero RS 
  5.1259      real_mult_less_cancel2) 3);
  5.1260 -by (auto_tac (claset(),simpset() addsimps [real_nat_less_zero, 
  5.1261 +by (auto_tac (claset(),
  5.1262 +	      simpset() addsimps [real_nat_less_zero, 
  5.1263      real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
  5.1264  qed "real_nat_less_rinv_iff";
  5.1265  
  5.1266  Goal "0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
  5.1267 -by (auto_tac (claset(),simpset() addsimps [real_rinv_rinv,
  5.1268 +by (auto_tac (claset(),
  5.1269 +	      simpset() addsimps [real_rinv_rinv,
  5.1270      real_nat_less_zero,real_not_refl2 RS not_sym]));
  5.1271  qed "real_nat_rinv_eq_iff";
  5.1272  
  5.1273 @@ -1458,3 +523,5 @@
  5.1274  qed "real_ubD";
  5.1275  
  5.1276  *)
  5.1277 +
  5.1278 +
     6.1 --- a/src/HOL/Real/Real.thy	Tue Sep 29 18:13:05 1998 +0200
     6.2 +++ b/src/HOL/Real/Real.thy	Thu Oct 01 18:18:01 1998 +0200
     6.3 @@ -1,61 +1,14 @@
     6.4 -(*  Title       : Real.thy
     6.5 -    Author      : Jacques D. Fleuriot
     6.6 -    Copyright   : 1998  University of Cambridge
     6.7 -    Description : The reals
     6.8 -*) 
     6.9 -
    6.10 -Real = PReal +
    6.11 -
    6.12 -constdefs
    6.13 -    realrel   ::  "((preal * preal) * (preal * preal)) set"
    6.14 -    "realrel  ==  {p. ? x1 y1 x2 y2. p=((x1::preal,y1),(x2,y2)) & x1+y2 = x2+y1}" 
    6.15 -
    6.16 -typedef real = "{x::(preal*preal).True}/realrel"          (Equiv.quotient_def)
    6.17 -
    6.18 -
    6.19 -instance
    6.20 -   real  :: {ord,plus,times}
    6.21 -
    6.22 -consts 
    6.23 -
    6.24 -  "0r"       :: real               ("0r")   
    6.25 -  "1r"       :: real               ("1r")  
    6.26 -
    6.27 -defs
    6.28 -
    6.29 -  real_zero_def      "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})"
    6.30 -  real_one_def       "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})"
    6.31 -
    6.32 -constdefs
    6.33 +(*  Title:      Real/Real.thy
    6.34 +    ID:         $Id$
    6.35 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    6.36 +    Copyright   1998  University of Cambridge
    6.37  
    6.38 -  real_preal :: preal => real              ("%#_" [80] 80)
    6.39 -  "%# m     == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})"
    6.40 -
    6.41 -  real_minus :: real => real               ("%~ _" [80] 80) 
    6.42 -  "%~ R     ==  Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)"
    6.43 -
    6.44 -  rinv       :: real => real
    6.45 -  "rinv(R)   == (@S. R ~= 0r & S*R = 1r)"
    6.46 -
    6.47 -  real_nat :: nat => real                  ("%%# _" [80] 80) 
    6.48 -  "%%# n      == %#(@#($#(*# n)))"
    6.49 -
    6.50 -defs
    6.51 +Type "real" is a linear order
    6.52 +*)
    6.53  
    6.54 -  real_add_def  
    6.55 -  "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
    6.56 -                split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"
    6.57 -  
    6.58 -  real_mult_def  
    6.59 -  "P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
    6.60 -                split(%x1 y1. split(%x2 y2. realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)"
    6.61 +Real = RealDef +
    6.62  
    6.63 -  real_less_def
    6.64 -  "P < (Q::real) == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
    6.65 -                                   (x1,y1::preal):Rep_real(P) &
    6.66 -                                   (x2,y2):Rep_real(Q)" 
    6.67 -
    6.68 -  real_le_def
    6.69 -  "P <= (Q::real) == ~(Q < P)"
    6.70 +instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
    6.71 +instance real :: linorder (real_le_linear)
    6.72  
    6.73  end
     7.1 --- a/src/HOL/Real/RealAbs.ML	Tue Sep 29 18:13:05 1998 +0200
     7.2 +++ b/src/HOL/Real/RealAbs.ML	Thu Oct 01 18:18:01 1998 +0200
     7.3 @@ -4,13 +4,11 @@
     7.4      Description : Absolute value function for the reals
     7.5  *) 
     7.6  
     7.7 -open RealAbs;
     7.8 -
     7.9  (*----------------------------------------------------------------------------
    7.10         Properties of the absolute value function over the reals
    7.11         (adapted version of previously proved theorems about abs)
    7.12   ----------------------------------------------------------------------------*)
    7.13 -Goalw [rabs_def] "rabs r = (if 0r<=r then r else %~r)";
    7.14 +Goalw [rabs_def] "rabs r = (if 0r<=r then r else -r)";
    7.15  by Auto_tac;
    7.16  qed "rabs_iff";
    7.17  
    7.18 @@ -20,7 +18,7 @@
    7.19  
    7.20  Addsimps [rabs_zero];
    7.21  
    7.22 -Goalw [rabs_def] "rabs 0r = %~0r";
    7.23 +Goalw [rabs_def] "rabs 0r = -0r";
    7.24  by (stac real_minus_zero 1);
    7.25  by (rtac if_cancel 1);
    7.26  qed "rabs_minus_zero";
    7.27 @@ -33,19 +31,19 @@
    7.28  by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1);
    7.29  qed "rabs_eqI2";
    7.30  
    7.31 -val [prem] = goalw thy [rabs_def,real_le_def] "x<0r ==> rabs x = %~x";
    7.32 +val [prem] = goalw thy [rabs_def,real_le_def] "x<0r ==> rabs x = -x";
    7.33  by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
    7.34  qed "rabs_minus_eqI2";
    7.35  
    7.36 -Goal "x<=0r ==> rabs x = %~x";
    7.37 +Goal "x<=0r ==> rabs x = -x";
    7.38  by (dtac real_le_imp_less_or_eq 1);
    7.39  by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
    7.40  qed "rabs_minus_eqI1";
    7.41  
    7.42  Goalw [rabs_def,real_le_def] "0r<= rabs x";
    7.43 -by (full_simp_tac (simpset()  setloop (split_tac [expand_if])) 1);
    7.44 +by (Full_simp_tac 1);
    7.45  by (blast_tac (claset() addDs [real_minus_zero_less_iff RS iffD2,
    7.46 -    real_less_asym]) 1);
    7.47 +			       real_less_asym]) 1);
    7.48  qed "rabs_ge_zero";
    7.49  
    7.50  Goal "rabs(rabs x)=rabs x";
    7.51 @@ -54,29 +52,27 @@
    7.52  qed "rabs_idempotent";
    7.53  
    7.54  Goalw [rabs_def] "(x=0r) = (rabs x = 0r)";
    7.55 -by (full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
    7.56 +by (Full_simp_tac 1);
    7.57  qed "rabs_zero_iff";
    7.58  
    7.59  Goal  "(x ~= 0r) = (rabs x ~= 0r)";
    7.60 -by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym] 
    7.61 -    setloop (split_tac [expand_if])) 1);
    7.62 +by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym]) 1);
    7.63  qed "rabs_not_zero_iff";
    7.64  
    7.65  Goalw [rabs_def] "x<=rabs x";
    7.66 -by (full_simp_tac (simpset() addsimps [real_le_refl] setloop (split_tac [expand_if])) 1);
    7.67 +by (Full_simp_tac 1);
    7.68  by (auto_tac (claset() addDs [not_real_leE RS real_less_imp_le],
    7.69 -    simpset() addsimps [real_le_zero_iff]));
    7.70 +	      simpset() addsimps [real_le_zero_iff]));
    7.71  qed "rabs_ge_self";
    7.72  
    7.73 -Goalw [rabs_def] "%~x<=rabs x";
    7.74 -by (full_simp_tac (simpset() addsimps [real_le_refl,
    7.75 -    real_ge_zero_iff] setloop (split_tac [expand_if])) 1);
    7.76 +Goalw [rabs_def] "-x<=rabs x";
    7.77 +by (full_simp_tac (simpset() addsimps [real_ge_zero_iff]) 1);
    7.78  qed "rabs_ge_minus_self";
    7.79  
    7.80  (* case splits nightmare *)
    7.81  Goalw [rabs_def] "rabs(x*y) = (rabs x)*(rabs y)";
    7.82  by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1,
    7.83 -   real_minus_mult_commute,real_minus_mult_eq2] setloop (split_tac [expand_if])));
    7.84 +   real_minus_mult_commute,real_minus_mult_eq2]));
    7.85  by (blast_tac (claset() addDs [real_le_mult_order]) 1);
    7.86  by (auto_tac (claset() addSDs [not_real_leE],simpset()));
    7.87  by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]);
    7.88 @@ -88,7 +84,7 @@
    7.89  
    7.90  Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
    7.91  by (auto_tac (claset(),simpset() addsimps [real_minus_rinv] 
    7.92 -    setloop (split_tac [expand_if])));
    7.93 +   ));
    7.94  by (ALLGOALS(dtac not_real_leE));
    7.95  by (etac real_less_asym 1);
    7.96  by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
    7.97 @@ -108,28 +104,30 @@
    7.98  
    7.99  Goal "rabs(x+y) <= rabs x + rabs y";
   7.100  by (EVERY1 [res_inst_tac [("Q1","0r<=x+y")] (expand_if RS ssubst), rtac conjI]);
   7.101 -by (asm_simp_tac (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1);
   7.102 -by (asm_simp_tac (simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono,
   7.103 -                                     rabs_ge_minus_self,real_minus_add_eq]) 1);
   7.104 +by (asm_simp_tac
   7.105 +    (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1);
   7.106 +by (asm_simp_tac 
   7.107 +    (simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono,
   7.108 +			 rabs_ge_minus_self]) 1);
   7.109  qed "rabs_triangle_ineq";
   7.110  
   7.111  Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)";
   7.112  by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   7.113  by (blast_tac (claset() addSIs [(rabs_triangle_ineq RS real_le_trans),
   7.114 -                real_add_left_le_mono1,real_le_refl]) 1);
   7.115 +				real_add_left_le_mono1]) 1);
   7.116  qed "rabs_triangle_ineq_four";
   7.117  
   7.118 -Goalw [rabs_def] "rabs(%~x)=rabs(x)";
   7.119 +Goalw [rabs_def] "rabs(-x)=rabs(x)";
   7.120  by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] addIs [real_le_anti_sym],
   7.121 -   simpset() addsimps [real_ge_zero_iff] setloop (split_tac [expand_if])));
   7.122 +   simpset() addsimps [real_ge_zero_iff]));
   7.123  qed "rabs_minus_cancel";
   7.124  
   7.125 -Goal "rabs(x + %~y) <= rabs x + rabs y";
   7.126 +Goal "rabs(x + -y) <= rabs x + rabs y";
   7.127  by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1);
   7.128  by (rtac rabs_triangle_ineq 1);
   7.129  qed "rabs_triangle_minus_ineq";
   7.130  
   7.131 -Goal "rabs (x + y + (%~l + %~m)) <= rabs(x + %~l) + rabs(y + %~m)";
   7.132 +Goal "rabs (x + y + (-l + -m)) <= rabs(x + -l) + rabs(y + -m)";
   7.133  by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   7.134  by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
   7.135  by (rtac (real_add_assoc RS subst) 1);
   7.136 @@ -142,7 +140,7 @@
   7.137  by (REPEAT (ares_tac [real_add_less_mono] 1));
   7.138  qed "rabs_add_less";
   7.139  
   7.140 -Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s";
   7.141 +Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ -y) < r+s";
   7.142  by (rotate_tac 1 1);
   7.143  by (dtac (rabs_minus_cancel RS ssubst) 1);
   7.144  by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
   7.145 @@ -176,8 +174,7 @@
   7.146  			     real_le_less_trans]) 1);
   7.147  qed "rabs_mult_less";
   7.148  
   7.149 -Goal "[| rabs x < r; rabs y < s |] \
   7.150 -\          ==> rabs(x)*rabs(y)<r*s";
   7.151 +Goal "[| rabs x < r; rabs y < s |] ==> rabs(x)*rabs(y)<r*s";
   7.152  by (auto_tac (claset() addIs [rabs_mult_less],
   7.153                simpset() addsimps [rabs_mult RS sym]));
   7.154  qed "rabs_mult_less2";
   7.155 @@ -186,13 +183,13 @@
   7.156  by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1);
   7.157  by (EVERY1[etac disjE,rtac real_less_imp_le]);
   7.158  by (dres_inst_tac [("W","1r")]  real_less_sum_gt_zero 1);
   7.159 -by (forw_inst_tac [("y","rabs x + %~1r")] real_mult_order 1);
   7.160 +by (forw_inst_tac [("y","rabs x + -1r")] real_mult_order 1);
   7.161  by (assume_tac 1);
   7.162  by (rtac real_sum_gt_zero_less 1);
   7.163  by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
   7.164 -    rabs_mult, real_mult_commute,real_minus_mult_eq1 RS sym]) 1);
   7.165 +    real_mult_commute, rabs_mult]) 1);
   7.166  by (dtac sym 1);
   7.167 -by (asm_full_simp_tac (simpset() addsimps [real_le_refl,rabs_mult]) 1);
   7.168 +by (asm_full_simp_tac (simpset() addsimps [rabs_mult]) 1);
   7.169  qed "rabs_mult_le";
   7.170  
   7.171  Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
   7.172 @@ -205,27 +202,27 @@
   7.173  
   7.174  Goalw [rabs_def] "rabs 1r = 1r";
   7.175  by (auto_tac (claset() addSDs [not_real_leE RS real_less_asym],
   7.176 -   simpset() addsimps [real_zero_less_one] setloop (split_tac [expand_if])));
   7.177 +   simpset() addsimps [real_zero_less_one]));
   7.178  qed "rabs_one";
   7.179  
   7.180  Goal "[| 0r < x ; x < r |] ==> rabs x < r";
   7.181  by (asm_simp_tac (simpset() addsimps [rabs_eqI2]) 1);
   7.182  qed "rabs_lessI";
   7.183  
   7.184 -Goal "rabs x =x | rabs x = %~x";
   7.185 +Goal "rabs x =x | rabs x = -x";
   7.186  by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1);
   7.187  by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2,
   7.188                              rabs_zero,rabs_minus_zero]) 1);
   7.189  qed "rabs_disj";
   7.190  
   7.191 -Goal "rabs x = y ==> x = y | %~x = y";
   7.192 +Goal "rabs x = y ==> x = y | -x = y";
   7.193  by (dtac sym 1);
   7.194  by (hyp_subst_tac 1);
   7.195  by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1);
   7.196  by (REPEAT(Asm_simp_tac 1));
   7.197  qed "rabs_eq_disj";
   7.198  
   7.199 -Goal "(rabs x < r) = (%~r<x & x<r)";
   7.200 +Goal "(rabs x < r) = (-r<x & x<r)";
   7.201  by Safe_tac;
   7.202  by (rtac (real_less_swap_iff RS iffD2) 1);
   7.203  by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self 
     8.1 --- a/src/HOL/Real/RealAbs.thy	Tue Sep 29 18:13:05 1998 +0200
     8.2 +++ b/src/HOL/Real/RealAbs.thy	Thu Oct 01 18:18:01 1998 +0200
     8.3 @@ -8,6 +8,6 @@
     8.4  
     8.5  constdefs
     8.6     rabs   :: real => real
     8.7 -   "rabs r      == if 0r<=r then r else %~r" 
     8.8 +   "rabs r      == if 0r<=r then r else -r" 
     8.9  
    8.10  end
    8.11 \ No newline at end of file
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Real/RealDef.ML	Thu Oct 01 18:18:01 1998 +0200
     9.3 @@ -0,0 +1,1042 @@
     9.4 +(*  Title       : Real/RealDef.ML
     9.5 +    Author      : Jacques D. Fleuriot
     9.6 +    Copyright   : 1998  University of Cambridge
     9.7 +    Description : The reals
     9.8 +*)
     9.9 +
    9.10 +(*** Proving that realrel is an equivalence relation ***)
    9.11 +
    9.12 +Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
    9.13 +\            ==> x1 + y3 = x3 + y1";        
    9.14 +by (res_inst_tac [("C","y2")] preal_add_right_cancel 1);
    9.15 +by (rotate_tac 1 1 THEN dtac sym 1);
    9.16 +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
    9.17 +by (rtac (preal_add_left_commute RS subst) 1);
    9.18 +by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1);
    9.19 +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
    9.20 +qed "preal_trans_lemma";
    9.21 +
    9.22 +(** Natural deduction for realrel **)
    9.23 +
    9.24 +Goalw [realrel_def]
    9.25 +    "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)";
    9.26 +by (Blast_tac 1);
    9.27 +qed "realrel_iff";
    9.28 +
    9.29 +Goalw [realrel_def]
    9.30 +    "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
    9.31 +by (Blast_tac  1);
    9.32 +qed "realrelI";
    9.33 +
    9.34 +Goalw [realrel_def]
    9.35 +  "p: realrel --> (EX x1 y1 x2 y2. \
    9.36 +\                  p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)";
    9.37 +by (Blast_tac 1);
    9.38 +qed "realrelE_lemma";
    9.39 +
    9.40 +val [major,minor] = goal thy
    9.41 +  "[| p: realrel;  \
    9.42 +\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1 \
    9.43 +\                    |] ==> Q |] ==> Q";
    9.44 +by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1);
    9.45 +by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    9.46 +qed "realrelE";
    9.47 +
    9.48 +AddSIs [realrelI];
    9.49 +AddSEs [realrelE];
    9.50 +
    9.51 +Goal "(x,x): realrel";
    9.52 +by (stac surjective_pairing 1 THEN rtac (refl RS realrelI) 1);
    9.53 +qed "realrel_refl";
    9.54 +
    9.55 +Goalw [equiv_def, refl_def, sym_def, trans_def]
    9.56 +    "equiv {x::(preal*preal).True} realrel";
    9.57 +by (fast_tac (claset() addSIs [realrel_refl] 
    9.58 +                      addSEs [sym,preal_trans_lemma]) 1);
    9.59 +qed "equiv_realrel";
    9.60 +
    9.61 +val equiv_realrel_iff =
    9.62 +    [TrueI, TrueI] MRS 
    9.63 +    ([CollectI, CollectI] MRS 
    9.64 +    (equiv_realrel RS eq_equiv_class_iff));
    9.65 +
    9.66 +Goalw  [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
    9.67 +by (Blast_tac 1);
    9.68 +qed "realrel_in_real";
    9.69 +
    9.70 +Goal "inj_on Abs_real real";
    9.71 +by (rtac inj_on_inverseI 1);
    9.72 +by (etac Abs_real_inverse 1);
    9.73 +qed "inj_on_Abs_real";
    9.74 +
    9.75 +Addsimps [equiv_realrel_iff,inj_on_Abs_real RS inj_on_iff,
    9.76 +          realrel_iff, realrel_in_real, Abs_real_inverse];
    9.77 +
    9.78 +Addsimps [equiv_realrel RS eq_equiv_class_iff];
    9.79 +val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class);
    9.80 +
    9.81 +Goal "inj(Rep_real)";
    9.82 +by (rtac inj_inverseI 1);
    9.83 +by (rtac Rep_real_inverse 1);
    9.84 +qed "inj_Rep_real";
    9.85 +
    9.86 +(** real_preal: the injection from preal to real **)
    9.87 +Goal "inj(real_preal)";
    9.88 +by (rtac injI 1);
    9.89 +by (rewtac real_preal_def);
    9.90 +by (dtac (inj_on_Abs_real RS inj_onD) 1);
    9.91 +by (REPEAT (rtac realrel_in_real 1));
    9.92 +by (dtac eq_equiv_class 1);
    9.93 +by (rtac equiv_realrel 1);
    9.94 +by (Blast_tac 1);
    9.95 +by Safe_tac;
    9.96 +by (Asm_full_simp_tac 1);
    9.97 +qed "inj_real_preal";
    9.98 +
    9.99 +val [prem] = goal thy
   9.100 +    "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
   9.101 +by (res_inst_tac [("x1","z")] 
   9.102 +    (rewrite_rule [real_def] Rep_real RS quotientE) 1);
   9.103 +by (dres_inst_tac [("f","Abs_real")] arg_cong 1);
   9.104 +by (res_inst_tac [("p","x")] PairE 1);
   9.105 +by (rtac prem 1);
   9.106 +by (asm_full_simp_tac (simpset() addsimps [Rep_real_inverse]) 1);
   9.107 +qed "eq_Abs_real";
   9.108 +
   9.109 +(**** real_minus: additive inverse on real ****)
   9.110 +
   9.111 +Goalw [congruent_def]
   9.112 +  "congruent realrel (%p. split (%x y. realrel^^{(y,x)}) p)";
   9.113 +by Safe_tac;
   9.114 +by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   9.115 +qed "real_minus_congruent";
   9.116 +
   9.117 +(*Resolve th against the corresponding facts for real_minus*)
   9.118 +val real_minus_ize = RSLIST [equiv_realrel, real_minus_congruent];
   9.119 +
   9.120 +Goalw [real_minus_def]
   9.121 +      "- (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})";
   9.122 +by (res_inst_tac [("f","Abs_real")] arg_cong 1);
   9.123 +by (simp_tac (simpset() addsimps 
   9.124 +   [realrel_in_real RS Abs_real_inverse,real_minus_ize UN_equiv_class]) 1);
   9.125 +qed "real_minus";
   9.126 +
   9.127 +Goal "- (- z) = (z::real)";
   9.128 +by (res_inst_tac [("z","z")] eq_Abs_real 1);
   9.129 +by (asm_simp_tac (simpset() addsimps [real_minus]) 1);
   9.130 +qed "real_minus_minus";
   9.131 +
   9.132 +Addsimps [real_minus_minus];
   9.133 +
   9.134 +Goal "inj(%r::real. -r)";
   9.135 +by (rtac injI 1);
   9.136 +by (dres_inst_tac [("f","uminus")] arg_cong 1);
   9.137 +by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
   9.138 +qed "inj_real_minus";
   9.139 +
   9.140 +Goalw [real_zero_def] "-0r = 0r";
   9.141 +by (simp_tac (simpset() addsimps [real_minus]) 1);
   9.142 +qed "real_minus_zero";
   9.143 +
   9.144 +Addsimps [real_minus_zero];
   9.145 +
   9.146 +Goal "(-x = 0r) = (x = 0r)"; 
   9.147 +by (res_inst_tac [("z","x")] eq_Abs_real 1);
   9.148 +by (auto_tac (claset(),
   9.149 +	      simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac));
   9.150 +qed "real_minus_zero_iff";
   9.151 +
   9.152 +Addsimps [real_minus_zero_iff];
   9.153 +
   9.154 +Goal "(-x ~= 0r) = (x ~= 0r)"; 
   9.155 +by Auto_tac;
   9.156 +qed "real_minus_not_zero_iff";
   9.157 +
   9.158 +(*** Congruence property for addition ***)
   9.159 +Goalw [congruent2_def]
   9.160 +    "congruent2 realrel (%p1 p2.                  \
   9.161 +\         split (%x1 y1. split (%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)";
   9.162 +by Safe_tac;
   9.163 +by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
   9.164 +by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
   9.165 +by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   9.166 +by (asm_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.167 +qed "real_add_congruent2";
   9.168 +
   9.169 +(*Resolve th against the corresponding facts for real_add*)
   9.170 +val real_add_ize = RSLIST [equiv_realrel, real_add_congruent2];
   9.171 +
   9.172 +Goalw [real_add_def]
   9.173 +  "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \
   9.174 +\  Abs_real(realrel^^{(x1+x2, y1+y2)})";
   9.175 +by (asm_simp_tac (simpset() addsimps [real_add_ize UN_equiv_class2]) 1);
   9.176 +qed "real_add";
   9.177 +
   9.178 +Goal "(z::real) + w = w + z";
   9.179 +by (res_inst_tac [("z","z")] eq_Abs_real 1);
   9.180 +by (res_inst_tac [("z","w")] eq_Abs_real 1);
   9.181 +by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
   9.182 +qed "real_add_commute";
   9.183 +
   9.184 +Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
   9.185 +by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   9.186 +by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   9.187 +by (res_inst_tac [("z","z3")] eq_Abs_real 1);
   9.188 +by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1);
   9.189 +qed "real_add_assoc";
   9.190 +
   9.191 +(*For AC rewriting*)
   9.192 +Goal "(x::real)+(y+z)=y+(x+z)";
   9.193 +by (rtac (real_add_commute RS trans) 1);
   9.194 +by (rtac (real_add_assoc RS trans) 1);
   9.195 +by (rtac (real_add_commute RS arg_cong) 1);
   9.196 +qed "real_add_left_commute";
   9.197 +
   9.198 +(* real addition is an AC operator *)
   9.199 +val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute];
   9.200 +
   9.201 +Goalw [real_preal_def,real_zero_def] "0r + z = z";
   9.202 +by (res_inst_tac [("z","z")] eq_Abs_real 1);
   9.203 +by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
   9.204 +qed "real_add_zero_left";
   9.205 +Addsimps [real_add_zero_left];
   9.206 +
   9.207 +Goal "z + 0r = z";
   9.208 +by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   9.209 +qed "real_add_zero_right";
   9.210 +Addsimps [real_add_zero_right];
   9.211 +
   9.212 +Goalw [real_zero_def] "z + -z = 0r";
   9.213 +by (res_inst_tac [("z","z")] eq_Abs_real 1);
   9.214 +by (asm_full_simp_tac (simpset() addsimps [real_minus,
   9.215 +        real_add, preal_add_commute]) 1);
   9.216 +qed "real_add_minus";
   9.217 +Addsimps [real_add_minus];
   9.218 +
   9.219 +Goal "-z + z = 0r";
   9.220 +by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   9.221 +qed "real_add_minus_left";
   9.222 +Addsimps [real_add_minus_left];
   9.223 +
   9.224 +
   9.225 +Goal "z + (- z + w) = (w::real)";
   9.226 +by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   9.227 +qed "real_add_minus_cancel";
   9.228 +
   9.229 +Goal "(-z) + (z + w) = (w::real)";
   9.230 +by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   9.231 +qed "real_minus_add_cancel";
   9.232 +
   9.233 +Addsimps [real_add_minus_cancel, real_minus_add_cancel];
   9.234 +
   9.235 +Goal "? y. (x::real) + y = 0r";
   9.236 +by (blast_tac (claset() addIs [real_add_minus]) 1);
   9.237 +qed "real_minus_ex";
   9.238 +
   9.239 +Goal "?! y. (x::real) + y = 0r";
   9.240 +by (auto_tac (claset() addIs [real_add_minus],simpset()));
   9.241 +by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   9.242 +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   9.243 +by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   9.244 +qed "real_minus_ex1";
   9.245 +
   9.246 +Goal "?! y. y + (x::real) = 0r";
   9.247 +by (auto_tac (claset() addIs [real_add_minus_left],simpset()));
   9.248 +by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   9.249 +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   9.250 +by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   9.251 +qed "real_minus_left_ex1";
   9.252 +
   9.253 +Goal "x + y = 0r ==> x = -y";
   9.254 +by (cut_inst_tac [("z","y")] real_add_minus_left 1);
   9.255 +by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
   9.256 +by (Blast_tac 1);
   9.257 +qed "real_add_minus_eq_minus";
   9.258 +
   9.259 +Goal "-(x + y) = -x + -(y::real)";
   9.260 +by (res_inst_tac [("z","x")] eq_Abs_real 1);
   9.261 +by (res_inst_tac [("z","y")] eq_Abs_real 1);
   9.262 +by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
   9.263 +qed "real_minus_add_distrib";
   9.264 +
   9.265 +Addsimps [real_minus_add_distrib];
   9.266 +
   9.267 +Goal "((x::real) + y = x + z) = (y = z)";
   9.268 +by (Step_tac 1);
   9.269 +by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   9.270 +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   9.271 +qed "real_add_left_cancel";
   9.272 +
   9.273 +Goal "(y + (x::real)= z + x) = (y = z)";
   9.274 +by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
   9.275 +qed "real_add_right_cancel";
   9.276 +
   9.277 +Goal "0r - x = -x";
   9.278 +by (simp_tac (simpset() addsimps [real_diff_def]) 1);
   9.279 +qed "real_diff_0";
   9.280 +
   9.281 +Goal "x - 0r = x";
   9.282 +by (simp_tac (simpset() addsimps [real_diff_def]) 1);
   9.283 +qed "real_diff_0_right";
   9.284 +
   9.285 +Goal "x - x = 0r";
   9.286 +by (simp_tac (simpset() addsimps [real_diff_def]) 1);
   9.287 +qed "real_diff_self";
   9.288 +
   9.289 +Addsimps [real_diff_0, real_diff_0_right, real_diff_self];
   9.290 +
   9.291 +
   9.292 +(*** Congruence property for multiplication ***)
   9.293 +
   9.294 +Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \
   9.295 +\         x * x1 + y * y1 + (x * y2 + x2 * y) = \
   9.296 +\         x * x2 + y * y2 + (x * y1 + x1 * y)";
   9.297 +by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute,
   9.298 +    preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1);
   9.299 +by (rtac (preal_mult_commute RS subst) 1);
   9.300 +by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1);
   9.301 +by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc,
   9.302 +    preal_add_mult_distrib2 RS sym]) 1);
   9.303 +by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   9.304 +qed "real_mult_congruent2_lemma";
   9.305 +
   9.306 +Goal 
   9.307 +    "congruent2 realrel (%p1 p2.                  \
   9.308 +\         split (%x1 y1. split (%x2 y2. realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
   9.309 +by (rtac (equiv_realrel RS congruent2_commuteI) 1);
   9.310 +by Safe_tac;
   9.311 +by (rewtac split_def);
   9.312 +by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1);
   9.313 +by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
   9.314 +qed "real_mult_congruent2";
   9.315 +
   9.316 +(*Resolve th against the corresponding facts for real_mult*)
   9.317 +val real_mult_ize = RSLIST [equiv_realrel, real_mult_congruent2];
   9.318 +
   9.319 +Goalw [real_mult_def]
   9.320 +   "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) =   \
   9.321 +\   Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})";
   9.322 +by (simp_tac (simpset() addsimps [real_mult_ize UN_equiv_class2]) 1);
   9.323 +qed "real_mult";
   9.324 +
   9.325 +Goal "(z::real) * w = w * z";
   9.326 +by (res_inst_tac [("z","z")] eq_Abs_real 1);
   9.327 +by (res_inst_tac [("z","w")] eq_Abs_real 1);
   9.328 +by (asm_simp_tac
   9.329 +    (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
   9.330 +qed "real_mult_commute";
   9.331 +
   9.332 +Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
   9.333 +by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   9.334 +by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   9.335 +by (res_inst_tac [("z","z3")] eq_Abs_real 1);
   9.336 +by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @ 
   9.337 +                                     preal_add_ac @ preal_mult_ac) 1);
   9.338 +qed "real_mult_assoc";
   9.339 +
   9.340 +qed_goal "real_mult_left_commute" thy
   9.341 +    "(z1::real) * (z2 * z3) = z2 * (z1 * z3)"
   9.342 + (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1,
   9.343 +           rtac (real_mult_commute RS arg_cong) 1]);
   9.344 +
   9.345 +(* real multiplication is an AC operator *)
   9.346 +val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute];
   9.347 +
   9.348 +Goalw [real_one_def,pnat_one_def] "1r * z = z";
   9.349 +by (res_inst_tac [("z","z")] eq_Abs_real 1);
   9.350 +by (asm_full_simp_tac
   9.351 +    (simpset() addsimps [real_mult,
   9.352 +			 preal_add_mult_distrib2,preal_mult_1_right] 
   9.353 +                        @ preal_mult_ac @ preal_add_ac) 1);
   9.354 +qed "real_mult_1";
   9.355 +
   9.356 +Addsimps [real_mult_1];
   9.357 +
   9.358 +Goal "z * 1r = z";
   9.359 +by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
   9.360 +qed "real_mult_1_right";
   9.361 +
   9.362 +Addsimps [real_mult_1_right];
   9.363 +
   9.364 +Goalw [real_zero_def,pnat_one_def] "0r * z = 0r";
   9.365 +by (res_inst_tac [("z","z")] eq_Abs_real 1);
   9.366 +by (asm_full_simp_tac (simpset() addsimps [real_mult,
   9.367 +    preal_add_mult_distrib2,preal_mult_1_right] 
   9.368 +    @ preal_mult_ac @ preal_add_ac) 1);
   9.369 +qed "real_mult_0";
   9.370 +
   9.371 +Goal "z * 0r = 0r";
   9.372 +by (simp_tac (simpset() addsimps [real_mult_commute, real_mult_0]) 1);
   9.373 +qed "real_mult_0_right";
   9.374 +
   9.375 +Addsimps [real_mult_0_right, real_mult_0];
   9.376 +
   9.377 +Goal "-(x * y) = -x * (y::real)";
   9.378 +by (res_inst_tac [("z","x")] eq_Abs_real 1);
   9.379 +by (res_inst_tac [("z","y")] eq_Abs_real 1);
   9.380 +by (auto_tac (claset(),
   9.381 +	      simpset() addsimps [real_minus,real_mult] 
   9.382 +    @ preal_mult_ac @ preal_add_ac));
   9.383 +qed "real_minus_mult_eq1";
   9.384 +
   9.385 +Goal "-(x * y) = x * -(y::real)";
   9.386 +by (res_inst_tac [("z","x")] eq_Abs_real 1);
   9.387 +by (res_inst_tac [("z","y")] eq_Abs_real 1);
   9.388 +by (auto_tac (claset(),
   9.389 +	      simpset() addsimps [real_minus,real_mult] 
   9.390 +    @ preal_mult_ac @ preal_add_ac));
   9.391 +qed "real_minus_mult_eq2";
   9.392 +
   9.393 +Goal "- 1r * z = -z";
   9.394 +by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1);
   9.395 +qed "real_mult_minus_1";
   9.396 +
   9.397 +Addsimps [real_mult_minus_1];
   9.398 +
   9.399 +Goal "z * - 1r = -z";
   9.400 +by (stac real_mult_commute 1);
   9.401 +by (Simp_tac 1);
   9.402 +qed "real_mult_minus_1_right";
   9.403 +
   9.404 +Addsimps [real_mult_minus_1_right];
   9.405 +
   9.406 +Goal "-x * -y = x * (y::real)";
   9.407 +by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
   9.408 +    real_minus_mult_eq1 RS sym]) 1);
   9.409 +qed "real_minus_mult_cancel";
   9.410 +
   9.411 +Addsimps [real_minus_mult_cancel];
   9.412 +
   9.413 +Goal "-x * y = x * -(y::real)";
   9.414 +by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
   9.415 +    real_minus_mult_eq1 RS sym]) 1);
   9.416 +qed "real_minus_mult_commute";
   9.417 +
   9.418 +(*-----------------------------------------------------------------------------
   9.419 +
   9.420 + -----------------------------------------------------------------------------*)
   9.421 +
   9.422 +(** Lemmas **)
   9.423 +
   9.424 +qed_goal "real_add_assoc_cong" thy
   9.425 +    "!!z. (z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   9.426 + (fn _ => [(asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1)]);
   9.427 +
   9.428 +qed_goal "real_add_assoc_swap" thy "(z::real) + (v + w) = v + (z + w)"
   9.429 + (fn _ => [(REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1))]);
   9.430 +
   9.431 +Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)";
   9.432 +by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   9.433 +by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   9.434 +by (res_inst_tac [("z","w")] eq_Abs_real 1);
   9.435 +by (asm_simp_tac 
   9.436 +    (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @ 
   9.437 +                        preal_add_ac @ preal_mult_ac) 1);
   9.438 +qed "real_add_mult_distrib";
   9.439 +
   9.440 +val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute;
   9.441 +
   9.442 +Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)";
   9.443 +by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1);
   9.444 +qed "real_add_mult_distrib2";
   9.445 +
   9.446 +(*** one and zero are distinct ***)
   9.447 +Goalw [real_zero_def,real_one_def] "0r ~= 1r";
   9.448 +by (auto_tac (claset(),
   9.449 +         simpset() addsimps [preal_self_less_add_left RS preal_not_refl2]));
   9.450 +qed "real_zero_not_eq_one";
   9.451 +
   9.452 +(*** existence of inverse ***)
   9.453 +(** lemma -- alternative definition for 0r **)
   9.454 +Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})";
   9.455 +by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   9.456 +qed "real_zero_iff";
   9.457 +
   9.458 +Goalw [real_zero_def,real_one_def] 
   9.459 +          "!!(x::real). x ~= 0r ==> ? y. x*y = 1r";
   9.460 +by (res_inst_tac [("z","x")] eq_Abs_real 1);
   9.461 +by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
   9.462 +by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   9.463 +           simpset() addsimps [real_zero_iff RS sym]));
   9.464 +by (res_inst_tac [("x","Abs_real (realrel ^^ {(@#$#1p,pinv(D)+@#$#1p)})")] exI 1);
   9.465 +by (res_inst_tac [("x","Abs_real (realrel ^^ {(pinv(D)+@#$#1p,@#$#1p)})")] exI 2);
   9.466 +by (auto_tac (claset(),
   9.467 +	      simpset() addsimps [real_mult,
   9.468 +    pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2,
   9.469 +    preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right] 
   9.470 +    @ preal_add_ac @ preal_mult_ac));
   9.471 +qed "real_mult_inv_right_ex";
   9.472 +
   9.473 +Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r";
   9.474 +by (asm_simp_tac (simpset() addsimps [real_mult_commute,
   9.475 +    real_mult_inv_right_ex]) 1);
   9.476 +qed "real_mult_inv_left_ex";
   9.477 +
   9.478 +Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r";
   9.479 +by (forward_tac [real_mult_inv_left_ex] 1);
   9.480 +by (Step_tac 1);
   9.481 +by (rtac selectI2 1);
   9.482 +by Auto_tac;
   9.483 +qed "real_mult_inv_left";
   9.484 +
   9.485 +Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r";
   9.486 +by (auto_tac (claset() addIs [real_mult_commute RS subst],
   9.487 +              simpset() addsimps [real_mult_inv_left]));
   9.488 +qed "real_mult_inv_right";
   9.489 +
   9.490 +Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
   9.491 +by Auto_tac;
   9.492 +by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   9.493 +by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   9.494 +qed "real_mult_left_cancel";
   9.495 +    
   9.496 +Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
   9.497 +by (Step_tac 1);
   9.498 +by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   9.499 +by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   9.500 +qed "real_mult_right_cancel";
   9.501 +
   9.502 +Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
   9.503 +by (forward_tac [real_mult_inv_left_ex] 1);
   9.504 +by (etac exE 1);
   9.505 +by (rtac selectI2 1);
   9.506 +by (auto_tac (claset(),
   9.507 +	      simpset() addsimps [real_mult_0,
   9.508 +    real_zero_not_eq_one]));
   9.509 +qed "rinv_not_zero";
   9.510 +
   9.511 +Addsimps [real_mult_inv_left,real_mult_inv_right];
   9.512 +
   9.513 +Goal "x ~= 0r ==> rinv(rinv x) = x";
   9.514 +by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
   9.515 +by (etac rinv_not_zero 1);
   9.516 +by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
   9.517 +qed "real_rinv_rinv";
   9.518 +
   9.519 +Goalw [rinv_def] "rinv(1r) = 1r";
   9.520 +by (cut_facts_tac [real_zero_not_eq_one RS 
   9.521 +       not_sym RS real_mult_inv_left_ex] 1);
   9.522 +by (etac exE 1);
   9.523 +by (rtac selectI2 1);
   9.524 +by (auto_tac (claset(),
   9.525 +	      simpset() addsimps 
   9.526 +    [real_zero_not_eq_one RS not_sym]));
   9.527 +qed "real_rinv_1";
   9.528 +
   9.529 +Goal "x ~= 0r ==> rinv(-x) = -rinv(x)";
   9.530 +by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
   9.531 +by Auto_tac;
   9.532 +qed "real_minus_rinv";
   9.533 +
   9.534 +      (*** theorems for ordering ***)
   9.535 +(* prove introduction and elimination rules for real_less *)
   9.536 +
   9.537 +(* real_less is a strong order i.e nonreflexive and transitive *)
   9.538 +(*** lemmas ***)
   9.539 +Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y";
   9.540 +by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   9.541 +qed "preal_lemma_eq_rev_sum";
   9.542 +
   9.543 +Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1";
   9.544 +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.545 +qed "preal_add_left_commute_cancel";
   9.546 +
   9.547 +Goal "!!(x::preal). [| x + y2a = x2a + y; \
   9.548 +\                      x + y2b = x2b + y |] \
   9.549 +\                   ==> x2a + y2b = x2b + y2a";
   9.550 +by (dtac preal_lemma_eq_rev_sum 1);
   9.551 +by (assume_tac 1);
   9.552 +by (thin_tac "x + y2b = x2b + y" 1);
   9.553 +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.554 +by (dtac preal_add_left_commute_cancel 1);
   9.555 +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.556 +qed "preal_lemma_for_not_refl";
   9.557 +
   9.558 +Goal "~ (R::real) < R";
   9.559 +by (res_inst_tac [("z","R")] eq_Abs_real 1);
   9.560 +by (auto_tac (claset(),simpset() addsimps [real_less_def]));
   9.561 +by (dtac preal_lemma_for_not_refl 1);
   9.562 +by (assume_tac 1 THEN rotate_tac 2 1);
   9.563 +by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
   9.564 +qed "real_less_not_refl";
   9.565 +
   9.566 +(*** y < y ==> P ***)
   9.567 +bind_thm("real_less_irrefl", real_less_not_refl RS notE);
   9.568 +AddSEs [real_less_irrefl];
   9.569 +
   9.570 +Goal "!!(x::real). x < y ==> x ~= y";
   9.571 +by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
   9.572 +qed "real_not_refl2";
   9.573 +
   9.574 +(* lemma re-arranging and eliminating terms *)
   9.575 +Goal "!! (a::preal). [| a + b = c + d; \
   9.576 +\            x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \
   9.577 +\         ==> x2b + y2e < x2e + y2b";
   9.578 +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.579 +by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1);
   9.580 +by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   9.581 +qed "preal_lemma_trans";
   9.582 +
   9.583 +(** heavy re-writing involved*)
   9.584 +Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   9.585 +by (res_inst_tac [("z","R1")] eq_Abs_real 1);
   9.586 +by (res_inst_tac [("z","R2")] eq_Abs_real 1);
   9.587 +by (res_inst_tac [("z","R3")] eq_Abs_real 1);
   9.588 +by (auto_tac (claset(),simpset() addsimps [real_less_def]));
   9.589 +by (REPEAT(rtac exI 1));
   9.590 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.591 +by (REPEAT(Blast_tac 2));
   9.592 +by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1);
   9.593 +by (blast_tac (claset() addDs [preal_add_less_mono] 
   9.594 +    addIs [preal_lemma_trans]) 1);
   9.595 +qed "real_less_trans";
   9.596 +
   9.597 +Goal "!! (R1::real). [| R1 < R2; R2 < R1 |] ==> P";
   9.598 +by (dtac real_less_trans 1 THEN assume_tac 1);
   9.599 +by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1);
   9.600 +qed "real_less_asym";
   9.601 +
   9.602 +(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
   9.603 +    (****** Map and more real_less ******)
   9.604 +(*** mapping from preal into real ***)
   9.605 +Goalw [real_preal_def] 
   9.606 +            "%#((z1::preal) + z2) = %#z1 + %#z2";
   9.607 +by (asm_simp_tac (simpset() addsimps [real_add,
   9.608 +       preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1);
   9.609 +qed "real_preal_add";
   9.610 +
   9.611 +Goalw [real_preal_def] 
   9.612 +            "%#((z1::preal) * z2) = %#z1* %#z2";
   9.613 +by (full_simp_tac (simpset() addsimps [real_mult,
   9.614 +        preal_add_mult_distrib2,preal_mult_1,
   9.615 +        preal_mult_1_right,pnat_one_def] 
   9.616 +        @ preal_add_ac @ preal_mult_ac) 1);
   9.617 +qed "real_preal_mult";
   9.618 +
   9.619 +Goalw [real_preal_def]
   9.620 +      "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m";
   9.621 +by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   9.622 +    simpset() addsimps preal_add_ac));
   9.623 +qed "real_preal_ExI";
   9.624 +
   9.625 +Goalw [real_preal_def]
   9.626 +      "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#m ==> y < x";
   9.627 +by (auto_tac (claset(),
   9.628 +	      simpset() addsimps 
   9.629 +    [preal_add_commute,preal_add_assoc]));
   9.630 +by (asm_full_simp_tac (simpset() addsimps 
   9.631 +    [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
   9.632 +qed "real_preal_ExD";
   9.633 +
   9.634 +Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)";
   9.635 +by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1);
   9.636 +qed "real_preal_iff";
   9.637 +
   9.638 +(*** Gleason prop 9-4.4 p 127 ***)
   9.639 +Goalw [real_preal_def,real_zero_def] 
   9.640 +      "? m. (x::real) = %#m | x = 0r | x = -(%#m)";
   9.641 +by (res_inst_tac [("z","x")] eq_Abs_real 1);
   9.642 +by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
   9.643 +by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
   9.644 +by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   9.645 +    simpset() addsimps [preal_add_assoc RS sym]));
   9.646 +by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   9.647 +qed "real_preal_trichotomy";
   9.648 +
   9.649 +Goal "!!P. [| !!m. x = %#m ==> P; \
   9.650 +\             x = 0r ==> P; \
   9.651 +\             !!m. x = -(%#m) ==> P |] ==> P";
   9.652 +by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
   9.653 +by Auto_tac;
   9.654 +qed "real_preal_trichotomyE";
   9.655 +
   9.656 +Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
   9.657 +by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
   9.658 +by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
   9.659 +by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   9.660 +qed "real_preal_lessD";
   9.661 +
   9.662 +Goal "m1 < m2 ==> %#m1 < %#m2";
   9.663 +by (dtac preal_less_add_left_Ex 1);
   9.664 +by (auto_tac (claset(),
   9.665 +	      simpset() addsimps [real_preal_add,
   9.666 +    real_preal_def,real_less_def]));
   9.667 +by (REPEAT(rtac exI 1));
   9.668 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.669 +by (REPEAT(Blast_tac 2));
   9.670 +by (simp_tac (simpset() addsimps [preal_self_less_add_left] 
   9.671 +    delsimps [preal_add_less_iff2]) 1);
   9.672 +qed "real_preal_lessI";
   9.673 +
   9.674 +Goal "(%#m1 < %#m2) = (m1 < m2)";
   9.675 +by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1);
   9.676 +qed "real_preal_less_iff1";
   9.677 +
   9.678 +Addsimps [real_preal_less_iff1];
   9.679 +
   9.680 +Goal "- %#m < %#m";
   9.681 +by (auto_tac (claset(),
   9.682 +	      simpset() addsimps 
   9.683 +    [real_preal_def,real_less_def,real_minus]));
   9.684 +by (REPEAT(rtac exI 1));
   9.685 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.686 +by (REPEAT(Blast_tac 2));
   9.687 +by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.688 +by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   9.689 +    preal_add_assoc RS sym]) 1);
   9.690 +qed "real_preal_minus_less_self";
   9.691 +
   9.692 +Goalw [real_zero_def] "- %#m < 0r";
   9.693 +by (auto_tac (claset(),
   9.694 +	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   9.695 +by (REPEAT(rtac exI 1));
   9.696 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.697 +by (REPEAT(Blast_tac 2));
   9.698 +by (full_simp_tac (simpset() addsimps 
   9.699 +  [preal_self_less_add_right] @ preal_add_ac) 1);
   9.700 +qed "real_preal_minus_less_zero";
   9.701 +
   9.702 +Goal "~ 0r < - %#m";
   9.703 +by (cut_facts_tac [real_preal_minus_less_zero] 1);
   9.704 +by (fast_tac (claset() addDs [real_less_trans] 
   9.705 +                        addEs [real_less_irrefl]) 1);
   9.706 +qed "real_preal_not_minus_gt_zero";
   9.707 +
   9.708 +Goalw [real_zero_def] "0r < %#m";
   9.709 +by (auto_tac (claset(),
   9.710 +	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   9.711 +by (REPEAT(rtac exI 1));
   9.712 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.713 +by (REPEAT(Blast_tac 2));
   9.714 +by (full_simp_tac (simpset() addsimps 
   9.715 +		   [preal_self_less_add_right] @ preal_add_ac) 1);
   9.716 +qed "real_preal_zero_less";
   9.717 +
   9.718 +Goal "~ %#m < 0r";
   9.719 +by (cut_facts_tac [real_preal_zero_less] 1);
   9.720 +by (blast_tac (claset() addDs [real_less_trans] 
   9.721 +               addEs [real_less_irrefl]) 1);
   9.722 +qed "real_preal_not_less_zero";
   9.723 +
   9.724 +Goal "0r < - - %#m";
   9.725 +by (simp_tac (simpset() addsimps 
   9.726 +    [real_preal_zero_less]) 1);
   9.727 +qed "real_minus_minus_zero_less";
   9.728 +
   9.729 +(* another lemma *)
   9.730 +Goalw [real_zero_def] "0r < %#m + %#m1";
   9.731 +by (auto_tac (claset(),
   9.732 +	      simpset() addsimps [real_preal_def,real_less_def,real_add]));
   9.733 +by (REPEAT(rtac exI 1));
   9.734 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.735 +by (REPEAT(Blast_tac 2));
   9.736 +by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.737 +by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   9.738 +    preal_add_assoc RS sym]) 1);
   9.739 +qed "real_preal_sum_zero_less";
   9.740 +
   9.741 +Goal "- %#m < %#m1";
   9.742 +by (auto_tac (claset(),
   9.743 +	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   9.744 +by (REPEAT(rtac exI 1));
   9.745 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.746 +by (REPEAT(Blast_tac 2));
   9.747 +by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   9.748 +by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   9.749 +    preal_add_assoc RS sym]) 1);
   9.750 +qed "real_preal_minus_less_all";
   9.751 +
   9.752 +Goal "~ %#m < - %#m1";
   9.753 +by (cut_facts_tac [real_preal_minus_less_all] 1);
   9.754 +by (blast_tac (claset() addDs [real_less_trans] 
   9.755 +               addEs [real_less_irrefl]) 1);
   9.756 +qed "real_preal_not_minus_gt_all";
   9.757 +
   9.758 +Goal "- %#m1 < - %#m2 ==> %#m2 < %#m1";
   9.759 +by (auto_tac (claset(),
   9.760 +	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   9.761 +by (REPEAT(rtac exI 1));
   9.762 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.763 +by (REPEAT(Blast_tac 2));
   9.764 +by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   9.765 +by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   9.766 +by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   9.767 +qed "real_preal_minus_less_rev1";
   9.768 +
   9.769 +Goal "%#m1 < %#m2 ==> - %#m2 < - %#m1";
   9.770 +by (auto_tac (claset(),
   9.771 +	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   9.772 +by (REPEAT(rtac exI 1));
   9.773 +by (EVERY[rtac conjI 1, rtac conjI 2]);
   9.774 +by (REPEAT(Blast_tac 2));
   9.775 +by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   9.776 +by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   9.777 +by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   9.778 +qed "real_preal_minus_less_rev2";
   9.779 +
   9.780 +Goal "(- %#m1 < - %#m2) = (%#m2 < %#m1)";
   9.781 +by (blast_tac (claset() addSIs [real_preal_minus_less_rev1,
   9.782 +               real_preal_minus_less_rev2]) 1);
   9.783 +qed "real_preal_minus_less_rev_iff";
   9.784 +
   9.785 +Addsimps [real_preal_minus_less_rev_iff];
   9.786 +
   9.787 +(*** linearity ***)
   9.788 +Goal "(R1::real) < R2 | R1 = R2 | R2 < R1";
   9.789 +by (res_inst_tac [("x","R1")]  real_preal_trichotomyE 1);
   9.790 +by (ALLGOALS(res_inst_tac [("x","R2")]  real_preal_trichotomyE));
   9.791 +by (auto_tac (claset() addSDs [preal_le_anti_sym],
   9.792 +              simpset() addsimps [preal_less_le_iff,real_preal_minus_less_zero,
   9.793 +               real_preal_zero_less,real_preal_minus_less_all]));
   9.794 +qed "real_linear";
   9.795 +
   9.796 +Goal "!!w::real. (w ~= z) = (w<z | z<w)";
   9.797 +by (cut_facts_tac [real_linear] 1);
   9.798 +by (Blast_tac 1);
   9.799 +qed "real_neq_iff";
   9.800 +
   9.801 +Goal "!!(R1::real). [| R1 < R2 ==> P;  R1 = R2 ==> P; \
   9.802 +\                      R2 < R1 ==> P |] ==> P";
   9.803 +by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1);
   9.804 +by Auto_tac;
   9.805 +qed "real_linear_less2";
   9.806 +
   9.807 +(*** Properties of <= ***)
   9.808 +
   9.809 +Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
   9.810 +by (assume_tac 1);
   9.811 +qed "real_leI";
   9.812 +
   9.813 +Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
   9.814 +by (assume_tac 1);
   9.815 +qed "real_leD";
   9.816 +
   9.817 +val real_leE = make_elim real_leD;
   9.818 +
   9.819 +Goal "(~(w < z)) = (z <= (w::real))";
   9.820 +by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);
   9.821 +qed "real_less_le_iff";
   9.822 +
   9.823 +Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
   9.824 +by (Blast_tac 1);
   9.825 +qed "not_real_leE";
   9.826 +
   9.827 +Goalw [real_le_def] "z < w ==> z <= (w::real)";
   9.828 +by (blast_tac (claset() addEs [real_less_asym]) 1);
   9.829 +qed "real_less_imp_le";
   9.830 +
   9.831 +Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
   9.832 +by (cut_facts_tac [real_linear] 1);
   9.833 +by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
   9.834 +qed "real_le_imp_less_or_eq";
   9.835 +
   9.836 +Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
   9.837 +by (cut_facts_tac [real_linear] 1);
   9.838 +by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
   9.839 +qed "real_less_or_eq_imp_le";
   9.840 +
   9.841 +Goal "(x <= (y::real)) = (x < y | x=y)";
   9.842 +by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1));
   9.843 +qed "real_le_less";
   9.844 +
   9.845 +Goal "w <= (w::real)";
   9.846 +by (simp_tac (simpset() addsimps [real_le_less]) 1);
   9.847 +qed "real_le_refl";
   9.848 +
   9.849 +AddIffs [real_le_refl];
   9.850 +
   9.851 +(* Axiom 'linorder_linear' of class 'linorder': *)
   9.852 +Goal "(z::real) <= w | w <= z";
   9.853 +by (simp_tac (simpset() addsimps [real_le_less]) 1);
   9.854 +by (cut_facts_tac [real_linear] 1);
   9.855 +by (Blast_tac 1);
   9.856 +qed "real_le_linear";
   9.857 +
   9.858 +Goal "[| i <= j; j < k |] ==> i < (k::real)";
   9.859 +by (dtac real_le_imp_less_or_eq 1);
   9.860 +by (blast_tac (claset() addIs [real_less_trans]) 1);
   9.861 +qed "real_le_less_trans";
   9.862 +
   9.863 +Goal "!! (i::real). [| i < j; j <= k |] ==> i < k";
   9.864 +by (dtac real_le_imp_less_or_eq 1);
   9.865 +by (blast_tac (claset() addIs [real_less_trans]) 1);
   9.866 +qed "real_less_le_trans";
   9.867 +
   9.868 +Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
   9.869 +by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
   9.870 +            rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]);
   9.871 +qed "real_le_trans";
   9.872 +
   9.873 +Goal "[| z <= w; w <= z |] ==> z = (w::real)";
   9.874 +by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
   9.875 +            fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
   9.876 +qed "real_le_anti_sym";
   9.877 +
   9.878 +Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
   9.879 +by (rtac not_real_leE 1);
   9.880 +by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
   9.881 +qed "not_less_not_eq_real_less";
   9.882 +
   9.883 +(* Axiom 'order_less_le' of class 'order': *)
   9.884 +Goal "(w::real) < z = (w <= z & w ~= z)";
   9.885 +by (simp_tac (simpset() addsimps [real_le_def, real_neq_iff]) 1);
   9.886 +by (blast_tac (claset() addSEs [real_less_asym]) 1);
   9.887 +qed "real_less_le";
   9.888 +
   9.889 +
   9.890 +Goal "(0r < -R) = (R < 0r)";
   9.891 +by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   9.892 +by (auto_tac (claset(),
   9.893 +	      simpset() addsimps [real_preal_not_minus_gt_zero,
   9.894 +                        real_preal_not_less_zero,real_preal_zero_less,
   9.895 +                        real_preal_minus_less_zero]));
   9.896 +qed "real_minus_zero_less_iff";
   9.897 +
   9.898 +Addsimps [real_minus_zero_less_iff];
   9.899 +
   9.900 +Goal "(-R < 0r) = (0r < R)";
   9.901 +by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   9.902 +by (auto_tac (claset(),
   9.903 +	      simpset() addsimps [real_preal_not_minus_gt_zero,
   9.904 +                        real_preal_not_less_zero,real_preal_zero_less,
   9.905 +                        real_preal_minus_less_zero]));
   9.906 +qed "real_minus_zero_less_iff2";
   9.907 +
   9.908 +
   9.909 +(*Alternative definition for real_less*)
   9.910 +Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S";
   9.911 +by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   9.912 +by (ALLGOALS(res_inst_tac [("x","S")]  real_preal_trichotomyE));
   9.913 +by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   9.914 +	      simpset() addsimps [real_preal_not_minus_gt_all,
   9.915 +				  real_preal_add, real_preal_not_less_zero,
   9.916 +				  real_less_not_refl,
   9.917 +				  real_preal_not_minus_gt_zero]));
   9.918 +by (res_inst_tac [("x","%#D")] exI 1);
   9.919 +by (res_inst_tac [("x","%#m+%#ma")] exI 2);
   9.920 +by (res_inst_tac [("x","%#m")] exI 3);
   9.921 +by (res_inst_tac [("x","%#D")] exI 4);
   9.922 +by (auto_tac (claset(),
   9.923 +	      simpset() addsimps [real_preal_zero_less,
   9.924 +				  real_preal_sum_zero_less,real_add_assoc]));
   9.925 +qed "real_less_add_positive_left_Ex";
   9.926 +
   9.927 +
   9.928 +
   9.929 +(** change naff name(s)! **)
   9.930 +Goal "(W < S) ==> (0r < S + -W)";
   9.931 +by (dtac real_less_add_positive_left_Ex 1);
   9.932 +by (auto_tac (claset(),
   9.933 +	      simpset() addsimps [real_add_minus,
   9.934 +    real_add_zero_right] @ real_add_ac));
   9.935 +qed "real_less_sum_gt_zero";
   9.936 +
   9.937 +Goal "!!S::real. T = S + W ==> S = T + -W";
   9.938 +by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
   9.939 +qed "real_lemma_change_eq_subj";
   9.940 +
   9.941 +(* FIXME: long! *)
   9.942 +Goal "(0r < S + -W) ==> (W < S)";
   9.943 +by (rtac ccontr 1);
   9.944 +by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
   9.945 +by (auto_tac (claset(),
   9.946 +	      simpset() addsimps [real_less_not_refl]));
   9.947 +by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]);
   9.948 +by (Asm_full_simp_tac 1);
   9.949 +by (dtac real_lemma_change_eq_subj 1);
   9.950 +by Auto_tac;
   9.951 +by (dtac real_less_sum_gt_zero 1);
   9.952 +by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
   9.953 +by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]);
   9.954 +by (auto_tac (claset() addEs [real_less_asym], simpset()));
   9.955 +qed "real_sum_gt_zero_less";
   9.956 +
   9.957 +Goal "(0r < S + -W) = (W < S)";
   9.958 +by (blast_tac (claset() addIs [real_less_sum_gt_zero,
   9.959 +			       real_sum_gt_zero_less]) 1);
   9.960 +qed "real_less_sum_gt_0_iff";
   9.961 +
   9.962 +
   9.963 +Goalw [real_diff_def] "(x<y) = (x-y < 0r)";
   9.964 +by (stac (real_minus_zero_less_iff RS sym) 1);
   9.965 +by (simp_tac (simpset() addsimps [real_add_commute,
   9.966 +				  real_less_sum_gt_0_iff]) 1);
   9.967 +qed "real_less_eq_diff";
   9.968 +
   9.969 +
   9.970 +(*** Subtraction laws ***)
   9.971 +
   9.972 +Goal "x + (y - z) = (x + y) - (z::real)";
   9.973 +by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   9.974 +qed "real_add_diff_eq";
   9.975 +
   9.976 +Goal "(x - y) + z = (x + z) - (y::real)";
   9.977 +by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   9.978 +qed "real_diff_add_eq";
   9.979 +
   9.980 +Goal "(x - y) - z = x - (y + (z::real))";
   9.981 +by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   9.982 +qed "real_diff_diff_eq";
   9.983 +
   9.984 +Goal "x - (y - z) = (x + z) - (y::real)";
   9.985 +by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   9.986 +qed "real_diff_diff_eq2";
   9.987 +
   9.988 +Goal "(x-y < z) = (x < z + (y::real))";
   9.989 +by (stac real_less_eq_diff 1);
   9.990 +by (res_inst_tac [("y1", "z")] (real_less_eq_diff RS ssubst) 1);
   9.991 +by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   9.992 +qed "real_diff_less_eq";
   9.993 +
   9.994 +Goal "(x < z-y) = (x + (y::real) < z)";
   9.995 +by (stac real_less_eq_diff 1);
   9.996 +by (res_inst_tac [("y1", "z-y")] (real_less_eq_diff RS ssubst) 1);
   9.997 +by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   9.998 +qed "real_less_diff_eq";
   9.999 +
  9.1000 +Goalw [real_le_def] "(x-y <= z) = (x <= z + (y::real))";
  9.1001 +by (simp_tac (simpset() addsimps [real_less_diff_eq]) 1);
  9.1002 +qed "real_diff_le_eq";
  9.1003 +
  9.1004 +Goalw [real_le_def] "(x <= z-y) = (x + (y::real) <= z)";
  9.1005 +by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
  9.1006 +qed "real_le_diff_eq";
  9.1007 +
  9.1008 +Goalw [real_diff_def] "(x-y = z) = (x = z + (y::real))";
  9.1009 +by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
  9.1010 +qed "real_diff_eq_eq";
  9.1011 +
  9.1012 +Goalw [real_diff_def] "(x = z-y) = (x + (y::real) = z)";
  9.1013 +by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
  9.1014 +qed "real_eq_diff_eq";
  9.1015 +
  9.1016 +(*This list of rewrites simplifies (in)equalities by bringing subtractions
  9.1017 +  to the top and then moving negative terms to the other side.  
  9.1018 +  Use with real_add_ac*)
  9.1019 +val real_compare_rls = 
  9.1020 +  [symmetric real_diff_def,
  9.1021 +   real_add_diff_eq, real_diff_add_eq, real_diff_diff_eq, real_diff_diff_eq2, 
  9.1022 +   real_diff_less_eq, real_less_diff_eq, real_diff_le_eq, real_le_diff_eq, 
  9.1023 +   real_diff_eq_eq, real_eq_diff_eq];
  9.1024 +
  9.1025 +
  9.1026 +(** For the cancellation simproc.
  9.1027 +    The idea is to cancel like terms on opposite sides by subtraction **)
  9.1028 +
  9.1029 +Goal "(x::real) - y = x' - y' ==> (x<y) = (x'<y')";
  9.1030 +by (stac real_less_eq_diff 1);
  9.1031 +by (res_inst_tac [("y1", "y")] (real_less_eq_diff RS ssubst) 1);
  9.1032 +by (Asm_simp_tac 1);
  9.1033 +qed "real_less_eqI";
  9.1034 +
  9.1035 +Goal "(x::real) - y = x' - y' ==> (y<=x) = (y'<=x')";
  9.1036 +by (dtac real_less_eqI 1);
  9.1037 +by (asm_simp_tac (simpset() addsimps [real_le_def]) 1);
  9.1038 +qed "real_le_eqI";
  9.1039 +
  9.1040 +Goal "(x::real) - y = x' - y' ==> (x=y) = (x'=y')";
  9.1041 +by Safe_tac;
  9.1042 +by (ALLGOALS
  9.1043 +    (asm_full_simp_tac
  9.1044 +     (simpset() addsimps [real_eq_diff_eq, real_diff_eq_eq])));
  9.1045 +qed "real_eq_eqI";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Real/RealDef.thy	Thu Oct 01 18:18:01 1998 +0200
    10.3 @@ -0,0 +1,62 @@
    10.4 +(*  Title       : Real/RealDef.thy
    10.5 +    Author      : Jacques D. Fleuriot
    10.6 +    Copyright   : 1998  University of Cambridge
    10.7 +    Description : The reals
    10.8 +*) 
    10.9 +
   10.10 +RealDef = PReal +
   10.11 +
   10.12 +constdefs
   10.13 +  realrel   ::  "((preal * preal) * (preal * preal)) set"
   10.14 +  "realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
   10.15 +
   10.16 +typedef real = "{x::(preal*preal).True}/realrel"          (Equiv.quotient_def)
   10.17 +
   10.18 +
   10.19 +instance
   10.20 +   real  :: {ord, plus, times, minus}
   10.21 +
   10.22 +consts 
   10.23 +
   10.24 +  "0r"       :: real               ("0r")   
   10.25 +  "1r"       :: real               ("1r")  
   10.26 +
   10.27 +defs
   10.28 +
   10.29 +  real_zero_def  "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})"
   10.30 +  real_one_def   "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})"
   10.31 +
   10.32 +  real_minus_def
   10.33 +    "- R ==  Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)"
   10.34 +
   10.35 +  real_diff_def "x - y == x + -(y::real)"
   10.36 +
   10.37 +constdefs
   10.38 +
   10.39 +  real_preal :: preal => real              ("%#_" [80] 80)
   10.40 +  "%# m     == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})"
   10.41 +
   10.42 +  rinv       :: real => real
   10.43 +  "rinv(R)   == (@S. R ~= 0r & S*R = 1r)"
   10.44 +
   10.45 +  real_nat :: nat => real                  ("%%# _" [80] 80) 
   10.46 +  "%%# n      == %#(@#($#(*# n)))"
   10.47 +
   10.48 +defs
   10.49 +
   10.50 +  real_add_def  
   10.51 +  "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
   10.52 +                split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"
   10.53 +  
   10.54 +  real_mult_def  
   10.55 +  "P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
   10.56 +                split(%x1 y1. split(%x2 y2. realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)"
   10.57 +
   10.58 +  real_less_def
   10.59 +  "P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
   10.60 +                                   (x1,y1):Rep_real(P) &
   10.61 +                                   (x2,y2):Rep_real(Q)" 
   10.62 +  real_le_def
   10.63 +  "P <= (Q::real) == ~(Q < P)"
   10.64 +
   10.65 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Real/simproc.ML	Thu Oct 01 18:18:01 1998 +0200
    11.3 @@ -0,0 +1,62 @@
    11.4 +(*  Title:      HOL/Real/simproc.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Copyright   1998  University of Cambridge
    11.8 +
    11.9 +Apply Abel_Cancel to the reals
   11.10 +*)
   11.11 +
   11.12 +(*** Two lemmas needed for the simprocs ***)
   11.13 +
   11.14 +(*Deletion of other terms in the formula, seeking the -x at the front of z*)
   11.15 +val real_add_cancel_21 = prove_goal RealDef.thy
   11.16 +    "((x::real) + (y + z) = y + u) = ((x + z) = u)"
   11.17 +  (fn _ => [stac real_add_left_commute 1,
   11.18 +	    rtac real_add_left_cancel 1]);
   11.19 +
   11.20 +(*A further rule to deal with the case that
   11.21 +  everything gets cancelled on the right.*)
   11.22 +val real_add_cancel_end = prove_goal RealDef.thy
   11.23 +    "((x::real) + (y + z) = y) = (x = -z)"
   11.24 +  (fn _ => [stac real_add_left_commute 1,
   11.25 +	    res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1,
   11.26 +	    stac real_add_left_cancel 1,
   11.27 +	    simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1]);
   11.28 +
   11.29 +
   11.30 +structure Real_Cancel_Data =
   11.31 +struct
   11.32 +  val ss		= HOL_ss
   11.33 +  val mk_eq		= HOLogic.mk_Trueprop o HOLogic.mk_eq
   11.34 +  fun mk_meta_eq r	= r RS eq_reflection
   11.35 +
   11.36 +  val thy		= RealDef.thy
   11.37 +  val T			= Type ("RealDef.real", [])
   11.38 +  val zero		= Const ("RealDef.0r", T)
   11.39 +  val add_cancel_21	= real_add_cancel_21
   11.40 +  val add_cancel_end	= real_add_cancel_end
   11.41 +  val add_left_cancel	= real_add_left_cancel
   11.42 +  val add_assoc		= real_add_assoc
   11.43 +  val add_commute	= real_add_commute
   11.44 +  val add_left_commute	= real_add_left_commute
   11.45 +  val add_0		= real_add_zero_left
   11.46 +  val add_0_right	= real_add_zero_right
   11.47 +
   11.48 +  val eq_diff_eq	= real_eq_diff_eq
   11.49 +  val eqI_rules		= [real_less_eqI, real_eq_eqI, real_le_eqI]
   11.50 +  fun dest_eqI th = 
   11.51 +      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
   11.52 +	      (HOLogic.dest_Trueprop (concl_of th)))
   11.53 +
   11.54 +  val diff_def		= real_diff_def
   11.55 +  val minus_add_distrib	= real_minus_add_distrib
   11.56 +  val minus_minus	= real_minus_minus
   11.57 +  val minus_0		= real_minus_zero
   11.58 +  val add_inverses	= [real_add_minus, real_add_minus_left];
   11.59 +  val cancel_simps	= [real_add_minus_cancel, real_minus_add_cancel]
   11.60 +end;
   11.61 +
   11.62 +structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
   11.63 +
   11.64 +Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
   11.65 +