--- 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";
--- 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}
--- 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";
--- 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)"
--- 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)";
--- 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
--- 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)";