# HG changeset patch # User desharna # Date 1671097906 -3600 # Node ID e322abb912af69f1e80f46e36f6d1acc38f6b284 # Parent d8ca2d0e81e57cbb4653700fc4a46e4e113a6e37 added lemmas antisym_onI and antisymp_onI diff -r d8ca2d0e81e5 -r e322abb912af NEWS --- a/NEWS Thu Dec 15 09:44:50 2022 +0100 +++ b/NEWS Thu Dec 15 10:51:46 2022 +0100 @@ -41,7 +41,9 @@ total_on_singleton - Added lemmas. antisym_if_asymp + antisym_onI antisymp_if_asymp + antisymp_onI antisymp_on_antisym_on_eq[pred_set_conv] asym_if_irrefl_and_trans asymp_if_irreflp_and_transp diff -r d8ca2d0e81e5 -r e322abb912af src/HOL/Relation.thy --- a/src/HOL/Relation.thy Thu Dec 15 09:44:50 2022 +0100 +++ b/src/HOL/Relation.thy Thu Dec 15 10:51:46 2022 +0100 @@ -449,13 +449,21 @@ lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] +lemma antisym_onI: + "(\x y. x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r \ x = y) \ antisym_on A r" + unfolding antisym_on_def by simp + lemma antisymI [intro?]: "(\x y. (x, y) \ r \ (y, x) \ r \ x = y) \ antisym r" - unfolding antisym_def by iprover + by (simp add: antisym_onI) + +lemma antisymp_onI: + "(\x y. x \ A \ y \ A \ R x y \ R y x \ x = y) \ antisymp_on A R" + by (rule antisym_onI[to_pred]) lemma antisympI [intro?]: - "(\x y. r x y \ r y x \ x = y) \ antisymp r" - by (fact antisymI [to_pred]) + "(\x y. R x y \ R y x \ x = y) \ antisymp R" + by (rule antisymI[to_pred]) lemma antisymD [dest?]: "antisym r \ (a, b) \ r \ (b, a) \ r \ a = b"