src/HOL/Relation.ML
changeset 6806 43c081a0858d
parent 6005 45186ec4d8b6
child 7007 b46ccfee8e59
     1.1 --- a/src/HOL/Relation.ML	Thu Jun 10 10:34:55 1999 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Jun 10 10:35:58 1999 +0200
     1.3 @@ -25,6 +25,19 @@
     1.4  qed "pair_in_Id_conv";
     1.5  Addsimps [pair_in_Id_conv];
     1.6  
     1.7 +Goalw [refl_def] "reflexive Id";
     1.8 +by Auto_tac;
     1.9 +qed "reflexive_Id";
    1.10 +
    1.11 +(*A strange result, since Id is also symmetric.*)
    1.12 +Goalw [antisym_def] "antisym Id";
    1.13 +by Auto_tac;
    1.14 +qed "antisym_Id";
    1.15 +
    1.16 +Goalw [trans_def] "trans Id";
    1.17 +by Auto_tac;
    1.18 +qed "trans_Id";
    1.19 +
    1.20  
    1.21  (** Diagonal relation: indentity restricted to some set **)
    1.22  
    1.23 @@ -108,6 +121,28 @@
    1.24  by (Blast_tac 1);
    1.25  qed "comp_subset_Sigma";
    1.26  
    1.27 +(** Natural deduction for refl(r) **)
    1.28 +
    1.29 +val prems = Goalw [refl_def]
    1.30 +    "[| r <= A Times A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
    1.31 +by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
    1.32 +qed "reflI";
    1.33 +
    1.34 +Goalw [refl_def] "[| refl A r; a:A |] ==> (a,a):r";
    1.35 +by (Blast_tac 1);
    1.36 +qed "reflD";
    1.37 +
    1.38 +(** Natural deduction for antisym(r) **)
    1.39 +
    1.40 +val prems = Goalw [antisym_def]
    1.41 +    "(!! x y. [| (x,y):r;  (y,x):r |] ==> x=y) ==> antisym(r)";
    1.42 +by (REPEAT (ares_tac (prems@[allI,impI]) 1));
    1.43 +qed "antisymI";
    1.44 +
    1.45 +Goalw [antisym_def] "[| antisym(r);  (a,b):r;  (b,a):r |] ==> a=b";
    1.46 +by (Blast_tac 1);
    1.47 +qed "antisymD";
    1.48 +
    1.49  (** Natural deduction for trans(r) **)
    1.50  
    1.51  val prems = Goalw [trans_def]