# HG changeset patch # User desharna # Date 1671435423 -3600 # Node ID 98880b2430ea800488a8cf17a11eea825e1862d9 # Parent 0c6aa6c27ba4c2b1e8a10088e75775de23681dc8 strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep diff -r 0c6aa6c27ba4 -r 98880b2430ea NEWS --- a/NEWS Mon Dec 19 08:34:32 2022 +0100 +++ b/NEWS Mon Dec 19 08:37:03 2022 +0100 @@ -50,6 +50,7 @@ reflp_equality[simp] ~> reflp_on_equality[simp] total_on_singleton sym_converse[simp] ~> sym_on_converse[simp] + antisym_converse[simp] ~> antisym_on_converse[simp] - Added lemmas. antisym_onD antisym_onI @@ -58,6 +59,7 @@ antisymp_onD antisymp_onI antisymp_on_antisym_on_eq[pred_set_conv] + antisymp_on_conversep[simp] antisymp_on_if_asymp_on antisymp_on_subset asym_if_irrefl_and_trans diff -r 0c6aa6c27ba4 -r 98880b2430ea src/HOL/Relation.thy --- a/src/HOL/Relation.thy Mon Dec 19 08:34:32 2022 +0100 +++ b/src/HOL/Relation.thy Mon Dec 19 08:37:03 2022 +0100 @@ -1122,8 +1122,11 @@ lemma asymp_on_conversep [simp]: "asymp_on A R\\ = asymp_on A R" by (rule asym_on_converse[to_pred]) -lemma antisym_converse [simp]: "antisym (converse r) = antisym r" - unfolding antisym_def by blast +lemma antisym_on_converse [simp]: "antisym_on A (r\) = antisym_on A r" + by (auto intro: antisym_onI dest: antisym_onD) + +lemma antisymp_on_conversep [simp]: "antisymp_on A R\\ = antisymp_on A R" + by (rule antisym_on_converse[to_pred]) lemma trans_converse [simp]: "trans (converse r) = trans r" unfolding trans_def by blast