src/HOL/Real/PReal.ML
author paulson
Thu Oct 01 18:18:01 1998 +0200 (1998-10-01)
changeset 5588 a3ab526bb891
parent 5521 7970832271cc
child 7077 60b098bb8b8a
permissions -rw-r--r--
Revised version with Abelian group simprocs
     1 (*  Title       : PReal.ML
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Description : The positive reals as Dedekind sections of positive
     5                   rationals. Fundamentals of Abstract Analysis 
     6                   [Gleason- p. 121] provides some of the definitions.
     7 *)
     8 
     9 claset_ref() := claset() delWrapper "bspec";
    10 
    11 open PReal;
    12 
    13 Goal "inj_on Abs_preal preal";
    14 by (rtac inj_on_inverseI 1);
    15 by (etac Abs_preal_inverse 1);
    16 qed "inj_on_Abs_preal";
    17 
    18 Addsimps [inj_on_Abs_preal RS inj_on_iff];
    19 
    20 Goal "inj(Rep_preal)";
    21 by (rtac inj_inverseI 1);
    22 by (rtac Rep_preal_inverse 1);
    23 qed "inj_Rep_preal";
    24 
    25 Goalw [preal_def] "{} ~: preal";
    26 by (Fast_tac 1);
    27 qed "empty_not_mem_preal";
    28 
    29 (* {} : preal ==> P *)
    30 bind_thm ("empty_not_mem_prealE", empty_not_mem_preal RS notE);
    31 
    32 Addsimps [empty_not_mem_preal];
    33 
    34 Goalw [preal_def] "{x::prat. x < $#Abs_pnat 1} : preal";
    35 by (rtac preal_1 1);
    36 qed "one_set_mem_preal";
    37 
    38 Addsimps [one_set_mem_preal];
    39 
    40 Goalw [preal_def] "x : preal ==> {} < x";
    41 by (Fast_tac 1);
    42 qed "preal_psubset_empty";
    43 
    44 Goal "{} < Rep_preal x";
    45 by (rtac (Rep_preal RS preal_psubset_empty) 1);
    46 qed "Rep_preal_psubset_empty";
    47 
    48 Goal "? x. x: Rep_preal X";
    49 by (cut_inst_tac [("x","X")]  Rep_preal_psubset_empty 1);
    50 by (auto_tac (claset() addIs [(equals0I RS sym)],
    51               simpset() addsimps [psubset_def]));
    52 qed "mem_Rep_preal_Ex";
    53 
    54 Goalw [preal_def] 
    55       "[| {} < A; A < {q::prat. True}; \
    56 \              (!y: A. ((!z. z < y --> z: A) & \
    57 \                        (? u: A. y < u))) |] ==> A : preal";
    58 by (Fast_tac 1);
    59 qed "prealI1";
    60     
    61 Goalw [preal_def] 
    62       "[| {} < A; A < {q::prat. True}; \
    63 \              !y: A. (!z. z < y --> z: A); \
    64 \              !y: A. (? u: A. y < u) |] ==> A : preal";
    65 by (Best_tac 1);
    66 qed "prealI2";
    67 
    68 Goalw [preal_def] 
    69       "A : preal ==> {} < A & A < {q::prat. True} & \
    70 \                         (!y: A. ((!z. z < y --> z: A) & \
    71 \                                  (? u: A. y < u)))";
    72 by (Fast_tac 1);
    73 qed "prealE_lemma";
    74 
    75 
    76 AddSIs [prealI1,prealI2];
    77 
    78 Addsimps [Abs_preal_inverse];
    79 
    80 
    81 Goalw [preal_def] "A : preal ==> {} < A";
    82 by (Fast_tac 1);
    83 qed "prealE_lemma1";
    84 
    85 Goalw [preal_def] "A : preal ==> A < {q::prat. True}";
    86 by (Fast_tac 1);
    87 qed "prealE_lemma2";
    88 
    89 Goalw [preal_def] "A : preal ==> !y: A. (!z. z < y --> z: A)";
    90 by (Fast_tac 1);
    91 qed "prealE_lemma3";
    92 
    93 Goal "[| A : preal; y: A |] ==> (!z. z < y --> z: A)";
    94 by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
    95 qed "prealE_lemma3a";
    96 
    97 Goal "[| A : preal; y: A; z < y |] ==> z: A";
    98 by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
    99 qed "prealE_lemma3b";
   100 
   101 Goalw [preal_def] "A : preal ==> !y: A. (? u: A. y < u)";
   102 by (Fast_tac 1);
   103 qed "prealE_lemma4";
   104 
   105 Goal "[| A : preal; y: A |] ==> ? u: A. y < u";
   106 by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
   107 qed "prealE_lemma4a";
   108 
   109 Goal "? x. x~: Rep_preal X";
   110 by (cut_inst_tac [("x","X")] Rep_preal 1);
   111 by (dtac prealE_lemma2 1);
   112 by (rtac ccontr 1);
   113 by (auto_tac (claset(),simpset() addsimps [psubset_def]));
   114 by (blast_tac (claset() addIs [set_ext] addEs [swap]) 1);
   115 qed "not_mem_Rep_preal_Ex";
   116 
   117 (** prat_pnat: the injection from prat to preal **)
   118 (** A few lemmas **)
   119 Goal "{} < {xa::prat. xa < y}";
   120 by (cut_facts_tac [qless_Ex] 1);
   121 by (auto_tac (claset() addEs [equalityCE],
   122               simpset() addsimps [psubset_def]));
   123 qed "lemma_prat_less_set_Ex";
   124 
   125 Goal "{xa::prat. xa < y} : preal";
   126 by (cut_facts_tac [qless_Ex] 1);
   127 by Safe_tac;
   128 by (rtac lemma_prat_less_set_Ex 1);
   129 by (auto_tac (claset() addIs [prat_less_trans],
   130     simpset() addsimps [psubset_def]));
   131 by (eres_inst_tac [("c","y")] equalityCE 1);
   132 by (auto_tac (claset() addDs [prat_less_irrefl],simpset()));
   133 by (dres_inst_tac [("q1.0","ya")] prat_dense 1);
   134 by (Fast_tac 1);
   135 qed "lemma_prat_less_set_mem_preal";
   136 
   137 Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y";
   138 by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
   139 by Auto_tac;
   140 by (dtac prat_dense 1 THEN etac exE 1);
   141 by (eres_inst_tac [("c","xa")] equalityCE 1);
   142 by (auto_tac (claset() addDs [prat_less_not_sym],simpset()));
   143 by (dtac prat_dense 1 THEN etac exE 1);
   144 by (eres_inst_tac [("c","xa")] equalityCE 1);
   145 by (auto_tac (claset() addDs [prat_less_not_sym],simpset()));
   146 qed "lemma_prat_set_eq";
   147 
   148 Goal "inj(preal_prat)";
   149 by (rtac injI 1);
   150 by (rewtac preal_prat_def);
   151 by (dtac (inj_on_Abs_preal RS inj_onD) 1);
   152 by (rtac lemma_prat_less_set_mem_preal 1);
   153 by (rtac lemma_prat_less_set_mem_preal 1);
   154 by (etac lemma_prat_set_eq 1);
   155 qed "inj_preal_prat";
   156 
   157       (*** theorems for ordering ***)
   158 (* prove introduction and elimination rules for preal_less *)
   159 
   160 (* A positive fraction not in a positive real is an upper bound *)
   161 (* Gleason p. 122 - Remark (1)                                  *)
   162 
   163 Goal "x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
   164 by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
   165 by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
   166 qed "not_in_preal_ub";
   167 
   168 (* preal_less is a strong order i.e nonreflexive and transitive *)
   169 
   170 Goalw [preal_less_def] "~ (x::preal) < x";
   171 by (simp_tac (simpset() addsimps [psubset_def]) 1);
   172 qed "preal_less_not_refl";
   173 
   174 (*** y < y ==> P ***)
   175 bind_thm("preal_less_irrefl",preal_less_not_refl RS notE);
   176 
   177 Goal "!!(x::preal). x < y ==> x ~= y";
   178 by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
   179 qed "preal_not_refl2";
   180 
   181 Goalw  [preal_less_def] "!!(x::preal). [| x < y; y < z |] ==> x < z";
   182 by (auto_tac (claset() addDs [subsetD,equalityI],
   183               simpset() addsimps [psubset_def]));
   184 qed "preal_less_trans";
   185 
   186 Goal "!! (q1::preal). q1 < q2 ==> ~ q2 < q1";
   187 by (rtac notI 1);
   188 by (dtac preal_less_trans 1 THEN assume_tac 1);
   189 by (asm_full_simp_tac (simpset() addsimps [preal_less_not_refl]) 1);
   190 qed "preal_less_not_sym";
   191 
   192 (* [| x < y;  ~P ==> y < x |] ==> P *)
   193 bind_thm ("preal_less_asym", preal_less_not_sym RS swap);
   194 
   195 Goalw [preal_less_def] 
   196       "(r1::preal) < r2 | r1 = r2 | r2 < r1";
   197 by (auto_tac (claset() addSDs [inj_Rep_preal RS injD],
   198               simpset() addsimps [psubset_def]));
   199 by (rtac prealE_lemma3b 1 THEN rtac Rep_preal 1);
   200 by (assume_tac 1);
   201 by (fast_tac (claset() addDs [not_in_preal_ub]) 1);
   202 qed "preal_linear";
   203 
   204 Goal "!!(r1::preal). [| r1 < r2 ==> P;  r1 = r2 ==> P; \
   205 \                       r2 < r1 ==> P |] ==> P";
   206 by (cut_inst_tac [("r1.0","r1"),("r2.0","r2")] preal_linear 1);
   207 by Auto_tac;
   208 qed "preal_linear_less2";
   209 
   210   (*** Properties of addition ***)
   211 
   212 Goalw [preal_add_def] "(x::preal) + y = y + x";
   213 by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   214 by (rtac set_ext 1);
   215 by (blast_tac (claset() addIs [prat_add_commute RS subst]) 1);
   216 qed "preal_add_commute";
   217 
   218 (** addition of two positive reals gives a positive real **)
   219 (** lemmas for proving positive reals addition set in preal **)
   220 
   221 (** Part 1 of Dedekind sections def **)
   222 Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
   223 by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
   224 by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   225 qed "preal_add_set_not_empty";
   226 
   227 (** Part 2 of Dedekind sections def **)
   228 Goal "? q. q  ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
   229 by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
   230 by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
   231 by (REPEAT(etac exE 1));
   232 by (REPEAT(dtac not_in_preal_ub 1));
   233 by (res_inst_tac [("x","x+xa")] exI 1);
   234 by (Auto_tac THEN (REPEAT(etac ballE 1)) THEN Auto_tac);
   235 by (dtac prat_add_less_mono 1);
   236 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   237 qed "preal_not_mem_add_set_Ex";
   238 
   239 Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < {q. True}";
   240 by (auto_tac (claset() addSIs [psubsetI],simpset()));
   241 by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
   242 by (etac exE 1);
   243 by (eres_inst_tac [("c","q")] equalityCE 1);
   244 by Auto_tac;
   245 qed "preal_add_set_not_prat_set";
   246 
   247 (** Part 3 of Dedekind sections def **)
   248 Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
   249 \         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
   250 by Auto_tac;
   251 by (forward_tac [prat_mult_qinv_less_1] 1);
   252 by (forw_inst_tac [("x","x"),("q2.0","$#Abs_pnat 1")] 
   253     prat_mult_less2_mono1 1);
   254 by (forw_inst_tac [("x","ya"),("q2.0","$#Abs_pnat 1")] 
   255     prat_mult_less2_mono1 1);
   256 by (Asm_full_simp_tac 1);
   257 by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
   258 by (REPEAT(etac allE 1));
   259 by Auto_tac;
   260 by (REPEAT(rtac bexI 1));
   261 by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2 
   262      RS sym,prat_add_assoc RS sym,prat_mult_assoc]));
   263 qed "preal_add_set_lemma3";
   264 
   265 Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
   266 \         ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. y < u";
   267 by Auto_tac;
   268 by (dtac (Rep_preal RS prealE_lemma4a) 1);
   269 by (auto_tac (claset() addIs [prat_add_less2_mono1],simpset()));
   270 qed "preal_add_set_lemma4";
   271 
   272 Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y} : preal";
   273 by (rtac prealI2 1);
   274 by (rtac preal_add_set_not_empty 1);
   275 by (rtac preal_add_set_not_prat_set 1);
   276 by (rtac preal_add_set_lemma3 1);
   277 by (rtac preal_add_set_lemma4 1);
   278 qed "preal_mem_add_set";
   279 
   280 Goalw [preal_add_def] "((x::preal) + y) + z = x + (y + z)";
   281 by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   282 by (rtac set_ext 1);
   283 by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
   284 by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
   285 by (auto_tac (claset(),simpset() addsimps prat_add_ac));
   286 by (rtac bexI 1);
   287 by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_add_ac));
   288 qed "preal_add_assoc";
   289 
   290 qed_goal "preal_add_left_commute" thy
   291     "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)"
   292  (fn _ => [rtac (preal_add_commute RS trans) 1, rtac (preal_add_assoc RS trans) 1,
   293            rtac (preal_add_commute RS arg_cong) 1]);
   294 
   295 (* Positive Reals addition is an AC operator *)
   296 val preal_add_ac = [preal_add_assoc, preal_add_commute, preal_add_left_commute];
   297 
   298   (*** Properties of multiplication ***)
   299 
   300 (** Proofs essentially same as for addition **)
   301 
   302 Goalw [preal_mult_def] "(x::preal) * y = y * x";
   303 by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   304 by (rtac set_ext 1);
   305 by (blast_tac (claset() addIs [prat_mult_commute RS subst]) 1);
   306 qed "preal_mult_commute";
   307 
   308 (** multiplication of two positive reals gives a positive real **)
   309 (** lemmas for proving positive reals multiplication set in preal **)
   310 
   311 (** Part 1 of Dedekind sections def **)
   312 Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
   313 by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
   314 by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   315 qed "preal_mult_set_not_empty";
   316 
   317 (** Part 2 of Dedekind sections def **)
   318 Goal "? q. q  ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
   319 by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
   320 by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
   321 by (REPEAT(etac exE 1));
   322 by (REPEAT(dtac not_in_preal_ub 1));
   323 by (res_inst_tac [("x","x*xa")] exI 1);
   324 by (Auto_tac  THEN (REPEAT(etac ballE 1)) THEN Auto_tac );
   325 by (dtac prat_mult_less_mono 1);
   326 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   327 qed "preal_not_mem_mult_set_Ex";
   328 
   329 Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < {q. True}";
   330 by (auto_tac (claset() addSIs [psubsetI],simpset()));
   331 by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
   332 by (etac exE 1);
   333 by (eres_inst_tac [("c","q")] equalityCE 1);
   334 by Auto_tac;
   335 qed "preal_mult_set_not_prat_set";
   336 
   337 (** Part 3 of Dedekind sections def **)
   338 Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
   339 \         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x * y}";
   340 by Auto_tac;
   341 by (forw_inst_tac [("x","qinv(ya)"),("q1.0","z")] 
   342     prat_mult_left_less2_mono1 1);
   343 by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
   344 by (dtac (Rep_preal RS prealE_lemma3a) 1);
   345 by (etac allE 1);
   346 by (REPEAT(rtac bexI 1));
   347 by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
   348 qed "preal_mult_set_lemma3";
   349 
   350 Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
   351 \         ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. y < u";
   352 by Auto_tac;
   353 by (dtac (Rep_preal RS prealE_lemma4a) 1);
   354 by (auto_tac (claset() addIs [prat_mult_less2_mono1],simpset()));
   355 qed "preal_mult_set_lemma4";
   356 
   357 Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y} : preal";
   358 by (rtac prealI2 1);
   359 by (rtac preal_mult_set_not_empty 1);
   360 by (rtac preal_mult_set_not_prat_set 1);
   361 by (rtac preal_mult_set_lemma3 1);
   362 by (rtac preal_mult_set_lemma4 1);
   363 qed "preal_mem_mult_set";
   364 
   365 Goalw [preal_mult_def] "((x::preal) * y) * z = x * (y * z)";
   366 by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   367 by (rtac set_ext 1);
   368 by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
   369 by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
   370 by (auto_tac (claset(),simpset() addsimps prat_mult_ac));
   371 by (rtac bexI 1);
   372 by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_mult_ac));
   373 qed "preal_mult_assoc";
   374 
   375 qed_goal "preal_mult_left_commute" thy
   376     "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)"
   377  (fn _ => [rtac (preal_mult_commute RS trans) 1, 
   378            rtac (preal_mult_assoc RS trans) 1,
   379            rtac (preal_mult_commute RS arg_cong) 1]);
   380 
   381 (* Positive Reals multiplication is an AC operator *)
   382 val preal_mult_ac = [preal_mult_assoc, 
   383                      preal_mult_commute, 
   384                      preal_mult_left_commute];
   385 
   386 (* Positive Real 1 is the multiplicative identity element *) 
   387 (* long *)
   388 Goalw [preal_prat_def,preal_mult_def] "(@#($#Abs_pnat 1)) * z = z";
   389 by (rtac (Rep_preal_inverse RS subst) 1);
   390 by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
   391 by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
   392 by (rtac set_ext 1);
   393 by (auto_tac(claset(),simpset() addsimps [Rep_preal_inverse]));
   394 by (EVERY1[dtac (Rep_preal RS prealE_lemma4a),etac bexE]);
   395 by (dtac prat_mult_less_mono 1);
   396 by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3a],simpset()));
   397 by (EVERY1[forward_tac [Rep_preal RS prealE_lemma4a],etac bexE]);
   398 by (forw_inst_tac [("x","qinv(u)"),("q1.0","x")] 
   399     prat_mult_less2_mono1 1);
   400 by (rtac exI 1 THEN Auto_tac THEN res_inst_tac [("x","u")] bexI 1);
   401 by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
   402 qed "preal_mult_1";
   403 
   404 Goal "z * (@#($#Abs_pnat 1)) = z";
   405 by (rtac (preal_mult_commute RS subst) 1);
   406 by (rtac preal_mult_1 1);
   407 qed "preal_mult_1_right";
   408 
   409 (** Lemmas **)
   410 
   411 qed_goal "preal_add_assoc_cong" thy
   412     "!!z. (z::preal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   413  (fn _ => [(asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1)]);
   414 
   415 qed_goal "preal_add_assoc_swap" thy "(z::preal) + (v + w) = v + (z + w)"
   416  (fn _ => [(REPEAT (ares_tac [preal_add_commute RS preal_add_assoc_cong] 1))]);
   417 
   418 (** Distribution of multiplication across addition **)
   419 (** lemmas for the proof **)
   420 
   421  (** lemmas **)
   422 Goalw [preal_add_def] 
   423       "z: Rep_preal(R+S) ==> \
   424 \           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y";
   425 by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
   426 by (Fast_tac 1);
   427 qed "mem_Rep_preal_addD";
   428 
   429 Goalw [preal_add_def] 
   430       "? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
   431 \      ==> z: Rep_preal(R+S)";
   432 by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
   433 by (Fast_tac 1);
   434 qed "mem_Rep_preal_addI";
   435 
   436 Goal " z: Rep_preal(R+S) = (? x: Rep_preal(R). \
   437 \                                 ? y: Rep_preal(S). z = x + y)";
   438 by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
   439 qed "mem_Rep_preal_add_iff";
   440 
   441 Goalw [preal_mult_def] 
   442       "z: Rep_preal(R*S) ==> \
   443 \           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y";
   444 by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
   445 by (Fast_tac 1);
   446 qed "mem_Rep_preal_multD";
   447 
   448 Goalw [preal_mult_def] 
   449       "? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
   450 \      ==> z: Rep_preal(R*S)";
   451 by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
   452 by (Fast_tac 1);
   453 qed "mem_Rep_preal_multI";
   454 
   455 Goal " z: Rep_preal(R*S) = (? x: Rep_preal(R). \
   456 \                                 ? y: Rep_preal(S). z = x * y)";
   457 by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
   458 qed "mem_Rep_preal_mult_iff";
   459 
   460 (** More lemmas for preal_add_mult_distrib2 **)
   461 goal PRat.thy "!!(a1::prat). a1 < a2 ==> a1 * b + a2 * c < a2 * (b + c)";
   462 by (auto_tac (claset() addSIs [prat_add_less2_mono1,prat_mult_less2_mono1],
   463               simpset() addsimps [prat_add_mult_distrib2]));
   464 qed "lemma_prat_add_mult_mono";
   465 
   466 Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
   467 \                  Rep_preal w; yb: Rep_preal w |] ==> \
   468 \                  xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
   469 by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
   470 qed "lemma_add_mult_mem_Rep_preal";
   471 
   472 Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
   473 \                  Rep_preal w; yb: Rep_preal w |] ==> \
   474 \                  yb*(xb + xc): Rep_preal (w*(z1 + z2))";
   475 by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
   476 qed "lemma_add_mult_mem_Rep_preal1";
   477 
   478 Goal "x: Rep_preal (w * z1 + w * z2) ==> \
   479 \              x: Rep_preal (w * (z1 + z2))";
   480 by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD],
   481               simpset()));
   482 by (forw_inst_tac [("ya","xa"),("yb","xb"),("xb","ya"),("xc","yb")] 
   483                                    lemma_add_mult_mem_Rep_preal1 1);
   484 by Auto_tac;
   485 by (res_inst_tac [("q1.0","xa"),("q2.0","xb")] prat_linear_less2 1);
   486 by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1);
   487 by (rtac (Rep_preal RS prealE_lemma3b) 1);
   488 by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2]));
   489 by (dres_inst_tac [("ya","xb"),("yb","xa"),("xc","ya"),("xb","yb")] 
   490                                    lemma_add_mult_mem_Rep_preal1 1);
   491 by Auto_tac;
   492 by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1);
   493 by (rtac (Rep_preal RS prealE_lemma3b) 1);
   494 by (thin_tac "xb * ya + xb * yb  : Rep_preal (w * (z1 + z2))" 1);
   495 by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib,
   496               prat_add_commute] @ preal_add_ac ));
   497 qed "lemma_preal_add_mult_distrib";
   498 
   499 Goal "x: Rep_preal (w * (z1 + z2)) ==> \
   500 \              x: Rep_preal (w * z1 + w * z2)";
   501 by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD]
   502               addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI],
   503               simpset() addsimps [prat_add_mult_distrib2]));
   504 qed "lemma_preal_add_mult_distrib2";
   505 
   506 Goal "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)";
   507 by (rtac (inj_Rep_preal RS injD) 1);
   508 by (rtac set_ext 1);
   509 by (fast_tac (claset() addIs [lemma_preal_add_mult_distrib,
   510                        lemma_preal_add_mult_distrib2]) 1);
   511 qed "preal_add_mult_distrib2";
   512 
   513 Goal "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)";
   514 by (simp_tac (simpset() addsimps [preal_mult_commute,
   515                        preal_add_mult_distrib2]) 1);
   516 qed "preal_add_mult_distrib";
   517 
   518 (*** Prove existence of inverse ***)
   519 (*** Inverse is a positive real ***)
   520 
   521 Goal "? y. qinv(y) ~:  Rep_preal X";
   522 by (cut_inst_tac [("X","X")] not_mem_Rep_preal_Ex 1);
   523 by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
   524 by Auto_tac;
   525 qed "qinv_not_mem_Rep_preal_Ex";
   526 
   527 Goal "? q. q: {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   528 by (cut_inst_tac [("X","A")] qinv_not_mem_Rep_preal_Ex 1);
   529 by Auto_tac;
   530 by (cut_inst_tac [("y","y")] qless_Ex 1);
   531 by (Fast_tac 1);
   532 qed "lemma_preal_mem_inv_set_ex";
   533 
   534 (** Part 1 of Dedekind sections def **)
   535 Goal "{} < {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   536 by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
   537 by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   538 qed "preal_inv_set_not_empty";
   539 
   540 (** Part 2 of Dedekind sections def **)
   541 Goal "? y. qinv(y) :  Rep_preal X";
   542 by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
   543 by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
   544 by Auto_tac;
   545 qed "qinv_mem_Rep_preal_Ex";
   546 
   547 Goal "? x. x ~: {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   548 by (rtac ccontr 1);
   549 by (cut_inst_tac [("X","A")] qinv_mem_Rep_preal_Ex 1);
   550 by Auto_tac;
   551 by (EVERY1[etac allE, etac exE, etac conjE]);
   552 by (dtac qinv_prat_less 1 THEN dtac not_in_preal_ub 1);
   553 by (eres_inst_tac [("x","qinv y")] ballE 1);
   554 by (dtac prat_less_trans 1);
   555 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   556 qed "preal_not_mem_inv_set_Ex";
   557 
   558 Goal "{x. ? y. x < y & qinv y ~:  Rep_preal A} < {q. True}";
   559 by (auto_tac (claset() addSIs [psubsetI],simpset()));
   560 by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
   561 by (etac exE 1);
   562 by (eres_inst_tac [("c","x")] equalityCE 1);
   563 by Auto_tac;
   564 qed "preal_inv_set_not_prat_set";
   565 
   566 (** Part 3 of Dedekind sections def **)
   567 Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
   568  \      !z. z < y --> z : {x. ? y. x < y & qinv y ~: Rep_preal A}";
   569 by Auto_tac;
   570 by (res_inst_tac [("x","ya")] exI 1);
   571 by (auto_tac (claset() addIs [prat_less_trans],simpset()));
   572 qed "preal_inv_set_lemma3";
   573 
   574 Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
   575 \       Bex {x. ? y. x < y & qinv y ~: Rep_preal A} (op < y)";
   576 by (blast_tac (claset() addDs [prat_dense]) 1);
   577 qed "preal_inv_set_lemma4";
   578 
   579 Goal "{x. ? y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
   580 by (rtac prealI2 1);
   581 by (rtac preal_inv_set_not_empty 1);
   582 by (rtac preal_inv_set_not_prat_set 1);
   583 by (rtac preal_inv_set_lemma3 1);
   584 by (rtac preal_inv_set_lemma4 1);
   585 qed "preal_mem_inv_set";
   586 
   587 (*more lemmas for inverse *)
   588 Goal "x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
   589 by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
   590               simpset() addsimps [pinv_def,preal_prat_def] ));
   591 by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
   592 by (auto_tac (claset() addSDs [not_in_preal_ub],simpset()));
   593 by (dtac prat_mult_less_mono 1 THEN Blast_tac 1);
   594 by (auto_tac (claset(),simpset()));
   595 qed "preal_mem_mult_invD";
   596 
   597 (*** Gleason's Lemma 9-3.4 p 122 ***)
   598 Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
   599 \            ? xb : Rep_preal(A). xb + ($#p)*x : Rep_preal(A)";
   600 by (cut_facts_tac [mem_Rep_preal_Ex] 1);
   601 by (res_inst_tac [("n","p")] pnat_induct 1);
   602 by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
   603     pSuc_is_plus_one,prat_add_mult_distrib,prat_pnat_add,prat_add_assoc RS sym]));
   604 qed "lemma1_gleason9_34";
   605 
   606 Goal "Abs_prat (ratrel ^^ {(y, z)}) < xb + \
   607 \         Abs_prat (ratrel ^^ {(x*y, Abs_pnat 1)})*Abs_prat (ratrel ^^ {(w, x)})";
   608 by (res_inst_tac [("j","Abs_prat (ratrel ^^ {(x * y, Abs_pnat 1)}) *\
   609 \                   Abs_prat (ratrel ^^ {(w, x)})")] prat_le_less_trans 1);
   610 by (rtac prat_self_less_add_right 2);
   611 by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
   612     simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
   613 qed "lemma1b_gleason9_34";
   614 
   615 Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
   616 by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
   617 by (etac exE 1);
   618 by (dtac not_in_preal_ub 1);
   619 by (res_inst_tac [("z","x")] eq_Abs_prat 1);
   620 by (res_inst_tac [("z","xa")] eq_Abs_prat 1);
   621 by (dres_inst_tac [("p","y*xb")] lemma1_gleason9_34 1);
   622 by (etac bexE 1);
   623 by (cut_inst_tac [("x","y"),("y","xb"),("w","xaa"),
   624     ("z","ya"),("xb","xba")] lemma1b_gleason9_34 1);
   625 by (dres_inst_tac [("x","xba + $#(y * xb) * x")]  bspec 1);
   626 by (auto_tac (claset() addIs [prat_less_asym],
   627     simpset() addsimps [prat_pnat_def]));
   628 qed "lemma_gleason9_34a";
   629 
   630 Goal "? r: Rep_preal(R). r + x ~: Rep_preal(R)";
   631 by (rtac ccontr 1);
   632 by (blast_tac (claset() addIs [lemma_gleason9_34a]) 1);
   633 qed "lemma_gleason9_34";
   634 
   635 (*** Gleason's Lemma 9-3.6  ***)
   636 (*  lemmas for Gleason 9-3.6  *)
   637 (*                            *) 
   638 (******************************)
   639 
   640 Goal "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)";
   641 by (full_simp_tac (simpset() addsimps [prat_add_mult_distrib2,
   642     prat_mult_assoc]) 1);
   643 qed "lemma1_gleason9_36";
   644 
   645 Goal "r*qinv(xa)*(xa*x) = r*x";
   646 by (full_simp_tac (simpset() addsimps prat_mult_ac) 1);
   647 qed "lemma2_gleason9_36";
   648 (******)
   649 
   650 (*** FIXME: long! ***)
   651 Goal "$#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   652 by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
   653 by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
   654 by (Fast_tac 1);
   655 by (dres_inst_tac [("x","xa")] prat_self_less_mult_right 1);
   656 by (etac prat_lessE 1);
   657 by (cut_inst_tac [("R","A"),("x","Q3")] lemma_gleason9_34 1);
   658 by (dtac sym 1 THEN Auto_tac );
   659 by (forward_tac [not_in_preal_ub] 1);
   660 by (dres_inst_tac [("x","xa + Q3")] bspec 1 THEN assume_tac 1);
   661 by (dtac prat_add_right_less_cancel 1);
   662 by (dres_inst_tac [("x","qinv(xa)*Q3")] prat_mult_less2_mono1 1);
   663 by (dres_inst_tac [("x","r")] prat_add_less2_mono2 1);
   664 by (asm_full_simp_tac (simpset() addsimps
   665     [prat_mult_assoc RS sym,lemma1_gleason9_36]) 1);
   666 by (dtac sym 1);
   667 by (auto_tac (claset(),simpset() addsimps [lemma2_gleason9_36]));
   668 by (res_inst_tac [("x","r")] bexI 1);
   669 by (rtac notI 1);
   670 by (dres_inst_tac [("y","r*x")] (Rep_preal RS prealE_lemma3b) 1);
   671 by Auto_tac;
   672 qed "lemma_gleason9_36";
   673 
   674 Goal "$#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   675 by (rtac lemma_gleason9_36 1);
   676 by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
   677 qed "lemma_gleason9_36a";
   678 
   679 (*** Part 2 of existence of inverse ***)
   680 Goal "x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
   681 by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
   682               simpset() addsimps [pinv_def,preal_prat_def] ));
   683 by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
   684 by (dtac prat_qinv_gt_1 1);
   685 by (dres_inst_tac [("A","A")] lemma_gleason9_36a 1);
   686 by Auto_tac;
   687 by (dtac (Rep_preal RS prealE_lemma4a) 1);
   688 by (Auto_tac  THEN dtac qinv_prat_less 1);
   689 by (res_inst_tac [("x","qinv(u)*x")] exI 1);
   690 by (rtac conjI 1);
   691 by (res_inst_tac [("x","qinv(r)*x")] exI 1);
   692 by (auto_tac (claset() addIs [prat_mult_less2_mono1],
   693     simpset() addsimps [qinv_mult_eq,qinv_qinv]));
   694 by (res_inst_tac [("x","u")] bexI 1);
   695 by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc,
   696     prat_mult_left_commute]));
   697 qed "preal_mem_mult_invI";
   698 
   699 Goal "pinv(A)*A = (@#($#Abs_pnat 1))";
   700 by (rtac (inj_Rep_preal RS injD) 1);
   701 by (rtac set_ext 1);
   702 by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
   703 qed "preal_mult_inv";
   704 
   705 Goal "A*pinv(A) = (@#($#Abs_pnat 1))";
   706 by (rtac (preal_mult_commute RS subst) 1);
   707 by (rtac preal_mult_inv 1);
   708 qed "preal_mult_inv_right";
   709 
   710 val [prem] = goal thy
   711     "(!!u. z = Abs_preal(u) ==> P) ==> P";
   712 by (cut_inst_tac [("x1","z")] 
   713     (rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1);
   714 by (res_inst_tac [("u","Rep_preal z")] prem 1);
   715 by (dtac (inj_Rep_preal RS injD) 1);
   716 by (Asm_simp_tac 1);
   717 qed "eq_Abs_preal";
   718 
   719 (*** Lemmas/Theorem(s) need lemma_gleason9_34 ***)
   720 Goal "Rep_preal (R1) <= Rep_preal(R1 + R2)";
   721 by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
   722 by (auto_tac (claset() addSIs [bexI] addIs [(Rep_preal RS prealE_lemma3b),
   723    prat_self_less_add_left,mem_Rep_preal_addI],simpset()));
   724 qed "Rep_preal_self_subset";
   725 
   726 Goal "~ Rep_preal (R1 + R2) <= Rep_preal(R1)";
   727 by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
   728 by (etac exE 1);
   729 by (cut_inst_tac [("R","R1")] lemma_gleason9_34 1);
   730 by (auto_tac (claset() addIs [mem_Rep_preal_addI],simpset()));
   731 qed "Rep_preal_sum_not_subset";
   732 
   733 Goal "Rep_preal (R1 + R2) ~= Rep_preal(R1)";
   734 by (rtac notI 1);
   735 by (etac equalityE 1);
   736 by (asm_full_simp_tac (simpset() addsimps [Rep_preal_sum_not_subset]) 1);
   737 qed "Rep_preal_sum_not_eq";
   738 
   739 (*** at last --- Gleason prop. 9-3.5(iii) p. 123 ***)
   740 Goalw [preal_less_def,psubset_def] "(R1::preal) < R1 + R2";
   741 by (simp_tac (simpset() addsimps [Rep_preal_self_subset,
   742     Rep_preal_sum_not_eq RS not_sym]) 1);
   743 qed "preal_self_less_add_left";
   744 
   745 Goal "(R1::preal) < R2 + R1";
   746 by (simp_tac (simpset() addsimps [preal_add_commute,preal_self_less_add_left]) 1);
   747 qed "preal_self_less_add_right";
   748 
   749 (*** Properties of <= ***)
   750 
   751 Goalw [preal_le_def,psubset_def,preal_less_def] 
   752                      "z<=w ==> ~(w<(z::preal))";
   753 by (auto_tac  (claset() addDs [equalityI],simpset()));
   754 qed "preal_leD";
   755 
   756 val preal_leE = make_elim preal_leD;
   757 
   758 Goalw [preal_le_def,psubset_def,preal_less_def]
   759                    "~ z <= w ==> w<(z::preal)";
   760 by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
   761 by (auto_tac  (claset(),simpset() addsimps [preal_less_def,psubset_def]));
   762 qed "not_preal_leE";
   763 		       
   764 Goal "~(w < z) ==> z <= (w::preal)";
   765 by (fast_tac (claset() addIs [not_preal_leE]) 1);
   766 qed "preal_leI";
   767 
   768 Goal "(~(w < z)) = (z <= (w::preal))";
   769 by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1);
   770 qed "preal_less_le_iff";
   771 
   772 Goalw [preal_le_def,preal_less_def,psubset_def] 
   773                   "z < w ==> z <= (w::preal)";
   774 by (Fast_tac 1);
   775 qed "preal_less_imp_le";
   776 
   777 Goalw [preal_le_def,preal_less_def,psubset_def] 
   778                       "!!(x::preal). x <= y ==> x < y | x = y";
   779 by (auto_tac (claset() addIs [inj_Rep_preal RS injD],simpset()));
   780 qed "preal_le_imp_less_or_eq";
   781 
   782 Goalw [preal_le_def,preal_less_def,psubset_def] 
   783                        "!!(x::preal). x < y | x = y ==> x <=y";
   784 by Auto_tac;
   785 qed "preal_less_or_eq_imp_le";
   786 
   787 Goalw [preal_le_def] "w <= (w::preal)";
   788 by (Simp_tac 1);
   789 qed "preal_le_refl";
   790 
   791 val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::preal)";
   792 by (dtac preal_le_imp_less_or_eq 1);
   793 by (fast_tac (claset() addIs [preal_less_trans]) 1);
   794 qed "preal_le_less_trans";
   795 
   796 val prems = goal thy "!!i. [| i < j; j <= k |] ==> i < (k::preal)";
   797 by (dtac preal_le_imp_less_or_eq 1);
   798 by (fast_tac (claset() addIs [preal_less_trans]) 1);
   799 qed "preal_less_le_trans";
   800 
   801 Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
   802 by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
   803             rtac preal_less_or_eq_imp_le, fast_tac (claset() addIs [preal_less_trans])]);
   804 qed "preal_le_trans";
   805 
   806 Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
   807 by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
   808             fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
   809 qed "preal_le_anti_sym";
   810 
   811 Goal "[| ~ y < x; y ~= x |] ==> x < (y::preal)";
   812 by (rtac not_preal_leE 1);
   813 by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
   814 qed "not_less_not_eq_preal_less";
   815 
   816 (****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
   817 
   818 (**** Set up all lemmas for proving A < B ==> ?D. A + D = B ****)
   819 (**** Gleason prop. 9-3.5(iv) p. 123 ****)
   820 (**** Define the D required and show that it is a positive real ****)
   821 
   822 (* useful lemmas - proved elsewhere? *)
   823 Goalw [psubset_def] "A < B ==> ? x. x ~: A & x : B";
   824 by (etac conjE 1);
   825 by (etac swap 1);
   826 by (etac equalityI 1);
   827 by Auto_tac;
   828 qed "lemma_psubset_mem";
   829 
   830 Goalw [psubset_def] "~ (A::'a set) < A";
   831 by (Fast_tac 1);
   832 qed "lemma_psubset_not_refl";
   833 
   834 Goalw [psubset_def] "!!(A::'a set). [| A < B; B < C |] ==> A < C";
   835 by (auto_tac (claset() addDs [subset_antisym],simpset()));
   836 qed "psubset_trans";
   837 
   838 Goalw [psubset_def] "!!(A::'a set). [| A <= B; B < C |] ==> A < C";
   839 by (auto_tac (claset() addDs [subset_antisym],simpset()));
   840 qed "subset_psubset_trans";
   841 
   842 Goalw [psubset_def] "!!(A::'a set). [| A < B; B <= C |] ==> A < C";
   843 by (auto_tac (claset() addDs [subset_antisym],simpset()));
   844 qed "subset_psubset_trans2";
   845 
   846 Goalw [psubset_def] "!!(A::'a set). [| A < B; c : A |] ==> c : B";
   847 by (auto_tac (claset() addDs [subsetD],simpset()));
   848 qed "psubsetD";
   849 
   850 (** Part 1 of Dedekind sections def **)
   851 Goalw [preal_less_def]
   852      "A < B ==> \
   853 \     ? q. q : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   854 by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
   855 by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
   856 by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
   857 qed "lemma_ex_mem_less_left_add1";
   858 
   859 Goal
   860      "A < B ==> \
   861 \       {} < {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   862 by (dtac lemma_ex_mem_less_left_add1 1);
   863 by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   864 qed "preal_less_set_not_empty";
   865 
   866 (** Part 2 of Dedekind sections def **)
   867 Goal "? q. q ~: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   868 by (cut_inst_tac [("X","B")] not_mem_Rep_preal_Ex 1);
   869 by (etac exE 1);
   870 by (res_inst_tac [("x","x")] exI 1);
   871 by Auto_tac;
   872 by (cut_inst_tac [("x","x"),("y","n")] prat_self_less_add_right 1);
   873 by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
   874 qed "lemma_ex_not_mem_less_left_add1";
   875 
   876 Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < {q. True}";
   877 by (auto_tac (claset() addSIs [psubsetI],simpset()));
   878 by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
   879 by (etac exE 1);
   880 by (eres_inst_tac [("c","q")] equalityCE 1);
   881 by Auto_tac;
   882 qed "preal_less_set_not_prat_set";
   883 
   884 (** Part 3 of Dedekind sections def **)
   885 Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   886  \      !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   887 by Auto_tac;
   888 by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
   889 by (dtac (Rep_preal RS prealE_lemma3b) 1);
   890 by Auto_tac;
   891 qed "preal_less_set_lemma3";
   892 
   893 Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   894 \       Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
   895 by Auto_tac;
   896 by (dtac (Rep_preal RS prealE_lemma4a) 1);
   897 by (auto_tac (claset(),simpset() addsimps [prat_less_def,prat_add_assoc]));
   898 qed "preal_less_set_lemma4";
   899 
   900 Goal 
   901      "!! (A::preal). A < B ==> \
   902 \     {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
   903 by (rtac prealI2 1);
   904 by (rtac preal_less_set_not_empty 1);
   905 by (rtac preal_less_set_not_prat_set 2);
   906 by (rtac preal_less_set_lemma3 2);
   907 by (rtac preal_less_set_lemma4 3);
   908 by Auto_tac;
   909 qed "preal_mem_less_set";
   910 
   911 (** proving that A + D <= B **)
   912 Goalw [preal_le_def] 
   913        "!! (A::preal). A < B ==> \
   914 \         A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
   915 by (rtac subsetI 1);
   916 by (dtac mem_Rep_preal_addD 1);
   917 by (auto_tac (claset(),simpset() addsimps [
   918     preal_mem_less_set RS Abs_preal_inverse]));
   919 by (dtac not_in_preal_ub 1);
   920 by (dtac bspec 1 THEN assume_tac 1);
   921 by (dres_inst_tac [("x","y")] prat_add_less2_mono1 1);
   922 by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma3b) 1);
   923 by Auto_tac;
   924 qed "preal_less_add_left_subsetI";
   925 
   926 (** proving that B <= A + D  --- trickier **)
   927 (** lemma **)
   928 Goal "x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
   929 by (dtac (Rep_preal RS prealE_lemma4a) 1);
   930 by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
   931 qed "lemma_sum_mem_Rep_preal_ex";
   932 
   933 Goalw [preal_le_def] 
   934        "!! (A::preal). A < B ==> \
   935 \         B <= A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
   936 by (rtac subsetI 1);
   937 by (res_inst_tac [("Q","x: Rep_preal(A)")] (excluded_middle RS disjE) 1);
   938 by (rtac mem_Rep_preal_addI 1);
   939 by (dtac lemma_sum_mem_Rep_preal_ex 1);
   940 by (etac exE 1);
   941 by (cut_inst_tac [("R","A"),("x","e")] lemma_gleason9_34 1 THEN etac bexE 1);
   942 by (dtac not_in_preal_ub 1 THEN dtac bspec 1 THEN assume_tac 1);
   943 by (etac prat_lessE 1);
   944 by (res_inst_tac [("x","r")] bexI 1);
   945 by (res_inst_tac [("x","Q3")] bexI 1);
   946 by (cut_facts_tac [Rep_preal_self_subset] 4);
   947 by (auto_tac (claset(),simpset() addsimps [
   948     preal_mem_less_set RS Abs_preal_inverse]));
   949 by (res_inst_tac [("x","r+e")] exI 1);
   950 by (asm_full_simp_tac (simpset() addsimps prat_add_ac) 1);
   951 qed "preal_less_add_left_subsetI2";
   952 
   953 (*** required proof ***)
   954 Goal "!! (A::preal). A < B ==> \
   955 \         A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
   956 by (blast_tac (claset() addIs [preal_le_anti_sym,
   957                 preal_less_add_left_subsetI,preal_less_add_left_subsetI2]) 1);
   958 qed "preal_less_add_left";
   959 
   960 Goal "!! (A::preal). A < B ==> ? D. A + D = B";
   961 by (fast_tac (claset() addDs [preal_less_add_left]) 1);
   962 qed "preal_less_add_left_Ex";        
   963 
   964 Goal "!!(A::preal). A < B ==> A + C < B + C";
   965 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   966     simpset() addsimps [preal_add_assoc]));
   967 by (res_inst_tac [("y1","D")] (preal_add_commute RS subst) 1);
   968 by (auto_tac (claset() addIs [preal_self_less_add_left],
   969           simpset() addsimps [preal_add_assoc RS sym]));
   970 qed "preal_add_less2_mono1";
   971 
   972 Goal "!!(A::preal). A < B ==> C + A < C + B";
   973 by (auto_tac (claset() addIs [preal_add_less2_mono1],
   974     simpset() addsimps [preal_add_commute]));
   975 qed "preal_add_less2_mono2";
   976 
   977 Goal 
   978       "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x";
   979 by (dtac preal_less_add_left_Ex 1);
   980 by (auto_tac (claset(),simpset() addsimps [preal_add_mult_distrib,
   981     preal_self_less_add_left]));
   982 qed "preal_mult_less_mono1";
   983 
   984 Goal "!!(q1::preal). q1 < q2  ==> x * q1 < x * q2";
   985 by (auto_tac (claset() addDs [preal_mult_less_mono1],
   986     simpset() addsimps [preal_mult_commute]));
   987 qed "preal_mult_left_less_mono1";
   988 
   989 Goal "!!(q1::preal). q1 <= q2  ==> x * q1 <= x * q2";
   990 by (dtac preal_le_imp_less_or_eq 1);
   991 by (Step_tac 1);
   992 by (auto_tac (claset() addSIs [preal_le_refl,
   993     preal_less_imp_le,preal_mult_left_less_mono1],simpset()));
   994 qed "preal_mult_left_le_mono1";
   995  
   996 Goal "!!(q1::preal). q1 <= q2  ==> q1 * x <= q2 * x";
   997 by (auto_tac (claset() addDs [preal_mult_left_le_mono1],
   998     simpset() addsimps [preal_mult_commute]));
   999 qed "preal_mult_le_mono1";
  1000  
  1001 Goal "!!(q1::preal). q1 <= q2  ==> x + q1 <= x + q2";
  1002 by (dtac preal_le_imp_less_or_eq 1);
  1003 by (Step_tac 1);
  1004 by (auto_tac (claset() addSIs [preal_le_refl,
  1005     preal_less_imp_le,preal_add_less2_mono1],
  1006     simpset() addsimps [preal_add_commute]));
  1007 qed "preal_add_left_le_mono1";
  1008 
  1009 Goal "!!(q1::preal). q1 <= q2  ==> q1 + x <= q2 + x";
  1010 by (auto_tac (claset() addDs [preal_add_left_le_mono1],
  1011     simpset() addsimps [preal_add_commute]));
  1012 qed "preal_add_le_mono1";
  1013  
  1014 Goal "!!(A::preal). A + C < B + C ==> A < B";
  1015 by (cut_facts_tac [preal_linear] 1);
  1016 by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
  1017 by (dres_inst_tac [("A","B"),("C","C")] preal_add_less2_mono1 1);
  1018 by (fast_tac (claset() addDs [preal_less_trans] 
  1019                 addEs [preal_less_irrefl]) 1);
  1020 qed "preal_add_right_less_cancel";
  1021 
  1022 Goal "!!(A::preal). C + A < C + B ==> A < B";
  1023 by (auto_tac (claset() addEs [preal_add_right_less_cancel],
  1024               simpset() addsimps [preal_add_commute]));
  1025 qed "preal_add_left_less_cancel";
  1026 
  1027 Goal "((A::preal) + C < B + C) = (A < B)";
  1028 by (REPEAT(ares_tac [iffI,preal_add_less2_mono1,
  1029     preal_add_right_less_cancel] 1));
  1030 qed "preal_add_less_iff1";
  1031 
  1032 Addsimps [preal_add_less_iff1];
  1033 
  1034 Goal "(C + (A::preal) < C + B) = (A < B)";
  1035 by (REPEAT(ares_tac [iffI,preal_add_less2_mono2,
  1036     preal_add_left_less_cancel] 1));
  1037 qed "preal_add_less_iff2";
  1038 
  1039 Addsimps [preal_add_less_iff2];
  1040 
  1041 Goal "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
  1042 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  1043     simpset() addsimps  preal_add_ac));
  1044 by (rtac (preal_add_assoc RS subst) 1);
  1045 by (rtac preal_self_less_add_right 1);
  1046 qed "preal_add_less_mono";
  1047 
  1048 Goal "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
  1049 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  1050               simpset() addsimps [preal_add_mult_distrib,
  1051               preal_add_mult_distrib2,preal_self_less_add_left,
  1052               preal_add_assoc] @ preal_mult_ac));
  1053 qed "preal_mult_less_mono";
  1054 
  1055 Goal "!!(A::preal). A + C = B + C ==> A = B";
  1056 by (cut_facts_tac [preal_linear] 1);
  1057 by Auto_tac;
  1058 by (ALLGOALS(dres_inst_tac [("C","C")] preal_add_less2_mono1));
  1059 by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
  1060 qed "preal_add_right_cancel";
  1061 
  1062 Goal "!!(A::preal). C + A = C + B ==> A = B";
  1063 by (auto_tac (claset() addIs [preal_add_right_cancel],
  1064               simpset() addsimps [preal_add_commute]));
  1065 qed "preal_add_left_cancel";
  1066 
  1067 Goal "(C + A = C + B) = ((A::preal) = B)";
  1068 by (fast_tac (claset() addIs [preal_add_left_cancel]) 1);
  1069 qed "preal_add_left_cancel_iff";
  1070 
  1071 Goal "(A + C = B + C) = ((A::preal) = B)";
  1072 by (fast_tac (claset() addIs [preal_add_right_cancel]) 1);
  1073 qed "preal_add_right_cancel_iff";
  1074 
  1075 Addsimps [preal_add_left_cancel_iff,preal_add_right_cancel_iff];
  1076 
  1077 (*** Completeness of preal ***)
  1078 
  1079 (*** prove that supremum is a cut ***)
  1080 Goal "? (X::preal). X: P ==> \
  1081 \         ? q.  q: {w. ? X. X : P & w : Rep_preal X}";
  1082 by Safe_tac;
  1083 by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
  1084 by Auto_tac;
  1085 qed "preal_sup_mem_Ex";
  1086 
  1087 (** Part 1 of Dedekind def **)
  1088 Goal "? (X::preal). X: P ==> \
  1089 \         {} < {w. ? X : P. w : Rep_preal X}";
  1090 by (dtac preal_sup_mem_Ex 1);
  1091 by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
  1092 qed "preal_sup_set_not_empty";
  1093 
  1094 (** Part 2 of Dedekind sections def **) 
  1095 Goalw [preal_less_def] "? Y. (! X: P. X < Y)  \             
  1096 \         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
  1097 by (auto_tac (claset(),simpset() addsimps [psubset_def]));
  1098 by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
  1099 by (etac exE 1);
  1100 by (res_inst_tac [("x","x")] exI 1);
  1101 by (auto_tac (claset() addSDs [bspec],simpset()));
  1102 qed "preal_sup_not_mem_Ex";
  1103 
  1104 Goalw [preal_le_def] "? Y. (! X: P. X <= Y)  \
  1105 \         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
  1106 by (Step_tac 1);
  1107 by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
  1108 by (etac exE 1);
  1109 by (res_inst_tac [("x","x")] exI 1);
  1110 by (auto_tac (claset() addSDs [bspec],simpset()));
  1111 qed "preal_sup_not_mem_Ex1";
  1112 
  1113 Goal "? Y. (! X: P. X < Y)  \                                    
  1114 \         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";       (**)
  1115 by (dtac preal_sup_not_mem_Ex 1);
  1116 by (auto_tac (claset() addSIs [psubsetI],simpset()));
  1117 by (eres_inst_tac [("c","q")] equalityCE 1);
  1118 by Auto_tac;
  1119 qed "preal_sup_set_not_prat_set";
  1120 
  1121 Goal "? Y. (! X: P. X <= Y)  \
  1122 \         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
  1123 by (dtac preal_sup_not_mem_Ex1 1);
  1124 by (auto_tac (claset() addSIs [psubsetI],simpset()));
  1125 by (eres_inst_tac [("c","q")] equalityCE 1);
  1126 by Auto_tac;
  1127 qed "preal_sup_set_not_prat_set1";
  1128 
  1129 (** Part 3 of Dedekind sections def **)
  1130 Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
  1131 \         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
  1132 \             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";         (**)
  1133 by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
  1134 qed "preal_sup_set_lemma3";
  1135 
  1136 Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  1137 \         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
  1138 \             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
  1139 by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
  1140 qed "preal_sup_set_lemma3_1";
  1141 
  1142 Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
  1143 \         ==>  !y: {w. ? X: P. w: Rep_preal X}. \                        
  1144 \             Bex {w. ? X: P. w: Rep_preal X} (op < y)";                (**)
  1145 by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
  1146 qed "preal_sup_set_lemma4";
  1147 
  1148 Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  1149 \         ==>  !y: {w. ? X: P. w: Rep_preal X}. \
  1150 \             Bex {w. ? X: P. w: Rep_preal X} (op < y)";
  1151 by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
  1152 qed "preal_sup_set_lemma4_1";
  1153 
  1154 Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \            
  1155 \         ==> {w. ? X: P. w: Rep_preal(X)}: preal";                      (**)
  1156 by (rtac prealI2 1);
  1157 by (rtac preal_sup_set_not_empty 1);
  1158 by (rtac preal_sup_set_not_prat_set 2);
  1159 by (rtac preal_sup_set_lemma3 3);
  1160 by (rtac preal_sup_set_lemma4 5);
  1161 by Auto_tac;
  1162 qed "preal_sup";
  1163 
  1164 Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  1165 \         ==> {w. ? X: P. w: Rep_preal(X)}: preal";
  1166 by (rtac prealI2 1);
  1167 by (rtac preal_sup_set_not_empty 1);
  1168 by (rtac preal_sup_set_not_prat_set1 2);
  1169 by (rtac preal_sup_set_lemma3_1 3);
  1170 by (rtac preal_sup_set_lemma4_1 5);
  1171 by Auto_tac;
  1172 qed "preal_sup1";
  1173 
  1174 Goalw [psup_def] "? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P";      (**) 
  1175 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  1176 by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
  1177 by Auto_tac;
  1178 qed "preal_psup_leI";
  1179 
  1180 Goalw [psup_def] "? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
  1181 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  1182 by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
  1183 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  1184 qed "preal_psup_leI2";
  1185 
  1186 Goal "[| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P";              (**)
  1187 by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
  1188 qed "preal_psup_leI2b";
  1189 
  1190 Goal "[| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
  1191 by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
  1192 qed "preal_psup_leI2a";
  1193 
  1194 Goalw [psup_def] "[| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y";   (**)
  1195 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  1196 by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
  1197 by (rotate_tac 1 2);
  1198 by (assume_tac 2);
  1199 by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
  1200 qed "psup_le_ub";
  1201 
  1202 Goalw [psup_def] "[| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
  1203 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  1204 by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
  1205 by (rotate_tac 1 2);
  1206 by (assume_tac 2);
  1207 by (auto_tac (claset() addSDs [bspec],
  1208     simpset() addsimps [preal_less_def,psubset_def,preal_le_def]));
  1209 qed "psup_le_ub1";
  1210 
  1211 (** supremum property **)
  1212 Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \                  
  1213 \         ==> (!Y. (? X: P. Y < X) = (Y < psup P))";              
  1214 by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
  1215 by (Fast_tac 1);
  1216 by (auto_tac (claset() addSIs [psubsetI],simpset() addsimps [psup_def,preal_less_def]));
  1217 by (blast_tac (claset() addDs [psubset_def RS meta_eq_to_obj_eq RS iffD1]) 1);
  1218 by (rotate_tac 4 1);
  1219 by (asm_full_simp_tac (simpset() addsimps [psubset_def]) 1);
  1220 by (dtac bspec 1 THEN assume_tac 1);
  1221 by (REPEAT(etac conjE 1));
  1222 by (EVERY1[rtac swap, assume_tac, rtac set_ext]);
  1223 by (auto_tac (claset() addSDs [lemma_psubset_mem],simpset()));
  1224 by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1);
  1225 by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def]));
  1226 qed "preal_complete";
  1227 
  1228 (****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
  1229     (****** Embedding ******)
  1230 (*** mapping from prat into preal ***)
  1231 
  1232 Goal "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
  1233 by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1);
  1234 by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
  1235 qed "lemma_preal_rat_less";
  1236 
  1237 Goal "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
  1238 by (stac prat_add_commute 1);
  1239 by (dtac (prat_add_commute RS subst) 1);
  1240 by (etac lemma_preal_rat_less 1);
  1241 qed "lemma_preal_rat_less2";
  1242 
  1243 Goalw [preal_prat_def,preal_add_def] 
  1244             "@#((z1::prat) + z2) = @#z1 + @#z2";
  1245 by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
  1246 by (auto_tac (claset() addIs [prat_add_less_mono] addSIs [set_ext],simpset() addsimps 
  1247     [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
  1248 by (res_inst_tac [("x","x*z1*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
  1249 by (etac lemma_preal_rat_less 1);
  1250 by (res_inst_tac [("x","x*z2*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
  1251 by (etac lemma_preal_rat_less2 1);
  1252 by (asm_full_simp_tac (simpset() addsimps [prat_add_mult_distrib RS sym,
  1253      prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
  1254 qed "preal_prat_add";
  1255 
  1256 Goal "x < xa ==> x*z1*qinv(xa) < z1";
  1257 by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
  1258 by (dtac (prat_mult_left_commute RS subst) 1);
  1259 by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
  1260 qed "lemma_preal_rat_less3";
  1261 
  1262 Goal "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
  1263 by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1);
  1264 by (dtac (prat_mult_left_commute RS subst) 1);
  1265 by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
  1266 qed "lemma_preal_rat_less4";
  1267 
  1268 Goalw [preal_prat_def,preal_mult_def] 
  1269             "@#((z1::prat) * z2) = @#z1 * @#z2";
  1270 by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
  1271 by (auto_tac (claset() addIs [prat_mult_less_mono] addSIs [set_ext],simpset() addsimps 
  1272     [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
  1273 by (dtac prat_dense 1);
  1274 by (Step_tac 1);
  1275 by (res_inst_tac [("x","x*z1*qinv(xa)")] exI 1 THEN rtac conjI 1);
  1276 by (etac lemma_preal_rat_less3 1);
  1277 by (res_inst_tac [("x"," xa*z2*qinv(z1*z2)")] exI 1 THEN rtac conjI 1);
  1278 by (etac lemma_preal_rat_less4 1);
  1279 by (asm_full_simp_tac (simpset() 
  1280     addsimps [qinv_mult_eq RS sym] @ prat_mult_ac) 1);
  1281 by (asm_full_simp_tac (simpset() 
  1282     addsimps [prat_mult_assoc RS sym]) 1);
  1283 qed "preal_prat_mult";
  1284 
  1285 Goalw [preal_prat_def,preal_less_def] 
  1286       "(@#p < @#q) = (p < q)";
  1287 by (auto_tac (claset() addSDs [lemma_prat_set_eq] addEs [prat_less_trans],
  1288     simpset() addsimps [lemma_prat_less_set_mem_preal,
  1289     psubset_def,prat_less_not_refl]));
  1290 by (res_inst_tac [("q1.0","p"),("q2.0","q")] prat_linear_less2 1);
  1291 by (auto_tac (claset() addIs [prat_less_irrefl],simpset()));
  1292 qed "preal_prat_less_iff";
  1293 
  1294 Addsimps [preal_prat_less_iff];