src/HOL/Transitive_Closure.thy
changeset 26271 e324f8918c98
parent 26179 bc5d582d6cfe
child 26340 a85fe32e7b2f
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Mar 14 12:18:56 2008 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 14 19:57:12 2008 +0100
     1.3 @@ -63,6 +63,18 @@
     1.4    reflcl  ("(_\<^sup>=)" [1000] 999)
     1.5  
     1.6  
     1.7 +subsection {* Reflexive closure *}
     1.8 +
     1.9 +lemma reflexive_reflcl[simp]: "reflexive(r^=)"
    1.10 +by(simp add:refl_def)
    1.11 +
    1.12 +lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
    1.13 +by(simp add:antisym_def)
    1.14 +
    1.15 +lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"
    1.16 +unfolding trans_def by blast
    1.17 +
    1.18 +
    1.19  subsection {* Reflexive-transitive closure *}
    1.20  
    1.21  lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)"
    1.22 @@ -546,7 +558,7 @@
    1.23    by (unfold Domain_def) (blast dest: tranclD)
    1.24  
    1.25  lemma trancl_range [simp]: "Range (r^+) = Range r"
    1.26 -  by (simp add: Range_def trancl_converse [symmetric])
    1.27 +unfolding Range_def by(simp add: trancl_converse [symmetric])
    1.28  
    1.29  lemma Not_Domain_rtrancl:
    1.30      "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"