# HG changeset patch
# User desharna
# Date 1671435044 -3600
# Node ID da062f9f2e53adc759003817cd399d5dc041a046
# Parent  ca258cf6c9779c4e3f126efd7769ac93000cd5f7
strengthened and renamed lemma sym_converse and added lemma symp_on_conversep

diff -r ca258cf6c977 -r da062f9f2e53 NEWS
--- a/NEWS	Mon Dec 19 08:18:07 2022 +0100
+++ b/NEWS	Mon Dec 19 08:30:44 2022 +0100
@@ -49,6 +49,7 @@
       preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
       reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
+      sym_converse[simp] ~> sym_on_converse[simp]
   - Added lemmas.
       antisym_on_if_asymp_on
       antisym_onD
@@ -93,6 +94,7 @@
       sym_on_subset
       symp_onD
       symp_onI
+      symp_on_conversep[simp]
       symp_on_subset
       symp_on_sym_on_eq[pred_set_conv]
       totalI
diff -r ca258cf6c977 -r da062f9f2e53 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 08:18:07 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:30:44 2022 +0100
@@ -1110,8 +1110,11 @@
 lemma irreflp_on_converse [simp]: "irreflp_on A (r\<inverse>\<inverse>) = irreflp_on A r"
   by (rule irrefl_on_converse[to_pred])
 
-lemma sym_converse [simp]: "sym (converse r) = sym r"
-  unfolding sym_def by blast
+lemma sym_on_converse [simp]: "sym_on A (r\<inverse>) = sym_on A r"
+  by (auto intro: sym_onI dest: sym_onD)
+
+lemma symp_on_conversep [simp]: "symp_on A R\<inverse>\<inverse> = symp_on A R"
+  by (rule sym_on_converse[to_pred])
 
 lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
   unfolding antisym_def by blast