# HG changeset patch
# User paulson
# Date 964002799 -7200
# Node ID a6ab3a442da614873627a4d2a4efcf544a5a8eaa
# Parent  e6b96d953965b43bf38744670d29fcbc8e116c3b
changed / to // for quotienting; general tidying

diff -r e6b96d953965 -r a6ab3a442da6 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jul 19 12:33:19 2000 +0200
@@ -107,8 +107,7 @@
 qed "FreeUltrafilterNat_UNIV";
 Addsimps [FreeUltrafilterNat_UNIV];
 
-Goal "{n::nat. True}: FreeUltrafilterNat";
-by (subgoal_tac "{n::nat. True} = (UNIV::nat set)" 1);
+Goal "UNIV : FreeUltrafilterNat";
 by Auto_tac;
 qed "FreeUltrafilterNat_Nat_set";
 Addsimps [FreeUltrafilterNat_Nat_set];
@@ -202,18 +201,16 @@
 by (Ultra_tac 1);
 qed_spec_mp "hyprel_trans";
 
-Goalw [equiv_def, refl_def, sym_def, trans_def]
-    "equiv {x::nat=>real. True} hyprel";
+Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV hyprel";
 by (auto_tac (claset() addSIs [hyprel_refl] 
                        addSEs [hyprel_sym,hyprel_trans] 
                        delrules [hyprelI,hyprelE],
 	      simpset() addsimps [FreeUltrafilterNat_Nat_set]));
 qed "equiv_hyprel";
 
+(* (hyprel ^^ {x} = hyprel ^^ {y}) = ((x,y) : hyprel) *)
 bind_thm ("equiv_hyprel_iff",
-    [TrueI, TrueI] MRS 
-    ([CollectI, CollectI] MRS 
-    (equiv_hyprel RS eq_equiv_class_iff)));
+    	  [equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
 
 Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal";
 by (Blast_tac 1);
@@ -288,14 +285,12 @@
 by (ALLGOALS Ultra_tac);
 qed "hypreal_minus_congruent";
 
-(*Resolve th against the corresponding facts for hypreal_minus*)
-val hypreal_minus_ize = RSLIST [equiv_hyprel, hypreal_minus_congruent];
-
 Goalw [hypreal_minus_def]
       "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
-   [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_minus_ize UN_equiv_class]) 1);
+   [hyprel_in_hypreal RS Abs_hypreal_inverse,
+    [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1);
 qed "hypreal_minus";
 
 Goal "- (- z) = (z::hypreal)";
@@ -331,15 +326,13 @@
 by (Auto_tac THEN Ultra_tac 1);
 qed "hypreal_hrinv_congruent";
 
-(* Resolve th against the corresponding facts for hrinv *)
-val hypreal_hrinv_ize = RSLIST [equiv_hyprel, hypreal_hrinv_congruent];
-
 Goalw [hrinv_def]
       "hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
 \      Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else rinv(X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
-   [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
+   [hyprel_in_hypreal RS Abs_hypreal_inverse,
+    [equiv_hyprel, hypreal_hrinv_congruent] MRS UN_equiv_class]) 1);
 qed "hypreal_hrinv";
 
 Goal "z ~= 0 ==> hrinv (hrinv z) = z";
@@ -369,14 +362,11 @@
 by (ALLGOALS(Ultra_tac));
 qed "hypreal_add_congruent2";
 
-(*Resolve th against the corresponding facts for hyppreal_add*)
-val hypreal_add_ize = RSLIST [equiv_hyprel, hypreal_add_congruent2];
-
 Goalw [hypreal_add_def]
   "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
 \  Abs_hypreal(hyprel^^{%n. X n + Y n})";
-by (asm_simp_tac
-    (simpset() addsimps [hypreal_add_ize UN_equiv_class2]) 1);
+by (simp_tac (simpset() addsimps 
+         [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1);
 qed "hypreal_add";
 
 Goal "(z::hypreal) + w = w + z";
@@ -531,14 +521,11 @@
 by (ALLGOALS(Ultra_tac));
 qed "hypreal_mult_congruent2";
 
-(*Resolve th against the corresponding facts for hypreal_mult*)
-val hypreal_mult_ize = RSLIST [equiv_hyprel, hypreal_mult_congruent2];
-
 Goalw [hypreal_mult_def]
   "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
 \  Abs_hypreal(hyprel^^{%n. X n * Y n})";
-by (asm_simp_tac
-    (simpset() addsimps [hypreal_mult_ize UN_equiv_class2]) 1);
+by (simp_tac (simpset() addsimps 
+      [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1);
 qed "hypreal_mult";
 
 Goal "(z::hypreal) * w = w * z";
diff -r e6b96d953965 -r a6ab3a442da6 src/HOL/Real/Hyperreal/HyperDef.thy
--- a/src/HOL/Real/Hyperreal/HyperDef.thy	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.thy	Wed Jul 19 12:33:19 2000 +0200
@@ -22,7 +22,7 @@
     "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
                    {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
 
-typedef hypreal = "{x::nat=>real. True}/hyprel"   (Equiv.quotient_def)
+typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
 
 instance
    hypreal  :: {ord, zero, plus, times, minus}
diff -r e6b96d953965 -r a6ab3a442da6 src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/PRat.ML	Wed Jul 19 12:33:19 2000 +0200
@@ -451,7 +451,7 @@
 
 (* lemma for proving $< is linear *)
 Goalw [prat_def,prat_less_def] 
-      "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}/ratrel";
+      "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel";
 by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1);
 by (Blast_tac 1);
 qed "lemma_prat_less_linear";
diff -r e6b96d953965 -r a6ab3a442da6 src/HOL/Real/PRat.thy
--- a/src/HOL/Real/PRat.thy	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/PRat.thy	Wed Jul 19 12:33:19 2000 +0200
@@ -11,7 +11,7 @@
     ratrel   ::  "((pnat * pnat) * (pnat * pnat)) set"
     "ratrel  ==  {p. ? x1 y1 x2 y2. p=((x1::pnat,y1),(x2,y2)) & x1*y2 = x2*y1}" 
 
-typedef prat = "UNIV/ratrel"          (Equiv.quotient_def)
+typedef prat = "UNIV//ratrel"          (Equiv.quotient_def)
 
 instance
    prat  :: {ord,plus,times}
@@ -20,7 +20,7 @@
 constdefs
 
   prat_of_pnat :: pnat => prat           
-  "prat_of_pnat m     == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
+  "prat_of_pnat m == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
 
   qinv      :: prat => prat
   "qinv(Q)  == Abs_prat(UN (x,y):Rep_prat(Q). ratrel^^{(y,x)})" 
@@ -37,7 +37,7 @@
  
   (*** Gleason p. 119 ***)
   prat_less_def
-  "P < (Q::prat) == ? T. P + T = Q"
+  "P < (Q::prat) == EX T. P + T = Q"
 
   prat_le_def
   "P <= (Q::prat) == ~(Q < P)" 
diff -r e6b96d953965 -r a6ab3a442da6 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/RealDef.ML	Wed Jul 19 12:33:19 2000 +0200
@@ -52,16 +52,14 @@
 by (rtac refl 1);
 qed "realrel_refl";
 
-Goalw [equiv_def, refl_def, sym_def, trans_def]
-    "equiv {x::(preal*preal).True} realrel";
+Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV realrel";
 by (fast_tac (claset() addSIs [realrel_refl] 
-                      addSEs [sym,preal_trans_lemma]) 1);
+                       addSEs [sym, preal_trans_lemma]) 1);
 qed "equiv_realrel";
 
+(* (realrel ^^ {x} = realrel ^^ {y}) = ((x,y) : realrel) *)
 bind_thm ("equiv_realrel_iff",
-    [TrueI, TrueI] MRS 
-    ([CollectI, CollectI] MRS 
-    (equiv_realrel RS eq_equiv_class_iff)));
+    	  [equiv_realrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
 
 Goalw  [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
 by (Blast_tac 1);
@@ -114,14 +112,12 @@
 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
 qed "real_minus_congruent";
 
-(*Resolve th against the corresponding facts for real_minus*)
-val real_minus_ize = RSLIST [equiv_realrel, real_minus_congruent];
-
 Goalw [real_minus_def]
       "- (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})";
 by (res_inst_tac [("f","Abs_real")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
-   [realrel_in_real RS Abs_real_inverse,real_minus_ize UN_equiv_class]) 1);
+   [realrel_in_real RS Abs_real_inverse,
+    [equiv_realrel, real_minus_congruent] MRS UN_equiv_class]) 1);
 qed "real_minus";
 
 Goal "- (- z) = (z::real)";
@@ -162,13 +158,11 @@
 by (asm_simp_tac (simpset() addsimps preal_add_ac) 1);
 qed "real_add_congruent2";
 
-(*Resolve th against the corresponding facts for real_add*)
-val real_add_ize = RSLIST [equiv_realrel, real_add_congruent2];
-
 Goalw [real_add_def]
   "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \
 \  Abs_real(realrel^^{(x1+x2, y1+y2)})";
-by (asm_simp_tac (simpset() addsimps [real_add_ize UN_equiv_class2]) 1);
+by (simp_tac (simpset() addsimps 
+              [[equiv_realrel, real_add_congruent2] MRS UN_equiv_class2]) 1);
 qed "real_add";
 
 Goal "(z::real) + w = w + z";
@@ -329,13 +323,11 @@
 by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
 qed "real_mult_congruent2";
 
-(*Resolve th against the corresponding facts for real_mult*)
-val real_mult_ize = RSLIST [equiv_realrel, real_mult_congruent2];
-
 Goalw [real_mult_def]
    "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) =   \
 \   Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})";
-by (simp_tac (simpset() addsimps [real_mult_ize UN_equiv_class2]) 1);
+by (simp_tac (simpset() addsimps
+               [[equiv_realrel, real_mult_congruent2] MRS UN_equiv_class2]) 1);
 qed "real_mult";
 
 Goal "(z::real) * w = w * z";
@@ -397,7 +389,7 @@
 by (res_inst_tac [("z","y")] eq_Abs_real 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [real_minus,real_mult] 
-    @ preal_mult_ac @ preal_add_ac));
+                                 @ preal_mult_ac @ preal_add_ac));
 qed "real_minus_mult_eq1";
 
 Goal "-(x * y) = x * (- y :: real)";
diff -r e6b96d953965 -r a6ab3a442da6 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jul 19 12:33:19 2000 +0200
@@ -11,7 +11,7 @@
   realrel   ::  "((preal * preal) * (preal * preal)) set"
   "realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
 
-typedef real = "{x::(preal*preal).True}/realrel"          (Equiv.quotient_def)
+typedef real = "UNIV//realrel"  (Equiv.quotient_def)
 
 
 instance
diff -r e6b96d953965 -r a6ab3a442da6 src/HOL/Real/RealInt.ML
--- a/src/HOL/Real/RealInt.ML	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/RealInt.ML	Wed Jul 19 12:33:19 2000 +0200
@@ -15,8 +15,6 @@
 				  preal_of_prat_add RS sym]));
 qed "real_of_int_congruent";
 
-val real_of_int_ize = RSLIST [equiv_intrel, real_of_int_congruent];
-
 Goalw [real_of_int_def]
    "real_of_int (Abs_Integ (intrel ^^ {(i, j)})) = \
 \     Abs_real(realrel ^^ \
@@ -24,7 +22,7 @@
 \         preal_of_prat (prat_of_pnat (pnat_of_nat j)))})";
 by (res_inst_tac [("f","Abs_real")] arg_cong 1);
 by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_real_inverse,
-				  real_of_int_ize UN_equiv_class]) 1);
+		[equiv_intrel, real_of_int_congruent] MRS UN_equiv_class]) 1);
 qed "real_of_int";
 
 Goal "inj(real_of_int)";