# HG changeset patch
# User desharna
# Date 1657036492 -7200
# Node ID c4a1088d008180bfd82ff93a32e709778518f25b
# Parent  f4116b7a66792cd335acac50ea0785da1c72a484
added lemmas total_on_trancl and totalp_on_tranclp

diff -r f4116b7a6679 -r c4a1088d0081 NEWS
--- a/NEWS	Mon Jul 04 16:12:47 2022 +0000
+++ b/NEWS	Tue Jul 05 17:54:52 2022 +0200
@@ -90,6 +90,11 @@
       totalp_on_subset
       totalp_on_total_on_eq[pred_set_conv]
 
+* Theory "HOL.Transitive_Closure":
+  - Added lemmas.
+      total_on_trancl
+      totalp_on_tranclp
+
 * Theory "HOL-Library.Multiset":
   - Consolidated operation and fact names.
         multp ~> multp_code
diff -r f4116b7a6679 -r c4a1088d0081 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Jul 04 16:12:47 2022 +0000
+++ b/src/HOL/Transitive_Closure.thy	Tue Jul 05 17:54:52 2022 +0200
@@ -312,6 +312,12 @@
 
 subsection \<open>Transitive closure\<close>
 
+lemma totalp_on_tranclp: "totalp_on A R \<Longrightarrow> totalp_on A (tranclp R)"
+  by (auto intro: totalp_onI dest: totalp_onD)
+
+lemma total_on_trancl: "total_on A r \<Longrightarrow> total_on A (trancl r)"
+  by (rule totalp_on_tranclp[to_set])
+
 lemma trancl_mono:
   assumes "p \<in> r\<^sup>+" "r \<subseteq> s"
   shows "p \<in> s\<^sup>+"