# HG changeset patch
# User desharna
# Date 1741855719 -3600
# Node ID 8a7620fe0e83c50661e1598b8a118a32b1450342
# Parent  8cf503824ccf9981ce516dc99f55b038ede568a4
added lemmas  irrefl_relation_ofD, refl_relation_ofD, total_relation_ofD

diff -r 8cf503824ccf -r 8a7620fe0e83 NEWS
--- a/NEWS	Thu Mar 13 09:41:56 2025 +0100
+++ b/NEWS	Thu Mar 13 09:48:39 2025 +0100
@@ -30,7 +30,10 @@
   - Added lemmas.
       antisym_relation_of[simp]
       asym_relation_of[simp]
+      irrefl_relation_ofD
+      refl_relation_ofD
       sym_relation_of[simp]
+      total_relation_ofD
       trans_relation_of[simp]
 
 * Theory "HOL-Library.Multiset":
diff -r 8cf503824ccf -r 8a7620fe0e83 src/HOL/Order_Relation.thy
--- a/src/HOL/Order_Relation.thy	Thu Mar 13 09:41:56 2025 +0100
+++ b/src/HOL/Order_Relation.thy	Thu Mar 13 09:48:39 2025 +0100
@@ -153,6 +153,12 @@
 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 refl_relation_ofD: "refl (relation_of R S) \<Longrightarrow> reflp_on S R"
+  by (auto simp: relation_of_def intro: reflp_onI dest: reflD)
+
+lemma irrefl_relation_ofD: "irrefl (relation_of R S) \<Longrightarrow> irreflp_on S R"
+  by (auto simp: relation_of_def intro: irreflp_onI dest: irreflD)
+
 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"
@@ -189,6 +195,9 @@
     by (auto simp: relation_of_def intro: transI dest: transp_onD)
 qed
 
+lemma total_relation_ofD: "total (relation_of R S) \<Longrightarrow> totalp_on S R"
+  by (auto simp: relation_of_def total_on_def intro: totalp_onI)
+
 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"