# HG changeset patch
# User desharna
# Date 1671106705 -3600
# Node ID 878ed0fcb5105309ff72f8cf6234732683397749
# Parent  e9f3f2b0c0a70f28ebfd80ff8d29d513c1d5418e
added lemmas antisym_on_subset and antisymp_on_subset

diff -r e9f3f2b0c0a7 -r 878ed0fcb510 NEWS
--- a/NEWS	Thu Dec 15 12:32:01 2022 +0100
+++ b/NEWS	Thu Dec 15 13:18:25 2022 +0100
@@ -45,10 +45,12 @@
       antisym_if_asymp
       antisym_onD
       antisym_onI
+      antisym_on_subset
       antisymp_if_asymp
       antisymp_onD
       antisymp_onI
       antisymp_on_antisym_on_eq[pred_set_conv]
+      antisymp_on_subset
       asym_if_irrefl_and_trans
       asymp_if_irreflp_and_transp
       irreflD
diff -r e9f3f2b0c0a7 -r 878ed0fcb510 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Dec 15 12:32:01 2022 +0100
+++ b/src/HOL/Relation.thy	Thu Dec 15 13:18:25 2022 +0100
@@ -447,7 +447,13 @@
   "antisymp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym_on A r"
   by (simp add: antisym_on_def antisymp_on_def)
 
-lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV]
+lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
+
+lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
+  by (auto simp: antisym_on_def)
+
+lemma antisymp_on_subset: "antisymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisymp_on B R"
+  by (auto simp: antisymp_on_def)
 
 lemma antisym_onI:
   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym_on A r"