# HG changeset patch
# User desharna
# Date 1742571740 -3600
# Node ID 6c68eff8355a9153b0b7df6695c41ca1456f028d
# Parent  c95eca07f6a09b96d51eb8e5a7cb4939b602bf71# Parent  c6193fc5ea3c17c0500861bdb2488c63b99be0bd
merged

diff -r c6193fc5ea3c -r 6c68eff8355a NEWS
--- a/NEWS	Fri Mar 21 14:35:11 2025 +0100
+++ b/NEWS	Fri Mar 21 16:42:20 2025 +0100
@@ -55,6 +55,7 @@
       totalp_on_mono_stronger_alt
       totalp_on_top[simp]
       trans_on_bot[simp]
+      trans_on_diff_Id
       trans_on_top[simp]
       transp_on_bot[simp]
       transp_on_top[simp]
diff -r c6193fc5ea3c -r 6c68eff8355a src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Mar 21 14:35:11 2025 +0100
+++ b/src/HOL/Relation.thy	Fri Mar 21 16:42:20 2025 +0100
@@ -1013,8 +1013,11 @@
 lemma irrefl_diff_Id [simp]: "irrefl (r - Id)"
   by (simp add: irrefl_def)
 
-lemma trans_diff_Id: "trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r - Id)"
-  unfolding antisym_def trans_def by blast
+lemma trans_on_diff_Id: "trans_on A r \<Longrightarrow> antisym_on A r \<Longrightarrow> trans_on A (r - Id)"
+  by (blast intro: trans_onI dest: trans_onD antisym_onD)
+
+lemma trans_diff_Id[no_atp]: "trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r - Id)"
+  using trans_on_diff_Id .
 
 lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
   by (simp add: total_on_def)
diff -r c6193fc5ea3c -r 6c68eff8355a src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Mar 21 14:35:11 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Fri Mar 21 16:42:20 2025 +0100
@@ -524,7 +524,7 @@
 text \<open>Well-foundedness of subsets\<close>
 
 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
-  by (simp add: wf_eq_minimal) fast
+  using wf_on_antimono[OF subset_UNIV, unfolded le_bool_def] ..
 
 lemmas wfp_subset = wf_subset [to_pred]