conversion of Real/PReal to Isar script;
authorpaulson
Thu Jan 01 21:47:07 2004 +0100 (2004-01-01)
changeset 143359c0b5e081037
parent 14334 6137d24eef79
child 14336 8f731d3cd65b
conversion of Real/PReal to Isar script;
type "complex" is now in class "field"
src/HOL/Complex/CLim.ML
src/HOL/Complex/Complex.thy
src/HOL/Complex/ComplexArith0.ML
src/HOL/Complex/NSCA.ML
src/HOL/Complex/NSComplex.thy
src/HOL/Complex/NSComplexArith.thy
src/HOL/Complex/NSComplexBin.ML
src/HOL/Complex/hcomplex_arith.ML
src/HOL/IsaMakefile
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/PReal.thy
src/HOL/Real/RealDef.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Complex/CLim.ML	Thu Jan 01 10:06:32 2004 +0100
     1.2 +++ b/src/HOL/Complex/CLim.ML	Thu Jan 01 21:47:07 2004 +0100
     1.3 @@ -5,9 +5,9 @@
     1.4                    differentiation for complex functions
     1.5  *)
     1.6  
     1.7 -(*------------------------------------------------------------------------------------*)
     1.8 +(*-----------------------------------------------------------------------*)
     1.9  (* Limit of complex to complex function                                               *)
    1.10 -(*------------------------------------------------------------------------------------*)
    1.11 +(*-----------------------------------------------------------------------*)
    1.12  
    1.13  Goalw [NSCLIM_def,NSCRLIM_def] 
    1.14     "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)";
    1.15 @@ -106,9 +106,9 @@
    1.16  by (blast_tac (claset() addIs [CLIM_NSCLIM,NSCLIM_CLIM]) 1);
    1.17  qed "CLIM_NSCLIM_iff";
    1.18  
    1.19 -(*------------------------------------------------------------------------------------*)
    1.20 +(*-----------------------------------------------------------------------*)
    1.21  (* Limit of complex to real function                                                  *)
    1.22 -(*------------------------------------------------------------------------------------*)
    1.23 +(*-----------------------------------------------------------------------*)
    1.24  
    1.25  Goalw [CRLIM_def,NSCRLIM_def,capprox_def] 
    1.26        "f -- x --CR> L ==> f -- x --NSCR> L";
    1.27 @@ -409,9 +409,9 @@
    1.28  qed "CLIM_CRLIM_Re_Im_iff";
    1.29  
    1.30  
    1.31 -(*------------------------------------------------------------------------------------*)
    1.32 +(*-----------------------------------------------------------------------*)
    1.33  (* Continuity                                                                         *)
    1.34 -(*------------------------------------------------------------------------------------*)
    1.35 +(*-----------------------------------------------------------------------*)
    1.36  
    1.37  Goalw [isNSContc_def] 
    1.38        "[| isNSContc f a; y @c= hcomplex_of_complex a |] \
    1.39 @@ -552,9 +552,9 @@
    1.40  Addsimps [isNSContc_const];
    1.41  
    1.42  
    1.43 -(*------------------------------------------------------------------------------------*)
    1.44 +(*-----------------------------------------------------------------------*)
    1.45  (* functions from complex to reals                                                    *)
    1.46 -(* -----------------------------------------------------------------------------------*)
    1.47 +(* ----------------------------------------------------------------------*)
    1.48  
    1.49  Goalw [isNSContCR_def] 
    1.50        "[| isNSContCR f a; y @c= hcomplex_of_complex a |] \
    1.51 @@ -619,9 +619,9 @@
    1.52  by (etac CLIM_CRLIM_Im 1);
    1.53  qed "isContc_isContCR_Im"; 
    1.54  
    1.55 -(*------------------------------------------------------------------------------------*)
    1.56 +(*-----------------------------------------------------------------------*)
    1.57  (* Derivatives                                                                        *)
    1.58 -(*------------------------------------------------------------------------------------*)
    1.59 +(*-----------------------------------------------------------------------*)
    1.60  
    1.61  Goalw [cderiv_def] 
    1.62        "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)";
    1.63 @@ -661,9 +661,9 @@
    1.64  qed "NSCDeriv_unique";
    1.65  
    1.66  
    1.67 -(*------------------------------------------------------------------------------------*)
    1.68 +(*-----------------------------------------------------------------------*)
    1.69  (* Differentiability                                                                  *)
    1.70 -(*------------------------------------------------------------------------------------*)
    1.71 +(*-----------------------------------------------------------------------*)
    1.72  
    1.73  Goalw [cdifferentiable_def] 
    1.74        "f cdifferentiable x ==> EX D. CDERIV f x :> D";
    1.75 @@ -686,9 +686,9 @@
    1.76  qed "NSCdifferentiableI";
    1.77  
    1.78  
    1.79 -(*------------------------------------------------------------------------------------*)
    1.80 +(*-----------------------------------------------------------------------*)
    1.81  (* Alternative definition for differentiability                                       *)
    1.82 -(*------------------------------------------------------------------------------------*)
    1.83 +(*-----------------------------------------------------------------------*)
    1.84  
    1.85  Goalw [CLIM_def] 
    1.86   "((%h. (f(a + h) - f(a))/h) -- 0 --C> D) = \
    1.87 @@ -710,9 +710,9 @@
    1.88  qed "CDERIV_iff2";
    1.89  
    1.90  
    1.91 -(*------------------------------------------------------------------------------------*)
    1.92 +(*-----------------------------------------------------------------------*)
    1.93  (* Equivalence of NS and standard defs of differentiation                             *)
    1.94 -(*------------------------------------------------------------------------------------*)
    1.95 +(*-----------------------------------------------------------------------*)
    1.96  
    1.97  (*** first equivalence ***)
    1.98  Goalw [nscderiv_def,NSCLIM_def] 
    1.99 @@ -767,10 +767,10 @@
   1.100      isNSContc_isContc_iff RS sym,NSCDERIV_isNSContc]) 1);
   1.101  qed "CDERIV_isContc";
   1.102  
   1.103 -(*------------------------------------------------------------------------------------*)
   1.104 +(*-----------------------------------------------------------------------*)
   1.105  (* Differentiation rules for combinations of functions follow from clear,             *)
   1.106  (* straightforard, algebraic manipulations                                            *)
   1.107 -(*------------------------------------------------------------------------------------*)
   1.108 +(*-----------------------------------------------------------------------*)
   1.109  
   1.110  (* use simple constant nslimit theorem *)
   1.111  Goal "(NSCDERIV (%x. k) x :> 0)";
   1.112 @@ -791,7 +791,7 @@
   1.113         simpset() addsimps [hcomplex_add_divide_distrib,hcomplex_diff_def]));
   1.114  by (dres_inst_tac [("b","hcomplex_of_complex Da"),
   1.115                     ("d","hcomplex_of_complex Db")] capprox_add 1);
   1.116 -by (auto_tac (claset(), simpset() addsimps hcomplex_add_ac));
   1.117 +by (auto_tac (claset(), simpset() addsimps add_ac));
   1.118  qed "NSCDERIV_add";
   1.119  
   1.120  Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \
   1.121 @@ -803,7 +803,7 @@
   1.122  (*** lemmas for multiplication ***)
   1.123  
   1.124  Goal "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))";
   1.125 -by (simp_tac (simpset() addsimps [hcomplex_diff_mult_distrib2]) 1);
   1.126 +by (simp_tac (simpset() addsimps [right_diff_distrib]) 1);
   1.127  val lemma_nscderiv1 = result();
   1.128  
   1.129  Goal "[| (x + y) / z = hcomplex_of_complex D + yb; z ~= 0; \
   1.130 @@ -833,7 +833,7 @@
   1.131  by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1);
   1.132  by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4);
   1.133  by (auto_tac (claset() addSIs [capprox_add_mono1],
   1.134 -      simpset() addsimps [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2, 
   1.135 +      simpset() addsimps [hcomplex_add_mult_distrib, right_distrib, 
   1.136  			  hcomplex_mult_commute, hcomplex_add_assoc]));
   1.137  by (res_inst_tac [("w1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")]
   1.138      (hcomplex_add_commute RS subst) 1);
   1.139 @@ -855,7 +855,10 @@
   1.140      (simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff,
   1.141                           complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym,
   1.142                           complex_diff_def] 
   1.143 -             delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym]) 1);
   1.144 +             delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym]
   1.145 +             delsimps [times_divide_eq_right, minus_mult_right RS sym]
   1.146 +
   1.147 +) 1);
   1.148  by (etac (NSCLIM_const RS NSCLIM_mult) 1);
   1.149  qed "NSCDERIV_cmult";
   1.150  
   1.151 @@ -868,7 +871,10 @@
   1.152  by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,complex_diff_def]) 1);
   1.153  by (res_inst_tac [("t","f x")] (complex_minus_minus RS subst) 1);
   1.154  by (asm_simp_tac (simpset() addsimps [complex_minus_add_distrib RS sym] 
   1.155 -                   delsimps [complex_minus_add_distrib, complex_minus_minus]) 1);
   1.156 +                   delsimps [complex_minus_add_distrib, complex_minus_minus]
   1.157 +                   delsimps [minus_add_distrib, minus_minus]
   1.158 +
   1.159 +) 1);
   1.160  by (etac NSCLIM_minus 1);
   1.161  qed "NSCDERIV_minus";
   1.162  
   1.163 @@ -995,9 +1001,9 @@
   1.164  by (auto_tac (claset() addDs [CDERIV_chain], simpset() addsimps [o_def]));
   1.165  qed "CDERIV_chain2";
   1.166  
   1.167 -(*------------------------------------------------------------------------------------*)
   1.168 +(*-----------------------------------------------------------------------*)
   1.169  (* Differentiation of natural number powers                                           *)
   1.170 -(*------------------------------------------------------------------------------------*)
   1.171 +(*-----------------------------------------------------------------------*)
   1.172  
   1.173  Goal "NSCDERIV (%x. x) x :> 1";
   1.174  by (auto_tac (claset(),
   1.175 @@ -1029,7 +1035,8 @@
   1.176  by (dtac (CDERIV_Id RS CDERIV_mult) 2);
   1.177  by (auto_tac (claset(), 
   1.178                simpset() addsimps [complex_of_real_add RS sym,
   1.179 -              complex_add_mult_distrib,real_of_nat_Suc] delsimps [complex_of_real_add]));
   1.180 +                        complex_add_mult_distrib,real_of_nat_Suc] 
   1.181 +                 delsimps [complex_of_real_add]));
   1.182  by (case_tac "n" 1);
   1.183  by (auto_tac (claset(), 
   1.184                simpset() addsimps [complex_mult_assoc, complex_add_commute]));
   1.185 @@ -1062,24 +1069,19 @@
   1.186  by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,numeral_2_eq_2]) 2); 
   1.187  by (auto_tac (claset(),
   1.188       simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def] 
   1.189 -               delsimps [minus_mult_right RS sym, minus_mult_left RS sym,
   1.190 -                         hcomplex_minus_mult_eq1 RS sym,
   1.191 -                         hcomplex_minus_mult_eq2 RS sym]));
   1.192 +               delsimps [minus_mult_left RS sym, minus_mult_right RS sym]));
   1.193  by (asm_simp_tac
   1.194       (simpset() addsimps [inverse_add,
   1.195 -          inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] 
   1.196 -          @ hcomplex_add_ac @ hcomplex_mult_ac 
   1.197 +          inverse_mult_distrib RS sym, inverse_minus_eq RS sym] 
   1.198 +          @ add_ac @ mult_ac 
   1.199         delsimps [inverse_minus_eq,
   1.200 -		 inverse_mult_distrib, minus_mult_right RS sym, minus_mult_left RS sym,
   1.201 -                         hcomplex_minus_mult_eq1 RS sym,
   1.202 -                 hcomplex_minus_mult_eq2 RS sym] ) 1);
   1.203 -by (asm_simp_tac (HOL_ss addsimps [hcomplex_mult_assoc RS sym,
   1.204 -                                      hcomplex_add_mult_distrib2]) 1);
   1.205 +		 inverse_mult_distrib, minus_mult_right RS sym, minus_mult_left RS sym] ) 1);
   1.206 +by (asm_simp_tac (HOL_ss addsimps [mult_assoc RS sym, right_distrib]) 1);
   1.207  by (res_inst_tac [("y"," inverse(- hcomplex_of_complex x * hcomplex_of_complex x)")] 
   1.208                   capprox_trans 1);
   1.209  by (rtac inverse_add_CInfinitesimal_capprox2 1);
   1.210  by (auto_tac (claset() addSDs [hcomplex_of_complex_CFinite_diff_CInfinitesimal] addIs [CFinite_mult], 
   1.211 -         simpset() addsimps [hcomplex_minus_inverse RS sym]));
   1.212 +         simpset() addsimps [inverse_minus_eq RS sym]));
   1.213  by (rtac CInfinitesimal_CFinite_mult2 1); 
   1.214  by Auto_tac;  
   1.215  qed "NSCDERIV_inverse";
   1.216 @@ -1090,16 +1092,16 @@
   1.217  qed "CDERIV_inverse";
   1.218  
   1.219  
   1.220 -(*------------------------------------------------------------------------------------*)
   1.221 +(*-----------------------------------------------------------------------*)
   1.222  (* Derivative of inverse                                                              *)
   1.223 -(*------------------------------------------------------------------------------------*)
   1.224 +(*-----------------------------------------------------------------------*)
   1.225  
   1.226  Goal "[| CDERIV f x :> d; f(x) ~= 0 |] \
   1.227  \     ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
   1.228  by (rtac (complex_mult_commute RS subst) 1);
   1.229  by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1,
   1.230 -    complexpow_inverse] delsimps [complexpow_Suc, 
   1.231 -    complex_minus_mult_eq1 RS sym]) 1);
   1.232 +    complexpow_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym,
   1.233 +complex_minus_mult_eq1 RS sym]) 1);
   1.234  by (fold_goals_tac [o_def]);
   1.235  by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1);
   1.236  qed "CDERIV_inverse_fun";
   1.237 @@ -1110,9 +1112,9 @@
   1.238              CDERIV_inverse_fun] delsimps [complexpow_Suc]) 1);
   1.239  qed "NSCDERIV_inverse_fun";
   1.240  
   1.241 -(*------------------------------------------------------------------------------------*)
   1.242 +(*-----------------------------------------------------------------------*)
   1.243  (* Derivative of quotient                                                             *)
   1.244 -(*------------------------------------------------------------------------------------*)
   1.245 +(*-----------------------------------------------------------------------*)
   1.246  
   1.247  
   1.248  Goal "x ~= (0::complex) \\<Longrightarrow> (x * inverse(x) ^ 2) = inverse x";
   1.249 @@ -1129,8 +1131,7 @@
   1.250  by (asm_full_simp_tac
   1.251      (simpset() addsimps [complex_divide_def, complex_add_mult_distrib2,
   1.252                           complexpow_inverse,complex_minus_mult_eq1] @ complex_mult_ac 
   1.253 -       delsimps [complexpow_Suc, complex_minus_mult_eq1 RS sym,
   1.254 -                 complex_minus_mult_eq2 RS sym]) 1);
   1.255 +       delsimps [complexpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
   1.256  qed "CDERIV_quotient";
   1.257  
   1.258  Goal "[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) ~= 0 |] \
   1.259 @@ -1140,9 +1141,9 @@
   1.260  qed "NSCDERIV_quotient";
   1.261   
   1.262  
   1.263 -(*------------------------------------------------------------------------------------*)
   1.264 +(*-----------------------------------------------------------------------*)
   1.265  (* Caratheodory formulation of derivative at a point: standard proof                  *)
   1.266 -(*------------------------------------------------------------------------------------*)
   1.267 +(*-----------------------------------------------------------------------*)
   1.268  
   1.269  
   1.270  Goalw [CLIM_def] 
     2.1 --- a/src/HOL/Complex/Complex.thy	Thu Jan 01 10:06:32 2004 +0100
     2.2 +++ b/src/HOL/Complex/Complex.thy	Thu Jan 01 21:47:07 2004 +0100
     2.3 @@ -483,28 +483,6 @@
     2.4  apply (auto simp add: complex_mult complex_minus real_diff_def)
     2.5  done
     2.6  
     2.7 -declare complex_minus_mult_eq1 [symmetric, simp] complex_minus_mult_eq2 [symmetric, simp]
     2.8 -
     2.9 -lemma complex_mult_minus_one: "-(1::complex) * z = -z"
    2.10 -apply (simp (no_asm))
    2.11 -done
    2.12 -declare complex_mult_minus_one [simp]
    2.13 -
    2.14 -lemma complex_mult_minus_one_right: "z * -(1::complex) = -z"
    2.15 -apply (subst complex_mult_commute)
    2.16 -apply (simp (no_asm))
    2.17 -done
    2.18 -declare complex_mult_minus_one_right [simp]
    2.19 -
    2.20 -lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)"
    2.21 -apply (simp (no_asm))
    2.22 -done
    2.23 -declare complex_minus_mult_cancel [simp]
    2.24 -
    2.25 -lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
    2.26 -apply (simp (no_asm))
    2.27 -done
    2.28 -
    2.29  lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)"
    2.30  apply (rule_tac z = z1 in eq_Abs_complex)
    2.31  apply (rule_tac z = z2 in eq_Abs_complex)
    2.32 @@ -541,6 +519,13 @@
    2.33  apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO)
    2.34  done
    2.35  
    2.36 +instance complex :: division_by_zero
    2.37 +proof
    2.38 +  fix x :: complex
    2.39 +  show "inverse 0 = (0::complex)" by (rule COMPLEX_INVERSE_ZERO)
    2.40 +  show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) 
    2.41 +qed
    2.42 +
    2.43  lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1"
    2.44  apply (rule_tac z = z in eq_Abs_complex)
    2.45  apply (auto simp add: complex_mult complex_inverse complex_one_def 
    2.46 @@ -554,6 +539,61 @@
    2.47  by (auto intro: complex_mult_commute [THEN subst])
    2.48  declare complex_mult_inv_right [simp]
    2.49  
    2.50 +
    2.51 +subsection {* The field of complex numbers *}
    2.52 +
    2.53 +instance complex :: field
    2.54 +proof
    2.55 +  fix z u v w :: complex
    2.56 +  show "(u + v) + w = u + (v + w)"
    2.57 +    by (rule complex_add_assoc) 
    2.58 +  show "z + w = w + z"
    2.59 +    by (rule complex_add_commute) 
    2.60 +  show "0 + z = z"
    2.61 +    by (rule complex_add_zero_left) 
    2.62 +  show "-z + z = 0"
    2.63 +    by (rule complex_add_minus_left_zero) 
    2.64 +  show "z - w = z + -w"
    2.65 +    by (simp add: complex_diff_def)
    2.66 +  show "(u * v) * w = u * (v * w)"
    2.67 +    by (rule complex_mult_assoc) 
    2.68 +  show "z * w = w * z"
    2.69 +    by (rule complex_mult_commute) 
    2.70 +  show "1 * z = z"
    2.71 +    by (rule complex_mult_one_left) 
    2.72 +  show "0 \<noteq> (1::complex)"  --{*for some reason it has to be early*}
    2.73 +    by (rule complex_zero_not_eq_one) 
    2.74 +  show "(u + v) * w = u * w + v * w"
    2.75 +    by (rule complex_add_mult_distrib) 
    2.76 +  assume neq: "w \<noteq> 0"
    2.77 +  thus "z / w = z * inverse w"
    2.78 +    by (simp add: complex_divide_def)
    2.79 +  show "inverse w * w = 1"
    2.80 +    by (simp add: neq complex_mult_inv_left) 
    2.81 +qed
    2.82 +
    2.83 +
    2.84 +lemma complex_mult_minus_one: "-(1::complex) * z = -z"
    2.85 +apply (simp (no_asm))
    2.86 +done
    2.87 +declare complex_mult_minus_one [simp]
    2.88 +
    2.89 +lemma complex_mult_minus_one_right: "z * -(1::complex) = -z"
    2.90 +apply (subst complex_mult_commute)
    2.91 +apply (simp (no_asm))
    2.92 +done
    2.93 +declare complex_mult_minus_one_right [simp]
    2.94 +
    2.95 +lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)"
    2.96 +apply (simp (no_asm))
    2.97 +done
    2.98 +declare complex_minus_mult_cancel [simp]
    2.99 +
   2.100 +lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
   2.101 +apply (simp (no_asm))
   2.102 +done
   2.103 +
   2.104 +
   2.105  lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)"
   2.106  apply auto
   2.107  apply (drule_tac f = "%x. x*inverse c" in arg_cong)
   2.108 @@ -603,11 +643,7 @@
   2.109  done
   2.110  
   2.111  lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)"
   2.112 -apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO)
   2.113 -apply (case_tac "y = 0", simp add: COMPLEX_INVERSE_ZERO)
   2.114 -apply (rule_tac c1 = "x*y" in complex_mult_left_cancel [THEN iffD1])
   2.115 -apply (auto simp add: complex_mult_not_zero complex_mult_ac)
   2.116 -apply (auto simp add: complex_mult_not_zero complex_mult_assoc [symmetric])
   2.117 +apply (rule inverse_mult_distrib) 
   2.118  done
   2.119  
   2.120  
     3.1 --- a/src/HOL/Complex/ComplexArith0.ML	Thu Jan 01 10:06:32 2004 +0100
     3.2 +++ b/src/HOL/Complex/ComplexArith0.ML	Thu Jan 01 21:47:07 2004 +0100
     3.3 @@ -24,8 +24,6 @@
     3.4  Goal "(inverse(x::complex) = 0) = (x = 0)";
     3.5  by (auto_tac (claset(), 
     3.6                simpset() addsimps [COMPLEX_INVERSE_ZERO]));  
     3.7 -by (rtac ccontr 1); 
     3.8 -by (blast_tac (claset() addDs [complex_inverse_not_zero]) 1); 
     3.9  qed "complex_inverse_zero_iff";
    3.10  Addsimps [complex_inverse_zero_iff];
    3.11  
    3.12 @@ -287,7 +285,6 @@
    3.13  
    3.14  Goal "(-b = -a) = (b = (a::complex))";
    3.15  by Auto_tac;
    3.16 -by (etac ( inj_complex_minus RS injD) 1);
    3.17  qed "complex_minus_eq_cancel";
    3.18  Addsimps [complex_minus_eq_cancel];
    3.19  
     4.1 --- a/src/HOL/Complex/NSCA.ML	Thu Jan 01 10:06:32 2004 +0100
     4.2 +++ b/src/HOL/Complex/NSCA.ML	Thu Jan 01 21:47:07 2004 +0100
     4.3 @@ -420,9 +420,9 @@
     4.4  val prem1::prem2::rest = 
     4.5  goalw thy [capprox_def,hcomplex_diff_def] 
     4.6       "[| a @c= b; c @c= d |] ==> a+c @c= b+d";
     4.7 -by (rtac (hcomplex_minus_add_distrib RS ssubst) 1);
     4.8 +by (rtac (minus_add_distrib RS ssubst) 1);
     4.9  by (rtac (hcomplex_add_assoc RS ssubst) 1);
    4.10 -by (res_inst_tac [("y1","c")] (hcomplex_add_left_commute RS subst) 1);
    4.11 +by (res_inst_tac [("b1","c")] (add_left_commute RS subst) 1);
    4.12  by (rtac (hcomplex_add_assoc RS subst) 1);
    4.13  by (rtac ([prem1,prem2] MRS CInfinitesimal_add) 1);
    4.14  qed "capprox_add";
    4.15 @@ -449,7 +449,7 @@
    4.16  Goalw [capprox_def,hcomplex_diff_def] 
    4.17        "[| a @c= b; c: CFinite|] ==> a*c @c= b*c"; 
    4.18  by (asm_full_simp_tac (HOL_ss addsimps [CInfinitesimal_CFinite_mult,
    4.19 -    hcomplex_minus_mult_eq1,hcomplex_add_mult_distrib RS sym]) 1);
    4.20 +    minus_mult_left,hcomplex_add_mult_distrib RS sym]) 1);
    4.21  qed "capprox_mult1";
    4.22  
    4.23  Goal "[|a @c= b; c: CFinite|] ==> c*a @c= c*b"; 
    4.24 @@ -525,8 +525,8 @@
    4.25  Goal "d + b  @c= d + c ==> b @c= c";
    4.26  by (dtac (capprox_minus_iff RS iffD1) 1);
    4.27  by (asm_full_simp_tac (simpset() addsimps 
    4.28 -    [hcomplex_minus_add_distrib,capprox_minus_iff RS sym] 
    4.29 -    @ hcomplex_add_ac) 1);
    4.30 +    [minus_add_distrib,capprox_minus_iff RS sym] 
    4.31 +    @ add_ac) 1);
    4.32  qed "capprox_add_left_cancel";
    4.33  
    4.34  Goal "b + d @c= c + d ==> b @c= c";
    4.35 @@ -538,7 +538,7 @@
    4.36  Goal "b @c= c ==> d + b @c= d + c";
    4.37  by (rtac (capprox_minus_iff RS iffD2) 1);
    4.38  by (asm_full_simp_tac (simpset() addsimps 
    4.39 -    [capprox_minus_iff RS sym] @ hcomplex_add_ac) 1);
    4.40 +    [capprox_minus_iff RS sym] @ add_ac) 1);
    4.41  qed "capprox_add_mono1";
    4.42  
    4.43  Goal "b @c= c ==> b + a @c= c + a";
    4.44 @@ -1223,7 +1223,7 @@
    4.45  by (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))" 1);
    4.46  by (dtac sym 2 THEN dtac sym 2);
    4.47  by (Asm_full_simp_tac 2);
    4.48 -by (asm_simp_tac (simpset() addsimps hcomplex_add_ac) 1);
    4.49 +by (asm_simp_tac (simpset() addsimps add_ac) 1);
    4.50  by (REPEAT(dtac stc_SComplex 1));
    4.51  by (dtac SComplex_add 1 THEN assume_tac 1);
    4.52  by (dtac CInfinitesimal_add 1 THEN assume_tac 1);
    4.53 @@ -1268,7 +1268,7 @@
    4.54  by (forw_inst_tac [("x","ea"),("y","x")] CInfinitesimal_CFinite_mult 2);
    4.55  by (dtac CInfinitesimal_mult 3);
    4.56  by (auto_tac (claset() addIs [CInfinitesimal_add],
    4.57 -              simpset() addsimps hcomplex_add_ac @ hcomplex_mult_ac));
    4.58 +              simpset() addsimps add_ac @ mult_ac));
    4.59  qed "lemma_stc_mult";
    4.60  
    4.61  Goal "[| x: CFinite; y: CFinite |] \
    4.62 @@ -1282,7 +1282,7 @@
    4.63  by (thin_tac "x = stc x + e" 1);
    4.64  by (thin_tac "y = stc y + ea" 1);
    4.65  by (asm_full_simp_tac (simpset() addsimps 
    4.66 -    [hcomplex_add_mult_distrib,hcomplex_add_mult_distrib2]) 1);
    4.67 +    [hcomplex_add_mult_distrib,right_distrib]) 1);
    4.68  by (REPEAT(dtac stc_SComplex 1));
    4.69  by (full_simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1);
    4.70  by (rtac stc_CInfinitesimal_add_SComplex 1);
     5.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Jan 01 10:06:32 2004 +0100
     5.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Jan 01 21:47:07 2004 +0100
     5.3 @@ -6,12 +6,38 @@
     5.4  
     5.5  theory NSComplex = NSInduct:
     5.6  
     5.7 +(*for Ring_and_Field?*)
     5.8 +declare field_mult_eq_0_iff [simp]
     5.9 +
    5.10  (* Move to one of the hyperreal theories *)
    5.11  lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
    5.12  apply (induct_tac "m")
    5.13  apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
    5.14  done
    5.15  
    5.16 +(* not proved already? strange! *)
    5.17 +lemma hypreal_of_nat_le_iff:
    5.18 +      "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)"
    5.19 +apply (unfold hypreal_le_def)
    5.20 +apply auto
    5.21 +done
    5.22 +declare hypreal_of_nat_le_iff [simp]
    5.23 +
    5.24 +lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n"
    5.25 +apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
    5.26 +         del: hypreal_of_nat_zero)
    5.27 +done
    5.28 +declare hypreal_of_nat_ge_zero [simp]
    5.29 +
    5.30 +declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
    5.31 +
    5.32 +lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n"
    5.33 +apply (rule_tac z = "n" in eq_Abs_hypnat)
    5.34 +apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
    5.35 +done
    5.36 +declare hypreal_of_hypnat_ge_zero [simp]
    5.37 +declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp]
    5.38 +
    5.39  constdefs
    5.40      hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
    5.41      "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) &
    5.42 @@ -232,7 +258,8 @@
    5.43  apply (auto , ultra)
    5.44  done
    5.45  
    5.46 -lemma hcomplex_hRe_hIm_cancel_iff: "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
    5.47 +lemma hcomplex_hRe_hIm_cancel_iff:
    5.48 +     "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
    5.49  apply (rule_tac z = "z" in eq_Abs_hcomplex)
    5.50  apply (rule_tac z = "w" in eq_Abs_hcomplex)
    5.51  apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
    5.52 @@ -293,34 +320,22 @@
    5.53     Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
    5.54  apply (unfold hcomplex_add_def)
    5.55  apply (rule_tac f = "Abs_hcomplex" in arg_cong)
    5.56 -apply auto
    5.57 -apply (ultra)
    5.58 +apply (auto, ultra)
    5.59  done
    5.60  
    5.61  lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
    5.62  apply (rule_tac z = "z" in eq_Abs_hcomplex)
    5.63  apply (rule_tac z = "w" in eq_Abs_hcomplex)
    5.64 -apply (simp (no_asm_simp) add: complex_add_commute hcomplex_add)
    5.65 +apply (simp add: complex_add_commute hcomplex_add)
    5.66  done
    5.67  
    5.68  lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
    5.69  apply (rule_tac z = "z1" in eq_Abs_hcomplex)
    5.70  apply (rule_tac z = "z2" in eq_Abs_hcomplex)
    5.71  apply (rule_tac z = "z3" in eq_Abs_hcomplex)
    5.72 -apply (simp (no_asm_simp) add: hcomplex_add complex_add_assoc)
    5.73 +apply (simp add: hcomplex_add complex_add_assoc)
    5.74  done
    5.75  
    5.76 -(*For AC rewriting*)
    5.77 -lemma hcomplex_add_left_commute: "(x::hcomplex)+(y+z)=y+(x+z)"
    5.78 -apply (rule hcomplex_add_commute [THEN trans])
    5.79 -apply (rule hcomplex_add_assoc [THEN trans])
    5.80 -apply (rule hcomplex_add_commute [THEN arg_cong])
    5.81 -done
    5.82 -
    5.83 -(* hcomplex addition is an AC operator *)
    5.84 -lemmas hcomplex_add_ac = hcomplex_add_assoc hcomplex_add_commute
    5.85 -                      hcomplex_add_left_commute 
    5.86 -
    5.87  lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
    5.88  apply (unfold hcomplex_zero_def)
    5.89  apply (rule_tac z = "z" in eq_Abs_hcomplex)
    5.90 @@ -328,9 +343,8 @@
    5.91  done
    5.92  
    5.93  lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
    5.94 -apply (simp (no_asm) add: hcomplex_add_zero_left hcomplex_add_commute)
    5.95 +apply (simp add: hcomplex_add_zero_left hcomplex_add_commute)
    5.96  done
    5.97 -declare hcomplex_add_zero_left [simp] hcomplex_add_zero_right [simp]
    5.98  
    5.99  lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
   5.100  apply (rule_tac z = "x" in eq_Abs_hcomplex)
   5.101 @@ -350,7 +364,6 @@
   5.102  
   5.103  lemma hcomplex_minus_congruent:
   5.104    "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
   5.105 -
   5.106  apply (unfold congruent_def)
   5.107  apply safe
   5.108  apply (ultra+)
   5.109 @@ -361,24 +374,24 @@
   5.110        Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
   5.111  apply (unfold hcomplex_minus_def)
   5.112  apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   5.113 -apply (auto , ultra)
   5.114 +apply (auto, ultra)
   5.115  done
   5.116  
   5.117  lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
   5.118  apply (rule_tac z = "z" in eq_Abs_hcomplex)
   5.119  apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
   5.120  done
   5.121 -declare hcomplex_add_minus_left [simp]
   5.122 +
   5.123  
   5.124  subsection{*Multiplication for Nonstandard Complex Numbers*}
   5.125  
   5.126  lemma hcomplex_mult:
   5.127 -  "Abs_hcomplex(hcomplexrel``{%n. X n}) * Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   5.128 +  "Abs_hcomplex(hcomplexrel``{%n. X n}) * 
   5.129 +     Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   5.130     Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
   5.131 -
   5.132  apply (unfold hcomplex_mult_def)
   5.133  apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   5.134 -apply (auto , ultra)
   5.135 +apply (auto, ultra)
   5.136  done
   5.137  
   5.138  lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
   5.139 @@ -399,16 +412,15 @@
   5.140  apply (rule_tac z = "z" in eq_Abs_hcomplex)
   5.141  apply (auto simp add: hcomplex_mult)
   5.142  done
   5.143 -declare hcomplex_mult_one_left [simp]
   5.144  
   5.145  lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
   5.146  apply (unfold hcomplex_zero_def)
   5.147  apply (rule_tac z = "z" in eq_Abs_hcomplex)
   5.148  apply (auto simp add: hcomplex_mult)
   5.149  done
   5.150 -declare hcomplex_mult_zero_left [simp]
   5.151  
   5.152 -lemma hcomplex_add_mult_distrib: "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
   5.153 +lemma hcomplex_add_mult_distrib:
   5.154 +     "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
   5.155  apply (rule_tac z = "z1" in eq_Abs_hcomplex)
   5.156  apply (rule_tac z = "z2" in eq_Abs_hcomplex)
   5.157  apply (rule_tac z = "w" in eq_Abs_hcomplex)
   5.158 @@ -430,7 +442,7 @@
   5.159        Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
   5.160  apply (unfold hcinv_def)
   5.161  apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   5.162 -apply (auto , ultra)
   5.163 +apply (auto, ultra)
   5.164  done
   5.165  
   5.166  lemma hcomplex_mult_inv_left:
   5.167 @@ -443,7 +455,6 @@
   5.168  apply (drule complex_mult_inv_left)
   5.169  apply auto
   5.170  done
   5.171 -declare hcomplex_mult_inv_left [simp]
   5.172  
   5.173  subsection {* The Field of Nonstandard Complex Numbers *}
   5.174  
   5.175 @@ -455,9 +466,9 @@
   5.176    show "z + w = w + z"
   5.177      by (simp add: hcomplex_add_commute)
   5.178    show "0 + z = z"
   5.179 -    by (simp)
   5.180 +    by (simp add: hcomplex_add_zero_left)
   5.181    show "-z + z = 0"
   5.182 -    by (simp)
   5.183 +    by (simp add: hcomplex_add_minus_left)
   5.184    show "z - w = z + -w"
   5.185      by (simp add: hcomplex_diff_def)
   5.186    show "(u * v) * w = u * (v * w)"
   5.187 @@ -465,7 +476,7 @@
   5.188    show "z * w = w * z"
   5.189      by (simp add: hcomplex_mult_commute)
   5.190    show "1 * z = z"
   5.191 -    by (simp)
   5.192 +    by (simp add: hcomplex_mult_one_left)
   5.193    show "0 \<noteq> (1::hcomplex)"
   5.194      by (rule hcomplex_zero_not_eq_one)
   5.195    show "(u + v) * w = u * w + v * w"
   5.196 @@ -478,12 +489,11 @@
   5.197  qed
   5.198  
   5.199  lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0"
   5.200 -apply (unfold hcomplex_zero_def)
   5.201 -apply (auto simp add: hcomplex_inverse)
   5.202 +apply (simp add:  hcomplex_zero_def hcomplex_inverse)
   5.203  done
   5.204  
   5.205  lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0"
   5.206 -apply (simp (no_asm) add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO)
   5.207 +apply (simp add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO)
   5.208  done
   5.209  
   5.210  instance hcomplex :: division_by_zero
   5.211 @@ -493,9 +503,6 @@
   5.212    show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO) 
   5.213  qed
   5.214  
   5.215 -lemma hcomplex_mult_left_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)"
   5.216 -by (simp add: field_mult_cancel_left) 
   5.217 -
   5.218  subsection{*More Minus Laws*}
   5.219  
   5.220  lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)"
   5.221 @@ -520,49 +527,13 @@
   5.222  apply (simp add: minus_equation_iff [of x y]) 
   5.223  done
   5.224  
   5.225 -lemma hcomplex_minus_add_distrib: "-(x + y) = -x + -(y::hcomplex)"
   5.226 -apply (rule Ring_and_Field.minus_add_distrib) 
   5.227 -done
   5.228 -
   5.229 -lemma hcomplex_add_left_cancel: "((x::hcomplex) + y = x + z) = (y = z)"
   5.230 -apply (rule Ring_and_Field.add_left_cancel) 
   5.231 -done
   5.232 -declare hcomplex_add_left_cancel [iff]
   5.233 -
   5.234 -lemma hcomplex_add_right_cancel: "(y + (x::hcomplex)= z + x) = (y = z)"
   5.235 -apply (rule Ring_and_Field.add_right_cancel)
   5.236 -done
   5.237 -declare hcomplex_add_right_cancel [iff]
   5.238  
   5.239  subsection{*More Multiplication Laws*}
   5.240  
   5.241 -lemma hcomplex_mult_left_commute: "(x::hcomplex) * (y * z) = y * (x * z)"
   5.242 -apply (rule Ring_and_Field.mult_left_commute)
   5.243 -done
   5.244 -
   5.245 -lemmas hcomplex_mult_ac = hcomplex_mult_assoc hcomplex_mult_commute
   5.246 -                          hcomplex_mult_left_commute
   5.247 -
   5.248  lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
   5.249  apply (rule Ring_and_Field.mult_1_right)
   5.250  done
   5.251  
   5.252 -lemma hcomplex_mult_zero_right: "z * (0::hcomplex) = 0"
   5.253 -apply (rule Ring_and_Field.mult_right_zero)
   5.254 -done
   5.255 -
   5.256 -lemma hcomplex_minus_mult_eq1: "-(x * y) = -x * (y::hcomplex)"
   5.257 -apply (rule Ring_and_Field.minus_mult_left)
   5.258 -done
   5.259 -
   5.260 -declare hcomplex_minus_mult_eq1 [symmetric, simp] 
   5.261 -
   5.262 -lemma hcomplex_minus_mult_eq2: "-(x * y) = x * -(y::hcomplex)"
   5.263 -apply (rule Ring_and_Field.minus_mult_right)
   5.264 -done
   5.265 -
   5.266 -declare hcomplex_minus_mult_eq2 [symmetric, simp]
   5.267 -
   5.268  lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
   5.269  apply (simp (no_asm))
   5.270  done
   5.271 @@ -574,26 +545,13 @@
   5.272  done
   5.273  declare hcomplex_mult_minus_one_right [simp]
   5.274  
   5.275 -lemma hcomplex_add_mult_distrib2: "(w::hcomplex) * (z1 + z2) = (w * z1) + (w * z2)"
   5.276 -apply (rule Ring_and_Field.right_distrib)
   5.277 -done
   5.278 -
   5.279 -lemma hcomplex_mult_right_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)"
   5.280 -apply (simp add: Ring_and_Field.field_mult_cancel_right); 
   5.281 -done
   5.282 +lemma hcomplex_mult_left_cancel:
   5.283 +     "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)"
   5.284 +by (simp add: field_mult_cancel_left) 
   5.285  
   5.286 -lemma hcomplex_inverse_not_zero: "z ~= (0::hcomplex) ==> inverse(z) ~= 0"
   5.287 -apply (simp add: ); 
   5.288 -done
   5.289 -
   5.290 -lemma hcomplex_mult_not_zero: "[| x ~= (0::hcomplex); y ~= 0 |] ==> x * y ~= 0"
   5.291 -apply (simp add: Ring_and_Field.field_mult_eq_0_iff); 
   5.292 -done
   5.293 -
   5.294 -lemmas hcomplex_mult_not_zeroE = hcomplex_mult_not_zero [THEN notE, standard]
   5.295 -
   5.296 -lemma hcomplex_minus_inverse: "inverse(-x) = -inverse(x::hcomplex)"
   5.297 -apply (rule Ring_and_Field.inverse_minus_eq) 
   5.298 +lemma hcomplex_mult_right_cancel:
   5.299 +     "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)"
   5.300 +apply (simp add: Ring_and_Field.field_mult_cancel_right); 
   5.301  done
   5.302  
   5.303  
   5.304 @@ -633,22 +591,26 @@
   5.305  apply (auto simp add: hcomplex_of_hypreal)
   5.306  done
   5.307  
   5.308 -lemma hcomplex_of_hypreal_cancel_iff: "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
   5.309 +lemma hcomplex_of_hypreal_cancel_iff:
   5.310 +     "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
   5.311  apply (auto dest: inj_hcomplex_of_hypreal [THEN injD])
   5.312  done
   5.313  declare hcomplex_of_hypreal_cancel_iff [iff]
   5.314  
   5.315 -lemma hcomplex_of_hypreal_minus: "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
   5.316 +lemma hcomplex_of_hypreal_minus:
   5.317 +     "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
   5.318  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.319  apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
   5.320  done
   5.321  
   5.322 -lemma hcomplex_of_hypreal_inverse: "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
   5.323 +lemma hcomplex_of_hypreal_inverse:
   5.324 +     "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
   5.325  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.326  apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
   5.327  done
   5.328  
   5.329 -lemma hcomplex_of_hypreal_add: "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
   5.330 +lemma hcomplex_of_hypreal_add:
   5.331 +     "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
   5.332        hcomplex_of_hypreal (x + y)"
   5.333  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.334  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.335 @@ -662,18 +624,20 @@
   5.336  apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
   5.337  done
   5.338  
   5.339 -lemma hcomplex_of_hypreal_mult: "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
   5.340 +lemma hcomplex_of_hypreal_mult:
   5.341 +     "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
   5.342        hcomplex_of_hypreal (x * y)"
   5.343  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.344  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.345 -apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
   5.346 +apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult 
   5.347 +                      complex_of_real_mult)
   5.348  done
   5.349  
   5.350  lemma hcomplex_of_hypreal_divide:
   5.351    "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
   5.352  apply (unfold hcomplex_divide_def)
   5.353  apply (case_tac "y=0")
   5.354 -apply (simp (no_asm_simp) add: HYPREAL_DIVISION_BY_ZERO HYPREAL_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO)
   5.355 +apply (simp)
   5.356  apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
   5.357  apply (simp (no_asm) add: hypreal_divide_def)
   5.358  done
   5.359 @@ -722,7 +686,7 @@
   5.360  
   5.361  apply (unfold hcmod_def)
   5.362  apply (rule_tac f = "Abs_hypreal" in arg_cong)
   5.363 -apply (auto , ultra)
   5.364 +apply (auto, ultra)
   5.365  done
   5.366  
   5.367  lemma hcmod_zero [simp]:
   5.368 @@ -744,7 +708,8 @@
   5.369  done
   5.370  declare hcmod_hcomplex_of_hypreal [simp]
   5.371  
   5.372 -lemma hcomplex_of_hypreal_abs: "hcomplex_of_hypreal (abs x) =
   5.373 +lemma hcomplex_of_hypreal_abs:
   5.374 +     "hcomplex_of_hypreal (abs x) =
   5.375        hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
   5.376  apply (simp (no_asm))
   5.377  done
   5.378 @@ -757,7 +722,7 @@
   5.379     Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
   5.380  apply (unfold hcnj_def)
   5.381  apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   5.382 -apply (auto , ultra)
   5.383 +apply (auto, ultra)
   5.384  done
   5.385  
   5.386  lemma inj_hcnj: "inj hcnj"
   5.387 @@ -778,7 +743,8 @@
   5.388  done
   5.389  declare hcomplex_hcnj_hcnj [simp]
   5.390  
   5.391 -lemma hcomplex_hcnj_hcomplex_of_hypreal: "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
   5.392 +lemma hcomplex_hcnj_hcomplex_of_hypreal:
   5.393 +     "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
   5.394  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.395  apply (auto simp add: hcnj hcomplex_of_hypreal)
   5.396  done
   5.397 @@ -864,42 +830,14 @@
   5.398  done
   5.399  declare hcomplex_hcnj_zero_iff [iff]
   5.400  
   5.401 -lemma hcomplex_mult_hcnj: "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
   5.402 +lemma hcomplex_mult_hcnj:
   5.403 +     "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
   5.404  apply (rule_tac z = "z" in eq_Abs_hcomplex)
   5.405  apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2)
   5.406  done
   5.407  
   5.408  
   5.409  (*---------------------------------------------------------------------------*)
   5.410 -(*  some algebra etc.                                                        *)
   5.411 -(*---------------------------------------------------------------------------*)
   5.412 -
   5.413 -lemma hcomplex_mult_zero_iff: "(x*y = (0::hcomplex)) = (x = 0 | y = 0)"
   5.414 -apply auto
   5.415 -apply (auto intro: ccontr dest: hcomplex_mult_not_zero)
   5.416 -done
   5.417 -declare hcomplex_mult_zero_iff [simp]
   5.418 -
   5.419 -lemma hcomplex_add_left_cancel_zero: "(x + y = x) = (y = (0::hcomplex))"
   5.420 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   5.421 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   5.422 -apply (auto simp add: hcomplex_add hcomplex_zero_def)
   5.423 -done
   5.424 -declare hcomplex_add_left_cancel_zero [simp]
   5.425 -
   5.426 -lemma hcomplex_diff_mult_distrib:
   5.427 -      "((z1::hcomplex) - z2) * w = (z1 * w) - (z2 * w)"
   5.428 -apply (unfold hcomplex_diff_def)
   5.429 -apply (simp (no_asm) add: hcomplex_add_mult_distrib)
   5.430 -done
   5.431 -
   5.432 -lemma hcomplex_diff_mult_distrib2:
   5.433 -      "(w::hcomplex) * (z1 - z2) = (w * z1) - (w * z2)"
   5.434 -apply (unfold hcomplex_diff_def)
   5.435 -apply (simp (no_asm) add: hcomplex_add_mult_distrib2)
   5.436 -done
   5.437 -
   5.438 -(*---------------------------------------------------------------------------*)
   5.439  (*  More theorems about hcmod                                                *)
   5.440  (*---------------------------------------------------------------------------*)
   5.441  
   5.442 @@ -909,36 +847,14 @@
   5.443  done
   5.444  declare hcomplex_hcmod_eq_zero_cancel [simp]
   5.445  
   5.446 -(* not proved already? strange! *)
   5.447 -lemma hypreal_of_nat_le_iff:
   5.448 -      "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)"
   5.449 -apply (unfold hypreal_le_def)
   5.450 -apply auto
   5.451 -done
   5.452 -declare hypreal_of_nat_le_iff [simp]
   5.453 -
   5.454 -lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n"
   5.455 -apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
   5.456 -         del: hypreal_of_nat_zero)
   5.457 -done
   5.458 -declare hypreal_of_nat_ge_zero [simp]
   5.459 -
   5.460 -declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
   5.461 -
   5.462 -lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n"
   5.463 -apply (rule_tac z = "n" in eq_Abs_hypnat)
   5.464 -apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
   5.465 -done
   5.466 -declare hypreal_of_hypnat_ge_zero [simp]
   5.467 -
   5.468 -declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp]
   5.469 -
   5.470 -lemma hcmod_hcomplex_of_hypreal_of_nat: "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
   5.471 +lemma hcmod_hcomplex_of_hypreal_of_nat:
   5.472 +     "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
   5.473  apply auto
   5.474  done
   5.475  declare hcmod_hcomplex_of_hypreal_of_nat [simp]
   5.476  
   5.477 -lemma hcmod_hcomplex_of_hypreal_of_hypnat: "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
   5.478 +lemma hcmod_hcomplex_of_hypreal_of_hypnat:
   5.479 +     "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
   5.480  apply auto
   5.481  done
   5.482  declare hcmod_hcomplex_of_hypreal_of_hypnat [simp]
   5.483 @@ -1025,7 +941,8 @@
   5.484  apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute)
   5.485  done
   5.486  
   5.487 -lemma hcmod_add_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
   5.488 +lemma hcmod_add_less:
   5.489 +     "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
   5.490  apply (rule_tac z = "x" in eq_Abs_hcomplex)
   5.491  apply (rule_tac z = "y" in eq_Abs_hcomplex)
   5.492  apply (rule_tac z = "r" in eq_Abs_hypreal)
   5.493 @@ -1035,7 +952,8 @@
   5.494  apply (auto intro: complex_mod_add_less)
   5.495  done
   5.496  
   5.497 -lemma hcmod_mult_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
   5.498 +lemma hcmod_mult_less:
   5.499 +     "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
   5.500  apply (rule_tac z = "x" in eq_Abs_hcomplex)
   5.501  apply (rule_tac z = "y" in eq_Abs_hcomplex)
   5.502  apply (rule_tac z = "r" in eq_Abs_hypreal)
   5.503 @@ -1062,10 +980,11 @@
   5.504     Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
   5.505  apply (unfold hcpow_def)
   5.506  apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   5.507 -apply (auto , ultra)
   5.508 +apply (auto, ultra)
   5.509  done
   5.510  
   5.511 -lemma hcomplex_of_hypreal_hyperpow: "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
   5.512 +lemma hcomplex_of_hypreal_hyperpow:
   5.513 +     "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
   5.514  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.515  apply (rule_tac z = "n" in eq_Abs_hypnat)
   5.516  apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
   5.517 @@ -1082,12 +1001,14 @@
   5.518  apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow)
   5.519  done
   5.520  
   5.521 -lemma hcomplexpow_minus: "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
   5.522 +lemma hcomplexpow_minus:
   5.523 +     "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
   5.524  apply (induct_tac "n")
   5.525  apply auto
   5.526  done
   5.527  
   5.528 -lemma hcpow_minus: "(-x::hcomplex) hcpow n =
   5.529 +lemma hcpow_minus:
   5.530 +     "(-x::hcomplex) hcpow n =
   5.531        (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
   5.532  apply (rule_tac z = "x" in eq_Abs_hcomplex)
   5.533  apply (rule_tac z = "n" in eq_Abs_hypnat)
   5.534 @@ -1129,7 +1050,7 @@
   5.535  
   5.536  lemma hcomplexpow_mult: "((r::hcomplex) * s) ^ n = (r ^ n) * (s ^ n)"
   5.537  apply (induct_tac "n")
   5.538 -apply (auto simp add: hcomplex_mult_ac)
   5.539 +apply (auto simp add: mult_ac)
   5.540  done
   5.541  
   5.542  lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
   5.543 @@ -1159,9 +1080,10 @@
   5.544  done
   5.545  declare hcpow_zero2 [simp]
   5.546  
   5.547 -lemma hcomplexpow_not_zero [rule_format (no_asm)]: "r ~= (0::hcomplex) --> r ^ n ~= 0"
   5.548 +lemma hcomplexpow_not_zero [rule_format (no_asm)]:
   5.549 +     "r ~= (0::hcomplex) --> r ^ n ~= 0"
   5.550  apply (induct_tac "n")
   5.551 -apply (auto simp add: hcomplex_mult_not_zero)
   5.552 +apply (auto)
   5.553  done
   5.554  declare hcomplexpow_not_zero [simp]
   5.555  declare hcomplexpow_not_zero [intro]
   5.556 @@ -1209,7 +1131,8 @@
   5.557  apply auto
   5.558  done
   5.559  
   5.560 -lemma hcomplex_mult_not_eq_zero_iff: "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)"
   5.561 +lemma hcomplex_mult_not_eq_zero_iff:
   5.562 +     "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)"
   5.563  apply auto
   5.564  done
   5.565  declare hcomplex_mult_not_eq_zero_iff [iff]
   5.566 @@ -1229,7 +1152,7 @@
   5.567        Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
   5.568  apply (unfold hsgn_def)
   5.569  apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   5.570 -apply (auto , ultra)
   5.571 +apply (auto, ultra)
   5.572  done
   5.573  
   5.574  lemma hsgn_zero: "hsgn 0 = 0"
   5.575 @@ -1255,7 +1178,8 @@
   5.576  apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
   5.577  done
   5.578  
   5.579 -lemma lemma_hypreal_P_EX2: "(EX (x::hypreal) y. P x y) =
   5.580 +lemma lemma_hypreal_P_EX2:
   5.581 +     "(EX (x::hypreal) y. P x y) =
   5.582        (EX f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
   5.583  apply auto
   5.584  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.585 @@ -1263,36 +1187,41 @@
   5.586  apply auto
   5.587  done
   5.588  
   5.589 -lemma complex_split2: "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
   5.590 +lemma complex_split2:
   5.591 +     "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
   5.592  apply (blast intro: complex_split)
   5.593  done
   5.594  
   5.595  (* Interesting proof! *)
   5.596 -lemma hcomplex_split: "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
   5.597 +lemma hcomplex_split:
   5.598 +     "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
   5.599  apply (rule_tac z = "z" in eq_Abs_hcomplex)
   5.600  apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
   5.601  apply (cut_tac z = "x" in complex_split2)
   5.602 -apply (drule choice , safe)+
   5.603 +apply (drule choice, safe)+
   5.604  apply (rule_tac x = "f" in exI)
   5.605  apply (rule_tac x = "fa" in exI)
   5.606  apply auto
   5.607  done
   5.608  
   5.609 -lemma hRe_hcomplex_i: "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
   5.610 +lemma hRe_hcomplex_i:
   5.611 +     "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
   5.612  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.613  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.614  apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   5.615  done
   5.616  declare hRe_hcomplex_i [simp]
   5.617  
   5.618 -lemma hIm_hcomplex_i: "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
   5.619 +lemma hIm_hcomplex_i:
   5.620 +     "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
   5.621  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.622  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.623  apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   5.624  done
   5.625  declare hIm_hcomplex_i [simp]
   5.626  
   5.627 -lemma hcmod_i: "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
   5.628 +lemma hcmod_i:
   5.629 +     "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
   5.630        ( *f* sqrt) (x ^ 2 + y ^ 2)"
   5.631  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.632  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.633 @@ -1325,52 +1254,60 @@
   5.634  apply (ultra)
   5.635  done
   5.636  
   5.637 -lemma hcomplex_eq_cancel_iff: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
   5.638 +lemma hcomplex_eq_cancel_iff:
   5.639 +     "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
   5.640         hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
   5.641        ((xa = xb) & (ya = yb))"
   5.642  apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
   5.643  done
   5.644  declare hcomplex_eq_cancel_iff [simp]
   5.645  
   5.646 -lemma hcomplex_eq_cancel_iffA: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
   5.647 +lemma hcomplex_eq_cancel_iffA:
   5.648 +     "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
   5.649         hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))"
   5.650  apply (auto simp add: hcomplex_mult_commute)
   5.651  done
   5.652  declare hcomplex_eq_cancel_iffA [iff]
   5.653  
   5.654 -lemma hcomplex_eq_cancel_iffB: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
   5.655 +lemma hcomplex_eq_cancel_iffB:
   5.656 +     "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
   5.657         hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
   5.658  apply (auto simp add: hcomplex_mult_commute)
   5.659  done
   5.660  declare hcomplex_eq_cancel_iffB [iff]
   5.661  
   5.662 -lemma hcomplex_eq_cancel_iffC: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
   5.663 +lemma hcomplex_eq_cancel_iffC:
   5.664 +     "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
   5.665         hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
   5.666  apply (auto simp add: hcomplex_mult_commute)
   5.667  done
   5.668  declare hcomplex_eq_cancel_iffC [iff]
   5.669  
   5.670 -lemma hcomplex_eq_cancel_iff2: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
   5.671 +lemma hcomplex_eq_cancel_iff2:
   5.672 +     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
   5.673        hcomplex_of_hypreal xa) = (x = xa & y = 0)"
   5.674  apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff)
   5.675  apply (simp del: hcomplex_eq_cancel_iff)
   5.676  done
   5.677  declare hcomplex_eq_cancel_iff2 [simp]
   5.678  
   5.679 -lemma hcomplex_eq_cancel_iff2a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
   5.680 +lemma hcomplex_eq_cancel_iff2a:
   5.681 +     "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
   5.682        hcomplex_of_hypreal xa) = (x = xa & y = 0)"
   5.683  apply (auto simp add: hcomplex_mult_commute)
   5.684  done
   5.685  declare hcomplex_eq_cancel_iff2a [simp]
   5.686  
   5.687 -lemma hcomplex_eq_cancel_iff3: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
   5.688 +lemma hcomplex_eq_cancel_iff3:
   5.689 +     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
   5.690        iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
   5.691  apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff)
   5.692  apply (simp del: hcomplex_eq_cancel_iff)
   5.693  done
   5.694  declare hcomplex_eq_cancel_iff3 [simp]
   5.695  
   5.696 -lemma hcomplex_eq_cancel_iff3a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
   5.697 +lemma hcomplex_eq_cancel_iff3a:
   5.698 +     "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
   5.699        iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
   5.700  apply (auto simp add: hcomplex_mult_commute)
   5.701  done
   5.702 @@ -1410,12 +1347,14 @@
   5.703  done
   5.704  declare hIm_hsgn [simp]
   5.705  
   5.706 -lemma real_two_squares_add_zero_iff: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
   5.707 +lemma real_two_squares_add_zero_iff:
   5.708 +     "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
   5.709  apply (auto intro: real_sum_squares_cancel)
   5.710  done
   5.711  declare real_two_squares_add_zero_iff [simp]
   5.712  
   5.713 -lemma hcomplex_inverse_complex_split: "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
   5.714 +lemma hcomplex_inverse_complex_split:
   5.715 +     "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
   5.716        hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
   5.717        iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
   5.718  apply (rule_tac z = "x" in eq_Abs_hypreal)
   5.719 @@ -1460,24 +1399,27 @@
   5.720  
   5.721  apply (unfold harg_def)
   5.722  apply (rule_tac f = "Abs_hypreal" in arg_cong)
   5.723 -apply (auto , ultra)
   5.724 +apply (auto, ultra)
   5.725  done
   5.726  
   5.727 -lemma cos_harg_i_mult_zero: "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   5.728 +lemma cos_harg_i_mult_zero:
   5.729 +     "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   5.730  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.731  apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
   5.732  apply (ultra)
   5.733  done
   5.734  declare cos_harg_i_mult_zero [simp]
   5.735  
   5.736 -lemma cos_harg_i_mult_zero2: "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   5.737 +lemma cos_harg_i_mult_zero2:
   5.738 +     "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   5.739  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.740  apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
   5.741  apply (ultra)
   5.742  done
   5.743  declare cos_harg_i_mult_zero2 [simp]
   5.744  
   5.745 -lemma hcomplex_of_hypreal_not_zero_iff: "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)"
   5.746 +lemma hcomplex_of_hypreal_not_zero_iff:
   5.747 +     "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)"
   5.748  apply (rule_tac z = "y" in eq_Abs_hypreal)
   5.749  apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
   5.750  done
   5.751 @@ -1489,7 +1431,8 @@
   5.752  done
   5.753  declare hcomplex_of_hypreal_zero_iff [simp]
   5.754  
   5.755 -lemma cos_harg_i_mult_zero3: "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   5.756 +lemma cos_harg_i_mult_zero3:
   5.757 +     "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   5.758  apply (cut_tac x = "y" and y = "0" in hypreal_linear)
   5.759  apply auto
   5.760  done
   5.761 @@ -1499,7 +1442,8 @@
   5.762  (* Polar form for nonstandard complex numbers                                 *)
   5.763  (*---------------------------------------------------------------------------*)
   5.764  
   5.765 -lemma complex_split_polar2: "ALL n. EX r a. (z n) = complex_of_real r *
   5.766 +lemma complex_split_polar2:
   5.767 +     "ALL n. EX r a. (z n) = complex_of_real r *
   5.768        (complex_of_real(cos a) + ii * complex_of_real(sin a))"
   5.769  apply (blast intro: complex_split_polar)
   5.770  done
   5.771 @@ -1510,7 +1454,7 @@
   5.772  apply (rule_tac z = "z" in eq_Abs_hcomplex)
   5.773  apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
   5.774  apply (cut_tac z = "x" in complex_split_polar2)
   5.775 -apply (drule choice , safe)+
   5.776 +apply (drule choice, safe)+
   5.777  apply (rule_tac x = "f" in exI)
   5.778  apply (rule_tac x = "fa" in exI)
   5.779  apply auto
   5.780 @@ -1545,10 +1489,11 @@
   5.781  apply (rule hcomplex_split_polar)
   5.782  done
   5.783  
   5.784 -lemma hRe_hcomplex_polar: "hRe(hcomplex_of_hypreal r *
   5.785 +lemma hRe_hcomplex_polar:
   5.786 +     "hRe(hcomplex_of_hypreal r *
   5.787        (hcomplex_of_hypreal(( *f* cos) a) +
   5.788         iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
   5.789 -apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac)
   5.790 +apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
   5.791  done
   5.792  declare hRe_hcomplex_polar [simp]
   5.793  
   5.794 @@ -1558,10 +1503,11 @@
   5.795  done
   5.796  declare hRe_hrcis [simp]
   5.797  
   5.798 -lemma hIm_hcomplex_polar: "hIm(hcomplex_of_hypreal r *
   5.799 +lemma hIm_hcomplex_polar:
   5.800 +     "hIm(hcomplex_of_hypreal r *
   5.801        (hcomplex_of_hypreal(( *f* cos) a) +
   5.802         iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
   5.803 -apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac)
   5.804 +apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
   5.805  done
   5.806  declare hIm_hcomplex_polar [simp]
   5.807  
   5.808 @@ -1571,7 +1517,8 @@
   5.809  done
   5.810  declare hIm_hrcis [simp]
   5.811  
   5.812 -lemma hcmod_complex_polar: "hcmod (hcomplex_of_hypreal r *
   5.813 +lemma hcmod_complex_polar:
   5.814 +     "hcmod (hcomplex_of_hypreal r *
   5.815        (hcomplex_of_hypreal(( *f* cos) a) +
   5.816         iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
   5.817  apply (rule_tac z = "r" in eq_Abs_hypreal)
   5.818 @@ -1656,7 +1603,8 @@
   5.819  apply (auto simp add: hcis_hypreal_of_nat_Suc_mult)
   5.820  done
   5.821  
   5.822 -lemma hcis_hypreal_of_hypnat_Suc_mult: "hcis (hypreal_of_hypnat (n + 1) * a) =
   5.823 +lemma hcis_hypreal_of_hypnat_Suc_mult:
   5.824 +     "hcis (hypreal_of_hypnat (n + 1) * a) =
   5.825        hcis a * hcis (hypreal_of_hypnat n * a)"
   5.826  apply (rule_tac z = "a" in eq_Abs_hypreal)
   5.827  apply (rule_tac z = "n" in eq_Abs_hypnat)
   5.828 @@ -1708,19 +1656,23 @@
   5.829  done
   5.830  declare hIm_hcis [simp]
   5.831  
   5.832 -lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
   5.833 +lemma cos_n_hRe_hcis_pow_n:
   5.834 +     "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
   5.835  apply (auto simp add: NSDeMoivre)
   5.836  done
   5.837  
   5.838 -lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
   5.839 +lemma sin_n_hIm_hcis_pow_n:
   5.840 +     "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
   5.841  apply (auto simp add: NSDeMoivre)
   5.842  done
   5.843  
   5.844 -lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
   5.845 +lemma cos_n_hRe_hcis_hcpow_n:
   5.846 +     "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
   5.847  apply (auto simp add: NSDeMoivre_ext)
   5.848  done
   5.849  
   5.850 -lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
   5.851 +lemma sin_n_hIm_hcis_hcpow_n:
   5.852 +     "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
   5.853  apply (auto simp add: NSDeMoivre_ext)
   5.854  done
   5.855  
   5.856 @@ -1755,7 +1707,8 @@
   5.857  done
   5.858  declare hcomplex_of_complex_eq_iff [simp]
   5.859  
   5.860 -lemma hcomplex_of_complex_minus: "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
   5.861 +lemma hcomplex_of_complex_minus:
   5.862 +     "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
   5.863  apply (unfold hcomplex_of_complex_def)
   5.864  apply (auto simp add: hcomplex_minus)
   5.865  done
   5.866 @@ -1777,7 +1730,8 @@
   5.867  apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
   5.868  done
   5.869  
   5.870 -lemma hcomplex_of_complex_inverse: "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
   5.871 +lemma hcomplex_of_complex_inverse:
   5.872 +     "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
   5.873  apply (case_tac "r=0")
   5.874  apply (simp (no_asm_simp) add: COMPLEX_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO hcomplex_of_complex_zero COMPLEX_DIVIDE_ZERO)
   5.875  apply (rule_tac c1 = "hcomplex_of_complex r" in hcomplex_mult_left_cancel [THEN iffD1])
   5.876 @@ -1787,7 +1741,8 @@
   5.877  done
   5.878  declare hcomplex_of_complex_inverse [simp]
   5.879  
   5.880 -lemma hcomplex_of_complex_divide: "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
   5.881 +lemma hcomplex_of_complex_divide:
   5.882 +     "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
   5.883  apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def)
   5.884  done
   5.885  declare hcomplex_of_complex_divide [simp]
   5.886 @@ -1848,7 +1803,6 @@
   5.887  val hcomplex_add = thm"hcomplex_add";
   5.888  val hcomplex_add_commute = thm"hcomplex_add_commute";
   5.889  val hcomplex_add_assoc = thm"hcomplex_add_assoc";
   5.890 -val hcomplex_add_left_commute = thm"hcomplex_add_left_commute";
   5.891  val hcomplex_add_zero_left = thm"hcomplex_add_zero_left";
   5.892  val hcomplex_add_zero_right = thm"hcomplex_add_zero_right";
   5.893  val hRe_add = thm"hRe_add";
   5.894 @@ -1860,25 +1814,17 @@
   5.895  val hRe_minus = thm"hRe_minus";
   5.896  val hIm_minus = thm"hIm_minus";
   5.897  val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus";
   5.898 -val hcomplex_minus_add_distrib = thm"hcomplex_minus_add_distrib";
   5.899 -val hcomplex_add_left_cancel = thm"hcomplex_add_left_cancel";
   5.900 -val hcomplex_add_right_cancel = thm"hcomplex_add_right_cancel";
   5.901  val hcomplex_diff = thm"hcomplex_diff";
   5.902  val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq";
   5.903  val hcomplex_mult = thm"hcomplex_mult";
   5.904  val hcomplex_mult_commute = thm"hcomplex_mult_commute";
   5.905  val hcomplex_mult_assoc = thm"hcomplex_mult_assoc";
   5.906 -val hcomplex_mult_left_commute = thm"hcomplex_mult_left_commute";
   5.907  val hcomplex_mult_one_left = thm"hcomplex_mult_one_left";
   5.908  val hcomplex_mult_one_right = thm"hcomplex_mult_one_right";
   5.909  val hcomplex_mult_zero_left = thm"hcomplex_mult_zero_left";
   5.910 -val hcomplex_mult_zero_right = thm"hcomplex_mult_zero_right";
   5.911 -val hcomplex_minus_mult_eq1 = thm"hcomplex_minus_mult_eq1";
   5.912 -val hcomplex_minus_mult_eq2 = thm"hcomplex_minus_mult_eq2";
   5.913  val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
   5.914  val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
   5.915  val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
   5.916 -val hcomplex_add_mult_distrib2 = thm"hcomplex_add_mult_distrib2";
   5.917  val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
   5.918  val hcomplex_inverse = thm"hcomplex_inverse";
   5.919  val HCOMPLEX_INVERSE_ZERO = thm"HCOMPLEX_INVERSE_ZERO";
   5.920 @@ -1886,10 +1832,6 @@
   5.921  val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
   5.922  val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
   5.923  val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
   5.924 -val hcomplex_inverse_not_zero = thm"hcomplex_inverse_not_zero";
   5.925 -val hcomplex_mult_not_zero = thm"hcomplex_mult_not_zero";
   5.926 -val hcomplex_mult_not_zeroE = thm"hcomplex_mult_not_zeroE";
   5.927 -val hcomplex_minus_inverse = thm"hcomplex_minus_inverse";
   5.928  val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
   5.929  val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
   5.930  val inj_hcomplex_of_hypreal = thm"inj_hcomplex_of_hypreal";
   5.931 @@ -1928,10 +1870,6 @@
   5.932  val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero";
   5.933  val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
   5.934  val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
   5.935 -val hcomplex_mult_zero_iff = thm"hcomplex_mult_zero_iff";
   5.936 -val hcomplex_add_left_cancel_zero = thm"hcomplex_add_left_cancel_zero";
   5.937 -val hcomplex_diff_mult_distrib = thm"hcomplex_diff_mult_distrib";
   5.938 -val hcomplex_diff_mult_distrib2 = thm"hcomplex_diff_mult_distrib2";
   5.939  val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
   5.940  val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
   5.941  val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
   5.942 @@ -2065,9 +2003,6 @@
   5.943  val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex";
   5.944  val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex";
   5.945  val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex";
   5.946 -
   5.947 -val hcomplex_add_ac = thms"hcomplex_add_ac";
   5.948 -val hcomplex_mult_ac = thms"hcomplex_mult_ac";
   5.949  *}
   5.950  
   5.951  end
     6.1 --- a/src/HOL/Complex/NSComplexArith.thy	Thu Jan 01 10:06:32 2004 +0100
     6.2 +++ b/src/HOL/Complex/NSComplexArith.thy	Thu Jan 01 21:47:07 2004 +0100
     6.3 @@ -14,6 +14,6 @@
     6.4  by simp
     6.5  
     6.6  lemma hcomplex_minus1_divide [simp]: "-1/(x::hcomplex) = - (1/x)"
     6.7 -by (simp add: hcomplex_divide_def hcomplex_minus_inverse)
     6.8 +by (simp add: hcomplex_divide_def inverse_minus_eq)
     6.9  
    6.10  end
     7.1 --- a/src/HOL/Complex/NSComplexBin.ML	Thu Jan 01 10:06:32 2004 +0100
     7.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Thu Jan 01 21:47:07 2004 +0100
     7.3 @@ -152,7 +152,7 @@
     7.4  
     7.5  Goal "number_of v + (c - number_of w) = \
     7.6  \     number_of (bin_add v (bin_minus w)) + (c::hcomplex)";
     7.7 -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]@ hcomplex_add_ac));
     7.8 +by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]@ add_ac));
     7.9  qed "hcomplex_add_number_of_diff2";
    7.10  
    7.11  Addsimps [hcomplex_add_number_of_left, hcomplex_mult_number_of_left,
    7.12 @@ -171,7 +171,7 @@
    7.13  
    7.14  Goal "i*u + (j*u + k) = (i+j)*u + (k::hcomplex)";
    7.15  by (asm_simp_tac (simpset() addsimps [hcomplex_add_mult_distrib]
    7.16 -    @ hcomplex_add_ac) 1);
    7.17 +    @ add_ac) 1);
    7.18  qed "left_hcomplex_add_mult_distrib";
    7.19  
    7.20  (** For cancel_numerals **)
    7.21 @@ -188,7 +188,7 @@
    7.22  
    7.23  Goal "!!i::hcomplex. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    7.24  by (auto_tac (claset(), simpset() addsimps [hcomplex_add_mult_distrib,
    7.25 -    hcomplex_diff_def] @ hcomplex_add_ac));
    7.26 +    hcomplex_diff_def] @ add_ac));
    7.27  by (asm_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 1);
    7.28  by (simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1);
    7.29  qed "hcomplex_eq_add_iff1";
    7.30 @@ -309,29 +309,27 @@
    7.31  
    7.32  
    7.33  (*To let us treat subtraction as addition*)
    7.34 -val diff_simps = [hcomplex_diff_def, hcomplex_minus_add_distrib, 
    7.35 -                  minus_minus];
    7.36 +val diff_simps = [hcomplex_diff_def, minus_add_distrib, minus_minus];
    7.37  
    7.38  (*push the unary minus down: - x * y = x * - y *)
    7.39  val hcomplex_minus_mult_eq_1_to_2 = 
    7.40 -    [hcomplex_minus_mult_eq1 RS sym, hcomplex_minus_mult_eq2] MRS trans 
    7.41 +    [minus_mult_left RS sym, minus_mult_right] MRS trans 
    7.42      |> standard;
    7.43  
    7.44  (*to extract again any uncancelled minuses*)
    7.45  val hcomplex_minus_from_mult_simps = 
    7.46 -    [minus_minus, hcomplex_minus_mult_eq1 RS sym, 
    7.47 -     hcomplex_minus_mult_eq2 RS sym];
    7.48 +    [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
    7.49  
    7.50  (*combine unary minus with numeric literals, however nested within a product*)
    7.51  val hcomplex_mult_minus_simps =
    7.52 -    [hcomplex_mult_assoc, hcomplex_minus_mult_eq1, hcomplex_minus_mult_eq_1_to_2];
    7.53 +    [hcomplex_mult_assoc, minus_mult_left, hcomplex_minus_mult_eq_1_to_2];
    7.54  
    7.55  (*Final simplification: cancel + and *  *)
    7.56  val simplify_meta_eq = 
    7.57      Int_Numeral_Simprocs.simplify_meta_eq
    7.58 -         [hcomplex_add_zero_left, hcomplex_add_zero_right,
    7.59 - 	  hcomplex_mult_zero_left, hcomplex_mult_zero_right, hcomplex_mult_one_left, 
    7.60 -          hcomplex_mult_one_right];
    7.61 +         [add_zero_left, add_zero_right,
    7.62 + 	  mult_left_zero, mult_right_zero, mult_1, 
    7.63 +          mult_1_right];
    7.64  
    7.65  val prep_simproc = Complex_Numeral_Simprocs.prep_simproc;
    7.66  
    7.67 @@ -346,11 +344,11 @@
    7.68    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    7.69    val norm_tac = 
    7.70       ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    7.71 -                                         hcomplex_minus_simps@hcomplex_add_ac))
    7.72 +                                         hcomplex_minus_simps@add_ac))
    7.73       THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
    7.74       THEN ALLGOALS
    7.75                (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
    7.76 -                                         hcomplex_add_ac@hcomplex_mult_ac))
    7.77 +                                         add_ac@mult_ac))
    7.78    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    7.79    val simplify_meta_eq  = simplify_meta_eq
    7.80    end;
    7.81 @@ -386,10 +384,10 @@
    7.82    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    7.83    val norm_tac = 
    7.84       ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    7.85 -                                         hcomplex_minus_simps@hcomplex_add_ac))
    7.86 +                                         hcomplex_minus_simps@add_ac))
    7.87       THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
    7.88       THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
    7.89 -                                              hcomplex_add_ac@hcomplex_mult_ac))
    7.90 +                                              add_ac@mult_ac))
    7.91    val numeral_simp_tac	= ALLGOALS 
    7.92                      (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    7.93    val simplify_meta_eq  = simplify_meta_eq
    7.94 @@ -501,7 +499,7 @@
    7.95    val sg_ref    = Sign.self_ref (Theory.sign_of (the_context ()))
    7.96    val T	     = HComplex_Numeral_Simprocs.hcomplexT
    7.97    val plus   = Const ("op *", [T,T] ---> T)
    7.98 -  val add_ac = hcomplex_mult_ac
    7.99 +  val add_ac = mult_ac
   7.100  end;
   7.101  
   7.102  structure HComplex_Times_Assoc = Assoc_Fold (HComplex_Times_Assoc_Data);
     8.1 --- a/src/HOL/Complex/hcomplex_arith.ML	Thu Jan 01 10:06:32 2004 +0100
     8.2 +++ b/src/HOL/Complex/hcomplex_arith.ML	Thu Jan 01 21:47:07 2004 +0100
     8.3 @@ -19,7 +19,7 @@
     8.4    val trans_tac         = Real_Numeral_Simprocs.trans_tac
     8.5    val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps @ mult_1s))
     8.6                   THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
     8.7 -                 THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_mult_ac))
     8.8 +                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
     8.9    val numeral_simp_tac	= 
    8.10           ALLGOALS (simp_tac (HOL_ss addsimps rel_hcomplex_number_of@bin_simps))
    8.11    val simplify_meta_eq  = simplify_meta_eq
    8.12 @@ -107,7 +107,7 @@
    8.13    val dest_coeff	= dest_coeff
    8.14    val find_first	= find_first []
    8.15    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    8.16 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hcomplex_mult_ac))
    8.17 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    8.18    end;
    8.19  
    8.20  
     9.1 --- a/src/HOL/IsaMakefile	Thu Jan 01 10:06:32 2004 +0100
     9.2 +++ b/src/HOL/IsaMakefile	Thu Jan 01 21:47:07 2004 +0100
     9.3 @@ -139,7 +139,7 @@
     9.4    Real/Complex_Numbers.thy \
     9.5    Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
     9.6    Real/PRat.ML Real/PRat.thy \
     9.7 -  Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
     9.8 +  Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
     9.9    Real/ROOT.ML Real/Real.thy \
    9.10    Real/RealArith0.thy Real/real_arith0.ML \
    9.11    Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
    10.1 --- a/src/HOL/Real/PRat.ML	Thu Jan 01 10:06:32 2004 +0100
    10.2 +++ b/src/HOL/Real/PRat.ML	Thu Jan 01 21:47:07 2004 +0100
    10.3 @@ -482,9 +482,9 @@
    10.4  by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1);
    10.5  qed "prat_linear";
    10.6  
    10.7 -Goal "!!(q1::prat). [| q1 < q2 ==> P;  q1 = q2 ==> P; \
    10.8 -\          q2 < q1 ==> P |] ==> P";
    10.9 -by (cut_inst_tac [("q1.0","q1"),("q2.0","q2")] prat_linear 1);
   10.10 +Goal "!!(x::prat). [| x < y ==> P;  x = y ==> P; \
   10.11 +\          y < x ==> P |] ==> P";
   10.12 +by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
   10.13  by Auto_tac;
   10.14  qed "prat_linear_less2";
   10.15  
   10.16 @@ -510,7 +510,7 @@
   10.17  qed "lemma2_qinv_prat_less";
   10.18  
   10.19  Goal "q1 < q2  ==> qinv (q2) < qinv (q1)";
   10.20 -by (res_inst_tac [("q2.0","qinv q1"), ("q1.0","qinv q2")] prat_linear_less2 1);
   10.21 +by (res_inst_tac [("y","qinv q1"), ("x","qinv q2")] prat_linear_less2 1);
   10.22  by (auto_tac (claset() addEs [lemma1_qinv_prat_less,
   10.23                   lemma2_qinv_prat_less],simpset()));
   10.24  qed "qinv_prat_less";
    11.1 --- a/src/HOL/Real/PReal.ML	Thu Jan 01 10:06:32 2004 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,1244 +0,0 @@
    11.4 -(*  Title       : HOL/Real/PReal.ML
    11.5 -    ID          : $Id$
    11.6 -    Author      : Jacques D. Fleuriot
    11.7 -    Copyright   : 1998  University of Cambridge
    11.8 -    Description : The positive reals as Dedekind sections of positive
    11.9 -                  rationals. Fundamentals of Abstract Analysis 
   11.10 -                  [Gleason- p. 121] provides some of the definitions.
   11.11 -*)
   11.12 -
   11.13 -Goal "inj_on Abs_preal preal";
   11.14 -by (rtac inj_on_inverseI 1);
   11.15 -by (etac Abs_preal_inverse 1);
   11.16 -qed "inj_on_Abs_preal";
   11.17 -
   11.18 -Addsimps [inj_on_Abs_preal RS inj_on_iff];
   11.19 -
   11.20 -Goal "inj(Rep_preal)";
   11.21 -by (rtac inj_inverseI 1);
   11.22 -by (rtac Rep_preal_inverse 1);
   11.23 -qed "inj_Rep_preal";
   11.24 -
   11.25 -Goalw [preal_def] "{} ~: preal";
   11.26 -by (Fast_tac 1);
   11.27 -qed "empty_not_mem_preal";
   11.28 -
   11.29 -(* {} : preal ==> P *)
   11.30 -bind_thm ("empty_not_mem_prealE", empty_not_mem_preal RS notE);
   11.31 -
   11.32 -Addsimps [empty_not_mem_preal];
   11.33 -
   11.34 -Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} : preal";
   11.35 -by (rtac preal_1 1);
   11.36 -qed "one_set_mem_preal";
   11.37 -
   11.38 -Addsimps [one_set_mem_preal];
   11.39 -
   11.40 -Goalw [preal_def] "x : preal ==> {} < x";
   11.41 -by (Fast_tac 1);
   11.42 -qed "preal_psubset_empty";
   11.43 -
   11.44 -Goal "{} < Rep_preal x";
   11.45 -by (rtac (Rep_preal RS preal_psubset_empty) 1);
   11.46 -qed "Rep_preal_psubset_empty";
   11.47 -
   11.48 -Goal "EX x. x: Rep_preal X";
   11.49 -by (cut_inst_tac [("x","X")]  Rep_preal_psubset_empty 1);
   11.50 -by (auto_tac (claset() addIs [(equals0I RS sym)],
   11.51 -              simpset() addsimps [psubset_def]));
   11.52 -qed "mem_Rep_preal_Ex";
   11.53 -
   11.54 -Goalw [preal_def] 
   11.55 -      "[| {} < A; A < UNIV; \
   11.56 -\              (ALL y: A. ((ALL z. z < y --> z: A) & \
   11.57 -\                        (EX u: A. y < u))) |] ==> A : preal";
   11.58 -by (Fast_tac 1);
   11.59 -qed "prealI1";
   11.60 -    
   11.61 -Goalw [preal_def] 
   11.62 -      "[| {} < A; A < UNIV; \
   11.63 -\              ALL y: A. (ALL z. z < y --> z: A); \
   11.64 -\              ALL y: A. (EX u: A. y < u) |] ==> A : preal";
   11.65 -by (Best_tac 1);
   11.66 -qed "prealI2";
   11.67 -
   11.68 -Goalw [preal_def] 
   11.69 -      "A : preal ==> {} < A & A < UNIV & \
   11.70 -\                         (ALL y: A. ((ALL z. z < y --> z: A) & \
   11.71 -\                                  (EX u: A. y < u)))";
   11.72 -by (Fast_tac 1);
   11.73 -qed "prealE_lemma";
   11.74 -
   11.75 -
   11.76 -AddSIs [prealI1,prealI2];
   11.77 -
   11.78 -Addsimps [Abs_preal_inverse];
   11.79 -
   11.80 -
   11.81 -Goalw [preal_def] "A : preal ==> {} < A";
   11.82 -by (Fast_tac 1);
   11.83 -qed "prealE_lemma1";
   11.84 -
   11.85 -Goalw [preal_def] "A : preal ==> A < UNIV";
   11.86 -by (Fast_tac 1);
   11.87 -qed "prealE_lemma2";
   11.88 -
   11.89 -Goalw [preal_def] "A : preal ==> ALL y: A. (ALL z. z < y --> z: A)";
   11.90 -by (Fast_tac 1);
   11.91 -qed "prealE_lemma3";
   11.92 -
   11.93 -Goal "[| A : preal; y: A |] ==> (ALL z. z < y --> z: A)";
   11.94 -by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
   11.95 -qed "prealE_lemma3a";
   11.96 -
   11.97 -Goal "[| A : preal; y: A; z < y |] ==> z: A";
   11.98 -by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
   11.99 -qed "prealE_lemma3b";
  11.100 -
  11.101 -Goalw [preal_def] "A : preal ==> ALL y: A. (EX u: A. y < u)";
  11.102 -by (Fast_tac 1);
  11.103 -qed "prealE_lemma4";
  11.104 -
  11.105 -Goal "[| A : preal; y: A |] ==> EX u: A. y < u";
  11.106 -by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
  11.107 -qed "prealE_lemma4a";
  11.108 -
  11.109 -Goal "EX x. x~: Rep_preal X";
  11.110 -by (cut_inst_tac [("x","X")] Rep_preal 1);
  11.111 -by (dtac prealE_lemma2 1);
  11.112 -by (auto_tac (claset(),simpset() addsimps [psubset_def]));
  11.113 -qed "not_mem_Rep_preal_Ex";
  11.114 -
  11.115 -(** preal_of_prat: the injection from prat to preal **)
  11.116 -(** A few lemmas **)
  11.117 -
  11.118 -Goal "{xa::prat. xa < y} : preal";
  11.119 -by (cut_facts_tac [qless_Ex] 1);
  11.120 -by (auto_tac (claset() addIs[prat_less_trans]
  11.121 -                       addSEs [prat_less_irrefl], 
  11.122 -	      simpset()));
  11.123 -by (blast_tac (claset() addDs [prat_dense]) 1);
  11.124 -qed "lemma_prat_less_set_mem_preal";
  11.125 -
  11.126 -Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y";
  11.127 -by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
  11.128 -by Safe_tac;
  11.129 -by (dtac prat_dense 2 THEN etac exE 2);
  11.130 -by (dtac prat_dense 1 THEN etac exE 1);
  11.131 -by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
  11.132 -by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
  11.133 -qed "lemma_prat_set_eq";
  11.134 -
  11.135 -Goal "inj(preal_of_prat)";
  11.136 -by (rtac injI 1);
  11.137 -by (rewtac preal_of_prat_def);
  11.138 -by (dtac (inj_on_Abs_preal RS inj_onD) 1);
  11.139 -by (rtac lemma_prat_less_set_mem_preal 1);
  11.140 -by (rtac lemma_prat_less_set_mem_preal 1);
  11.141 -by (etac lemma_prat_set_eq 1);
  11.142 -qed "inj_preal_of_prat";
  11.143 -
  11.144 -      (*** theorems for ordering ***)
  11.145 -(* prove introduction and elimination rules for preal_less *)
  11.146 -
  11.147 -(* A positive fraction not in a positive real is an upper bound *)
  11.148 -(* Gleason p. 122 - Remark (1)                                  *)
  11.149 -
  11.150 -Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x";
  11.151 -by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
  11.152 -by (fast_tac (claset() addIs [not_less_not_eq_prat_less] addss simpset()) 1);
  11.153 -qed "not_in_preal_ub";
  11.154 -
  11.155 -(* preal_less is a strong order i.e nonreflexive and transitive *)
  11.156 -
  11.157 -Goalw [preal_less_def] "~ (x::preal) < x";
  11.158 -by (simp_tac (simpset() addsimps [psubset_def]) 1);
  11.159 -qed "preal_less_not_refl";
  11.160 -
  11.161 -(*** y < y ==> P ***)
  11.162 -bind_thm("preal_less_irrefl", preal_less_not_refl RS notE);
  11.163 -
  11.164 -Goal "!!(x::preal). x < y ==> x ~= y";
  11.165 -by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
  11.166 -qed "preal_not_refl2";
  11.167 -
  11.168 -Goalw  [preal_less_def] "!!(x::preal). [| x < y; y < z |] ==> x < z";
  11.169 -by (auto_tac (claset() addDs [subsetD,equalityI],
  11.170 -              simpset() addsimps [psubset_def]));
  11.171 -qed "preal_less_trans";
  11.172 -
  11.173 -Goal "!! (q1::preal). q1 < q2 ==> ~ q2 < q1";
  11.174 -by (rtac notI 1);
  11.175 -by (dtac preal_less_trans 1 THEN assume_tac 1);
  11.176 -by (asm_full_simp_tac (simpset() addsimps [preal_less_not_refl]) 1);
  11.177 -qed "preal_less_not_sym";
  11.178 -
  11.179 -(* [| x < y;  ~P ==> y < x |] ==> P *)
  11.180 -bind_thm ("preal_less_asym", preal_less_not_sym RS contrapos_np);
  11.181 -
  11.182 -Goalw [preal_less_def] 
  11.183 -      "(r1::preal) < r2 | r1 = r2 | r2 < r1";
  11.184 -by (auto_tac (claset() addSDs [inj_Rep_preal RS injD],
  11.185 -              simpset() addsimps [psubset_def]));
  11.186 -by (rtac prealE_lemma3b 1 THEN rtac Rep_preal 1);
  11.187 -by (assume_tac 1);
  11.188 -by (fast_tac (claset() addDs [not_in_preal_ub]) 1);
  11.189 -qed "preal_linear";
  11.190 -
  11.191 -Goal "!!(r1::preal). [| r1 < r2 ==> P;  r1 = r2 ==> P; \
  11.192 -\                       r2 < r1 ==> P |] ==> P";
  11.193 -by (cut_inst_tac [("r1.0","r1"),("r2.0","r2")] preal_linear 1);
  11.194 -by Auto_tac;
  11.195 -qed "preal_linear_less2";
  11.196 -
  11.197 -  (*** Properties of addition ***)
  11.198 -
  11.199 -Goalw [preal_add_def] "(x::preal) + y = y + x";
  11.200 -by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
  11.201 -by (blast_tac (claset() addIs [prat_add_commute RS subst]) 1);
  11.202 -qed "preal_add_commute";
  11.203 -
  11.204 -(** addition of two positive reals gives a positive real **)
  11.205 -(** lemmas for proving positive reals addition set in preal **)
  11.206 -
  11.207 -(** Part 1 of Dedekind sections def **)
  11.208 -Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
  11.209 -by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
  11.210 -by (auto_tac (claset() addSIs [psubsetI], simpset()));
  11.211 -qed "preal_add_set_not_empty";
  11.212 -
  11.213 -(** Part 2 of Dedekind sections def **)
  11.214 -Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
  11.215 -by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
  11.216 -by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
  11.217 -by (REPEAT(etac exE 1));
  11.218 -by (REPEAT(dtac not_in_preal_ub 1));
  11.219 -by (res_inst_tac [("x","x+xa")] exI 1);
  11.220 -by (Auto_tac THEN (REPEAT(etac ballE 1)) THEN Auto_tac);
  11.221 -by (dtac prat_add_less_mono 1);
  11.222 -by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
  11.223 -qed "preal_not_mem_add_set_Ex";
  11.224 -
  11.225 -Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y} < UNIV";
  11.226 -by (auto_tac (claset() addSIs [psubsetI],simpset()));
  11.227 -by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
  11.228 -by Auto_tac;
  11.229 -qed "preal_add_set_not_prat_set";
  11.230 -
  11.231 -(** Part 3 of Dedekind sections def **)
  11.232 -Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
  11.233 -\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
  11.234 -by Auto_tac;
  11.235 -by (ftac prat_mult_qinv_less_1 1);
  11.236 -by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat (Suc 0))")] 
  11.237 -    prat_mult_less2_mono1 1);
  11.238 -by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat (Suc 0))")] 
  11.239 -    prat_mult_less2_mono1 1);
  11.240 -by (Asm_full_simp_tac 1);
  11.241 -by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
  11.242 -by (REPEAT(etac allE 1));
  11.243 -by Auto_tac;
  11.244 -by (REPEAT(rtac bexI 1));
  11.245 -by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2 
  11.246 -     RS sym,prat_add_assoc RS sym,prat_mult_assoc]));
  11.247 -qed "preal_add_set_lemma3";
  11.248 -
  11.249 -Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
  11.250 -\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. y < u";
  11.251 -by Auto_tac;
  11.252 -by (dtac (Rep_preal RS prealE_lemma4a) 1);
  11.253 -by (auto_tac (claset() addIs [prat_add_less2_mono1],simpset()));
  11.254 -qed "preal_add_set_lemma4";
  11.255 -
  11.256 -Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y} : preal";
  11.257 -by (rtac prealI2 1);
  11.258 -by (rtac preal_add_set_not_empty 1);
  11.259 -by (rtac preal_add_set_not_prat_set 1);
  11.260 -by (rtac preal_add_set_lemma3 1);
  11.261 -by (rtac preal_add_set_lemma4 1);
  11.262 -qed "preal_mem_add_set";
  11.263 -
  11.264 -Goalw [preal_add_def] "((x::preal) + y) + z = x + (y + z)";
  11.265 -by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
  11.266 -by (simp_tac (simpset() addsimps [preal_mem_add_set RS Abs_preal_inverse]) 1); 
  11.267 -by (auto_tac (claset(),simpset() addsimps prat_add_ac));
  11.268 -by (rtac bexI 1);
  11.269 -by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_add_ac));
  11.270 -qed "preal_add_assoc";
  11.271 -
  11.272 -Goal "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)";
  11.273 -by(rtac ([preal_add_assoc,preal_add_commute] MRS
  11.274 -         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
  11.275 -qed "preal_add_left_commute";
  11.276 -
  11.277 -(* Positive Reals addition is an AC operator *)
  11.278 -bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]);
  11.279 -
  11.280 -  (*** Properties of multiplication ***)
  11.281 -
  11.282 -(** Proofs essentially same as for addition **)
  11.283 -
  11.284 -Goalw [preal_mult_def] "(x::preal) * y = y * x";
  11.285 -by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
  11.286 -by (blast_tac (claset() addIs [prat_mult_commute RS subst]) 1);
  11.287 -qed "preal_mult_commute";
  11.288 -
  11.289 -(** multiplication of two positive reals gives a positive real **)
  11.290 -(** lemmas for proving positive reals multiplication set in preal **)
  11.291 -
  11.292 -(** Part 1 of Dedekind sections def **)
  11.293 -Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
  11.294 -by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
  11.295 -by (auto_tac (claset() addSIs [psubsetI], simpset()));
  11.296 -qed "preal_mult_set_not_empty";
  11.297 -
  11.298 -(** Part 2 of Dedekind sections def **)
  11.299 -Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
  11.300 -by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
  11.301 -by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
  11.302 -by (REPEAT(etac exE 1));
  11.303 -by (REPEAT(dtac not_in_preal_ub 1));
  11.304 -by (res_inst_tac [("x","x*xa")] exI 1);
  11.305 -by (Auto_tac  THEN (REPEAT(etac ballE 1)) THEN Auto_tac );
  11.306 -by (dtac prat_mult_less_mono 1);
  11.307 -by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
  11.308 -qed "preal_not_mem_mult_set_Ex";
  11.309 -
  11.310 -Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y} < UNIV";
  11.311 -by (auto_tac (claset() addSIs [psubsetI],simpset()));
  11.312 -by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
  11.313 -by Auto_tac;
  11.314 -qed "preal_mult_set_not_prat_set";
  11.315 -
  11.316 -(** Part 3 of Dedekind sections def **)
  11.317 -Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
  11.318 -\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x * y}";
  11.319 -by Auto_tac;
  11.320 -by (forw_inst_tac [("x","qinv(ya)"),("q1.0","z")] 
  11.321 -    prat_mult_left_less2_mono1 1);
  11.322 -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
  11.323 -by (dtac (Rep_preal RS prealE_lemma3a) 1);
  11.324 -by (etac allE 1);
  11.325 -by (REPEAT(rtac bexI 1));
  11.326 -by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
  11.327 -qed "preal_mult_set_lemma3";
  11.328 -
  11.329 -Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
  11.330 -\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. y < u";
  11.331 -by Auto_tac;
  11.332 -by (dtac (Rep_preal RS prealE_lemma4a) 1);
  11.333 -by (auto_tac (claset() addIs [prat_mult_less2_mono1],simpset()));
  11.334 -qed "preal_mult_set_lemma4";
  11.335 -
  11.336 -Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y} : preal";
  11.337 -by (rtac prealI2 1);
  11.338 -by (rtac preal_mult_set_not_empty 1);
  11.339 -by (rtac preal_mult_set_not_prat_set 1);
  11.340 -by (rtac preal_mult_set_lemma3 1);
  11.341 -by (rtac preal_mult_set_lemma4 1);
  11.342 -qed "preal_mem_mult_set";
  11.343 -
  11.344 -Goalw [preal_mult_def] "((x::preal) * y) * z = x * (y * z)";
  11.345 -by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
  11.346 -by (simp_tac (simpset() addsimps [preal_mem_mult_set RS Abs_preal_inverse]) 1);
  11.347 -by (auto_tac (claset(),simpset() addsimps prat_mult_ac));
  11.348 -by (rtac bexI 1);
  11.349 -by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_mult_ac));
  11.350 -qed "preal_mult_assoc";
  11.351 -
  11.352 -Goal "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)";
  11.353 -by(rtac ([preal_mult_assoc,preal_mult_commute] MRS
  11.354 -         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
  11.355 -qed "preal_mult_left_commute";
  11.356 -
  11.357 -(* Positive Reals multiplication is an AC operator *)
  11.358 -bind_thms ("preal_mult_ac", [preal_mult_assoc, 
  11.359 -                     preal_mult_commute, 
  11.360 -                     preal_mult_left_commute]);
  11.361 -
  11.362 -(* Positive Real 1 is the multiplicative identity element *) 
  11.363 -(* long *)
  11.364 -Goalw [preal_of_prat_def,preal_mult_def] 
  11.365 -      "(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) * z = z";
  11.366 -by (rtac (Rep_preal_inverse RS subst) 1);
  11.367 -by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
  11.368 -by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
  11.369 -by (auto_tac(claset(),simpset() addsimps [Rep_preal_inverse]));
  11.370 -by (EVERY1[dtac (Rep_preal RS prealE_lemma4a),etac bexE]);
  11.371 -by (dtac prat_mult_less_mono 1);
  11.372 -by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3a],simpset()));
  11.373 -by (EVERY1[forward_tac [Rep_preal RS prealE_lemma4a],etac bexE]);
  11.374 -by (forw_inst_tac [("x","qinv(u)"),("q1.0","x")] 
  11.375 -    prat_mult_less2_mono1 1);
  11.376 -by (rtac exI 1 THEN Auto_tac THEN res_inst_tac [("x","u")] bexI 1);
  11.377 -by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
  11.378 -qed "preal_mult_1";
  11.379 -
  11.380 -Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) = z";
  11.381 -by (rtac (preal_mult_commute RS subst) 1);
  11.382 -by (rtac preal_mult_1 1);
  11.383 -qed "preal_mult_1_right";
  11.384 -
  11.385 -(** Lemmas **)
  11.386 -
  11.387 -Goal "(z::preal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
  11.388 -by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
  11.389 -qed "preal_add_assoc_cong";
  11.390 -
  11.391 -Goal "(z::preal) + (v + w) = v + (z + w)";
  11.392 -by (REPEAT (ares_tac [preal_add_commute RS preal_add_assoc_cong] 1));
  11.393 -qed "preal_add_assoc_swap";
  11.394 -
  11.395 -(** Distribution of multiplication across addition **)
  11.396 -(** lemmas for the proof **)
  11.397 -
  11.398 - (** lemmas **)
  11.399 -Goalw [preal_add_def] 
  11.400 -      "z: Rep_preal(R+S) ==> \
  11.401 -\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y";
  11.402 -by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
  11.403 -by (Fast_tac 1);
  11.404 -qed "mem_Rep_preal_addD";
  11.405 -
  11.406 -Goalw [preal_add_def] 
  11.407 -      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y \
  11.408 -\      ==> z: Rep_preal(R+S)";
  11.409 -by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
  11.410 -by (Fast_tac 1);
  11.411 -qed "mem_Rep_preal_addI";
  11.412 -
  11.413 -Goal "(z: Rep_preal(R+S)) = (EX x: Rep_preal(R). \
  11.414 -\                                 EX y: Rep_preal(S). z = x + y)";
  11.415 -by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
  11.416 -qed "mem_Rep_preal_add_iff";
  11.417 -
  11.418 -Goalw [preal_mult_def] 
  11.419 -      "z: Rep_preal(R*S) ==> \
  11.420 -\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y";
  11.421 -by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
  11.422 -by (Fast_tac 1);
  11.423 -qed "mem_Rep_preal_multD";
  11.424 -
  11.425 -Goalw [preal_mult_def] 
  11.426 -      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y \
  11.427 -\      ==> z: Rep_preal(R*S)";
  11.428 -by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
  11.429 -by (Fast_tac 1);
  11.430 -qed "mem_Rep_preal_multI";
  11.431 -
  11.432 -Goal "(z: Rep_preal(R*S)) = (EX x: Rep_preal(R). \
  11.433 -\                                 EX y: Rep_preal(S). z = x * y)";
  11.434 -by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
  11.435 -qed "mem_Rep_preal_mult_iff";
  11.436 -
  11.437 -(** More lemmas for preal_add_mult_distrib2 **)
  11.438 -
  11.439 -Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
  11.440 -\                  Rep_preal w; yb: Rep_preal w |] ==> \
  11.441 -\                  xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
  11.442 -by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
  11.443 -qed "lemma_add_mult_mem_Rep_preal";
  11.444 -
  11.445 -Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
  11.446 -\                  Rep_preal w; yb: Rep_preal w |] ==> \
  11.447 -\                  yb*(xb + xc): Rep_preal (w*(z1 + z2))";
  11.448 -by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
  11.449 -qed "lemma_add_mult_mem_Rep_preal1";
  11.450 -
  11.451 -Goal "x: Rep_preal (w * z1 + w * z2) ==> \
  11.452 -\              x: Rep_preal (w * (z1 + z2))";
  11.453 -by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD],
  11.454 -              simpset()));
  11.455 -by (forw_inst_tac [("ya","xa"),("yb","xb"),("xb","ya"),("xc","yb")] 
  11.456 -                                   lemma_add_mult_mem_Rep_preal1 1);
  11.457 -by Auto_tac;
  11.458 -by (res_inst_tac [("q1.0","xa"),("q2.0","xb")] prat_linear_less2 1);
  11.459 -by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1);
  11.460 -by (rtac (Rep_preal RS prealE_lemma3b) 1);
  11.461 -by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2]));
  11.462 -by (dres_inst_tac [("ya","xb"),("yb","xa"),("xc","ya"),("xb","yb")] 
  11.463 -                                   lemma_add_mult_mem_Rep_preal1 1);
  11.464 -by Auto_tac;
  11.465 -by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1);
  11.466 -by (rtac (Rep_preal RS prealE_lemma3b) 1);
  11.467 -by (thin_tac "xb * ya + xb * yb  : Rep_preal (w * (z1 + z2))" 1);
  11.468 -by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib,
  11.469 -              prat_add_commute] @ preal_add_ac ));
  11.470 -qed "lemma_preal_add_mult_distrib";
  11.471 -
  11.472 -Goal "x: Rep_preal (w * (z1 + z2)) ==> \
  11.473 -\              x: Rep_preal (w * z1 + w * z2)";
  11.474 -by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD]
  11.475 -              addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI],
  11.476 -              simpset() addsimps [prat_add_mult_distrib2]));
  11.477 -qed "lemma_preal_add_mult_distrib2";
  11.478 -
  11.479 -Goal "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)";
  11.480 -by (rtac (inj_Rep_preal RS injD) 1);
  11.481 -by (fast_tac (claset() addIs [lemma_preal_add_mult_distrib,
  11.482 -                              lemma_preal_add_mult_distrib2]) 1);
  11.483 -qed "preal_add_mult_distrib2";
  11.484 -
  11.485 -Goal "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)";
  11.486 -by (simp_tac (simpset() addsimps [preal_mult_commute,
  11.487 -                                  preal_add_mult_distrib2]) 1);
  11.488 -qed "preal_add_mult_distrib";
  11.489 -
  11.490 -(*** Prove existence of inverse ***)
  11.491 -(*** Inverse is a positive real ***)
  11.492 -
  11.493 -Goal "EX y. qinv(y) ~:  Rep_preal X";
  11.494 -by (cut_inst_tac [("X","X")] not_mem_Rep_preal_Ex 1);
  11.495 -by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
  11.496 -by Auto_tac;
  11.497 -qed "qinv_not_mem_Rep_preal_Ex";
  11.498 -
  11.499 -Goal "EX q. q: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
  11.500 -by (cut_inst_tac [("X","A")] qinv_not_mem_Rep_preal_Ex 1);
  11.501 -by Auto_tac;
  11.502 -by (cut_inst_tac [("y","y")] qless_Ex 1);
  11.503 -by (Fast_tac 1);
  11.504 -qed "lemma_preal_mem_inv_set_ex";
  11.505 -
  11.506 -(** Part 1 of Dedekind sections def **)
  11.507 -Goal "{} < {x. EX y. x < y & qinv y ~:  Rep_preal A}";
  11.508 -by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
  11.509 -by (auto_tac (claset() addSIs [psubsetI], simpset()));
  11.510 -qed "preal_inv_set_not_empty";
  11.511 -
  11.512 -(** Part 2 of Dedekind sections def **)
  11.513 -Goal "EX y. qinv(y) :  Rep_preal X";
  11.514 -by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
  11.515 -by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
  11.516 -by Auto_tac;
  11.517 -qed "qinv_mem_Rep_preal_Ex";
  11.518 -
  11.519 -Goal "EX x. x ~: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
  11.520 -by (rtac ccontr 1);
  11.521 -by (cut_inst_tac [("X","A")] qinv_mem_Rep_preal_Ex 1);
  11.522 -by Auto_tac;
  11.523 -by (EVERY1[etac allE, etac exE, etac conjE]);
  11.524 -by (dtac qinv_prat_less 1 THEN dtac not_in_preal_ub 1);
  11.525 -by (eres_inst_tac [("x","qinv y")] ballE 1);
  11.526 -by (dtac prat_less_trans 1);
  11.527 -by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
  11.528 -qed "preal_not_mem_inv_set_Ex";
  11.529 -
  11.530 -Goal "{x. EX y. x < y & qinv y ~:  Rep_preal A} < UNIV";
  11.531 -by (auto_tac (claset() addSIs [psubsetI],simpset()));
  11.532 -by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
  11.533 -by Auto_tac;
  11.534 -qed "preal_inv_set_not_prat_set";
  11.535 -
  11.536 -(** Part 3 of Dedekind sections def **)
  11.537 -Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
  11.538 - \      ALL z. z < y --> z : {x. EX y. x < y & qinv y ~: Rep_preal A}";
  11.539 -by Auto_tac;
  11.540 -by (res_inst_tac [("x","ya")] exI 1);
  11.541 -by (auto_tac (claset() addIs [prat_less_trans],simpset()));
  11.542 -qed "preal_inv_set_lemma3";
  11.543 -
  11.544 -Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
  11.545 -\       Bex {x. EX y. x < y & qinv y ~: Rep_preal A} (op < y)";
  11.546 -by (blast_tac (claset() addDs [prat_dense]) 1);
  11.547 -qed "preal_inv_set_lemma4";
  11.548 -
  11.549 -Goal "{x. EX y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
  11.550 -by (rtac prealI2 1);
  11.551 -by (rtac preal_inv_set_not_empty 1);
  11.552 -by (rtac preal_inv_set_not_prat_set 1);
  11.553 -by (rtac preal_inv_set_lemma3 1);
  11.554 -by (rtac preal_inv_set_lemma4 1);
  11.555 -qed "preal_mem_inv_set";
  11.556 -
  11.557 -(*more lemmas for inverse *)
  11.558 -Goal "x: Rep_preal(pinv(A)*A) ==> \
  11.559 -\     x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))";
  11.560 -by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
  11.561 -              simpset() addsimps [pinv_def,preal_of_prat_def] ));
  11.562 -by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
  11.563 -by (auto_tac (claset() addSDs [not_in_preal_ub],simpset()));
  11.564 -by (dtac prat_mult_less_mono 1 THEN Blast_tac 1);
  11.565 -by (auto_tac (claset(),simpset()));
  11.566 -qed "preal_mem_mult_invD";
  11.567 -
  11.568 -(*** Gleason's Lemma 9-3.4 p 122 ***)
  11.569 -Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
  11.570 -\            EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
  11.571 -by (cut_facts_tac [mem_Rep_preal_Ex] 1);
  11.572 -by (induct_thm_tac pnat_induct "p" 1);
  11.573 -by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
  11.574 -    pSuc_is_plus_one,prat_add_mult_distrib,
  11.575 -   prat_of_pnat_add,prat_add_assoc RS sym]));
  11.576 -qed "lemma1_gleason9_34";
  11.577 -
  11.578 -Goal "Abs_prat (ratrel `` {(y, z)}) < xb + \
  11.579 -\         Abs_prat (ratrel `` {(x*y, Abs_pnat (Suc 0))})*Abs_prat (ratrel `` {(w, x)})";
  11.580 -by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat (Suc 0))}) *\
  11.581 -\                   Abs_prat (ratrel `` {(w, x)})")] prat_le_less_trans 1);
  11.582 -by (rtac prat_self_less_add_right 2);
  11.583 -by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
  11.584 -    simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
  11.585 -qed "lemma1b_gleason9_34";
  11.586 -
  11.587 -Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
  11.588 -by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
  11.589 -by (etac exE 1);
  11.590 -by (dtac not_in_preal_ub 1);
  11.591 -by (res_inst_tac [("z","x")] eq_Abs_prat 1);
  11.592 -by (res_inst_tac [("z","xa")] eq_Abs_prat 1);
  11.593 -by (dres_inst_tac [("p","y*xb")] lemma1_gleason9_34 1);
  11.594 -by (etac bexE 1);
  11.595 -by (cut_inst_tac [("x","y"),("y","xb"),("w","xaa"),
  11.596 -    ("z","ya"),("xb","xba")] lemma1b_gleason9_34 1);
  11.597 -by (dres_inst_tac [("x","xba + prat_of_pnat (y * xb) * x")]  bspec 1);
  11.598 -by (auto_tac (claset() addIs [prat_less_asym],
  11.599 -    simpset() addsimps [prat_of_pnat_def]));
  11.600 -qed "lemma_gleason9_34a";
  11.601 -
  11.602 -Goal "EX r: Rep_preal(R). r + x ~: Rep_preal(R)";
  11.603 -by (rtac ccontr 1);
  11.604 -by (blast_tac (claset() addIs [lemma_gleason9_34a]) 1);
  11.605 -qed "lemma_gleason9_34";
  11.606 -
  11.607 -(*** Gleason's Lemma 9-3.6  ***)
  11.608 -(*  lemmas for Gleason 9-3.6  *)
  11.609 -(*                            *) 
  11.610 -(******************************)
  11.611 -
  11.612 -Goal "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)";
  11.613 -by (full_simp_tac (simpset() addsimps [prat_add_mult_distrib2,
  11.614 -    prat_mult_assoc]) 1);
  11.615 -qed "lemma1_gleason9_36";
  11.616 -
  11.617 -Goal "r*qinv(xa)*(xa*x) = r*x";
  11.618 -by (full_simp_tac (simpset() addsimps prat_mult_ac) 1);
  11.619 -qed "lemma2_gleason9_36";
  11.620 -(******)
  11.621 -
  11.622 -(*** FIXME: long! ***)
  11.623 -Goal "prat_of_pnat 1 < x ==> EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
  11.624 -by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
  11.625 -by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
  11.626 -by (Fast_tac 1);
  11.627 -by (dres_inst_tac [("x","xa")] prat_self_less_mult_right 1);
  11.628 -by (etac prat_lessE 1);
  11.629 -by (cut_inst_tac [("R","A"),("x","Q3")] lemma_gleason9_34 1);
  11.630 -by (dtac sym 1 THEN Auto_tac );
  11.631 -by (ftac not_in_preal_ub 1);
  11.632 -by (dres_inst_tac [("x","xa + Q3")] bspec 1 THEN assume_tac 1);
  11.633 -by (dtac prat_add_right_less_cancel 1);
  11.634 -by (dres_inst_tac [("x","qinv(xa)*Q3")] prat_mult_less2_mono1 1);
  11.635 -by (dres_inst_tac [("x","r")] prat_add_less2_mono2 1);
  11.636 -by (asm_full_simp_tac (simpset() addsimps
  11.637 -    [prat_mult_assoc RS sym,lemma1_gleason9_36]) 1);
  11.638 -by (dtac sym 1);
  11.639 -by (auto_tac (claset(),simpset() addsimps [lemma2_gleason9_36]));
  11.640 -by (res_inst_tac [("x","r")] bexI 1);
  11.641 -by (rtac notI 1);
  11.642 -by (dres_inst_tac [("y","r*x")] (Rep_preal RS prealE_lemma3b) 1);
  11.643 -by Auto_tac;
  11.644 -qed "lemma_gleason9_36";
  11.645 -
  11.646 -Goal "prat_of_pnat (Abs_pnat (Suc 0)) < x ==> \
  11.647 -\     EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
  11.648 -by (rtac lemma_gleason9_36 1);
  11.649 -by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
  11.650 -qed "lemma_gleason9_36a";
  11.651 -
  11.652 -(*** Part 2 of existence of inverse ***)
  11.653 -Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) \
  11.654 -\     ==> x: Rep_preal(pinv(A)*A)";
  11.655 -by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
  11.656 -              simpset() addsimps [pinv_def,preal_of_prat_def] ));
  11.657 -by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
  11.658 -by (dtac prat_qinv_gt_1 1);
  11.659 -by (dres_inst_tac [("A","A")] lemma_gleason9_36a 1);
  11.660 -by Auto_tac;
  11.661 -by (dtac (Rep_preal RS prealE_lemma4a) 1);
  11.662 -by (Auto_tac  THEN dtac qinv_prat_less 1);
  11.663 -by (res_inst_tac [("x","qinv(u)*x")] exI 1);
  11.664 -by (rtac conjI 1);
  11.665 -by (res_inst_tac [("x","qinv(r)*x")] exI 1);
  11.666 -by (auto_tac (claset() addIs [prat_mult_less2_mono1],
  11.667 -    simpset() addsimps [qinv_mult_eq,qinv_qinv]));
  11.668 -by (res_inst_tac [("x","u")] bexI 1);
  11.669 -by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc,
  11.670 -    prat_mult_left_commute]));
  11.671 -qed "preal_mem_mult_invI";
  11.672 -
  11.673 -Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))";
  11.674 -by (rtac (inj_Rep_preal RS injD) 1);
  11.675 -by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
  11.676 -qed "preal_mult_inv";
  11.677 -
  11.678 -Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))";
  11.679 -by (rtac (preal_mult_commute RS subst) 1);
  11.680 -by (rtac preal_mult_inv 1);
  11.681 -qed "preal_mult_inv_right";
  11.682 -
  11.683 -val [prem] = Goal
  11.684 -    "(!!u. z = Abs_preal(u) ==> P) ==> P";
  11.685 -by (cut_inst_tac [("x1","z")] 
  11.686 -    (rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1);
  11.687 -by (res_inst_tac [("u","Rep_preal z")] prem 1);
  11.688 -by (dtac (inj_Rep_preal RS injD) 1);
  11.689 -by (Asm_simp_tac 1);
  11.690 -qed "eq_Abs_preal";
  11.691 -
  11.692 -(*** Lemmas/Theorem(s) need lemma_gleason9_34 ***)
  11.693 -Goal "Rep_preal (R1) <= Rep_preal(R1 + R2)";
  11.694 -by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
  11.695 -by (auto_tac (claset() addSIs [bexI] addIs [(Rep_preal RS prealE_lemma3b),
  11.696 -   prat_self_less_add_left,mem_Rep_preal_addI],simpset()));
  11.697 -qed "Rep_preal_self_subset";
  11.698 -
  11.699 -Goal "~ Rep_preal (R1 + R2) <= Rep_preal(R1)";
  11.700 -by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
  11.701 -by (etac exE 1);
  11.702 -by (cut_inst_tac [("R","R1")] lemma_gleason9_34 1);
  11.703 -by (auto_tac (claset() addIs [mem_Rep_preal_addI],simpset()));
  11.704 -qed "Rep_preal_sum_not_subset";
  11.705 -
  11.706 -Goal "Rep_preal (R1 + R2) ~= Rep_preal(R1)";
  11.707 -by (rtac notI 1);
  11.708 -by (etac equalityE 1);
  11.709 -by (asm_full_simp_tac (simpset() addsimps [Rep_preal_sum_not_subset]) 1);
  11.710 -qed "Rep_preal_sum_not_eq";
  11.711 -
  11.712 -(*** at last --- Gleason prop. 9-3.5(iii) p. 123 ***)
  11.713 -Goalw [preal_less_def,psubset_def] "(R1::preal) < R1 + R2";
  11.714 -by (simp_tac (simpset() addsimps [Rep_preal_self_subset,
  11.715 -    Rep_preal_sum_not_eq RS not_sym]) 1);
  11.716 -qed "preal_self_less_add_left";
  11.717 -
  11.718 -Goal "(R1::preal) < R2 + R1";
  11.719 -by (simp_tac (simpset() addsimps [preal_add_commute,preal_self_less_add_left]) 1);
  11.720 -qed "preal_self_less_add_right";
  11.721 -
  11.722 -(*** Properties of <= ***)
  11.723 -
  11.724 -Goalw [preal_le_def,psubset_def,preal_less_def] 
  11.725 -                     "z<=w ==> ~(w<(z::preal))";
  11.726 -by (auto_tac  (claset() addDs [equalityI],simpset()));
  11.727 -qed "preal_leD";
  11.728 -
  11.729 -bind_thm ("preal_leE", make_elim preal_leD);
  11.730 -
  11.731 -Goalw [preal_le_def,psubset_def,preal_less_def]
  11.732 -                   "~ z <= w ==> w<(z::preal)";
  11.733 -by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
  11.734 -by (auto_tac  (claset(),simpset() addsimps [preal_less_def,psubset_def]));
  11.735 -qed "not_preal_leE";
  11.736 -		       
  11.737 -Goal "~(w < z) ==> z <= (w::preal)";
  11.738 -by (fast_tac (claset() addIs [not_preal_leE]) 1);
  11.739 -qed "preal_leI";
  11.740 -
  11.741 -Goal "(~(w < z)) = (z <= (w::preal))";
  11.742 -by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1);
  11.743 -qed "preal_less_le_iff";
  11.744 -
  11.745 -Goalw [preal_le_def,preal_less_def,psubset_def] 
  11.746 -     "z < w ==> z <= (w::preal)";
  11.747 -by (Fast_tac 1);
  11.748 -qed "preal_less_imp_le";
  11.749 -
  11.750 -Goalw [preal_le_def,preal_less_def,psubset_def] 
  11.751 -     "!!(x::preal). x <= y ==> x < y | x = y";
  11.752 -by (auto_tac (claset() addIs [inj_Rep_preal RS injD],simpset()));
  11.753 -qed "preal_le_imp_less_or_eq";
  11.754 -
  11.755 -Goalw [preal_le_def,preal_less_def,psubset_def] 
  11.756 -     "!!(x::preal). x < y | x = y ==> x <=y";
  11.757 -by Auto_tac;
  11.758 -qed "preal_less_or_eq_imp_le";
  11.759 -
  11.760 -Goalw [preal_le_def] "w <= (w::preal)";
  11.761 -by (Simp_tac 1);
  11.762 -qed "preal_le_refl";
  11.763 -
  11.764 -Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
  11.765 -by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
  11.766 -          rtac preal_less_or_eq_imp_le, 
  11.767 -                 fast_tac (claset() addIs [preal_less_trans])]);
  11.768 -qed "preal_le_trans";
  11.769 -
  11.770 -Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
  11.771 -by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
  11.772 -            fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
  11.773 -qed "preal_le_anti_sym";
  11.774 -
  11.775 -Goal "!!w::preal. (w ~= z) = (w<z | z<w)";
  11.776 -by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
  11.777 -by (auto_tac (claset() addEs [preal_less_irrefl], simpset()));
  11.778 -qed "preal_neq_iff";
  11.779 -
  11.780 -(* Axiom 'order_less_le' of class 'order': *)
  11.781 -Goal "((w::preal) < z) = (w <= z & w ~= z)";
  11.782 -by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
  11.783 -by (blast_tac (claset() addSEs [preal_less_asym]) 1);
  11.784 -qed "preal_less_le";
  11.785 -
  11.786 -
  11.787 -(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
  11.788 -
  11.789 -(**** Set up all lemmas for proving A < B ==> ?D. A + D = B ****)
  11.790 -(**** Gleason prop. 9-3.5(iv) p. 123 ****)
  11.791 -(**** Define the D required and show that it is a positive real ****)
  11.792 -
  11.793 -(* useful lemmas - proved elsewhere? *)
  11.794 -Goalw [psubset_def] "A < B ==> EX x. x ~: A & x : B";
  11.795 -by Auto_tac;
  11.796 -qed "lemma_psubset_mem";
  11.797 -
  11.798 -Goalw [psubset_def] "~ (A::'a set) < A";
  11.799 -by (Fast_tac 1);
  11.800 -qed "lemma_psubset_not_refl";
  11.801 -
  11.802 -Goalw [psubset_def] "!!(A::'a set). [| A < B; B < C |] ==> A < C";
  11.803 -by (auto_tac (claset() addDs [subset_antisym],simpset()));
  11.804 -qed "psubset_trans";
  11.805 -
  11.806 -Goalw [psubset_def] "!!(A::'a set). [| A <= B; B < C |] ==> A < C";
  11.807 -by (auto_tac (claset() addDs [subset_antisym],simpset()));
  11.808 -qed "subset_psubset_trans";
  11.809 -
  11.810 -Goalw [psubset_def] "!!(A::'a set). [| A < B; B <= C |] ==> A < C";
  11.811 -by (auto_tac (claset() addDs [subset_antisym],simpset()));
  11.812 -qed "subset_psubset_trans2";
  11.813 -
  11.814 -Goalw [psubset_def] "!!(A::'a set). [| A < B; c : A |] ==> c : B";
  11.815 -by (auto_tac (claset() addDs [subsetD],simpset()));
  11.816 -qed "psubsetD";
  11.817 -
  11.818 -(** Part 1 of Dedekind sections def **)
  11.819 -Goalw [preal_less_def]
  11.820 -     "A < B ==> \
  11.821 -\     EX q. q : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
  11.822 -by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
  11.823 -by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
  11.824 -by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
  11.825 -qed "lemma_ex_mem_less_left_add1";
  11.826 -
  11.827 -Goal "A < B ==> {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
  11.828 -by (dtac lemma_ex_mem_less_left_add1 1);
  11.829 -by (auto_tac (claset() addSIs [psubsetI], simpset()));
  11.830 -qed "preal_less_set_not_empty";
  11.831 -
  11.832 -(** Part 2 of Dedekind sections def **)
  11.833 -Goal "EX q. q ~: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
  11.834 -by (cut_inst_tac [("X","B")] not_mem_Rep_preal_Ex 1);
  11.835 -by (etac exE 1);
  11.836 -by (res_inst_tac [("x","x")] exI 1);
  11.837 -by Auto_tac;
  11.838 -by (cut_inst_tac [("x","x"),("y","n")] prat_self_less_add_right 1);
  11.839 -by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
  11.840 -qed "lemma_ex_not_mem_less_left_add1";
  11.841 -
  11.842 -Goal "{d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
  11.843 -by (auto_tac (claset() addSIs [psubsetI],simpset()));
  11.844 -by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
  11.845 -by Auto_tac;
  11.846 -qed "preal_less_set_not_prat_set";
  11.847 -
  11.848 -(** Part 3 of Dedekind sections def **)
  11.849 -Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
  11.850 - \   ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
  11.851 -by Auto_tac;
  11.852 -by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
  11.853 -by (dtac (Rep_preal RS prealE_lemma3b) 1);
  11.854 -by Auto_tac;
  11.855 -qed "preal_less_set_lemma3";
  11.856 -
  11.857 -Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
  11.858 -\       Bex {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
  11.859 -by Auto_tac;
  11.860 -by (dtac (Rep_preal RS prealE_lemma4a) 1);
  11.861 -by (auto_tac (claset(),simpset() addsimps [prat_less_def,prat_add_assoc]));
  11.862 -qed "preal_less_set_lemma4";
  11.863 -
  11.864 -Goal 
  11.865 -     "!! (A::preal). A < B ==> \
  11.866 -\     {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
  11.867 -by (rtac prealI2 1);
  11.868 -by (rtac preal_less_set_not_empty 1);
  11.869 -by (rtac preal_less_set_not_prat_set 2);
  11.870 -by (rtac preal_less_set_lemma3 2);
  11.871 -by (rtac preal_less_set_lemma4 3);
  11.872 -by Auto_tac;
  11.873 -qed "preal_mem_less_set";
  11.874 -
  11.875 -(** proving that A + D <= B **)
  11.876 -Goalw [preal_le_def] 
  11.877 -       "!! (A::preal). A < B ==> \
  11.878 -\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
  11.879 -by (rtac subsetI 1);
  11.880 -by (dtac mem_Rep_preal_addD 1);
  11.881 -by (auto_tac (claset(),simpset() addsimps [
  11.882 -    preal_mem_less_set RS Abs_preal_inverse]));
  11.883 -by (dtac not_in_preal_ub 1);
  11.884 -by (dtac bspec 1 THEN assume_tac 1);
  11.885 -by (dres_inst_tac [("x","y")] prat_add_less2_mono1 1);
  11.886 -by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma3b) 1);
  11.887 -by Auto_tac;
  11.888 -qed "preal_less_add_left_subsetI";
  11.889 -
  11.890 -(** proving that B <= A + D  --- trickier **)
  11.891 -(** lemma **)
  11.892 -Goal "x : Rep_preal(B) ==> EX e. x + e : Rep_preal(B)";
  11.893 -by (dtac (Rep_preal RS prealE_lemma4a) 1);
  11.894 -by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
  11.895 -qed "lemma_sum_mem_Rep_preal_ex";
  11.896 -
  11.897 -Goalw [preal_le_def] 
  11.898 -       "!! (A::preal). A < B ==> \
  11.899 -\         B <= A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
  11.900 -by (rtac subsetI 1);
  11.901 -by (res_inst_tac [("Q","x: Rep_preal(A)")] (excluded_middle RS disjE) 1);
  11.902 -by (rtac mem_Rep_preal_addI 1);
  11.903 -by (dtac lemma_sum_mem_Rep_preal_ex 1);
  11.904 -by (etac exE 1);
  11.905 -by (cut_inst_tac [("R","A"),("x","e")] lemma_gleason9_34 1 THEN etac bexE 1);
  11.906 -by (dtac not_in_preal_ub 1 THEN dtac bspec 1 THEN assume_tac 1);
  11.907 -by (etac prat_lessE 1);
  11.908 -by (res_inst_tac [("x","r")] bexI 1);
  11.909 -by (res_inst_tac [("x","Q3")] bexI 1);
  11.910 -by (cut_facts_tac [Rep_preal_self_subset] 4);
  11.911 -by (auto_tac (claset(),simpset() addsimps [
  11.912 -    preal_mem_less_set RS Abs_preal_inverse]));
  11.913 -by (res_inst_tac [("x","r+e")] exI 1);
  11.914 -by (asm_full_simp_tac (simpset() addsimps prat_add_ac) 1);
  11.915 -qed "preal_less_add_left_subsetI2";
  11.916 -
  11.917 -(*** required proof ***)
  11.918 -Goal "!! (A::preal). A < B ==> \
  11.919 -\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
  11.920 -by (blast_tac (claset() addIs [preal_le_anti_sym,
  11.921 -                preal_less_add_left_subsetI,preal_less_add_left_subsetI2]) 1);
  11.922 -qed "preal_less_add_left";
  11.923 -
  11.924 -Goal "!! (A::preal). A < B ==> EX D. A + D = B";
  11.925 -by (fast_tac (claset() addDs [preal_less_add_left]) 1);
  11.926 -qed "preal_less_add_left_Ex";        
  11.927 -
  11.928 -Goal "!!(A::preal). A < B ==> A + C < B + C";
  11.929 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  11.930 -    simpset() addsimps [preal_add_assoc]));
  11.931 -by (res_inst_tac [("y1","D")] (preal_add_commute RS subst) 1);
  11.932 -by (auto_tac (claset() addIs [preal_self_less_add_left],
  11.933 -          simpset() addsimps [preal_add_assoc RS sym]));
  11.934 -qed "preal_add_less2_mono1";
  11.935 -
  11.936 -Goal "!!(A::preal). A < B ==> C + A < C + B";
  11.937 -by (auto_tac (claset() addIs [preal_add_less2_mono1],
  11.938 -    simpset() addsimps [preal_add_commute]));
  11.939 -qed "preal_add_less2_mono2";
  11.940 -
  11.941 -Goal 
  11.942 -      "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x";
  11.943 -by (dtac preal_less_add_left_Ex 1);
  11.944 -by (auto_tac (claset(),simpset() addsimps [preal_add_mult_distrib,
  11.945 -    preal_self_less_add_left]));
  11.946 -qed "preal_mult_less_mono1";
  11.947 -
  11.948 -Goal "!!(q1::preal). q1 < q2  ==> x * q1 < x * q2";
  11.949 -by (auto_tac (claset() addDs [preal_mult_less_mono1],
  11.950 -    simpset() addsimps [preal_mult_commute]));
  11.951 -qed "preal_mult_left_less_mono1";
  11.952 -
  11.953 -Goal "!!(q1::preal). q1 <= q2  ==> x * q1 <= x * q2";
  11.954 -by (dtac preal_le_imp_less_or_eq 1);
  11.955 -by (Step_tac 1);
  11.956 -by (auto_tac (claset() addSIs [preal_le_refl,
  11.957 -    preal_less_imp_le,preal_mult_left_less_mono1],simpset()));
  11.958 -qed "preal_mult_left_le_mono1";
  11.959 - 
  11.960 -Goal "!!(q1::preal). q1 <= q2  ==> q1 * x <= q2 * x";
  11.961 -by (auto_tac (claset() addDs [preal_mult_left_le_mono1],
  11.962 -    simpset() addsimps [preal_mult_commute]));
  11.963 -qed "preal_mult_le_mono1";
  11.964 - 
  11.965 -Goal "!!(q1::preal). q1 <= q2  ==> x + q1 <= x + q2";
  11.966 -by (dtac preal_le_imp_less_or_eq 1);
  11.967 -by (Step_tac 1);
  11.968 -by (auto_tac (claset() addSIs [preal_le_refl,
  11.969 -                               preal_less_imp_le,preal_add_less2_mono1],
  11.970 -              simpset() addsimps [preal_add_commute]));
  11.971 -qed "preal_add_left_le_mono1";
  11.972 -
  11.973 -Goal "!!(q1::preal). q1 <= q2  ==> q1 + x <= q2 + x";
  11.974 -by (auto_tac (claset() addDs [preal_add_left_le_mono1],
  11.975 -    simpset() addsimps [preal_add_commute]));
  11.976 -qed "preal_add_le_mono1";
  11.977 - 
  11.978 -Goal "!!(A::preal). A + C < B + C ==> A < B";
  11.979 -by (cut_facts_tac [preal_linear] 1);
  11.980 -by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
  11.981 -by (dres_inst_tac [("A","B"),("C","C")] preal_add_less2_mono1 1);
  11.982 -by (fast_tac (claset() addDs [preal_less_trans] 
  11.983 -                addEs [preal_less_irrefl]) 1);
  11.984 -qed "preal_add_right_less_cancel";
  11.985 -
  11.986 -Goal "!!(A::preal). C + A < C + B ==> A < B";
  11.987 -by (auto_tac (claset() addEs [preal_add_right_less_cancel],
  11.988 -              simpset() addsimps [preal_add_commute]));
  11.989 -qed "preal_add_left_less_cancel";
  11.990 -
  11.991 -Goal "((A::preal) + C < B + C) = (A < B)";
  11.992 -by (REPEAT(ares_tac [iffI,preal_add_less2_mono1,
  11.993 -    preal_add_right_less_cancel] 1));
  11.994 -qed "preal_add_less_iff1";
  11.995 -
  11.996 -Addsimps [preal_add_less_iff1];
  11.997 -
  11.998 -Goal "(C + (A::preal) < C + B) = (A < B)";
  11.999 -by (REPEAT(ares_tac [iffI,preal_add_less2_mono2,
 11.1000 -    preal_add_left_less_cancel] 1));
 11.1001 -qed "preal_add_less_iff2";
 11.1002 -
 11.1003 -Addsimps [preal_add_less_iff2];
 11.1004 -
 11.1005 -Goal "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
 11.1006 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
 11.1007 -    simpset() addsimps  preal_add_ac));
 11.1008 -by (rtac (preal_add_assoc RS subst) 1);
 11.1009 -by (rtac preal_self_less_add_right 1);
 11.1010 -qed "preal_add_less_mono";
 11.1011 -
 11.1012 -Goal "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
 11.1013 -by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
 11.1014 -              simpset() addsimps [preal_add_mult_distrib,
 11.1015 -              preal_add_mult_distrib2,preal_self_less_add_left,
 11.1016 -              preal_add_assoc] @ preal_mult_ac));
 11.1017 -qed "preal_mult_less_mono";
 11.1018 -
 11.1019 -Goal "!!(A::preal). A + C = B + C ==> A = B";
 11.1020 -by (cut_facts_tac [preal_linear] 1);
 11.1021 -by Auto_tac;
 11.1022 -by (ALLGOALS(dres_inst_tac [("C","C")] preal_add_less2_mono1));
 11.1023 -by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
 11.1024 -qed "preal_add_right_cancel";
 11.1025 -
 11.1026 -Goal "!!(A::preal). C + A = C + B ==> A = B";
 11.1027 -by (auto_tac (claset() addIs [preal_add_right_cancel],
 11.1028 -              simpset() addsimps [preal_add_commute]));
 11.1029 -qed "preal_add_left_cancel";
 11.1030 -
 11.1031 -Goal "(C + A = C + B) = ((A::preal) = B)";
 11.1032 -by (fast_tac (claset() addIs [preal_add_left_cancel]) 1);
 11.1033 -qed "preal_add_left_cancel_iff";
 11.1034 -
 11.1035 -Goal "(A + C = B + C) = ((A::preal) = B)";
 11.1036 -by (fast_tac (claset() addIs [preal_add_right_cancel]) 1);
 11.1037 -qed "preal_add_right_cancel_iff";
 11.1038 -
 11.1039 -Addsimps [preal_add_left_cancel_iff,preal_add_right_cancel_iff];
 11.1040 -
 11.1041 -(*** Completeness of preal ***)
 11.1042 -
 11.1043 -(*** prove that supremum is a cut ***)
 11.1044 -Goal "EX (X::preal). X: P ==> \
 11.1045 -\         EX q.  q: {w. EX X. X : P & w : Rep_preal X}";
 11.1046 -by Safe_tac;
 11.1047 -by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
 11.1048 -by Auto_tac;
 11.1049 -qed "preal_sup_mem_Ex";
 11.1050 -
 11.1051 -(** Part 1 of Dedekind def **)
 11.1052 -Goal "EX (X::preal). X: P ==> \
 11.1053 -\         {} < {w. EX X : P. w : Rep_preal X}";
 11.1054 -by (dtac preal_sup_mem_Ex 1);
 11.1055 -by (auto_tac (claset() addSIs [psubsetI], simpset()));
 11.1056 -qed "preal_sup_set_not_empty";
 11.1057 -
 11.1058 -(** Part 2 of Dedekind sections def **) 
 11.1059 -Goalw [preal_less_def] "EX Y. (ALL X: P. X < Y)  \             
 11.1060 -\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}"; (**)
 11.1061 -by (auto_tac (claset(),simpset() addsimps [psubset_def]));
 11.1062 -by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
 11.1063 -by (etac exE 1);
 11.1064 -by (res_inst_tac [("x","x")] exI 1);
 11.1065 -by (auto_tac (claset() addSDs [bspec],simpset()));
 11.1066 -qed "preal_sup_not_mem_Ex";
 11.1067 -
 11.1068 -Goalw [preal_le_def] "EX Y. (ALL X: P. X <= Y)  \
 11.1069 -\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}";
 11.1070 -by (Step_tac 1);
 11.1071 -by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
 11.1072 -by (etac exE 1);
 11.1073 -by (res_inst_tac [("x","x")] exI 1);
 11.1074 -by (auto_tac (claset() addSDs [bspec],simpset()));
 11.1075 -qed "preal_sup_not_mem_Ex1";
 11.1076 -
 11.1077 -Goal "EX Y. (ALL X: P. X < Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; (**)
 11.1078 -by (dtac preal_sup_not_mem_Ex 1);
 11.1079 -by (auto_tac (claset() addSIs [psubsetI],simpset()));
 11.1080 -qed "preal_sup_set_not_prat_set";
 11.1081 -
 11.1082 -Goal "EX Y. (ALL X: P. X <= Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
 11.1083 -by (dtac preal_sup_not_mem_Ex1 1);
 11.1084 -by (auto_tac (claset() addSIs [psubsetI],simpset()));
 11.1085 -qed "preal_sup_set_not_prat_set1";
 11.1086 -
 11.1087 -(** Part 3 of Dedekind sections def **)
 11.1088 -Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
 11.1089 -\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
 11.1090 -\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";         (**)
 11.1091 -by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b], simpset()));
 11.1092 -qed "preal_sup_set_lemma3";
 11.1093 -
 11.1094 -Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
 11.1095 -\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
 11.1096 -\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";
 11.1097 -by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
 11.1098 -qed "preal_sup_set_lemma3_1";
 11.1099 -
 11.1100 -Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
 11.1101 -\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \                        
 11.1102 -\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";                (**)
 11.1103 -by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
 11.1104 -qed "preal_sup_set_lemma4";
 11.1105 -
 11.1106 -Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
 11.1107 -\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \
 11.1108 -\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";
 11.1109 -by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
 11.1110 -qed "preal_sup_set_lemma4_1";
 11.1111 -
 11.1112 -Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \            
 11.1113 -\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";                      (**)
 11.1114 -by (rtac prealI2 1);
 11.1115 -by (rtac preal_sup_set_not_empty 1);
 11.1116 -by (rtac preal_sup_set_not_prat_set 2);
 11.1117 -by (rtac preal_sup_set_lemma3 3);
 11.1118 -by (rtac preal_sup_set_lemma4 5);
 11.1119 -by Auto_tac;
 11.1120 -qed "preal_sup";
 11.1121 -
 11.1122 -Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
 11.1123 -\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";
 11.1124 -by (rtac prealI2 1);
 11.1125 -by (rtac preal_sup_set_not_empty 1);
 11.1126 -by (rtac preal_sup_set_not_prat_set1 2);
 11.1127 -by (rtac preal_sup_set_lemma3_1 3);
 11.1128 -by (rtac preal_sup_set_lemma4_1 5);
 11.1129 -by Auto_tac;
 11.1130 -qed "preal_sup1";
 11.1131 -
 11.1132 -Goalw [psup_def] "EX Y. (ALL X:P. X < Y) ==> ALL x: P. x <= psup P";      (**) 
 11.1133 -by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 11.1134 -by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
 11.1135 -by Auto_tac;
 11.1136 -qed "preal_psup_leI";
 11.1137 -
 11.1138 -Goalw [psup_def] "EX Y. (ALL X:P. X <= Y) ==> ALL x: P. x <= psup P";
 11.1139 -by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 11.1140 -by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
 11.1141 -by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 11.1142 -qed "preal_psup_leI2";
 11.1143 -
 11.1144 -Goal "[| EX Y. (ALL X:P. X < Y); x : P |] ==> x <= psup P";              (**)
 11.1145 -by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
 11.1146 -qed "preal_psup_leI2b";
 11.1147 -
 11.1148 -Goal "[| EX Y. (ALL X:P. X <= Y); x : P |] ==> x <= psup P";
 11.1149 -by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
 11.1150 -qed "preal_psup_leI2a";
 11.1151 -
 11.1152 -Goalw [psup_def] "[| EX X. X : P; ALL X:P. X < Y |] ==> psup P <= Y";   (**)
 11.1153 -by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 11.1154 -by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
 11.1155 -by (rotate_tac 1 2);
 11.1156 -by (assume_tac 2);
 11.1157 -by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
 11.1158 -qed "psup_le_ub";
 11.1159 -
 11.1160 -Goalw [psup_def] "[| EX X. X : P; ALL X:P. X <= Y |] ==> psup P <= Y";
 11.1161 -by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 11.1162 -by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
 11.1163 -by (rotate_tac 1 2);
 11.1164 -by (assume_tac 2);
 11.1165 -by (auto_tac (claset() addSDs [bspec],
 11.1166 -    simpset() addsimps [preal_less_def,psubset_def,preal_le_def]));
 11.1167 -qed "psup_le_ub1";
 11.1168 -
 11.1169 -(** supremum property **)
 11.1170 -Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \                  
 11.1171 -\         ==> (ALL Y. (EX X: P. Y < X) = (Y < psup P))";              
 11.1172 -by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
 11.1173 -by (Fast_tac 1);
 11.1174 -by (auto_tac (claset(), simpset() addsimps [psup_def,preal_less_def]));
 11.1175 -by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1);
 11.1176 -by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def]));
 11.1177 -qed "preal_complete";
 11.1178 -
 11.1179 -(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
 11.1180 -    (****** Embedding ******)
 11.1181 -(*** mapping from prat into preal ***)
 11.1182 -
 11.1183 -Goal "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
 11.1184 -by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1);
 11.1185 -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
 11.1186 -qed "lemma_preal_rat_less";
 11.1187 -
 11.1188 -Goal "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
 11.1189 -by (stac prat_add_commute 1);
 11.1190 -by (dtac (prat_add_commute RS subst) 1);
 11.1191 -by (etac lemma_preal_rat_less 1);
 11.1192 -qed "lemma_preal_rat_less2";
 11.1193 -
 11.1194 -Goalw [preal_of_prat_def,preal_add_def] 
 11.1195 -      "preal_of_prat ((z1::prat) + z2) = \
 11.1196 -\      preal_of_prat z1 + preal_of_prat z2";
 11.1197 -by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
 11.1198 -by (auto_tac (claset() addIs [prat_add_less_mono],
 11.1199 -     simpset() addsimps [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
 11.1200 -by (res_inst_tac [("x","x*z1*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
 11.1201 -by (etac lemma_preal_rat_less 1);
 11.1202 -by (res_inst_tac [("x","x*z2*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
 11.1203 -by (etac lemma_preal_rat_less2 1);
 11.1204 -by (asm_full_simp_tac (simpset() addsimps [prat_add_mult_distrib RS sym,
 11.1205 -     prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
 11.1206 -qed "preal_of_prat_add";
 11.1207 -
 11.1208 -Goal "x < xa ==> x*z1*qinv(xa) < z1";
 11.1209 -by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
 11.1210 -by (dtac (prat_mult_left_commute RS subst) 1);
 11.1211 -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
 11.1212 -qed "lemma_preal_rat_less3";
 11.1213 -
 11.1214 -Goal "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
 11.1215 -by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1);
 11.1216 -by (dtac (prat_mult_left_commute RS subst) 1);
 11.1217 -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
 11.1218 -qed "lemma_preal_rat_less4";
 11.1219 -
 11.1220 -Goalw [preal_of_prat_def,preal_mult_def] 
 11.1221 -      "preal_of_prat ((z1::prat) * z2) = \
 11.1222 -\      preal_of_prat z1 * preal_of_prat z2";
 11.1223 -by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
 11.1224 -by (auto_tac (claset() addIs [prat_mult_less_mono],
 11.1225 -     simpset() addsimps [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
 11.1226 -by (dtac prat_dense 1);
 11.1227 -by (Step_tac 1);
 11.1228 -by (res_inst_tac [("x","x*z1*qinv(xa)")] exI 1 THEN rtac conjI 1);
 11.1229 -by (etac lemma_preal_rat_less3 1);
 11.1230 -by (res_inst_tac [("x"," xa*z2*qinv(z1*z2)")] exI 1 THEN rtac conjI 1);
 11.1231 -by (etac lemma_preal_rat_less4 1);
 11.1232 -by (asm_full_simp_tac (simpset() 
 11.1233 -    addsimps [qinv_mult_eq RS sym] @ prat_mult_ac) 1);
 11.1234 -by (asm_full_simp_tac (simpset() 
 11.1235 -    addsimps [prat_mult_assoc RS sym]) 1);
 11.1236 -qed "preal_of_prat_mult";
 11.1237 -
 11.1238 -Goalw [preal_of_prat_def,preal_less_def] 
 11.1239 -      "(preal_of_prat p < preal_of_prat q) = (p < q)";
 11.1240 -by (auto_tac (claset() addSDs [lemma_prat_set_eq] addEs [prat_less_trans],
 11.1241 -              simpset() addsimps [lemma_prat_less_set_mem_preal,
 11.1242 -                                  psubset_def,prat_less_not_refl]));
 11.1243 -by (res_inst_tac [("q1.0","p"),("q2.0","q")] prat_linear_less2 1);
 11.1244 -by (auto_tac (claset() addIs [prat_less_irrefl],simpset()));
 11.1245 -qed "preal_of_prat_less_iff";
 11.1246 -
 11.1247 -Addsimps [preal_of_prat_less_iff];
    12.1 --- a/src/HOL/Real/PReal.thy	Thu Jan 01 10:06:32 2004 +0100
    12.2 +++ b/src/HOL/Real/PReal.thy	Thu Jan 01 21:47:07 2004 +0100
    12.3 @@ -3,41 +3,1303 @@
    12.4      Author      : Jacques D. Fleuriot
    12.5      Copyright   : 1998  University of Cambridge
    12.6      Description : The positive reals as Dedekind sections of positive
    12.7 -                  rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] 
    12.8 +         rationals. Fundamentals of Abstract Analysis [Gleason- p. 121]
    12.9                    provides some of the definitions.
   12.10  *)
   12.11  
   12.12 -PReal = PRat +
   12.13 +theory PReal = PRat:
   12.14  
   12.15  typedef preal = "{A::prat set. {} < A & A < UNIV &
   12.16 -                               (!y: A. ((!z. z < y --> z: A) &
   12.17 -                                        (? u: A. y < u)))}"      (preal_1)
   12.18 -instance
   12.19 -   preal :: {ord, plus, times}
   12.20 +                               (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
   12.21 +                                        (\<exists>u \<in> A. y < u)))}"
   12.22 +apply (rule exI) 
   12.23 +apply (rule preal_1) 
   12.24 +done
   12.25 +
   12.26 +
   12.27 +instance preal :: ord ..
   12.28 +instance preal :: plus ..
   12.29 +instance preal :: times ..
   12.30 +
   12.31  
   12.32  constdefs
   12.33 -  preal_of_prat :: prat => preal             
   12.34 +  preal_of_prat :: "prat => preal"
   12.35     "preal_of_prat q     == Abs_preal({x::prat. x < q})"
   12.36  
   12.37 -  pinv       :: preal => preal
   12.38 -  "pinv(R)   == Abs_preal({w. ? y. w < y & qinv y ~: Rep_preal(R)})" 
   12.39 +  pinv       :: "preal => preal"
   12.40 +  "pinv(R)   == Abs_preal({w. \<exists>y. w < y & qinv y \<notin> Rep_preal(R)})"
   12.41  
   12.42 -  psup       :: preal set => preal
   12.43 -  "psup(P)   == Abs_preal({w. ? X: P. w: Rep_preal(X)})"
   12.44 +  psup       :: "preal set => preal"
   12.45 +  "psup(P)   == Abs_preal({w. \<exists>X \<in> P. w \<in> Rep_preal(X)})"
   12.46  
   12.47 -defs
   12.48 +defs (overloaded)
   12.49  
   12.50 -  preal_add_def
   12.51 -    "R + S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x + y})"
   12.52 +  preal_add_def:
   12.53 +    "R + S == Abs_preal({w. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). w = x + y})"
   12.54  
   12.55 -  preal_mult_def
   12.56 -    "R * S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x * y})"
   12.57 +  preal_mult_def:
   12.58 +    "R * S == Abs_preal({w. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). w = x * y})"
   12.59  
   12.60 -  preal_less_def
   12.61 +  preal_less_def:
   12.62      "R < (S::preal) == Rep_preal(R) < Rep_preal(S)"
   12.63  
   12.64 -  preal_le_def
   12.65 -    "R <= (S::preal) == Rep_preal(R) <= Rep_preal(S)"
   12.66 - 
   12.67 +  preal_le_def:
   12.68 +    "R \<le> (S::preal) == Rep_preal(R) \<subseteq> Rep_preal(S)"
   12.69 +
   12.70 +
   12.71 +lemma inj_on_Abs_preal: "inj_on Abs_preal preal"
   12.72 +apply (rule inj_on_inverseI)
   12.73 +apply (erule Abs_preal_inverse)
   12.74 +done
   12.75 +
   12.76 +declare inj_on_Abs_preal [THEN inj_on_iff, simp]
   12.77 +
   12.78 +lemma inj_Rep_preal: "inj(Rep_preal)"
   12.79 +apply (rule inj_on_inverseI)
   12.80 +apply (rule Rep_preal_inverse)
   12.81 +done
   12.82 +
   12.83 +lemma empty_not_mem_preal [simp]: "{} \<notin> preal"
   12.84 +by (unfold preal_def, fast)
   12.85 +
   12.86 +lemma one_set_mem_preal: "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} \<in> preal"
   12.87 +apply (unfold preal_def)
   12.88 +apply (rule preal_1)
   12.89 +done
   12.90 +
   12.91 +declare one_set_mem_preal [simp]
   12.92 +
   12.93 +lemma preal_psubset_empty: "x \<in> preal ==> {} < x"
   12.94 +by (unfold preal_def, fast)
   12.95 +
   12.96 +lemma Rep_preal_psubset_empty: "{} < Rep_preal x"
   12.97 +by (rule Rep_preal [THEN preal_psubset_empty])
   12.98 +
   12.99 +lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
  12.100 +apply (cut_tac x = X in Rep_preal_psubset_empty)
  12.101 +apply (auto intro: equals0I [symmetric] simp add: psubset_def)
  12.102 +done
  12.103 +
  12.104 +lemma prealI1:
  12.105 +      "[| {} < A; A < UNIV;
  12.106 +               (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
  12.107 +                         (\<exists>u \<in> A. y < u))) |] ==> A \<in> preal"
  12.108 +apply (unfold preal_def, fast)
  12.109 +done
  12.110 +
  12.111 +lemma prealI2:
  12.112 +      "[| {} < A; A < UNIV;
  12.113 +               \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A);
  12.114 +               \<forall>y \<in> A. (\<exists>u \<in> A. y < u) |] ==> A \<in> preal"
  12.115 +
  12.116 +apply (unfold preal_def, best)
  12.117 +done
  12.118 +
  12.119 +lemma prealE_lemma:
  12.120 +      "A \<in> preal ==> {} < A & A < UNIV &
  12.121 +                          (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
  12.122 +                                   (\<exists>u \<in> A. y < u)))"
  12.123 +apply (unfold preal_def, fast)
  12.124 +done
  12.125 +
  12.126 +declare prealI1 [intro!] prealI2 [intro!]
  12.127 +
  12.128 +declare Abs_preal_inverse [simp]
  12.129 +
  12.130 +
  12.131 +lemma prealE_lemma1: "A \<in> preal ==> {} < A"
  12.132 +by (unfold preal_def, fast)
  12.133 +
  12.134 +lemma prealE_lemma2: "A \<in> preal ==> A < UNIV"
  12.135 +by (unfold preal_def, fast)
  12.136 +
  12.137 +lemma prealE_lemma3: "A \<in> preal ==> \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A)"
  12.138 +by (unfold preal_def, fast)
  12.139 +
  12.140 +lemma prealE_lemma3a: "[| A \<in> preal; y \<in> A |] ==> (\<forall>z. z < y --> z \<in> A)"
  12.141 +by (fast dest!: prealE_lemma3)
  12.142 +
  12.143 +lemma prealE_lemma3b: "[| A \<in> preal; y \<in> A; z < y |] ==> z \<in> A"
  12.144 +by (fast dest!: prealE_lemma3a)
  12.145 +
  12.146 +lemma prealE_lemma4: "A \<in> preal ==> \<forall>y \<in> A. (\<exists>u \<in> A. y < u)"
  12.147 +by (unfold preal_def, fast)
  12.148 +
  12.149 +lemma prealE_lemma4a: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
  12.150 +by (fast dest!: prealE_lemma4)
  12.151 +
  12.152 +lemma not_mem_Rep_preal_Ex: "\<exists>x. x\<notin> Rep_preal X"
  12.153 +apply (cut_tac x = X in Rep_preal)
  12.154 +apply (drule prealE_lemma2)
  12.155 +apply (auto simp add: psubset_def)
  12.156 +done
  12.157 +
  12.158 +
  12.159 +subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
  12.160 +
  12.161 +text{*A few lemmas*}
  12.162 +
  12.163 +lemma lemma_prat_less_set_mem_preal: "{u::prat. u < y} \<in> preal"
  12.164 +apply (cut_tac qless_Ex)
  12.165 +apply (auto intro: prat_less_trans elim!: prat_less_irrefl)
  12.166 +apply (blast dest: prat_dense)
  12.167 +done
  12.168 +
  12.169 +lemma lemma_prat_set_eq: "{u::prat. u < x} = {x. x < y} ==> x = y"
  12.170 +apply (insert prat_linear [of x y], safe)
  12.171 +apply (drule_tac [2] prat_dense, erule_tac [2] exE)
  12.172 +apply (drule prat_dense, erule exE)
  12.173 +apply (blast dest: prat_less_not_sym)
  12.174 +apply (blast dest: prat_less_not_sym)
  12.175 +done
  12.176 +
  12.177 +lemma inj_preal_of_prat: "inj(preal_of_prat)"
  12.178 +apply (rule inj_onI)
  12.179 +apply (unfold preal_of_prat_def)
  12.180 +apply (drule inj_on_Abs_preal [THEN inj_onD])
  12.181 +apply (rule lemma_prat_less_set_mem_preal)
  12.182 +apply (rule lemma_prat_less_set_mem_preal)
  12.183 +apply (erule lemma_prat_set_eq)
  12.184 +done
  12.185 +
  12.186 +
  12.187 +subsection{*Theorems for Ordering*}
  12.188 +
  12.189 +text{*A positive fraction not in a positive real is an upper bound.
  12.190 + Gleason p. 122 - Remark (1)*}
  12.191 +
  12.192 +lemma not_in_preal_ub: "x \<notin> Rep_preal(R) ==> \<forall>y \<in> Rep_preal(R). y < x"
  12.193 +apply (cut_tac x1 = R in Rep_preal [THEN prealE_lemma]) 
  12.194 +apply (blast intro: not_less_not_eq_prat_less)
  12.195 +done
  12.196 +
  12.197 +
  12.198 +text{*@{text preal_less} is a strict order: nonreflexive and transitive *}
  12.199 +
  12.200 +lemma preal_less_not_refl: "~ (x::preal) < x"
  12.201 +apply (unfold preal_less_def)
  12.202 +apply (simp (no_asm) add: psubset_def)
  12.203 +done
  12.204 +
  12.205 +lemmas preal_less_irrefl = preal_less_not_refl [THEN notE, standard]
  12.206 +
  12.207 +lemma preal_not_refl2: "!!(x::preal). x < y ==> x \<noteq> y"
  12.208 +by (auto simp add: preal_less_not_refl)
  12.209 +
  12.210 +lemma preal_less_trans: "!!(x::preal). [| x < y; y < z |] ==> x < z"
  12.211 +apply (unfold preal_less_def)
  12.212 +apply (auto dest: subsetD equalityI simp add: psubset_def)
  12.213 +done
  12.214 +
  12.215 +lemma preal_less_not_sym: "!! (q1::preal). q1 < q2 ==> ~ q2 < q1"
  12.216 +apply (rule notI)
  12.217 +apply (drule preal_less_trans, assumption)
  12.218 +apply (simp add: preal_less_not_refl)
  12.219 +done
  12.220 +
  12.221 +(* [| x < y;  ~P ==> y < x |] ==> P *)
  12.222 +lemmas preal_less_asym = preal_less_not_sym [THEN contrapos_np, standard]
  12.223 +
  12.224 +lemma preal_linear:
  12.225 +      "(x::preal) < y | x = y | y < x"
  12.226 +apply (unfold preal_less_def)
  12.227 +apply (auto dest!: inj_Rep_preal [THEN injD] simp add: psubset_def)
  12.228 +apply (rule prealE_lemma3b, rule Rep_preal, assumption)
  12.229 +apply (fast dest: not_in_preal_ub)
  12.230 +done
  12.231 +
  12.232 +
  12.233 +subsection{*Properties of Addition*}
  12.234 +
  12.235 +lemma preal_add_commute: "(x::preal) + y = y + x"
  12.236 +apply (unfold preal_add_def)
  12.237 +apply (rule_tac f = Abs_preal in arg_cong)
  12.238 +apply (blast intro: prat_add_commute [THEN subst])
  12.239 +done
  12.240 +
  12.241 +text{*Addition of two positive reals gives a positive real*}
  12.242 +
  12.243 +text{*Lemmas for proving positive reals addition set in @{typ preal}*}
  12.244 +
  12.245 +text{*Part 1 of Dedekind sections definition*}
  12.246 +lemma preal_add_set_not_empty:
  12.247 +     "{} < {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}"
  12.248 +apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex)
  12.249 +apply (auto intro!: psubsetI)
  12.250 +done
  12.251 +
  12.252 +text{*Part 2 of Dedekind sections definition*}
  12.253 +lemma preal_not_mem_add_set_Ex:
  12.254 +     "\<exists>q. q  \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}"
  12.255 +apply (cut_tac X = R in not_mem_Rep_preal_Ex)
  12.256 +apply (cut_tac X = S in not_mem_Rep_preal_Ex, clarify) 
  12.257 +apply (drule not_in_preal_ub)+
  12.258 +apply (rule_tac x = "x+xa" in exI)
  12.259 +apply (auto dest!: bspec) 
  12.260 +apply (drule prat_add_less_mono)
  12.261 +apply (auto simp add: prat_less_not_refl)
  12.262 +done
  12.263 +
  12.264 +lemma preal_add_set_not_prat_set:
  12.265 +     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y} < UNIV"
  12.266 +apply (auto intro!: psubsetI)
  12.267 +apply (cut_tac R = R and S = S in preal_not_mem_add_set_Ex, auto)
  12.268 +done
  12.269 +
  12.270 +text{*Part 3 of Dedekind sections definition*}
  12.271 +lemma preal_add_set_lemma3:
  12.272 +     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
  12.273 +         \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x+y}"
  12.274 +apply auto
  12.275 +apply (frule prat_mult_qinv_less_1)
  12.276 +apply (frule_tac x = x 
  12.277 +       in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"])
  12.278 +apply (frule_tac x = ya 
  12.279 +       in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"])
  12.280 +apply simp
  12.281 +apply (drule Rep_preal [THEN prealE_lemma3a])+
  12.282 +apply (erule allE)+
  12.283 +apply auto
  12.284 +apply (rule bexI)+
  12.285 +apply (auto simp add: prat_add_mult_distrib2 [symmetric] 
  12.286 +      prat_add_assoc [symmetric] prat_mult_assoc)
  12.287 +done
  12.288 +
  12.289 +lemma preal_add_set_lemma4:
  12.290 +     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
  12.291 +          \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}. y < u"
  12.292 +apply auto
  12.293 +apply (drule Rep_preal [THEN prealE_lemma4a])
  12.294 +apply (auto intro: prat_add_less2_mono1)
  12.295 +done
  12.296 +
  12.297 +lemma preal_mem_add_set:
  12.298 +     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y} \<in> preal"
  12.299 +apply (rule prealI2)
  12.300 +apply (rule preal_add_set_not_empty)
  12.301 +apply (rule preal_add_set_not_prat_set)
  12.302 +apply (rule preal_add_set_lemma3)
  12.303 +apply (rule preal_add_set_lemma4)
  12.304 +done
  12.305 +
  12.306 +lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
  12.307 +apply (unfold preal_add_def)
  12.308 +apply (rule_tac f = Abs_preal in arg_cong)
  12.309 +apply (simp (no_asm) add: preal_mem_add_set [THEN Abs_preal_inverse])
  12.310 +apply (auto simp add: prat_add_ac)
  12.311 +apply (rule bexI)
  12.312 +apply (auto intro!: exI simp add: prat_add_ac)
  12.313 +done
  12.314 +
  12.315 +lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
  12.316 +  apply (rule mk_left_commute [of "op +"])
  12.317 +  apply (rule preal_add_assoc)
  12.318 +  apply (rule preal_add_commute)
  12.319 +  done
  12.320 +
  12.321 +(* Positive Reals addition is an AC operator *)
  12.322 +lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
  12.323 +
  12.324 +
  12.325 +subsection{*Properties of Multiplication*}
  12.326 +
  12.327 +text{*Proofs essentially same as for addition*}
  12.328 +
  12.329 +lemma preal_mult_commute: "(x::preal) * y = y * x"
  12.330 +apply (unfold preal_mult_def)
  12.331 +apply (rule_tac f = Abs_preal in arg_cong)
  12.332 +apply (blast intro: prat_mult_commute [THEN subst])
  12.333 +done
  12.334 +
  12.335 +text{*Multiplication of two positive reals gives a positive real.}
  12.336 +
  12.337 +text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
  12.338 +
  12.339 +text{*Part 1 of Dedekind sections definition*}
  12.340 +lemma preal_mult_set_not_empty:
  12.341 +     "{} < {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}"
  12.342 +apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex)
  12.343 +apply (auto intro!: psubsetI)
  12.344 +done
  12.345 +
  12.346 +text{*Part 2 of Dedekind sections definition*}
  12.347 +lemma preal_not_mem_mult_set_Ex:
  12.348 +     "\<exists>q. q  \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}"
  12.349 +apply (cut_tac X = R in not_mem_Rep_preal_Ex)
  12.350 +apply (cut_tac X = S in not_mem_Rep_preal_Ex)
  12.351 +apply (erule exE)+
  12.352 +apply (drule not_in_preal_ub)+
  12.353 +apply (rule_tac x = "x*xa" in exI)
  12.354 +apply (auto, (erule ballE)+, auto)
  12.355 +apply (drule prat_mult_less_mono)
  12.356 +apply (auto simp add: prat_less_not_refl)
  12.357 +done
  12.358 +
  12.359 +lemma preal_mult_set_not_prat_set:
  12.360 +     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y} < UNIV"
  12.361 +apply (auto intro!: psubsetI)
  12.362 +apply (cut_tac R = R and S = S in preal_not_mem_mult_set_Ex, auto)
  12.363 +done
  12.364 +
  12.365 +text{*Part 3 of Dedekind sections definition*}
  12.366 +lemma preal_mult_set_lemma3:
  12.367 +     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
  12.368 +         \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x*y}"
  12.369 +apply auto
  12.370 +apply (frule_tac x = "qinv (ya)" in prat_mult_left_less2_mono1)
  12.371 +apply (simp add: prat_mult_ac)
  12.372 +apply (drule Rep_preal [THEN prealE_lemma3a])
  12.373 +apply (erule allE)
  12.374 +apply (rule bexI)+
  12.375 +apply (auto simp add: prat_mult_assoc)
  12.376 +done
  12.377 +
  12.378 +lemma preal_mult_set_lemma4:
  12.379 +     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
  12.380 +          \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}. y < u"
  12.381 +apply auto
  12.382 +apply (drule Rep_preal [THEN prealE_lemma4a])
  12.383 +apply (auto intro: prat_mult_less2_mono1)
  12.384 +done
  12.385 +
  12.386 +lemma preal_mem_mult_set:
  12.387 +     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y} \<in> preal"
  12.388 +apply (rule prealI2)
  12.389 +apply (rule preal_mult_set_not_empty)
  12.390 +apply (rule preal_mult_set_not_prat_set)
  12.391 +apply (rule preal_mult_set_lemma3)
  12.392 +apply (rule preal_mult_set_lemma4)
  12.393 +done
  12.394 +
  12.395 +lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
  12.396 +apply (unfold preal_mult_def)
  12.397 +apply (rule_tac f = Abs_preal in arg_cong)
  12.398 +apply (simp (no_asm) add: preal_mem_mult_set [THEN Abs_preal_inverse])
  12.399 +apply (auto simp add: prat_mult_ac)
  12.400 +apply (rule bexI)
  12.401 +apply (auto intro!: exI simp add: prat_mult_ac)
  12.402 +done
  12.403 +
  12.404 +lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
  12.405 +  apply (rule mk_left_commute [of "op *"])
  12.406 +  apply (rule preal_mult_assoc)
  12.407 +  apply (rule preal_mult_commute)
  12.408 +  done
  12.409 +
  12.410 +(* Positive Reals multiplication is an AC operator *)
  12.411 +lemmas preal_mult_ac =
  12.412 +       preal_mult_assoc preal_mult_commute preal_mult_left_commute
  12.413 +
  12.414 +(* Positive Real 1 is the multiplicative identity element *)
  12.415 +(* long *)
  12.416 +lemma preal_mult_1:
  12.417 +      "(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) * z = z"
  12.418 +apply (unfold preal_of_prat_def preal_mult_def)
  12.419 +apply (rule Rep_preal_inverse [THEN subst])
  12.420 +apply (rule_tac f = Abs_preal in arg_cong)
  12.421 +apply (rule one_set_mem_preal [THEN Abs_preal_inverse, THEN ssubst])
  12.422 +apply (auto simp add: Rep_preal_inverse)
  12.423 +apply (drule Rep_preal [THEN prealE_lemma4a]) 
  12.424 +apply (erule bexE) 
  12.425 +apply (drule prat_mult_less_mono)
  12.426 +apply (auto dest: Rep_preal [THEN prealE_lemma3a])
  12.427 +apply (frule Rep_preal [THEN prealE_lemma4a]) 
  12.428 +apply (erule bexE) 
  12.429 +apply (frule_tac x = "qinv (u)" in prat_mult_less2_mono1)
  12.430 +apply (rule exI, auto, rule_tac x = u in bexI)
  12.431 +apply (auto simp add: prat_mult_assoc)
  12.432 +done
  12.433 +
  12.434 +lemma preal_mult_1_right:
  12.435 +     "z * (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) = z"
  12.436 +apply (rule preal_mult_commute [THEN subst])
  12.437 +apply (rule preal_mult_1)
  12.438 +done
  12.439 +
  12.440 +
  12.441 +subsection{*Distribution of Multiplication across Addition*}
  12.442 +
  12.443 +lemma mem_Rep_preal_addD:
  12.444 +      "z \<in> Rep_preal(R+S) ==>
  12.445 +            \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x + y"
  12.446 +apply (unfold preal_add_def)
  12.447 +apply (drule preal_mem_add_set [THEN Abs_preal_inverse, THEN subst], fast)
  12.448 +done
  12.449 +
  12.450 +lemma mem_Rep_preal_addI:
  12.451 +      "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x + y
  12.452 +       ==> z \<in> Rep_preal(R+S)"
  12.453 +apply (unfold preal_add_def)
  12.454 +apply (rule preal_mem_add_set [THEN Abs_preal_inverse, THEN ssubst], fast)
  12.455 +done
  12.456 +
  12.457 +lemma mem_Rep_preal_add_iff:
  12.458 +     "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal(R).
  12.459 +                                  \<exists>y \<in> Rep_preal(S). z = x + y)"
  12.460 +apply (fast intro!: mem_Rep_preal_addD mem_Rep_preal_addI)
  12.461 +done
  12.462 +
  12.463 +lemma mem_Rep_preal_multD:
  12.464 +      "z \<in> Rep_preal(R*S) ==>
  12.465 +            \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y"
  12.466 +apply (unfold preal_mult_def)
  12.467 +apply (drule preal_mem_mult_set [THEN Abs_preal_inverse, THEN subst], fast)
  12.468 +done
  12.469 +
  12.470 +lemma mem_Rep_preal_multI:
  12.471 +      "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y
  12.472 +       ==> z \<in> Rep_preal(R*S)"
  12.473 +apply (unfold preal_mult_def)
  12.474 +apply (rule preal_mem_mult_set [THEN Abs_preal_inverse, THEN ssubst], fast)
  12.475 +done
  12.476 +
  12.477 +lemma mem_Rep_preal_mult_iff:
  12.478 +     "(z \<in> Rep_preal(R*S)) =
  12.479 +      (\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y)"
  12.480 +by (fast intro!: mem_Rep_preal_multD mem_Rep_preal_multI)
  12.481 +
  12.482 +lemma lemma_add_mult_mem_Rep_preal:
  12.483 +     "[| xb \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
  12.484 +                   Rep_preal w; yb \<in> Rep_preal w |] ==>
  12.485 +                   xb * ya + xc * yb \<in> Rep_preal (z1 * w + z2 * w)"
  12.486 +by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI)
  12.487 +
  12.488 +lemma lemma_add_mult_mem_Rep_preal1:
  12.489 +     "[| xb \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
  12.490 +                   Rep_preal w; yb \<in> Rep_preal w |] ==>
  12.491 +                   yb*(xb + xc) \<in> Rep_preal (w*(z1 + z2))"
  12.492 +by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI)
  12.493 +
  12.494 +lemma lemma_preal_add_mult_distrib:
  12.495 +     "x \<in> Rep_preal (w * z1 + w * z2) ==>
  12.496 +               x \<in> Rep_preal (w * (z1 + z2))"
  12.497 +apply (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD)
  12.498 +apply (frule_tac ya = xa and yb = xb and xb = ya and xc = yb in lemma_add_mult_mem_Rep_preal1, auto)
  12.499 +apply (rule_tac x = xa and y = xb in prat_linear_less2)
  12.500 +apply (drule_tac b = ya and c = yb in lemma_prat_add_mult_mono)
  12.501 +apply (rule Rep_preal [THEN prealE_lemma3b])
  12.502 +apply (auto simp add: prat_add_mult_distrib2)
  12.503 +apply (drule_tac ya = xb and yb = xa and xc = ya and xb = yb in lemma_add_mult_mem_Rep_preal1, auto)
  12.504 +apply (drule_tac b = yb and c = ya in lemma_prat_add_mult_mono)
  12.505 +apply (rule Rep_preal [THEN prealE_lemma3b])
  12.506 +apply (erule_tac V = "xb * ya + xb * yb \<in> Rep_preal (w * (z1 + z2))" in thin_rl)
  12.507 +apply (auto simp add: prat_add_mult_distrib prat_add_commute preal_add_ac)
  12.508 +done
  12.509 +
  12.510 +lemma lemma_preal_add_mult_distrib2:
  12.511 +     "x \<in> Rep_preal (w * (z1 + z2)) ==>
  12.512 +               x \<in> Rep_preal (w * z1 + w * z2)"
  12.513 +by (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD
  12.514 +         intro!: bexI mem_Rep_preal_addI mem_Rep_preal_multI 
  12.515 +         simp add: prat_add_mult_distrib2)
  12.516 +
  12.517 +lemma preal_add_mult_distrib2: "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)"
  12.518 +apply (rule inj_Rep_preal [THEN injD])
  12.519 +apply (fast intro: lemma_preal_add_mult_distrib lemma_preal_add_mult_distrib2)
  12.520 +done
  12.521 +
  12.522 +lemma preal_add_mult_distrib: "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)"
  12.523 +apply (simp (no_asm) add: preal_mult_commute preal_add_mult_distrib2)
  12.524 +done
  12.525 +
  12.526 +
  12.527 +subsection{*Existence of Inverse, a Positive Real*}
  12.528 +
  12.529 +lemma qinv_not_mem_Rep_preal_Ex: "\<exists>y. qinv(y) \<notin>  Rep_preal X"
  12.530 +apply (cut_tac X = X in not_mem_Rep_preal_Ex)
  12.531 +apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto)
  12.532 +done
  12.533 +
  12.534 +lemma lemma_preal_mem_inv_set_ex:
  12.535 +     "\<exists>q. q \<in> {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
  12.536 +apply (cut_tac X = A in qinv_not_mem_Rep_preal_Ex, auto)
  12.537 +apply (cut_tac y = y in qless_Ex, fast)
  12.538 +done
  12.539 +
  12.540 +text{*Part 1 of Dedekind sections definition*}
  12.541 +lemma preal_inv_set_not_empty: "{} < {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
  12.542 +apply (cut_tac lemma_preal_mem_inv_set_ex)
  12.543 +apply (auto intro!: psubsetI)
  12.544 +done
  12.545 +
  12.546 +text{*Part 2 of Dedekind sections definition*}
  12.547 +lemma qinv_mem_Rep_preal_Ex: "\<exists>y. qinv(y) \<in>  Rep_preal X"
  12.548 +apply (cut_tac X = X in mem_Rep_preal_Ex)
  12.549 +apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto)
  12.550 +done
  12.551 +
  12.552 +lemma preal_not_mem_inv_set_Ex:
  12.553 +     "\<exists>x. x \<notin> {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
  12.554 +apply (rule ccontr)
  12.555 +apply (cut_tac X = A in qinv_mem_Rep_preal_Ex, auto)
  12.556 +apply (erule allE, clarify) 
  12.557 +apply (drule qinv_prat_less, drule not_in_preal_ub)
  12.558 +apply (erule_tac x = "qinv y" in ballE)
  12.559 +apply (drule prat_less_trans)
  12.560 +apply (auto simp add: prat_less_not_refl)
  12.561 +done
  12.562 +
  12.563 +lemma preal_inv_set_not_prat_set:
  12.564 +     "{x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A} < UNIV"
  12.565 +apply (auto intro!: psubsetI)
  12.566 +apply (cut_tac A = A in preal_not_mem_inv_set_Ex, auto)
  12.567 +done
  12.568 +
  12.569 +text{*Part 3 of Dedekind sections definition*}
  12.570 +lemma preal_inv_set_lemma3:
  12.571 +     "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
  12.572 +        \<forall>z. z < y --> z \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}"
  12.573 +apply auto
  12.574 +apply (rule_tac x = ya in exI)
  12.575 +apply (auto intro: prat_less_trans)
  12.576 +done
  12.577 +
  12.578 +lemma preal_inv_set_lemma4:
  12.579 +     "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
  12.580 +        Bex {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A} (op < y)"
  12.581 +by (blast dest: prat_dense)
  12.582 +
  12.583 +lemma preal_mem_inv_set: "{x. \<exists>y. x < y & qinv(y) \<notin> Rep_preal(A)} \<in> preal"
  12.584 +apply (rule prealI2)
  12.585 +apply (rule preal_inv_set_not_empty)
  12.586 +apply (rule preal_inv_set_not_prat_set)
  12.587 +apply (rule preal_inv_set_lemma3)
  12.588 +apply (rule preal_inv_set_lemma4)
  12.589 +done
  12.590 +
  12.591 +(*more lemmas for inverse *)
  12.592 +lemma preal_mem_mult_invD:
  12.593 +     "x \<in> Rep_preal(pinv(A)*A) ==>
  12.594 +      x \<in> Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
  12.595 +apply (auto dest!: mem_Rep_preal_multD simp add: pinv_def preal_of_prat_def)
  12.596 +apply (drule preal_mem_inv_set [THEN Abs_preal_inverse, THEN subst])
  12.597 +apply (auto dest!: not_in_preal_ub)
  12.598 +apply (drule prat_mult_less_mono, blast, auto)
  12.599 +done
  12.600 +
  12.601 +subsection{*Gleason's Lemma 9-3.4, page 122*}
  12.602 +
  12.603 +lemma lemma1_gleason9_34:
  12.604 +     "\<forall>xa \<in> Rep_preal(A). xa + x \<in> Rep_preal(A) ==>
  12.605 +             \<exists>xb \<in> Rep_preal(A). xb + (prat_of_pnat p)*x \<in> Rep_preal(A)"
  12.606 +apply (cut_tac mem_Rep_preal_Ex)
  12.607 +apply (induct_tac "p" rule: pnat_induct)
  12.608 +apply (auto simp add: pnat_one_def pSuc_is_plus_one prat_add_mult_distrib 
  12.609 +                      prat_of_pnat_add prat_add_assoc [symmetric])
  12.610 +done
  12.611 +
  12.612 +lemma lemma1b_gleason9_34:
  12.613 +     "Abs_prat (ratrel `` {(y, z)}) < 
  12.614 +      xb +
  12.615 +      Abs_prat (ratrel `` {(x*y, Abs_pnat (Suc 0))}) * 
  12.616 +      Abs_prat (ratrel `` {(w, x)})"
  12.617 +apply (rule_tac j =
  12.618 +        "Abs_prat (ratrel `` 
  12.619 +           { (x * y, Abs_pnat (Suc 0))}) * Abs_prat (ratrel `` {(w, x)})" 
  12.620 +       in prat_le_less_trans)
  12.621 +apply (rule_tac [2] prat_self_less_add_right)
  12.622 +apply (auto intro: lemma_Abs_prat_le3 
  12.623 +            simp add: prat_mult pre_lemma_gleason9_34b pnat_mult_assoc)
  12.624 +done
  12.625 +
  12.626 +lemma lemma_gleason9_34a:
  12.627 +     "\<forall>xa \<in> Rep_preal(A). xa + x \<in> Rep_preal(A) ==> False"
  12.628 +apply (cut_tac X = A in not_mem_Rep_preal_Ex)
  12.629 +apply (erule exE)
  12.630 +apply (drule not_in_preal_ub)
  12.631 +apply (rule_tac z = x in eq_Abs_prat)
  12.632 +apply (rule_tac z = xa in eq_Abs_prat)
  12.633 +apply (drule_tac p = "y*xb" in lemma1_gleason9_34)
  12.634 +apply (erule bexE)
  12.635 +apply (cut_tac x = y and y = xb and w = xaa and z = ya and xb = xba in lemma1b_gleason9_34)
  12.636 +apply (drule_tac x = "xba + prat_of_pnat (y * xb) * x" in bspec)
  12.637 +apply (auto intro: prat_less_asym simp add: prat_of_pnat_def)
  12.638 +done
  12.639 +
  12.640 +lemma lemma_gleason9_34: "\<exists>r \<in> Rep_preal(R). r + x \<notin> Rep_preal(R)"
  12.641 +apply (rule ccontr)
  12.642 +apply (blast intro: lemma_gleason9_34a)
  12.643 +done
  12.644 +
  12.645 +
  12.646 +subsection{*Gleason's Lemma 9-3.6*}
  12.647 +
  12.648 +lemma lemma1_gleason9_36: "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)"
  12.649 +apply (simp (no_asm_use) add: prat_add_mult_distrib2 prat_mult_assoc)
  12.650 +done
  12.651 +
  12.652 +lemma lemma2_gleason9_36: "r*qinv(xa)*(xa*x) = r*x"
  12.653 +apply (simp (no_asm_use) add: prat_mult_ac)
  12.654 +done
  12.655 +
  12.656 +(*** FIXME: long! ***)
  12.657 +lemma lemma_gleason9_36:
  12.658 +     "prat_of_pnat 1 < x ==> \<exists>r \<in> Rep_preal(A). r*x \<notin> Rep_preal(A)"
  12.659 +apply (rule_tac X1 = A in mem_Rep_preal_Ex [THEN exE])
  12.660 +apply (rule_tac Q = "xa*x \<in> Rep_preal (A) " in excluded_middle [THEN disjE])
  12.661 +apply fast
  12.662 +apply (drule_tac x = xa in prat_self_less_mult_right)
  12.663 +apply (erule prat_lessE)
  12.664 +apply (cut_tac R = A and x = Q3 in lemma_gleason9_34)
  12.665 +apply (drule sym, auto)
  12.666 +apply (frule not_in_preal_ub)
  12.667 +apply (drule_tac x = "xa + Q3" in bspec, assumption)
  12.668 +apply (drule prat_add_right_less_cancel)
  12.669 +apply (drule_tac x = "qinv (xa) *Q3" in prat_mult_less2_mono1)
  12.670 +apply (drule_tac x = r in prat_add_less2_mono2)
  12.671 +apply (simp add: prat_mult_assoc [symmetric] lemma1_gleason9_36)
  12.672 +apply (drule sym)
  12.673 +apply (auto simp add: lemma2_gleason9_36)
  12.674 +apply (rule_tac x = r in bexI)
  12.675 +apply (rule notI)
  12.676 +apply (drule_tac y = "r*x" in Rep_preal [THEN prealE_lemma3b], auto)
  12.677 +done
  12.678 +
  12.679 +lemma lemma_gleason9_36a:
  12.680 +     "prat_of_pnat (Abs_pnat (Suc 0)) < x ==>
  12.681 +      \<exists>r \<in> Rep_preal(A). r*x \<notin> Rep_preal(A)"
  12.682 +apply (rule lemma_gleason9_36)
  12.683 +apply (simp (no_asm_simp) add: pnat_one_def)
  12.684 +done
  12.685 +
  12.686 +
  12.687 +subsection{*Existence of Inverse: Part 2*}
  12.688 +lemma preal_mem_mult_invI:
  12.689 +     "x \<in> Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))
  12.690 +      ==> x \<in> Rep_preal(pinv(A)*A)"
  12.691 +apply (auto intro!: mem_Rep_preal_multI simp add: pinv_def preal_of_prat_def)
  12.692 +apply (rule preal_mem_inv_set [THEN Abs_preal_inverse, THEN ssubst])
  12.693 +apply (drule prat_qinv_gt_1)
  12.694 +apply (drule_tac A = A in lemma_gleason9_36a, auto)
  12.695 +apply (drule Rep_preal [THEN prealE_lemma4a])
  12.696 +apply (auto, drule qinv_prat_less)
  12.697 +apply (rule_tac x = "qinv (u) *x" in exI)
  12.698 +apply (rule conjI)
  12.699 +apply (rule_tac x = "qinv (r) *x" in exI)
  12.700 +apply (auto intro: prat_mult_less2_mono1 simp add: qinv_mult_eq qinv_qinv)
  12.701 +apply (rule_tac x = u in bexI)
  12.702 +apply (auto simp add: prat_mult_assoc prat_mult_left_commute)
  12.703 +done
  12.704 +
  12.705 +lemma preal_mult_inv:
  12.706 +     "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
  12.707 +apply (rule inj_Rep_preal [THEN injD])
  12.708 +apply (fast dest: preal_mem_mult_invD preal_mem_mult_invI)
  12.709 +done
  12.710 +
  12.711 +lemma preal_mult_inv_right:
  12.712 +     "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
  12.713 +apply (rule preal_mult_commute [THEN subst])
  12.714 +apply (rule preal_mult_inv)
  12.715 +done
  12.716 +
  12.717 +
  12.718 +text{*Theorems needing @{text lemma_gleason9_34}*}
  12.719 +
  12.720 +lemma Rep_preal_self_subset: "Rep_preal (R1) \<subseteq> Rep_preal(R1 + R2)"
  12.721 +apply (cut_tac X = R2 in mem_Rep_preal_Ex)
  12.722 +apply (auto intro!: bexI 
  12.723 +            intro: Rep_preal [THEN prealE_lemma3b] prat_self_less_add_left 
  12.724 +                   mem_Rep_preal_addI)
  12.725 +done
  12.726 +
  12.727 +lemma Rep_preal_sum_not_subset: "~ Rep_preal (R1 + R2) \<subseteq> Rep_preal(R1)"
  12.728 +apply (cut_tac X = R2 in mem_Rep_preal_Ex)
  12.729 +apply (erule exE)
  12.730 +apply (cut_tac R = R1 in lemma_gleason9_34)
  12.731 +apply (auto intro: mem_Rep_preal_addI)
  12.732 +done
  12.733 +
  12.734 +lemma Rep_preal_sum_not_eq: "Rep_preal (R1 + R2) \<noteq> Rep_preal(R1)"
  12.735 +apply (rule notI)
  12.736 +apply (erule equalityE)
  12.737 +apply (simp add: Rep_preal_sum_not_subset)
  12.738 +done
  12.739 +
  12.740 +text{*at last, Gleason prop. 9-3.5(iii) page 123*}
  12.741 +lemma preal_self_less_add_left: "(R1::preal) < R1 + R2"
  12.742 +apply (unfold preal_less_def psubset_def)
  12.743 +apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
  12.744 +done
  12.745 +
  12.746 +lemma preal_self_less_add_right: "(R1::preal) < R2 + R1"
  12.747 +apply (simp add: preal_add_commute preal_self_less_add_left)
  12.748 +done
  12.749 +
  12.750 +
  12.751 +subsection{*The @{text "\<le>"} Ordering*}
  12.752 +
  12.753 +lemma preal_less_le_iff: "(~(w < z)) = (z \<le> (w::preal))"
  12.754 +apply (unfold preal_le_def psubset_def preal_less_def)
  12.755 +apply (insert preal_linear [of w z])
  12.756 +apply (auto simp add: preal_less_def psubset_def)
  12.757 +done
  12.758 +
  12.759 +lemma preal_le_iff_less_or_eq:
  12.760 +     "((x::preal) \<le> y) = (x < y | x = y)"
  12.761 +apply (unfold preal_le_def preal_less_def psubset_def)
  12.762 +apply (auto intro: inj_Rep_preal [THEN injD])
  12.763 +done
  12.764 +
  12.765 +lemma preal_le_refl: "w \<le> (w::preal)"
  12.766 +apply (simp add: preal_le_def)
  12.767 +done
  12.768 +
  12.769 +lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
  12.770 +apply (simp add: preal_le_iff_less_or_eq) 
  12.771 +apply (blast intro: preal_less_trans)
  12.772 +done
  12.773 +
  12.774 +lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
  12.775 +apply (simp add: preal_le_iff_less_or_eq) 
  12.776 +apply (blast intro: preal_less_asym)
  12.777 +done
  12.778 +
  12.779 +lemma preal_neq_iff: "(w \<noteq> z) = (w<z | z < (w::preal))"
  12.780 +apply (insert preal_linear [of w z])
  12.781 +apply (auto elim: preal_less_irrefl)
  12.782 +done
  12.783 +
  12.784 +(* Axiom 'order_less_le' of class 'order': *)
  12.785 +lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
  12.786 +apply (simp (no_asm) add: preal_less_le_iff [symmetric] preal_neq_iff)
  12.787 +apply (blast elim!: preal_less_asym)
  12.788 +done
  12.789 +
  12.790 +instance preal :: order
  12.791 +proof qed
  12.792 + (assumption |
  12.793 +  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
  12.794 +
  12.795 +lemma preal_le_linear: "x <= y | y <= (x::preal)"
  12.796 +apply (insert preal_linear [of x y]) 
  12.797 +apply (auto simp add: order_less_le) 
  12.798 +done
  12.799 +
  12.800 +instance preal :: linorder
  12.801 +  by (intro_classes, rule preal_le_linear)
  12.802 +
  12.803 +
  12.804 +subsection{*Gleason prop. 9-3.5(iv), page 123*}
  12.805 +
  12.806 +text{*Proving @{term "A < B ==> \<exists>D. A + D = B"}*}
  12.807 +
  12.808 +text{*Define the claimed D and show that it is a positive real*}
  12.809 +
  12.810 +text{*Part 1 of Dedekind sections definition*}
  12.811 +lemma lemma_ex_mem_less_left_add1:
  12.812 +     "A < B ==>
  12.813 +      \<exists>q. q \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
  12.814 +apply (unfold preal_less_def psubset_def)
  12.815 +apply (clarify) 
  12.816 +apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma4a])
  12.817 +apply (auto simp add: prat_less_def)
  12.818 +done
  12.819 +
  12.820 +lemma preal_less_set_not_empty:
  12.821 +     "A < B ==> {} < {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
  12.822 +apply (drule lemma_ex_mem_less_left_add1)
  12.823 +apply (auto intro!: psubsetI)
  12.824 +done
  12.825 +
  12.826 +text{*Part 2 of Dedekind sections definition*}
  12.827 +lemma lemma_ex_not_mem_less_left_add1:
  12.828 +     "\<exists>q. q \<notin> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
  12.829 +apply (cut_tac X = B in not_mem_Rep_preal_Ex)
  12.830 +apply (erule exE)
  12.831 +apply (rule_tac x = x in exI, auto)
  12.832 +apply (cut_tac x = x and y = n in prat_self_less_add_right)
  12.833 +apply (auto dest: Rep_preal [THEN prealE_lemma3b])
  12.834 +done
  12.835 +
  12.836 +lemma preal_less_set_not_prat_set:
  12.837 +     "{d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)} < UNIV"
  12.838 +apply (auto intro!: psubsetI)
  12.839 +apply (cut_tac A = A and B = B in lemma_ex_not_mem_less_left_add1, auto)
  12.840 +done
  12.841 +
  12.842 +text{*Part 3 of Dedekind sections definition*}
  12.843 +lemma preal_less_set_lemma3:
  12.844 +     "A < B ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
  12.845 +     \<forall>z. z < y --> z \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
  12.846 +apply auto
  12.847 +apply (drule_tac x = n in prat_add_less2_mono2)
  12.848 +apply (drule Rep_preal [THEN prealE_lemma3b], auto)
  12.849 +done
  12.850 +
  12.851 +lemma preal_less_set_lemma4:
  12.852 +     "A < B ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
  12.853 +        Bex {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)} (op < y)"
  12.854 +apply auto
  12.855 +apply (drule Rep_preal [THEN prealE_lemma4a])
  12.856 +apply (auto simp add: prat_less_def prat_add_assoc)
  12.857 +done
  12.858 +
  12.859 +lemma preal_mem_less_set:
  12.860 +     "!! (A::preal). A < B ==>
  12.861 +      {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}: preal"
  12.862 +apply (rule prealI2)
  12.863 +apply (rule preal_less_set_not_empty)
  12.864 +apply (rule_tac [2] preal_less_set_not_prat_set)
  12.865 +apply (rule_tac [2] preal_less_set_lemma3)
  12.866 +apply (rule_tac [3] preal_less_set_lemma4, auto)
  12.867 +done
  12.868 +
  12.869 +text{*proving that @{term "A + D \<le> B"}*}
  12.870 +lemma preal_less_add_left_subsetI:
  12.871 +       "!! (A::preal). A < B ==>
  12.872 +          A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}) \<le> B"
  12.873 +apply (unfold preal_le_def)
  12.874 +apply (rule subsetI)
  12.875 +apply (drule mem_Rep_preal_addD)
  12.876 +apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse])
  12.877 +apply (drule not_in_preal_ub)
  12.878 +apply (drule bspec, assumption)
  12.879 +apply (drule_tac x = y in prat_add_less2_mono1)
  12.880 +apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma3b], auto)
  12.881 +done
  12.882 +
  12.883 +subsection{*proving that @{term "B \<le> A + D"} --- trickier*}
  12.884 +
  12.885 +lemma lemma_sum_mem_Rep_preal_ex:
  12.886 +     "x \<in> Rep_preal(B) ==> \<exists>e. x + e \<in> Rep_preal(B)"
  12.887 +apply (drule Rep_preal [THEN prealE_lemma4a])
  12.888 +apply (auto simp add: prat_less_def)
  12.889 +done
  12.890 +
  12.891 +lemma preal_less_add_left_subsetI2:
  12.892 +       "!! (A::preal). A < B ==>
  12.893 +          B \<le> A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)})"
  12.894 +apply (unfold preal_le_def)
  12.895 +apply (rule subsetI)
  12.896 +apply (rule_tac Q = "x \<in> Rep_preal (A) " in excluded_middle [THEN disjE])
  12.897 +apply (rule mem_Rep_preal_addI)
  12.898 +apply (drule lemma_sum_mem_Rep_preal_ex)
  12.899 +apply (erule exE)
  12.900 +apply (cut_tac R = A and x = e in lemma_gleason9_34, erule bexE)
  12.901 +apply (drule not_in_preal_ub, drule bspec, assumption)
  12.902 +apply (erule prat_lessE)
  12.903 +apply (rule_tac x = r in bexI)
  12.904 +apply (rule_tac x = Q3 in bexI)
  12.905 +apply (cut_tac [4] Rep_preal_self_subset)
  12.906 +apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse])
  12.907 +apply (rule_tac x = "r+e" in exI)
  12.908 +apply (simp add: prat_add_ac)
  12.909 +done
  12.910 +
  12.911 +(*** required proof ***)
  12.912 +lemma preal_less_add_left:
  12.913 +     "!! (A::preal). A < B ==>
  12.914 +          A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}) = B"
  12.915 +apply (blast intro: preal_le_anti_sym preal_less_add_left_subsetI preal_less_add_left_subsetI2)
  12.916 +done
  12.917 +
  12.918 +lemma preal_less_add_left_Ex: "!! (A::preal). A < B ==> \<exists>D. A + D = B"
  12.919 +by (fast dest: preal_less_add_left)
  12.920 +
  12.921 +lemma preal_add_less2_mono1: "!!(A::preal). A < B ==> A + C < B + C"
  12.922 +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_assoc)
  12.923 +apply (rule_tac y1 = D in preal_add_commute [THEN subst])
  12.924 +apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
  12.925 +done
  12.926 +
  12.927 +lemma preal_add_less2_mono2: "!!(A::preal). A < B ==> C + A < C + B"
  12.928 +by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute)
  12.929 +
  12.930 +lemma preal_mult_less_mono1:
  12.931 +      "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x"
  12.932 +apply (drule preal_less_add_left_Ex)
  12.933 +apply (auto simp add: preal_add_mult_distrib preal_self_less_add_left)
  12.934 +done
  12.935 +
  12.936 +lemma preal_mult_left_less_mono1: "!!(q1::preal). q1 < q2  ==> x * q1 < x * q2"
  12.937 +by (auto dest: preal_mult_less_mono1 simp add: preal_mult_commute)
  12.938 +
  12.939 +lemma preal_mult_left_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> x * q1 \<le> x * q2"
  12.940 +apply (simp add: preal_le_iff_less_or_eq) 
  12.941 +apply (blast intro!: preal_mult_left_less_mono1)
  12.942 +done
  12.943 +
  12.944 +lemma preal_mult_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> q1 * x \<le> q2 * x"
  12.945 +by (auto dest: preal_mult_left_le_mono1 simp add: preal_mult_commute)
  12.946 +
  12.947 +lemma preal_add_left_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> x + q1 \<le> x + q2"
  12.948 +apply (simp add: preal_le_iff_less_or_eq) 
  12.949 +apply (auto intro!: preal_add_less2_mono1 simp add: preal_add_commute)
  12.950 +done
  12.951 +
  12.952 +lemma preal_add_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> q1 + x \<le> q2 + x"
  12.953 +by (auto dest: preal_add_left_le_mono1 simp add: preal_add_commute)
  12.954 +
  12.955 +lemma preal_add_right_less_cancel: "!!(A::preal). A + C < B + C ==> A < B"
  12.956 +apply (cut_tac preal_linear)
  12.957 +apply (auto elim: preal_less_irrefl)
  12.958 +apply (drule_tac A = B and C = C in preal_add_less2_mono1)
  12.959 +apply (fast dest: preal_less_trans elim: preal_less_irrefl)
  12.960 +done
  12.961 +
  12.962 +lemma preal_add_left_less_cancel: "!!(A::preal). C + A < C + B ==> A < B"
  12.963 +by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute)
  12.964 +
  12.965 +lemma preal_add_less_iff1 [simp]: "((A::preal) + C < B + C) = (A < B)"
  12.966 +by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
  12.967 +
  12.968 +lemma preal_add_less_iff2 [simp]: "(C + (A::preal) < C + B) = (A < B)"
  12.969 +by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
  12.970 +
  12.971 +lemma preal_add_less_mono:
  12.972 +     "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
  12.973 +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_ac)
  12.974 +apply (rule preal_add_assoc [THEN subst])
  12.975 +apply (rule preal_self_less_add_right)
  12.976 +done
  12.977 +
  12.978 +lemma preal_mult_less_mono:
  12.979 +     "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)"
  12.980 +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_mult_distrib preal_add_mult_distrib2 preal_self_less_add_left preal_add_assoc preal_mult_ac)
  12.981 +done
  12.982 +
  12.983 +lemma preal_add_right_cancel: "(A::preal) + C = B + C ==> A = B"
  12.984 +apply (cut_tac preal_linear [of A B], safe)
  12.985 +apply (drule_tac [!] C = C in preal_add_less2_mono1)
  12.986 +apply (auto elim: preal_less_irrefl)
  12.987 +done
  12.988 +
  12.989 +lemma preal_add_left_cancel: "!!(A::preal). C + A = C + B ==> A = B"
  12.990 +by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
  12.991 +
  12.992 +lemma preal_add_left_cancel_iff [simp]: "(C + A = C + B) = ((A::preal) = B)"
  12.993 +by (fast intro: preal_add_left_cancel)
  12.994 +
  12.995 +lemma preal_add_right_cancel_iff [simp]: "(A + C = B + C) = ((A::preal) = B)"
  12.996 +by (fast intro: preal_add_right_cancel)
  12.997 +
  12.998 +
  12.999 +
 12.1000 +subsection{*Completeness of type @{typ preal}*}
 12.1001 +
 12.1002 +text{*Prove that supremum is a cut*}
 12.1003 +
 12.1004 +lemma preal_sup_mem_Ex:
 12.1005 +     "\<exists>X. X \<in> P ==> \<exists>q.  q \<in> {w. \<exists>X. X \<in> P & w \<in> Rep_preal X}"
 12.1006 +apply safe
 12.1007 +apply (cut_tac X = X in mem_Rep_preal_Ex, auto)
 12.1008 +done
 12.1009 +
 12.1010 +text{*Part 1 of Dedekind sections definition*}
 12.1011 +lemma preal_sup_set_not_empty:
 12.1012 +     "\<exists>(X::preal). X \<in> P ==>
 12.1013 +          {} < {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
 12.1014 +apply (drule preal_sup_mem_Ex)
 12.1015 +apply (auto intro!: psubsetI)
 12.1016 +done
 12.1017 +
 12.1018 +text{*Part 2 of Dedekind sections definition*}
 12.1019 +lemma preal_sup_not_mem_Ex:
 12.1020 +     "\<exists>Y. (\<forall>X \<in> P. X < Y)
 12.1021 +          ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> Rep_preal(X)}"
 12.1022 +apply (unfold preal_less_def)
 12.1023 +apply (auto simp add: psubset_def)
 12.1024 +apply (cut_tac X = Y in not_mem_Rep_preal_Ex)
 12.1025 +apply (erule exE)
 12.1026 +apply (rule_tac x = x in exI)
 12.1027 +apply (auto dest!: bspec)
 12.1028 +done
 12.1029 +
 12.1030 +lemma preal_sup_not_mem_Ex1:
 12.1031 +     "\<exists>Y. (\<forall>X \<in> P. X \<le> Y)
 12.1032 +          ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> Rep_preal(X)}"
 12.1033 +apply (unfold preal_le_def, safe)
 12.1034 +apply (cut_tac X = Y in not_mem_Rep_preal_Ex)
 12.1035 +apply (erule exE)
 12.1036 +apply (rule_tac x = x in exI)
 12.1037 +apply (auto dest!: bspec)
 12.1038 +done
 12.1039 +
 12.1040 +lemma preal_sup_set_not_prat_set:
 12.1041 +     "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)} < UNIV"
 12.1042 +apply (drule preal_sup_not_mem_Ex)
 12.1043 +apply (auto intro!: psubsetI)
 12.1044 +done
 12.1045 +
 12.1046 +lemma preal_sup_set_not_prat_set1:
 12.1047 +     "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)} < UNIV"
 12.1048 +apply (drule preal_sup_not_mem_Ex1)
 12.1049 +apply (auto intro!: psubsetI)
 12.1050 +done
 12.1051 +
 12.1052 +text{*Part 3 of Dedekind sections definition*}
 12.1053 +lemma preal_sup_set_lemma3:
 12.1054 +     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
 12.1055 +          ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
 12.1056 +              \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
 12.1057 +apply (auto elim: Rep_preal [THEN prealE_lemma3b])
 12.1058 +done
 12.1059 +
 12.1060 +lemma preal_sup_set_lemma3_1:
 12.1061 +     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
 12.1062 +          ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
 12.1063 +              \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
 12.1064 +apply (auto elim: Rep_preal [THEN prealE_lemma3b])
 12.1065 +done
 12.1066 +
 12.1067 +lemma preal_sup_set_lemma4:
 12.1068 +     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
 12.1069 +          ==>  \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
 12.1070 +              Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
 12.1071 +apply (blast dest: Rep_preal [THEN prealE_lemma4a])
 12.1072 +done
 12.1073 +
 12.1074 +lemma preal_sup_set_lemma4_1:
 12.1075 +     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
 12.1076 +          ==>  \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
 12.1077 +              Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
 12.1078 +apply (blast dest: Rep_preal [THEN prealE_lemma4a])
 12.1079 +done
 12.1080 +
 12.1081 +lemma preal_sup:
 12.1082 +     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
 12.1083 +          ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)}: preal"
 12.1084 +apply (rule prealI2)
 12.1085 +apply (rule preal_sup_set_not_empty)
 12.1086 +apply (rule_tac [2] preal_sup_set_not_prat_set)
 12.1087 +apply (rule_tac [3] preal_sup_set_lemma3)
 12.1088 +apply (rule_tac [5] preal_sup_set_lemma4, auto)
 12.1089 +done
 12.1090 +
 12.1091 +lemma preal_sup1:
 12.1092 +     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
 12.1093 +          ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)}: preal"
 12.1094 +apply (rule prealI2)
 12.1095 +apply (rule preal_sup_set_not_empty)
 12.1096 +apply (rule_tac [2] preal_sup_set_not_prat_set1)
 12.1097 +apply (rule_tac [3] preal_sup_set_lemma3_1)
 12.1098 +apply (rule_tac [5] preal_sup_set_lemma4_1, auto)
 12.1099 +done
 12.1100 +
 12.1101 +lemma preal_psup_leI: "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> \<forall>x \<in> P. x \<le> psup P"
 12.1102 +apply (unfold psup_def)
 12.1103 +apply (auto simp add: preal_le_def)
 12.1104 +apply (rule preal_sup [THEN Abs_preal_inverse, THEN ssubst], auto)
 12.1105 +done
 12.1106 +
 12.1107 +lemma preal_psup_leI2: "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> \<forall>x \<in> P. x \<le> psup P"
 12.1108 +apply (unfold psup_def)
 12.1109 +apply (auto simp add: preal_le_def)
 12.1110 +apply (rule preal_sup1 [THEN Abs_preal_inverse, THEN ssubst])
 12.1111 +apply (auto simp add: preal_le_def)
 12.1112 +done
 12.1113 +
 12.1114 +lemma preal_psup_leI2b:
 12.1115 +     "[| \<exists>Y. (\<forall>X \<in> P. X < Y); x \<in> P |] ==> x \<le> psup P"
 12.1116 +apply (blast dest!: preal_psup_leI)
 12.1117 +done
 12.1118 +
 12.1119 +lemma preal_psup_leI2a:
 12.1120 +     "[| \<exists>Y. (\<forall>X \<in> P. X \<le> Y); x \<in> P |] ==> x \<le> psup P"
 12.1121 +apply (blast dest!: preal_psup_leI2)
 12.1122 +done
 12.1123 +
 12.1124 +lemma psup_le_ub: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X < Y |] ==> psup P \<le> Y"
 12.1125 +apply (unfold psup_def)
 12.1126 +apply (auto simp add: preal_le_def)
 12.1127 +apply (drule preal_sup [OF exI exI, THEN Abs_preal_inverse, THEN subst])
 12.1128 +apply (rotate_tac [2] 1)
 12.1129 +prefer 2 apply assumption
 12.1130 +apply (auto dest!: bspec simp add: preal_less_def psubset_def)
 12.1131 +done
 12.1132 +
 12.1133 +lemma psup_le_ub1: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
 12.1134 +apply (unfold psup_def)
 12.1135 +apply (auto simp add: preal_le_def)
 12.1136 +apply (drule preal_sup1 [OF exI exI, THEN Abs_preal_inverse, THEN subst])
 12.1137 +apply (rotate_tac [2] 1)
 12.1138 +prefer 2 apply assumption
 12.1139 +apply (auto dest!: bspec simp add: preal_less_def psubset_def preal_le_def)
 12.1140 +done
 12.1141 +
 12.1142 +text{*Supremum property*}
 12.1143 +lemma preal_complete:
 12.1144 +     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
 12.1145 +          ==> (\<forall>Y. (\<exists>X \<in> P. Y < X) = (Y < psup P))"
 12.1146 +apply (frule preal_sup [THEN Abs_preal_inverse], fast)
 12.1147 +apply (auto simp add: psup_def preal_less_def)
 12.1148 +apply (cut_tac x = Xa and y = Ya in preal_linear)
 12.1149 +apply (auto dest: psubsetD simp add: preal_less_def)
 12.1150 +done
 12.1151 +
 12.1152 +
 12.1153 +subsection{*The Embadding from @{typ prat} into @{typ preal}*}
 12.1154 +
 12.1155 +lemma lemma_preal_rat_less: "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1"
 12.1156 +apply (drule_tac x = "z1 * qinv (z1 + z2) " in prat_mult_less2_mono1)
 12.1157 +apply (simp add: prat_mult_ac)
 12.1158 +done
 12.1159 +
 12.1160 +lemma lemma_preal_rat_less2: "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2"
 12.1161 +apply (subst prat_add_commute)
 12.1162 +apply (drule prat_add_commute [THEN subst])
 12.1163 +apply (erule lemma_preal_rat_less)
 12.1164 +done
 12.1165 +
 12.1166 +lemma preal_of_prat_add:
 12.1167 +      "preal_of_prat ((z1::prat) + z2) =
 12.1168 +       preal_of_prat z1 + preal_of_prat z2"
 12.1169 +apply (unfold preal_of_prat_def preal_add_def)
 12.1170 +apply (rule_tac f = Abs_preal in arg_cong)
 12.1171 +apply (auto intro: prat_add_less_mono 
 12.1172 +            simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse])
 12.1173 +apply (rule_tac x = "x*z1*qinv (z1+z2) " in exI, rule conjI)
 12.1174 +apply (erule lemma_preal_rat_less)
 12.1175 +apply (rule_tac x = "x*z2*qinv (z1+z2) " in exI, rule conjI)
 12.1176 +apply (erule lemma_preal_rat_less2)
 12.1177 +apply (simp add: prat_add_mult_distrib [symmetric] 
 12.1178 +                 prat_add_mult_distrib2 [symmetric] prat_mult_ac)
 12.1179 +done
 12.1180 +
 12.1181 +lemma lemma_preal_rat_less3: "x < xa ==> x*z1*qinv(xa) < z1"
 12.1182 +apply (drule_tac x = "z1 * qinv xa" in prat_mult_less2_mono1)
 12.1183 +apply (drule prat_mult_left_commute [THEN subst])
 12.1184 +apply (simp add: prat_mult_ac)
 12.1185 +done
 12.1186 +
 12.1187 +lemma lemma_preal_rat_less4: "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2"
 12.1188 +apply (drule_tac x = "z2 * qinv (z1*z2) " in prat_mult_less2_mono1)
 12.1189 +apply (drule prat_mult_left_commute [THEN subst])
 12.1190 +apply (simp add: prat_mult_ac)
 12.1191 +done
 12.1192 +
 12.1193 +lemma preal_of_prat_mult:
 12.1194 +      "preal_of_prat ((z1::prat) * z2) =
 12.1195 +       preal_of_prat z1 * preal_of_prat z2"
 12.1196 +apply (unfold preal_of_prat_def preal_mult_def)
 12.1197 +apply (rule_tac f = Abs_preal in arg_cong)
 12.1198 +apply (auto intro: prat_mult_less_mono 
 12.1199 +            simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse])
 12.1200 +apply (drule prat_dense, safe)
 12.1201 +apply (rule_tac x = "x*z1*qinv (xa) " in exI, rule conjI)
 12.1202 +apply (erule lemma_preal_rat_less3)
 12.1203 +apply (rule_tac x = " xa*z2*qinv (z1*z2) " in exI, rule conjI)
 12.1204 +apply (erule lemma_preal_rat_less4)
 12.1205 +apply (simp add: qinv_mult_eq [symmetric] prat_mult_ac)
 12.1206 +apply (simp add: prat_mult_assoc [symmetric])
 12.1207 +done
 12.1208 +
 12.1209 +lemma preal_of_prat_less_iff [simp]:
 12.1210 +      "(preal_of_prat p < preal_of_prat q) = (p < q)"
 12.1211 +apply (unfold preal_of_prat_def preal_less_def)
 12.1212 +apply (auto dest!: lemma_prat_set_eq elim: prat_less_trans 
 12.1213 +        simp add: lemma_prat_less_set_mem_preal psubset_def prat_less_not_refl)
 12.1214 +apply (rule_tac x = p and y = q in prat_linear_less2)
 12.1215 +apply (auto intro: prat_less_irrefl)
 12.1216 +done
 12.1217 +
 12.1218 +
 12.1219 +ML
 12.1220 +{*
 12.1221 +val inj_on_Abs_preal = thm"inj_on_Abs_preal";
 12.1222 +val inj_Rep_preal = thm"inj_Rep_preal";
 12.1223 +val empty_not_mem_preal = thm"empty_not_mem_preal";
 12.1224 +val one_set_mem_preal = thm"one_set_mem_preal";
 12.1225 +val preal_psubset_empty = thm"preal_psubset_empty";
 12.1226 +val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex";
 12.1227 +val inj_preal_of_prat = thm"inj_preal_of_prat";
 12.1228 +val not_in_preal_ub = thm"not_in_preal_ub";
 12.1229 +val preal_less_not_refl = thm"preal_less_not_refl";
 12.1230 +val preal_less_trans = thm"preal_less_trans";
 12.1231 +val preal_less_not_sym = thm"preal_less_not_sym";
 12.1232 +val preal_linear = thm"preal_linear";
 12.1233 +val preal_add_commute = thm"preal_add_commute";
 12.1234 +val preal_add_set_not_empty = thm"preal_add_set_not_empty";
 12.1235 +val preal_not_mem_add_set_Ex = thm"preal_not_mem_add_set_Ex";
 12.1236 +val preal_add_set_not_prat_set = thm"preal_add_set_not_prat_set";
 12.1237 +val preal_mem_add_set = thm"preal_mem_add_set";
 12.1238 +val preal_add_assoc = thm"preal_add_assoc";
 12.1239 +val preal_add_left_commute = thm"preal_add_left_commute";
 12.1240 +val preal_mult_commute = thm"preal_mult_commute";
 12.1241 +val preal_mult_set_not_empty = thm"preal_mult_set_not_empty";
 12.1242 +val preal_not_mem_mult_set_Ex = thm"preal_not_mem_mult_set_Ex";
 12.1243 +val preal_mult_set_not_prat_set = thm"preal_mult_set_not_prat_set";
 12.1244 +val preal_mem_mult_set = thm"preal_mem_mult_set";
 12.1245 +val preal_mult_assoc = thm"preal_mult_assoc";
 12.1246 +val preal_mult_left_commute = thm"preal_mult_left_commute";
 12.1247 +val preal_mult_1 = thm"preal_mult_1";
 12.1248 +val preal_mult_1_right = thm"preal_mult_1_right";
 12.1249 +val mem_Rep_preal_addD = thm"mem_Rep_preal_addD";
 12.1250 +val mem_Rep_preal_addI = thm"mem_Rep_preal_addI";
 12.1251 +val mem_Rep_preal_add_iff = thm"mem_Rep_preal_add_iff";
 12.1252 +val mem_Rep_preal_multD = thm"mem_Rep_preal_multD";
 12.1253 +val mem_Rep_preal_multI = thm"mem_Rep_preal_multI";
 12.1254 +val mem_Rep_preal_mult_iff = thm"mem_Rep_preal_mult_iff";
 12.1255 +val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2";
 12.1256 +val preal_add_mult_distrib = thm"preal_add_mult_distrib";
 12.1257 +val qinv_not_mem_Rep_preal_Ex = thm"qinv_not_mem_Rep_preal_Ex";
 12.1258 +val preal_inv_set_not_empty = thm"preal_inv_set_not_empty";
 12.1259 +val qinv_mem_Rep_preal_Ex = thm"qinv_mem_Rep_preal_Ex";
 12.1260 +val preal_not_mem_inv_set_Ex = thm"preal_not_mem_inv_set_Ex";
 12.1261 +val preal_inv_set_not_prat_set = thm"preal_inv_set_not_prat_set";
 12.1262 +val preal_mem_inv_set = thm"preal_mem_inv_set";
 12.1263 +val preal_mem_mult_invD = thm"preal_mem_mult_invD";
 12.1264 +val preal_mem_mult_invI = thm"preal_mem_mult_invI";
 12.1265 +val preal_mult_inv = thm"preal_mult_inv";
 12.1266 +val preal_mult_inv_right = thm"preal_mult_inv_right";
 12.1267 +val Rep_preal_self_subset = thm"Rep_preal_self_subset";
 12.1268 +val Rep_preal_sum_not_subset = thm"Rep_preal_sum_not_subset";
 12.1269 +val Rep_preal_sum_not_eq = thm"Rep_preal_sum_not_eq";
 12.1270 +val preal_self_less_add_left = thm"preal_self_less_add_left";
 12.1271 +val preal_self_less_add_right = thm"preal_self_less_add_right";
 12.1272 +val preal_less_le_iff = thm"preal_less_le_iff";
 12.1273 +val preal_le_refl = thm"preal_le_refl";
 12.1274 +val preal_le_trans = thm"preal_le_trans";
 12.1275 +val preal_le_anti_sym = thm"preal_le_anti_sym";
 12.1276 +val preal_neq_iff = thm"preal_neq_iff";
 12.1277 +val preal_less_le = thm"preal_less_le";
 12.1278 +val psubset_trans = thm"psubset_trans";
 12.1279 +val preal_less_set_not_empty = thm"preal_less_set_not_empty";
 12.1280 +val preal_less_set_not_prat_set = thm"preal_less_set_not_prat_set";
 12.1281 +val preal_mem_less_set = thm"preal_mem_less_set";
 12.1282 +val preal_less_add_left_subsetI = thm"preal_less_add_left_subsetI";
 12.1283 +val preal_less_add_left_subsetI2 = thm"preal_less_add_left_subsetI2";
 12.1284 +val preal_less_add_left = thm"preal_less_add_left";
 12.1285 +val preal_less_add_left_Ex = thm"preal_less_add_left_Ex";
 12.1286 +val preal_add_less2_mono1 = thm"preal_add_less2_mono1";
 12.1287 +val preal_add_less2_mono2 = thm"preal_add_less2_mono2";
 12.1288 +val preal_mult_less_mono1 = thm"preal_mult_less_mono1";
 12.1289 +val preal_mult_left_less_mono1 = thm"preal_mult_left_less_mono1";
 12.1290 +val preal_mult_left_le_mono1 = thm"preal_mult_left_le_mono1";
 12.1291 +val preal_mult_le_mono1 = thm"preal_mult_le_mono1";
 12.1292 +val preal_add_left_le_mono1 = thm"preal_add_left_le_mono1";
 12.1293 +val preal_add_le_mono1 = thm"preal_add_le_mono1";
 12.1294 +val preal_add_right_less_cancel = thm"preal_add_right_less_cancel";
 12.1295 +val preal_add_left_less_cancel = thm"preal_add_left_less_cancel";
 12.1296 +val preal_add_less_iff1 = thm"preal_add_less_iff1";
 12.1297 +val preal_add_less_iff2 = thm"preal_add_less_iff2";
 12.1298 +val preal_add_less_mono = thm"preal_add_less_mono";
 12.1299 +val preal_mult_less_mono = thm"preal_mult_less_mono";
 12.1300 +val preal_add_right_cancel = thm"preal_add_right_cancel";
 12.1301 +val preal_add_left_cancel = thm"preal_add_left_cancel";
 12.1302 +val preal_add_left_cancel_iff = thm"preal_add_left_cancel_iff";
 12.1303 +val preal_add_right_cancel_iff = thm"preal_add_right_cancel_iff";
 12.1304 +val preal_sup_mem_Ex = thm"preal_sup_mem_Ex";
 12.1305 +val preal_sup_set_not_empty = thm"preal_sup_set_not_empty";
 12.1306 +val preal_sup_not_mem_Ex = thm"preal_sup_not_mem_Ex";
 12.1307 +val preal_sup_not_mem_Ex1 = thm"preal_sup_not_mem_Ex1";
 12.1308 +val preal_sup_set_not_prat_set = thm"preal_sup_set_not_prat_set";
 12.1309 +val preal_sup_set_not_prat_set1 = thm"preal_sup_set_not_prat_set1";
 12.1310 +val preal_sup = thm"preal_sup";
 12.1311 +val preal_sup1 = thm"preal_sup1";
 12.1312 +val preal_psup_leI = thm"preal_psup_leI";
 12.1313 +val preal_psup_leI2 = thm"preal_psup_leI2";
 12.1314 +val preal_psup_leI2b = thm"preal_psup_leI2b";
 12.1315 +val preal_psup_leI2a = thm"preal_psup_leI2a";
 12.1316 +val psup_le_ub = thm"psup_le_ub";
 12.1317 +val psup_le_ub1 = thm"psup_le_ub1";
 12.1318 +val preal_complete = thm"preal_complete";
 12.1319 +val preal_of_prat_add = thm"preal_of_prat_add";
 12.1320 +val preal_of_prat_mult = thm"preal_of_prat_mult";
 12.1321 +
 12.1322 +val preal_add_ac = thms"preal_add_ac";
 12.1323 +val preal_mult_ac = thms"preal_mult_ac";
 12.1324 +*}
 12.1325 +
 12.1326  end
 12.1327 -
    13.1 --- a/src/HOL/Real/RealDef.thy	Thu Jan 01 10:06:32 2004 +0100
    13.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jan 01 21:47:07 2004 +0100
    13.3 @@ -7,26 +7,6 @@
    13.4  
    13.5  theory RealDef = PReal:
    13.6  
    13.7 -(*MOVE TO THEORY PREAL*)
    13.8 -instance preal :: order
    13.9 -proof qed
   13.10 - (assumption |
   13.11 -  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
   13.12 -
   13.13 -instance preal :: order
   13.14 -  by (intro_classes,
   13.15 -      (assumption | 
   13.16 -       rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+)
   13.17 -
   13.18 -lemma preal_le_linear: "x <= y | y <= (x::preal)"
   13.19 -apply (insert preal_linear [of x y]) 
   13.20 -apply (auto simp add: order_less_le) 
   13.21 -done
   13.22 -
   13.23 -instance preal :: linorder
   13.24 -  by (intro_classes, rule preal_le_linear)
   13.25 -
   13.26 -
   13.27  constdefs
   13.28    realrel   ::  "((preal * preal) * (preal * preal)) set"
   13.29    "realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
   13.30 @@ -781,8 +761,8 @@
   13.31  
   13.32  lemma real_of_preal_le_iff:
   13.33       "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
   13.34 -apply (auto intro!: preal_leI simp add: linorder_not_less [symmetric])
   13.35 -done
   13.36 +by (auto intro!: preal_le_iff_less_or_eq [THEN iffD1]  
   13.37 +          simp add: linorder_not_less [symmetric])
   13.38  
   13.39  
   13.40  subsection{*Monotonicity of Addition*}
   13.41 @@ -797,11 +777,15 @@
   13.42  lemma real_less_add_positive_left_Ex: "R < S ==> \<exists>T::real. 0 < T & R + T = S"
   13.43  apply (rule_tac x = R in real_of_preal_trichotomyE)
   13.44  apply (rule_tac [!] x = S in real_of_preal_trichotomyE)
   13.45 -apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero real_of_preal_minus_less_rev_iff)
   13.46 +apply (auto dest!: preal_less_add_left_Ex 
   13.47 +        simp add: real_of_preal_not_minus_gt_all real_of_preal_add
   13.48 +                real_of_preal_not_less_zero real_less_not_refl 
   13.49 +             real_of_preal_not_minus_gt_zero real_of_preal_minus_less_rev_iff)
   13.50  apply (rule real_of_preal_zero_less) 
   13.51  apply (rule_tac [1] x = "real_of_preal m+real_of_preal ma" in exI)
   13.52  apply (rule_tac [2] x = "real_of_preal D" in exI)
   13.53 -apply (auto simp add: real_of_preal_minus_less_rev_iff real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc)
   13.54 +apply (auto simp add: real_of_preal_minus_less_rev_iff real_of_preal_zero_less
   13.55 +                 real_of_preal_sum_zero_less real_add_assoc)
   13.56  apply (simp add: real_add_assoc [symmetric])
   13.57  done
   13.58  
    14.1 --- a/src/HOL/Set.thy	Thu Jan 01 10:06:32 2004 +0100
    14.2 +++ b/src/HOL/Set.thy	Thu Jan 01 21:47:07 2004 +0100
    14.3 @@ -868,6 +868,16 @@
    14.4  lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
    14.5    by (simp add: psubset_eq)
    14.6  
    14.7 +lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
    14.8 +apply (unfold psubset_def)
    14.9 +apply (auto dest: subset_antisym)
   14.10 +done
   14.11 +
   14.12 +lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
   14.13 +apply (unfold psubset_def)
   14.14 +apply (auto dest: subsetD)
   14.15 +done
   14.16 +
   14.17  lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
   14.18    by (auto simp add: psubset_eq)
   14.19