three new theorems
authorpaulson
Mon Jul 26 16:29:38 1999 +0200 (1999-07-26)
changeset 70839663eb2bce05
parent 7082 f444e632cdf5
child 7084 4af4f4d8035c
three new theorems
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Mon Jul 26 16:08:15 1999 +0200
     1.2 +++ b/src/HOL/Relation.ML	Mon Jul 26 16:29:38 1999 +0200
     1.3 @@ -4,8 +4,6 @@
     1.4      Copyright   1996  University of Cambridge
     1.5  *)
     1.6  
     1.7 -open Relation;
     1.8 -
     1.9  (** Identity relation **)
    1.10  
    1.11  Goalw [Id_def] "(a,a) : Id";  
    1.12 @@ -201,6 +199,18 @@
    1.13  qed "converse_diag";
    1.14  Addsimps [converse_diag];
    1.15  
    1.16 +Goalw [refl_def] "refl A r ==> refl A (converse r)";
    1.17 +by (Blast_tac 1);
    1.18 +qed "refl_converse";
    1.19 +
    1.20 +Goalw [antisym_def] "antisym (converse r) = antisym r";
    1.21 +by (Blast_tac 1);
    1.22 +qed "antisym_converse";
    1.23 +
    1.24 +Goalw [trans_def] "trans (converse r) = trans r";
    1.25 +by (Blast_tac 1);
    1.26 +qed "trans_converse";
    1.27 +
    1.28  (** Domain **)
    1.29  
    1.30  Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";