replaced {x. True} by UNIV to work with the new simprule, Collect_const
authorpaulson
Mon Oct 11 10:52:51 1999 +0200 (1999-10-11)
changeset 78251be9b63e7d93
parent 7824 1a85ba81d019
child 7826 c6a8b73b6c2a
replaced {x. True} by UNIV to work with the new simprule, Collect_const
src/HOL/Induct/LList.ML
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/PReal.thy
     1.1 --- a/src/HOL/Induct/LList.ML	Mon Oct 11 10:51:24 1999 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Mon Oct 11 10:52:51 1999 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5  (*A typical use of co-induction to show membership in the gfp. 
     1.6    Bisimulation is  range(%x. LList_corec x f) *)
     1.7 -Goal "LList_corec a f : llist({u. True})";
     1.8 +Goal "LList_corec a f : llist UNIV";
     1.9  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    1.10  by (rtac rangeI 1);
    1.11  by Safe_tac;
    1.12 @@ -247,14 +247,14 @@
    1.13  \ ==> h1=h2";
    1.14  by (rtac ext 1);
    1.15  (*next step avoids an unknown (and flexflex pair) in simplification*)
    1.16 -by (res_inst_tac [("A", "{u. True}"),
    1.17 +by (res_inst_tac [("A", "UNIV"),
    1.18                    ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
    1.19  by (rtac rangeI 1);
    1.20  by Safe_tac;
    1.21  by (stac prem1 1);
    1.22  by (stac prem2 1);
    1.23  by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
    1.24 -				  CollectI RS LListD_Fun_CONS_I]) 1);
    1.25 +				  UNIV_I RS LListD_Fun_CONS_I]) 1);
    1.26  qed "LList_corec_unique";
    1.27  
    1.28  val [prem] = 
     2.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Oct 11 10:51:24 1999 +0200
     2.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Oct 11 10:52:51 1999 +0200
     2.3 @@ -1848,7 +1848,7 @@
     2.4  Goal "inj hypreal_of_nat";
     2.5  by (rtac injI 1);
     2.6  by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
     2.7 -        simpset() addsimps [hypreal_of_nat_iff,
     2.8 +        simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
     2.9          real_add_right_cancel,inj_real_of_nat RS injD]));
    2.10  qed "inj_hypreal_of_nat";
    2.11  
     3.1 --- a/src/HOL/Real/PRat.ML	Mon Oct 11 10:51:24 1999 +0200
     3.2 +++ b/src/HOL/Real/PRat.ML	Mon Oct 11 10:52:51 1999 +0200
     3.3 @@ -786,22 +786,22 @@
     3.4  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
     3.5  qed "lemma_prat_less_1_not_memEx";
     3.6  
     3.7 -Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {q::prat. True}";
     3.8 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= UNIV";
     3.9  by (rtac notI 1);
    3.10  by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
    3.11  by (Asm_full_simp_tac 1);
    3.12  qed "lemma_prat_less_1_set_not_rat_set";
    3.13  
    3.14  Goalw [psubset_def,subset_def] 
    3.15 -      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < {q::prat. True}";
    3.16 -by (asm_full_simp_tac (simpset() addsimps 
    3.17 -      [lemma_prat_less_1_set_not_rat_set,
    3.18 -       lemma_prat_less_1_not_memEx]) 1);
    3.19 +      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < UNIV";
    3.20 +by (asm_full_simp_tac
    3.21 +    (simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
    3.22 +			 lemma_prat_less_1_not_memEx]) 1);
    3.23  qed "lemma_prat_less_1_set_psubset_rat_set";
    3.24  
    3.25  (*** prove non_emptiness of type ***)
    3.26  Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
    3.27 -\               A < {q::prat. True} & \
    3.28 +\               A < UNIV & \
    3.29  \               (!y: A. ((!z. z < y --> z: A) & \
    3.30  \               (? u: A. y < u)))}";
    3.31  by (auto_tac (claset() addDs [prat_less_trans],
     4.1 --- a/src/HOL/Real/PReal.ML	Mon Oct 11 10:51:24 1999 +0200
     4.2 +++ b/src/HOL/Real/PReal.ML	Mon Oct 11 10:52:51 1999 +0200
     4.3 @@ -51,21 +51,21 @@
     4.4  qed "mem_Rep_preal_Ex";
     4.5  
     4.6  Goalw [preal_def] 
     4.7 -      "[| {} < A; A < {q::prat. True}; \
     4.8 +      "[| {} < A; A < UNIV; \
     4.9  \              (!y: A. ((!z. z < y --> z: A) & \
    4.10  \                        (? u: A. y < u))) |] ==> A : preal";
    4.11  by (Fast_tac 1);
    4.12  qed "prealI1";
    4.13      
    4.14  Goalw [preal_def] 
    4.15 -      "[| {} < A; A < {q::prat. True}; \
    4.16 +      "[| {} < A; A < UNIV; \
    4.17  \              !y: A. (!z. z < y --> z: A); \
    4.18  \              !y: A. (? u: A. y < u) |] ==> A : preal";
    4.19  by (Best_tac 1);
    4.20  qed "prealI2";
    4.21  
    4.22  Goalw [preal_def] 
    4.23 -      "A : preal ==> {} < A & A < {q::prat. True} & \
    4.24 +      "A : preal ==> {} < A & A < UNIV & \
    4.25  \                         (!y: A. ((!z. z < y --> z: A) & \
    4.26  \                                  (? u: A. y < u)))";
    4.27  by (Fast_tac 1);
    4.28 @@ -81,7 +81,7 @@
    4.29  by (Fast_tac 1);
    4.30  qed "prealE_lemma1";
    4.31  
    4.32 -Goalw [preal_def] "A : preal ==> A < {q::prat. True}";
    4.33 +Goalw [preal_def] "A : preal ==> A < UNIV";
    4.34  by (Fast_tac 1);
    4.35  qed "prealE_lemma2";
    4.36  
    4.37 @@ -235,7 +235,7 @@
    4.38  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
    4.39  qed "preal_not_mem_add_set_Ex";
    4.40  
    4.41 -Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < {q. True}";
    4.42 +Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < UNIV";
    4.43  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    4.44  by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
    4.45  by (etac exE 1);
    4.46 @@ -325,7 +325,7 @@
    4.47  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
    4.48  qed "preal_not_mem_mult_set_Ex";
    4.49  
    4.50 -Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < {q. True}";
    4.51 +Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < UNIV";
    4.52  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    4.53  by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
    4.54  by (etac exE 1);
    4.55 @@ -555,7 +555,7 @@
    4.56  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
    4.57  qed "preal_not_mem_inv_set_Ex";
    4.58  
    4.59 -Goal "{x. ? y. x < y & qinv y ~:  Rep_preal A} < {q. True}";
    4.60 +Goal "{x. ? y. x < y & qinv y ~:  Rep_preal A} < UNIV";
    4.61  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    4.62  by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
    4.63  by (etac exE 1);
    4.64 @@ -877,7 +877,7 @@
    4.65  by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
    4.66  qed "lemma_ex_not_mem_less_left_add1";
    4.67  
    4.68 -Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < {q. True}";
    4.69 +Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
    4.70  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    4.71  by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
    4.72  by (etac exE 1);
    4.73 @@ -1115,7 +1115,7 @@
    4.74  qed "preal_sup_not_mem_Ex1";
    4.75  
    4.76  Goal "? Y. (! X: P. X < Y)  \                                    
    4.77 -\         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";       (**)
    4.78 +\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";       (**)
    4.79  by (dtac preal_sup_not_mem_Ex 1);
    4.80  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    4.81  by (eres_inst_tac [("c","q")] equalityCE 1);
    4.82 @@ -1123,7 +1123,7 @@
    4.83  qed "preal_sup_set_not_prat_set";
    4.84  
    4.85  Goal "? Y. (! X: P. X <= Y)  \
    4.86 -\         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
    4.87 +\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";
    4.88  by (dtac preal_sup_not_mem_Ex1 1);
    4.89  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    4.90  by (eres_inst_tac [("c","q")] equalityCE 1);
     5.1 --- a/src/HOL/Real/PReal.thy	Mon Oct 11 10:51:24 1999 +0200
     5.2 +++ b/src/HOL/Real/PReal.thy	Mon Oct 11 10:52:51 1999 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  
     5.5  PReal = PRat +
     5.6  
     5.7 -typedef preal = "{A::prat set. {} < A & A < {q::prat. True} &
     5.8 +typedef preal = "{A::prat set. {} < A & A < UNIV &
     5.9                                 (!y: A. ((!z. z < y --> z: A) &
    5.10                                          (? u: A. y < u)))}"      (preal_1)
    5.11  instance