author paulson Mon, 24 May 1999 15:53:28 +0200 changeset 6715 89891b0b596f parent 6714 6b2b4ec58178 child 6716 87c750df8888
UN_singleton->UN_constant_eq removes clash with other UN_singleton
 src/HOL/Integ/Equiv.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integ/Equiv.ML	Mon May 24 15:51:33 1999 +0200
+++ b/src/HOL/Integ/Equiv.ML	Mon May 24 15:53:28 1999 +0200
@@ -125,20 +125,19 @@
(**** Defining unary operations upon equivalence classes ****)

(* theorem needed to prove UN_equiv_class *)
-goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
+goal Set.thy "!!A. [| a:A; ! y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
-qed "UN_singleton_lemma";
-val UN_singleton = ballI RSN (2,UN_singleton_lemma);
+qed "UN_constant_eq";

-(** These proofs really require the local premises
+(** Could introduce a LOCALE with the assumptions
equiv A r;  congruent r b
**)

(*Conversion rule*)
Goal "[| equiv A r;  congruent r b;  a: A |] \
-\                      ==> (UN x:r^^{a}. b(x)) = b(a)";
-by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
+\     ==> (UN x:r^^{a}. b(x)) = b(a)";
+by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1));
by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
by (Blast_tac 1);
qed "UN_equiv_class";```