--- 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
--- 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