--- a/NEWS Mon Dec 19 08:30:44 2022 +0100
+++ b/NEWS Mon Dec 19 08:34:32 2022 +0100
@@ -51,22 +51,24 @@
total_on_singleton
sym_converse[simp] ~> sym_on_converse[simp]
- Added lemmas.
- antisym_on_if_asymp_on
antisym_onD
antisym_onI
+ antisym_on_if_asymp_on
antisym_on_subset
- antisymp_on_if_asymp_on
antisymp_onD
antisymp_onI
antisymp_on_antisym_on_eq[pred_set_conv]
+ antisymp_on_if_asymp_on
antisymp_on_subset
asym_if_irrefl_and_trans
asym_onD
asym_onI
+ asym_on_converse[simp]
asymp_if_irreflp_and_transp
asymp_onD
asymp_onI
asymp_on_asym_on_eq[pred_set_conv]
+ asymp_on_conversep[simp]
irreflD
irrefl_onD
irrefl_onI
--- a/src/HOL/Relation.thy Mon Dec 19 08:30:44 2022 +0100
+++ b/src/HOL/Relation.thy Mon Dec 19 08:34:32 2022 +0100
@@ -1116,6 +1116,12 @@
lemma symp_on_conversep [simp]: "symp_on A R\<inverse>\<inverse> = symp_on A R"
by (rule sym_on_converse[to_pred])
+lemma asym_on_converse [simp]: "asym_on A (r\<inverse>) = asym_on A r"
+ by (auto dest: asym_onD)
+
+lemma asymp_on_conversep [simp]: "asymp_on A R\<inverse>\<inverse> = 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