# HG changeset patch
# User desharna
# Date 1670312623 -3600
# Node ID 66addfbb092328225152645bee42a70599cbbe3e
# Parent  5150e1f62c86069235c0ce167eb144738c68699e# Parent  7bc934b99faf7b0259ef3a0ea22646dc2c1b5d1b
merged

diff -r 5150e1f62c86 -r 66addfbb0923 NEWS
--- a/NEWS	Mon Dec 05 22:46:38 2022 +0100
+++ b/NEWS	Tue Dec 06 08:43:43 2022 +0100
@@ -31,16 +31,22 @@
     explicitly provided for backward compatibility but their usage is
     discouraged. Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+      preorder.irreflp_greater[simp] ~> irreflp_on_greater[simp]
+      preorder.irreflp_less[simp] ~> irreflp_on_less[simp]
+      reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
-      reflp_equality[simp] ~> reflp_on_equality[simp]
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
+      asym_if_irrefl_and_trans
+      asymp_if_irreflp_and_transp
       irrefl_onD
       irrefl_onI
+      irrefl_on_converse[simp]
       irrefl_on_subset
       irreflp_onD
       irreflp_onI
+      irreflp_on_converse[simp]
       irreflp_on_irrefl_on_eq[pred_set_conv]
       irreflp_on_subset
       linorder.totalp_on_ge[simp]
@@ -54,6 +60,8 @@
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
+      totalI
+      totalp_on_converse[simp]
       totalp_on_singleton[simp]
 
 * Theory "HOL.Transitive_Closure":
diff -r 5150e1f62c86 -r 66addfbb0923 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Dec 05 22:46:38 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Dec 06 08:43:43 2022 +0100
@@ -3433,7 +3433,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_less irreflp_multp transpE transp_less transp_multp)
+    by (metis irreflp_def irreflp_on_less irreflp_multp transpE transp_less transp_multp)
 next
   fix M :: "'a multiset"
   show "M \<le> M"
@@ -3450,7 +3450,7 @@
   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_less, unfolded irreflp_def, rule_format]
+    using irreflp_multp[OF transp_less irreflp_on_less, unfolded irreflp_def, rule_format]
     by blast
 qed
 
diff -r 5150e1f62c86 -r 66addfbb0923 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 05 22:46:38 2022 +0100
+++ b/src/HOL/Relation.thy	Tue Dec 06 08:43:43 2022 +0100
@@ -326,11 +326,11 @@
 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)
+lemma (in preorder) irreflp_on_less[simp]: "irreflp_on A (<)"
+  by (simp add: irreflp_onI)
 
-lemma (in preorder) irreflp_greater[simp]: "irreflp (>)"
-  by (simp add: irreflpI)
+lemma (in preorder) irreflp_on_greater[simp]: "irreflp_on A (>)"
+  by (simp add: irreflp_onI)
 
 subsubsection \<open>Asymmetry\<close>
 
@@ -561,6 +561,12 @@
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
   by (simp add: transp_def)
 
+lemma asym_if_irrefl_and_trans: "irrefl R \<Longrightarrow> trans R \<Longrightarrow> asym R"
+  by (auto intro: asymI dest: transD irreflD)
+
+lemma asymp_if_irreflp_and_transp: "irreflp R \<Longrightarrow> transp R \<Longrightarrow> asymp R"
+  by (rule asym_if_irrefl_and_trans[to_pred])
+
 context preorder
 begin
 
@@ -580,26 +586,29 @@
 
 subsubsection \<open>Totality\<close>
 
-definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
-  where "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)"
+definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+  "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)"
 
-lemma total_onI [intro?]:
-  "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r"
-  unfolding total_on_def by blast
+abbreviation total :: "'a rel \<Rightarrow> bool" where
+  "total \<equiv> total_on UNIV"
 
-abbreviation "total \<equiv> total_on UNIV"
-
-definition totalp_on where
+definition totalp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   "totalp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> R x y \<or> R y x)"
 
-abbreviation totalp where
+abbreviation totalp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   "totalp \<equiv> totalp_on UNIV"
 
 lemma totalp_on_refl_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r"
   by (simp add: totalp_on_def total_on_def)
 
-lemma totalp_onI:
-  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp_on A R"
+lemma total_onI [intro?]:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r"
+  unfolding total_on_def by blast
+
+lemma totalI: "(\<And>x y. x \<noteq> y \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total r"
+  by (rule total_onI)
+
+lemma totalp_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp_on A R"
   by (simp add: totalp_on_def)
 
 lemma totalpI: "(\<And>x y. x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp R"
@@ -985,12 +994,18 @@
 lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A"
   by blast
 
-lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
+lemma refl_on_converse [simp]: "refl_on A (r\<inverse>) = refl_on A r"
   by (auto simp: refl_on_def)
 
 lemma reflp_on_conversp [simp]: "reflp_on A R\<inverse>\<inverse> \<longleftrightarrow> reflp_on A R"
   by (auto simp: reflp_on_def)
 
+lemma irrefl_on_converse [simp]: "irrefl_on A (r\<inverse>) = irrefl_on A r"
+  by (simp add: irrefl_on_def)
+
+lemma irreflp_on_converse [simp]: "irreflp_on A (r\<inverse>\<inverse>) = irreflp_on A r"
+  by (rule irrefl_on_converse[to_pred])
+
 lemma sym_converse [simp]: "sym (converse r) = sym r"
   unfolding sym_def by blast
 
@@ -1012,6 +1027,9 @@
 lemma total_on_converse [simp]: "total_on A (r\<inverse>) = total_on A r"
   by (auto simp: total_on_def)
 
+lemma totalp_on_converse [simp]: "totalp_on A R\<inverse>\<inverse> = totalp_on A R"
+  by (rule total_on_converse[to_pred])
+
 lemma finite_converse [iff]: "finite (r\<inverse>) = finite r"
 unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
 by (auto elim: finite_imageD simp: inj_on_def)