# HG changeset patch
# User desharna
# Date 1654351214 -7200
# Node ID 75e1b94396c6d63ed7d163548831cff7957bb471
# Parent  e5d88927e0177ea5af39b46810319ab0b15a57b9
added lemmas reflp_on_subset, totalp_on_subset, and total_on_subset

diff -r e5d88927e017 -r 75e1b94396c6 NEWS
--- a/NEWS	Sat Jun 04 15:43:34 2022 +0200
+++ b/NEWS	Sat Jun 04 16:00:14 2022 +0200
@@ -41,11 +41,17 @@
 longer. INCOMPATIBILITY.
 
 * Theory "HOL.Relation":
-  - Added lemmas asymp_less and asymp_greater to type class preorder.
   - Added predicate reflp_on and redefined reflp to ab an abbreviation.
     Lemma reflp_def is explicitly provided for backward compatibility
     but its usage is discouraged. Minor INCOMPATIBILITY.
-  - Added lemmas reflp_onI and reflp_onD.
+  - Added lemmas.
+      preorder.asymp_greater
+      preorder.asymp_less
+      reflp_onD
+      reflp_onI
+      reflp_on_subset
+      total_on_subset
+      totalp_on_subset
 
 * Theory "HOL-Library.Multiset":
   - Consolidated operation and fact names.
diff -r e5d88927e017 -r 75e1b94396c6 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Jun 04 15:43:34 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 16:00:14 2022 +0200
@@ -200,6 +200,9 @@
   obtains "r x x"
   using assms by (auto dest: refl_onD simp add: reflp_def)
 
+lemma reflp_on_subset: "reflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> reflp_on B R"
+  by (auto intro: reflp_onI dest: reflp_onD)
+
 lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)"
   unfolding refl_on_def by blast
 
@@ -520,6 +523,12 @@
 lemma totalpD: "totalp R \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x"
   by (simp add: totalp_onD)
 
+lemma total_on_subset: "total_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> total_on B r"
+  by (auto simp: total_on_def)
+
+lemma totalp_on_subset: "totalp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> totalp_on B R"
+  by (auto intro: totalp_onI dest: totalp_onD)
+
 lemma total_on_empty [simp]: "total_on {} r"
   by (simp add: total_on_def)