# HG changeset patch
# User desharna
# Date 1671460912 -3600
# Node ID 76f93e2620fef55b99627162830e995fb82d3d08
# Parent  201cbd9027fc0d2de89d3452c3bdb0fda18b9353
added lemmas trans_onI and transp_onI

diff -r 201cbd9027fc -r 76f93e2620fe NEWS
--- a/NEWS	Mon Dec 19 15:36:45 2022 +0100
+++ b/NEWS	Mon Dec 19 15:41:52 2022 +0100
@@ -110,6 +110,8 @@
       totalI
       totalp_on_converse[simp]
       totalp_on_singleton[simp]
+      trans_onI
+      transp_onI
       transp_on_trans_on_eq[pred_set_conv]
 
 * Theory "HOL.Transitive_Closure":
diff -r 201cbd9027fc -r 76f93e2620fe src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 15:36:45 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 15:41:52 2022 +0100
@@ -628,11 +628,21 @@
 
 lemmas transp_trans_eq = transp_on_trans_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
-lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
-  by (unfold trans_def) iprover
+lemma trans_onI:
+  "(\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow>
+  trans_on A r"
+  unfolding trans_on_def
+  by (intro ballI) iprover
 
-lemma transpI [intro?]: "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
-  by (fact transI [to_pred])
+lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
+  by (rule trans_onI)
+
+lemma transp_onI:
+  "(\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z) \<Longrightarrow> transp_on A R"
+  by (rule trans_onI[to_pred])
+
+lemma transpI [intro?]: "(\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z) \<Longrightarrow> transp R"
+  by (rule transI[to_pred])
 
 lemma transE:
   assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"