# HG changeset patch
# User paulson
# Date 929003758 -7200
# Node ID 43c081a0858d57e4bb4534897d4c38aa7c75315d
# Parent  52b13dfbe9548b584a687675b13e18d409100873
new preficates refl, sym [from Integ/Equiv], antisym

diff -r 52b13dfbe954 -r 43c081a0858d src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Jun 10 10:34:55 1999 +0200
+++ b/src/HOL/Relation.ML	Thu Jun 10 10:35:58 1999 +0200
@@ -25,6 +25,19 @@
 qed "pair_in_Id_conv";
 Addsimps [pair_in_Id_conv];
 
+Goalw [refl_def] "reflexive Id";
+by Auto_tac;
+qed "reflexive_Id";
+
+(*A strange result, since Id is also symmetric.*)
+Goalw [antisym_def] "antisym Id";
+by Auto_tac;
+qed "antisym_Id";
+
+Goalw [trans_def] "trans Id";
+by Auto_tac;
+qed "trans_Id";
+
 
 (** Diagonal relation: indentity restricted to some set **)
 
@@ -108,6 +121,28 @@
 by (Blast_tac 1);
 qed "comp_subset_Sigma";
 
+(** Natural deduction for refl(r) **)
+
+val prems = Goalw [refl_def]
+    "[| r <= A Times A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
+by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
+qed "reflI";
+
+Goalw [refl_def] "[| refl A r; a:A |] ==> (a,a):r";
+by (Blast_tac 1);
+qed "reflD";
+
+(** Natural deduction for antisym(r) **)
+
+val prems = Goalw [antisym_def]
+    "(!! x y. [| (x,y):r;  (y,x):r |] ==> x=y) ==> antisym(r)";
+by (REPEAT (ares_tac (prems@[allI,impI]) 1));
+qed "antisymI";
+
+Goalw [antisym_def] "[| antisym(r);  (a,b):r;  (b,a):r |] ==> a=b";
+by (Blast_tac 1);
+qed "antisymD";
+
 (** Natural deduction for trans(r) **)
 
 val prems = Goalw [trans_def]
diff -r 52b13dfbe954 -r 43c081a0858d src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Jun 10 10:34:55 1999 +0200
+++ b/src/HOL/Relation.thy	Thu Jun 10 10:35:58 1999 +0200
@@ -17,22 +17,37 @@
   Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
   
 constdefs
-  Id          :: "('a * 'a)set"               (*the identity relation*)
+  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 :: "('a*'b) set => 'a set"
     "Domain(r) == {x. ? y. (x,y):r}"
 
-  Range       :: "('a*'b) set => 'b set"
+  Range  :: "('a*'b) set => 'b set"
     "Range(r) == Domain(r^-1)"
 
-  trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
+  refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
+    "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
+
+  sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
+    "sym(r) == ALL x y. (x,y): r --> (y,x): r"
+
+  antisym:: "('a * 'a)set => bool"          (*antisymmetry predicate*)
+    "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
+
+  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 :: "('a * 'b)set => bool"
     "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
 
+syntax
+  reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
+
+translations
+  "reflexive" == "refl UNIV"
+
 end