# HG changeset patch
# User paulson
# Date 910017089 -3600
# Node ID e3a98a7c0634dcd838bc3dd56f99abc08f819182
# Parent  4e5c74b7cd9e17579a4a3f783371822c0ca61fe2
Domain r, Range r   replace   fst``r, snd``r

diff -r 4e5c74b7cd9e -r e3a98a7c0634 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Mon Nov 02 12:36:16 1998 +0100
+++ b/src/HOL/Induct/LList.ML	Mon Nov 02 15:31:29 1998 +0100
@@ -63,16 +63,6 @@
 by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1);
 qed "CONS_UN1";
 
-(*UNUSED; obsolete?
-goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
-by (Simp_tac 1);
-qed "split_UN1";
-
-goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
-by (Simp_tac 1);
-qed "sum_case2_UN1";
-*)
-
 val prems = goalw LList.thy [CONS_def]
     "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
 by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
@@ -148,7 +138,7 @@
 end;
 qed "LListD_unfold";
 
-Goal "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
+Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
 by (res_inst_tac [("n", "k")] less_induct 1);
 by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
 by (etac LListD.elim 1);
@@ -163,16 +153,16 @@
 
 (*The domain of the LListD relation*)
 Goalw (llist.defs @ [NIL_def, CONS_def])
-    "fst``LListD(diag(A)) <= llist(A)";
+    "Domain (LListD(diag A)) <= llist(A)";
 by (rtac gfp_upperbound 1);
 (*avoids unfolding LListD on the rhs*)
-by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
+by (res_inst_tac [("P", "%x. Domain x <= ?B")] (LListD_unfold RS ssubst) 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
-qed "fst_image_LListD";
+qed "Domain_LListD";
 
 (*This inclusion justifies the use of coinduction to show M=N*)
-Goal "LListD(diag(A)) <= diag(llist(A))";
+Goal "LListD(diag A) <= diag(llist(A))";
 by (rtac subsetI 1);
 by (res_inst_tac [("p","x")] PairE 1);
 by Safe_tac;
@@ -180,7 +170,7 @@
 by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
           ntrunc_equality) 1);
 by (assume_tac 1);
-by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1);
+by (etac (DomainI RS (Domain_LListD RS subsetD)) 1);
 qed "LListD_subset_diag";
 
 
@@ -216,7 +206,7 @@
 
 
 (*This converse inclusion helps to strengthen LList_equalityI*)
-Goal "diag(llist(A)) <= LListD(diag(A))";
+Goal "diag(llist(A)) <= LListD(diag A)";
 by (rtac subsetI 1);
 by (etac LListD_coinduct 1);
 by (rtac subsetI 1);
@@ -228,7 +218,7 @@
 				       LListD_Fun_CONS_I])));
 qed "diag_subset_LListD";
 
-Goal "LListD(diag(A)) = diag(llist(A))";
+Goal "LListD(diag A) = diag(llist(A))";
 by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, 
                          diag_subset_LListD] 1));
 qed "LListD_eq_diag";
diff -r 4e5c74b7cd9e -r e3a98a7c0634 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Mon Nov 02 12:36:16 1998 +0100
+++ b/src/HOL/Prod.ML	Mon Nov 02 15:31:29 1998 +0100
@@ -301,6 +301,9 @@
 by (blast_tac (claset() addIs [prod_fun]) 1);
 qed "prod_fun_imageE";
 
+AddIs  [prod_fun_imageI];
+AddSEs [prod_fun_imageE];
+
 
 (*** Disjoint union of a family of sets - Sigma ***)
 
@@ -369,41 +372,6 @@
 by (Blast_tac 1);
 qed "UNION_Times_distrib";
 
-(*** Domain of a relation ***)
-
-Goalw [image_def] "(a,b) : r ==> a : fst``r";
-by (rtac CollectI 1);
-by (rtac bexI 1);
-by (rtac (fst_conv RS sym) 1);
-by (assume_tac 1);
-qed "fst_imageI";
-
-val major::prems = Goal
-    "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
-by (rtac (major RS imageE) 1);
-by (resolve_tac prems 1);
-by (etac ssubst 1);
-by (rtac (surjective_pairing RS subst) 1);
-by (assume_tac 1);
-qed "fst_imageE";
-
-(*** Range of a relation ***)
-
-Goalw [image_def] "(a,b) : r ==> b : snd``r";
-by (rtac CollectI 1);
-by (rtac bexI 1);
-by (rtac (snd_conv RS sym) 1);
-by (assume_tac 1);
-qed "snd_imageI";
-
-val major::prems = Goal "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
-by (rtac (major RS imageE) 1);
-by (resolve_tac prems 1);
-by (etac ssubst 1);
-by (rtac (surjective_pairing RS subst) 1);
-by (assume_tac 1);
-qed "snd_imageE";
-
 
 (** Exhaustion rule for unit -- a degenerate form of induction **)
 
@@ -413,10 +381,6 @@
 by (rtac (Rep_unit_inverse RS sym) 1);
 qed "unit_eq";
  
-AddIs  [fst_imageI, snd_imageI, prod_fun_imageI];
-AddSEs [fst_imageE, snd_imageE, prod_fun_imageE];
-
-
 (*simplification procedure for unit_eq.
   Cannot use this rule directly -- it loops!*)
 local
diff -r 4e5c74b7cd9e -r e3a98a7c0634 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Mon Nov 02 12:36:16 1998 +0100
+++ b/src/HOL/Univ.ML	Mon Nov 02 15:31:29 1998 +0100
@@ -568,16 +568,16 @@
 
 (*** Domain ***)
 
-Goal "fst `` diag(A) = A";
+Goal "Domain (diag A) = A";
 by Auto_tac;
-qed "fst_image_diag";
+qed "Domain_diag";
 
-Goal "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
+Goal "Domain (r<**>s) = (Domain r) <*> (Domain s)";
 by Auto_tac;
-qed "fst_image_dprod";
+qed "Domain_dprod";
 
-Goal "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
+Goal "Domain (r<++>s) = (Domain r) <+> (Domain s)";
 by Auto_tac;
-qed "fst_image_dsum";
+qed "Domain_dsum";
 
-Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
+Addsimps [Domain_diag, Domain_dprod, Domain_dsum];