--- a/NEWS Wed Dec 21 23:18:28 2022 +0100
+++ b/NEWS Thu Dec 22 08:56:16 2022 +0100
@@ -78,11 +78,13 @@
irrefl_onD
irrefl_onI
irrefl_on_converse[simp]
+ irrefl_on_if_asym_on[simp]
irrefl_on_subset
irreflpD
irreflp_onD
irreflp_onI
irreflp_on_converse[simp]
+ irreflp_on_if_asymp_on[simp]
irreflp_on_irrefl_on_eq[pred_set_conv]
irreflp_on_subset
linorder.totalp_on_ge[simp]
--- a/src/HOL/Relation.thy Wed Dec 21 23:18:28 2022 +0100
+++ b/src/HOL/Relation.thy Thu Dec 22 08:56:16 2022 +0100
@@ -393,6 +393,12 @@
lemma asymp_on_subset: "asymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asymp_on B R"
by (auto simp: asymp_on_def)
+lemma irrefl_on_if_asym_on[simp]: "asym_on A r \<Longrightarrow> irrefl_on A r"
+ by (auto intro: irrefl_onI dest: asym_onD)
+
+lemma irreflp_on_if_asymp_on[simp]: "asymp_on A r \<Longrightarrow> irreflp_on A r"
+ by (rule irrefl_on_if_asym_on[to_pred])
+
lemma (in preorder) asymp_on_less[simp]: "asymp_on A (<)"
by (auto intro: dual_order.asym)