# HG changeset patch
# User desharna
# Date 1669193693 -3600
# Node ID df6ba3cf7874da470692e84d40f8fb7dd5d10d09
# Parent  4352d0ff165a3b6156f186417ddd6e624b1da3e1
added lemmas irrefl_on_subset and irreflp_on_subset

diff -r 4352d0ff165a -r df6ba3cf7874 NEWS
--- 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]
diff -r 4352d0ff165a -r df6ba3cf7874 src/HOL/Relation.thy
--- 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)