# HG changeset patch
# User desharna
# Date 1671460393 -3600
# Node ID d33fc5228aaec7b346e30bd4670add5081a6833a
# Parent  0b5efc6de3858af497e67fe794ce6890338f5f4c
added predicates trans_on and transp_on and redefined trans and transp to be abbreviations

diff -r 0b5efc6de385 -r d33fc5228aae NEWS
--- a/NEWS	Mon Dec 19 14:09:37 2022 +0100
+++ b/NEWS	Mon Dec 19 15:33:13 2022 +0100
@@ -40,6 +40,10 @@
     antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are
     explicitly provided for backward compatibility but their usage is
     discouraged. Minor INCOMPATIBILITY.
+  - Added predicates trans_on and transp_on and redefined trans and transp to
+    be abbreviations. Lemmas trans_def and transp_def are explicitly provided
+    for backward compatibility but their usage is discouraged.
+    Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
       order.antisymp_le[simp] ~> order.antisymp_on_le[simp]
diff -r 0b5efc6de385 -r d33fc5228aae src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 15:33:13 2022 +0100
@@ -603,11 +603,25 @@
 
 subsubsection \<open>Transitivity\<close>
 
-definition trans :: "'a rel \<Rightarrow> bool"
-  where "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
+definition trans_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+  "trans_on A r \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
+
+abbreviation trans :: "'a rel \<Rightarrow> bool" where
+  "trans \<equiv> trans_on UNIV"
+
+definition transp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "transp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. R x y \<longrightarrow> R y z \<longrightarrow> R x z)"
 
-definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)"
+abbreviation transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "transp \<equiv> transp_on UNIV"
+
+lemma trans_def[no_atp]: "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
+  by (simp add: trans_on_def)
+
+lemma transp_def: "transp R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R y z \<longrightarrow> R x z)"
+  by (simp add: transp_on_def)
+
+text \<open>@{thm [source] trans_def} and @{thm [source] transp_def} are for backward compatibility.\<close>
 
 lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r"
   by (simp add: trans_def transp_def)
diff -r 0b5efc6de385 -r d33fc5228aae src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Dec 19 15:33:13 2022 +0100
@@ -400,7 +400,7 @@
   Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
 val mk_reflp = mk_pred \<^const_abbrev>\<open>reflp\<close>;
 val mk_symp = mk_pred \<^const_abbrev>\<open>symp\<close>;
-val mk_transp =  mk_pred \<^const_name>\<open>transp\<close>;
+val mk_transp =  mk_pred \<^const_abbrev>\<open>transp\<close>;
 
 fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
 fun mk_sym thm = thm RS sym;