# 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 \Transitive closure\ +lemma totalp_on_tranclp: "totalp_on A R \ totalp_on A (tranclp R)" + by (auto intro: totalp_onI dest: totalp_onD) + +lemma total_on_trancl: "total_on A r \ total_on A (trancl r)" + by (rule totalp_on_tranclp[to_set]) + lemma trancl_mono: assumes "p \ r\<^sup>+" "r \ s" shows "p \ s\<^sup>+"