# 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\\) = 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\) = sym_on A r" + by (auto intro: sym_onI dest: sym_onD) + +lemma symp_on_conversep [simp]: "symp_on A R\\ = 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