Added simp-rules: "R O {} = {}" and "{} O R = {}"
authorkrauss
Fri Jun 01 15:12:56 2007 +0200 (2007-06-01)
changeset 231851fa87978cf27
parent 23184 f3b967273975
child 23186 f948708bc100
Added simp-rules: "R O {} = {}" and "{} O R = {}"
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Fri Jun 01 10:44:31 2007 +0200
     1.2 +++ b/src/HOL/Relation.thy	Fri Jun 01 15:12:56 2007 +0200
     1.3 @@ -147,6 +147,12 @@
     1.4  lemma Id_O_R [simp]: "Id O R = R"
     1.5    by fast
     1.6  
     1.7 +lemma rel_comp_empty1[simp]: "{} O R = {}"
     1.8 +  by blast
     1.9 +
    1.10 +lemma rel_comp_empty2[simp]: "R O {} = {}"
    1.11 +  by blast
    1.12 +
    1.13  lemma O_assoc: "(R O S) O T = R O (S O T)"
    1.14    by blast
    1.15