added lemmas and made concerse executable
authornipkow
Tue Sep 17 08:42:51 2013 +0200 (2013-09-17)
changeset 53680c5096c22892b
parent 53679 81e244e71986
child 53681 7e80b558c751
added lemmas and made concerse executable
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Tue Sep 17 01:11:37 2013 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Sep 17 08:42:51 2013 +0200
     1.3 @@ -680,6 +680,12 @@
     1.4    "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
     1.5    by (fact converse_converse [to_pred])
     1.6  
     1.7 +lemma converse_empty[simp]: "{}\<inverse> = {}"
     1.8 +by auto
     1.9 +
    1.10 +lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV"
    1.11 +by auto
    1.12 +
    1.13  lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
    1.14    by blast
    1.15  
    1.16 @@ -762,7 +768,7 @@
    1.17  lemma conversep_eq [simp]: "(op =)^--1 = op ="
    1.18    by (auto simp add: fun_eq_iff)
    1.19  
    1.20 -lemma converse_unfold:
    1.21 +lemma converse_unfold [code]:
    1.22    "r\<inverse> = {(y, x). (x, y) \<in> r}"
    1.23    by (simp add: set_eq_iff)
    1.24