src/HOL/Real/PReal.ML

Added hook for presburger arithmetic decision procedure.

(*  Title       : HOL/Real/PReal.ML
    ID          : $Id$
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : The positive reals as Dedekind sections of positive
                  rationals. Fundamentals of Abstract Analysis 
                  [Gleason- p. 121] provides some of the definitions.
*)

Goal "inj_on Abs_preal preal";
by (rtac inj_on_inverseI 1);
by (etac Abs_preal_inverse 1);
qed "inj_on_Abs_preal";

Addsimps [inj_on_Abs_preal RS inj_on_iff];

Goal "inj(Rep_preal)";
by (rtac inj_inverseI 1);
by (rtac Rep_preal_inverse 1);
qed "inj_Rep_preal";

Goalw [preal_def] "{} ~: preal";
by (Fast_tac 1);
qed "empty_not_mem_preal";

(* {} : preal ==> P *)
bind_thm ("empty_not_mem_prealE", empty_not_mem_preal RS notE);

Addsimps [empty_not_mem_preal];

Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} : preal";
by (rtac preal_1 1);
qed "one_set_mem_preal";

Addsimps [one_set_mem_preal];

Goalw [preal_def] "x : preal ==> {} < x";
by (Fast_tac 1);
qed "preal_psubset_empty";

Goal "{} < Rep_preal x";
by (rtac (Rep_preal RS preal_psubset_empty) 1);
qed "Rep_preal_psubset_empty";

Goal "EX x. x: Rep_preal X";
by (cut_inst_tac [("x","X")]  Rep_preal_psubset_empty 1);
by (auto_tac (claset() addIs [(equals0I RS sym)],
              simpset() addsimps [psubset_def]));
qed "mem_Rep_preal_Ex";

Goalw [preal_def] 
      "[| {} < A; A < UNIV; \
\              (ALL y: A. ((ALL z. z < y --> z: A) & \
\                        (EX u: A. y < u))) |] ==> A : preal";
by (Fast_tac 1);
qed "prealI1";
    
Goalw [preal_def] 
      "[| {} < A; A < UNIV; \
\              ALL y: A. (ALL z. z < y --> z: A); \
\              ALL y: A. (EX u: A. y < u) |] ==> A : preal";
by (Best_tac 1);
qed "prealI2";

Goalw [preal_def] 
      "A : preal ==> {} < A & A < UNIV & \
\                         (ALL y: A. ((ALL z. z < y --> z: A) & \
\                                  (EX u: A. y < u)))";
by (Fast_tac 1);
qed "prealE_lemma";


AddSIs [prealI1,prealI2];

Addsimps [Abs_preal_inverse];


Goalw [preal_def] "A : preal ==> {} < A";
by (Fast_tac 1);
qed "prealE_lemma1";

Goalw [preal_def] "A : preal ==> A < UNIV";
by (Fast_tac 1);
qed "prealE_lemma2";

Goalw [preal_def] "A : preal ==> ALL y: A. (ALL z. z < y --> z: A)";
by (Fast_tac 1);
qed "prealE_lemma3";

Goal "[| A : preal; y: A |] ==> (ALL z. z < y --> z: A)";
by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
qed "prealE_lemma3a";

Goal "[| A : preal; y: A; z < y |] ==> z: A";
by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
qed "prealE_lemma3b";

Goalw [preal_def] "A : preal ==> ALL y: A. (EX u: A. y < u)";
by (Fast_tac 1);
qed "prealE_lemma4";

Goal "[| A : preal; y: A |] ==> EX u: A. y < u";
by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
qed "prealE_lemma4a";

Goal "EX x. x~: Rep_preal X";
by (cut_inst_tac [("x","X")] Rep_preal 1);
by (dtac prealE_lemma2 1);
by (auto_tac (claset(),simpset() addsimps [psubset_def]));
qed "not_mem_Rep_preal_Ex";

(** preal_of_prat: the injection from prat to preal **)
(** A few lemmas **)

Goal "{xa::prat. xa < y} : preal";
by (cut_facts_tac [qless_Ex] 1);
by (auto_tac (claset() addIs[prat_less_trans]
                       addSEs [prat_less_irrefl], 
	      simpset()));
by (blast_tac (claset() addDs [prat_dense]) 1);
qed "lemma_prat_less_set_mem_preal";

Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y";
by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
by Safe_tac;
by (dtac prat_dense 2 THEN etac exE 2);
by (dtac prat_dense 1 THEN etac exE 1);
by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
qed "lemma_prat_set_eq";

Goal "inj(preal_of_prat)";
by (rtac injI 1);
by (rewtac preal_of_prat_def);
by (dtac (inj_on_Abs_preal RS inj_onD) 1);
by (rtac lemma_prat_less_set_mem_preal 1);
by (rtac lemma_prat_less_set_mem_preal 1);
by (etac lemma_prat_set_eq 1);
qed "inj_preal_of_prat";

      (*** theorems for ordering ***)
(* prove introduction and elimination rules for preal_less *)

(* A positive fraction not in a positive real is an upper bound *)
(* Gleason p. 122 - Remark (1)                                  *)

Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x";
by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
by (fast_tac (claset() addIs [not_less_not_eq_prat_less] addss simpset()) 1);
qed "not_in_preal_ub";

(* preal_less is a strong order i.e nonreflexive and transitive *)

Goalw [preal_less_def] "~ (x::preal) < x";
by (simp_tac (simpset() addsimps [psubset_def]) 1);
qed "preal_less_not_refl";

(*** y < y ==> P ***)
bind_thm("preal_less_irrefl", preal_less_not_refl RS notE);

Goal "!!(x::preal). x < y ==> x ~= y";
by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
qed "preal_not_refl2";

Goalw  [preal_less_def] "!!(x::preal). [| x < y; y < z |] ==> x < z";
by (auto_tac (claset() addDs [subsetD,equalityI],
              simpset() addsimps [psubset_def]));
qed "preal_less_trans";

Goal "!! (q1::preal). q1 < q2 ==> ~ q2 < q1";
by (rtac notI 1);
by (dtac preal_less_trans 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [preal_less_not_refl]) 1);
qed "preal_less_not_sym";

(* [| x < y;  ~P ==> y < x |] ==> P *)
bind_thm ("preal_less_asym", preal_less_not_sym RS contrapos_np);

Goalw [preal_less_def] 
      "(r1::preal) < r2 | r1 = r2 | r2 < r1";
by (auto_tac (claset() addSDs [inj_Rep_preal RS injD],
              simpset() addsimps [psubset_def]));
by (rtac prealE_lemma3b 1 THEN rtac Rep_preal 1);
by (assume_tac 1);
by (fast_tac (claset() addDs [not_in_preal_ub]) 1);
qed "preal_linear";

Goal "!!(r1::preal). [| r1 < r2 ==> P;  r1 = r2 ==> P; \
\                       r2 < r1 ==> P |] ==> P";
by (cut_inst_tac [("r1.0","r1"),("r2.0","r2")] preal_linear 1);
by Auto_tac;
qed "preal_linear_less2";

  (*** Properties of addition ***)

Goalw [preal_add_def] "(x::preal) + y = y + x";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (blast_tac (claset() addIs [prat_add_commute RS subst]) 1);
qed "preal_add_commute";

(** addition of two positive reals gives a positive real **)
(** lemmas for proving positive reals addition set in preal **)

(** Part 1 of Dedekind sections def **)
Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
by (auto_tac (claset() addSIs [psubsetI], simpset()));
qed "preal_add_set_not_empty";

(** Part 2 of Dedekind sections def **)
Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
by (REPEAT(etac exE 1));
by (REPEAT(dtac not_in_preal_ub 1));
by (res_inst_tac [("x","x+xa")] exI 1);
by (Auto_tac THEN (REPEAT(etac ballE 1)) THEN Auto_tac);
by (dtac prat_add_less_mono 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_add_set_Ex";

Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
by Auto_tac;
qed "preal_add_set_not_prat_set";

(** Part 3 of Dedekind sections def **)
Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
by Auto_tac;
by (ftac prat_mult_qinv_less_1 1);
by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat (Suc 0))")] 
    prat_mult_less2_mono1 1);
by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat (Suc 0))")] 
    prat_mult_less2_mono1 1);
by (Asm_full_simp_tac 1);
by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
by (REPEAT(etac allE 1));
by Auto_tac;
by (REPEAT(rtac bexI 1));
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2 
     RS sym,prat_add_assoc RS sym,prat_mult_assoc]));
qed "preal_add_set_lemma3";

Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. y < u";
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset() addIs [prat_add_less2_mono1],simpset()));
qed "preal_add_set_lemma4";

Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y} : preal";
by (rtac prealI2 1);
by (rtac preal_add_set_not_empty 1);
by (rtac preal_add_set_not_prat_set 1);
by (rtac preal_add_set_lemma3 1);
by (rtac preal_add_set_lemma4 1);
qed "preal_mem_add_set";

Goalw [preal_add_def] "((x::preal) + y) + z = x + (y + z)";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (simp_tac (simpset() addsimps [preal_mem_add_set RS Abs_preal_inverse]) 1); 
by (auto_tac (claset(),simpset() addsimps prat_add_ac));
by (rtac bexI 1);
by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_add_ac));
qed "preal_add_assoc";

Goal "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)";
by(rtac ([preal_add_assoc,preal_add_commute] MRS
         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "preal_add_left_commute";

(* Positive Reals addition is an AC operator *)
bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]);

  (*** Properties of multiplication ***)

(** Proofs essentially same as for addition **)

Goalw [preal_mult_def] "(x::preal) * y = y * x";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (blast_tac (claset() addIs [prat_mult_commute RS subst]) 1);
qed "preal_mult_commute";

(** multiplication of two positive reals gives a positive real **)
(** lemmas for proving positive reals multiplication set in preal **)

(** Part 1 of Dedekind sections def **)
Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
by (auto_tac (claset() addSIs [psubsetI], simpset()));
qed "preal_mult_set_not_empty";

(** Part 2 of Dedekind sections def **)
Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
by (REPEAT(etac exE 1));
by (REPEAT(dtac not_in_preal_ub 1));
by (res_inst_tac [("x","x*xa")] exI 1);
by (Auto_tac  THEN (REPEAT(etac ballE 1)) THEN Auto_tac );
by (dtac prat_mult_less_mono 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_mult_set_Ex";

Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
by Auto_tac;
qed "preal_mult_set_not_prat_set";

(** Part 3 of Dedekind sections def **)
Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x * y}";
by Auto_tac;
by (forw_inst_tac [("x","qinv(ya)"),("q1.0","z")] 
    prat_mult_left_less2_mono1 1);
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
by (dtac (Rep_preal RS prealE_lemma3a) 1);
by (etac allE 1);
by (REPEAT(rtac bexI 1));
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
qed "preal_mult_set_lemma3";

Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. y < u";
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset() addIs [prat_mult_less2_mono1],simpset()));
qed "preal_mult_set_lemma4";

Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y} : preal";
by (rtac prealI2 1);
by (rtac preal_mult_set_not_empty 1);
by (rtac preal_mult_set_not_prat_set 1);
by (rtac preal_mult_set_lemma3 1);
by (rtac preal_mult_set_lemma4 1);
qed "preal_mem_mult_set";

Goalw [preal_mult_def] "((x::preal) * y) * z = x * (y * z)";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (simp_tac (simpset() addsimps [preal_mem_mult_set RS Abs_preal_inverse]) 1);
by (auto_tac (claset(),simpset() addsimps prat_mult_ac));
by (rtac bexI 1);
by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_mult_ac));
qed "preal_mult_assoc";

Goal "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)";
by(rtac ([preal_mult_assoc,preal_mult_commute] MRS
         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "preal_mult_left_commute";

(* Positive Reals multiplication is an AC operator *)
bind_thms ("preal_mult_ac", [preal_mult_assoc, 
                     preal_mult_commute, 
                     preal_mult_left_commute]);

(* Positive Real 1 is the multiplicative identity element *) 
(* long *)
Goalw [preal_of_prat_def,preal_mult_def] 
      "(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) * z = z";
by (rtac (Rep_preal_inverse RS subst) 1);
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
by (auto_tac(claset(),simpset() addsimps [Rep_preal_inverse]));
by (EVERY1[dtac (Rep_preal RS prealE_lemma4a),etac bexE]);
by (dtac prat_mult_less_mono 1);
by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3a],simpset()));
by (EVERY1[forward_tac [Rep_preal RS prealE_lemma4a],etac bexE]);
by (forw_inst_tac [("x","qinv(u)"),("q1.0","x")] 
    prat_mult_less2_mono1 1);
by (rtac exI 1 THEN Auto_tac THEN res_inst_tac [("x","u")] bexI 1);
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
qed "preal_mult_1";

Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) = z";
by (rtac (preal_mult_commute RS subst) 1);
by (rtac preal_mult_1 1);
qed "preal_mult_1_right";

(** Lemmas **)

Goal "(z::preal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
qed "preal_add_assoc_cong";

Goal "(z::preal) + (v + w) = v + (z + w)";
by (REPEAT (ares_tac [preal_add_commute RS preal_add_assoc_cong] 1));
qed "preal_add_assoc_swap";

(** Distribution of multiplication across addition **)
(** lemmas for the proof **)

 (** lemmas **)
Goalw [preal_add_def] 
      "z: Rep_preal(R+S) ==> \
\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y";
by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_addD";

Goalw [preal_add_def] 
      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y \
\      ==> z: Rep_preal(R+S)";
by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_addI";

Goal "(z: Rep_preal(R+S)) = (EX x: Rep_preal(R). \
\                                 EX y: Rep_preal(S). z = x + y)";
by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
qed "mem_Rep_preal_add_iff";

Goalw [preal_mult_def] 
      "z: Rep_preal(R*S) ==> \
\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y";
by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_multD";

Goalw [preal_mult_def] 
      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y \
\      ==> z: Rep_preal(R*S)";
by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_multI";

Goal "(z: Rep_preal(R*S)) = (EX x: Rep_preal(R). \
\                                 EX y: Rep_preal(S). z = x * y)";
by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
qed "mem_Rep_preal_mult_iff";

(** More lemmas for preal_add_mult_distrib2 **)

Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
\                  Rep_preal w; yb: Rep_preal w |] ==> \
\                  xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
qed "lemma_add_mult_mem_Rep_preal";

Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
\                  Rep_preal w; yb: Rep_preal w |] ==> \
\                  yb*(xb + xc): Rep_preal (w*(z1 + z2))";
by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
qed "lemma_add_mult_mem_Rep_preal1";

Goal "x: Rep_preal (w * z1 + w * z2) ==> \
\              x: Rep_preal (w * (z1 + z2))";
by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD],
              simpset()));
by (forw_inst_tac [("ya","xa"),("yb","xb"),("xb","ya"),("xc","yb")] 
                                   lemma_add_mult_mem_Rep_preal1 1);
by Auto_tac;
by (res_inst_tac [("q1.0","xa"),("q2.0","xb")] prat_linear_less2 1);
by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1);
by (rtac (Rep_preal RS prealE_lemma3b) 1);
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2]));
by (dres_inst_tac [("ya","xb"),("yb","xa"),("xc","ya"),("xb","yb")] 
                                   lemma_add_mult_mem_Rep_preal1 1);
by Auto_tac;
by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1);
by (rtac (Rep_preal RS prealE_lemma3b) 1);
by (thin_tac "xb * ya + xb * yb  : Rep_preal (w * (z1 + z2))" 1);
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib,
              prat_add_commute] @ preal_add_ac ));
qed "lemma_preal_add_mult_distrib";

Goal "x: Rep_preal (w * (z1 + z2)) ==> \
\              x: Rep_preal (w * z1 + w * z2)";
by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD]
              addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI],
              simpset() addsimps [prat_add_mult_distrib2]));
qed "lemma_preal_add_mult_distrib2";

Goal "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)";
by (rtac (inj_Rep_preal RS injD) 1);
by (fast_tac (claset() addIs [lemma_preal_add_mult_distrib,
                              lemma_preal_add_mult_distrib2]) 1);
qed "preal_add_mult_distrib2";

Goal "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)";
by (simp_tac (simpset() addsimps [preal_mult_commute,
                                  preal_add_mult_distrib2]) 1);
qed "preal_add_mult_distrib";

(*** Prove existence of inverse ***)
(*** Inverse is a positive real ***)

Goal "EX y. qinv(y) ~:  Rep_preal X";
by (cut_inst_tac [("X","X")] not_mem_Rep_preal_Ex 1);
by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
by Auto_tac;
qed "qinv_not_mem_Rep_preal_Ex";

Goal "EX q. q: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
by (cut_inst_tac [("X","A")] qinv_not_mem_Rep_preal_Ex 1);
by Auto_tac;
by (cut_inst_tac [("y","y")] qless_Ex 1);
by (Fast_tac 1);
qed "lemma_preal_mem_inv_set_ex";

(** Part 1 of Dedekind sections def **)
Goal "{} < {x. EX y. x < y & qinv y ~:  Rep_preal A}";
by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
by (auto_tac (claset() addSIs [psubsetI], simpset()));
qed "preal_inv_set_not_empty";

(** Part 2 of Dedekind sections def **)
Goal "EX y. qinv(y) :  Rep_preal X";
by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
by Auto_tac;
qed "qinv_mem_Rep_preal_Ex";

Goal "EX x. x ~: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
by (rtac ccontr 1);
by (cut_inst_tac [("X","A")] qinv_mem_Rep_preal_Ex 1);
by Auto_tac;
by (EVERY1[etac allE, etac exE, etac conjE]);
by (dtac qinv_prat_less 1 THEN dtac not_in_preal_ub 1);
by (eres_inst_tac [("x","qinv y")] ballE 1);
by (dtac prat_less_trans 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_inv_set_Ex";

Goal "{x. EX y. x < y & qinv y ~:  Rep_preal A} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
by Auto_tac;
qed "preal_inv_set_not_prat_set";

(** Part 3 of Dedekind sections def **)
Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
 \      ALL z. z < y --> z : {x. EX y. x < y & qinv y ~: Rep_preal A}";
by Auto_tac;
by (res_inst_tac [("x","ya")] exI 1);
by (auto_tac (claset() addIs [prat_less_trans],simpset()));
qed "preal_inv_set_lemma3";

Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
\       Bex {x. EX y. x < y & qinv y ~: Rep_preal A} (op < y)";
by (blast_tac (claset() addDs [prat_dense]) 1);
qed "preal_inv_set_lemma4";

Goal "{x. EX y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
by (rtac prealI2 1);
by (rtac preal_inv_set_not_empty 1);
by (rtac preal_inv_set_not_prat_set 1);
by (rtac preal_inv_set_lemma3 1);
by (rtac preal_inv_set_lemma4 1);
qed "preal_mem_inv_set";

(*more lemmas for inverse *)
Goal "x: Rep_preal(pinv(A)*A) ==> \
\     x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))";
by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
              simpset() addsimps [pinv_def,preal_of_prat_def] ));
by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
by (auto_tac (claset() addSDs [not_in_preal_ub],simpset()));
by (dtac prat_mult_less_mono 1 THEN Blast_tac 1);
by (auto_tac (claset(),simpset()));
qed "preal_mem_mult_invD";

(*** Gleason's Lemma 9-3.4 p 122 ***)
Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
\            EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
by (cut_facts_tac [mem_Rep_preal_Ex] 1);
by (induct_thm_tac pnat_induct "p" 1);
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
    pSuc_is_plus_one,prat_add_mult_distrib,
   prat_of_pnat_add,prat_add_assoc RS sym]));
qed "lemma1_gleason9_34";

Goal "Abs_prat (ratrel `` {(y, z)}) < xb + \
\         Abs_prat (ratrel `` {(x*y, Abs_pnat (Suc 0))})*Abs_prat (ratrel `` {(w, x)})";
by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat (Suc 0))}) *\
\                   Abs_prat (ratrel `` {(w, x)})")] prat_le_less_trans 1);
by (rtac prat_self_less_add_right 2);
by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
    simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
qed "lemma1b_gleason9_34";

Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
by (dtac not_in_preal_ub 1);
by (res_inst_tac [("z","x")] eq_Abs_prat 1);
by (res_inst_tac [("z","xa")] eq_Abs_prat 1);
by (dres_inst_tac [("p","y*xb")] lemma1_gleason9_34 1);
by (etac bexE 1);
by (cut_inst_tac [("x","y"),("y","xb"),("w","xaa"),
    ("z","ya"),("xb","xba")] lemma1b_gleason9_34 1);
by (dres_inst_tac [("x","xba + prat_of_pnat (y * xb) * x")]  bspec 1);
by (auto_tac (claset() addIs [prat_less_asym],
    simpset() addsimps [prat_of_pnat_def]));
qed "lemma_gleason9_34a";

Goal "EX r: Rep_preal(R). r + x ~: Rep_preal(R)";
by (rtac ccontr 1);
by (blast_tac (claset() addIs [lemma_gleason9_34a]) 1);
qed "lemma_gleason9_34";

(*** Gleason's Lemma 9-3.6  ***)
(*  lemmas for Gleason 9-3.6  *)
(*                            *) 
(******************************)

Goal "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)";
by (full_simp_tac (simpset() addsimps [prat_add_mult_distrib2,
    prat_mult_assoc]) 1);
qed "lemma1_gleason9_36";

Goal "r*qinv(xa)*(xa*x) = r*x";
by (full_simp_tac (simpset() addsimps prat_mult_ac) 1);
qed "lemma2_gleason9_36";
(******)

(*** FIXME: long! ***)
Goal "prat_of_pnat 1 < x ==> EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
by (Fast_tac 1);
by (dres_inst_tac [("x","xa")] prat_self_less_mult_right 1);
by (etac prat_lessE 1);
by (cut_inst_tac [("R","A"),("x","Q3")] lemma_gleason9_34 1);
by (dtac sym 1 THEN Auto_tac );
by (ftac not_in_preal_ub 1);
by (dres_inst_tac [("x","xa + Q3")] bspec 1 THEN assume_tac 1);
by (dtac prat_add_right_less_cancel 1);
by (dres_inst_tac [("x","qinv(xa)*Q3")] prat_mult_less2_mono1 1);
by (dres_inst_tac [("x","r")] prat_add_less2_mono2 1);
by (asm_full_simp_tac (simpset() addsimps
    [prat_mult_assoc RS sym,lemma1_gleason9_36]) 1);
by (dtac sym 1);
by (auto_tac (claset(),simpset() addsimps [lemma2_gleason9_36]));
by (res_inst_tac [("x","r")] bexI 1);
by (rtac notI 1);
by (dres_inst_tac [("y","r*x")] (Rep_preal RS prealE_lemma3b) 1);
by Auto_tac;
qed "lemma_gleason9_36";

Goal "prat_of_pnat (Abs_pnat (Suc 0)) < x ==> \
\     EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (rtac lemma_gleason9_36 1);
by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
qed "lemma_gleason9_36a";

(*** Part 2 of existence of inverse ***)
Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) \
\     ==> x: Rep_preal(pinv(A)*A)";
by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
              simpset() addsimps [pinv_def,preal_of_prat_def] ));
by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
by (dtac prat_qinv_gt_1 1);
by (dres_inst_tac [("A","A")] lemma_gleason9_36a 1);
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (Auto_tac  THEN dtac qinv_prat_less 1);
by (res_inst_tac [("x","qinv(u)*x")] exI 1);
by (rtac conjI 1);
by (res_inst_tac [("x","qinv(r)*x")] exI 1);
by (auto_tac (claset() addIs [prat_mult_less2_mono1],
    simpset() addsimps [qinv_mult_eq,qinv_qinv]));
by (res_inst_tac [("x","u")] bexI 1);
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc,
    prat_mult_left_commute]));
qed "preal_mem_mult_invI";

Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))";
by (rtac (inj_Rep_preal RS injD) 1);
by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
qed "preal_mult_inv";

Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))";
by (rtac (preal_mult_commute RS subst) 1);
by (rtac preal_mult_inv 1);
qed "preal_mult_inv_right";

val [prem] = Goal
    "(!!u. z = Abs_preal(u) ==> P) ==> P";
by (cut_inst_tac [("x1","z")] 
    (rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1);
by (res_inst_tac [("u","Rep_preal z")] prem 1);
by (dtac (inj_Rep_preal RS injD) 1);
by (Asm_simp_tac 1);
qed "eq_Abs_preal";

(*** Lemmas/Theorem(s) need lemma_gleason9_34 ***)
Goal "Rep_preal (R1) <= Rep_preal(R1 + R2)";
by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
by (auto_tac (claset() addSIs [bexI] addIs [(Rep_preal RS prealE_lemma3b),
   prat_self_less_add_left,mem_Rep_preal_addI],simpset()));
qed "Rep_preal_self_subset";

Goal "~ Rep_preal (R1 + R2) <= Rep_preal(R1)";
by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
by (etac exE 1);
by (cut_inst_tac [("R","R1")] lemma_gleason9_34 1);
by (auto_tac (claset() addIs [mem_Rep_preal_addI],simpset()));
qed "Rep_preal_sum_not_subset";

Goal "Rep_preal (R1 + R2) ~= Rep_preal(R1)";
by (rtac notI 1);
by (etac equalityE 1);
by (asm_full_simp_tac (simpset() addsimps [Rep_preal_sum_not_subset]) 1);
qed "Rep_preal_sum_not_eq";

(*** at last --- Gleason prop. 9-3.5(iii) p. 123 ***)
Goalw [preal_less_def,psubset_def] "(R1::preal) < R1 + R2";
by (simp_tac (simpset() addsimps [Rep_preal_self_subset,
    Rep_preal_sum_not_eq RS not_sym]) 1);
qed "preal_self_less_add_left";

Goal "(R1::preal) < R2 + R1";
by (simp_tac (simpset() addsimps [preal_add_commute,preal_self_less_add_left]) 1);
qed "preal_self_less_add_right";

(*** Properties of <= ***)

Goalw [preal_le_def,psubset_def,preal_less_def] 
                     "z<=w ==> ~(w<(z::preal))";
by (auto_tac  (claset() addDs [equalityI],simpset()));
qed "preal_leD";

bind_thm ("preal_leE", make_elim preal_leD);

Goalw [preal_le_def,psubset_def,preal_less_def]
                   "~ z <= w ==> w<(z::preal)";
by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
by (auto_tac  (claset(),simpset() addsimps [preal_less_def,psubset_def]));
qed "not_preal_leE";
		       
Goal "~(w < z) ==> z <= (w::preal)";
by (fast_tac (claset() addIs [not_preal_leE]) 1);
qed "preal_leI";

Goal "(~(w < z)) = (z <= (w::preal))";
by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1);
qed "preal_less_le_iff";

Goalw [preal_le_def,preal_less_def,psubset_def] 
     "z < w ==> z <= (w::preal)";
by (Fast_tac 1);
qed "preal_less_imp_le";

Goalw [preal_le_def,preal_less_def,psubset_def] 
     "!!(x::preal). x <= y ==> x < y | x = y";
by (auto_tac (claset() addIs [inj_Rep_preal RS injD],simpset()));
qed "preal_le_imp_less_or_eq";

Goalw [preal_le_def,preal_less_def,psubset_def] 
     "!!(x::preal). x < y | x = y ==> x <=y";
by Auto_tac;
qed "preal_less_or_eq_imp_le";

Goalw [preal_le_def] "w <= (w::preal)";
by (Simp_tac 1);
qed "preal_le_refl";

Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
          rtac preal_less_or_eq_imp_le, 
                 fast_tac (claset() addIs [preal_less_trans])]);
qed "preal_le_trans";

Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
            fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
qed "preal_le_anti_sym";

Goal "!!w::preal. (w ~= z) = (w<z | z<w)";
by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
by (auto_tac (claset() addEs [preal_less_irrefl], simpset()));
qed "preal_neq_iff";

(* Axiom 'order_less_le' of class 'order': *)
Goal "((w::preal) < z) = (w <= z & w ~= z)";
by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
by (blast_tac (claset() addSEs [preal_less_asym]) 1);
qed "preal_less_le";


(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)

(**** Set up all lemmas for proving A < B ==> ?D. A + D = B ****)
(**** Gleason prop. 9-3.5(iv) p. 123 ****)
(**** Define the D required and show that it is a positive real ****)

(* useful lemmas - proved elsewhere? *)
Goalw [psubset_def] "A < B ==> EX x. x ~: A & x : B";
by Auto_tac;
qed "lemma_psubset_mem";

Goalw [psubset_def] "~ (A::'a set) < A";
by (Fast_tac 1);
qed "lemma_psubset_not_refl";

Goalw [psubset_def] "!!(A::'a set). [| A < B; B < C |] ==> A < C";
by (auto_tac (claset() addDs [subset_antisym],simpset()));
qed "psubset_trans";

Goalw [psubset_def] "!!(A::'a set). [| A <= B; B < C |] ==> A < C";
by (auto_tac (claset() addDs [subset_antisym],simpset()));
qed "subset_psubset_trans";

Goalw [psubset_def] "!!(A::'a set). [| A < B; B <= C |] ==> A < C";
by (auto_tac (claset() addDs [subset_antisym],simpset()));
qed "subset_psubset_trans2";

Goalw [psubset_def] "!!(A::'a set). [| A < B; c : A |] ==> c : B";
by (auto_tac (claset() addDs [subsetD],simpset()));
qed "psubsetD";

(** Part 1 of Dedekind sections def **)
Goalw [preal_less_def]
     "A < B ==> \
\     EX q. q : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
qed "lemma_ex_mem_less_left_add1";

Goal "A < B ==> {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (dtac lemma_ex_mem_less_left_add1 1);
by (auto_tac (claset() addSIs [psubsetI], simpset()));
qed "preal_less_set_not_empty";

(** Part 2 of Dedekind sections def **)
Goal "EX q. q ~: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (cut_inst_tac [("X","B")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
by (res_inst_tac [("x","x")] exI 1);
by Auto_tac;
by (cut_inst_tac [("x","x"),("y","n")] prat_self_less_add_right 1);
by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
qed "lemma_ex_not_mem_less_left_add1";

Goal "{d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
by Auto_tac;
qed "preal_less_set_not_prat_set";

(** Part 3 of Dedekind sections def **)
Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
 \   ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by Auto_tac;
by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
by (dtac (Rep_preal RS prealE_lemma3b) 1);
by Auto_tac;
qed "preal_less_set_lemma3";

Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
\       Bex {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_def,prat_add_assoc]));
qed "preal_less_set_lemma4";

Goal 
     "!! (A::preal). A < B ==> \
\     {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
by (rtac prealI2 1);
by (rtac preal_less_set_not_empty 1);
by (rtac preal_less_set_not_prat_set 2);
by (rtac preal_less_set_lemma3 2);
by (rtac preal_less_set_lemma4 3);
by Auto_tac;
qed "preal_mem_less_set";

(** proving that A + D <= B **)
Goalw [preal_le_def] 
       "!! (A::preal). A < B ==> \
\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
by (rtac subsetI 1);
by (dtac mem_Rep_preal_addD 1);
by (auto_tac (claset(),simpset() addsimps [
    preal_mem_less_set RS Abs_preal_inverse]));
by (dtac not_in_preal_ub 1);
by (dtac bspec 1 THEN assume_tac 1);
by (dres_inst_tac [("x","y")] prat_add_less2_mono1 1);
by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma3b) 1);
by Auto_tac;
qed "preal_less_add_left_subsetI";

(** proving that B <= A + D  --- trickier **)
(** lemma **)
Goal "x : Rep_preal(B) ==> EX e. x + e : Rep_preal(B)";
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
qed "lemma_sum_mem_Rep_preal_ex";

Goalw [preal_le_def] 
       "!! (A::preal). A < B ==> \
\         B <= A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
by (rtac subsetI 1);
by (res_inst_tac [("Q","x: Rep_preal(A)")] (excluded_middle RS disjE) 1);
by (rtac mem_Rep_preal_addI 1);
by (dtac lemma_sum_mem_Rep_preal_ex 1);
by (etac exE 1);
by (cut_inst_tac [("R","A"),("x","e")] lemma_gleason9_34 1 THEN etac bexE 1);
by (dtac not_in_preal_ub 1 THEN dtac bspec 1 THEN assume_tac 1);
by (etac prat_lessE 1);
by (res_inst_tac [("x","r")] bexI 1);
by (res_inst_tac [("x","Q3")] bexI 1);
by (cut_facts_tac [Rep_preal_self_subset] 4);
by (auto_tac (claset(),simpset() addsimps [
    preal_mem_less_set RS Abs_preal_inverse]));
by (res_inst_tac [("x","r+e")] exI 1);
by (asm_full_simp_tac (simpset() addsimps prat_add_ac) 1);
qed "preal_less_add_left_subsetI2";

(*** required proof ***)
Goal "!! (A::preal). A < B ==> \
\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
by (blast_tac (claset() addIs [preal_le_anti_sym,
                preal_less_add_left_subsetI,preal_less_add_left_subsetI2]) 1);
qed "preal_less_add_left";

Goal "!! (A::preal). A < B ==> EX D. A + D = B";
by (fast_tac (claset() addDs [preal_less_add_left]) 1);
qed "preal_less_add_left_Ex";        

Goal "!!(A::preal). A < B ==> A + C < B + C";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
    simpset() addsimps [preal_add_assoc]));
by (res_inst_tac [("y1","D")] (preal_add_commute RS subst) 1);
by (auto_tac (claset() addIs [preal_self_less_add_left],
          simpset() addsimps [preal_add_assoc RS sym]));
qed "preal_add_less2_mono1";

Goal "!!(A::preal). A < B ==> C + A < C + B";
by (auto_tac (claset() addIs [preal_add_less2_mono1],
    simpset() addsimps [preal_add_commute]));
qed "preal_add_less2_mono2";

Goal 
      "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x";
by (dtac preal_less_add_left_Ex 1);
by (auto_tac (claset(),simpset() addsimps [preal_add_mult_distrib,
    preal_self_less_add_left]));
qed "preal_mult_less_mono1";

Goal "!!(q1::preal). q1 < q2  ==> x * q1 < x * q2";
by (auto_tac (claset() addDs [preal_mult_less_mono1],
    simpset() addsimps [preal_mult_commute]));
qed "preal_mult_left_less_mono1";

Goal "!!(q1::preal). q1 <= q2  ==> x * q1 <= x * q2";
by (dtac preal_le_imp_less_or_eq 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [preal_le_refl,
    preal_less_imp_le,preal_mult_left_less_mono1],simpset()));
qed "preal_mult_left_le_mono1";
 
Goal "!!(q1::preal). q1 <= q2  ==> q1 * x <= q2 * x";
by (auto_tac (claset() addDs [preal_mult_left_le_mono1],
    simpset() addsimps [preal_mult_commute]));
qed "preal_mult_le_mono1";
 
Goal "!!(q1::preal). q1 <= q2  ==> x + q1 <= x + q2";
by (dtac preal_le_imp_less_or_eq 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [preal_le_refl,
                               preal_less_imp_le,preal_add_less2_mono1],
              simpset() addsimps [preal_add_commute]));
qed "preal_add_left_le_mono1";

Goal "!!(q1::preal). q1 <= q2  ==> q1 + x <= q2 + x";
by (auto_tac (claset() addDs [preal_add_left_le_mono1],
    simpset() addsimps [preal_add_commute]));
qed "preal_add_le_mono1";
 
Goal "!!(A::preal). A + C < B + C ==> A < B";
by (cut_facts_tac [preal_linear] 1);
by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
by (dres_inst_tac [("A","B"),("C","C")] preal_add_less2_mono1 1);
by (fast_tac (claset() addDs [preal_less_trans] 
                addEs [preal_less_irrefl]) 1);
qed "preal_add_right_less_cancel";

Goal "!!(A::preal). C + A < C + B ==> A < B";
by (auto_tac (claset() addEs [preal_add_right_less_cancel],
              simpset() addsimps [preal_add_commute]));
qed "preal_add_left_less_cancel";

Goal "((A::preal) + C < B + C) = (A < B)";
by (REPEAT(ares_tac [iffI,preal_add_less2_mono1,
    preal_add_right_less_cancel] 1));
qed "preal_add_less_iff1";

Addsimps [preal_add_less_iff1];

Goal "(C + (A::preal) < C + B) = (A < B)";
by (REPEAT(ares_tac [iffI,preal_add_less2_mono2,
    preal_add_left_less_cancel] 1));
qed "preal_add_less_iff2";

Addsimps [preal_add_less_iff2];

Goal "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
    simpset() addsimps  preal_add_ac));
by (rtac (preal_add_assoc RS subst) 1);
by (rtac preal_self_less_add_right 1);
qed "preal_add_less_mono";

Goal "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
              simpset() addsimps [preal_add_mult_distrib,
              preal_add_mult_distrib2,preal_self_less_add_left,
              preal_add_assoc] @ preal_mult_ac));
qed "preal_mult_less_mono";

Goal "!!(A::preal). A + C = B + C ==> A = B";
by (cut_facts_tac [preal_linear] 1);
by Auto_tac;
by (ALLGOALS(dres_inst_tac [("C","C")] preal_add_less2_mono1));
by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
qed "preal_add_right_cancel";

Goal "!!(A::preal). C + A = C + B ==> A = B";
by (auto_tac (claset() addIs [preal_add_right_cancel],
              simpset() addsimps [preal_add_commute]));
qed "preal_add_left_cancel";

Goal "(C + A = C + B) = ((A::preal) = B)";
by (fast_tac (claset() addIs [preal_add_left_cancel]) 1);
qed "preal_add_left_cancel_iff";

Goal "(A + C = B + C) = ((A::preal) = B)";
by (fast_tac (claset() addIs [preal_add_right_cancel]) 1);
qed "preal_add_right_cancel_iff";

Addsimps [preal_add_left_cancel_iff,preal_add_right_cancel_iff];

(*** Completeness of preal ***)

(*** prove that supremum is a cut ***)
Goal "EX (X::preal). X: P ==> \
\         EX q.  q: {w. EX X. X : P & w : Rep_preal X}";
by Safe_tac;
by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
by Auto_tac;
qed "preal_sup_mem_Ex";

(** Part 1 of Dedekind def **)
Goal "EX (X::preal). X: P ==> \
\         {} < {w. EX X : P. w : Rep_preal X}";
by (dtac preal_sup_mem_Ex 1);
by (auto_tac (claset() addSIs [psubsetI], simpset()));
qed "preal_sup_set_not_empty";

(** Part 2 of Dedekind sections def **) 
Goalw [preal_less_def] "EX Y. (ALL X: P. X < Y)  \             
\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}"; (**)
by (auto_tac (claset(),simpset() addsimps [psubset_def]));
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
by (res_inst_tac [("x","x")] exI 1);
by (auto_tac (claset() addSDs [bspec],simpset()));
qed "preal_sup_not_mem_Ex";

Goalw [preal_le_def] "EX Y. (ALL X: P. X <= Y)  \
\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}";
by (Step_tac 1);
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
by (res_inst_tac [("x","x")] exI 1);
by (auto_tac (claset() addSDs [bspec],simpset()));
qed "preal_sup_not_mem_Ex1";

Goal "EX Y. (ALL X: P. X < Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; (**)
by (dtac preal_sup_not_mem_Ex 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
qed "preal_sup_set_not_prat_set";

Goal "EX Y. (ALL X: P. X <= Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
by (dtac preal_sup_not_mem_Ex1 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
qed "preal_sup_set_not_prat_set1";

(** Part 3 of Dedekind sections def **)
Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";         (**)
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b], simpset()));
qed "preal_sup_set_lemma3";

Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
qed "preal_sup_set_lemma3_1";

Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \                        
\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";                (**)
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
qed "preal_sup_set_lemma4";

Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \
\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
qed "preal_sup_set_lemma4_1";

Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \            
\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";                      (**)
by (rtac prealI2 1);
by (rtac preal_sup_set_not_empty 1);
by (rtac preal_sup_set_not_prat_set 2);
by (rtac preal_sup_set_lemma3 3);
by (rtac preal_sup_set_lemma4 5);
by Auto_tac;
qed "preal_sup";

Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";
by (rtac prealI2 1);
by (rtac preal_sup_set_not_empty 1);
by (rtac preal_sup_set_not_prat_set1 2);
by (rtac preal_sup_set_lemma3_1 3);
by (rtac preal_sup_set_lemma4_1 5);
by Auto_tac;
qed "preal_sup1";

Goalw [psup_def] "EX Y. (ALL X:P. X < Y) ==> ALL x: P. x <= psup P";      (**) 
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
by Auto_tac;
qed "preal_psup_leI";

Goalw [psup_def] "EX Y. (ALL X:P. X <= Y) ==> ALL x: P. x <= psup P";
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
qed "preal_psup_leI2";

Goal "[| EX Y. (ALL X:P. X < Y); x : P |] ==> x <= psup P";              (**)
by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
qed "preal_psup_leI2b";

Goal "[| EX Y. (ALL X:P. X <= Y); x : P |] ==> x <= psup P";
by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
qed "preal_psup_leI2a";

Goalw [psup_def] "[| EX X. X : P; ALL X:P. X < Y |] ==> psup P <= Y";   (**)
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
by (rotate_tac 1 2);
by (assume_tac 2);
by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
qed "psup_le_ub";

Goalw [psup_def] "[| EX X. X : P; ALL X:P. X <= Y |] ==> psup P <= Y";
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
by (rotate_tac 1 2);
by (assume_tac 2);
by (auto_tac (claset() addSDs [bspec],
    simpset() addsimps [preal_less_def,psubset_def,preal_le_def]));
qed "psup_le_ub1";

(** supremum property **)
Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \                  
\         ==> (ALL Y. (EX X: P. Y < X) = (Y < psup P))";              
by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
by (Fast_tac 1);
by (auto_tac (claset(), simpset() addsimps [psup_def,preal_less_def]));
by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1);
by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def]));
qed "preal_complete";

(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
    (****** Embedding ******)
(*** mapping from prat into preal ***)

Goal "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1);
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
qed "lemma_preal_rat_less";

Goal "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
by (stac prat_add_commute 1);
by (dtac (prat_add_commute RS subst) 1);
by (etac lemma_preal_rat_less 1);
qed "lemma_preal_rat_less2";

Goalw [preal_of_prat_def,preal_add_def] 
      "preal_of_prat ((z1::prat) + z2) = \
\      preal_of_prat z1 + preal_of_prat z2";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (auto_tac (claset() addIs [prat_add_less_mono],
     simpset() addsimps [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
by (res_inst_tac [("x","x*z1*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
by (etac lemma_preal_rat_less 1);
by (res_inst_tac [("x","x*z2*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
by (etac lemma_preal_rat_less2 1);
by (asm_full_simp_tac (simpset() addsimps [prat_add_mult_distrib RS sym,
     prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
qed "preal_of_prat_add";

Goal "x < xa ==> x*z1*qinv(xa) < z1";
by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
by (dtac (prat_mult_left_commute RS subst) 1);
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
qed "lemma_preal_rat_less3";

Goal "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1);
by (dtac (prat_mult_left_commute RS subst) 1);
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
qed "lemma_preal_rat_less4";

Goalw [preal_of_prat_def,preal_mult_def] 
      "preal_of_prat ((z1::prat) * z2) = \
\      preal_of_prat z1 * preal_of_prat z2";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (auto_tac (claset() addIs [prat_mult_less_mono],
     simpset() addsimps [lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
by (dtac prat_dense 1);
by (Step_tac 1);
by (res_inst_tac [("x","x*z1*qinv(xa)")] exI 1 THEN rtac conjI 1);
by (etac lemma_preal_rat_less3 1);
by (res_inst_tac [("x"," xa*z2*qinv(z1*z2)")] exI 1 THEN rtac conjI 1);
by (etac lemma_preal_rat_less4 1);
by (asm_full_simp_tac (simpset() 
    addsimps [qinv_mult_eq RS sym] @ prat_mult_ac) 1);
by (asm_full_simp_tac (simpset() 
    addsimps [prat_mult_assoc RS sym]) 1);
qed "preal_of_prat_mult";

Goalw [preal_of_prat_def,preal_less_def] 
      "(preal_of_prat p < preal_of_prat q) = (p < q)";
by (auto_tac (claset() addSDs [lemma_prat_set_eq] addEs [prat_less_trans],
              simpset() addsimps [lemma_prat_less_set_mem_preal,
                                  psubset_def,prat_less_not_refl]));
by (res_inst_tac [("q1.0","p"),("q2.0","q")] prat_linear_less2 1);
by (auto_tac (claset() addIs [prat_less_irrefl],simpset()));
qed "preal_of_prat_less_iff";

Addsimps [preal_of_prat_less_iff];