# HG changeset patch
# User desharna
# Date 1670255037 -3600
# Node ID 595261b3d03341e4e1df5bbaa59959b876698568
# Parent  d6a2a8bc40e17115e0fcb230ead31f67a5ffafcc# Parent  df6ba3cf7874da470692e84d40f8fb7dd5d10d09
merged

diff -r d6a2a8bc40e1 -r 595261b3d033 NEWS
--- a/NEWS	Mon Dec 05 15:19:52 2022 +0100
+++ b/NEWS	Mon Dec 05 16:43:57 2022 +0100
@@ -26,14 +26,23 @@
     Minor INCOMPATIBILITY.
 
 * Theory "HOL.Relation":
+  - Added predicates irrefl_on and irreflp_on and redefined irrefl and
+    irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
+    explicitly provided for backward compatibility but their usage is
+    discouraged. Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       total_on_singleton
       reflp_equality[simp] ~> reflp_on_equality[simp]
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
-      irreflD
-      irreflpD
+      irrefl_onD
+      irrefl_onI
+      irrefl_on_subset
+      irreflp_onD
+      irreflp_onI
+      irreflp_on_irrefl_on_eq[pred_set_conv]
+      irreflp_on_subset
       linorder.totalp_on_ge[simp]
       linorder.totalp_on_greater[simp]
       linorder.totalp_on_le[simp]
diff -r d6a2a8bc40e1 -r 595261b3d033 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 05 15:19:52 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 05 16:43:57 2022 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Relation.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Stefan Berghofer, TU Muenchen
+    Author:     Martin Desharnais, MPI-INF Saarbruecken
 *)
 
 section \<open>Relations -- as sets of pairs, and binary predicates\<close>
@@ -265,29 +266,65 @@
 
 subsubsection \<open>Irreflexivity\<close>
 
-definition irrefl :: "'a rel \<Rightarrow> bool"
-  where "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)"
+definition irrefl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+  "irrefl_on A r \<longleftrightarrow> (\<forall>a \<in> A. (a, a) \<notin> r)"
+
+abbreviation irrefl :: "'a rel \<Rightarrow> bool" where
+  "irrefl \<equiv> irrefl_on UNIV"
+
+definition irreflp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "irreflp_on A R \<longleftrightarrow> (\<forall>a \<in> A. \<not> R a a)"
 
-definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)"
+abbreviation irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "irreflp \<equiv> irreflp_on UNIV"
+
+lemma irrefl_def[no_atp]: "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)"
+  by (simp add: irrefl_on_def)
+
+lemma irreflp_def[no_atp]: "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)"
+  by (simp add: irreflp_on_def)
+
+text \<open>@{thm [source] irrefl_def} and @{thm [source] irreflp_def} are for backward compatibility.\<close>
 
-lemma irreflp_irrefl_eq [pred_set_conv]: "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R"
-  by (simp add: irrefl_def irreflp_def)
+lemma irreflp_on_irrefl_on_eq [pred_set_conv]: "irreflp_on A (\<lambda>a b. (a, b) \<in> r) \<longleftrightarrow> irrefl_on A r"
+  by (simp add: irrefl_on_def irreflp_on_def)
+
+lemmas irreflp_irrefl_eq = irreflp_on_irrefl_on_eq[of UNIV]
+
+lemma irrefl_onI: "(\<And>a. a \<in> A \<Longrightarrow> (a, a) \<notin> r) \<Longrightarrow> irrefl_on A r"
+  by (simp add: irrefl_on_def)
 
-lemma irreflI [intro?]: "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R"
-  by (simp add: irrefl_def)
+lemma irreflI[intro?]: "(\<And>a. (a, a) \<notin> r) \<Longrightarrow> irrefl r"
+  by (rule irrefl_onI[of UNIV, simplified])
+
+lemma irreflp_onI: "(\<And>a. a \<in> A \<Longrightarrow> \<not> R a a) \<Longrightarrow> irreflp_on A R"
+  by (simp add: irreflp_on_def)
 
-lemma irreflpI [intro?]: "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
-  by (fact irreflI [to_pred])
+lemma irreflpI[intro?]: "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
+  by (rule irreflp_onI[of UNIV, simplified])
+
+lemma irrefl_onD: "irrefl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<notin> r"
+  by (simp add: irrefl_on_def)
 
 lemma irreflD: "irrefl r \<Longrightarrow> (x, x) \<notin> r"
-  unfolding irrefl_def by simp
+  by (rule irrefl_onD[of UNIV, simplified])
+
+lemma irreflp_onD: "irreflp_on A R \<Longrightarrow> a \<in> A \<Longrightarrow> \<not> R a a"
+  by (simp add: irreflp_on_def)
 
 lemma irreflpD: "irreflp R \<Longrightarrow> \<not> R x x"
-  unfolding irreflp_def by simp
+  by (rule irreflp_onD[of UNIV, simplified])
+
+lemma irrefl_on_distinct [code]: "irrefl_on A r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<noteq> b)"
+  by (auto simp add: irrefl_on_def)
 
-lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
-  by (auto simp add: irrefl_def)
+lemmas irrefl_distinct = irrefl_on_distinct \<comment> \<open>For backward compatibility\<close>
+
+lemma irrefl_on_subset: "irrefl_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irrefl_on B r"
+  by (auto simp: irrefl_on_def)
+
+lemma irreflp_on_subset: "irreflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irreflp_on B R"
+  by (auto simp: irreflp_on_def)
 
 lemma (in preorder) irreflp_less[simp]: "irreflp (<)"
   by (simp add: irreflpI)
diff -r d6a2a8bc40e1 -r 595261b3d033 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Dec 05 15:19:52 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 05 16:43:57 2022 +0100
@@ -75,7 +75,7 @@
   using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
 
 lemma wfP_imp_irreflp: "wfP r \<Longrightarrow> irreflp r"
-  by (rule wf_imp_irrefl[to_pred])
+  by (rule wf_imp_irrefl[to_pred, folded top_set_def])
 
 lemma wf_wellorderI:
   assumes wf: "wf {(x::'a::ord, y). x < y}"