# HG changeset patch
# User desharna
# Date 1671182917 -3600
# Node ID 3042416b2e657bda86a2c0986093707a1d7c2f27
# Parent  9bbc085fce861123be4f1347afd1f68defd21a5c
added lemmas sym_onD and symp_onD

diff -r 9bbc085fce86 -r 3042416b2e65 NEWS
--- a/NEWS	Fri Dec 16 10:23:51 2022 +0100
+++ b/NEWS	Fri Dec 16 10:28:37 2022 +0100
@@ -79,7 +79,9 @@
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
+      sym_onD
       sym_onI
+      symp_onD
       symp_onI
       symp_on_sym_on_eq[pred_set_conv]
       totalI
diff -r 9bbc085fce86 -r 3042416b2e65 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Dec 16 10:23:51 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 10:28:37 2022 +0100
@@ -408,15 +408,17 @@
   obtains "r a b"
   using assms by (rule symE [to_pred])
 
-lemma symD [dest?]:
-  assumes "sym r" and "(b, a) \<in> r"
-  shows "(a, b) \<in> r"
-  using assms by (rule symE)
+lemma sym_onD: "sym_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+  by (simp add: sym_on_def)
+
+lemma symD [dest?]: "sym r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+  by (simp add: sym_onD)
 
-lemma sympD [dest?]:
-  assumes "symp r" and "r b a"
-  shows "r a b"
-  using assms by (rule symD [to_pred])
+lemma symp_onD: "symp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (rule sym_onD[to_pred])
+
+lemma sympD [dest?]: "symp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (rule symD[to_pred])
 
 lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
   by (fast intro: symI elim: symE)