src/HOL/Transitive_Closure.thy

   tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
   reflclp  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
   rtrancl  ("(_\<^sup>*)" [1000] 999) and
   trancl  ("(_\<^sup>+)" [1000] 999) and
   reflcl  ("(_\<^sup>=)" [1000] 999)
+
+
+subsection {* Reflexive closure *}
+
+lemma reflexive_reflcl[simp]: "reflexive(r^=)"
+by(simp add:refl_def)
+
+lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
+by(simp add:antisym_def)
+
+lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"
+unfolding trans_def by blast
 
 
 subsection {* Reflexive-transitive closure *}
 
 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)"

 
 lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
   by (unfold Domain_def) (blast dest: tranclD)
 
 lemma trancl_range [simp]: "Range (r^+) = Range r"
-  by (simp add: Range_def trancl_converse [symmetric])
+unfolding Range_def by(simp add: trancl_converse [symmetric])
 
 lemma Not_Domain_rtrancl:
     "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
   apply auto
   apply (erule rev_mp)