Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemma transp_reflclp[simp]
authordesharna
Wed, 09 Nov 2022 15:38:43 +0100
changeset 76498 11077c158b37
parent 76497 ebcfaddd3cb6
child 76499 0fbfb4293ff7
added lemma transp_reflclp[simp]
NEWS file | annotate | diff | comparison | revisions
src/HOL/Transitive_Closure.thy file | annotate | diff | comparison | revisions 
--- a/NEWS	Wed Nov 09 15:37:21 2022 +0100
+++ b/NEWS	Wed Nov 09 15:38:43 2022 +0100
@@ -53,6 +53,7 @@
   - Added lemmas.
       reflclp_ident_if_reflp[simp]
       reflp_on_reflclp[simp]
+      transp_reflclp[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
--- a/src/HOL/Transitive_Closure.thy	Wed Nov 09 15:37:21 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 09 15:38:43 2022 +0100
@@ -79,6 +79,9 @@
 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)"
   unfolding trans_def by blast
 
+lemma transp_reflclp[simp]: "transp R \<Longrightarrow> transp R\<^sup>=\<^sup>="
+  unfolding transp_def by blast
+
 lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
   by blast
isabelle