--- 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]
--- 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)
--- 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>
--- 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
--- 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
--- 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>