# HG changeset patch # User desharna # Date 1668004641 -3600 # Node ID ebcfaddd3cb616c037c0b2b6a270218076b53ddd # Parent 855b5f0456d8f2d7376e4faf88c6b5c1b691a5f7 added lemma reflclp_ident_if_reflp[simp] diff -r 855b5f0456d8 -r ebcfaddd3cb6 NEWS --- a/NEWS Wed Nov 09 16:39:45 2022 +0100 +++ b/NEWS Wed Nov 09 15:37:21 2022 +0100 @@ -51,6 +51,7 @@ - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp. Minor INCOMPATIBILITY. - Added lemmas. + reflclp_ident_if_reflp[simp] reflp_on_reflclp[simp] * Theory "HOL.Wellfounded": diff -r 855b5f0456d8 -r ebcfaddd3cb6 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Nov 09 16:39:45 2022 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Nov 09 15:37:21 2022 +0100 @@ -82,6 +82,9 @@ lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>=" by blast +lemma reflclp_ident_if_reflp[simp]: "reflp R \ R\<^sup>=\<^sup>= = R" + by (auto dest: reflpD) + subsection \Reflexive-transitive closure\