# HG changeset patch
# User paulson
# Date 912159629 -3600
# Node ID fa2c2dd74f8cd0e974fdbc57e49a24eee7df61e5
# Parent  9f0c8869cf71df89c2da4f007fc32472fd131bae
moved diag (diagonal relation) from Univ to Relation

diff -r 9f0c8869cf71 -r fa2c2dd74f8c src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Nov 26 17:40:10 1998 +0100
+++ b/src/HOL/Relation.ML	Fri Nov 27 10:40:29 1998 +0100
@@ -26,6 +26,38 @@
 Addsimps [pair_in_Id_conv];
 
 
+(** Diagonal relation: indentity restricted to some set **)
+
+(*** Equality : the diagonal relation ***)
+
+Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
+by (Blast_tac 1);
+qed "diag_eqI";
+
+val diagI = refl RS diag_eqI |> standard;
+
+(*The general elimination rule*)
+val major::prems = Goalw [diag_def]
+    "[| c : diag(A);  \
+\       !!x y. [| x:A;  c = (x,x) |] ==> P \
+\    |] ==> P";
+by (rtac (major RS UN_E) 1);
+by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
+qed "diagE";
+
+AddSIs [diagI];
+AddSEs [diagE];
+
+Goal "((x,y) : diag A) = (x=y & x : A)";
+by (Blast_tac 1);
+qed "diag_iff";
+
+Goal "diag(A) <= A Times A";
+by (Blast_tac 1);
+qed "diag_subset_Sigma";
+
+
+
 (** Composition of two relations **)
 
 Goalw [comp_def]
@@ -152,6 +184,11 @@
 qed "Domain_Id";
 Addsimps [Domain_Id];
 
+Goal "Domain (diag A) = A";
+by Auto_tac;
+qed "Domain_diag";
+Addsimps [Domain_diag];
+
 Goal "Domain(A Un B) = Domain(A) Un Domain(B)";
 by (Blast_tac 1);
 qed "Domain_Un_eq";
diff -r 9f0c8869cf71 -r fa2c2dd74f8c src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Nov 26 17:40:10 1998 +0100
+++ b/src/HOL/Relation.thy	Fri Nov 27 10:40:29 1998 +0100
@@ -5,22 +5,34 @@
 *)
 
 Relation = Prod +
+
 consts
-    Id          :: "('a * 'a)set"               (*the identity relation*)
-    O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
-    converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
-    "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
-    Domain      :: "('a*'b) set => 'a set"
-    Range       :: "('a*'b) set => 'b set"
-    trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
-    Univalent   :: "('a * 'b)set => bool"
+  O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
+  converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
+  "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
+  
 defs
-    Id_def        "Id == {p. ? x. p = (x,x)}"
-    comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
-    converse_def   "r^-1 == {(y,x). (x,y):r}"
-    Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
-    Range_def     "Range(r) == Domain(r^-1)"
-    Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
-    trans_def     "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
-    Univalent_def "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
+  comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
+  converse_def  "r^-1 == {(y,x). (x,y):r}"
+  Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
+  
+constdefs
+  Id          :: "('a * 'a)set"               (*the identity relation*)
+      "Id == {p. ? x. p = (x,x)}"
+
+  diag   :: "'a set => ('a * 'a)set"
+    "diag(A) == UN x:A. {(x,x)}"
+  
+  Domain      :: "('a*'b) set => 'a set"
+    "Domain(r) == {x. ? y. (x,y):r}"
+
+  Range       :: "('a*'b) set => 'b set"
+    "Range(r) == Domain(r^-1)"
+
+  trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
+    "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
+
+  Univalent   :: "('a * 'b)set => bool"
+    "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
+
 end
diff -r 9f0c8869cf71 -r fa2c2dd74f8c src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu Nov 26 17:40:10 1998 +0100
+++ b/src/HOL/Univ.ML	Fri Nov 27 10:40:29 1998 +0100
@@ -465,23 +465,6 @@
 qed "In1_UN1";
 
 
-(*** Equality : the diagonal relation ***)
-
-Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
-by (Blast_tac 1);
-qed "diag_eqI";
-
-val diagI = refl RS diag_eqI |> standard;
-
-(*The general elimination rule*)
-val major::prems = Goalw [diag_def]
-    "[| c : diag(A);  \
-\       !!x y. [| x:A;  c = (x,x) |] ==> P \
-\    |] ==> P";
-by (rtac (major RS UN_E) 1);
-by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
-qed "diagE";
-
 (*** Equality for Cartesian Product ***)
 
 Goalw [dprod_def]
@@ -520,10 +503,10 @@
 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1));
 qed "dsumE";
 
+AddSIs [uprodI, dprodI];
+AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
+AddSEs [uprodE, dprodE, usumE, dsumE];
 
-AddSIs [diagI, uprodI, dprodI];
-AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
-AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
 
 (*** Monotonicity ***)
 
@@ -538,10 +521,6 @@
 
 (*** Bounding theorems ***)
 
-Goal "diag(A) <= A Times A";
-by (Blast_tac 1);
-qed "diag_subset_Sigma";
-
 Goal "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
 by (Blast_tac 1);
 qed "dprod_Sigma";
@@ -564,10 +543,6 @@
 
 (*** Domain ***)
 
-Goal "Domain (diag A) = A";
-by Auto_tac;
-qed "Domain_diag";
-
 Goal "Domain (r<**>s) = (Domain r) <*> (Domain s)";
 by Auto_tac;
 qed "Domain_dprod";
@@ -576,4 +551,4 @@
 by Auto_tac;
 qed "Domain_dsum";
 
-Addsimps [Domain_diag, Domain_dprod, Domain_dsum];
+Addsimps [Domain_dprod, Domain_dsum];
diff -r 9f0c8869cf71 -r fa2c2dd74f8c src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Thu Nov 26 17:40:10 1998 +0100
+++ b/src/HOL/Univ.thy	Fri Nov 27 10:40:29 1998 +0100
@@ -42,7 +42,6 @@
   Split  :: [['a item, 'a item]=>'b, 'a item] => 'b
   Case   :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b
 
-  diag   :: "'a set => ('a * 'a)set"
   "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
            => ('a item * 'a item)set" (infixr 80)
   "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
@@ -88,13 +87,11 @@
                               | (? y . M = In1(y) & u = d(y))"
 
 
-  (** diagonal sets and equality for the "universe" **)
-
-  diag_def   "diag(A) == UN x:A. {(x,x)}"
+  (** equality for the "universe" **)
 
   dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
 
   dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
-                       (UN (y,y'):s. {(In1(y),In1(y'))})"
+                        (UN (y,y'):s. {(In1(y),In1(y'))})"
 
 end