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