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 totalp_on_converse[simp]
authordesharna
Wed, 23 Nov 2022 10:27:24 +0100
changeset 76573 cbf38b7cb195
parent 76572 d8542bc5a3fa
child 76574 7bc934b99faf
added lemma totalp_on_converse[simp]
NEWS file | annotate | diff | comparison | revisions
src/HOL/Relation.thy file | annotate | diff | comparison | revisions 
--- a/NEWS	Wed Nov 23 10:23:18 2022 +0100
+++ b/NEWS	Wed Nov 23 10:27:24 2022 +0100
@@ -59,6 +59,7 @@
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
       totalI
+      totalp_on_converse[simp]
       totalp_on_singleton[simp]
 
 * Theory "HOL.Transitive_Closure":
--- a/src/HOL/Relation.thy	Wed Nov 23 10:23:18 2022 +0100
+++ b/src/HOL/Relation.thy	Wed Nov 23 10:27:24 2022 +0100
@@ -1021,6 +1021,9 @@
 lemma total_on_converse [simp]: "total_on A (r\<inverse>) = total_on A r"
   by (auto simp: total_on_def)
 
+lemma totalp_on_converse [simp]: "totalp_on A R\<inverse>\<inverse> = totalp_on A R"
+  by (rule total_on_converse[to_pred])
+
 lemma finite_converse [iff]: "finite (r\<inverse>) = finite r"
 unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
 by (auto elim: finite_imageD simp: inj_on_def)
isabelle