--- a/NEWS Mon Nov 21 14:11:30 2022 +0100
+++ b/NEWS Wed Nov 23 09:54:53 2022 +0100
@@ -38,9 +38,11 @@
antisymp_if_asymp
irrefl_onD
irrefl_onI
+ irrefl_on_subset
irreflp_onD
irreflp_onI
irreflp_on_irrefl_on_eq[pred_set_conv]
+ irreflp_on_subset
linorder.totalp_on_ge[simp]
linorder.totalp_on_greater[simp]
linorder.totalp_on_le[simp]
--- a/src/HOL/Relation.thy Mon Nov 21 14:11:30 2022 +0100
+++ b/src/HOL/Relation.thy Wed Nov 23 09:54:53 2022 +0100
@@ -320,6 +320,12 @@
lemmas irrefl_distinct = irrefl_on_distinct \<comment> \<open>For backward compatibility\<close>
+lemma irrefl_on_subset: "irrefl_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irrefl_on B r"
+ by (auto simp: irrefl_on_def)
+
+lemma irreflp_on_subset: "irreflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irreflp_on B R"
+ by (auto simp: irreflp_on_def)
+
lemma (in preorder) irreflp_less[simp]: "irreflp (<)"
by (simp add: irreflpI)