# HG changeset patch
# User desharna
# Date 1671183015 -3600
# Node ID 8fff4e4d81cb2e4cfb3af749fa209e177df93939
# Parent  3042416b2e657bda86a2c0986093707a1d7c2f27
added lemmas sym_on_subset and symp_on_subset

diff -r 3042416b2e65 -r 8fff4e4d81cb NEWS
--- a/NEWS	Fri Dec 16 10:28:37 2022 +0100
+++ b/NEWS	Fri Dec 16 10:30:15 2022 +0100
@@ -81,8 +81,10 @@
       reflp_on_conversp[simp]
       sym_onD
       sym_onI
+      sym_on_subset
       symp_onD
       symp_onI
+      symp_on_subset
       symp_on_sym_on_eq[pred_set_conv]
       totalI
       totalp_on_converse[simp]
diff -r 3042416b2e65 -r 8fff4e4d81cb src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Dec 16 10:28:37 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 10:30:15 2022 +0100
@@ -386,6 +386,12 @@
 
 lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma sym_on_subset: "sym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> sym_on B r"
+  by (auto simp: sym_on_def)
+
+lemma symp_on_subset: "symp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> symp_on B R"
+  by (auto simp: symp_on_def)
+
 lemma sym_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r) \<Longrightarrow> sym_on A r"
   by (simp add: sym_on_def)