# HG changeset patch # User desharna # Date 1671658555 -3600 # Node ID 9d9a2731a4e33e41c7b39ac1a74459f9bd057297 # Parent b4a9c907e062cc28d797fe4671912d1be90aa503 added lemmas irrefl_on_if_asym_on[simp] and irreflp_on_if_asymp_on[simp] diff -r b4a9c907e062 -r 9d9a2731a4e3 NEWS --- a/NEWS Wed Dec 21 22:11:16 2022 +0100 +++ b/NEWS Wed Dec 21 22:35:55 2022 +0100 @@ -75,11 +75,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] diff -r b4a9c907e062 -r 9d9a2731a4e3 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Wed Dec 21 22:11:16 2022 +0100 +++ b/src/HOL/Relation.thy Wed Dec 21 22:35:55 2022 +0100 @@ -393,6 +393,12 @@ lemma asymp_on_subset: "asymp_on A R \ B \ A \ asymp_on B R" by (auto simp: asymp_on_def) +lemma irrefl_on_if_asym_on[simp]: "asym_on A r \ irrefl_on A r" + by (auto intro: irrefl_onI dest: asym_onD) + +lemma irreflp_on_if_asymp_on[simp]: "asymp_on A r \ 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)