replaced {x. True} by UNIV to work with the new simprule, Collect_const
--- a/src/HOL/Induct/LList.ML Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Induct/LList.ML Mon Oct 11 10:52:51 1999 +0200
@@ -108,7 +108,7 @@
(*A typical use of co-induction to show membership in the gfp.
Bisimulation is range(%x. LList_corec x f) *)
-Goal "LList_corec a f : llist({u. True})";
+Goal "LList_corec a f : llist UNIV";
by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
by Safe_tac;
@@ -247,14 +247,14 @@
\ ==> h1=h2";
by (rtac ext 1);
(*next step avoids an unknown (and flexflex pair) in simplification*)
-by (res_inst_tac [("A", "{u. True}"),
+by (res_inst_tac [("A", "UNIV"),
("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
by (rtac rangeI 1);
by Safe_tac;
by (stac prem1 1);
by (stac prem2 1);
by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
- CollectI RS LListD_Fun_CONS_I]) 1);
+ UNIV_I RS LListD_Fun_CONS_I]) 1);
qed "LList_corec_unique";
val [prem] =
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Mon Oct 11 10:52:51 1999 +0200
@@ -1848,7 +1848,7 @@
Goal "inj hypreal_of_nat";
by (rtac injI 1);
by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
- simpset() addsimps [hypreal_of_nat_iff,
+ simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
real_add_right_cancel,inj_real_of_nat RS injD]));
qed "inj_hypreal_of_nat";
--- a/src/HOL/Real/PRat.ML Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/PRat.ML Mon Oct 11 10:52:51 1999 +0200
@@ -786,22 +786,22 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "lemma_prat_less_1_not_memEx";
-Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {q::prat. True}";
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= UNIV";
by (rtac notI 1);
by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
by (Asm_full_simp_tac 1);
qed "lemma_prat_less_1_set_not_rat_set";
Goalw [psubset_def,subset_def]
- "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < {q::prat. True}";
-by (asm_full_simp_tac (simpset() addsimps
- [lemma_prat_less_1_set_not_rat_set,
- lemma_prat_less_1_not_memEx]) 1);
+ "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < UNIV";
+by (asm_full_simp_tac
+ (simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
+ lemma_prat_less_1_not_memEx]) 1);
qed "lemma_prat_less_1_set_psubset_rat_set";
(*** prove non_emptiness of type ***)
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
-\ A < {q::prat. True} & \
+\ A < UNIV & \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (? u: A. y < u)))}";
by (auto_tac (claset() addDs [prat_less_trans],
--- a/src/HOL/Real/PReal.ML Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/PReal.ML Mon Oct 11 10:52:51 1999 +0200
@@ -51,21 +51,21 @@
qed "mem_Rep_preal_Ex";
Goalw [preal_def]
- "[| {} < A; A < {q::prat. True}; \
+ "[| {} < A; A < UNIV; \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (? u: A. y < u))) |] ==> A : preal";
by (Fast_tac 1);
qed "prealI1";
Goalw [preal_def]
- "[| {} < A; A < {q::prat. True}; \
+ "[| {} < A; A < UNIV; \
\ !y: A. (!z. z < y --> z: A); \
\ !y: A. (? u: A. y < u) |] ==> A : preal";
by (Best_tac 1);
qed "prealI2";
Goalw [preal_def]
- "A : preal ==> {} < A & A < {q::prat. True} & \
+ "A : preal ==> {} < A & A < UNIV & \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (? u: A. y < u)))";
by (Fast_tac 1);
@@ -81,7 +81,7 @@
by (Fast_tac 1);
qed "prealE_lemma1";
-Goalw [preal_def] "A : preal ==> A < {q::prat. True}";
+Goalw [preal_def] "A : preal ==> A < UNIV";
by (Fast_tac 1);
qed "prealE_lemma2";
@@ -235,7 +235,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_add_set_Ex";
-Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < {q. True}";
+Goal "{w. ? x: Rep_preal R. ? 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 (etac exE 1);
@@ -325,7 +325,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_mult_set_Ex";
-Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < {q. True}";
+Goal "{w. ? x: Rep_preal R. ? 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 (etac exE 1);
@@ -555,7 +555,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_inv_set_Ex";
-Goal "{x. ? y. x < y & qinv y ~: Rep_preal A} < {q. True}";
+Goal "{x. ? 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 (etac exE 1);
@@ -877,7 +877,7 @@
by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
qed "lemma_ex_not_mem_less_left_add1";
-Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < {q. True}";
+Goal "{d. ? 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 (etac exE 1);
@@ -1115,7 +1115,7 @@
qed "preal_sup_not_mem_Ex1";
Goal "? Y. (! X: P. X < Y) \
-\ ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}"; (**)
+\ ==> {w. ? X: P. w: Rep_preal(X)} < UNIV"; (**)
by (dtac preal_sup_not_mem_Ex 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (eres_inst_tac [("c","q")] equalityCE 1);
@@ -1123,7 +1123,7 @@
qed "preal_sup_set_not_prat_set";
Goal "? Y. (! X: P. X <= Y) \
-\ ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
+\ ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";
by (dtac preal_sup_not_mem_Ex1 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (eres_inst_tac [("c","q")] equalityCE 1);
--- a/src/HOL/Real/PReal.thy Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/PReal.thy Mon Oct 11 10:52:51 1999 +0200
@@ -9,7 +9,7 @@
PReal = PRat +
-typedef preal = "{A::prat set. {} < A & A < {q::prat. True} &
+typedef preal = "{A::prat set. {} < A & A < UNIV &
(!y: A. ((!z. z < y --> z: A) &
(? u: A. y < u)))}" (preal_1)
instance