# HG changeset patch
# User paulson
# Date 864306577 -7200
# Node ID 2ee6c397003dd19310f57186d349a76dbc6630c4
# Parent  c9c99aa082fb6b44c16f5f10603299c56ab3f25b
Deleted rprod: lex_prod is (usually?) enough

diff -r c9c99aa082fb -r 2ee6c397003d src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Thu May 22 15:09:09 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Thu May 22 15:09:37 1997 +0200
@@ -3,7 +3,7 @@
     Author: 	Konrad Slind
     Copyright   1996  TU Munich
 
-Derived wellfounded relations: inverse image, relational product, measure, ...
+Derived WF relations: inverse image, lexicographic product, measure, ...
 *)
 
 open WF_Rel;
@@ -79,20 +79,6 @@
 qed "wf_lex_prod";
 AddSIs [wf_lex_prod];
 
-(*----------------------------------------------------------------------------
- * Wellfoundedness of relational product
- *---------------------------------------------------------------------------*)
-val [wfa,wfb] = goalw thy [wf_def,rprod_def]
- "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
-by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
-by (rtac (wfa RS spec RS mp) 1);
-by (EVERY1 [rtac allI,rtac impI]);
-by (rtac (wfb RS spec RS mp) 1);
-by (Blast_tac 1);
-qed "wf_rel_prod";
-AddSIs [wf_rel_prod];
-
-
 (*---------------------------------------------------------------------------
  * Wellfoundedness of subsets
  *---------------------------------------------------------------------------*)
@@ -122,13 +108,6 @@
 qed "trans_lex_prod";
 AddSIs [trans_lex_prod];
 
-goalw thy [trans_def, rprod_def]
-    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "trans_rprod";
-AddSIs [trans_rprod];
-
 
 (*---------------------------------------------------------------------------
  * Wellfoundedness of proper subset on finite sets.
diff -r c9c99aa082fb -r 2ee6c397003d src/HOL/WF_Rel.thy
--- a/src/HOL/WF_Rel.thy	Thu May 22 15:09:09 1997 +0200
+++ b/src/HOL/WF_Rel.thy	Thu May 22 15:09:37 1997 +0200
@@ -3,7 +3,11 @@
     Author:     Konrad Slind
     Copyright   1995 TU Munich
 
-Derived wellfounded relations: inverse image, relational product, measure, ...
+Derived WF relations: inverse image, lexicographic product, measure, ...
+
+The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
+subset of the lexicographic product, and therefore does not need to be defined
+separately.
 *)
 
 WF_Rel = Finite +
@@ -12,7 +16,6 @@
   inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
   measure   :: "('a => nat) => ('a * 'a)set"
   "**"      :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
-  rprod     :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
   finite_psubset  :: "('a set * 'a set) set"
 
 
@@ -27,10 +30,6 @@
                                 p = ((a,b),(a',b')) & 
                                ((a,a') : ra | a=a' & (b,b') : rb)}"
 
-  rprod_def     "rprod ra rb == {p. ? a a' b b'. 
-                                p = ((a,b),(a',b')) & 
-                               ((a,a') : ra & (b,b') : rb)}"
-
   (* finite proper subset*)
   finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
 end