# HG changeset patch # User desharna # Date 1671098101 -3600 # Node ID 8eb23d34323b9c38b7db5c360af83e04c21aa601 # Parent e322abb912af69f1e80f46e36f6d1acc38f6b284 added lemmas antisym_onD and antisymp_onD diff -r e322abb912af -r 8eb23d34323b NEWS --- a/NEWS Thu Dec 15 10:51:46 2022 +0100 +++ b/NEWS Thu Dec 15 10:55:01 2022 +0100 @@ -41,8 +41,10 @@ total_on_singleton - Added lemmas. antisym_if_asymp + antisym_onD antisym_onI antisymp_if_asymp + antisymp_onD antisymp_onI antisymp_on_antisym_on_eq[pred_set_conv] asym_if_irrefl_and_trans diff -r e322abb912af -r 8eb23d34323b src/HOL/Relation.thy --- a/src/HOL/Relation.thy Thu Dec 15 10:51:46 2022 +0100 +++ b/src/HOL/Relation.thy Thu Dec 15 10:55:01 2022 +0100 @@ -465,13 +465,21 @@ "(\x y. R x y \ R y x \ x = y) \ antisymp R" by (rule antisymI[to_pred]) +lemma antisym_onD: + "antisym_on A r \ x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r \ x = y" + by (simp add: antisym_on_def) + lemma antisymD [dest?]: - "antisym r \ (a, b) \ r \ (b, a) \ r \ a = b" - unfolding antisym_def by iprover + "antisym r \ (x, y) \ r \ (y, x) \ r \ x = y" + by (simp add: antisym_onD) + +lemma antisymp_onD: + "antisymp_on A R \ x \ A \ y \ A \ R x y \ R y x \ x = y" + by (rule antisym_onD[to_pred]) lemma antisympD [dest?]: - "antisymp r \ r a b \ r b a \ a = b" - by (fact antisymD [to_pred]) + "antisymp R \ R x y \ R y x \ x = y" + by (rule antisymD[to_pred]) lemma antisym_subset: "r \ s \ antisym s \ antisym r"