# HG changeset patch
# User desharna
# Date 1741855316 -3600
# Node ID 8cf503824ccf9981ce516dc99f55b038ede568a4
# Parent  71d9d59d6bb5423badc31655f17d865c5fc55b5a
added lemmas antisym_relation_of[simp], asym_relation_of[simp], sym_relation_of[simp], trans_relation_of[simp]

diff -r 71d9d59d6bb5 -r 8cf503824ccf NEWS
--- a/NEWS	Wed Mar 12 21:53:25 2025 +0100
+++ b/NEWS	Thu Mar 13 09:41:56 2025 +0100
@@ -26,6 +26,13 @@
       wf_on_lex_prod[intro]
       wfp_on_iff_wfp
 
+* Theory "HOL.Order_Relation":
+  - Added lemmas.
+      antisym_relation_of[simp]
+      asym_relation_of[simp]
+      sym_relation_of[simp]
+      trans_relation_of[simp]
+
 * Theory "HOL-Library.Multiset":
   - Renamed lemmas. Minor INCOMPATIBILITY.
       filter_image_mset ~> filter_mset_image_mset
diff -r 71d9d59d6bb5 -r 8cf503824ccf src/HOL/Order_Relation.thy
--- a/src/HOL/Order_Relation.thy	Wed Mar 12 21:53:25 2025 +0100
+++ b/src/HOL/Order_Relation.thy	Thu Mar 13 09:41:56 2025 +0100
@@ -153,6 +153,42 @@
 definition relation_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
   where "relation_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
 
+lemma sym_relation_of[simp]: "sym (relation_of R S) \<longleftrightarrow> symp_on S R"
+proof (rule iffI)
+  show "sym (relation_of R S) \<Longrightarrow> symp_on S R"
+    by (auto simp: relation_of_def intro: symp_onI dest: symD)
+next
+  show "symp_on S R \<Longrightarrow> sym (relation_of R S)"
+    by (auto simp: relation_of_def intro: symI dest: symp_onD)
+qed
+
+lemma asym_relation_of[simp]: "asym (relation_of R S) \<longleftrightarrow> asymp_on S R"
+proof (rule iffI)
+  show "asym (relation_of R S) \<Longrightarrow> asymp_on S R"
+    by (auto simp: relation_of_def intro: asymp_onI dest: asymD)
+next
+  show "asymp_on S R \<Longrightarrow> asym (relation_of R S)"
+    by (auto simp: relation_of_def intro: asymI dest: asymp_onD)
+qed
+
+lemma antisym_relation_of[simp]: "antisym (relation_of R S) \<longleftrightarrow> antisymp_on S R"
+proof (rule iffI)
+  show "antisym (relation_of R S) \<Longrightarrow> antisymp_on S R"
+    by (simp add: antisym_on_def antisymp_on_def relation_of_def)
+next
+  show "antisymp_on S R \<Longrightarrow> antisym (relation_of R S)"
+    by (simp add: antisym_on_def antisymp_on_def relation_of_def)
+qed
+
+lemma trans_relation_of[simp]: "trans (relation_of R S) \<longleftrightarrow> transp_on S R"
+proof (rule iffI)
+  show "trans (relation_of R S) \<Longrightarrow> transp_on S R"
+    by (auto simp: relation_of_def intro: transp_onI dest: transD)
+next
+  show "transp_on S R \<Longrightarrow> trans (relation_of R S)"
+    by (auto simp: relation_of_def intro: transI dest: transp_onD)
+qed
+
 lemma Field_relation_of:
   assumes "relation_of P A \<subseteq> A \<times> A" and "refl_on A (relation_of P A)"
   shows "Field (relation_of P A) = A"