# HG changeset patch
# User desharna
# Date 1671462049 -3600
# Node ID 11a24dab1880f8d21377124e5128a754a8cc051f
# Parent  b35ffbe82031f139694e3d5192a0b2594cd02e0b
strengthened and renamed lemmas preorder.transp_(ge|gr|le|less)

diff -r b35ffbe82031 -r 11a24dab1880 NEWS
--- a/NEWS	Mon Dec 19 15:54:03 2022 +0100
+++ b/NEWS	Mon Dec 19 16:00:49 2022 +0100
@@ -51,6 +51,10 @@
       preorder.asymp_less[simp] ~> preorder.asymp_on_less[simp]
       preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
       preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
+      preorder.transp_ge[simp] ~> preorder.transp_on_ge[simp]
+      preorder.transp_gr[simp] ~> preorder.transp_on_greater[simp]
+      preorder.transp_le[simp] ~> preorder.transp_on_le[simp]
+      preorder.transp_less[simp] ~> preorder.transp_on_less[simp]
       reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
       sym_converse[simp] ~> sym_on_converse[simp]
diff -r b35ffbe82031 -r 11a24dab1880 src/HOL/Data_Structures/Sorted_Less.thy
--- a/src/HOL/Data_Structures/Sorted_Less.thy	Mon Dec 19 15:54:03 2022 +0100
+++ b/src/HOL/Data_Structures/Sorted_Less.thy	Mon Dec 19 16:00:49 2022 +0100
@@ -20,7 +20,7 @@
 
 declare
   sorted_wrt.simps(2)[simp del]
-  sorted_wrt1[simp] sorted_wrt2[OF transp_less, simp]
+  sorted_wrt1[simp] sorted_wrt2[OF transp_on_less, simp]
 
 lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
 by(simp add: sorted_wrt_Cons)
diff -r b35ffbe82031 -r 11a24dab1880 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Mon Dec 19 15:54:03 2022 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Mon Dec 19 16:00:49 2022 +0100
@@ -432,7 +432,7 @@
 
 context preorder begin
 
-declare transp_le[cont_intro]
+declare transp_on_le[cont_intro]
 
 lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)"
 by(rule monotoneI) simp
@@ -441,7 +441,7 @@
 
 lemma transp_le [cont_intro, simp]:
   "class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
-by(rule preorder.transp_le)
+by(rule preorder.transp_on_le)
 
 context partial_function_definitions begin
 
@@ -561,7 +561,7 @@
      \<And>y. mcont lub ord Sup (\<le>) (\<lambda>x. f x y);
      mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x (t x))"
-unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply)
+unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
 
 lemma mcont2mcont:
   "\<lbrakk>mcont lub' ord' Sup (\<le>) (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
diff -r b35ffbe82031 -r 11a24dab1880 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Dec 19 15:54:03 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Dec 19 16:00:49 2022 +0100
@@ -3458,7 +3458,7 @@
   fix M N :: "'a multiset"
   show "(M < N) = (M \<le> N \<and> \<not> N \<le> M)"
     unfolding less_eq_multiset_def less_multiset_def
-    by (metis irreflp_def irreflp_on_less irreflp_multp transpE transp_less transp_multp)
+    by (metis irreflp_def irreflp_on_less irreflp_multp transpE transp_on_less transp_multp)
 next
   fix M :: "'a multiset"
   show "M \<le> M"
@@ -3468,14 +3468,14 @@
   fix M1 M2 M3 :: "'a multiset"
   show "M1 \<le> M2 \<Longrightarrow> M2 \<le> M3 \<Longrightarrow> M1 \<le> M3"
     unfolding less_eq_multiset_def less_multiset_def
-    using transp_multp[OF transp_less, THEN transpD]
+    using transp_multp[OF transp_on_less, THEN transpD]
     by blast
 next
   fix M N :: "'a multiset"
   show "M \<le> N \<Longrightarrow> N \<le> M \<Longrightarrow> M = N"
     unfolding less_eq_multiset_def less_multiset_def
-    using transp_multp[OF transp_less, THEN transpD]
-    using irreflp_multp[OF transp_less irreflp_on_less, unfolded irreflp_def, rule_format]
+    using transp_multp[OF transp_on_less, THEN transpD]
+    using irreflp_multp[OF transp_on_less irreflp_on_less, unfolded irreflp_def, rule_format]
     by blast
 qed
 
diff -r b35ffbe82031 -r 11a24dab1880 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 19 15:54:03 2022 +0100
+++ b/src/HOL/List.thy	Mon Dec 19 16:00:49 2022 +0100
@@ -5535,7 +5535,7 @@
 next
   assume ?R
   have "i < j \<Longrightarrow> j < length xs \<Longrightarrow> P (xs ! i) (xs ! j)" for i j
-    by(induct i j rule: less_Suc_induct)(simp add: \<open>?R\<close>, meson assms transpE transp_less)
+    by(induct i j rule: less_Suc_induct)(simp add: \<open>?R\<close>, meson assms transpE transp_on_less)
   thus ?L
     by (simp add: sorted_wrt_iff_nth_less)
 qed
diff -r b35ffbe82031 -r 11a24dab1880 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 15:54:03 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 16:00:49 2022 +0100
@@ -718,22 +718,26 @@
 lemma asymp_on_iff_irreflp_on_if_transp: "transp R \<Longrightarrow> asymp_on A R \<longleftrightarrow> irreflp_on A R"
   by (rule asym_on_iff_irrefl_on_if_trans[to_pred])
 
-context preorder
-begin
+lemma (in preorder) transp_on_le[simp]: "transp_on A (\<le>)"
+  by (auto intro: transp_onI order_trans)
+
+lemmas (in preorder) transp_le = transp_on_le[of UNIV]
 
-lemma transp_le[simp]: "transp (\<le>)"
-by(auto simp add: transp_def intro: order_trans)
+lemma (in preorder) transp_on_less[simp]: "transp_on A (<)"
+  by (auto intro: transp_onI less_trans)
+
+lemmas (in preorder) transp_less = transp_on_less[of UNIV]
 
-lemma transp_less[simp]: "transp (<)"
-by(auto simp add: transp_def intro: less_trans)
+lemma (in preorder) transp_on_ge[simp]: "transp_on A (\<ge>)"
+  by (auto intro: transp_onI order_trans)
+
+lemmas (in preorder) transp_ge = transp_on_ge[of UNIV]
 
-lemma transp_ge[simp]: "transp (\<ge>)"
-by(auto simp add: transp_def intro: order_trans)
+lemma (in preorder) transp_on_greater[simp]: "transp_on A (>)"
+  by (auto intro: transp_onI less_trans)
 
-lemma transp_gr[simp]: "transp (>)"
-by(auto simp add: transp_def intro: less_trans)
+lemmas (in preorder) transp_gr = transp_on_greater[of UNIV]
 
-end
 
 subsubsection \<open>Totality\<close>