Added R_O_id and id_O_R
authornipkow
Sat Apr 27 12:07:31 1996 +0200 (1996-04-27)
changeset 16943452958f85a8
parent 1693 7083f6b05423
child 1695 0f9b9eda2a2c
Added R_O_id and id_O_R
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Sat Apr 27 12:05:58 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Sat Apr 27 12:07:31 1996 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4  goalw Relation.thy [id_def] "(a,b):id = (a=b)";
     1.5  by (fast_tac prod_cs 1);
     1.6  qed "pair_in_id_conv";
     1.7 +Addsimps [pair_in_id_conv];
     1.8  
     1.9  
    1.10  (** Composition of two relations **)
    1.11 @@ -172,4 +173,12 @@
    1.12  
    1.13  val rel_eq_cs = rel_cs addSIs [equalityI];
    1.14  
    1.15 -Addsimps [pair_in_id_conv];
    1.16 +goal Relation.thy "R O id = R";
    1.17 +by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
    1.18 +qed "R_O_id";
    1.19 +
    1.20 +goal Relation.thy "id O R = R";
    1.21 +by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
    1.22 +qed "id_O_R";
    1.23 +
    1.24 +Addsimps [R_O_id,id_O_R];