--- 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]
--- 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)
--- 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]